CODEWITHSUNDEEP
z3
sean
sean

Reputation: 1832

Z3 complains that assumption is not a propositional variable, even when it actually is

I'm using the Java API. This is a minimal working example for this warning:

HashMap<String, String> cfg = new HashMap<String, String>();
cfg.put("model", "true");
Context ctx = new Context(cfg);
Solver solver = ctx.mkSolver();
BoolExpr a = ctx.mkBoolConst("a");
BoolExpr b = ctx.mkBoolConst("b");
BoolExpr and = ctx.mkAnd(a,b); 
solver.check(and);

For this small program, Z3 complained that:

WARNING: an assumption must be a propositional variable or the negation of one

Unless I misunderstood something, and is a propositional variable, so I do not understand why there is this warning. Moreover, the check method takes an array of BoolExpr as parameters, so why it requires a propositional variable?

My question: can I safely ignore this warning?

Upvotes: 0

Views: 203

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8402

No, and is not a propositional variable, but it's a propositional term (or in other words a BoolExpr). Assumption literals for solver.check(...) need to be variables or the negation of a variable, i.e., a or not a, but not a and b.

This warning is not safe to ignore, because it means that Z3 will ignore those assumptions, i.e., you may get unexpected results.

Just to avoid confusion: the arguments to solver.check(...) are assumption literals, they are not assertions, i.e., if we want to check whether and is satisfiable we need to first assert it and then ask the solver to check without further assumptions, e.g.,

...
solver.assert(and);
solver.check();

Upvotes: 1

Related Questions