z3 - Z3 無効関数適用: false にしない

Question

プログラムに次の行があります。

return Z3_mk_not(ctx, term);

プログラムを実行すると、Z3 はこの行で失敗し、次のエラー メッセージが表示されます。

WARNING: invalid function application, sort mismatch on argument at position 1
WARNING: (define not Bool Bool) applied to: false of sort Bool

Error: type error

...これをどうするか知っている人はいますか？Z3 バージョン 4.3.1 と新しいソルバー API を使用しています。

valgrindメモリ違反は報告されません。

Answer 1

問題のtermは間違っていましたZ3_context。valgrindエラー メッセージはほんの少しだけ誤解を招くものであり、文句を言わなかったという事実とともに、これは私が最初に考えたものではありませんでした。