来自 KLEE 的 Z3 无限循环

Posted 2023-02-16

【中文标题】来自 KLEE 的 Z3 无限循环

【英文标题】：Z3 infinite loop from KLEE

【发布时间】：2017-11-16 14:30:19

【问题描述】：

我有一个 KLEE 的修改版本和一个基本简单的查询 喜欢

(assert (= 173 (str.len "OREN"))) (meant to be false).

当我调用 Z3 求解器时，我陷入了无限循环 （虽然没有永远等待:]）在下面的while语句中 z3/src/ast/rewriter/rewriter_def.h：

while (!frame_stack().empty())

我已将其作为潜在错误发布在 GitHub/Z3Prover/z3/issues 但我完全不确定这确实是一个错误。非常感谢任何帮助，谢谢！

【问题讨论】：

我看到 github 问题已解决。您可以在这里为其他人发布答案吗？

您也可以接受自己的答案来关闭问题

【参考方案1】：

来自GitHub/Z3Prover/z3/issues的答案：

KLEE 使用 C API，但使用 包装类 来正确进行引用计数。

然而我当时所做的是：

没有使用 KLEE 的包装类调用 Z3 C API：Z3ASTHandle

这让事情变得（非常）错误......