boolector formal engine crashed with broken pipe error #2950
Unanswered
buttercutter
asked this question in
Q&A
Replies: 1 comment
-
|
Are you running out of memory, perhaps? |
Beta Was this translation helpful? Give feedback.
0 replies
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
Steps to reproduce the issue
In this sby file, comment out
smtbmc yicesand then uncommentsmtbmc boolector, and also modifyproof: depth 20toproof: depth 1000, then runsby -f spidergon.sbyExpected 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 pipeerrorBeta Was this translation helpful? Give feedback.
All reactions