ProB z3 interface does not work with Z3 version 4.8.8 or newer

Description

Z3's behaviour concerning push/pop has changed.

Environment

None

Activity

Show:

Michael Leuschel October 29, 2020 at 9:32 AM

Michael Leuschel October 27, 2020 at 5:02 PM

Feedback by Niklaj Bjørner:

 

Based on the log, you are doing a pop before retrieving the model. The solver will then not be able to access the state of the satisfiability check. This is for sure changed behavior, but I would argue it is legal behavior and applications can take it into account. Z3 used to compute models after every check and keep them around until new constraints were added, but I find it hard to argue that the state after a pop should be considered on par with the state before. Model building requires access to all decisions that were made during search so it is not possible to build a model after a pop. Furthermore, building models if none were asked for can have significant cost.

Details

Assignee

Reporter

Priority

Created October 27, 2020 at 4:59 PM
Updated October 29, 2020 at 9:32 AM