Valores mínimos e máximos da variável inteira

Vamos supor uma restrição muito simples:solve(x > 0 && x < 5).

O Z3 (ou qualquer outro solucionador SMT, ou qualquer outra técnica automática) pode calcular os valores mínimo e máximo da variável (inteiro)x que satisfaz as restrições dadas?

No nosso caso, o mínimo é 1 e o máximo é 4.