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 btornode.c:1202 #110

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula,

(set-logic ABV)
(declare-const v1 Bool)
(declare-const arr-5150161022424467620_666089369372786930-0 (Array (_ BitVec 24) Bool))
(assert (exists ((q2 Bool) (q3 (_ BitVec 24))) (bvsgt (_ bv0 24) q3)))
(assert (=> v1 (select arr-5150161022424467620_666089369372786930-0 (_ bv0 24))))
(check-sat)

boolector (commit 76aafdf) throws an assertion violation

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

Duplicate of #113.