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

see

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.