Skip to:

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

inverse: z3_exception in mk_couple : Sort mismatch at argument #1 for function

Description

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

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:

>>> :z3 x={1|->TRUE, 2|->FALSE} & y=x~ PREDICATE is TRUE Solution: x = {(1|->TRUE),(2|->FALSE)} y = {(FALSE|->2),(TRUE|->1)} >>> :z3 x={1|->TRUE, 2|->FALSE} & y={TRUE|->FALSE} PREDICATE is TRUE Solution: x = {(1|->TRUE),(2|->FALSE)} y = {(TRUE|->FALSE)}

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

Assignee

Reporter

Priority

Created October 27, 2020 at 5:01 PM
Updated October 29, 2020 at 1:51 PM
Configure