diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -6,6 +6,17 @@
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [PVP versioning](https://pvp.haskell.org/).
 
+## v2.1.0 _(2024-07-26)_
+
+### Added
+- Added solver Bitwuzla
+- Added debugging capabilities for `Pipe` by introducing `debugInteractiveWith`
+
+### Changed
+- Yices now uses flag `--incremental` by default
+- *(breaking change)* Removed functional dependency `m -> s` from `MonadIncrSMT s m`. This forces you to specify the underlying state when using `interactiveWith`. Therefore `interactiveWith cvc5Living $ do ...` now becomes `interactiveWith @Pipe cvc5Living $ do ...`.
+- *(breaking change)* Removed `newtype ProcessSolver` and replaced it with underlying `SMTLIB.Backends.Process.Config`. This may only affect you if you instantiated custom solvers.
+
 ## v2.0.1 _(2024-07-23)_
 
 ### Added
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,6 +1,6 @@
 [![Hackage](https://img.shields.io/hackage/v/hasmtlib.svg)](https://hackage.haskell.org/package/hasmtlib) ![Static Badge](https://img.shields.io/badge/Lang-GHC2021-blue) [![Haskell-CI](https://github.com/bruderj15/Hasmtlib/actions/workflows/haskell-ci.yml/badge.svg)](https://github.com/bruderj15/Hasmtlib/actions/workflows/haskell-ci.yml) [![License: GPL v3](https://img.shields.io/badge/License-GPLv3-blue.svg)](https://www.gnu.org/licenses/gpl-3.0)
 
-# Hasmtlib
+# Hasmtlib - Haskell SMTLib MTL Library
 
 Hasmtlib is a library for generating SMTLib2-problems using a monad.
 It takes care of encoding your problem, marshaling the data to an external solver and parsing and interpreting the result into Haskell types.
@@ -41,7 +41,7 @@
 
 main :: IO ()
 main = do
-  res <- solveWith (solver @SMT cvc5) $ do
+  res <- solveWith @SMT (solver cvc5) $ do
     setLogic "QF_NRA"
 
     u :: V3 (Expr RealSort) <- variable
@@ -71,7 +71,7 @@
   ```
 - [x] Pure API with Expression-instances for Num, Floating, Bounded, ...
   ```haskell
-    solveWith (solver @SMT yices) $ do
+    solveWith @SMT (solver yices) $ do
       setLogic "QF_BV"
       x <- var @(BvSort 16)
       y <- var
@@ -83,16 +83,16 @@
     -- | Function that turns a state (usually SMT or OMT) into a result and a solution
     type Solver s m = s -> m (Result, Solution)
   ```
-- [x] Solvers via external processes: CVC5, Z3, Yices2-SMT, MathSAT, OptiMathSAT & OpenSMT
+- [x] Solvers via external processes: CVC5, Z3, Yices2-SMT, MathSAT, OptiMathSAT, OpenSMT & Bitwuzla
   ```haskell
-    (result, solution) <- solveWith (solver @SMT mathsat) $ do
+    (result, solution) <- solveWith @SMT (solver mathsat) $ do
       setLogic "QF_LIA"
       assert $ ...
   ```
 - [x] Incremental solving
   ```haskell
       cvc5Living <- interactiveSolver cvc5
-      interactiveWith cvc5Living $ do
+      interactiveWith @Pipe cvc5Living $ do
         setLogic "QF_LIA"
         setOption $ Incremental True
         setOption $ ProduceModels True
@@ -108,7 +108,7 @@
   ```
 - [x] Pure quantifiers `for_all` and `exists`
   ```haskell
-    solveWith (solver @SMT z3) $ do
+    solveWith @SMT (solver z3) $ do
       setLogic "LIA"
       z <- var @IntSort
       assert $ z === 0
@@ -120,7 +120,7 @@
   ```
 - [x] Optimization Modulo Theories (OMT) / MaxSMT
   ```haskell
-    res <- solveWith (solver @OMT z3) $ do
+    res <- solveWith @OMT (solver z3) $ do
       setLogic "QF_LIA"
       x <- var @IntSort
 
diff --git a/hasmtlib.cabal b/hasmtlib.cabal
--- a/hasmtlib.cabal
+++ b/hasmtlib.cabal
@@ -1,7 +1,7 @@
 cabal-version:         3.0
 
 name:                  hasmtlib
-version:               2.0.1
+version:               2.1.0
 synopsis:              A monad for interfacing with external SMT solvers
 description:           Hasmtlib is a library for generating SMTLib2-problems using a monad.
   It takes care of encoding your problem, marshaling the data to an external solver and parsing and interpreting the result into Haskell types.
@@ -38,6 +38,7 @@
                      , Language.Hasmtlib.Internal.Bitvec
                      , Language.Hasmtlib.Internal.Render
                      , Language.Hasmtlib.Solver.Common
+                     , Language.Hasmtlib.Solver.Bitwuzla
                      , Language.Hasmtlib.Solver.CVC5
                      , Language.Hasmtlib.Solver.MathSAT
                      , Language.Hasmtlib.Solver.OpenSMT
diff --git a/src/Language/Hasmtlib.hs b/src/Language/Hasmtlib.hs
--- a/src/Language/Hasmtlib.hs
+++ b/src/Language/Hasmtlib.hs
@@ -19,6 +19,7 @@
   , module Language.Hasmtlib.Counting
   , module Language.Hasmtlib.Variable
   , module Language.Hasmtlib.Solver.Common
+  , module Language.Hasmtlib.Solver.Bitwuzla
   , module Language.Hasmtlib.Solver.CVC5
   , module Language.Hasmtlib.Solver.Z3
   , module Language.Hasmtlib.Solver.Yices
@@ -46,6 +47,7 @@
 import Language.Hasmtlib.Counting
 import Language.Hasmtlib.Variable
 import Language.Hasmtlib.Solver.Common
+import Language.Hasmtlib.Solver.Bitwuzla
 import Language.Hasmtlib.Solver.CVC5
 import Language.Hasmtlib.Solver.Z3
 import Language.Hasmtlib.Solver.Yices
diff --git a/src/Language/Hasmtlib/Counting.hs b/src/Language/Hasmtlib/Counting.hs
--- a/src/Language/Hasmtlib/Counting.hs
+++ b/src/Language/Hasmtlib/Counting.hs
@@ -9,25 +9,27 @@
 import Language.Hasmtlib.Iteable
 import Data.Proxy
 
+-- | Wrapper for 'count' which takes a 'Proxy'.
 count' :: forall t f. (Functor f, Foldable f, Num (Expr t)) => Proxy t -> f (Expr BoolSort) -> Expr t
 count' _ = sum . fmap (\b -> ite b 1 0)
 {-# INLINEABLE count' #-}
 
+-- | Out of many bool-expressions build a formula which encodes how many of them are 'true'.
 count :: forall t f. (Functor f, Foldable f, Num (Expr t)) => f (Expr BoolSort) -> Expr t
 count = count' (Proxy @t)
 {-# INLINE count #-}
 
--- | Out of many bool-expressions build a formula which encodes that __at most__ 'k' of them are 'true'
+-- | Out of many bool-expressions build a formula which encodes that __at most__ 'k' of them are 'true'.
 atMost  :: forall t f. (Functor f, Foldable f, Num (Expr t), Orderable (Expr t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort
 atMost  k = (<=? k) . count
 {-# INLINEABLE atMost #-}
 
--- | Out of many bool-expressions build a formula which encodes that __at least__ 'k' of them are 'true'
+-- | Out of many bool-expressions build a formula which encodes that __at least__ 'k' of them are 'true'.
 atLeast :: forall t f. (Functor f, Foldable f, Num (Expr t), Orderable (Expr t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort
 atLeast k = (>=? k) . count
 {-# INLINEABLE atLeast #-}
 
--- | Out of many bool-expressions build a formula which encodes that __exactly__ 'k' of them are 'true'
+-- | Out of many bool-expressions build a formula which encodes that __exactly__ 'k' of them are 'true'.
 exactly :: forall t f. (Functor f, Foldable f, Num (Expr t), Orderable (Expr t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort
 exactly k = (=== k) . count
 {-# INLINEABLE exactly #-}
diff --git a/src/Language/Hasmtlib/Solver/Bitwuzla.hs b/src/Language/Hasmtlib/Solver/Bitwuzla.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Hasmtlib/Solver/Bitwuzla.hs
@@ -0,0 +1,19 @@
+module Language.Hasmtlib.Solver.Bitwuzla where
+
+import SMTLIB.Backends.Process
+
+-- | A 'Config' for Bitwuzla.
+--   Requires binary @bitwuzla@ to be in path.
+--
+--   As of v0.5 Bitwuzla uses Cadical as SAT-Solver by default.
+--   Make sure it's default SAT-Solver binary - probably @cadical@ - is in path too.
+bitwuzla :: Config
+bitwuzla = defaultConfig { exe = "bitwuzla", args = [] }
+
+-- | A 'Config' for Bitwuzla which uses Kissat for SAT-Solving.
+--   Requires binary @bitwuzla@ and @kissat@ to be in path.
+--
+-- Combination with Kissat currently behaves weirdly: https://github.com/bitwuzla/bitwuzla/issues/119
+--
+-- bitwuzlaWithKissat :: Config
+-- bitwuzlaWithKissat = defaultConfig { exe = "bitwuzla", args = ["--sat-solver=kissat"] }
diff --git a/src/Language/Hasmtlib/Solver/CVC5.hs b/src/Language/Hasmtlib/Solver/CVC5.hs
--- a/src/Language/Hasmtlib/Solver/CVC5.hs
+++ b/src/Language/Hasmtlib/Solver/CVC5.hs
@@ -1,9 +1,8 @@
 module Language.Hasmtlib.Solver.CVC5 where
 
-import Language.Hasmtlib.Solver.Common
-import qualified SMTLIB.Backends.Process as P
+import SMTLIB.Backends.Process
 
--- | A 'ProcessSolver' for CVC5.
+-- | A 'Config' for CVC5.
 --   Requires binary @cvc5@ to be in path.
-cvc5 :: ProcessSolver
-cvc5 = ProcessSolver $ P.defaultConfig { P.exe = "cvc5", P.args = [] }
+cvc5 :: Config
+cvc5 = defaultConfig { exe = "cvc5", args = [] }
diff --git a/src/Language/Hasmtlib/Solver/Common.hs b/src/Language/Hasmtlib/Solver/Common.hs
--- a/src/Language/Hasmtlib/Solver/Common.hs
+++ b/src/Language/Hasmtlib/Solver/Common.hs
@@ -14,25 +14,23 @@
 import Control.Lens
 import Control.Monad
 import Control.Monad.IO.Class
-import qualified SMTLIB.Backends.Process as P
-import qualified SMTLIB.Backends as B
-
--- | A newtype-wrapper for 'P.Config' which configures a solver via external process.
-newtype ProcessSolver = ProcessSolver { conf :: P.Config }
+import qualified SMTLIB.Backends.Process as Process
+import qualified SMTLIB.Backends as Backend
 
--- | Creates a 'Solver' from a 'ProcessSolver'.
-solver :: (RenderSeq s, MonadIO m) => ProcessSolver -> Solver s m
-solver (ProcessSolver cfg) = processSolver cfg Nothing
+-- | Creates a 'Solver' from a 'Process.Config'.
+solver :: (RenderSeq s, MonadIO m) => Process.Config -> Solver s m
+solver cfg = processSolver cfg Nothing
 
--- | Creates a debugging 'Solver' from a 'ProcessSolver'.
-debug :: (RenderSeq s, Default (Debugger s), MonadIO m) => ProcessSolver -> Solver s m
-debug (ProcessSolver cfg) = processSolver cfg $ Just def
+-- | Creates a debugging 'Solver' from a 'Process.Config'.
+debug :: (RenderSeq s, MonadIO m) => Process.Config -> Debugger s -> Solver s m
+debug cfg = processSolver cfg . Just
 
--- | Creates an interactive session with a solver by creating and returning an alive process-handle 'P.Handle'.
-interactiveSolver :: MonadIO m => ProcessSolver -> m (B.Solver, P.Handle)
-interactiveSolver (ProcessSolver cfg) = liftIO $ do
-  handle  <- P.new cfg
-  liftM2 (,) (B.initSolver B.Queuing $ P.toBackend handle) (return handle)
+-- | Creates an interactive session with a solver by creating and returning an alive process-handle 'Process.Handle'.
+--   Queues commands by default, see 'Backend.Queuing'.
+interactiveSolver :: MonadIO m => Process.Config -> m (Backend.Solver, Process.Handle)
+interactiveSolver cfg = liftIO $ do
+  handle  <- Process.new cfg
+  liftM2 (,) (Backend.initSolver Backend.Queuing $ Process.toBackend handle) (return handle)
 
 -- | A type holding actions for debugging states.
 data Debugger s = Debugger
@@ -77,20 +75,20 @@
 --
 -- 5. close the process and clean up all resources.
 --
-processSolver :: (RenderSeq s, MonadIO m) => P.Config -> Maybe (Debugger s) -> Solver s m
+processSolver :: (RenderSeq s, MonadIO m) => Process.Config -> Maybe (Debugger s) -> Solver s m
 processSolver cfg debugger s = do
-  liftIO $ P.with cfg $ \handle -> do
+  liftIO $ Process.with cfg $ \handle -> do
     maybe mempty (`debugState` s) debugger
-    pSolver <- B.initSolver B.Queuing $ P.toBackend handle
+    pSolver <- Backend.initSolver Backend.Queuing $ Process.toBackend handle
 
     let problem = renderSeq s
     maybe mempty (`debugProblem` problem) debugger
 
-    forM_ problem (B.command_ pSolver)
-    resultResponse <- B.command pSolver "(check-sat)"
+    forM_ problem (Backend.command_ pSolver)
+    resultResponse <- Backend.command pSolver "(check-sat)"
     maybe mempty (`debugResultResponse` resultResponse) debugger
 
-    modelResponse  <- B.command pSolver "(get-model)"
+    modelResponse  <- Backend.command pSolver "(get-model)"
     maybe mempty (`debugModelResponse` modelResponse) debugger
 
     case parseOnly resultParser (toStrict resultResponse) of
diff --git a/src/Language/Hasmtlib/Solver/MathSAT.hs b/src/Language/Hasmtlib/Solver/MathSAT.hs
--- a/src/Language/Hasmtlib/Solver/MathSAT.hs
+++ b/src/Language/Hasmtlib/Solver/MathSAT.hs
@@ -1,14 +1,13 @@
 module Language.Hasmtlib.Solver.MathSAT where
 
-import Language.Hasmtlib.Solver.Common
-import qualified SMTLIB.Backends.Process as P
+import SMTLIB.Backends.Process
 
--- | A 'ProcessSolver' for MathSAT.
+-- | A 'Config' for MathSAT.
 --   Requires binary @mathsat@ to be in path.
-mathsat :: ProcessSolver
-mathsat = ProcessSolver $ P.defaultConfig { P.exe = "mathsat", P.args = [] }
+mathsat :: Config
+mathsat = defaultConfig { exe = "mathsat", args = [] }
 
--- | A 'ProcessSolver' for OptiMathSAT.
+-- | A 'Config' for OptiMathSAT.
 --   Requires binary @optimathsat@ to be in path.
-optimathsat :: ProcessSolver
-optimathsat = ProcessSolver $ P.defaultConfig { P.exe = "optimathsat", P.args = ["-optimization=true"] }
+optimathsat :: Config
+optimathsat = defaultConfig { exe = "optimathsat", args = ["-optimization=true"] }
diff --git a/src/Language/Hasmtlib/Solver/OpenSMT.hs b/src/Language/Hasmtlib/Solver/OpenSMT.hs
--- a/src/Language/Hasmtlib/Solver/OpenSMT.hs
+++ b/src/Language/Hasmtlib/Solver/OpenSMT.hs
@@ -1,9 +1,8 @@
 module Language.Hasmtlib.Solver.OpenSMT where
 
-import Language.Hasmtlib.Solver.Common
-import qualified SMTLIB.Backends.Process as P
+import SMTLIB.Backends.Process
 
--- | A 'ProcessSolver' for OpenSMT.
+-- | A 'Config' for OpenSMT.
 --   Requires binary @opensmt@ to be in path.
-opensmt :: ProcessSolver
-opensmt = ProcessSolver $ P.defaultConfig { P.exe = "opensmt", P.args = [] }
+opensmt :: Config
+opensmt = defaultConfig { exe = "opensmt", args = [] }
diff --git a/src/Language/Hasmtlib/Solver/Yices.hs b/src/Language/Hasmtlib/Solver/Yices.hs
--- a/src/Language/Hasmtlib/Solver/Yices.hs
+++ b/src/Language/Hasmtlib/Solver/Yices.hs
@@ -1,9 +1,8 @@
 module Language.Hasmtlib.Solver.Yices where
 
-import Language.Hasmtlib.Solver.Common
-import qualified SMTLIB.Backends.Process as P
+import SMTLIB.Backends.Process
 
--- | A 'ProcessSolver' for Yices.
+-- | A 'Config' for Yices.
 --   Requires binary @yices-smt2@ to be in path.
-yices :: ProcessSolver
-yices = ProcessSolver $ P.defaultConfig { P.exe = "yices-smt2", P.args = ["--smt2-model-format"] }
+yices :: Config
+yices = defaultConfig { exe = "yices-smt2", args = ["--smt2-model-format", "--incremental"] }
diff --git a/src/Language/Hasmtlib/Solver/Z3.hs b/src/Language/Hasmtlib/Solver/Z3.hs
--- a/src/Language/Hasmtlib/Solver/Z3.hs
+++ b/src/Language/Hasmtlib/Solver/Z3.hs
@@ -1,9 +1,8 @@
 module Language.Hasmtlib.Solver.Z3 where
 
-import Language.Hasmtlib.Solver.Common
-import qualified SMTLIB.Backends.Process as P
+import SMTLIB.Backends.Process
 
--- | A 'ProcessSolver' for Z3.
+-- | A 'Config' for Z3.
 --   Requires binary @z3@ to be in path.
-z3 :: ProcessSolver
-z3 = ProcessSolver P.defaultConfig
+z3 :: Config
+z3 = defaultConfig
diff --git a/src/Language/Hasmtlib/Type/ArrayMap.hs b/src/Language/Hasmtlib/Type/ArrayMap.hs
--- a/src/Language/Hasmtlib/Type/ArrayMap.hs
+++ b/src/Language/Hasmtlib/Type/ArrayMap.hs
@@ -4,22 +4,22 @@
 module Language.Hasmtlib.Type.ArrayMap where
 
 import Data.Proxy
-import qualified Data.Map as Map  
+import qualified Data.Map as Map
 import Control.Lens
 
--- | Class that allows access to a map-like array where specific values are is the default value or overwritten values.
+-- | Class that allows access to a map-like array where any value is either the default value or an overwritten values.
 --   Every index has a value by default.
 --   Values at indices can be overwritten manually.
--- 
+--
 --   Based on McCarthy`s basic array theory.
--- 
+--
 --   Therefore the following axioms must hold:
--- 
+--
 -- 1. forall A i x: arrSelect (store A i x) == x
--- 
+--
 -- 2. forall A i j x: i /= j ==> (arrSelect (arrStore A i x) j === arrSelect A j)
 class ArrayMap f k v where
-  asConst'   :: Proxy f -> Proxy k -> v -> f k v 
+  asConst'   :: Proxy f -> Proxy k -> v -> f k v
   viewConst  :: f k v -> v
   arrSelect  :: f k v -> k -> v
   arrStore   :: f k v -> k -> v -> f k v
@@ -28,8 +28,8 @@
 asConst :: forall f k v. ArrayMap f k v => v -> f k v
 asConst = asConst' (Proxy @f) (Proxy @k)
 
--- | A map-like array with a default constant value and partially overwritten values.  
-data ConstArray k v = ConstArray 
+-- | A map-like array with a default constant value and partially overwritten values.
+data ConstArray k v = ConstArray
   { _arrConst :: v
   , _stored :: Map.Map k v
   } deriving (Show, Eq, Ord, Functor, Foldable, Traversable)
diff --git a/src/Language/Hasmtlib/Type/MonadSMT.hs b/src/Language/Hasmtlib/Type/MonadSMT.hs
--- a/src/Language/Hasmtlib/Type/MonadSMT.hs
+++ b/src/Language/Hasmtlib/Type/MonadSMT.hs
@@ -1,5 +1,3 @@
-{-# LANGUAGE FunctionalDependencies #-}
-
 module Language.Hasmtlib.Type.MonadSMT where
 
 import Language.Hasmtlib.Internal.Expr
@@ -111,7 +109,7 @@
 quantify expr = return expr
 
 -- | A 'MonadSMT' that allows incremental solving.
-class MonadSMT s m => MonadIncrSMT s m | m -> s where
+class MonadSMT s m => MonadIncrSMT s m where
   -- | Push a new context (one) to the solvers context-stack.
   push :: m ()
 
diff --git a/src/Language/Hasmtlib/Type/OMT.hs b/src/Language/Hasmtlib/Type/OMT.hs
--- a/src/Language/Hasmtlib/Type/OMT.hs
+++ b/src/Language/Hasmtlib/Type/OMT.hs
@@ -34,7 +34,7 @@
 
 -- | The state of the OMT-problem.
 data OMT = OMT
-  { _smt            :: SMT                                  -- ^ The underlying 'SMT'-Problem
+  { _smt            :: !SMT                                 -- ^ The underlying 'SMT'-Problem
   , _targetMinimize :: !(Seq (SomeKnownSMTSort Minimize))   -- ^ All expressions to minimize
   , _targetMaximize :: !(Seq (SomeKnownSMTSort Maximize))   -- ^ All expressions to maximize
   , _softFormulas   :: !(Seq SoftFormula)                   -- ^ All soft assertions of boolean expressions
diff --git a/src/Language/Hasmtlib/Type/Pipe.hs b/src/Language/Hasmtlib/Type/Pipe.hs
--- a/src/Language/Hasmtlib/Type/Pipe.hs
+++ b/src/Language/Hasmtlib/Type/Pipe.hs
@@ -17,10 +17,12 @@
 import Data.IntMap as IMap (singleton)
 import Data.Dependent.Map as DMap
 import Data.Coerce
+import qualified Data.ByteString.Lazy.Char8 as ByteString.Char8
 import Data.ByteString.Builder
 import Data.ByteString.Lazy hiding (filter, singleton, isPrefixOf)
 import Data.Attoparsec.ByteString hiding (Result)
 import Control.Monad.State
+import Control.Monad
 import Control.Lens hiding (List)
 
 -- | A pipe to the solver.
@@ -31,6 +33,7 @@
   { _lastPipeVarId :: {-# UNPACK #-} !Int              -- ^ Last Id assigned to a new var
   , _mPipeLogic    :: Maybe String                     -- ^ Logic for the SMT-Solver
   , _pipe          :: !B.Solver                        -- ^ Active pipe to the backend
+  , _isDebugging   :: Bool                             -- ^ Flag if pipe shall debug
   }
 
 $(makeLenses ''Pipe)
@@ -42,7 +45,9 @@
   var' p = do
     smt <- get
     newVar <- smtvar' p
-    liftIO $ B.command_ (smt^.pipe) $ renderDeclareVar newVar
+    let cmd = renderDeclareVar newVar
+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd
+    liftIO $ B.command_ (smt^.pipe) cmd
     return $ Var newVar
   {-# INLINEABLE var' #-}
 
@@ -51,32 +56,45 @@
     qExpr <- case smt^.mPipeLogic of
       Nothing    -> return expr
       Just logic -> if "QF" `isPrefixOf` logic then return expr else quantify expr
-    liftIO $ B.command_ (smt^.pipe) $ renderAssert qExpr
+    let cmd = renderAssert qExpr
+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd
+    liftIO $ B.command_ (smt^.pipe) cmd
   {-# INLINEABLE assert #-}
 
   setOption opt = do
     smt <- get
-    liftIO $ B.command_ (smt^.pipe) $ render opt
+    let cmd = render opt
+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd
+    liftIO $ B.command_ (smt^.pipe) cmd
 
   setLogic l = do
     mPipeLogic ?= l
     smt <- get
-    liftIO $ B.command_ (smt^.pipe) $ renderSetLogic (stringUtf8 l)
+    let cmd = renderSetLogic (stringUtf8 l)
+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd
+    liftIO $ B.command_ (smt^.pipe) cmd
 
 instance (MonadState Pipe m, MonadIO m) => MonadIncrSMT Pipe m where
   push = do
     smt <- get
-    liftIO $ B.command_ (smt^.pipe) "(push 1)"
+    let cmd = "(push 1)"
+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd
+    liftIO $ B.command_ (smt^.pipe) cmd
   {-# INLINE push #-}
 
   pop = do
     smt <- get
-    liftIO $ B.command_ (smt^.pipe) "(pop 1)"
+    let cmd = "(pop 1)"
+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd
+    liftIO $ B.command_ (smt^.pipe) cmd
   {-# INLINE pop #-}
 
   checkSat = do
     smt <- get
-    result <- liftIO $ B.command (smt^.pipe) "(check-sat)"
+    let cmd = "(check-sat)"
+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd
+    result <- liftIO $ B.command (smt^.pipe) cmd
+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn result
     case parseOnly resultParser (toStrict result) of
       Left e    -> liftIO $ do
         print result
@@ -85,7 +103,10 @@
 
   getModel = do
     smt   <- get
-    model <- liftIO $ B.command (smt^.pipe) "(get-model)"
+    let cmd = "(get-model)"
+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd
+    model <- liftIO $ B.command (smt^.pipe) cmd
+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn model
     case parseOnly anyModelParser (toStrict model) of
       Left e    -> liftIO $ do
         print model
@@ -95,7 +116,10 @@
   getValue :: forall t. KnownSMTSort t => Expr t -> m (Maybe (Decoded (Expr t)))
   getValue v@(Var x) = do
     smt   <- get
-    model <- liftIO $ B.command (smt^.pipe) $ renderUnary "get-value" $ "(" <> render x <> ")"
+    let cmd = renderUnary "get-value" $ "(" <> render x <> ")"
+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd
+    model <- liftIO $ B.command (smt^.pipe) cmd
+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn model
     case parseOnly (getValueParser @t x) (toStrict model) of
       Left e    -> liftIO $ do
         print model
@@ -115,14 +139,21 @@
 instance (MonadSMT Pipe m, MonadIO m) => MonadOMT Pipe m where
   minimize expr = do
     smt <- get
-    liftIO $ B.command_ (smt^.pipe) $ render $ Minimize expr
+    let cmd = render $ Minimize expr
+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd
+    liftIO $ B.command_ (smt^.pipe) cmd
   {-# INLINEABLE minimize #-}
 
   maximize expr = do
     smt <- get
-    liftIO $ B.command_ (smt^.pipe) $ render $ Maximize expr
+    let cmd = render $ Maximize expr
+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd
+    liftIO $ B.command_ (smt^.pipe) cmd
   {-# INLINEABLE maximize #-}
 
   assertSoft expr w gid = do
     smt <- get
-    liftIO $ B.command_ (smt^.pipe) $ render $ SoftFormula expr w gid
+    let cmd = render $ SoftFormula expr w gid
+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd
+    liftIO $ B.command_ (smt^.pipe) cmd
+  {-# INLINEABLE assertSoft #-}
diff --git a/src/Language/Hasmtlib/Type/Solver.hs b/src/Language/Hasmtlib/Type/Solver.hs
--- a/src/Language/Hasmtlib/Type/Solver.hs
+++ b/src/Language/Hasmtlib/Type/Solver.hs
@@ -1,6 +1,7 @@
 module Language.Hasmtlib.Type.Solver
   ( WithSolver(..)
-  , solveWith, interactiveWith
+  , solveWith
+  , interactiveWith, debugInteractiveWith
   , solveMinimized, solveMinimizedDebug
   , solveMaximized, solveMaximizedDebug
   )
@@ -13,14 +14,15 @@
 import Language.Hasmtlib.Type.Pipe
 import Language.Hasmtlib.Orderable
 import Language.Hasmtlib.Codec
-import qualified SMTLIB.Backends as B
-import qualified SMTLIB.Backends.Process as P
+import qualified SMTLIB.Backends as Backend
+import qualified SMTLIB.Backends.Process as Process
 import Data.Default
 import Control.Monad.State
 
--- | Data that can have a 'B.Solver'.
+-- | Data that can have a 'Backend.Solver' which may be debugged.
 class WithSolver a where
-  withSolver :: B.Solver -> a
+  -- | Create a datum with a 'Backend.Solver' and a 'Bool for whether to debug the 'Backend.Solver'.
+  withSolver :: Backend.Solver -> Bool -> a
 
 instance WithSolver Pipe where
   withSolver = Pipe 0 Nothing
@@ -43,7 +45,7 @@
 --
 -- main :: IO ()
 -- main = do
---   res <- solveWith (solver cvc5) $ do
+--   res <- solveWith @SMT (solver cvc5) $ do
 --     setLogic \"QF_LIA\"
 --
 --     x <- var @IntSort
@@ -54,7 +56,7 @@
 --
 --   print res
 -- @
-solveWith :: (Monad m, Default s, Codec a) => Solver s m -> StateT s m a -> m (Result, Maybe (Decoded a))
+solveWith :: (Default s, Monad m, Codec a) => Solver s m -> StateT s m a -> m (Result, Maybe (Decoded a))
 solveWith solver m = do
   (a, problem) <- runStateT m def
   (result, solution) <- solver problem
@@ -72,7 +74,7 @@
 -- main :: IO ()
 -- main = do
 --   cvc5Living <- interactiveSolver cvc5
---   interactiveWith cvc5Living $ do
+--   interactiveWith @Pipe cvc5Living $ do
 --     setOption $ Incremental True
 --     setOption $ ProduceModels True
 --     setLogic \"QF_LIA\"
@@ -100,10 +102,16 @@
 --
 --   return ()
 -- @
-interactiveWith :: (MonadIO m, WithSolver s) => (B.Solver, P.Handle) -> StateT s m () -> m ()
+interactiveWith :: (WithSolver s, MonadIO m) => (Backend.Solver, Process.Handle) -> StateT s m () -> m ()
 interactiveWith (solver, handle) m = do
-   _ <- runStateT m $ withSolver solver
-   liftIO $ P.close handle
+  _ <- runStateT m $ withSolver solver False
+  liftIO $ Process.close handle
+
+-- | Like 'interactiveWith' but it prints all communication with the solver to console.
+debugInteractiveWith :: (WithSolver s, MonadIO m) => (Backend.Solver, Process.Handle) -> StateT s m () -> m ()
+debugInteractiveWith (solver, handle) m = do
+  _ <- runStateT m $ withSolver solver True
+  liftIO $ Process.close handle
 
 -- | Solves the current problem with respect to a minimal solution for a given numerical expression.
 --