He leído las publicaciones sobre aritmética no lineal y funciones no interpretadas. Todavía soy muy nuevo en el mundo de SMT, así que pido disculpas si no uso el vocabulario correcto o esta es una mala pregunta.

Para el siguiente código, hay aserciones colocadas en la pila sobre un aserto de nivel superior no relacionado,(assert (> i 10)). Sin embargo, Z3 devuelve unsat para el caso de Reales (el primer impulso al primer pop). Creo que esto tiene algo que ver con un intento de Z3 de usar un solucionador de Int ya que la primera afirmación fue en un Int, y Z3 asigna e1(/ 1.0 2.0), un número sin representación de Int, debido a la restricción(assert (< e3 1)) (Si elimino esta restricción, funciona). Utilizando(check-sat-using qfnra-nlsat) Resuelve el problema para los reales, pero vuelve.unknown para el caso de Ints, sin embargo, todavía puedo obtener un modelo para el caso Int que satisfaga las restricciones.

(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)

¿Hay una sola llamada para verificar que puedo usar en todos los casos, o tendré que usar(check-sat-using ...) Dependiendo de los tipos que fueron declarados?