Empty model in z3

Question

z3py snippet:

x = Int('x') s = Solver() s.add(x <= x) print s.check() print s.model() print s.model().sexpr() 

http://rise4fun.com/Z3Py/mfPU

Output:

 sat [] 

Any value of x will do, but z3 returns an empty model. Does the missing free variable x in the model indicate that any integer value is a valid model?

Answer 1

Yes, in Z3, if a constant (for example, x ) is not displayed in the model, then it doesn’t care. That is, any value of x will satisfy the formula. When evaluating the value of a constant, we can include "model completion". That is, Z3 will use arbitrary interpretation for the characters "not caring." Here is an example http://rise4fun.com/Z3Py/bvVO

 x = Int('x') s = Solver() s.add(x <= x) print s.check() m = s.model() print m.evaluate(x) print m.evaluate(x, model_completion=True) print m