Skip to:

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

model translation failed due to Z3 using lambda

Description

For the query:
```
:z3 a<:1..3 & 2:a
```
I get Unknown exception in solver z3: model_translation_failed

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

Assignee

Reporter

Priority

Created October 27, 2020 at 5:05 PM
Updated October 30, 2020 at 9:54 AM
Resolved October 30, 2020 at 9:54 AM
Configure