Skip to content
This repository has been archived by the owner on Aug 23, 2024. It is now read-only.

Assertion violation at src/btorexp.c:1875 #157

Open
rainoftime opened this issue Oct 17, 2020 · 1 comment
Open

Assertion violation at src/btorexp.c:1875 #157

rainoftime opened this issue Oct 17, 2020 · 1 comment
Labels
wontfix This will not be worked on

Comments

@rainoftime
Copy link

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 mpreiner added the wontfix This will not be worked on label Aug 23, 2024
@mpreiner
Copy link
Member

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

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
wontfix This will not be worked on
Projects
None yet
Development

No branches or pull requests

2 participants