Я читал посты о нелинейной арифметике и неинтерпретируемых функциях. Я все еще очень плохо знаком с миром SMT, поэтому извиняюсь, если я не использую правильный словарный запас или это плохой вопрос.

Для следующего кода есть утверждения, помещенные в стек над несвязанным утверждением верхнего уровня,(assert (> i 10)), Тем не менее, Z3 возвращает unsat для случая с Reals (первый толчок к первому трепу). Я думаю, что это как-то связано с попыткой Z3 использовать решатель Int, так как первое утверждение было в Int, а Z3 назначает e1(/ 1.0 2.0), число без представления Int из-за ограничения(assert (< e3 1)) (если я уберу это ограничение, оно будет работать). С помощью(check-sat-using qfnra-nlsat) решает проблему для Реалов, но возвращаетunknown для случая Ints, однако, я все еще могу получить модель для случая Int, которая удовлетворяет ограничениям.

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

Есть ли один вызов, чтобы проверить, что я могу использовать во всех случаях, или мне нужно будет использовать(check-sat-using ...) в зависимости от типов, которые были утверждены?