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 src/btorexp.c:1875 #157

Open rainoftime opened 3 years ago

rainoftime commented 3 years ago

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
mpreiner commented 1 month ago

Boolector is not actively maintained and developed anymore. It was succeeded by Bitwuzla and the repository is now archived.