z3 basic question (python)

May 21, 2015 at 11:46 AM
Edited May 21, 2015 at 11:49 AM
In [1]: from z3 import *

In [2]: x = Int('x')

In [3]: solve(x < 5, x > 0)
[x = 1]
I want to produce 1,2,3,4.

how should I do?

I dont want to repeat some routine. I mean is there any way to enumerate satisfiable results?

sorry for my english hehe
May 21, 2015 at 12:34 PM
Thanks for your question. Z3 has moved to github and this forum is not active anymore. Please consider posting your question on StackOverflow or open an issue in the new issue tracker here.