Assertion violation at src/parser/btorsmt.c:335

Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.

http://boolector.github.io

Other

325 stars 63 forks source link

Assertion violation at src/parser/btorsmt.c:335 #130

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula, 335.txt

boolector 59c9ade throws an assertion violation

boolector: /home/boolector/src/parser/btorsmt.c:335: delete_smt_node: Assertion `parser->nodes->count > 0' failed.
[btor>main] CAUGHT SIGNAL 6
unknown
Aborted

mpreiner commented 4 years ago

Crash is in btorsmt.c, which is the old and unmaintained SMT-LIB v1 parser. Please do not submit any more issues on btorsmt.c