Make regression tests work when cvc5 is not available

[tautschnig]

We should not have cvc5 as firm build (and test) dependency as CBMC works just fine when cvc5 is not available.

This remains work-in-progress:

•  no-cvc5 should be more fine-grained for the cbmc-output-file test suite
• CMake test suites should also become conditional on cvc5 availability
• We should have similar conditional test runs for Z3.
• At least one CI job should be changed such as not to have z3 and cvc5 available.

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

[codecov]

Codecov Report

All modified and coverable lines are covered by tests ✅

Comparison is base (1939544) 79.66% compared to head (ff48795) 79.66%.

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #8214   +/-   ##
========================================
  Coverage    79.66%   79.66%           
========================================
  Files         1682     1682           
  Lines       195378   195378           
========================================
  Hits        155642   155642           
  Misses       39736    39736           

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[thomasspriggs]

A few thought/questions -

1. Could this give the false impression that the cbmc + cvc5 tests have passed when they haven't been run? It would kind of make sense to me if this issue was handled using an option to exclude tests supplied by the build / test environment rather than something which is autodetected by the test suite.
2. Presumably this isn't needed for any ctest based test running because ctest can already be instructed to exclude a set of tests?
3. Why does this apply to cvc5 but not z3? I can see how if the same logic is applied to both then there could be issues where the tests "pass" but cbmc hasn't been tested with any SMT solver. But I don't really see that the two solvers should be treated differently for testing when they aren't treated specially by the implementation.

When I was was working on the implementation I wanted to ensure that we tested with at least 2 solvers as insurance against accidentally producing an implementation which only works with one specific solver.

[tautschnig]

A few thought/questions -

Thank you for your comments! A couple of notes:

1. Could this give the false impression that the `cbmc` + `cvc5` tests have passed when they haven't been run? It would kind of make sense to me if this issue was handled using an option to exclude tests supplied by the build / test environment rather than something which is autodetected by the test suite.

Yes, at bare minimum I should add some output that tests have been skipped.

2. Presumably this isn't needed for any `ctest` based test running because `ctest` can already be instructed to exclude a set of tests?

Good idea that we should perhaps not bake this into the CMake/ctest set-up and instead document how to skip those. (But we also need to make sure they are skippable at that level.)

3. Why does this apply to `cvc5` but not `z3`? I can see how if the same logic is applied to both then there could be issues where the tests "pass" but `cbmc` hasn't been tested with any SMT solver. But I don't really see that the two solvers should be treated differently for testing when they aren't treated specially by the implementation.

See my PR notes: this should also apply to z3, I just haven't yet set aside the time to do it.

[thomasspriggs]

Good idea that we should perhaps not bake this into the CMake/ctest set-up and instead document how to skip those. (But we also need to make sure they are skippable at that level.)

The existing ctest argument you are looking for is -E cvc5.

[tautschnig]

Good idea that we should perhaps not bake this into the CMake/ctest set-up and instead document how to skip those. (But we also need to make sure they are skippable at that level.)

The existing ctest argument you are looking for is -E cvc5.

Thanks, this will work for cvc5! But I don't think the same would be true of z3, which is used by tests spread out across several suites.

[thomasspriggs]

Good idea that we should perhaps not bake this into the CMake/ctest set-up and instead document how to skip those. (But we also need to make sure they are skippable at that level.)

The existing ctest argument you are looking for is -E cvc5.

Thanks, this will work for cvc5! But I don't think the same would be true of z3, which is used by tests spread out across several suites.

The -E argument does regex match against the test names provided to add_test_pl_profile. It could be made to work against the z3 tests by adding "z3" to the names. For example by renaming cbmc-new-smt-backend to cbmc-new-smt-backend-z3. You can check the match results using the -R positive match argument with a dry run. For example ctest -L CORE -V -N -R smt to get all the "smt" related tests.