search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.29k stars 1.48k forks source link

Nondeterministic seg faults / unreachable code error via C API #5070

Closed tjknoth closed 3 years ago

tjknoth commented 3 years ago

I'm using z3 via a Haskell library (that uses the C API). I'm using it in the backend for a simple typechecker, incrementally making queries to a single z3 instance. Around 20% of the time I will get a seg fault. Occasionally I will also get the following error:

ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 449
UNREACHABLE CODE WAS REACHED.
Z3 4.8.8.0

I haven't yet spent much time figuring out how to reproduce this issue. As far as I can tell so far, the errors occur at random points when repeatedly re-running a given benchmark.

This gist below contains the output of Z3_benchmark_to_smtlib_string() applied to each subsequent solver query. On this particular run I got the unreachable code error above. Running z3 on the given smtlib works fine -- not sure this record will be very helpful, but here it is: https://gist.github.com/tjknoth/8506f71988a207ab8ab6f3860beb6b46

This issue in the Haskell binding library seems related: https://github.com/IagoAbal/haskell-z3/issues/27

NikolajBjorner commented 3 years ago

Most likely you are not updating reference counts correctly on all reference counted objects. If you write a wrapper on top of C++, as the current Julia bindings exploit, tracking life-times is less error prone.