z3klee

Z3 infinite loop from KLEE

I have a modified version of KLEE and an essentially simple query like

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

When I invoke the Z3 solver I get stuck in an infinite loop (haven't waited forever though :]) inside the following while statement in z3/src/ast/rewriter/rewriter_def.h:

while (!frame_stack().empty())

I've posted it as a potential bug in GitHub/Z3Prover/z3/issues but I'm not at all sure it is indeed a bug. Any help is very much appreciated, thanks!

Solution

  • From the answer in GitHub/Z3Prover/z3/issues:

    KLEE uses the C API but uses wrapper classes to correctly do reference counting.

    However what I did back at the time was:

    called the Z3 C API without using KLEE's wrapper class: Z3ASTHandle

    That made things go (very) wrong ...