python - Z3 結果のランダム性

Question

私が書いている研究ツールの一部として Z3 Python インターフェイスを使用しています。同じクエリで Z3 ソルバーを繰り返し実行すると、かなり奇妙な動作に気付きました。特に、毎回同じ結果が得られないようです。実行する前にソルバーを明示的にリセットしましたが。参考までに、私のコードは次のとおりです。

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 ""

上記のコードは、Z3 ソルバーを 3 回再作成し、同じクエリの充足可能性をチェックします。クエリはここにあります。

上記のコード セクションは、私が Z3 Python インターフェースをどのように使用するかを正確に示したものではありませんが、問題は、Z3 ソルバーが同じクエリのコードの異なるポイントで 2 回呼び出されたときに、異なる結果を返すという認識から生じました。これが意図的なものなのか、これを無効にする方法や決定論を保証する方法があるのか​​ どうか疑問に思っていました.