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 btorsynth.c:217 #112

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula,

(set-logic ABV)
(declare-const v8 Bool)
(declare-const arr--5763275690868569689_-5763275690868569689-0 (Array (_ BitVec 5) (_ BitVec 5)))
(assert (not (exists ((q1 Bool) (q2 Bool) (q3 (_ BitVec 10))) q1)))
(assert (or (= (select arr--5763275690868569689_-5763275690868569689-0 (_ bv0 5)) (_ bv0 5) (_ bv0 5) (_ bv0 5)) v8))
(check-sat)

boolector (commit 76aafdf) throws an assertion violation

boolector: /home/peisen/test/tofuzz/boolector/src/btorsynth.c:217: collect_exps_post_order: Assertion `!btor_node_is_apply (real_cur)' failed.
[btor>main] CAUGHT SIGNAL 6
unknown
Aborted (core dumped
aniemetz commented 4 years ago

Duplicate of #113.