Assertion violation at smt_consequences.cpp:637

[rainoftime]

Hi, for the following formula

(set-logic UF) 
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(assert (! (not (exists ((q0 Bool) (q1 Bool) (q2 Bool)) v11)) :named IP_1))
(declare-const v14 Bool)
(declare-const v15 Bool)
(assert (! (not (forall ((q3 Bool) (q4 Bool) (q5 Bool)) (not (or q3 q3 v8 q4)))) :named IP_2))
(declare-const v16 Bool)
(assert (! (exists ((q6 Bool) (q7 Bool) (q8 Bool)) v12) :named IP_3))
(push 1)
(declare-const v17 Bool)
(declare-const v18 Bool)
(assert (! (not (forall ((q9 Bool) (q10 Bool) (q11 Bool) (q12 Bool)) (not (or q10 q9 q9 v2 v6 v10 q11 v13)))) :named IP_4))
(declare-const v19 Bool)
(declare-const v20 Bool)
(declare-const v21 Bool)
(declare-const v22 Bool)
(assert (! (not (exists ((q13 Bool) (q14 Bool)) v15)) :named IP_5))
(push 1)
(declare-const v23 Bool)
(assert (! (or v18 v14) :named IP_6))
(assert (! (or v18 v16 v9) :named IP_7))
(assert (! (or v1 (or v19 v0 v1) v3 v7 v16 v21 (or v19 v0 v1)) :named IP_8))
(assert (! (or v1) :named IP_9))
(assert (! (or (or v19 v0 v1)) :named IP_10))
(assert (! (or v18) :named IP_11))
(assert (! (or v7) :named IP_12))
(assert (! (or v7 v18 (not v4)) :named IP_13))
(assert (! (or v7 (not v4) (not v4) (or v19 v0 v1) v18) :named IP_14))
(assert (! (or v9 v23 v3 v1 v16 v16 v9) :named IP_15))
(assert (! (or v1 v7 v16 v7 v1 v3 v23 (or v19 v0 v1)) :named IP_16))
(assert (! (or v7) :named IP_17))
(assert (! (or v18) :named IP_18))
(assert (! (or v14 (or v19 v0 v1) v21 v12 v6 (or v19 v0 v1) v1) :named IP_19))
(assert (! (or v23 v1) :named IP_20))
(assert (! (or v1 v18 v21 v14 (not v4)) :named IP_21))
(assert (! (or v1) :named IP_22))
(assert (! (or (not v4) v18 v18) :named IP_23))
(assert (! (or v18 v21 v16 (not v4) v12 v7) :named IP_24))
(assert (! (or v14 v12 v6 v9 v6 v6) :named IP_25))
(assert (! (or v16) :named IP_26))
(assert (! (or (or v19 v0 v1) v1 v18) :named IP_27))
(assert (! (or (not v4) v6 v3) :named IP_28))
(assert (! (or v7 v6 v7) :named IP_29))
(assert (! (or v12 v12) :named IP_30))
(assert (! (or v1) :named IP_32))
(assert (! (or v16) :named IP_33))
(assert (! (or v23 v1 v9 v12 (or v19 v0 v1) v21) :named IP_35))
(check-sat)
(get-consequences (IP_5 IP_19 IP_35 IP_24 IP_2 IP_11 IP_27 IP_14 ) (IP_2 IP_32 IP_26 IP_5 IP_33 IP_14 IP_21 IP_23 ))

z3 7597396 throws an assertion violation

ASSERTION VIOLATION
File: ../src/smt/smt_consequences.cpp
Line: 637
is_sat != l_false
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

Another formula

(set-logic AUFBV)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(assert (! (not (forall ((q0 Bool) (q1 Bool) (q2 Bool) (q3 Bool)) (not (or q3 v0 v6 v9 q2 q0 v1 q2 q2 v7)))) :named IP_1))
(assert (! (or (exists ((q0 Bool) (q1 Bool) (q2 Bool) (q3 Bool)) (not (and q3 v3 v2))) (exists ((q0 Bool) (q1 Bool) (q2 Bool) (q3 Bool)) (not (xor q3 v2 q3 q2 q3 q2 q2 v8 q1)))) :named IP_2))
(push 1)
(assert (! (not (exists ((q4 (_ BitVec 11)) (q5 (_ BitVec 11)) (q6 (_ BitVec 11))) v7)) :named IP_3))
(pop 1)
(declare-const v10 Bool)
(assert (! (or v8) :named IP_4))
(assert (! (or (not (and v0 v4 v7 v7 v8 v7 v8 v4 v8 v8)) v7 v8 v7) :named IP_5))
(assert (! (or v8 v8) :named IP_6))
(assert (! (or (not (and v0 v4 v7 v7 v8 v7 v8 v4 v8 v8)) v7) :named IP_7))
(assert (! (or (not (and v0 v4 v7 v7 v8 v7 v8 v4 v8 v8)) v7 (not (and v0 v4 v7 v7 v8 v7 v8 v4 v8 v8)) v8) :named IP_8))
(assert (! (or v7 v8 (not (and v0 v4 v7 v7 v8 v7 v8 v4 v8 v8)) (not (and v0 v4 v7 v7 v8 v7 v8 v4 v8 v8))) :named IP_9))
(assert (! (or v7) :named IP_10))
(assert (! (or v8) :named IP_11))
(assert (! (or v7 v7 v7 (not (and v0 v4 v7 v7 v8 v7 v8 v4 v8 v8)) (not (and v0 v4 v7 v7 v8 v7 v8 v4 v8 v8)) (not (and v0 v4 v7 v7 v8 v7 v8 v4 v8 v8)) (not (and v0 v4 v7 v7 v8 v7 v8 v4 v8 v8)) v8 (not (and v0 v4 v7 v7 v8 v7 v8 v4 v8 v8)) (not (and v0 v4 v7 v7 v8 v7 v8 v4 v8 v8)) v8 (not (and v0 v4 v7 v7 v8 v7 v8 v4 v8 v8)) (not (and v0 v4 v7 v7 v8 v7 v8 v4 v8 v8)) (not (and v0 v4 v7 v7 v8 v7 v8 v4 v8 v8)) v7) :named IP_12))
(assert (! (or (not (and v0 v4 v7 v7 v8 v7 v8 v4 v8 v8))) :named IP_13))
(assert (! (or (not (and v0 v4 v7 v7 v8 v7 v8 v4 v8 v8))) :named IP_14))
(assert (! (or v7 (not (and v0 v4 v7 v7 v8 v7 v8 v4 v8 v8))) :named IP_15))
(assert (! (or (not (and v0 v4 v7 v7 v8 v7 v8 v4 v8 v8)) (not (and v0 v4 v7 v7 v8 v7 v8 v4 v8 v8)) v8 v8 v8) :named IP_16))
(assert (! (or v8 (not (and v0 v4 v7 v7 v8 v7 v8 v4 v8 v8)) (not (and v0 v4 v7 v7 v8 v7 v8 v4 v8 v8)) v7 (not (and v0 v4 v7 v7 v8 v7 v8 v4 v8 v8))) :named IP_17))
(assert (! (or v8) :named IP_18))
(assert (! (or (not (and v0 v4 v7 v7 v8 v7 v8 v4 v8 v8)) v7) :named IP_19))
(check-sat)
(get-consequences (IP_7 IP_9 IP_6 IP_16 IP_15 IP_1 IP_8 IP_19 ) (IP_15 IP_17 IP_12 IP_2 IP_14 IP_16 IP_10 IP_5 ))