Z3無效的功能應用：不假

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沒有抱怨，這不是我首先考慮的事情。