Skip to content

Added new solver-specific tags for SMT regression tests #5985

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 1 commit into from
Mar 31, 2021

Conversation

SaswatPadhi
Copy link
Contributor

@SaswatPadhi SaswatPadhi commented Mar 30, 2021

As per the proposal described in #5982 and offline discussions with @tautschnig, this PR introduces new tags that can be used to label tests that are known to be broken with specific solvers. It also updates the Makefile targets to use these solver-specific tags.

This PR would unblock #5973. The regression test there was tagged broken-smt-backend and has been fixed to work with Z3 and CVC4 (and other solvers that support quantifiers), but currently there is no viable fix for CPROVER SMT2. Once this PR is merged, I would label that regression test as broken-cprover-smt-backend instead.

  • Each commit message has a non-empty body, explaining why the change was made.
  • NA Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • NA The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • NA 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).
  • NA My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • NA White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@SaswatPadhi SaswatPadhi marked this pull request as draft March 30, 2021 22:41
@SaswatPadhi SaswatPadhi force-pushed the smt2_regression_tags branch from 848beac to 53e320c Compare March 30, 2021 22:44
@SaswatPadhi SaswatPadhi added aws Bugs or features of importance to AWS CBMC users enhancement Solvers Tests labels Mar 30, 2021
@SaswatPadhi SaswatPadhi self-assigned this Mar 30, 2021
@SaswatPadhi SaswatPadhi marked this pull request as ready for review March 30, 2021 23:20
@SaswatPadhi SaswatPadhi force-pushed the smt2_regression_tags branch from 53e320c to 269e768 Compare March 31, 2021 00:08
@SaswatPadhi
Copy link
Contributor Author

Note that I have added additional targets to the Makefile but those are not built as part of the default target (that's run on the CI). I didn't know of a way to do that with cmake -- using add_test_pl_profile directly adds them to the build queue.

@codecov
Copy link

codecov bot commented Mar 31, 2021

Codecov Report

Merging #5985 (afc385f) into develop (e76d811) will not change coverage.
The diff coverage is n/a.

Impacted file tree graph

@@           Coverage Diff            @@
##           develop    #5985   +/-   ##
========================================
  Coverage    75.12%   75.12%           
========================================
  Files         1435     1435           
  Lines       156301   156301           
========================================
  Hits        117416   117416           
  Misses       38885    38885           

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 2f7dcb5...afc385f. Read the comment docs.

Copy link
Collaborator

@martin-cs martin-cs left a comment

Choose a reason for hiding this comment

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

This is more distinctions than I would make but ... if you are happy to work with these then, cool.

As per the proposal described in diffblue#5982, this PR introduces new tags that
can be used to label tests that are known to be broken with specific solvers.
It also updates the Makefile targets to use these solver-specific tags.
@SaswatPadhi SaswatPadhi force-pushed the smt2_regression_tags branch from 269e768 to afc385f Compare March 31, 2021 14:28
@SaswatPadhi
Copy link
Contributor Author

SaswatPadhi commented Mar 31, 2021

Thanks for taking a look @martin-cs.

I removed the cvc4 tags for now since we don't run cvc4 on CI. I will keep #5982 open for further discussion and we can add more tags later if we need to.

@SaswatPadhi SaswatPadhi changed the title Added new tags for SMT regression tests Added new solver-specific tags for SMT regression tests Mar 31, 2021
@SaswatPadhi SaswatPadhi merged commit 01c2cd1 into diffblue:develop Mar 31, 2021
@SaswatPadhi SaswatPadhi deleted the smt2_regression_tags branch March 31, 2021 16:38
@tautschnig tautschnig mentioned this pull request Apr 6, 2021
7 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
aws Bugs or features of importance to AWS CBMC users enhancement Solvers Tests
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants