Skip to:

  1. Skip to Jira Navigation
  2. Skip to Side Navigation
  3. Skip to Main Content

No value in model with Z3 4.8.9 or later

Description

>>> :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 = _

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

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
Configure