小编Ven*_*ath的帖子

下面的Python代码段说明了Z3的存储性能行为。在不push()调用的情况下，z3会在0.1秒内检查公式。有了push()（并且没有额外的断言），z3需要0.8s。即使在交换s.append(f)和之后也会发生类似的结果s.push()。

import time
import z3
f = z3.parse_smt2_file("smt-lib/QF_BV/RWS/Example_1.txt.smt2")
s = z3.Solver()
s.append(f)
t1 = time.time()
s.check()  # 0.10693597793579102 seconds
print(time.time() - t1)

s = z3.Solver()
t1 = time.time()
s.append(f)
s.push()
s.check()  # 0.830916166305542 seconds
print(time.time() - t1)

知道为什么会出现这种减速吗？而且，如何解决？

我正在使用z3-4.3.2.bb56885147e4-x64-osx-10.9.2。