The term
in question was in the wrong Z3_context
. The error message was just slightly misleading, and along with the fact that valgrind
didn't complain this wasn't the thing I considered first.
Z3 invalid function application: not to false
Question
I have the following line in my program:
return Z3_mk_not(ctx, term);
When I run the program, Z3 fails at this line with the following error message:
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
... does anybody know what to make of this? I'm using Z3 version 4.3.1 with the new solvers API.
valgrind
does not report any memory violations.
Solution
Licensed under: CC-BY-SA with attribution
Not affiliated with StackOverflow