Z3 在增量模式下会在 pop() 之后丢弃引理吗？答案

【问题标题】：Does Z3 discard lemmas after pop() in incremental mode?Z3 在增量模式下会在 pop() 之后丢弃引理吗？
【发布时间】：2014-07-07 07:34:01
【问题描述】：

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

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

【问题讨论】：

标签： z3 smt

【解决方案1】：

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

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

【讨论】：