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

Assertion violation at src/preprocess/btorminiscope.c:193 #156

Closed rainoftime closed 2 years ago

rainoftime commented 3 years ago

Hi, for the following formula, boolector 6fce0ac

(set-logic BV)
(declare-fun _substvar_259_ () Bool)
(declare-fun _substvar_261_ () Bool)
(declare-fun _substvar_273_ () Bool)
(declare-fun _substvar_300_ () (_ BitVec 160))
(assert (forall ((q83 (_ BitVec 51)) (q84 (_ BitVec 9)) (q85 (_ BitVec 17)) (q86 (_ BitVec 39)) (q87 (_ BitVec 76)) (q88 (_ BitVec 44))) (or _substvar_259_ (not (forall ((q73 (_ BitVec 44)) (q74 (_ BitVec 76)) (q75 Bool) (q76 (_ BitVec 160)) (q77 (_ BitVec 12))) (distinct _substvar_273_ (= (_ bv0 160) (_ bv0 160) q76 _substvar_300_) _substvar_261_ true))))))
(check-sat)

$ boolector xx.smt2
boolector: /home/peisen/test/tofuzz/boolector/src/preprocess/btorminiscope.c:193: rebuild_mk_quantifiers: Assertion `btor_node_is_inverted (top_q) == btor_node_is_inverted (q)' failed.
[btor>main] CAUGHT SIGNAL 6
unknown
Aborted
vedadux commented 2 years ago

This issue no longer happens in 0783aa844. Should be closed for now.