search

Z3Prover / z3

The Z3 Theorem Prover
Other
9.96k stars 1.46k forks source link

Unexpected code reached #7266

Closed Lotan-Raz closed 1 week ago

Lotan-Raz commented 1 week ago

I got this error:

ASSERTION VIOLATION File: ..\src\ast\ast.cpp Line: 433 UNEXPECTED CODE WAS REACHED. Z3 4.12.2.0

while using z3 with python.

I can expand on details if necessary, but my code is kind of complicated (basically it generates a lot of formulas and checks their satisfiability, I use quantifiers and uinterpreted sorts.) I had some simple bug in my code that caused this (wrong arity for functions) but I don't know what this caused for Z3

NikolajBjorner commented 1 week ago

The error has happened before when users have a stale z3 library installed and the python bindings access them. You should check your installations of z3 and make sure there is only one. Furthermore, there is no support for old versions of z3.