z3 basic question (python)

May 21, 2015 at 12:46 PM
Edited May 21, 2015 at 12:49 PM
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
Coordinator
May 21, 2015 at 1: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.