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

btormc: really stop at first reached property with --stop-first #128

Closed nakengelhardt closed 4 years ago

nakengelhardt commented 4 years ago

If a model contains multiple properties and the stop-first option is set, you can still get multiple witnesses returned when several properties are satisfiable in the same time step. This is inconvenient if you only want one result, especially as it takes extra time to check the others.

With this PR, instead break out of the loop after finding the first satisfied property.