Skip to:

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

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

>>> :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

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
Configure