Assertion violation at diff_logic.h:518 (smt.arith.solver 1)

[rainoftime]

Hi, for the following formula,

(set-logic QF_AUFNIRA)
(set-option :smt.arith.solver 1)
(declare-const r1 Real)
(declare-const r2 Real)
(declare-const arr1 (Array Real Real))
(assert (< 1560.0 6585646.0 r1 0.0 r1))
(declare-const arr2 (Array (Array Real Real) Real))
(push 1)
(assert (<= 52433.4563 52433.4563 r2 (select (store arr2 (store arr1 387.0463851 86061.0) 0) arr1) 0.0))
(check-sat)

z3 (commit 38e0968) throws an assertion violation

ASSERTION VIOLATION
File: ../src/smt/diff_logic.h
Line: 518
is_feasible()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

Another quantified case

(set-logic LIA)
(declare-fun _substvar_21_ () Int)
(set-option :smt.arith.solver 1)
(declare-const i1 Int)
(assert (forall ((q38 Bool)) (>= 431 i1 _substvar_21_ 773 0)))
(push 1)
(assert (not (forall ((q42 Int) (q43 Bool) (q44 Bool)) (= (+ i1 i1) q42))))
(push 1)