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 --kind not converging #220

Open cgjohannsen opened 9 months ago

cgjohannsen commented 9 months ago

BtorMC with the --kind flag does not appear to converge. We haven't found an input where BtorMC converges within k=1000. AVR converges on many of them.

To reproduce one example:

Input file: gulwani_cegar1.btor2.txt

Command: ./boolector/build/bin/btormc gulwani_cegar1.btor2.txt --kind -kmax 1000 -v

Output: btormc.out.txt

Running with AVR, it converges at k=3 as expected:

Command: python avr.py --kind gulwani_cegar1.btor2.txt

Output: avr.out.txt

mpreiner commented 2 months ago

Boolector is not actively maintained and developed anymore. It was succeeded by Bitwuzla and the repository is now archived.