2

UFBV カテゴリのベンチマークを探しています。このカテゴリは、まだ SMT コンペティションに直接参加していません。

確かに、ほとんどの (A)UFLIA ベンチマークは、解釈されていない並べ替えをビットベクトル並べ替えに、整数演算をビットベクトル演算に変更することで、簡単に UFBV ベンチマークに変更できます。これを自動化するためのスクリプトも役立ちます。

よろしく、 Aboubakr Achraf El Ghazi

4

1 に答える 1