Z3 C-API を使用して、非線形整数演算 (NIA) の制約を含むいくつかの問題を解決しています。Linuxにz3 4.0を使用しています。Z3 C-API を呼び出すプログラムを実行すると、いくつかの問題でスタックし、応答が返されません (sat、unsat、unknown など)。Z3_check_and_get_model() 呼び出し内でスタックします。10分以上実行してみましたが、応答がありませんでした。バイナリは何らかの作業を続けており、CPU 使用率はほぼ 100% です。
これは非線形の制約が原因で発生していると思いましたが、オンラインの Z3-SMT と -smt2 オプション付きの z3 linux バイナリで同じ例を試したところ、モデルを使用してすぐに解決策が得られました。NIA の領域ではありますが、問題は比較的単純です。
なぜこれが起こっているのかわかりません。-smt2 入力を使用した z3 バイナリと同じパフォーマンスを得るために提供する必要がある構成設定が何かありますか? それともこれはバグですか？