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 btorcore.c:3164 #116

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula,

(set-logic BV)
(push 1)
(check-sat)
(assert (forall ((q3 Bool) (q4 (_ BitVec 17)) (q5 (_ BitVec 17))) q3))
(check-sat)

boolector (commit 76aafdf) throws an assertion violation

sat
boolector: /home/rainoftime/Work/tofuzz/boolector/src/btorcore.c:3164: exp_to_aig: Assertion `av' failed.
[btor>main] CAUGHT SIGNAL 6
unknown
Aborted (core dumped)

BV does not support incremental mode. After removing the first (check-sat), boolector can identify the conflict.