Assertion violation at smt_internalizer.cpp:660

[rainoftime]

Hi, for the following instance,

(set-logic QF_UFNRA)
(set-option :parallel.enable true)
(set-option :rewriter.arith_ineq_lhs true)
(set-option :parallel.conquer.delay 1)
(set-option :smt.random_seed 2)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const r0 Real)
(declare-const r1 Real)
(declare-const v3 Bool)
(declare-const r2 Real)
(assert (or (> (/ r0 r0) r2 (* r1 r0 r2)) (= r2 r1) (> (/ r0 r0) r2 (* r1 r0 r2)) v2 (> (/ r0 r0) r2 (* r1 r0 r2)) (= (xor v0 v0) (= v3 v3 (xor v0 v0) v1 (xor v0 v0)) (> (/ r0 r0) r1 r2 r1 r2) (distinct r0 r1 r2 r1) (> (/ r0 r0) r1 r2 r1 r2) (xor (distinct v1 v2 (xor v0 v0) (> (/ r0 r0) (/ r0 r0) (/ r0 r0) (/ r0 r0) r0) (xor v0 v0) (= v3 v3 (xor v0 v0) v1 (xor v0 v0)) v2 v2) v2 v1) (xor (distinct r0 r1 r2 r1) v3 (distinct v1 v2 (xor v0 v0) (> (/ r0 r0) (/ r0 r0) (/ r0 r0) (/ r0 r0) r0) (xor v0 v0) (= v3 v3 (xor v0 v0) v1 (xor v0 v0)) v2 v2)) (xor (distinct r0 r1 r2 r1) v3 (distinct v1 v2 (xor v0 v0) (> (/ r0 r0) (/ r0 r0) (/ r0 r0) (/ r0 r0) r0) (xor v0 v0) (= v3 v3 (xor v0 v0) v1 (xor v0 v0)) v2 v2))) v2))
(assert (or v2))
(assert (or (> (/ r0 r0) r2 (* r1 r0 r2)) (= (xor v0 v0) (= v3 v3 (xor v0 v0) v1 (xor v0 v0)) (> (/ r0 r0) r1 r2 r1 r2) (distinct r0 r1 r2 r1) (> (/ r0 r0) r1 r2 r1 r2) (xor (distinct v1 v2 (xor v0 v0) (> (/ r0 r0) (/ r0 r0) (/ r0 r0) (/ r0 r0) r0) (xor v0 v0) (= v3 v3 (xor v0 v0) v1 (xor v0 v0)) v2 v2) v2 v1) (xor (distinct r0 r1 r2 r1) v3 (distinct v1 v2 (xor v0 v0) (> (/ r0 r0) (/ r0 r0) (/ r0 r0) (/ r0 r0) r0) (xor v0 v0) (= v3 v3 (xor v0 v0) v1 (xor v0 v0)) v2 v2)) (xor (distinct r0 r1 r2 r1) v3 (distinct v1 v2 (xor v0 v0) (> (/ r0 r0) (/ r0 r0) (/ r0 r0) (/ r0 r0) r0) (xor v0 v0) (= v3 v3 (xor v0 v0) v1 (xor v0 v0)) v2 v2))) v0 (distinct r0 r1 r2 r1)))
(check-sat-using (then simplify ctx-solver-simplify qfbv))

z3 commit cf0952c throws an assertion violation

File: ../src/smt/smt_internalizer.cpp
Line: 660
UNREACHABLE CODE WAS REACHED

[NikolajBjorner]

why is this qfbv?