Skip to content

Add regression tests from CBMC folder to incremental SMT2 backend #7434

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 1 commit into from
Jan 20, 2023
Merged

Add regression tests from CBMC folder to incremental SMT2 backend #7434

merged 1 commit into from
Jan 20, 2023

Conversation

esteffin
Copy link
Contributor

Run 645 tests from regression/cbmc with the incremental smt2 backend.

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@tautschnig
Copy link
Collaborator

Apart from the failing CI job: please rebase once #7432 is merged, for it might affect what truly works.

@thomasspriggs thomasspriggs force-pushed the esteffin/incr-smt2-new-regressions branch from b22ec12 to 50e417e Compare December 15, 2022 20:28
@esteffin esteffin force-pushed the esteffin/incr-smt2-new-regressions branch from 50e417e to f7eec2c Compare December 16, 2022 13:28
@esteffin esteffin force-pushed the esteffin/incr-smt2-new-regressions branch 4 times, most recently from c38117b to 52788af Compare January 18, 2023 01:00
@esteffin esteffin force-pushed the esteffin/incr-smt2-new-regressions branch from 52788af to bdc3538 Compare January 19, 2023 16:20
@NlightNFotis NlightNFotis merged commit 85b7bb9 into diffblue:develop Jan 20, 2023
tautschnig added a commit to tautschnig/cbmc that referenced this pull request Jan 24, 2023
@tautschnig
Array_UF21 does not always work with incremental SMT back-end
1eb8803 
The test consistently fails when doing coverage checking (was also the
case in the coverage check run of diffblue#7434, which was the PR introducing this
test). The output is:
`Invalid SMT response "corrupted"`
The test appears to be working fine when not doing coverage checking,
though.
@tautschnig tautschnig mentioned this pull request Jan 24, 2023
Merged
3 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tautschnig tautschnig tautschnig approved these changes

@martin-cs martin-cs martin-cs approved these changes

Assignees

@esteffin esteffin

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@esteffin @tautschnig @martin-cs @NlightNFotis @thomasspriggs