Skip to content

ebmc: re-enable IC3 #273

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

Merged
merged 2 commits into from
Dec 11, 2023
Merged

ebmc: re-enable IC3 #273

merged 2 commits into from
Dec 11, 2023

Conversation

kroening
Copy link
Member

No description provided.

@kroening kroening marked this pull request as ready for review December 10, 2023 19:23
This moves the IC3 tests so they can be run by the script and marks them as
KNOWNBUG.
@kroening kroening changed the title ebmc: move IC3 tests ebmc: re-enable IC3 Dec 10, 2023
This fixes the IC3 to ebmc interface and re-enables the tests.
Comment on lines +4 to 7
^EXIT=2$
^SIGNAL=0$
^property HOLDS
^inductive invariant verification is ok
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What do these exit codes (here: 2, in other tests: 1) mean, and why is the result output seemingly so different?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The result reporting is very different, both in terms of exit code and console output, and it's a todo item to align it. The changes to the test merely document the existing behaviour.

@tautschnig tautschnig merged commit fe2d2fa into main Dec 11, 2023
@tautschnig tautschnig deleted the ic3 branch December 11, 2023 10:22
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants