diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml
index 7ccd3142784..7d8faeeb126 100644
--- a/.github/workflows/pull-request-checks.yaml
+++ b/.github/workflows/pull-request-checks.yaml
@@ -634,6 +634,12 @@ jobs:
           sudo apt-get install -y --allow-downgrades --reinstall gcc g++ libgcc-s1- libstdc++6=$target liblsan0=$target libtsan0=$target libcc1-0=$target libgcc1=1:$target gdb=8.1.1-0ubuntu1
       - name: Confirm z3 solver is available and log the version installed
         run: z3 --version
+      - name: Download cvc-5 from the releases page and make sure it can be deployed
+        run: |
+          wget -O cvc5 https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux
+          chmod u+x cvc5
+          mv cvc5 /usr/local/bin
+          cvc5 --version
       - name: Prepare ccache
         uses: actions/cache@v2
         with:
diff --git a/regression/cbmc-incr-smt2/CMakeLists.txt b/regression/cbmc-incr-smt2/CMakeLists.txt
index 06a41cf3496..6b00d1fc51d 100644
--- a/regression/cbmc-incr-smt2/CMakeLists.txt
+++ b/regression/cbmc-incr-smt2/CMakeLists.txt
@@ -1,10 +1,20 @@
 
 if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
-    set(exclude_win_broken_tests -X winbug)
+    set(exclude_win_broken_tests "-X;winbug")
 else()
     set(exclude_win_broken_tests "")
 endif()
 
-add_test_pl_tests(
-    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation --slice-formula" ${exclude_win_broken_tests}
+add_test_pl_profile(
+    "cbmc-incr-smt2-z3"
+    "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation --slice-formula"
+    "-C;${exclude_win_broken_tests};-s;new-smt-z3"
+    "CORE"
+)
+
+add_test_pl_profile(
+    "cbmc-incr-smt2-cvc5"
+    "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation --slice-formula"
+    "-C;${exclude_win_broken_tests};-s;new-smt-cvc5"
+    "CORE"
 )
diff --git a/regression/cbmc-incr-smt2/Makefile b/regression/cbmc-incr-smt2/Makefile
index 603200de746..a5e36136c30 100644
--- a/regression/cbmc-incr-smt2/Makefile
+++ b/regression/cbmc-incr-smt2/Makefile
@@ -9,8 +9,13 @@ else
 	exclude_broken_windows_tests=
 endif
 
-test:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation --slice-formula" $(exclude_broken_windows_tests)
+test: test.z3 test.cvc5
+
+test.z3:
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation --slice-formula" $(exclude_broken_windows_tests)
+
+test.cvc5:
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation --slice-formula" $(exclude_broken_windows_tests)
 
 tests.log: ../test.pl test
 
diff --git a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/overflow_behaviour.desc b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/overflow_behaviour.desc
index 4e2f90d69b1..d45e6ebe787 100644
--- a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/overflow_behaviour.desc
+++ b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/overflow_behaviour.desc
@@ -1,6 +1,6 @@
 CORE
 overflow_behaviour.c
---incremental-smt2-solver 'z3 --smt2 -in' --trace
+--trace
 \[main\.assertion\.1\] line \d+ Wrap-around to INT_MIN when adding to INT_MAX: SUCCESS
 \[main\.assertion\.2\] line \d+ Wrap-around to INT_MAX when subtracting from INT_MIN: SUCCESS
 \[main\.assertion\.3\] line \d+ INT_MAX minus INT_MIN equals -1: SUCCESS
diff --git a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/polynomial.desc b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/polynomial.desc
index 6149a33f6d1..55f19120fb0 100644
--- a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/polynomial.desc
+++ b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/polynomial.desc
@@ -1,6 +1,6 @@
 CORE
 polynomial.c
---incremental-smt2-solver 'z3 --smt2 -in' --trace
+--trace
 \[main\.assertion\.1\] line \d+ No negative solution: FAILURE
 \[main\.assertion\.2\] line \d+ No positive solution: FAILURE
 x=-8\ \(11111111 11111111 11111111 11111000\)
diff --git a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/simple_equation.desc b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/simple_equation.desc
index 8ae4bae24b7..499ccbe044b 100644
--- a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/simple_equation.desc
+++ b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/simple_equation.desc
@@ -1,6 +1,6 @@
 CORE
 simple_equation.c
---incremental-smt2-solver 'z3 --smt2 -in' --trace --verbosity 10
+--trace --verbosity 10
 \[main\.assertion\.1\] line \d+ a plus a always equals two times a: SUCCESS
 \[main\.assertion\.2\] line \d+ a minus a always equals 0: SUCCESS
 \[main\.assertion\.3\] line \d+ a plus its additive inverse equals 0: SUCCESS
diff --git a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/unsigned_behaviour.desc b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/unsigned_behaviour.desc
index db0157d613b..52ecdacce30 100644
--- a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/unsigned_behaviour.desc
+++ b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/unsigned_behaviour.desc
@@ -1,6 +1,6 @@
 CORE
 unsigned_behaviour.c
---incremental-smt2-solver 'z3 --smt2 -in' --trace
+--trace
 \[main\.assertion\.1\] line \d+ a plus b should be more than 27: FAILURE
 \[main\.assertion\.2\] line \d+ a plus b should be more than 27: FAILURE
 \[main\.assertion\.3\] line \d+ c plus d should be more than 27: FAILURE
diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/bitwise.desc b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/bitwise.desc
index e5431ba76e6..44db46465de 100644
--- a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/bitwise.desc
+++ b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/bitwise.desc
@@ -1,6 +1,6 @@
 CORE
 bitwise_ops.c
---incremental-smt2-solver 'z3 --smt2 -in' --slice-formula
+--slice-formula
 \[main\.assertion\.1\] line \d+ This is going to fail for bit-opposites: FAILURE
 \[main\.assertion\.2\] line \d+ This is going to hold for all values != 0: SUCCESS
 \[main\.assertion\.3\] line \d+ This is going to fail for the same value in A and B: FAILURE
diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_left.desc b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_left.desc
index e6248c053ea..ffe947dd21e 100644
--- a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_left.desc
+++ b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_left.desc
@@ -1,6 +1,6 @@
 CORE
 shift_left.c
---incremental-smt2-solver 'z3 --smt2 -in' --slice-formula
+--slice-formula
 \[main\.assertion\.1\] line \d Shifted result should be greater than one: FAILURE
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.c b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.c
index 301fe1a180b..02a4471cd04 100644
--- a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.c
+++ b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.c
@@ -10,6 +10,10 @@ int main()
 {
   int first;
   uint8_t second;
+  // This assumption is here in order to constrain the value the solver
+  // can produce to just 128 so that we don't get test failures for different
+  // values returned by different SMT solvers.
+  __CPROVER_assume((second & 1) == 0);
 
   int place;
   __CPROVER_assume(place >= 1);
diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.desc b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.desc
index d7e290ae8b8..dc7a14fd911 100644
--- a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.desc
+++ b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.desc
@@ -1,6 +1,6 @@
 CORE
 shift_right.c
---incremental-smt2-solver 'z3 --smt2 -in' --slice-formula --trace
+--slice-formula --trace
 \[main\.assertion\.1\] line \d+ Right shifting a uint with leftmost bit set is a logical shift: FAILURE
 \[main\.assertion\.2\] line \d+ Right shifting a positive number has a lower bound of 0: SUCCESS
 \[main\.assertion\.3\] line \d+ Right shifting a negative number has a lower bound value of -1: SUCCESS
diff --git a/regression/cbmc-incr-smt2/bitvector-flag-tests/div_by_zero.desc b/regression/cbmc-incr-smt2/bitvector-flag-tests/div_by_zero.desc
index 9f093877f9f..0279e9b9725 100644
--- a/regression/cbmc-incr-smt2/bitvector-flag-tests/div_by_zero.desc
+++ b/regression/cbmc-incr-smt2/bitvector-flag-tests/div_by_zero.desc
@@ -1,6 +1,6 @@
 CORE
 div_by_zero.c
---incremental-smt2-solver 'z3 --smt2 -in' --div-by-zero-check --trace
+--div-by-zero-check --trace
 \[main\.division-by-zero\.1\] line \d division by zero in x / y: FAILURE
 \[main\.division-by-zero\.2\] line \d+ division by zero in x / z: SUCCESS
 y=0
diff --git a/regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.desc b/regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.desc
index 9c561b2433b..8b3cce08da5 100644
--- a/regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.desc
+++ b/regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.desc
@@ -1,6 +1,6 @@
 CORE
 signed_overflow.c
---incremental-smt2-solver 'z3 --smt2 -in' --signed-overflow-check --trace
+--signed-overflow-check --trace
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc b/regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc
index cb971aec828..cdf8a033eec 100644
--- a/regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc
+++ b/regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc
@@ -1,7 +1,7 @@
 CORE
 control_flow.c
---incremental-smt2-solver 'z3 --smt2 -in' --verbosity 10
-Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
+--verbosity 10
+Passing problem to incremental SMT2 solving via
 Sending command to SMT2 solver - \(set-option :produce-models true\)
 Sending command to SMT2 solver - \(set-logic QF_UFBV\)
 Sending command to SMT2 solver - \(declare-fun |goto_symex::&92;guard#1| \(\) Bool\)
diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc b/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc
index 38b41075e78..4212286e9fd 100644
--- a/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc
+++ b/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc
@@ -1,7 +1,7 @@
 CORE
 test.c
---incremental-smt2-solver 'z3 --smt2 -in' --verbosity 10
-Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
+--verbosity 10
+Passing problem to incremental SMT2 solving via
 Sending command to SMT2 solver - \(set-option :produce-models true\)
 Sending command to SMT2 solver - \(set-logic QF_UFBV\)
 Sending command to SMT2 solver - \(define-fun |B0| \(\) Bool true\)
diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/stdbool.desc b/regression/cbmc-incr-smt2/nondeterministic-int-assert/stdbool.desc
index 2135ea76791..61d49d1fbe5 100644
--- a/regression/cbmc-incr-smt2/nondeterministic-int-assert/stdbool.desc
+++ b/regression/cbmc-incr-smt2/nondeterministic-int-assert/stdbool.desc
@@ -1,7 +1,7 @@
 CORE
 stdbool_example.c
---incremental-smt2-solver 'z3 --smt2 -in' --trace
-Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
+--trace
+Passing problem to incremental SMT2 solving via
 VERIFICATION FAILED
 equal=FALSE\s*\([0 ]+\)
 equal=TRUE\s*\([0 ]+1\)
diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/trace.desc b/regression/cbmc-incr-smt2/nondeterministic-int-assert/trace.desc
index d7546c34f8c..69bdd2bf605 100644
--- a/regression/cbmc-incr-smt2/nondeterministic-int-assert/trace.desc
+++ b/regression/cbmc-incr-smt2/nondeterministic-int-assert/trace.desc
@@ -1,7 +1,7 @@
 CORE
 trace.c
---incremental-smt2-solver 'z3 --smt2 -in' --trace
-Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
+--trace
+Passing problem to incremental SMT2 solving via
 Assert of inequality to 4\.: FAILURE
 Assert of inequality to 2\.: FAILURE
 y=4
diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/valid_unsat.desc b/regression/cbmc-incr-smt2/nondeterministic-int-assert/valid_unsat.desc
index e34ae2426b4..7535bf54fa0 100644
--- a/regression/cbmc-incr-smt2/nondeterministic-int-assert/valid_unsat.desc
+++ b/regression/cbmc-incr-smt2/nondeterministic-int-assert/valid_unsat.desc
@@ -1,7 +1,7 @@
 CORE
 valid_unsat.c
---incremental-smt2-solver 'z3 --smt2 -in' --verbosity 10
-Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
+--verbosity 10
+Passing problem to incremental SMT2 solving via
 Sending command to SMT2 solver - \(check-sat\)
 Solver response - unsat
 VERIFICATION SUCCESSFUL