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

Environment

None

Activity

Show:

Michael Leuschel October 30, 2020 at 9:55 AM

This is now solved

>>> :z3 x ={1|->TRUE, 2|->FALSE} & y=x
Result of get_model_string: (store (store ((as const (Array couple Bool)) false) (couple 2 false) true)
       (couple 1 true)
       true)
Result of get_model_string: (store (store ((as const (Array couple Bool)) false) (couple 2 false) true)
       (couple 1 true)
       true)
PREDICATE is TRUE
Solution: 
       x = {(1|->TRUE),(2|->FALSE)}
       y = {(1|->TRUE),(2|->FALSE)}

Michael Leuschel October 27, 2020 at 5:31 PM

A similar issue arises when using cvc4:

cvc4: called get_model_string(2,(UNION (SINGLETON (APPLY_CONSTRUCTOR __cvc4_tuple_ctor (CONST_RATIONAL 1) (CONST_BITVECTOR 1))) (SINGLETON (APPLY_CONSTRUCTOR __cvc4_tuple_ctor (CONST_RATIONAL 2) (CONST_BITVECTOR 0)))))
Unknown exception in solver cvc4: model_translation_failed
stopped_timer(3,5133,5130)
smt_result(cvc4,no_solution_found(model_translation_failed))
PREDICATE is UNKNOWN: model_translation_failed
>>> :cvc4 x ={1|->TRUE, 2|->FALSE} & y=x

Michael Leuschel October 27, 2020 at 5:22 PM

When debugging one can see the returned model:

3: called get_full_model_string((define-fun y () (Array couple Bool)
  (_ as-array k!2))
(define-fun x () (Array couple Bool)
  (_ as-array k!2))
(define-fun k!2 ((x!0 couple)) Bool
  (or (= x!0 (couple 1 true)) (= x!0 (couple 2 false))))
)

Fixed

Details

Assignee

Michael Leuschel

Reporter

Michael Leuschel

Priority

Major

Created October 27, 2020 at 5:00 PM

Updated October 30, 2020 at 9:57 AM

Resolved October 30, 2020 at 9:57 AM

Configure