z3 - 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

...有人知道该怎么做吗？我正在使用带有新求解器 API 的 Z3 版本 4.3.1。

valgrind不报告任何内存违规。

Answer 1

term问题是错误的Z3_context。错误消息只是有点误导，而且valgrind没有抱怨这不是我首先考虑的事情。