Nonlinear Arithmetic and Uninterpreted Functions

Question

(declare-const x Real) (declare-fun f (Real) Real) (assert (= (f 1.0) 0.0)) (assert (= (* xx) (* 1.0 1.0))) (check-sat) (get-model) 

I have two independent statements, one in nonlinear arithmetic and other non-interpreted functions. Z3 gives the "model unavailable" to the problem described above. Is there a way to set the logic for something that can work at the same time? Thanks.

Answer 1

The new nonlinear solver is not yet integrated with other theories (arrays, non-integrated functions, bit vectors). In Z3 4.0, it can only be used to solve problems containing only non-linear arithmetic statements. This will change in future versions.