-
Notifications
You must be signed in to change notification settings - Fork 20
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
jfs-smt2cxx can't handle all formulas that jfs can #39
Comments
The It would be useful to know which expression is causing the crash though because ideally we don't want |
Aha, that does explain it. After diffing the output of jfs-opt and jfs-opt -standard-passes, the culprit seems to be this line:
which gets simplified to
|
It's most likely the |
There seems to be a slight mismatch in the set of formulas accepted by jfs-smt2cxx versus jfs. An example is
20170501-Heizmann-UltimateAutomizer/cos_polynomial_true-unreach-call.c_9.smt2
(attached), which is quickly solved using jfs but dies withunsupported kind
underjfs-smt2cxx
:I'll try to look into this more when I have some time but thought I'd file the issue in case it was instantly obvious what was going wrong.
cos_polynomial_true-unreach-call.c_9.txt
The text was updated successfully, but these errors were encountered: