Assertion violation at src/parser/btorsmt2.c:3360

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/btorsmt2.c:3360 #131

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula, 3360.txt

boolector 59c9ade throws an assertion violation

boolector: /home/boolector/src/parser/btorsmt2.c:3360: parse_open_term_as: Assertion `parser->work.start[1].tag == BTOR_UNDERSCORE_TAG_SMT2' failed.
[btor>main] CAUGHT SIGNAL 6
unknown
Aborted

aniemetz commented 4 years ago

This is intended behavior when compiled in debug mode. This assertion just additionally checks behavior in a code block that handles this error case.