来自克利的Z3无限循环

Question

我有一个修改版的 KREE 和一个本质上简单的查询喜欢

(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中将其作为潜在错误发布但我完全不确定这确实是一个错误。非常感谢任何帮助，谢谢！

Answer 1

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

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

然而，我当时所做的是：

调用 Z3 C API，而不使用 KLEE 的包装类：Z3ASTHandle

这让事情变得(非常(错误...