Skip to content

This issue was moved to a discussion.

You can continue the conversation there. Go to discussion →

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.

Sign up for GitHub

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

Jump to bottom

boolector formal engine crashed with broken pipe error #2533

Closed
buttercutter opened this issue Jan 9, 2021 · 1 comment
Closed

boolector formal engine crashed with broken pipe error #2533

buttercutter opened this issue Jan 9, 2021 · 1 comment
Labels
question

Comments

@buttercutter
Copy link

buttercutter commented Jan 9, 2021 •
edited

Steps to reproduce the issue

In this sby file, comment out smtbmc yices and then uncomment smtbmc boolector , and also modify proof: depth 20 to proof: depth 1000, then run sby -f spidergon.sby

Expected behavior

The formal engine should finish the BMC and induction verification without crashing and terminated on its own

Actual behavior

The formal engine crashed and gave me broken pipe error

boolector_broken_pipe_error
@whitequark
Copy link
Member

whitequark commented Jul 18, 2021 •
edited

Are you running out of memory, perhaps?

@YosysHQ YosysHQ locked and limited conversation to collaborators Aug 13, 2021
@mmicko mmicko closed this as completed Aug 13, 2021

This issue was moved to a discussion.

You can continue the conversation there. Go to discussion →

Assignees
No one assigned
Labels
question
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@whitequark @buttercutter @mmicko