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

Incorrect result when using induction #164

Closed ravipr72 closed 3 years ago

ravipr72 commented 3 years ago

Following trivial testcase produces incorrect UNSAT for the b1 prop. btormc --kind Note how the two identical checks produce different result when using -stop-first 0

1 sort bitvec 1 6 zero 1 7 state 1 one_bit_3 8 init 1 7 6 9 not 1 7 12 next 1 7 9 one_bit_3 13 bad -9 one_bit_xx 14 bad -9 one_bit

mpreiner commented 3 years ago

Thanks for reporting, we'll have a look!