Search code examples
pythonz3z3py

z3py, give random solution using seed

from z3 import *

a = Int('a')

s = Solver()
s.add(a > 0)
set_option('smt.arith.random_initial_value', True)
set_option('auto_config', False)
set_option('smt.phase_selection', 5)
set_option('smt.random_seed', 1)

while s.check() == sat:
    m = s.model()
    print m[a]
    s.add(a != m[a])

The result is 

1
2
3
4
5
...

How can I make the random work? Please provide an example in Python using z3py... I already know how to do this in smt... But I am having a real hard time figuring it out how to translate the smt script to python.

Solution

  • This seems to be a duplicate of Z3py, random different solution generation

    Are you trying to ask a different question? Please modify the question if so, if not you can delete it.