z3.prove намного быстрее, чем решатель и проверка

Я использую последний основной код z3 от Codeplex, помеченный как v4.3.1.

Мне нужна такая функция, как prove, которая имеет полезное возвращаемое значение и не печатает. Итак, я написал то, что казалось очевидным:

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

Однако этот код работает значительно медленнее, чем функция prove по умолчанию.

Код для prove (упрощенный) в 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 не очень помогли.

Любой совет приветствуется!