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 src/btorexp.c:1874 #155

Open rainoftime opened 3 years ago

rainoftime commented 3 years ago

Hi, for the following formula, boolector 6fce0ac

(set-logic BV)
(declare-fun _substvar_261_ () Bool)
(declare-fun _substvar_410_ () Bool)
(declare-const v0 Bool)
(declare-const v8 Bool)
(assert (or (exists ((q38 (_ BitVec 21)) (q39 (_ BitVec 46)) (q40 (_ BitVec 6)) (q41 Bool)) (= (xor true true true true (forall ((q23 Bool) (q24 (_ BitVec 6)) (q25 Bool) (q26 Bool)) (or (= #b010101 q24 #b010101 q24) (forall ((q11 Bool) (q12 Bool) (q13 Bool) (q14 Bool)) (= true true true (exists ((q0 Bool) (q1 Bool) (q2 Bool) (q3 Bool)) q0) v8 true true true)))) _substvar_261_ true) _substvar_410_ true)) v0 v0))
(check-sat)

$ boolector xx.smt2
boolector: /home/peisen/test/tofuzz/boolector/src/btorexp.c:1874: quantifier_exp: Assertion `btor_node_is_regular (param)' failed.
[btor>main] CAUGHT SIGNAL 6
unknown
Aborted