If the difference between Solver and Optimize is intended, please add documentation for this.
from z3 import *
s = Optimize()
x = Bool("x")
s.add(x)
s.add(Not(x))
s.check() #unsat
s.model()
Output:
Solver:
from z3 import *
s = Solver()
x = Bool("x")
s.add(x)
s.add(Not(x))
s.check() #unsat
s.model()
Output:
Z3Exception: model is not available
z3py Versions 4.14.1.0, 4.15.4.0
If the difference between Solver and Optimize is intended, please add documentation for this.
Output:
Solver:
Output:
z3py Versions 4.14.1.0, 4.15.4.0