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

Add support for the (reset) SMTLIB command #32

Open sy6sy2 opened 5 years ago

sy6sy2 commented 5 years ago

Hi, Do you plan to add the support for the (reset) SMTLIB command?

According to http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf:

The new command reset brings the state of a solver to the state it had immediately after start up (resetting everything).

In my case, I have a lot of formula to check but they are not related at all. This is why I use the (reset) command with Z3 and CVC4. But with Boolector I have to kill the Boolector process and start a new one each time I want to "start a fresh session".

Thank you!

mpreiner commented 5 years ago

Should be doable! We'll have a look.

sy6sy2 commented 4 years ago

Hi, is the SMTLIBv2 (reset) support sill on the table? 😇 Thank you!

aytey commented 4 years ago

You might be interested in this other issue: https://github.com/Boolector/boolector/issues/139 (particularly https://github.com/Boolector/boolector/issues/139#issuecomment-665218554)

mpreiner commented 1 week ago

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