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
325 stars 63 forks source link

Witness for second bad claims to be witness for both #89

Closed nakengelhardt closed 4 years ago

nakengelhardt commented 4 years ago

The attached design contains two bads: design_btor.btor.txt

Running btormc design_btor.btor.txt accordingly produces two witnesses: design_btor.wit1.txt and design_btor.wit2.txt

The first witness is a witness for b0 and works correctly:

> btorsim design_btor.btor.txt design_btor.wit1.txt
.

The second however claims to be a witness for b0 b1 but is actually only a witness for b1:

> btorsim design_btor.btor.txt design_btor.wit2.txt
.
*** 'btorsim' error: claimed bad state property 'b0' id 25 not reached
mpreiner commented 4 years ago

Thanks Nina! Fixed with 9a13228 on master.

nakengelhardt commented 4 years ago

Excellent! Now I have boolector for cover mode working in SymbiYosys 🎉