QF_NIAスクリプトは、Z3 4.3.2で瞬時に終了しますが、4.4.2ではありません

Question

このscriptは、Z3 4.3.2ではほとんど時間のない正しいモデルを生成しますが、数秒後には一見永遠にZ3 4.4.2とタイムアウトで動作しますRise4funで。 n=5（リンクされているものはn=4）のスクリプトのバージョンは、4.3.2でも長時間実行されます。私はsat.random_seedとsmt.random_seedを変更しようとしましたが、役に立たなかった。それ以外に何ができますか？

Answer 1

ありがとうございます。ビットブラスターは、これが有限領域であることを検出するようになりました。 「別個」を処理していなかったので、非常に高価なグレブナー塩基計算を使用するデフォルトのソルバに戻っていました。それはオフにすることができますが、有限領域検出を修正する方が良いです。