Soundness bug on QF_NRA formula (mcsat)

[rainoftime]

Hi, for the following formula

(set-logic QF_NRA) 
(declare-fun v0 () Bool)
(declare-fun v1 () Bool)
(declare-fun v2 () Bool)
(declare-fun v3 () Bool)
(declare-fun v4 () Bool)
(declare-fun v5 () Bool)
(declare-fun v6 () Bool)
(declare-fun v7 () Bool)
(declare-fun v8 () Bool)
(declare-fun v9 () Bool)
(declare-fun v10 () Bool)
(declare-fun v11 () Bool)
(declare-fun v12 () Bool)
(declare-fun v13 () Bool)
(declare-fun v14 () Bool)
(declare-fun r1 () Real)
(declare-fun r2 () Real)
(declare-fun r5 () Real)
(declare-fun r6 () Real)
(declare-fun r10 () Real)
(declare-fun r11 () Real)
(declare-fun v15 () Bool)
(assert (=> v15 v9))
(declare-fun v16 () Bool)
(assert (distinct v12 v15))
(assert v11)
(assert (=> (< 6904.0 34.0) v15))
(declare-fun v17 () Bool)
(assert (and v4 (distinct v12 v15)))
(declare-fun v18 () Bool)
(declare-fun v19 () Bool)
(assert (=> v15 v9))
(assert (and v13 (or (and v4 (distinct v12 v15)) v10)))
(assert (distinct (not v12) v15))
(declare-fun v20 () Bool)
(assert (or v12 (and (and v4 (distinct v12 v15)) v4)))
(assert (=> (distinct v12 v15) v6))
(declare-fun v21 () Bool)
(declare-fun r12 () Real)
(assert (distinct r11 r6))
(assert (xor (and v4 v18) v20))
(assert (distinct r11 r6))
(assert v15)
(assert (distinct v8 (=> (and v13 (or (and v4 (distinct v12 v15)) v10)) (=> (< 6904.0 34.0) v15))))
(check-sat)

smtrat 0e70dd2 gives "sat".
But z3 7f3bdea0 and CVC4 feea2d248e (both latest commits) return "unsat"

set(SMTRAT_Strategy "MCSATFMICPVSOC" CACHE STRING "Used strategy in the solver")