[685] % cvc4 -q small.smt2
sat
[686] % z3release small.smt2
sat
[687] % z3release nlsat.reorder=false nlsat.simplify_conflicts=false rewriter.flat=false small.smt2
unsat
[688] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(assert (>= (* a a) 0))
(assert (> 0 (* a (- 1 a))))
(assert (> 0 (- (ite (= a 0) 0 1))))
(assert (> 0 (+ a (* b (- b)))))
(assert (>= a 0))
(check-sat)
[689] %