z3 - z3.prove は、ソルバーとチェックよりもはるかに高速です

Question

v4.3.1 としてタグ付けされた Codeplex の最新の z3 マスター コードを使用しています。

prove有用な戻り値を持ち、印刷されないような関数が必要です。だから、私は明らかだと思われることを書きました：

def prove2(claim):
    s = Solver()
    s.add(Not(claim))
    if s.check() == unsat:
        return True, []
    return False, s.model()

ただし、このコードの実行はデフォルトの関数よりも大幅に遅くなりますprove。

prove(slimmed)のコードsrc/api/python/z3.pyは次のとおりです。

def prove(claim, **keywords):
    s = Solver()
    s.set(**keywords)
    s.add(Not(claim))
    if keywords.get('show', False):
        print s
    r = s.check()
    if r == unsat:
        print "proved"
    elif r == unknown:
        print "failed to prove"
        print s.model()
    else:
        print "counterexample"
        print s.model()

s.set()コードに追加すると、高速で同じ反例が見つかります。

ここで何が起こっているのですか？

• s.set()一般的に悪いいくつかのオプションを何らかの方法でクリアするためのその空の呼び出しはありますか?
• ..私の特定のテストには悪いですか？
• 他の何か？

デフォルトのソルバー オプションが何であるかを調べようとしましたがstr(s) repr(s)、 、s.__dict__、および google はあまり役に立ちませんでした。

どんなアドバイスでも大歓迎です！