queryキーワードを使用して固定小数点クエリを実行しようとすると、「不明な並べ替え」エラーが発生します。たとえば、固定小数点チュートリアルの次の例は、Z3 のオンライン バージョンで正常に動作します。
(declare-rel mc (Int Int))
(declare-var n Int)
(declare-var m Int)
(declare-var p Int)
(rule (=> (> m 100) (mc m (- m 10))))
(rule (=> (and (<= m 100) (mc (+ m 11) p) (mc p n)) (mc m n)))
(query (and (mc m n) (< n 91))
:print-certificate true)
戻り値：
(error "line 9 column 13: unknown sort 'mc'")
コマンドラインから実行すると。Linux の github リポジトリからコンパイルされた Z3 バージョン 4.4.2 を使用します。私のコマンドラインは次のとおりです。z3 -smt2 example.smt
この機能を有効にするために設定する必要があるコンパイル フラグはありますか?