z3 - 来自 KLEE 的 Z3 无限循环

Question

我有一个 KLEE 的修改版本和一个基本上简单的查询，例如

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

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

while (!frame_stack().empty())

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

Answer 1

从GitHub/Z3Prover/z3/issues中的答案：

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

然而，我当时所做的是：

在不使用 KLEE 的包装类的情况下调用 Z3 C API ： Z3ASTHandle

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