model translation failed due to Z3 using lambda
Description
Environment
None
Activity
Show:
Michael Leuschel October 28, 2020 at 9:51 AM
This now works in commit 52a5a309d756d4a0e810d6a001670843d97f8d32
Michael Leuschel October 27, 2020 at 5:18 PM
When debugging we can see the model string that is returned by Z3:
z3: called get_model_string(2,(lambda ((x!1 Int)) (and (<= 2 x!1) (not (<= 4 x!1)))))
Fixed
Details
Details
Assignee
Michael Leuschel
Michael LeuschelReporter
Michael Leuschel
Michael LeuschelPriority
Created October 27, 2020 at 5:05 PM
Updated October 30, 2020 at 9:54 AM
Resolved October 30, 2020 at 9:54 AM
For the query:
```
:z3 a<:1..3 & 2:a
```
I get Unknown exception in solver z3: model_translation_failed