diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml
index f8218b86da1..e2b15483d74 100644
--- a/.github/workflows/pull-request-checks.yaml
+++ b/.github/workflows/pull-request-checks.yaml
@@ -18,6 +18,8 @@ jobs:
         run: |
           sudo apt-get update
           sudo apt-get install --no-install-recommends -yq gcc gdb g++ maven jq flex bison libxml2-utils ccache cmake z3
+      - name: Confirm z3 solver is available and log the version installed
+        run: z3 --version
       - name: Prepare ccache
         uses: actions/cache@v2
         with:
@@ -78,6 +80,8 @@ jobs:
           sudo apt-get install --no-install-recommends -yq clang-10 clang++-10 gdb maven jq flex bison libxml2-utils cpanminus ccache z3
           make -C src minisat2-download
           cpanm Thread::Pool::Simple
+      - name: Confirm z3 solver is available and log the version installed
+        run: z3 --version
       - name: Prepare ccache
         uses: actions/cache@v2
         with:
@@ -129,6 +133,8 @@ jobs:
         run: |
           sudo apt-get update
           sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc g++ maven flex bison libxml2-utils dpkg-dev ccache doxygen z3
+      - name: Confirm z3 solver is available and log the version installed
+        run: z3 --version
       - name: Prepare ccache
         uses: actions/cache@v2
         with:
@@ -172,6 +178,8 @@ jobs:
           submodules: recursive
       - name: Fetch dependencies
         run: brew install maven flex bison parallel ccache z3
+      - name: Confirm z3 solver is available and log the version installed
+        run: z3 --version
       - name: Prepare ccache
         uses: actions/cache@v2
         with:
@@ -212,6 +220,8 @@ jobs:
           submodules: recursive
       - name: Fetch dependencies
         run: brew install cmake ninja maven flex bison ccache z3
+      - name: Confirm z3 solver is available and log the version installed
+        run: z3 --version
       - name: Prepare ccache
         uses: actions/cache@v2
         with:
@@ -248,9 +258,14 @@ jobs:
           submodules: recursive
       - name: Fetch dependencies
         run: |
-          choco install winflexbison3 z3
+          choco install winflexbison3
           nuget install clcache -OutputDirectory "c:\tools" -ExcludeVersion -Version 4.1.0
           echo "c:\tools\clcache\clcache-4.1.0" >> $env:GITHUB_PATH
+          Invoke-WebRequest -Uri https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-win.zip -OutFile .\z3.zip
+          Expand-Archive -LiteralPath '.\z3.Zip' -DestinationPath C:\tools
+          echo "c:\tools\z3-4.8.10-x64-win\bin;" >> $env:GITHUB_PATH
+      - name: Confirm z3 solver is available and log the version installed
+        run: z3 --version
       - name: Setup Visual Studio environment
         uses: microsoft/setup-msbuild@v1.0.2
       - name: Prepare ccache
@@ -292,6 +307,11 @@ jobs:
           echo "c:\tools\clcache\clcache-4.1.0" >> $env:GITHUB_PATH
           echo "c:\ProgramData\chocolatey\bin" >> $env:GITHUB_PATH
           echo "c:\Strawberry\" >> $env:GITHUB_PATH
+          Invoke-WebRequest -Uri https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-win.zip -OutFile .\z3.zip
+          Expand-Archive -LiteralPath '.\z3.Zip' -DestinationPath C:\tools
+          echo "c:\tools\z3-4.8.10-x64-win\bin;" >> $env:GITHUB_PATH
+      - name: Confirm z3 solver is available and log the version installed
+        run: z3 --version
       - name: Setup MSBuild
         uses: microsoft/setup-msbuild@v1.0.2
       - name: Initialise Developer Command Line
@@ -428,11 +448,13 @@ jobs:
       - name: Fetch dependencies
         run: | 
           sudo apt-get update
-          sudo apt-get install --no-install-recommends -y g++ flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache
+          sudo apt-get install --no-install-recommends -y g++ flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache z3
           # remove libgcc-s1, which isn't normally available in Ubuntu 18.04
           target=$(dpkg-query -W --showformat='${Version}\n' gcc-8-base | head -n 1)
           # libgcc1 uses an epoch, thus the extra 1:
           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
+      - name: Confirm z3 solver is available and log the version installed
+        run: z3 --version
       - name: Prepare ccache
         uses: actions/cache@v2
         with:
@@ -515,6 +537,8 @@ jobs:
         run: |
           sudo apt-get update
           sudo apt-get install --no-install-recommends -y g++ gcc binutils flex bison cmake maven jq libxml2-utils openjdk-11-jdk-headless lcov ccache z3
+      - name: Confirm z3 solver is available and log the version installed
+        run: z3 --version
       - name: Prepare ccache
         uses: actions/cache@v2
         with:
diff --git a/regression/cbmc/z3/invalid.c b/regression/cbmc/z3/invalid.c
new file mode 100644
index 00000000000..5c753a292da
--- /dev/null
+++ b/regression/cbmc/z3/invalid.c
@@ -0,0 +1,8 @@
+#include <assert.h>
+
+int main()
+{
+  unsigned int non_det;
+  assert(non_det * non_det != 9u);
+  return 0;
+}
diff --git a/regression/cbmc/z3/invalid.desc b/regression/cbmc/z3/invalid.desc
new file mode 100644
index 00000000000..e6bc587e7ad
--- /dev/null
+++ b/regression/cbmc/z3/invalid.desc
@@ -0,0 +1,14 @@
+CORE
+invalid.c
+--trace --smt2 --z3
+^EXIT=10$
+^SIGNAL=0$
+line 6 assertion non_det \* non_det != 9u: FAILURE
+non_det=\d+u
+VERIFICATION FAILED
+--
+line 6 assertion non_det \* non_det != 9u: ERROR
+error running SMT2 solver
+--
+Run cbmc with the --z3 option to confirm that support for the Z3 solver is
+available and working for an invalid program where the assertion may fail.
diff --git a/regression/cbmc/z3/valid.c b/regression/cbmc/z3/valid.c
new file mode 100644
index 00000000000..946a5dfa8bd
--- /dev/null
+++ b/regression/cbmc/z3/valid.c
@@ -0,0 +1,8 @@
+#include <assert.h>
+
+int main()
+{
+  unsigned int non_det;
+  assert(non_det * non_det != 12u);
+  return 0;
+}
diff --git a/regression/cbmc/z3/valid.desc b/regression/cbmc/z3/valid.desc
new file mode 100644
index 00000000000..ced8c4b6e56
--- /dev/null
+++ b/regression/cbmc/z3/valid.desc
@@ -0,0 +1,13 @@
+CORE
+valid.c
+--trace --smt2 --z3
+^EXIT=0$
+^SIGNAL=0$
+line 6 assertion non_det \* non_det != 12u: SUCCESS
+VERIFICATION SUCCESSFUL
+--
+line 6 assertion non_det \* non_det != 12u: ERROR
+error running SMT2 solver
+--
+Run cbmc with the --z3 option to confirm that support for the Z3 solver is
+available and working for a valid program.