Soundness bug in QF_NRA

[numairmansur]

Hi,
For the following satisfiable file, I get unsat:

(set-logic QF_NRA)
(declare-fun skoS () Real)
(declare-fun skoC () Real)
(declare-fun skoX () Real)
(assert
 (let (($x77 (not (<= (* skoC (/ 400.0 441.0)) skoS))))
 (let (($x108 (not (not (and (not (and (<= skoX 75.0) (<= 0.0 skoX))) $x77)))))
 (not (not (not $x108))))))
(assert
 (let (($x77 (not (<= (* skoC (/ 400.0 441.0)) skoS))))
 (let (($x108 (not (not (and (not (and (<= skoX 75.0) (<= 0.0 skoX))) $x77)))))
 (let (($x24 (not (not (not $x108)))))
 (let (($x65 (<= 0.0 skoX)))
 (let (($x198 (not $x65)))
 (let (($x91 (<= skoX 75.0)))
 (let (($x68 (and $x91 $x65)))
 (let (($x214 (<= 0.0 skoC)))
 (let (($x123 (not (<= skoX (/ 1570.0 21.0)))))
 (let (($x109 (or $x123 $x214)))
 (let (($x168 (or $x198 $x109)))
 (let (($x50 (and (not (not $x168)) (and $x168 $x68))))
 (let ((?x21 (+ (+ (/ 460.0 11.0) (* skoC (/ 1600.0 33.0))) (* skoS (/ (- 588.0) 11.0)))))
 (let ((?x33 (+ (+ (/ (- 19343.0) 165000000.0) (* skoC (/ (- 841.0) 6187500.0))) (* skoS (/ 41209.0 275000000.0)))))
 (let ((?x126 (+ (+ (/ (- 667.0) 5500.0) (* skoC (/ 116.0 825.0))) (* skoS (/ (- 4263.0) 27500.0)))))
 (let (($x159 (and (not (not (not (<= (* skoX (+ ?x126 (* skoX ?x33))) ?x21)))) (not (and (and $x50 (not $x77)) $x198)))))
 (let (($x19 (not $x123)))
 (let ((?x90 (* skoS skoS)))
 (let (($x43 (= ?x90 (+ 1.0 (* skoC (* skoC (- 1.0)))))))
 (let (($x66 (and $x43 $x19)))
 (let (($x178 (and (not (not (and $x66 (and $x66 (not (not (and $x214 $x19))))))) $x19)))
 (let ((?x25 (+ (+ (/ 88320.0 11.0) (* skoC (/ 102400.0 11.0))) (* skoS (/ (- 112896.0) 11.0)))))
 (let ((?x78 (* skoX (+ (/ (- 471756427.0) 1718750000000000000.0) (* skoX (/ (- 13680936383.0) 103125000000000000000000.0))))))
 (let ((?x29 (* skoX (+ (/ (- 560947.0) 2148437500.0) (* skoX (+ (/ (- 113872241.0) 343750000000000.0) ?x78))))))
 (let ((?x146 (* skoX (+ (/ (- 64032.0) 1375.0) (* skoX (+ (/ (- 116058.0) 859375.0) ?x29))))))
 (let (($x166 (and (and (and $x214 $x123) (not (not (<= ?x146 ?x25)))) (or $x123 (<= 0.0 skoS)))))
 (let (($x129 (and (and (and (and (not $x198) $x198) (not $x198)) (not (not (not $x166)))) $x50)))
 (let (($x150 (and (not (and (and (and (not $x91) (and $x109 $x91)) $x129) $x168)) $x43)))
 (let (($x158 (and (and (not (and (and (not $x198) $x166) (not (not $x109)))) $x150) (and $x178 (not (not $x159))))))
 (not (not (and (and $x24 (not (not $x158))) $x24)))))))))))))))))))))))))))))))))
(check-sat)

$ ./yices-smt2 --version

Yices 2.6.2
Copyright SRI International.
Linked with GMP 6.1.2
Copyright Free Software Foundation, Inc.
Build date: 2020-08-01
Platform: x86_64-pc-linux-gnu (release)
Revision: e51be0d6ec48c737849798f1a54c04a9ee409636