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.

Answer 1

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.