Assertion violation on QF_FPLRA formulas at vector.h:370 (opt)

[rainoftime]

Hi, for the following formula, 370.txt

z3 (commit 7f1b147) throws an assertion violation

ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 370
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

Option

(set-option :smt.threads 2)
(set-option :smt.arith.solver 3)

[rainoftime]

Another case with different options

(set-logic QF_FPLRA)
(set-option :opt.priority box)
(set-option :smt.threads 6)
(set-option :smt.phase_selection 5)
(set-option :smt.arith.solver 3)
(declare-const fpv0 Float32)
(declare-const fpv1 Float32)
(declare-const fpv2 Float32)
(declare-const fpv3 Float32)
(declare-const fpv4 Float32)
(declare-const fpv5 Float32)
(declare-const fpv6 Float32)
(declare-const fpv7 Float32)
(declare-const fpv9 Float32)
(declare-const fpv10 Float32)
(declare-const fpv13 Float32)
(declare-const fpv14 Float32)
(declare-const fpv17 Float32)
(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 r0 Real)
(declare-const r1 Real)
(declare-const r2 Real)
(declare-const v11 Bool)
(push 1)
(declare-const v12 Bool)
(assert (and v8 v12 v0 (fp.lt fpv14 fpv6 fpv17) (fp.geq fpv9 fpv14) (distinct r1 r2)))
(declare-const v13 Bool)
(declare-const fpv18 Float32)
(declare-const r4 Real)
(assert (xor (and v8 v12 v0 (fp.lt fpv14 fpv6 fpv17) (fp.geq fpv9 fpv14) (distinct r1 r2)) v1 (and v0 v11 v7 v2 (fp.lt fpv14 fpv6 fpv17) v11 v11 v9 v5 (distinct r0 r0)) v1 v11 (fp.geq fpv9 fpv14) v2))
(assert (xor v13 (distinct r0 r0) (and v0 v11 v7 v2 (fp.lt fpv14 fpv6 fpv17) v11 v11 v9 v5 (distinct r0 r0)) v0))
(declare-const v14 Bool)
(declare-const v15 Bool)
(assert (not v1))
(maximize r0)
(maximize r1)
(minimize r2)
(minimize r4)
(check-sat)