[523] % z3release small.smt2
sat
(
  (define-fun b () Real
    (root-obj (+ (* 2 (^ x 4)) (* (- 2) (^ x 3)) (* (- 2) (^ x 2)) (* 2 x) 1) 2))
  (define-fun a () Real
    (root-obj (+ (* 2 (^ x 4)) (* 2 (^ x 3)) (* (- 2) x) (- 1)) 2))
)
sat
[524] % z3release rewriter.eq2ineq=true small.smt2
unsat
(error "line 7 column 10: model is not available")
sat
[525] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(assert (< b 0 a))
(assert (= (* (+ a b) a) (- b)))
(assert (= (+ (* a a) (* b b)) 1))
(check-sat)
(get-model)

(reset)

(define-fun a () Real (root-obj (+ (* 2 (^ x 4)) (* 2 (^ x 3)) (* (- 2) x) (- 1)) 2))
(define-fun b () Real (root-obj (+ (* 2 (^ x 4)) (* (- 2) (^ x 3)) (* (- 2) (^ x 2)) (* 2 x) 1) 2))
(assert (< b 0 a))
(assert (= (* (+ a b) a) (- b)))
(assert (= (+ (* a a) (* b b)) 1))
(check-sat)
[526] %