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.