diff --git a/Data/SBV/Tools/KDKernel.hs b/Data/SBV/Tools/KDKernel.hs
index 56a842acc..2ccfa9fa9 100644
--- a/Data/SBV/Tools/KDKernel.hs
+++ b/Data/SBV/Tools/KDKernel.hs
@@ -97,11 +97,14 @@ sorry = Proof { rootOfTrust = Self
         p (Forall (x :: SBool)) = label "SORRY: KnuckleDragger, proof uses \"sorry\"" x
 
 -- | Helper to generate lemma/theorem statements.
-lemmaGen :: Proposition a => SMTConfig -> String -> [String] -> a -> [Proof] -> KD Proof
+lemmaGen :: Proposition a => KDConfig -> String -> [String] -> a -> [Proof] -> KD Proof
 lemmaGen cfg what nms inputProp by = do
-    tab <- start (verbose cfg) what nms
+    tab <- start (kdVerbose cfg) what nms
 
-    let nm = intercalate "." nms
+    let underlyingSolver = kdSolverConfig cfg
+        solver           = underlyingSolver{verbose = verbose underlyingSolver || kdVerbose cfg}
+
+        nm = intercalate "." nms
 
         -- What to do if all goes well
         good = do finish ("Q.E.D." ++ modulo) tab
@@ -126,14 +129,16 @@ lemmaGen cfg what nms inputProp by = do
 
         -- What to do if the proof fails
         cex  = liftIO $ do putStrLn $ "\n*** Failed to prove " ++ nm ++ "."
+
                            -- When trying to get a counter-example, only include in the
                            -- implication those facts that are user-given axioms. This
                            -- way our counter-example will be more likely to be relevant
                            -- to the proposition we're currently proving. (Hopefully.)
                            -- Remember that we first have to negate, and then skolemize!
-                           SatResult res <- satWith cfg $ do
+                           SatResult res <- satWith solver $ do
                                                mapM_ constrain [getProof | Proof{isUserAxiom, getProof} <- by, isUserAxiom] :: Symbolic ()
                                                pure $ skolemize (qNot inputProp)
+
                            print $ ThmResult res
                            error "Failed"
 
@@ -142,7 +147,7 @@ lemmaGen cfg what nms inputProp by = do
                                print r
                                error "Failed"
 
-    pRes <- liftIO $ proveWith cfg $ do
+    pRes <- liftIO $ proveWith solver $ do
                 mapM_ (constrain . getProof) by :: Symbolic ()
                 pure $ skolemize (quantifiedBool inputProp)
 
@@ -156,20 +161,20 @@ lemmaGen cfg what nms inputProp by = do
 
 -- | Prove a given statement, using auxiliaries as helpers. Using the default solver.
 lemma :: Proposition a => String -> a -> [Proof] -> KD Proof
-lemma nm f by = do KDConfig{kdSolverConfig} <- ask
-                   lemmaWith kdSolverConfig nm f by
+lemma nm f by = do cfg <- ask
+                   lemmaWith cfg nm f by
 
 -- | Prove a given statement, using auxiliaries as helpers. Using the given solver.
-lemmaWith :: Proposition a => SMTConfig -> String -> a -> [Proof] -> KD Proof
+lemmaWith :: Proposition a => KDConfig -> String -> a -> [Proof] -> KD Proof
 lemmaWith cfg nm = lemmaGen cfg "Lemma" [nm]
 
 -- | Prove a given statement, using auxiliaries as helpers. Essentially the same as 'lemma', except for the name, using the default solver.
 theorem :: Proposition a => String -> a -> [Proof] -> KD Proof
-theorem nm f by = do KDConfig{kdSolverConfig} <- ask
-                     theoremWith kdSolverConfig nm f by
+theorem nm f by = do cfg <- ask
+                     theoremWith cfg nm f by
 
 -- | Prove a given statement, using auxiliaries as helpers. Essentially the same as 'lemmaWith', except for the name.
-theoremWith :: Proposition a => SMTConfig -> String -> a -> [Proof] -> KD Proof
+theoremWith :: Proposition a => KDConfig -> String -> a -> [Proof] -> KD Proof
 theoremWith cfg nm = lemmaGen cfg "Theorem" [nm]
 
 -- | Given a predicate, return an induction principle for it. Typically, we only have one viable
diff --git a/Data/SBV/Tools/KDUtils.hs b/Data/SBV/Tools/KDUtils.hs
index ac159d217..60e59b1fc 100644
--- a/Data/SBV/Tools/KDUtils.hs
+++ b/Data/SBV/Tools/KDUtils.hs
@@ -18,7 +18,7 @@
 module Data.SBV.Tools.KDUtils (
          KD, runKD, runKDWith
        , start, finish
-       , KDConfig(..), defaultKDConfig
+       , KDConfig(..), defaultKDConfig, z3KD, cvc5KD
        ) where
 
 import Control.Monad.Reader (ReaderT, runReaderT, ask, MonadReader)
@@ -28,19 +28,29 @@ import Data.List (intercalate)
 import System.IO (hFlush, stdout)
 
 import Data.SBV.Core.Symbolic  (SMTConfig)
-import Data.SBV.Provers.Prover (defaultSMTCfg)
+import Data.SBV.Provers.Prover (defaultSMTCfg, z3, cvc5)
 
 -- | Keeping track of KD options/state
 data KDConfig = KDConfig { kdRibbonLength :: Int        -- ^ Lenght of the line as we print the proof
+                         , kdVerbose      :: Bool       -- ^ Run verbose
                          , kdSolverConfig :: SMTConfig  -- ^ The backend solver to use
                          }
 
--- | Default KD-config
+-- | Default KD-config uses the default SBV config (which is z3)
 defaultKDConfig :: KDConfig
 defaultKDConfig = KDConfig { kdRibbonLength = 40
+                           , kdVerbose      = False
                            , kdSolverConfig = defaultSMTCfg
                            }
 
+-- | Run KD proof with z3 configuration.
+z3KD :: KDConfig
+z3KD = defaultKDConfig{kdSolverConfig = z3}
+
+-- | Run KD proof with z3 configuration.
+cvc5KD :: KDConfig
+cvc5KD = defaultKDConfig{kdSolverConfig = cvc5}
+
 -- | Monad for running KnuckleDragger proofs in.
 newtype KD a = KD (ReaderT KDConfig IO a)
             deriving newtype (Applicative, Functor, Monad, MonadIO, MonadReader KDConfig, MonadFail)
diff --git a/Data/SBV/Tools/KnuckleDragger.hs b/Data/SBV/Tools/KnuckleDragger.hs
index c8dfc11a8..851cf646b 100644
--- a/Data/SBV/Tools/KnuckleDragger.hs
+++ b/Data/SBV/Tools/KnuckleDragger.hs
@@ -42,7 +42,7 @@ module Data.SBV.Tools.KnuckleDragger (
        -- * Faking proofs
        , sorry
        -- * Running KnuckleDragger proofs
-       , KD, runKD, runKDWith, KDConfig(..), defaultKDConfig
+       , KD, runKD, runKDWith, KDConfig(..), defaultKDConfig, z3KD, cvc5KD
        ) where
 
 import Control.Monad.Trans (liftIO)
@@ -80,25 +80,25 @@ class ChainLemma steps step | steps -> step where
   chainTheorem :: Proposition a => String -> a -> steps -> [Proof] -> KD Proof
 
   -- | Prove a property via a series of equality steps, using the given solver.
-  chainLemmaWith :: Proposition a => SMTConfig -> String -> a -> steps -> [Proof] -> KD Proof
+  chainLemmaWith :: Proposition a => KDConfig -> String -> a -> steps -> [Proof] -> KD Proof
 
   -- | Same as chainLemmaWith, except tagged as Theorem
-  chainTheoremWith :: Proposition a => SMTConfig -> String -> a -> steps -> [Proof] -> KD Proof
+  chainTheoremWith :: Proposition a => KDConfig -> String -> a -> steps -> [Proof] -> KD Proof
 
   -- | Internal, shouldn't be needed outside the library
   makeSteps :: steps -> [step]
   makeInter :: steps -> step -> step -> SBool
 
-  chainLemma nm p steps by = do KDConfig{kdSolverConfig} <- ask
-                                chainLemmaWith kdSolverConfig nm p steps by
+  chainLemma nm p steps by = do cfg <- ask
+                                chainLemmaWith cfg nm p steps by
 
-  chainTheorem nm p steps by = do KDConfig{kdSolverConfig} <- ask
-                                  chainTheoremWith kdSolverConfig nm p steps by
+  chainTheorem nm p steps by = do cfg <- ask
+                                  chainTheoremWith cfg nm p steps by
 
   chainLemmaWith   = chainGeneric False
   chainTheoremWith = chainGeneric True
 
-  chainGeneric :: Proposition a => Bool -> SMTConfig -> String -> a -> steps -> [Proof] -> KD Proof
+  chainGeneric :: Proposition a => Bool -> KDConfig -> String -> a -> steps -> [Proof] -> KD Proof
   chainGeneric taggedTheorem cfg nm result steps base = do
         liftIO $ putStrLn $ "Chain: " ++ nm
         let proofSteps = makeSteps steps