Soundness bug in QF_NRA

[junzew]

$cat bug.smt2 
(set-logic QF_NRA)
(declare-fun skoX () Real)
(declare-fun skoSQ3 () Real)
(declare-fun pi () Real)
(assert (or (> (* skoX (* skoX (- skoX (+ skoX (/ 1 24))))) 0) (and (not (>= skoSQ3 0)) (or (not (< skoX 0)) (and (not (>= (/ 31415927 10000000) pi)) (and (not (<= pi (/ 15707963 5000000))) (and (not (< (* (/ (- 1) 10000000) (- pi (/ 1 2))) skoX)) (= (+ skoSQ3 skoSQ3) 3))))))))
(check-sat)
(exit)
$cvc4 -q bug.smt2 
sat
$z3 bug.smt2 
unsat
$z3 --version
Z3 version 4.8.9 - 64 bit