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