test/regress/regress1/nl/red-exp.smt2

   1 ; COMMAND-LINE: --nl-ext=full
   2 ; EXPECT: unsat
   3 (set-logic QF_NRA)
   4 (set-info :status unsat)
   5
   6 (declare-fun a () Real)
   7 (declare-fun b () Real)
   8
   9 (assert (or (= a (* b b)) (and (= a 9) (= b 3))))
  10 (assert (not (= (* a a) (* b b b b))))
  11 (check-sat)