-
Notifications
You must be signed in to change notification settings - Fork 16
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
No warning when no quantifiers are used in quantified logic #76
Comments
I'll add that warning (maybe behind a cli flag, but I'm not sure yet). |
I wonder if this fits into the "find minimal logic" feature. The warning would be emitted on the |
This would indeed fit into the "minimal logic" feature, considering that dolmen would ultimately warn when a problem is set in a logic that is not the minimal one for the problem. |
A first implementation of minimal logic detection is in #211. I'll probably add a warning that can be triggered (and made fatal if wanted) when the input logic of a problem is not minimal. |
It would be great if Dolmen warns if no quantifiers are used, but a quantified logic was specified:
For example for
Dolmen parses the benchmark without any warning, however, it'd be great if it would inform the user that QF_BV would be sufficient for the logic.
The text was updated successfully, but these errors were encountered: