Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Assertion violation at btornode.c:1201 #111

Closed
rainoftime opened this issue Apr 29, 2020 · 1 comment
Closed

Assertion violation at btornode.c:1201 #111

rainoftime opened this issue Apr 29, 2020 · 1 comment
Assignees
Labels
duplicate This issue or pull request already exists

Comments

@rainoftime
Copy link

Hi, for the following formula,

(set-logic ABV)
(declare-fun _substvar_34_ () (Array (_ BitVec 9) (_ BitVec 9)))
(declare-fun _substvar_35_ () (Array (_ BitVec 9) (_ BitVec 9)))
(assert (exists ((q1 Bool) (q2 (_ BitVec 30)) (q3 (_ BitVec 30)) (q4 Bool)) q1))
(assert (distinct _substvar_35_ _substvar_34_))
(check-sat)

boolector (commit 76aafdf) throws an assertion violation

boolector: /home/peisen/test/tofuzz/boolector/src/btornode.c:1201: btor_node_bv_get_width: Assertion `!btor_node_is_fun (exp)' failed.
[btor>main] CAUGHT SIGNAL 6
unknown
Aborted (core dumped)
@aniemetz aniemetz self-assigned this Apr 29, 2020
@aniemetz
Copy link
Member

Duplicate of #113.

@aniemetz aniemetz added the duplicate This issue or pull request already exists label Apr 29, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
duplicate This issue or pull request already exists
Projects
None yet
Development

No branches or pull requests

2 participants