No value in model with Z3 4.8.9 or later
Description
Environment
None
Activity
Show:

Michael Leuschel October 29, 2020 at 9:41 AM
This solves it:

Michael Leuschel October 29, 2020 at 9:37 AM
adding p.set("completion",true); does not seem to work

Michael Leuschel October 29, 2020 at 9:33 AM
we have to set model-completion to true
Fixed
Details
Details
Assignee

Reporter

Priority
Created October 29, 2020 at 9:29 AM
Updated October 30, 2020 at 9:58 AM
Resolved October 30, 2020 at 9:58 AM
>>> :z3 x:INTEGER & (x>y & y>z) => x>=z
Warning: No value for z in Z3 model (Z3 version 4.8.9.0); try installing Z3 4.8.7
PREDICATE is TRUE
Solution:
x = 0
y = 0
z = _