Assertion error at src/smt/smt_context.cpp:2017 (Conseq)

[rainoftime]

Hi, for the formula below,
z3 df09cb7

ASSERTION VIOLATION
File: ../src/smt/smt_context.cpp
Line: 2017
m_flushing || !cls->in_reinit_stack()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

(set-option :smt.arith.random_initial_value true)
(set-option :smt.phase_selection 6)
(set-option :smt.arith.solver 2)
(declare-fun uf7_2 (Bool Bool Bool Bool Bool Bool Bool) Bool)
(declare-fun v0 () Bool)
(declare-fun v1 () Bool)
(declare-fun v2 () Bool)
(declare-fun v4 () Bool)
(declare-fun v5 () Bool)
(declare-fun v6 () Bool)
(declare-fun v7 () Bool)
(declare-fun v8 () Bool)
(declare-fun r0 () Real)
(declare-fun r4 () Real)
(declare-fun r5 () Real)
(declare-fun r9 () Real)
(declare-fun r12 () Real)
(declare-fun ufrb3 (Real Real Real) Bool)
(declare-fun v10 () Bool)
(declare-fun v11 () Bool)
(declare-fun r13 () Real)
(declare-fun v13 () Bool)
(declare-fun v14 () Bool)
(declare-fun v15 () Bool)
(declare-fun v16 () Bool)
(declare-sort S0 0)
(declare-fun arr () (Array S0 Real))
(declare-fun v24 () Bool)
(declare-fun r15 () Real)
(declare-fun v30 () Bool)
(declare-fun v32 () Bool)
(declare-fun v36 () Bool)
(assert (! (or (distinct (- r5) r15 0.18 0.996) (= arr arr arr arr arr) (= arr arr arr arr arr)) :named IP_4))
(assert (! (or v24 v16 (distinct v1 v32 v36 v8 (<= (+ r4 r13 r15 (/ r4 r5) 78276.0) r9 r12 1.0 37.0 (+ r0 r12)) (< 463.0 (/ r4 r5) (+ 47322.0 (- (/ r4 r5)) 0.996)))) :named IP_26))
(assert (! (or (distinct 2.0 3.0 r12 422246605.0) (distinct (- r5) r15 0.18 0.996) v16) :named IP_54))
(assert (! (or v14 v15 v16) :named IP_78))
(assert (! (or v30 (distinct v1 v32 v36 v8 (<= (+ r4 r13 r15 (/ r4 r5) 78276.0) r9 r12 1.0 37.0 (+ r0 r12)) (< 463.0 (/ r4 r5) (+ 47322.0 (- (/ r4 r5)) 0.996))) (ufrb3 (+ (- 0.996) 7735.0 0.55997 (* 2.0 r4 r13 r0 (- (/ r4 r5))) 78276.0) r13 0.18)) :named IP_171))
(assert (! (or (distinct (- r5) r15 0.18 0.996) (distinct 2.0 3.0 r12 422246605.0) (distinct 2.0 3.0 r12 422246605.0)) :named IP_296))
(assert (! (or (distinct (- r5) r15 0.18 0.996) (not (= (< 37.0 r4 422246605.0 47322.0 r13) v13 (distinct v10 v0 v13 (= v11 (distinct v10 v4 v4) (>= 463.0 919.0 r4) (distinct v10 v4 v4) v2 v10) v1 (= 37.0 463.0 r5) (uf7_2 v0 v7 (distinct v10 v4 v4) v11 (distinct v10 v4 v4) (distinct v10 v4 v4) v5)) (not v6) v1 v13)) (not (= (< 37.0 r4 422246605.0 47322.0 r13) v13 (distinct v10 v0 v13 (= v11 (distinct v10 v4 v4) (>= 463.0 919.0 r4) (distinct v10 v4 v4) v2 v10) v1 (= 37.0 463.0 r5) (uf7_2 v0 v7 (distinct v10 v4 v4) v11 (distinct v10 v4 v4) (distinct v10 v4 v4) v5)) (not v6) v1 v13))) :named IP_331))
(assert (! (or (not (= (< 37.0 r4 422246605.0 47322.0 r13) v13 (distinct v10 v0 v13 (= v11 (distinct v10 v4 v4) (>= 463.0 919.0 r4) (distinct v10 v4 v4) v2 v10) v1 (= 37.0 463.0 r5) (uf7_2 v0 v7 (distinct v10 v4 v4) v11 (distinct v10 v4 v4) (distinct v10 v4 v4) v5)) (not v6) v1 v13)) (= arr arr arr arr arr) v8) :named IP_347))
(assert (! (or (= arr arr arr arr arr) v30 v8) :named IP_392))
(assert (! (or v8 v14 (= arr arr arr arr arr)) :named IP_402))
(assert (! (or v8 v16 v24) :named IP_420))
(assert (! (or (distinct (- r5) r15 0.18 0.996) v8 (distinct v1 v32 v36 v8 (<= (+ r4 r13 r15 (/ r4 r5) 78276.0) r9 r12 1.0 37.0 (+ r0 r12)) (< 463.0 (/ r4 r5) (+ 47322.0 (- (/ r4 r5)) 0.996)))) :named IP_425))
(assert (! (or v30 (ufrb3 (+ (- 0.996) 7735.0 0.55997 (* 2.0 r4 r13 r0 (- (/ r4 r5))) 78276.0) r13 0.18) (distinct v1 v32 v36 v8 (<= (+ r4 r13 r15 (/ r4 r5) 78276.0) r9 r12 1.0 37.0 (+ r0 r12)) (< 463.0 (/ r4 r5) (+ 47322.0 (- (/ r4 r5)) 0.996)))) :named IP_485))
(assert (! (or v24 (ufrb3 (+ (- 0.996) 7735.0 0.55997 (* 2.0 r4 r13 r0 (- (/ r4 r5))) 78276.0) r13 0.18) (distinct 2.0 3.0 r12 422246605.0)) :named IP_499))
(assert (! (or v24 (not (= (< 37.0 r4 422246605.0 47322.0 r13) v13 (distinct v10 v0 v13 (= v11 (distinct v10 v4 v4) (>= 463.0 919.0 r4) (distinct v10 v4 v4) v2 v10) v1 (= 37.0 463.0 r5) (uf7_2 v0 v7 (distinct v10 v4 v4) v11 (distinct v10 v4 v4) (distinct v10 v4 v4) v5)) (not v6) v1 v13)) (distinct 2.0 3.0 r12 422246605.0)) :named IP_512))
(assert (! (or v24 v16 (distinct v1 v32 v36 v8 (<= (+ r4 r13 r15 (/ r4 r5) 78276.0) r9 r12 1.0 37.0 (+ r0 r12)) (< 463.0 (/ r4 r5) (+ 47322.0 (- (/ r4 r5)) 0.996)))) :named IP_543))
(get-consequences (IP_54 IP_171 IP_512 IP_420 IP_347 IP_499 IP_402 IP_78 ) (IP_4 IP_543 IP_392 IP_296 IP_485 IP_331 IP_26 IP_425 ))