Any of those help Z3 has a new solver (nlsat) for nonlinear arithmetic. It is more efficient than other solvers (

see this article). The new solver is complete for quantifier-free problems. However, the new solver does not support proof generation. If we disable proof generation, then Z3 will use nlsat and easily solve the problem. Based on your question, it seems you are really looking for solutions, thus disabling proof generation does not seem to be an issue.

Moreover, Z3 does not produce approximate solutions (like hand calculators). It uses a precise representation for real algebraic numbers. We can also ask Z3 to display the result in decimal notation (option :pp-decimal).

Here is your example online.

```
(root-obj (+ (^ x 2) (- 2)) 1)
```

```
(- 1.4142135623?)
```

```
(set-option :pp-decimal true)
(declare-const a Real)
(declare-const b Real)
(declare-const c Real)
(assert (= a 1.0))
(assert (= b 1.0))
(assert (> c 0))
(assert (= (+ (* a a) (* b b)) (* c c)))
(check-sat)
(get-model)
```

```
(set-option :pp-decimal true)
(declare-const a Real)
(declare-const b Real)
(declare-const c Real)
(assert (> c 0))
(assert (> a c))
(assert (= (+ (* a a) (* b b)) (* c c)))
(check-sat)
```