inverse: z3_exception in mk_couple : Sort mismatch at argument #1 for function
Description
Environment
None
Activity
Show:

Michael Leuschel October 29, 2020 at 1:51 PM
This also seems to be the reason that test 1947 fails and had to be skipped, I get:
z3_exception in mk_couple : Sort mismatch at argument #1 for function (declare-fun couple (K (Array A Bool)) couple) supplied sort is L
PREDICATE is UNKNOWN: Sort mismatch at argument #1 for function (declare-fun couple (K (Array A Bool)) couple) supplied sort is L
### Evaluation error, expected result to be: TRUE (but was UNKNOWN) in :z3 x:liefert[{l1}] & k|->b : bes & x:b

Michael Leuschel October 27, 2020 at 5:36 PM
With version 1.6.1 of ProB and 4.4.1 of Z3 it all still worked:

Michael Leuschel October 27, 2020 at 5:17 PM
There seems to be a problem as soon as couples of different types are used, e.g. for
:z3 x ={1|->TRUE, 2|->FALSE} & y= {TRUE|->FALSE}
Details
Details
Assignee

Reporter

Priority
Created October 27, 2020 at 5:01 PM
Updated October 29, 2020 at 1:51 PM
For
```
:z3 x ={1|>TRUE, 2|>FALSE} & y=x~
```
I get z3_exception in mk_couple : Sort mismatch at argument #1 for function (declare-fun couple (Bool Int) couple) supplied sort is Int