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 btorslvquant.c:1055 #113

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula,

(set-logic ABV)
(declare-const arr--1418469125072990249_-1418469125069742674-0 (Array (_ BitVec 9) (_ BitVec 10)))
(assert (not (exists ((q2 (_ BitVec 9)) (q3 (_ BitVec 10))) (bvugt q3 (select arr--1418469125072990249_-1418469125069742674-0 (_ bv0 9))))))
(check-sat)

boolector (commit 76aafdf) throws an assertion violation

boolector: /home/peisen/test/tofuzz/boolector/src/btorslvquant.c:1055: refine_exists_solver: Assertion `!btor_hashptr_table_get (gslv->forall_ces, ce)' failed.
[btor>main] CAUGHT SIGNAL 6
unknown
Aborted (core dumped)
aniemetz commented 4 years ago

Boolector does not support logic ABV. The error handling for this logic in the SMT2 parser was missing, added in https://github.com/Boolector/boolector/commit/4999474f4e717c206577fd2b1549bd4a9f4a36e7.