z3_set_to_b_set failed on fun / result pair ['k!2',couple(integer,boolean)]
Description
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
Details
Assignee
Michael Leuschel
Michael LeuschelReporter
Michael Leuschel
Michael LeuschelPriority
Created October 27, 2020 at 5:00 PM
Updated October 30, 2020 at 9:57 AM
Resolved October 30, 2020 at 9:57 AM
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)]