Assertion violation at theory_diff_logic_def.h:955 (smt.arith.solver 1)

[rainoftime]

Hi, for the following formula, z3 8fe3caa throws an assertion violation

ASSERTION VIOLATION
File: ../src/smt/theory_diff_logic_def.h
Line: 955
(asgn == l_true) == a->is_true()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

(set-logic QF_AUFNIA)
(set-option :smt.arith.solver 1)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const i1 Int)
(declare-const i3 Int)
(declare-const i5 Int)
(declare-const i6 Int)
(declare-const i8 Int)
(declare-const i14 Int)
(declare-const i16 Int)
(declare-const v5 Bool)
(assert (! (or (<= i3 i16) (> 20 i14) (xor (<= i3 i16) v2 v2 v1 (> i14 i6) v2 v2 v3 v2 v2)) :named IP_1))
(assert (! (or (> 20 i14) (> 4 i14) (>= i8 i14) (> 4 i14)) :named IP_2))
(assert (! (or v2 v5) :named IP_3))
(assert (! (or (>= i8 i14) (>= i8 i14) (<= i3 i16) (<= i3 i16) v2) :named IP_4))
(assert (! (or v2) :named IP_5))
(assert (! (or (xor (<= i3 i16) v2 v2 v1 (> i14 i6) v2 v2 v3 v2 v2) (xor (<= i3 i16) v2 v2 v1 (> i14 i6) v2 v2 v3 v2 v2) (> 4 i14)) :named IP_6))
(assert (! (or (>= i8 i14) (> 4 i14) (> 4 i14) v0 (> 20 i14)) :named IP_7))
(assert (! (or (xor (<= i3 i16) v2 v2 v1 (> i14 i6) v2 v2 v3 v2 v2) (xor (<= i3 i16) v2 v2 v1 (> i14 i6) v2 v2 v3 v2 v2)) :named IP_8))
(assert (! (or (xor (<= i3 i16) v2 v2 v1 (> i14 i6) v2 v2 v3 v2 v2) (<= i3 i16) (> 4 i14) (> 20 i14) v2) :named IP_9))
(assert (! (or (> 4 i14) v0) :named IP_10))
(assert (! (or v5 (> 4 i14)) :named IP_11))
(assert (! (or v5 (> 4 i14) v2 v2 v0 (> 20 i14)) :named IP_12))
(assert (! (or v5 v0 (> 20 i14) (xor (<= i3 i16) v2 v2 v1 (> i14 i6) v2 v2 v3 v2 v2) (> 20 i14) (> 4 i14) v0 v5) :named IP_13))
(assert (! (or (>= i8 i14)) :named IP_14))
(assert (! (or (> 4 i14) v0 (xor (<= i3 i16) v2 v2 v1 (> i14 i6) v2 v2 v3 v2 v2) v2) :named IP_15))
(assert (! (or v0 (> 4 i14) (> 4 i14)) :named IP_16))
(assert (! (or (> 4 i14)) :named IP_17))
(assert (! (or (xor (<= i3 i16) v2 v2 v1 (> i14 i6) v2 v2 v3 v2 v2) (> 20 i14)) :named IP_21))
(check-sat)
(get-consequences (IP_16 IP_6 IP_11  IP_13 IP_1 IP_2 IP_3 ) (IP_6 IP_13 IP_11 IP_5 ))
(get-consequences (IP_10 IP_16 IP_13 IP_6 IP_9 ) (IP_1 IP_21 IP_7 IP_11 IP_2 IP_5 IP_13 IP_6 ))