QF_UF
ロジック フラグメントを使用した (大きな) SMT-LIBv2 入力ファイルがあります。unsat
Z3 は、ファイルが数秒であると判断できます。ただし、プルーフ プロダクションをオンにすると、z3 はunknown
わずか数秒後にレポートを作成し、大量のメモリ リソースを使用しません。同じファイルを別のソルバー (veriT) で試すと、わずか数秒で証明 (~500 KB) を取得できます。
QF_UF
決定可能なフラグメントであり、ファイルもそれほど難しくないように見えるため、この結果にはかなり驚いています。私たちの推測では、z3 はある種の内部リソース制限を使い果たしていると考えられます。2 つの質問があります。なぜ z3 があきらめて報告するのかを調べる方法はありますunknown
か? また、これが何らかの内部制限によるものである場合、構成設定によってこれを増やすことはできますか?