Mark a test that uses --smt2 as needing the smt-backend #6244
Conversation
Codecov Report
@@ Coverage Diff @@
## develop #6244 +/- ##
===========================================
- Coverage 76.18% 76.16% -0.02%
===========================================
Files 1484 1484
Lines 162092 162173 +81
===========================================
+ Hits 123495 123525 +30
- Misses 38597 38648 +51
Continue to review full report at Codecov.
|
martin-cs
force-pushed
the
fix/tag-z3-regression-tests-3
branch
from
9e32399 to
5af69a9
Compare
| CORE smt-backend broken-cprover-smt-backend | ||
| main.c | ||
| --apply-loop-contracts _ --z3 | ||
| --apply-loop-contracts _ |
There was a problem hiding this comment.
I understand the tag to mark this is broken for the cprover backend, but removing the --z3 tag hides that this uses functionality explicit to z3. I know the default at the moment is z3, but leaving this explicit has clarity that I'm not sure we want to remove.
There was a problem hiding this comment.
Unless I have radically misunderstood, this should work with any SMT solver that supports quantifiers. I will re-add --z3 but this means that the smt-backend tests will fail if another solver is used and z3 is not present.
There was a problem hiding this comment.
Not for this specific example, but a lot of the quantified output is a problem for other solvers. Typically cvc3 and cvc4 will error out due to quantifiers while specifying quantifier free logic, similar behaviour for mathsat and boolector. I think only z3 can handle it out of the box from cbmc, while modifying the set-logic command allows cvc4 to handle it (but can produce unknowns... which we were avoiding until it became clear this happens for z3 and is now handled gracefully). Also in the current backend the output for z3 is different to most other solvers, so turning of the --z3 flag may reveal different SMT code.
There was a problem hiding this comment.
due to quantifiers while specifying quantifier free logic
This is the intended and correct behaviour of the solver.
but can produce unknowns... which we were avoiding until it became clear this happens for z3 and is now handled gracefully
Again, if the logic you have requested / fragment of logic you have used is undecideable, this is intended behaviour.
There was a problem hiding this comment.
Apologies if my comment was unclear. I was not implying the behaviour was incorrect, only commenting on what we see now (and why I think being explicit on z3 is helpful). No requested change or displeasure with the PR.
There was a problem hiding this comment.
Sorry about the late response on this, and for reopening this conversation.
I guess, until #6248 is merged, we could keep the _ --z3 arguments, but it doesn't really matter for the CI because we don't run CVC4 anyway and so this test wouldn't really break anything (without the _ --z3 part).
It would be nice to aim for solver-agnostic SMT encoding for as many cases as possible, and I think in this case we do get a solver-agnostic encoding that should work with both Z3 and CVC4 (modulo the set-logic issue). To me, _ --z3 indicates that this test triggers some Z3-specific encoding that wouldn't work on other SMT solvers in general.
Moreover, if that's the case, we should use the broken-<solver-X>-backend tags to explicitly document that at least for Z3, CVC4 and CPROVER SMT2 solvers.
What do you think?
There was a problem hiding this comment.
TBH for the purposes of this test all I want is to be able to run the regression tests on a machine that doesn't have Z3 installed. For me anything else is a discussion for another ticket / issue.
There was a problem hiding this comment.
Approving this and unblocking you. We can revisit this issue once #6248 is merged may be.
martin-cs
force-pushed
the
fix/tag-z3-regression-tests-3
branch
from
3fa50ec to
8f21822
Compare
| - be tagged `smt-backend`: | ||
| because the SAT backend does not support (simply ignores) `forall` in negative (e.g. assume) contexts. | ||
| - be tagged `broken-cprover-smt-backend`: | ||
| because the CPROVER SMT2 solver cannot handle (errors out on) `forall` in negative (e.g. assume) contexts. | ||
| - not use the `_ --z3` parameters: |
There was a problem hiding this comment.
Do we still need the _ --z3, now that you have added Makefile rules to handle SMT-related tags?
There was a problem hiding this comment.
See @TGWDB 's request above.
martin-cs
force-pushed
the
fix/tag-z3-regression-tests-3
branch
from
8f21822 to
77c5d5d
Compare
|
@SaswatPadhi @TGWDB please could you re-review? @feliperodri please coul you have a look as a maintainer for code contracts? I would like to get this merged ASAP. |
martin-cs
force-pushed
the
fix/tag-z3-regression-tests-3
branch
from
166b3cf to
64151c2
Compare
martin-cs
force-pushed
the
fix/tag-z3-regression-tests-3
branch
from
64151c2 to
266b1b5
Compare
martin-cs
force-pushed
the
fix/tag-z3-regression-tests-3
branch
from
266b1b5 to
76f736c
Compare
These cause a substantial increase in regression run time and so are disabled for now.
martin-cs
force-pushed
the
fix/tag-z3-regression-tests-3
branch
from
76f736c to
3493061
Compare
|
Thanks @SaswatPadhi . I have disabled the CMake SMT solver configurations for now as they were increasing the run time of the regressions by a lot. As discussed above, there may be changes to how the regression tests are run for SMT solvers so I will leave enabling them to be part of that discussion. |
|
Sounds good. Thanks a lot for adding the SMT tags support to regression/contracts! |
As I noted last time #6187 (comment) if one of the images that doesn't use the SMT back-end also doesn't have Z3 on the path then these bugs will manifest on PR and I won't need to keep patching them.