Assertion violation at src/btorexp.c:1875
rainoftime opened this issue · 1 comments
rainoftime commented
Hi, for the following formula,
boolector 6fce0ac
(set-logic BV)
(declare-fun _substvar_1408_ () Bool)
(declare-fun _substvar_2024_ () Bool)
(declare-fun _substvar_2091_ () Bool)
(declare-fun _substvar_2291_ () Bool)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v3 Bool)
(assert (or v3 (= true _substvar_1408_ (exists ((q10 (_ BitVec 25)) (q11 (_ BitVec 53)) (q12 Bool) (q13 (_ BitVec 7)) (q14 Bool) (q15 (_ BitVec 25))) (exists ((q0 Bool) (q1 Bool) (q2 Bool) (q3 Bool)) (or q3 (exists ((q0 Bool) (q1 Bool) (q2 Bool) (q3 Bool)) (= true v1 (forall ((q0 Bool) (q1 Bool) (q2 Bool) (q3 Bool)) (and v0 v0 v0 v0 q3 q3)) _substvar_2091_ true q1 v0 v0 true v0)) (forall ((q0 Bool) (q1 Bool) (q2 Bool) (q3 Bool)) (and v0 v0 v0 v0 q0 q0)) v0 v0))) _substvar_2024_ _substvar_2291_ true true v0)))
(check-sat)
$ boolector xx.smt2
boolector: /home/peisen/test/tofuzz/boolector/src/btorexp.c:1875: quantifier_exp: Assertion `btor_node_is_param (param)' failed.
[btor>main] CAUGHT SIGNAL 6
unknown
Aborted