Run regression tests with z3 as the backend solver.

[NlightNFotis]

As things currently stand, we install z3 in a number of CI platforms,
but don't run the regression suite with z3 as the backend solver.
This adds a job whose purpose is to run the regression tests under regression/cbmc/
with z3.

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

[codecov]

Codecov Report

Merging #6213 (ddbe35b) into develop (0002950) will increase coverage by 7.80%.
The diff coverage is n/a.

❗ Current head ddbe35b differs from pull request most recent head cdbc539. Consider uploading reports for the commit cdbc539 to get more accurate results

@@             Coverage Diff             @@
##           develop    #6213      +/-   ##
===========================================
+ Coverage    67.40%   75.21%   +7.80%     
===========================================
  Files         1157     1458     +301     
  Lines        95236   161402   +66166     
===========================================
+ Hits         64197   121392   +57195     
- Misses       31039    40010    +8971     

Flag	Coverage Δ
cproversmt2	?
regression	?
unit	?

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files	Coverage Δ
src/util/string_container.cpp	52.94% <0.00%> (-47.06%)	⬇️
src/solvers/prop/prop.cpp	42.85% <0.00%> (-41.76%)	⬇️
src/solvers/flattening/boolbv_member.cpp	53.65% <0.00%> (-38.65%)	⬇️
src/cpp/cpp_storage_spec.cpp	65.00% <0.00%> (-35.00%)	⬇️
src/util/cmdline.h	66.66% <0.00%> (-33.34%)	⬇️
src/solvers/strings/array_pool.h	66.66% <0.00%> (-33.34%)	⬇️
src/solvers/strings/string_refinement.h	66.66% <0.00%> (-33.34%)	⬇️
...rs/strings/string_concatenation_builtin_function.h	0.00% <0.00%> (-33.34%)	⬇️
src/cbmc/c_test_input_generator.cpp	60.00% <0.00%> (-30.33%)	⬇️
src/analyses/local_cfg.h	75.00% <0.00%> (-25.00%)	⬇️
... and 1437 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 dd77754...cdbc539. Read the comment docs.

[thomasspriggs]

Looks good to me overall. However I note that the run time of the "Run regression/cbmc tests with z3 as the backend" step is down to 1m 10s with the long running test disabled. Given that the testing is that quick I am not sure how good an idea a separate job is. However I am approving as-is because running the tests with Z3 is a step forward whether they are done in a separate job or an existing job.

[thomasspriggs]

⛏️ I'd move smt-z3 closer to the start of the name. That way the purpose of the job can be seen sooner and still read when the name has been truncated by github.

[TGWDB]

Looks good to me overall. However I note that the run time of the "Run regression/cbmc tests with z3 as the backend" step is down to 1m 10s with the long running test disabled. Given that the testing is that quick I am not sure how good an idea a separate job is. However I am approving as-is because running the tests with Z3 is a step forward whether they are done in a separate job or an existing job.

I would argue for a separate job since we don't want to enforce z3 dependency any further than necessary... Also this way if there is some issue specifically with z3, it should only appear in one job.