Add regression testing against z3 in a various assortment of environments.

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 starts exercising some of the regression suite with `z3` as the
backend in some of the platforms it has been installed under.

Author: NlightNFotis

.github/workflows/pull-request-checks.yaml

@@ -58,6 +58,7 @@ jobs:
         run: |
           make -C regression test-parallel JOBS=2
           make -C regression/cbmc test-paths-lifo
+          make -C regression/cbmc test-z3
           env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
           make -C jbmc/regression test-parallel JOBS=2
 
@@ -116,6 +117,7 @@ jobs:
         run: |
           make -C regression test-parallel JOBS=2
           make -C regression/cbmc test-paths-lifo
+          make -C regression/cbmc test-z3
           env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
           make -C jbmc/regression test-parallel JOBS=2
 
@@ -293,6 +295,8 @@ jobs:
         run: cd jbmc/unit; ./unit_tests
       - name: Run regression tests
         run: make -C regression test-parallel JOBS=3
+      - name: Run regression/cbmc/ regression tests using z3
+        run: make -C regression/cbmc test-z3 test-parallel JOBS=3
       - name: Run JBMC regression tests
         run: make -C jbmc/regression test-parallel JOBS=3
 
@@ -438,6 +442,8 @@ jobs:
           make CXX=clcache BUILD_ENV=MSVC -C jbmc/unit test
       - name: Run CBMC regression tests
         run: make CXX=clcache BUILD_ENV=MSVC -C regression test
+      - name: Run regression/cbmc/ tests with z3
+        run: make CXX=clcache BUILD_ENV=MSVC -C regression/cbmc test-z3
 
 
   check-clang-format: