search

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
335 stars 62 forks source link

btormc crash on exit #86

Closed nakengelhardt closed 4 years ago

nakengelhardt commented 4 years ago

When running "btormc btormc_crash.txt" on the attached btor model (renamed .txt because github doesn't like .btor) the witness is printed successfully but then a segfault occurs. With -v 1:

[btor>mc] found 1 reachable and 0 unreachable bad state properties at bound k = 3
[btor>mc] deleting model checker: 16 inputs, 28 states, 2 bad, 17 constraints
Segmentation fault (core dumped)
mpreiner commented 4 years ago

The issue was that symbol miter.sv:0.0-0.0 was assigned to two different expressions and we didn't have a corresponding check in the API. Boolector now prints a warning in this case.

Fixed with 28f266aefc421848abe9fd002bd94694c7d7dc48.

nakengelhardt commented 4 years ago

Oh wow, another victim of the recent source location patch in yosys! That's now three crashes from just a bad line number annotation, impressive...

Anyway, thanks for fixing this!