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 preprocess/btorder.c:162 #96

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula,

(set-logic BV)
(declare-fun _substvar_12_ () Bool)
(declare-const v6 Bool)
(declare-const v12 Bool)
(assert (or (forall ((q0 Bool) (q1 Bool) (q2 Bool)) (not (= v6 q1 true v12 q0 q1 v6 q2))) _substvar_12_))
(check-sat)

boolector (commit 76aafdf) throws an assertion violation

boolector: /home/boolector/src/preprocess/btorder.c:162: find_substitutions: Assertion `!btor_node_is_quantifier (root)' failed.
[btor>main] CAUGHT SIGNAL 6
unknown
Aborted (core dumped)