diff --git a/.github/ci.sh b/.github/ci.sh
index dc536f6a..f36602ba 100755
--- a/.github/ci.sh
+++ b/.github/ci.sh
@@ -77,7 +77,7 @@ install_system_deps() {
   cp $BIN/yices_smt2$EXT $BIN/yices-smt2$EXT
   export PATH=$BIN:$PATH
   echo "$BIN" >> "$GITHUB_PATH"
-  is_exe "$BIN" z3 && is_exe "$BIN" cvc4 && is_exe "$BIN" yices
+  is_exe "$BIN" z3 && is_exe "$BIN" cvc4 && is_exe "$BIN" cvc5 && is_exe "$BIN" yices
 }
 
 check_docs() {
@@ -132,6 +132,7 @@ zip_dist_with_solvers() {
   sname="${name}-with-solvers"
   cp "$(which abc)"        dist/bin/
   cp "$(which cvc4)"       dist/bin/
+  cp "$(which cvc5)"       dist/bin/
   cp "$(which yices)"      dist/bin/
   cp "$(which yices-smt2)" dist/bin/
   cp "$(which z3)"         dist/bin/
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 52362e64..db40c9fd 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -315,6 +315,7 @@ jobs:
           .github/ci.sh install_system_deps
           .github/ci.sh deps bin/abc*
           .github/ci.sh deps bin/cvc4*
+          .github/ci.sh deps bin/cvc5*
           .github/ci.sh deps bin/yices-smt2*
           .github/ci.sh deps bin/z3*
           ghc_ver="$(ghc --numeric-version)"
diff --git a/CHANGES.md b/CHANGES.md
index d12b799e..608081c5 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -30,10 +30,14 @@
 * Add a syntax highlight file for Vim,
   available in `syntax-highlight/cryptol.vim`
 
-* Add `:new-seed` and `:set-seed` commands to the REPL. 
+* Add `:new-seed` and `:set-seed` commands to the REPL.
   These affect random test generation,
   and help write reproducable Cryptol scripts.
 
+* Add support for the CVC5 solver, which can be selected with
+  `:set prover=cvc5`. If you want to specify a What4 or SBV backend, you can
+  use `:set prover=w4-cvc5` or `:set prover=sbv-cvc5`, respectively.
+
 ## Bug fixes
 
 * Fix a bug in the What4 backend that could cause applications of `(@)` with
diff --git a/Dockerfile b/Dockerfile
index d9a7b5bc..8d8d4c72 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -40,6 +40,7 @@ ENV PATH=/usr/local/bin:/cryptol/rootfs/usr/local/bin:$PATH
 RUN    ! $(cryptol -c ":s prover=yices" | tail -n +2 | grep -q .) \
     #    && ! $(cryptol -c ":s prover=mathsat" | tail -n +2 | grep -q .) \
     && ! $(cryptol -c ":s prover=cvc4" | tail -n +2 | grep -q .) \
+    && ! $(cryptol -c ":s prover=cvc5" | tail -n +2 | grep -q .) \
     && ! $(cryptol -c ":s prover=abc" | tail -n +2 | grep -q .) \
     # && ! $(cryptol -c ":s prover=boolector" | tail -n +2 | grep -q .) \
     && ! $(cryptol -c ":s prover=z3" | tail -n +2 | grep -q .)
diff --git a/README.md b/README.md
index 82640844..0dd7d1ce 100644
--- a/README.md
+++ b/README.md
@@ -25,7 +25,7 @@ predicates written in Cryptol against randomly-generated test vectors
 (in the style of
 [QuickCheck](http://hackage.haskell.org/package/QuickCheck)). There is
 also a `:prove` command, which calls out to SMT solvers, such as
-Yices, Z3, or CVC4, to prove predicates for all possible inputs.
+Yices, Z3, CVC4, or CVC5, to prove predicates for all possible inputs.
 
 # Getting Cryptol Binaries
 
diff --git a/cabal.GHC-8.10.7.config b/cabal.GHC-8.10.7.config
index 6fc6e450..dc6a3adb 100644
--- a/cabal.GHC-8.10.7.config
+++ b/cabal.GHC-8.10.7.config
@@ -207,7 +207,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              s-cargot -build-example,
              any.safe ==0.3.19,
              any.safe-exceptions ==0.1.7.3,
-             any.sbv ==9.0,
+             any.sbv ==9.2,
              any.scientific ==0.3.7.0,
              scientific -bytestring-builder -integer-simple,
              any.scotty ==0.12.1,
diff --git a/cabal.GHC-9.2.4.config b/cabal.GHC-9.2.4.config
index 3d21ea61..95f60406 100644
--- a/cabal.GHC-9.2.4.config
+++ b/cabal.GHC-9.2.4.config
@@ -208,7 +208,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              s-cargot -build-example,
              any.safe ==0.3.19,
              any.safe-exceptions ==0.1.7.3,
-             any.sbv ==9.0,
+             any.sbv ==9.2,
              any.scientific ==0.3.7.0,
              scientific -bytestring-builder -integer-simple,
              any.scotty ==0.12.1,
diff --git a/cabal.GHC-9.4.4.config b/cabal.GHC-9.4.4.config
index ea5146d5..a8b341b6 100644
--- a/cabal.GHC-9.4.4.config
+++ b/cabal.GHC-9.4.4.config
@@ -208,7 +208,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              s-cargot -build-example,
              any.safe ==0.3.19,
              any.safe-exceptions ==0.1.7.3,
-             any.sbv ==9.0,
+             any.sbv ==9.2,
              any.scientific ==0.3.7.0,
              scientific -bytestring-builder -integer-simple,
              any.scotty ==0.12.1,
diff --git a/cryptol-remote-api/docs/Cryptol.rst b/cryptol-remote-api/docs/Cryptol.rst
index 38f6144d..54a4c616 100644
--- a/cryptol-remote-api/docs/Cryptol.rst
+++ b/cryptol-remote-api/docs/Cryptol.rst
@@ -557,7 +557,7 @@ Parameter fields
 
 
 ``prover``
-  The SMT solver to use to check for satisfiability. I.e., one of the following: ``w4-cvc4``, ``w4-yices``, ``w4-z3``, ``w4-boolector``, ``w4-abc``, ``w4-offline``, ``w4-any``, ``cvc4``, ``yices``, ``z3``, ``boolector``, ``mathsat``, ``abc``, ``offline``, ``any``, ``sbv-cvc4``, ``sbv-yices``, ``sbv-z3``, ``sbv-boolector``, ``sbv-mathsat``, ``sbv-abc``, ``sbv-offline``, ``sbv-any``.
+  The SMT solver to use to check for satisfiability. I.e., one of the following: ``w4-cvc4``, ``w4-cvc5``, ``w4-yices``, ``w4-z3``, ``w4-boolector``, ``w4-abc``, ``w4-offline``, ``w4-any``, ``cvc4``, ``cvc5``, ``yices``, ``z3``, ``boolector``, ``mathsat``, ``abc``, ``offline``, ``any``, ``sbv-cvc4``, ``sbv-cvc5``, ``sbv-yices``, ``sbv-z3``, ``sbv-boolector``, ``sbv-mathsat``, ``sbv-abc``, ``sbv-offline``, ``sbv-any``.
   
   
 
diff --git a/cryptol-remote-api/python/cryptol/solver.py b/cryptol-remote-api/python/cryptol/solver.py
index 99484fcf..d8246e2a 100644
--- a/cryptol-remote-api/python/cryptol/solver.py
+++ b/cryptol-remote-api/python/cryptol/solver.py
@@ -52,6 +52,7 @@ class OfflineSolver(Solver):
 # Cryptol-supported SMT configurations/solvers
 # (see Cryptol.Symbolic.SBV Haskell module)
 CVC4: OnlineSolver          = OnlineSolver("cvc4")
+CVC5: OnlineSolver          = OnlineSolver("cvc5")
 YICES: OnlineSolver         = OnlineSolver("yices")
 Z3: OnlineSolver            = OnlineSolver("z3")
 BOOLECTOR: OnlineSolver     = OnlineSolver("boolector")
@@ -60,6 +61,7 @@ ABC: OnlineSolver           = OnlineSolver("abc")
 OFFLINE: OfflineSolver      = OfflineSolver("offline")
 ANY: OnlineSolver           = OnlineSolver("any")
 SBV_CVC4: OnlineSolver      = OnlineSolver("sbv-cvc4")
+SBV_CVC5: OnlineSolver      = OnlineSolver("sbv-cvc5")
 SBV_YICES: OnlineSolver     = OnlineSolver("sbv-yices")
 SBV_Z3: OnlineSolver        = OnlineSolver("sbv-z3")
 SBV_BOOLECTOR: OnlineSolver = OnlineSolver("sbv-boolector")
@@ -68,6 +70,7 @@ SBV_ABC: OnlineSolver       = OnlineSolver("sbv-abc")
 SBV_OFFLINE: OfflineSolver  = OfflineSolver("sbv-offline")
 SBV_ANY: OnlineSolver       = OnlineSolver("sbv-any")
 W4_CVC4: OnlineSolver       = OnlineSolver("w4-cvc4")
+W4_CVC5: OnlineSolver       = OnlineSolver("w4-cvc5")
 W4_YICES: OnlineSolver      = OnlineSolver("w4-yices")
 W4_Z3: OnlineSolver         = OnlineSolver("w4-z3")
 W4_BOOLECTOR: OnlineSolver  = OnlineSolver("w4-boolector")
diff --git a/cryptol.cabal b/cryptol.cabal
index 7dac3d7e..1f690cfb 100644
--- a/cryptol.cabal
+++ b/cryptol.cabal
@@ -73,7 +73,7 @@ library
                        pretty,
                        prettyprinter     >= 1.7.0,
                        process           >= 1.2,
-                       sbv               >= 8.10 && < 9.1,
+                       sbv               >= 9.1 && < 9.3,
                        simple-smt        >= 0.9.7,
                        stm               >= 2.4,
                        strict,
diff --git a/cryptol/Main.hs b/cryptol/Main.hs
index 13e001b7..253c8493 100644
--- a/cryptol/Main.hs
+++ b/cryptol/Main.hs
@@ -200,7 +200,7 @@ displayHelp errs = do
             , "via the `:edit` command"
             ]
           )
-        , ( "SBV_{ABC,BOOLECTOR,CVC4,MATHSAT,YICES,Z3}_OPTIONS"
+        , ( "SBV_{ABC,BOOLECTOR,CVC4,CVC5,MATHSAT,YICES,Z3}_OPTIONS"
           , [ "A string of command-line arguments to be passed to the"
             , "corresponding solver invoked for `:sat` and `:prove`"
             , "when using a prover via SBV"
diff --git a/src/Cryptol/Symbolic/SBV.hs b/src/Cryptol/Symbolic/SBV.hs
index 7679c964..2e3e895b 100644
--- a/src/Cryptol/Symbolic/SBV.hs
+++ b/src/Cryptol/Symbolic/SBV.hs
@@ -81,6 +81,7 @@ doSBVEval m =
 proverConfigs :: [(String, SBV.SMTConfig)]
 proverConfigs =
   [ ("cvc4"     , SBV.cvc4     )
+  , ("cvc5"     , SBV.cvc5     )
   , ("yices"    , SBV.yices    )
   , ("z3"       , SBV.z3       )
   , ("boolector", SBV.boolector)
@@ -90,6 +91,7 @@ proverConfigs =
   , ("any"      , SBV.defaultSMTCfg )
 
   , ("sbv-cvc4"     , SBV.cvc4     )
+  , ("sbv-cvc5"     , SBV.cvc5     )
   , ("sbv-yices"    , SBV.yices    )
   , ("sbv-z3"       , SBV.z3       )
   , ("sbv-boolector", SBV.boolector)
diff --git a/src/Cryptol/Symbolic/What4.hs b/src/Cryptol/Symbolic/What4.hs
index 1e9f290d..d7cb7f8c 100644
--- a/src/Cryptol/Symbolic/What4.hs
+++ b/src/Cryptol/Symbolic/What4.hs
@@ -83,6 +83,7 @@ import qualified What4.SWord as SW
 import           What4.Solver
 import qualified What4.Solver.Boolector as W4
 import qualified What4.Solver.CVC4 as W4
+import qualified What4.Solver.CVC5 as W4
 import qualified What4.Solver.ExternalABC as W4
 import qualified What4.Solver.Yices as W4
 import qualified What4.Solver.Z3 as W4
@@ -161,6 +162,7 @@ data W4ProverConfig
 proverConfigs :: [(String, W4ProverConfig)]
 proverConfigs =
   [ ("w4-cvc4"      , W4ProverConfig cvc4OnlineAdapter)
+  , ("w4-cvc5"      , W4ProverConfig cvc5OnlineAdapter)
   , ("w4-yices"     , W4ProverConfig yicesOnlineAdapter)
   , ("w4-z3"        , W4ProverConfig z3OnlineAdapter)
   , ("w4-boolector" , W4ProverConfig boolectorOnlineAdapter)
@@ -186,6 +188,11 @@ cvc4OnlineAdapter =
   AnOnlineAdapter "CVC4" W4.cvc4Features W4.cvc4Options
          (Proxy :: Proxy (W4.Writer W4.CVC4))
 
+cvc5OnlineAdapter :: AnAdapter
+cvc5OnlineAdapter =
+  AnOnlineAdapter "CVC5" W4.cvc5Features W4.cvc5Options
+         (Proxy :: Proxy (W4.Writer W4.CVC5))
+
 boolectorOnlineAdapter :: AnAdapter
 boolectorOnlineAdapter =
   AnOnlineAdapter "Boolector" W4.boolectorFeatures W4.boolectorOptions
@@ -195,6 +202,7 @@ allSolvers :: W4ProverConfig
 allSolvers = W4Portfolio
   $ z3OnlineAdapter :|
   [ cvc4OnlineAdapter
+  , cvc5OnlineAdapter
   , boolectorOnlineAdapter
   , yicesOnlineAdapter
   , AnAdapter W4.externalABCAdapter
diff --git a/tests/issues/issue1503.cry b/tests/issues/issue1503.cry
new file mode 100644
index 00000000..ddf17798
--- /dev/null
+++ b/tests/issues/issue1503.cry
@@ -0,0 +1,4 @@
+add_mul_lemma : Integer -> Integer -> Integer -> Integer -> Bit
+add_mul_lemma m n p q =
+  (0 <= m /\ 0 <= n /\ 0 <= p /\ 0 <= q /\ n < q /\ p < m) ==>
+  (m * n + p < m * q)
diff --git a/tests/issues/issue1503.icry b/tests/issues/issue1503.icry
new file mode 100644
index 00000000..9726d6ea
--- /dev/null
+++ b/tests/issues/issue1503.icry
@@ -0,0 +1,11 @@
+:l issue1503.cry
+
+:set prover=w4-cvc5
+:prove add_mul_lemma
+
+// We avoid testing sbv-cvc5 for now, as using CVC5 with SBV on Windows will go
+// likely go into an infinite loop.
+// See https://github.com/LeventErkok/sbv/issues/644.
+//
+// :set prover=sbv-cvc5
+// :prove add_mul_lemma
diff --git a/tests/issues/issue1503.icry.stdout b/tests/issues/issue1503.icry.stdout
new file mode 100644
index 00000000..52cd4132
--- /dev/null
+++ b/tests/issues/issue1503.icry.stdout
@@ -0,0 +1,4 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+Q.E.D.