Drop support for CVC4

.github/ci.sh

@@ -87,7 +87,6 @@ install_solvers() {
   export PATH=$BIN:$PATH
   echo "$BIN" >> "$GITHUB_PATH"
   is_exe   "$BIN" z3 && \
-    is_exe "$BIN" cvc4 && \
     is_exe "$BIN" cvc5 && \
     is_exe "$BIN" boolector && \
     is_exe "$BIN" bitwuzla && \

crucible/CHANGELOG.md

@@ -1,7 +1,10 @@
 # next
 
-* Add `withStateBackend` and additional infrastructure for including stack 
+* Add `withStateBackend` and additional infrastructure for including stack
   traces in `SimError` and `IsSymBackend`
+* The CVC4 SMT solver is no longer supported. As such,
+  `Lang.Crucible.Backend.Online` no longer defines `CVC4OnlineBackend` or
+  `withCVC4OnlineBackend`.
 
 # 0.9 -- 2026-01-29
 

crucible/crucible.cabal

@@ -13,10 +13,10 @@ Description:
   Crucible provides a program representation format based on single-static assignment
   (SSA) form control flow graphs, and a symbolic simulation engine for executing
   programs expressed in this format.  It also provides support for communicating with
-  a variety of SAT and SMT solvers, including Z3, CVC4, Yices, STP, and dReal.
+  a variety of SAT and SMT solvers, including Z3, CVC5, Yices, STP, and dReal.
   .
   For an overview of Crucible please have a look at "Lang.Crucible.README"
-  
+
 extra-doc-files: CHANGELOG.md
 
 source-repository head
@@ -141,7 +141,7 @@ common bldflags
       -Werror=badly-staged-types
       -Werror=data-kinds-tc
       -Werror=incomplete-record-selectors
-              
+
   -- TODO(#1308): Enable and fix this warning when GHC 9.6 is dropped from CI
   -- -Werror=deprecated-type-abstractions
 

crucible/src/Lang/Crucible/Backend/Online.hs

@@ -67,9 +67,6 @@ module Lang.Crucible.Backend.Online
     -- ** Boolector
   , BoolectorOnlineBackend
   , withBoolectorOnlineBackend
-    -- ** CVC4
-  , CVC4OnlineBackend
-  , withCVC4OnlineBackend
     -- ** CVC5
   , CVC5OnlineBackend
   , withCVC5OnlineBackend
@@ -104,7 +101,6 @@ import           What4.Protocol.SMTLib2 as SMT2
 import           What4.SatResult
 import qualified What4.Solver.Bitwuzla as Bitwuzla
 import qualified What4.Solver.Boolector as Boolector
-import qualified What4.Solver.CVC4 as CVC4
 import qualified What4.Solver.CVC5 as CVC5
 import qualified What4.Solver.STP as STP
 import qualified What4.Solver.Yices as Yices
@@ -561,26 +557,6 @@ withBoolectorOnlineBackend sym unsatFeat action =
     liftIO $ tryExtendConfig Boolector.boolectorOptions (getConfiguration sym)
     action bak
 
-type CVC4OnlineBackend scope st fs = OnlineBackend (SMT2.Writer CVC4.CVC4) scope st fs
-
--- | Do something with a CVC4 online backend.
---   The backend is only valid in the continuation.
---
---   The CVC4 configuration options will be automatically
---   installed into the backend configuration object.
-withCVC4OnlineBackend ::
-  (MonadIO m, MonadMask m) =>
-  B.ExprBuilder scope st fs ->
-  UnsatFeatures ->
-  ProblemFeatures ->
-  (CVC4OnlineBackend scope st fs -> m a) ->
-  m a
-withCVC4OnlineBackend sym unsatFeat extraFeatures action =
-  let feat = (SMT2.defaultFeatures CVC4.CVC4 .|. unsatFeaturesToProblemFeatures unsatFeat .|. extraFeatures) in
-  withOnlineBackend sym feat $ \bak -> do
-    liftIO $ tryExtendConfig CVC4.cvc4Options (getConfiguration sym)
-    action bak
-
 type CVC5OnlineBackend scope st fs = OnlineBackend (SMT2.Writer CVC5.CVC5) scope st fs
 
 -- | Do something with a CVC5 online backend.

crux-llvm/CHANGELOG.md

@@ -1,5 +1,8 @@
 # next
 
+* The CVC4 SMT solver is no longer supported. As such, the `--solver`
+  command-line option no longer accepts `cvc4` as a valid option.
+
 # 0.12 -- 2026-01-29
 
 # 0.11 -- 2025-11-09

crux-llvm/README.md

@@ -17,7 +17,7 @@ to the `LICENSE` file. Some binary distributions of `crux-llvm` come bundled
 with external compilers and SMT solvers:
 
 * `clang` and `llvm-link` (Apache v2.0 licensed)
-* CVC4 (BSD-3 licensed)
+* CVC5 (BSD-3 licensed)
 * Yices (GPLv3 licensed)
 * Z3 (MIT licensed)
 
@@ -48,7 +48,7 @@ software:
 
 We have tested `crux-llvm` most heavily with GHC 9.4, GHC 9.6, GHC 9.8,
 and `cabal` version 3.10. We recommend Yices 2.6.x, and Z3
-4.8.x. Technically, only one of Yices or Z3 is required, and CVC4 is
+4.8.x. Technically, only one of Yices or Z3 is required, and CVC5 is
 also supported. However, in practice, having both tends to be
 convenient. Finally, LLVM versions from 3.6 through 21 are likely to
 work well, and any failures with versions in that range should be
@@ -281,7 +281,7 @@ In addition, the following flags can optionally be provided:
 * `--floating-point=FPREP`, `-f FPREP`: Select the floating point
   representation to use. The value of `FPREP` can be one of `real`,
   `ieee`, `uninterpreted`, or `default`. Default representation is
-  solver specific: `real` for CVC4 and Yices, and `ieee` for Z3.
+  solver specific: `real` for CVC5 and Yices, and `ieee` for Z3.
 
 * `--iteration-bound=N`, `-i N`: Set a bound on the number of times a
   single loop can iterate. This can also make it more likely to get at
@@ -304,7 +304,7 @@ In addition, the following flags can optionally be provided:
 
 * `--solver=NAME`, `-s NAME`: Use the given SMT solver to discharge
   proof obligations. Valid values for `NAME` are `bitwuzla`, `boolector`,
-  `cvc4`, `cvc5`, `yices`, and `z3`.
+  `cvc5`, `yices`, and `z3`.
 
 * `--timeout=N`, `-t N`: Set the timeout for the first phase of analysis
   (symbolic execution) which happens before sending the main goals to an

crux-llvm/svcomp/mk-svcomp-bindist.sh

@@ -40,7 +40,6 @@ bundle_crux_llvm_svcomp_files() {
 
   # SV-COMP–specific requirements begin
   ## SMT solvers
-  cp "$(which cvc4)"       dist/bin/
   cp "$(which yices)"      dist/bin/
   cp "$(which yices-smt2)" dist/bin/
   cp "$(which z3)"         dist/bin/

crux-llvm/test/Test.hs

@@ -172,16 +172,6 @@ getSTPVersion =
       getVer (Left full) = full
   in mkVC "stp" . getVer <$> readProcessVersion "stp"
 
-getCVC4Version :: IO VersionCheck
-getCVC4Version =
-  let getVer (Right inp) =
-        -- example inp: "This is CVC4 version 1.8\ncompiled ..."
-        case words inp of
-          "This":"is":"CVC4":"version":verNum:_ -> verNum
-          _ -> "?"
-      getVer (Left full) = full
-  in mkVC "cvc4" . getVer <$> readProcessVersion "cvc4"
-
 getCVC5Version :: IO VersionCheck
 getCVC5Version =
   let getVer (Right inp) =
@@ -384,7 +374,6 @@ mkTest sweet _ expct =
       "z3" -> getZ3Version
       "yices" -> getYicesVersion
       "stp" -> getSTPVersion
-      "cvc4" -> getCVC4Version
       "cvc5" -> getCVC5Version
       "boolector" -> getBoolectorVersion
       "bitwuzla" -> getBitwuzlaVersion

crux-mir/CHANGELOG.md

@@ -4,6 +4,9 @@ This release supports [version
 9](https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md#9) of
 `mir-json`'s schema.
 
+* The CVC4 SMT solver is no longer supported. As such, the `--solver`
+  command-line option no longer accepts `cvc4` as a valid option.
+
 # 0.12 -- 2026-01-29
 
 This release supports [version

crux/CHANGELOG.md

@@ -1,5 +1,9 @@
 # next
 
+* The CVC4 SMT solver is no longer supported. As such, the `CVC4` data
+  constructor in `SolverOnline` has been removed, and `crux`'s `--solver`
+  command-line option no longer accepts `cvc4` as a valid option.
+
 # 0.9 -- 2026-01-29
 
 # 0.8 -- 2025-11-09

crux/src/Crux.hs

@@ -83,7 +83,6 @@ import           What4.Interface (IsExprBuilder, getConfiguration)
 import           What4.Protocol.Online (OnlineSolver)
 import qualified What4.Solver as WS
 import           What4.Solver.Bitwuzla (bitwuzlaTimeout)
-import           What4.Solver.CVC4 (cvc4Timeout)
 import           What4.Solver.CVC5 (cvc5Timeout)
 import           What4.Solver.Yices (yicesEnableMCSat, yicesGoalTimeout)
 import           What4.Solver.Z3 (z3Timeout)
@@ -375,7 +374,6 @@ withSelectedOnlineBackend cruxOpts nonceGen selectedSolver maybeExplicitFloatMod
     "default" ->
       case selectedSolver of
         CCS.Yices -> withOnlineBackendFM WE.FloatRealRepr
-        CCS.CVC4 -> withOnlineBackendFM WE.FloatRealRepr
         CCS.CVC5 -> withOnlineBackendFM WE.FloatRealRepr
         CCS.STP -> withOnlineBackendFM WE.FloatRealRepr
         CCS.Z3 -> withOnlineBackendFM WE.FloatIEEERepr
@@ -416,11 +414,6 @@ withSelectedOnlineBackend' cruxOpts selectedSolver sym k =
          Just s -> symCfg sym yicesGoalTimeout (floor s)
          Nothing -> return ()
        k bak
-     CCS.CVC4 -> withCVC4OnlineBackend sym unsatCoreFeat extraFeatures $ \bak -> do
-       case goalTimeout cruxOpts of
-         Just s -> symCfg sym cvc4Timeout (floor (s * 1000))
-         Nothing -> return ()
-       k bak
      CCS.CVC5 -> withCVC5OnlineBackend sym unsatCoreFeat extraFeatures $ \bak -> do
        case goalTimeout cruxOpts of
          Just s -> symCfg sym cvc5Timeout (floor (s * 1000))
@@ -573,7 +566,6 @@ withSolverAdapter solverOff k =
     CCS.Boolector -> k WS.boolectorAdapter
     CCS.DReal -> k WS.drealAdapter
     CCS.RME -> k rmeAdapter
-    CCS.SolverOnline CCS.CVC4 -> k WS.cvc4Adapter
     CCS.SolverOnline CCS.CVC5 -> k WS.cvc5Adapter
     CCS.SolverOnline CCS.STP -> k WS.stpAdapter
     CCS.SolverOnline CCS.Yices -> k WS.yicesAdapter

crux/src/Crux/Config/Common.hs

@@ -318,7 +318,7 @@ cruxOptions = Config
             section "floating-point" stringSpec "default"
             (pack $ "Select floating point representation,"
              ++ " i.e. one of [real|ieee|uninterpreted|default]. "
-             ++ "Default representation is solver specific: [cvc4|yices]=>real, z3=>ieee.")
+             ++ "Default representation is solver specific: yices=>real, z3=>ieee.")
 
           hashConsing <-
             section "hash-consing" yesOrNoSpec False
@@ -530,7 +530,7 @@ cruxOptions = Config
       , Option "f" ["floating-point"]
         ("Select floating point representation,"
          ++ " i.e. one of [real|ieee|uninterpreted|default]. "
-         ++ "Default representation is solver specific: [cvc4|yices]=>real, z3=>ieee.")
+         ++ "Default representation is solver specific: yices=>real, z3=>ieee.")
         $ ReqArg "FPREP" $ \v opts -> Right opts { floatMode = map toLower v }
 
       , Option [] ["debug"]

crux/src/Crux/Config/Solver.hs

@@ -23,7 +23,7 @@ import qualified What4.InterpretedFloatingPoint as WIF
 
 import qualified Crux.Config.Common as CCC
 
-data SolverOnline = Yices | Z3 | CVC4 | CVC5 | STP | Bitwuzla
+data SolverOnline = Yices | Z3 | CVC5 | STP | Bitwuzla
   deriving (Eq, Ord, Show)
 data SolverOffline = SolverOnline SolverOnline | Boolector | DReal | RME
   deriving (Eq, Ord, Show)
@@ -38,7 +38,6 @@ class HasDefaultFloatRepr solver where
 instance HasDefaultFloatRepr SolverOnline where
   withDefaultFloatRepr _ s k =
     case s of
-      CVC4 -> k WEB.FloatRealRepr
       CVC5 -> k WEB.FloatRealRepr
       STP -> k WEB.FloatRealRepr
       Yices -> k WEB.FloatRealRepr
@@ -125,15 +124,14 @@ asAnyOfflineSolver s = case s of
       "rme" -> pure RME
       "z3" -> pure (SolverOnline Z3)
       "yices" -> pure (SolverOnline Yices)
-      "cvc4" -> pure (SolverOnline CVC4)
       "cvc5" -> pure (SolverOnline CVC5)
       "stp" -> pure (SolverOnline STP)
       "bitwuzla" -> pure (SolverOnline Bitwuzla)
-      _ -> invalid (printf "%s is not a valid solver (expected dreal, boolector, z3, yices, cvc4, cvc5, stp, rme, or bitwuzla)" s)
+      _ -> invalid (printf "%s is not a valid solver (expected dreal, boolector, z3, yices, cvc5, stp, rme, or bitwuzla)" s)
 
 asManyOfflineSolvers :: String -> Validated [SolverOffline]
 asManyOfflineSolvers s
-  | s == "all"         = asManyOfflineSolvers "dreal,boolector,z3,yices,cvc4,cvc5,stp,bitwuzla,rme"
+  | s == "all"         = asManyOfflineSolvers "dreal,boolector,z3,yices,cvc5,stp,bitwuzla,rme"
   | length solvers > 1 = traverse asAnyOfflineSolver solvers
   | otherwise          = invalid (printf "%s is not a valid solver list (expected 'all' or a comma separated list of solvers)" s)
   where
@@ -144,12 +142,11 @@ asOnlineSolver :: String -> Validated SolverOnline
 asOnlineSolver s =
   case s of
     "yices" -> pure Yices
-    "cvc4" -> pure CVC4
     "cvc5" -> pure CVC5
     "z3" -> pure Z3
     "stp" -> pure STP
     "bitwuzla" -> pure Bitwuzla
-    _ -> invalid (printf "%s is not a valid online solver (expected yices, cvc4, cvc5, z3, stp, or bitwuzla)" s)
+    _ -> invalid (printf "%s is not a valid online solver (expected yices, cvc5, z3, stp, or bitwuzla)" s)
 
 -- | Examine a 'CCC.CruxOptions' and determine what solver configuration to use for
 -- symbolic execution.  This can fail if an invalid solver configuration is