Исключение квантификатора -Дополнительные вопросы

Большое спасибо Джошу и Леонардо за ответ на предыдущий вопрос.

У меня есть еще несколько вопросов.

<1> Рассмотрим другой пример.

(exists k) i * k > = 4 and k > 1.

Это имеет простое решение i > 0. (как для Int, так и для Real)

Однако, когда я попытался выполнить следующее,

(declare-const i Int)
(assert (exists ((k Int)) (and (>= (* i k)  4) (> k 1))))
(apply (using-params qe :qe-nonlinear true))

Z3 Не удалось исключить квантификатор здесь.

Тем не менее, это может исключить реальный случай. (когда i и k оба действительные числа )Является ли исключение квантификаторов более сложным для целых чисел?

<2> Я использую Z3 C API в своей системе. Я добавляю в свою систему некоторые нелинейные -ограничения на целые числа с кванторами. В настоящее время Z3 проверяет выполнимость и дает мне правильную модель, когда система выполнима.

Я знаю, что после исключения квантификатора эти ограничения сводятся к линейным ограничениям.

Я думал, что z3 автоматически устраняет квантификатор перед проверкой выполнимости. Но поскольку он не мог этого сделать в случае 1 выше, теперь я думаю, что он обычно находит модель без исключения квантификатора. Я прав?

В настоящее время z3 может устранить ограничения в моей системе. Но это может привести к сбою в сложных системах. В таком случае, это хорошая идея, чтобы удалить квантификатор каким-либо другим методом без z3 и добавить ограничения к z3 позже?

<3> Я могу подумать о добавлении вещественных нелинейных -ограничений вместо целочисленных нелинейных -ограничений в моей системе. В этом случае, как я могу заставить z3 выполнять исключение квантификатора с помощью C -API?

<4> Наконец, стоит ли заставлять z3 выполнять исключение квантификатора? Или обычно он находит модель более разумно, не выполняя исключение квантификатора?

Спасибо.