Давайте предположим очень простое ограничение:solve(x > 0 && x < 5).

Может Z3 (или любой другой SMT решатель, или любой другой автоматический метод) вычислить минимальное и максимальное значения (целочисленной) переменнойx что удовлетворяет заданным ограничениям?

В нашем случае минимум равен 1, а максимум - 4.