正しい結果はUNSAT（オンラインバージョン）であるはずですが、ローカルではZ33.2がSATを報告します。また、列挙型（データ型）のユニバースとカーディナリティの制約を含む興味深いモデルも生成します。アイデア？ありがとう！
2 に答える
2
待ちは終わりました。4.0がリリースされました。
于 2012-05-09T02:28:25.867 に答える
1
これはバグです。Z3 3.2は、スクリプトの再帰データ型エンジンをインストールしません。したがって、ソートQとTは解釈されないソートとして扱われます。Z34.0はこのバグを修正します。オンラインバージョンはすでにZ34.0を実行しています。そのため、オンラインバージョンで正しい結果が得られました。Z3 3.2では、次の回避策を使用できます。
（set-option：auto-config false）
于 2012-05-08T18:32:58.547 に答える