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

Assertion violation at preprocess/btorder.c:372 #104

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula,

(set-logic BV)
(declare-const bv_7-0 (_ BitVec 7))
(assert (not (forall ((q1 (_ BitVec 12)) (q2 (_ BitVec 7)) (q3 (_ BitVec 27)) (q4 Bool)) (xor true true true (= bv_7-0 q2 (bvashr bv_7-0 bv_7-0) q2)))))
(check-sat)

boolector (commit 76aafdf) throws an assertion violation

boolector: /home/peisen/test/tofuzz/boolector/src/preprocess/btorder.c:372: elim_vars: Assertion `d' failed.
[btor>main] CAUGHT SIGNAL 6
unknown
Aborted (core dumped)
mpreiner commented 4 years ago

Fixed with aac63cb2776b3cc98890d0e9a301c3efacccc6fc