Tag another test that fails if you don't have z3 on your path

[martin-cs]

• 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.

[martin-cs]

@db-ci-cprover please could one of the CI images not have z3 on the path so that we can catch this kind of issue before it is merged?

[SaswatPadhi]

The Makefiles in regression/contracts do not respect backend tags (see #5986 (comment)), so I left this as TODO.

I don't think just adding the tags would leads to these tests being ignored; we also need to update the Make and CMake files.

[martin-cs]

At the moment you can't cleanly run the regression tests without z3. I don't quite know why the CI doesn't flag this up. Presumably there is some common set-up which includes adding z3? I think we should either fix this or add z3 as a dependency. My preference is fix.

[codecov]

Codecov Report

Merging #6187 (5923084) into develop (7486222) will increase coverage by 0.26%.
The diff coverage is 98.71%.

@@             Coverage Diff             @@
##           develop    #6187      +/-   ##
===========================================
+ Coverage    75.25%   75.52%   +0.26%     
===========================================
  Files         1454     1454              
  Lines       160796   160922     +126     
===========================================
+ Hits        121006   121529     +523     
+ Misses       39790    39393     -397     

Impacted Files	Coverage Δ
...bytecode_convert_method/convert_invoke_dynamic.cpp	0.00% <ø> (ø)
...alyses/variable-sensitivity/abstract_environment.h	100.00% <ø> (ø)
...lyses/variable-sensitivity/abstract_value_object.h	87.71% <ø> (ø)
...ses/variable-sensitivity/constant_abstract_value.h	100.00% <ø> (ø)
...ble-sensitivity/constant_pointer_abstract_object.h	100.00% <ø> (ø)
...ses/variable-sensitivity/data_dependency_context.h	100.00% <ø> (ø)
.../variable-sensitivity/full_array_abstract_object.h	100.00% <ø> (ø)
...variable-sensitivity/full_struct_abstract_object.h	100.00% <ø> (ø)
...s/variable-sensitivity/value_set_abstract_object.h	100.00% <ø> (ø)
...le-sensitivity/value_set_pointer_abstract_object.h	100.00% <ø> (ø)
... and 93 more

---

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 0ae6010...5923084. Read the comment docs.

[SaswatPadhi]

I think we should either fix this or add z3 as a dependency. My preference is fix.

+1. I think we should fix this.

1. The Make and CMake scripts should correctly enforce the tags
2. May be for one platform, say linux?, we could have two separate images: one with Z3 and one without Z3?

[martin-cs]

Sounds great. I can try to do 1. but we will need @db-ci-cprover to do 2.

[TGWDB]

Note that #6213 has merged a CI job that specifically does some regression tests with z3.

[martin-cs]

Fixed by a different route.