-
Notifications
You must be signed in to change notification settings - Fork 42
[CI] Invariant Verification Test Cases #699
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
base: main
Are you sure you want to change the base?
Conversation
Jiahui17
left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If we add a new CLI command, make sure to document it in docs/
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
- Wrap this test in
#ifdef DYNAMATIC_ENABLE_LEQ... - Add
--enable-leq-binariesindynamatic/.github/workflows/ci.yml
Line 83 in 8074f73
run: ./build.sh --release --force - Change this to invariant fixture
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You mentioned that we can add more test cases for the verify-invariants fixture as it should be fast. The current test cases are taking around 5 seconds each (on the eda machine). Is this a reasonable time for a larger set of tests?
Adding tests to verify the automatically annotated invariants in rigidification to