z3_set_to_b_set failed on fun / result pair ['k!2',couple(integer,boolean)]

Description

For the query
```
:z3 x ={1|>TRUE, 2|>FALSE} & y=x
```
I get

z3_set_to_b_set failed on fun / result pair ['k!2',couple(integer,boolean)]

Environment

None

Activity

Show:

Michael Leuschel October 30, 2020 at 9:55 AM

This is now solved

Michael Leuschel October 27, 2020 at 5:31 PM

A similar issue arises when using cvc4:

Michael Leuschel October 27, 2020 at 5:22 PM

When debugging one can see the returned model:

Fixed

Details

Assignee

Reporter

Priority

Created October 27, 2020 at 5:00 PM
Updated October 30, 2020 at 9:57 AM
Resolved October 30, 2020 at 9:57 AM