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

[Bug] `(push 0)`/`(pop 0)` raises an error message #43

Closed pkreutzer closed 5 years ago

pkreutzer commented 5 years ago

Hi there,

SMT-LIB v2 explicitly defines (push 0) and (pop 0) as operations without effect (cf. p. 59 in version 2.6 of the language standard), but the current version of Boolector prints an error message instead:

(set-logic QF_UFBV)
(push 0)
(check-sat)
[boolector] boolector_push: context level must be greater than 0

The following patch seems to fix the problem: boolector-3.0.0_push_pop_0.patch.txt

aniemetz commented 5 years ago

Thanks for pointing this out! We will address immediately.