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 btornode.c:1201 #111

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula,

(set-logic ABV)
(declare-fun _substvar_34_ () (Array (_ BitVec 9) (_ BitVec 9)))
(declare-fun _substvar_35_ () (Array (_ BitVec 9) (_ BitVec 9)))
(assert (exists ((q1 Bool) (q2 (_ BitVec 30)) (q3 (_ BitVec 30)) (q4 Bool)) q1))
(assert (distinct _substvar_35_ _substvar_34_))
(check-sat)

boolector (commit 76aafdf) throws an assertion violation

boolector: /home/peisen/test/tofuzz/boolector/src/btornode.c:1201: btor_node_bv_get_width: Assertion `!btor_node_is_fun (exp)' failed.
[btor>main] CAUGHT SIGNAL 6
unknown
Aborted (core dumped)
aniemetz commented 4 years ago

Duplicate of #113.