z3 - Z3 是否在增量模式下丢弃 pop() 之后的引理？

Question

在增量模式下使用 Z3 时，求解器是否会在执行 pop() 操作后丢弃所有引理？

2012 年，Leonardo de Moura 证实 Z3 实际上会在 pop() [1] 之后丢弃引理。然而，我使用 Z3 4.3.1 的基准测试并没有显示在 pop() 之后 check-sat 的统计显着性能下降。

[1] Efficiency of constraint strengthening in SMT solvers

Answer 1

是的，在 pop() 之后，Z3 丢弃了在该 pop 及其相应推送的范围内派生的所有引理。

很抱歉造成混淆，旧帖子对此并不完全清楚并且已经更新。