Randomness in Z3 Results

Question

I am using the Z3 Python interface as part of a research tool that I am writing, and I noticed some pretty odd behavior when I run the Z3 solver repeatedly on the same query: In particular, I seem to not get the same results each time, even though I explicitly reset the solver before running. For reference, here's my code:

import z3

with open("query.smt", "r") as smt_reader:
    query_lines = "".join(smt_reader.readlines())
    for i in xrange(3):
        solver = z3.Solver()
        solver.reset()

        queryExpr = z3.parse_smt2_string(query_lines)
        equivalences = queryExpr.children()[:-1]
        for equivalence in equivalences:
            solver.add(equivalence)

        # Obtain the Boolean variables associated with the constraints.
        constraintVars = [equivalence.children()[0] for equivalence
                          in equivalences]
        # Check the satisfiability of the query.
        querySatResult = solver.check(*constraintVars)

        print solver.model().sexpr()
        print solver.statistics()
        print ""

The code above re-creates the Z3 solver thrice and checks the satisfiability of the same query. The query is located here.

While the above section of code is not exactly how I will be using the Z3 Python interface, the problem stemmed from a realization that the Z3 solver, when called twice at different points of the code on the same query, returned different results. I was wondering if this was intentional, and whether there was any way to disable this or to ensure determinism.

Answer 1

I'm assuming by different you meant a different model. If the result changes from sat to unsat, then it is a bug.

That being said, if we solve the same problem twice in the same execution path, then Z3 can produce different models. Z3 assigns internal unique IDs to expressions. The internal IDs are used to break ties in some heuristics used by Z3. Note that the loop in your program is creating/deleting expressions. So, in each iteration, the expressions representing your constraints may have different internal IDs, and consequently the solver may produce different solutions.

See the following related question:

• Z3 timing variation