来自 KLEE 的 Z3 无限循环答案

【问题标题】：Z3 infinite loop from KLEE来自 KLEE 的 Z3 无限循环
【发布时间】：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 但我完全不确定这确实是一个错误。非常感谢任何帮助，谢谢！

【问题讨论】：

标签： z3 klee

【解决方案1】：

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

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

然而我当时所做的是：

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

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

【讨论】：