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

I have two independent assertions one in non-linear arithmetic and other uninterpreted functions. Z3 gives a "model is not available" to the problem above. Is there a way to set the logic to something that can handle both at the same time? Thank you.

user
  • 5,335
  • 7
  • 47
  • 63
Hesam
  • 31
  • 2

1 Answers1

1

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

Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53