Assertion violation at smt/theory_utvpi_def.h:862

[rainoftime]

Hi, for the following formula,

(set-logic AUFNIRA)
(declare-fun _substvar_15_ () Bool)
(declare-fun _substvar_23_ () Bool)
(set-option :smt.arith.solver 4)
(declare-const r5 Real)
(assert (not (exists ((q3 Bool) (q4 Real)) (< r5 0.0 r5 0.4467963 472603.7747))))
(assert _substvar_23_)
(assert _substvar_15_)
(check-sat-using (then simplify qe2))

z3 (commit dc9221e) throws an assertion violation

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