z3 - Combining nonlinear Real with linear Int

Question

I've read the posts about nonlinear arithmetic and uninterpreted functions. I'm still very new to SMT world, so apologies if I'm not using the right vocabulary or this is a bad question.

For the following code, there are asserts put onto the stack above an unrelated top-level assert, (assert (> i 10)). However, Z3 returns unsat for the case with Reals (the first push to the first pop). I think this has something to do with an attempt by Z3 to use an Int solver since the first assertion was on an Int, and Z3 assigns e1 to (/ 1.0 2.0), a number with no Int representation, because of the constraint (assert (< e3 1)) (if I remove this constraint, it works). Using (check-sat-using qfnra-nlsat) solves the problem for Reals, but returns unknown for the case of Ints, However, I can still get model for the Int case that satisfies the constraints.

(set-option :global-decls false)

(declare-const i Int)
(assert (> i 10))

(push)
  (declare-const e1 Real)
  (declare-const e2 Real)

  (define-fun e3 () Real (/ e1 e2))
  (assert (> e1 0))
  (assert (> e2 0))
  (assert (< e3 1))

  ;(check-sat-using qfnra-nlsat)
  (check-sat)
(pop)
(push)
  (declare-const e1 Int)
  (declare-const e2 Int)

  (define-fun e3 () Int (div e1 e2))
  (assert (> e2 0))
  (assert (> e3 0))

  ;(check-sat-using qfnra-nlsat)
  (check-sat)
(pop)

Is there single call to check that I can use in all cases, or will I need to use (check-sat-using ...) depending on the types that were asserted on?

Answer 1

Since you are mixing real and integer sorts, I think you'll need to use check-sat-using. From How does Z3 handle non-linear integer arithmetic?:

"the nonlinear real arithmetic (NLSat) solver is not used by default for nonlinear integer problems. It is usually very ineffective on integer problems. Nonetheless, we can force Z3 to use NLSat even for integer problems."

You're forcing Z3 to use the nonlinear real arithmetic solver on the integer constraints with the (check-sat-using qfnra-nlsat). Here's also how to do it in Python with z3py: z3 fails with this system of equations

I imagine at some point in the future (although devs can confirm) you will not have to do this, but the last I heard (see e.g., mixing reals and bit-vectors and Using Z3Py online to prove that n^5 <= 5 ^n for n >= 5), the nonlinear real arithmetic solver tactic is not fully integrated with the other solvers yet.