diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -6,6 +6,29 @@
 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.7.0 _(2024-09-12)_
+
+### Added
+- Added helpful instances for standard types for `Codec` to ease deriving.
+- Added decorator `timingout` in `Language.Hasmtlib.Type.Solver` to set a time-out for solvers.
+Unfortunately as of SMTLib standard v2.6 there is no SMT-Option for this. Although some solvers like `Z3` (unreliably) support it,
+we instead do it by internally coordinating the kill of the solver process from Haskell using `System.Timeout.Lifted#timeout`. Works like a charme.
+- Added `Language.Hasmtlib.Type.Debugger` for debugging problem construction and solver interaction.
+
+### Changed
+- *(breaking change)* Completely revised the way solver process-configurations are handled and debugged.
+Solvers which previously had the type `Process.Config` from `smtlib-backends` now have the type `SolverConfig` from `Language.Hasmtlib.Type.Solver`.
+This bundles information on the executable of the solver with additional information such as debugging and time-outs.
+Actual solver creation still is done by funtion `solver`. Therefore this change is only breaking, if you created custom solvers or debugged solvers.
+- Debugging solvers changed from `solveWith (debug z3 def) $ ...` to `solveWith (solver $ debugging z3 def) $ ...`.
+Also note that there are plenty debugging configurations besides `def` existing in `Language.Hasmtlib.Type.Debugger` now.
+- Interactive solving before was a two-stepper like `iZ3 <- interactiveSolver z3 ; interactiveWith iZ3 $ ...`.
+Leveraging `SolverConfig` this has been changed to a more uniform way with `interactiveWith z3 $ do ...`.
+Also note that `debugInteractiveWith z3 $ ...` now is replaced by `interactiveWith (debugging def z3) $ ...`.
+
+### Removed
+- Removed `Language.Hasmtlib.Solver.Common`. Contents are now in `Language.Hasmtlib.Type.Solver`.
+
 ## v2.6.3 _(2024-09-07)_
 
 ### Added
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.6.3
+version:               2.7.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.
@@ -37,7 +37,6 @@
                      , Language.Hasmtlib.Internal.Sharing
                      , Language.Hasmtlib.Internal.Uniplate1
                      , Language.Hasmtlib.Internal.Constraint
-                     , Language.Hasmtlib.Solver.Common
                      , Language.Hasmtlib.Solver.Bitwuzla
                      , Language.Hasmtlib.Solver.CVC5
                      , Language.Hasmtlib.Solver.MathSAT
@@ -57,10 +56,13 @@
                      , Language.Hasmtlib.Type.ArrayMap
                      , Language.Hasmtlib.Type.Bitvec
                      , Language.Hasmtlib.Type.Relation
+                     , Language.Hasmtlib.Type.Debugger
 
   build-depends:       array                        >= 0.5    && < 1
                      , attoparsec                   >= 0.14.4 && < 1
                      , base                         >= 4.17.2 && < 5
+                     , lifted-base                  >= 0.2 && < 0.5
+                     , monad-control                >= 1.0 && < 1.2
                      , bytestring                   >= 0.11.5 && < 1
                      , containers                   >= 0.6.7  && < 1
                      , unordered-containers         >= 0.2.20 && < 0.3
diff --git a/src/Language/Hasmtlib.hs b/src/Language/Hasmtlib.hs
--- a/src/Language/Hasmtlib.hs
+++ b/src/Language/Hasmtlib.hs
@@ -32,7 +32,7 @@
   -- ** Type
   , module Language.Hasmtlib.Type.Solution
   , module Language.Hasmtlib.Type.Solver
-  , module Language.Hasmtlib.Solver.Common
+  , module Language.Hasmtlib.Type.Debugger
 
   -- ** Concrete solvers
   , module Language.Hasmtlib.Solver.Z3
@@ -61,11 +61,11 @@
 import Language.Hasmtlib.Type.ArrayMap
 import Language.Hasmtlib.Type.Bitvec
 import Language.Hasmtlib.Type.Relation
+import Language.Hasmtlib.Type.Debugger
 import Language.Hasmtlib.Boolean
 import Language.Hasmtlib.Codec
 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
@@ -73,3 +73,4 @@
 import Language.Hasmtlib.Solver.OpenSMT
 import Language.Hasmtlib.Solver.MathSAT
 import Language.Hasmtlib.Internal.Sharing
+import Language.Hasmtlib.Internal.Render ()
diff --git a/src/Language/Hasmtlib/Codec.hs b/src/Language/Hasmtlib/Codec.hs
--- a/src/Language/Hasmtlib/Codec.hs
+++ b/src/Language/Hasmtlib/Codec.hs
@@ -48,6 +48,8 @@
 import Data.Dependent.Map as DMap
 import Data.Tree (Tree)
 import Data.Array (Array, Ix)
+import Data.Word
+import Data.Int
 import qualified Data.Text as Text
 import Data.Monoid (Sum, Product, First, Last, Dual)
 import qualified Data.Vector.Sized as V
@@ -223,6 +225,91 @@
   type Decoded (Array i e) = Array i (Decoded e)
   decode = traverse . decode
   encode = fmap encode
+
+instance Codec Int where
+  type Decoded Int = Int
+  decode _ = Just
+  encode = id
+
+instance Codec Integer where
+  type Decoded Integer = Integer
+  decode _ = Just
+  encode = id
+
+instance Codec Natural where
+  type Decoded Natural = Natural
+  decode _ = Just
+  encode = id
+
+instance Codec Word where
+  type Decoded Word = Word
+  decode _ = Just
+  encode = id
+
+instance Codec Word8 where
+  type Decoded Word8 = Word8
+  decode _ = Just
+  encode = id
+
+instance Codec Word16 where
+  type Decoded Word16 = Word16
+  decode _ = Just
+  encode = id
+
+instance Codec Word32 where
+  type Decoded Word32 = Word32
+  decode _ = Just
+  encode = id
+
+instance Codec Word64 where
+  type Decoded Word64 = Word64
+  decode _ = Just
+  encode = id
+
+instance Codec Int8 where
+  type Decoded Int8 = Int8
+  decode _ = Just
+  encode = id
+
+instance Codec Int16 where
+  type Decoded Int16 = Int16
+  decode _ = Just
+  encode = id
+
+instance Codec Int32 where
+  type Decoded Int32 = Int32
+  decode _ = Just
+  encode = id
+
+instance Codec Int64 where
+  type Decoded Int64 = Int64
+  decode _ = Just
+  encode = id
+
+instance Codec Char where
+  type Decoded Char = Char
+  decode _ = Just
+  encode = id
+
+instance Codec Float where
+  type Decoded Float = Float
+  decode _ = Just
+  encode = id
+
+instance Codec Double where
+  type Decoded Double = Double
+  decode _ = Just
+  encode = id
+
+instance Codec Ordering where
+  type Decoded Ordering = Ordering
+  decode _ = Just
+  encode = id
+
+instance Codec Bool where
+  type Decoded Bool = Bool
+  decode _ = Just
+  encode = id
 
 class GCodec f where
   type GDecoded f :: Type -> Type
diff --git a/src/Language/Hasmtlib/Internal/Render.hs b/src/Language/Hasmtlib/Internal/Render.hs
--- a/src/Language/Hasmtlib/Internal/Render.hs
+++ b/src/Language/Hasmtlib/Internal/Render.hs
@@ -1,35 +1,68 @@
+{-# LANGUAGE LambdaCase #-}
+
 module Language.Hasmtlib.Internal.Render where
 
-import Data.ByteString.Builder
-import Data.Foldable (foldl')
+import Language.Hasmtlib.Type.OMT
+import Language.Hasmtlib.Type.SMT
+import Language.Hasmtlib.Type.Expr
+import Language.Hasmtlib.Type.Value
+import Language.Hasmtlib.Type.Option
+import Language.Hasmtlib.Type.SMTSort
+import Language.Hasmtlib.Type.Bitvec
+import Language.Hasmtlib.Type.ArrayMap
+import Data.Coerce
 import Data.Sequence
+import Data.Foldable (foldl')
+import Data.Map (size, minViewWithKey)
+import Data.ByteString.Builder
+import Data.ByteString.Lazy.UTF8 (toString)
 import qualified Data.Text as Text
 import qualified Data.Text.Encoding as Text.Enc
+import qualified Data.Vector.Sized as V
+import Control.Lens hiding (op)
 import GHC.TypeNats
 
+render1 :: Render a => Builder -> a -> Builder
+render1 op x = "(" <> op <> " " <> render x <> ")"
+{-# INLINE render1 #-}
+
+render2 :: (Render a, Render b) => Builder -> a -> b -> Builder
+render2 op x y = "(" <> op <> " " <> render x <> " " <> render y <> ")"
+{-# INLINE render2 #-}
+
+render3 :: (Render a, Render b, Render c) => Builder -> a -> b -> c -> Builder
+render3 op x y z = "(" <> op <> " " <> render x <> " " <> render y <> " " <> render z <> ")"
+{-# INLINE render3 #-}
+
+renderN :: Render a => Builder -> [a] -> Builder
+renderN op xs = "(" <> op <> renderedXs <> ")"
+  where
+    renderedXs = foldl' (\s x -> s <> " " <> render x) mempty xs
+{-# INLINE renderN #-}
+
 -- | Render values to their SMTLib2-Lisp form, represented as 'Builder'.
 class Render a where
   render :: a -> Builder
 
 instance Render Bool where
   render b = if b then "true" else "false"
-  {-# INLINEABLE render #-}
+  {-# INLINE render #-}
 
 instance Render Nat where
   render = integerDec . fromIntegral
-  {-# INLINEABLE render #-}
+  {-# INLINE render #-}
 
 instance Render Integer where
   render x
     | x < 0     = "(- " <> integerDec (abs x) <> ")"
     | otherwise = integerDec x
-  {-# INLINEABLE render #-}
+  {-# INLINE render #-}
 
 instance Render Double where
   render x
     | x < 0     = "(- " <> formatDouble standardDefaultPrecision (abs x) <> ")"
     | otherwise = formatDouble standardDefaultPrecision x
-  {-# INLINEABLE render #-}
+  {-# INLINE render #-}
 
 instance Render Char where
   render = char8
@@ -47,24 +80,229 @@
   render = Text.Enc.encodeUtf8Builder
   {-# INLINE render #-}
 
-renderUnary :: Render a => Builder -> a -> Builder
-renderUnary op x = "(" <> op <> " " <> render x <> ")"
-{-# INLINEABLE renderUnary #-}
+instance Render (Bitvec enc n) where
+  render = stringUtf8 . show
+  {-# INLINE render #-}
 
-renderBinary :: (Render a, Render b) => Builder -> a -> b -> Builder
-renderBinary op x y = "(" <> op <> " " <> render x <> " " <> render y <> ")"
-{-# INLINEABLE renderBinary #-}
+instance Render (SMTVar t) where
+  render v = "var_" <> intDec (coerce @(SMTVar t) @Int v)
+  {-# INLINE render #-}
 
-renderTernary :: (Render a, Render b, Render c) => Builder -> a -> b -> c -> Builder
-renderTernary op x y z = "(" <> op <> " " <> render x <> " " <> render y <> " " <> render z <> ")"
-{-# INLINEABLE renderTernary #-}
+instance Show (Value t) where
+  show = toString . toLazyByteString . render
 
-renderNary :: Render a => Builder -> [a] -> Builder
-renderNary op xs = "(" <> op <> renderedXs <> ")"
+instance Render (Value t) where
+  render (IntValue x)   = render x
+  render (RealValue x)  = render x
+  render (BoolValue x)  = render x
+  render (BvValue   v)  = "#b" <> render v
+  render (ArrayValue arr) = case minViewWithKey (arr^.stored) of
+    Nothing -> constRender $ arr^.arrConst
+    Just ((k,v), stored')
+      | size (arr^.stored) > 1 -> render $ ArrStore (Constant (wrapValue (arr & stored .~ stored'))) (Constant (wrapValue k)) (Constant (wrapValue v))
+      | otherwise  -> constRender v
+    where
+      constRender v = "((as const " <> render (goSing arr) <> ") " <> render (wrapValue v) <> ")"
+      goSing :: forall k v. (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => ConstArray (HaskellType k) (HaskellType v) -> SSMTSort (ArraySort k v)
+      goSing _ = sortSing @(ArraySort k v)
+  render (StringValue x) = "\"" <> render x <> "\""
+
+instance KnownSMTSort t => Show (Expr t) where
+  show = toString . toLazyByteString . render
+
+instance KnownSMTSort t => Render (Expr t) where
+  render (Var v)      = render v
+  render (Constant c) = render c
+  render (Plus x y)   = render2 (case sortSing' x of SBvSort _ _ -> "bvadd" ; _ -> "+") x y
+  render (Minus x y)  = render2 (case sortSing' x of SBvSort _ _ -> "bvsub" ; _ -> "-") x y
+  render (Neg x)      = render1  (case sortSing' x of SBvSort _ _ -> "bvneg" ; _ -> "-") x
+  render (Mul x y)    = render2 (case sortSing' x of SBvSort _ _ -> "bvmul" ; _ -> "*") x y
+  render (Abs x)      = render1  "abs" x
+  render (Mod x y)    = render2 opStr x y
+    where
+      opStr = case sortSing' x of
+        SBvSort enc _ -> case bvEncSing' enc of
+          SUnsigned -> "bvurem"
+          SSigned -> "bvsmod"
+        _ -> "mod"
+  render (Rem x y)    = render2 opStr x y
+    where
+      opStr = case sortSing' x of
+        SBvSort enc _ -> case bvEncSing' enc of
+          SUnsigned -> "bvurem"
+          SSigned -> "bvsrem"
+        _ -> "rem"
+  render (IDiv x y)   = render2 opStr x y
+    where
+      opStr = case sortSing' x of
+        SBvSort enc _ -> case bvEncSing' enc of
+          SUnsigned -> "bvudiv"
+          SSigned -> "bvsdiv"
+        _ -> "div"
+  render (Div x y)    = render2 "/" x y
+  render (LTH x y)    = render2 opStr x y
+    where
+      opStr = case sortSing' x of
+        SBvSort enc _ -> case bvEncSing' enc of
+          SUnsigned -> "bvult"
+          SSigned -> "bvslt"
+        SStringSort -> "str.<"
+        _ -> "<"
+  render (LTHE x y)   = render2 opStr x y
+    where
+      opStr = case sortSing' x of
+        SBvSort enc _ -> case bvEncSing' enc of
+          SUnsigned -> "bvule"
+          SSigned -> "bvsle"
+        SStringSort -> "str.<="
+        _ -> "<="
+  render (EQU xs)     = renderN "=" $ V.toList xs
+  render (Distinct xs)= renderN "distinct" $ V.toList xs
+  render (GTHE x y)   = case sortSing' x of
+    SBvSort enc _ -> case bvEncSing' enc of
+      SUnsigned -> render2 "bvuge" x y
+      SSigned   -> render2 "bvsge" x y
+    SStringSort -> render2 "str.<=" y x
+    _           -> render2 ">=" x y
+  render (GTH x y)    = case sortSing' x of
+    SBvSort enc _ -> case bvEncSing' enc of
+      SUnsigned -> render2 "bvugt" x y
+      SSigned   -> render2 "bvsgt" x y
+    SStringSort -> render2 "str.<" y x
+    _           -> render2 ">" x y
+  render (Not x)      = render1  (case sortSing' x of SBvSort _ _ -> "bvnot" ; _ -> "not") x
+  render (And x y)    = render2 (case sortSing' x of SBvSort _ _ -> "bvand" ; _ -> "and") x y
+  render (Or x y)     = render2 (case sortSing' x of SBvSort _ _ -> "bvor" ; _ -> "or") x y
+  render (Impl x y)   = render2 "=>" x y
+  render (Xor x y)    = render2 (case sortSing' x of SBvSort _ _ -> "bvxor" ; _ -> "xor") x y
+  render Pi           = "real.pi"
+  render (Sqrt x)     = render1 "sqrt" x
+  render (Exp x)      = render1 "exp" x
+  render (Sin x)      = render1 "sin" x
+  render (Cos x)      = render1 "cos" x
+  render (Tan x)      = render1 "tan" x
+  render (Asin x)     = render1 "arcsin" x
+  render (Acos x)     = render1 "arccos" x
+  render (Atan x)     = render1 "arctan" x
+  render (ToReal x)   = render1 "to_real" x
+  render (ToInt x)    = render1 "to_int" x
+  render (IsInt x)    = render1 "is_int" x
+  render (Ite p t f)  = render3 "ite" p t f
+  render (BvNand x y)       = render2 "bvnand" (render x) (render y)
+  render (BvNor x y)        = render2 "bvnor"  (render x) (render y)
+  render (BvShL x y)        = render2 "bvshl"  (render x) (render y)
+  render (BvLShR x y)       = render2 "bvlshr" (render x) (render y)
+  render (BvAShR x y)       = render2 "bvashr" (render x) (render y)
+  render (BvConcat x y)     = render2 "concat" (render x) (render y)
+  render (BvRotL i x)       = render1 (render2 "_" ("rotate_left"  :: Builder) (render $ toInteger i)) (render x)
+  render (BvRotR i x)       = render1 (render2 "_" ("rotate_right" :: Builder) (render $ toInteger i)) (render x)
+  render (ArrSelect a i)    = render2  "select" (render a) (render i)
+  render (ArrStore a i v)   = render3 "store"  (render a) (render i) (render v)
+  render (StrConcat x y)        = render2 "str.++"  (render x) (render y)
+  render (StrLength x)          = render1  "str.len" (render x)
+  render (StrAt x i)            = render2 "str.at"  (render x) (render i)
+  render (StrSubstring x i j)   = render3 "str.substr"  (render x) (render i) (render j)
+  render (StrPrefixOf x y)      = render2 "str.prefixof" (render x) (render y)
+  render (StrSuffixOf x y)      = render2 "str.suffixof" (render x) (render y)
+  render (StrContains x y)      = render2 "str.contains" (render x) (render y)
+  render (StrIndexOf x y i)     = render3 "str.indexof"     (render x) (render y) (render i)
+  render (StrReplace x y y')    = render3 "str.replace"     (render x) (render y) (render y')
+  render (StrReplaceAll x y y') = render3 "str.replace_all" (render x) (render y) (render y')
+  render (ForAll mQvar f) = renderQuantifier "forall" mQvar f
+  render (Exists mQvar f) = renderQuantifier "exists" mQvar f
+
+renderQuantifier :: forall t. KnownSMTSort t => Builder -> Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Builder
+renderQuantifier qname (Just qvar) f =
+  render2
+    qname
+    ("(" <> render1 (render qvar) (sortSing @t) <> ")")
+    expr
   where
-    renderedXs = foldl' (\s x -> s <> " " <> render x) mempty xs
-{-# INLINEABLE renderNary #-}
+    expr = render $ f $ Var qvar
+renderQuantifier _ Nothing _ = mempty
 
--- | Render values to their sequential SMTLib2-Lisp form, represented as a 'Seq' 'Builder'.
-class RenderSeq a where
-  renderSeq :: a -> Seq Builder
+instance Render (SSMTSort t) where
+  render SBoolSort   = "Bool"
+  render SIntSort    = "Int"
+  render SRealSort   = "Real"
+  render (SBvSort _ p) = render2 "_" ("BitVec" :: Builder) (natVal p)
+  render (SArraySort k v) = render2 "Array" (sortSing' k) (sortSing' v)
+  render SStringSort   = "String"
+  {-# INLINE render #-}
+
+instance Render SMTOption where
+  render (PrintSuccess  b) = render2 "set-option" (":print-success"  :: Builder) b
+  render (ProduceModels b) = render2 "set-option" (":produce-models" :: Builder) b
+  render (Incremental   b) = render2 "set-option" (":incremental"    :: Builder) b
+  render (Custom k v)      = render2 "set-option" (":" <> render k) (render v)
+
+instance Render SoftFormula where
+  render sf = "(assert-soft " <> render (sf^.formula) <> " :weight " <> maybe "1" render (sf^.mWeight) <> renderGroupId (sf^.mGroupId) <> ")"
+    where
+      renderGroupId Nothing = mempty
+      renderGroupId (Just groupId) = " :id " <> render groupId
+
+instance KnownSMTSort t => Render (Minimize t) where
+  render (Minimize expr) = "(minimize " <> render expr <> ")"
+
+instance KnownSMTSort t => Render (Maximize t) where
+  render (Maximize expr) = "(maximize " <> render expr <> ")"
+
+renderSetLogic :: Builder -> Builder
+renderSetLogic = render1 "set-logic"
+{-# INLINE renderSetLogic #-}
+
+renderDeclareVar :: forall t. KnownSMTSort t => SMTVar t -> Builder
+renderDeclareVar v = render3 "declare-fun" v ("()" :: Builder) (sortSing @t)
+{-# INLINE renderDeclareVar #-}
+
+renderAssert :: Expr BoolSort -> Builder
+renderAssert = render1 "assert"
+{-# INLINE renderAssert #-}
+
+renderGetValue :: SMTVar t -> Builder
+renderGetValue x = render1 "get-value" $ "(" <> render x <> ")"
+{-# INLINE renderGetValue #-}
+
+renderPush :: Integer -> Builder
+renderPush i = "(push "<> render i <>")"
+{-# INLINE renderPush #-}
+
+renderPop :: Integer -> Builder
+renderPop i = "(pop "<> render i <>")"
+{-# INLINE renderPop #-}
+
+renderCheckSat :: Builder
+renderCheckSat = "(check-sat)"
+{-# INLINE renderCheckSat #-}
+
+renderGetModel :: Builder
+renderGetModel = "(get-model)"
+{-# INLINE renderGetModel #-}
+
+class RenderProblem s where
+  renderOptions        :: s -> Seq Builder
+  renderLogic          :: s -> Builder
+  renderDeclareVars    :: s -> Seq Builder
+  renderAssertions     :: s -> Seq Builder
+  renderSoftAssertions :: s -> Seq Builder
+  renderMinimizations  :: s -> Seq Builder
+  renderMaximizations  :: s -> Seq Builder
+
+instance RenderProblem SMT where
+  renderOptions = fromList . fmap render . view options
+  renderLogic = maybe mempty (renderSetLogic . stringUtf8) . view mlogic
+  renderDeclareVars = fmap (\(SomeSMTSort v) -> renderDeclareVar v) . view vars
+  renderAssertions = fmap renderAssert . view formulas
+  renderSoftAssertions _ = mempty
+  renderMinimizations _ = mempty
+  renderMaximizations _ = mempty
+
+instance RenderProblem OMT where
+  renderOptions = renderOptions . view smt
+  renderLogic = renderLogic . view smt
+  renderDeclareVars = renderDeclareVars . view smt
+  renderAssertions = renderAssertions . view smt
+  renderSoftAssertions = fmap render . view softFormulas
+  renderMinimizations = fmap (\case SomeSMTSort minExpr -> render minExpr) . view targetMinimize
+  renderMaximizations = fmap (\case SomeSMTSort maxExpr -> render maxExpr) . view targetMaximize
diff --git a/src/Language/Hasmtlib/Solver/Bitwuzla.hs b/src/Language/Hasmtlib/Solver/Bitwuzla.hs
--- a/src/Language/Hasmtlib/Solver/Bitwuzla.hs
+++ b/src/Language/Hasmtlib/Solver/Bitwuzla.hs
@@ -1,21 +1,28 @@
 module Language.Hasmtlib.Solver.Bitwuzla where
 
 import SMTLIB.Backends.Process
+import Language.Hasmtlib.Type.Solver
 
--- | A 'Config' for Bitwuzla.
+-- | A 'SolverConfig' 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 = [] }
+bitwuzla :: SolverConfig s
+bitwuzla = SolverConfig
+  (defaultConfig { exe = "bitwuzla", args = [] })
+  Nothing
+  Nothing
 
 
--- | A 'Config' for Bitwuzla with Kissat as underlying sat-solver.
+-- | A 'SolverConfig' for Bitwuzla with Kissat as underlying sat-solver.
 --
 --   Requires binary @bitwuzla@ and to be in path.
 --   Will use the @kissat@ shipped with @bitwuzla@.
 --
 --   It is recommended to build @bitwuzla@ from source for this to work as expected.
-bitwuzlaKissat :: Config
-bitwuzlaKissat = defaultConfig { exe = "bitwuzla", args = ["--sat-solver=kissat"] }
+bitwuzlaKissat :: SolverConfig s
+bitwuzlaKissat = SolverConfig
+  (defaultConfig { exe = "bitwuzla", args = ["--sat-solver=kissat"] })
+  Nothing
+  Nothing
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,8 +1,11 @@
 module Language.Hasmtlib.Solver.CVC5 where
 
 import SMTLIB.Backends.Process
+import Language.Hasmtlib.Type.Solver
 
--- | A 'Config' for CVC5.
+-- | A 'SolverConfig' for CVC5.
 --   Requires binary @cvc5@ to be in path.
-cvc5 :: Config
-cvc5 = defaultConfig { exe = "cvc5", args = [] }
+cvc5 :: SolverConfig s
+cvc5 = SolverConfig
+  (defaultConfig { exe = "cvc5", args = [] })
+  Nothing Nothing
diff --git a/src/Language/Hasmtlib/Solver/Common.hs b/src/Language/Hasmtlib/Solver/Common.hs
deleted file mode 100644
--- a/src/Language/Hasmtlib/Solver/Common.hs
+++ /dev/null
@@ -1,121 +0,0 @@
-{- |
-This module handles common IO interaction with external SMT-Solvers via external processes.
-
-It is built on top of Tweag's package @smtlib-backends@.
-
-Although there already are several concrete solvers like @Z3@ in @Language.Hasmtlib.Solver.Z3@,
-you may use this module to create your own solver bindings.
--}
-module Language.Hasmtlib.Solver.Common
-(
-  -- * Construction
-  processSolver
-, solver
-, interactiveSolver
-
-  -- * Debugging
-, Debugger(..)
-, debug
-, def
-)
-where
-
-import Language.Hasmtlib.Type.SMT
-import Language.Hasmtlib.Type.OMT
-import Language.Hasmtlib.Type.Solution
-import Language.Hasmtlib.Internal.Render
-import Language.Hasmtlib.Internal.Parser
-import Data.Default
-import Data.Sequence as Seq hiding ((|>), filter)
-import Data.ByteString.Lazy hiding (singleton)
-import Data.ByteString.Lazy.UTF8 (toString)
-import Data.ByteString.Builder
-import Data.Attoparsec.ByteString
-import Control.Lens
-import Control.Monad
-import Control.Monad.IO.Class
-import qualified SMTLIB.Backends.Process as Process
-import qualified SMTLIB.Backends as Backend
-
--- | 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 '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 '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
-  { debugState          :: s -> IO ()               -- ^ Debug the entire state
-  , debugProblem        :: Seq Builder -> IO ()     -- ^ Debug the linewise-rendered problem
-  , debugResultResponse :: ByteString -> IO ()      -- ^ Debug the solvers raw response for @(check-sat)@
-  , debugModelResponse  :: ByteString -> IO ()      -- ^ Debug the solvers raw response for @(get-model)@
-  }
-
-instance Default (Debugger SMT) where
-  def = Debugger
-    { debugState            = \s -> liftIO $ do
-        putStrLn $ "Vars: "       ++ show (Seq.length (s^.vars))
-        putStrLn $ "Assertions: " ++ show (Seq.length (s^.formulas))
-    , debugProblem        = liftIO . mapM_ (putStrLn . toString . toLazyByteString)
-    , debugResultResponse = liftIO . putStrLn . (\s -> "\n" ++ s ++ "\n") . toString
-    , debugModelResponse  = liftIO . mapM_ (putStrLn . toString) . split 13
-    }
-
-instance Default (Debugger OMT) where
-  def = Debugger
-    { debugState          = \omt -> liftIO $ do
-        putStrLn $ "Vars: "                 ++ show (Seq.length (omt^.smt.vars))
-        putStrLn $ "Hard assertions: "      ++ show (Seq.length (omt^.smt.formulas))
-        putStrLn $ "Soft assertions: "      ++ show (Seq.length (omt^.softFormulas))
-        putStrLn $ "Optimization targets: " ++ show (Seq.length (omt^.targetMinimize) + Seq.length (omt^.targetMaximize))
-    , debugProblem        = liftIO . mapM_ (putStrLn . toString . toLazyByteString)
-    , debugResultResponse = liftIO . putStrLn . (\s -> "\n" ++ s ++ "\n") . toString
-    , debugModelResponse  = liftIO . mapM_ (putStrLn . toString) . split 13
-    }
-
--- | A 'Solver' which holds an external process with a SMT-Solver.
---   This will:
---
--- 1. Encode the 'SMT'-problem,
---
--- 2. start a new external process for the SMT-Solver,
---
--- 3. send the problem to the SMT-Solver,
---
--- 4. wait for an answer and parse it,
---
--- 5. close the process and clean up all resources and
---
--- 6. return the decoded solution.
-processSolver :: (RenderSeq s, MonadIO m) => Process.Config -> Maybe (Debugger s) -> Solver s m
-processSolver cfg debugger s = do
-  liftIO $ Process.with cfg $ \handle -> do
-    maybe mempty (`debugState` s) debugger
-    pSolver <- Backend.initSolver Backend.Queuing $ Process.toBackend handle
-
-    let problem = renderSeq s
-    maybe mempty (`debugProblem` problem) debugger
-
-    forM_ problem (Backend.command_ pSolver)
-    resultResponse <- Backend.command pSolver "(check-sat)"
-    maybe mempty (`debugResultResponse` resultResponse) debugger
-
-    modelResponse  <- Backend.command pSolver "(get-model)"
-    maybe mempty (`debugModelResponse` modelResponse) debugger
-
-    case parseOnly resultParser (toStrict resultResponse) of
-      Left e    -> fail e
-      Right res -> case res of
-        Unsat -> return (res, mempty)
-        _     -> case parseOnly anyModelParser (toStrict modelResponse) of
-          Left e    -> fail e
-          Right sol -> return (res, sol)
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,13 +1,20 @@
 module Language.Hasmtlib.Solver.MathSAT where
 
 import SMTLIB.Backends.Process
+import Language.Hasmtlib.Type.Solver
 
--- | A 'Config' for MathSAT.
+-- | A 'SolverConfig' for MathSAT.
 --   Requires binary @mathsat@ to be in path.
-mathsat :: Config
-mathsat = defaultConfig { exe = "mathsat", args = [] }
+mathsat :: SolverConfig s
+mathsat = SolverConfig
+  (defaultConfig { exe = "mathsat", args = [] })
+  Nothing
+  Nothing
 
--- | A 'Config' for OptiMathSAT.
+-- | A 'SolverConfig' for OptiMathSAT.
 --   Requires binary @optimathsat@ to be in path.
-optimathsat :: Config
-optimathsat = defaultConfig { exe = "optimathsat", args = ["-optimization=true"] }
+optimathsat :: SolverConfig s
+optimathsat = SolverConfig
+  (defaultConfig { exe = "optimathsat", args = ["-optimization=true"] })
+  Nothing
+  Nothing
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,8 +1,11 @@
 module Language.Hasmtlib.Solver.OpenSMT where
 
 import SMTLIB.Backends.Process
+import Language.Hasmtlib.Type.Solver
 
--- | A 'Config' for OpenSMT.
+-- | A 'SolverConfig' for OpenSMT.
 --   Requires binary @opensmt@ to be in path.
-opensmt :: Config
-opensmt = defaultConfig { exe = "opensmt", args = [] }
+opensmt :: SolverConfig s
+opensmt = SolverConfig
+  (defaultConfig { exe = "opensmt", args = [] })
+  Nothing Nothing
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,8 +1,11 @@
 module Language.Hasmtlib.Solver.Yices where
 
 import SMTLIB.Backends.Process
+import Language.Hasmtlib.Type.Solver
 
--- | A 'Config' for Yices.
+-- | A 'SolverConfig' for Yices.
 --   Requires binary @yices-smt2@ to be in path.
-yices :: Config
-yices = defaultConfig { exe = "yices-smt2", args = ["--smt2-model-format", "--incremental"] }
+yices :: SolverConfig s
+yices = SolverConfig
+  (defaultConfig { exe = "yices-smt2", args = ["--smt2-model-format", "--incremental"] })
+  Nothing Nothing
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,8 +1,11 @@
 module Language.Hasmtlib.Solver.Z3 where
 
 import SMTLIB.Backends.Process
+import Language.Hasmtlib.Type.Solver
 
--- | A 'Config' for Z3.
+-- | A 'SolverConfig' for Z3.
 --   Requires binary @z3@ to be in path.
-z3 :: Config
-z3 = defaultConfig
+z3 :: SolverConfig s
+z3 = SolverConfig
+  defaultConfig
+  Nothing Nothing
diff --git a/src/Language/Hasmtlib/Type/Bitvec.hs b/src/Language/Hasmtlib/Type/Bitvec.hs
--- a/src/Language/Hasmtlib/Type/Bitvec.hs
+++ b/src/Language/Hasmtlib/Type/Bitvec.hs
@@ -45,9 +45,7 @@
 
 import Prelude hiding ((&&), (||), not)
 import Language.Hasmtlib.Boolean
-import Language.Hasmtlib.Internal.Render
 import Data.GADT.Compare
-import Data.ByteString.Builder
 import Data.Bit
 import Data.Bits
 import Data.Coerce
@@ -117,10 +115,6 @@
 instance Show (Bitvec enc n) where
   show = V.toList . V.map (\b -> if coerce b then '1' else '0') . coerce @_ @(V.Vector n Bit)
   {-# INLINEABLE show #-}
-
-instance Render (Bitvec enc n) where
-  render = stringUtf8 . show
-  {-# INLINE render #-}
 
 instance (KnownBvEnc enc, KnownNat n) => Bits (Bitvec enc n) where
   (.&.) = (&&)
diff --git a/src/Language/Hasmtlib/Type/Debugger.hs b/src/Language/Hasmtlib/Type/Debugger.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Hasmtlib/Type/Debugger.hs
@@ -0,0 +1,172 @@
+{- |
+This module provides debugging capabilites for the problem definition and communication with the external solver.
+-}
+module Language.Hasmtlib.Type.Debugger
+  (
+    -- * Type
+    Debugger(..), StateDebugger(..)
+
+    -- * Construction
+    -- ** Volume
+  , silently
+  , noisy
+  , verbosely
+
+    -- ** Information
+  , optionish
+  , logicish
+  , varish
+  , assertionish
+  , incrementalStackish, getValueish
+  , responseish
+
+  )
+where
+
+import Language.Hasmtlib.Type.SMT
+import Language.Hasmtlib.Type.OMT
+import Data.Sequence as Seq hiding ((|>), filter)
+import Data.ByteString.Lazy hiding (singleton)
+import Data.ByteString.Lazy.UTF8 (toString)
+import Data.ByteString.Builder
+import qualified Data.ByteString.Lazy.Char8 as ByteString.Char8
+import Data.Default
+import Control.Lens hiding (op)
+
+-- | A type holding actions for debugging states holding SMT-Problems.
+data Debugger s = Debugger
+  { debugState          :: s -> IO ()               -- ^ Debug the entire state
+  , debugOption         :: Builder -> IO ()
+  , debugLogic          :: Builder -> IO ()
+  , debugVar            :: Builder -> IO ()
+  , debugAssert         :: Builder -> IO ()
+  , debugPush           :: Builder -> IO ()
+  , debugPop            :: Builder -> IO ()
+  , debugCheckSat       :: Builder -> IO ()
+  , debugGetModel       :: Builder -> IO ()
+  , debugGetValue       :: Builder -> IO ()
+  , debugMinimize       :: Builder -> IO ()
+  , debugMaximize       :: Builder -> IO ()
+  , debugAssertSoft     :: Builder -> IO ()
+  , debugResultResponse :: ByteString -> IO ()      -- ^ Debug the solvers raw response for @(check-sat)@
+  , debugModelResponse  :: ByteString -> IO ()      -- ^ Debug the solvers raw response for @(get-model)@
+  }
+
+instance Default (Debugger s) where
+  def = verbosely
+
+printer :: Builder -> IO ()
+printer = ByteString.Char8.putStrLn . toLazyByteString
+
+-- | The silent 'Debugger'. Does not debug at all.
+silently :: Debugger s
+silently = Debugger
+  (const mempty)
+  (const mempty)
+  (const mempty)
+  (const mempty)
+  (const mempty)
+  (const mempty)
+  (const mempty)
+  (const mempty)
+  (const mempty)
+  (const mempty)
+  (const mempty)
+  (const mempty)
+  (const mempty)
+  (const mempty)
+  (const mempty)
+
+-- | The noisy 'Debugger'.
+--
+--   Debugs the entire problem definition.
+noisy :: Debugger s
+noisy = Debugger
+  (const mempty)
+  printer
+  printer
+  printer
+  printer
+  printer
+  printer
+  printer
+  printer
+  printer
+  printer
+  printer
+  printer
+  (const mempty)
+  (const mempty)
+
+-- | The verbose 'Debugger'.
+--
+--   Debugs all communication between Haskell and the external solver.
+verbosely :: Debugger s
+verbosely = Debugger
+  (const mempty)
+  printer
+  printer
+  printer
+  printer
+  printer
+  printer
+  printer
+  printer
+  printer
+  printer
+  printer
+  printer
+  (ByteString.Char8.putStrLn . (\s -> "\n" <> s <> "\n"))
+  (mapM_ (putStrLn . toString) . split 13)
+
+-- | A 'Debugger' for debugging all rendered options that have been set.
+optionish :: Debugger s
+optionish = silently { debugOption = printer }
+
+-- | A 'Debugger' for debugging the logic that has been set.
+logicish :: Debugger s
+logicish = silently { debugLogic = printer }
+
+-- | A 'Debugger' for debugging all variable declarations.
+varish :: Debugger s
+varish = silently { debugVar = printer }
+
+-- | A 'Debugger' for debugging all assertions.
+assertionish :: Debugger s
+assertionish = silently { debugAssert = printer, debugAssertSoft = printer }
+
+-- | A 'Debugger' for debugging every push/pop-interaction with the solvers incremental stack.
+incrementalStackish :: Debugger s
+incrementalStackish = silently { debugPush = printer, debugPop = printer }
+
+-- | A 'Debugger' for debugging every @(get-value)@ call to the solver.
+getValueish :: Debugger s
+getValueish = silently { debugGetValue = printer }
+
+-- | A 'Debugger' for debugging the entire and raw responses of a solver for the commands @(check-sat)@ and @(get-model)@.
+responseish :: Debugger s
+responseish = silently
+  { debugResultResponse = ByteString.Char8.putStrLn . (\s -> "\n" <> s <> "\n")
+  , debugModelResponse = mapM_ (putStrLn . toString) . split 13
+  }
+
+-- | A class that allows debugging states.
+class StateDebugger s where
+  -- | Debugs information about the problem like the amount of variables and assertions.
+  statistically :: Debugger s
+
+instance StateDebugger SMT where
+  statistically = silently
+    { debugState = \s -> do
+      putStrLn $ "Variables:  " ++ show (Seq.length (s^.vars))
+      putStrLn $ "Assertions: " ++ show (Seq.length (s^.formulas))
+    }
+
+instance StateDebugger OMT where
+  statistically = silently
+    { debugState = \omt -> do
+      putStrLn $ "Variables:       " ++ show (Seq.length (omt^.smt.vars))
+      putStrLn $ "Hard assertions: " ++ show (Seq.length (omt^.smt.formulas))
+      putStrLn $ "Soft assertions: " ++ show (Seq.length (omt^.softFormulas))
+      putStrLn $ "Optimizations:   " ++ show (Seq.length (omt^.targetMinimize) + Seq.length (omt^.targetMaximize))
+    }
diff --git a/src/Language/Hasmtlib/Type/Expr.hs b/src/Language/Hasmtlib/Type/Expr.hs
--- a/src/Language/Hasmtlib/Type/Expr.hs
+++ b/src/Language/Hasmtlib/Type/Expr.hs
@@ -77,15 +77,12 @@
 
 import Prelude hiding (not, and, or, any, all, (&&), (||))
 import Language.Hasmtlib.Internal.Uniplate1
-import Language.Hasmtlib.Internal.Render
-import Language.Hasmtlib.Type.Bitvec (BvEnc(..), KnownBvEnc(..), SBvEnc(..), bvEncSing')
-import Language.Hasmtlib.Type.ArrayMap
+import Language.Hasmtlib.Type.Bitvec (BvEnc(..), KnownBvEnc(..), SBvEnc(..))
 import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Value
 import Language.Hasmtlib.Boolean
 import Data.GADT.Compare
 import Data.GADT.DeepSeq
-import Data.Map hiding (toList)
 import Data.Coerce
 import Data.Proxy
 import Data.Int
@@ -99,8 +96,6 @@
 import Data.Text (pack)
 import Data.List(genericLength)
 import Data.Foldable (toList)
-import Data.ByteString.Builder
-import Data.ByteString.Lazy.UTF8 (toString)
 import qualified Data.Vector.Sized as V
 import Control.Lens hiding (from, to)
 import GHC.TypeLits hiding (someNatVal)
@@ -697,13 +692,13 @@
 -- | This instance is __partial__ for 'toRational', this method is only intended for use with constants.
 instance (KnownSMTSort t, Real (HaskellType t)) => Real (Expr t) where
   toRational (Constant x) = toRational $ unwrapValue x
-  toRational x = error $ "Real#toRational[Expr " <> show (sortSing @t) <> "] only supported for constants. But given: " <> show x
+  toRational _ = error $ "Real#toRational[Expr " <> show (sortSing @t) <> "] only supported for constants."
   {-# INLINE toRational #-}
 
 -- | This instance is __partial__ for 'fromEnum', this method is only intended for use with constants.
 instance (KnownSMTSort t, Enum (HaskellType t)) => Enum (Expr t) where
   fromEnum (Constant x) = fromEnum $ unwrapValue x
-  fromEnum x = error $ "Enum#fromEnum[Expr " <> show (sortSing @t) <> "] only supported for constants. But given: " <> show x
+  fromEnum _ = error $ "Enum#fromEnum[Expr " <> show (sortSing @t) <> "] only supported for constants."
   {-# INLINE fromEnum #-}
   toEnum = Constant . wrapValue . toEnum
   {-# INLINE toEnum #-}
@@ -715,7 +710,7 @@
   divMod x y  = (IDiv x y, Mod x y)
   {-# INLINE divMod #-}
   toInteger (Constant x) = toInteger $ unwrapValue x
-  toInteger x = error $ "Integer#toInteger[Expr " <> show (sortSing @t) <> "] only supported for constants. But given: " <> show x
+  toInteger _ = error $ "Integer#toInteger[Expr " <> show (sortSing @t) <> "] only supported for constants."
   {-# INLINE toInteger #-}
 
 instance Boolean (Expr BoolSort) where
@@ -789,7 +784,7 @@
   complementBit b _ = Not b
   {-# INLINE complementBit #-}
   testBit (Constant (BoolValue b)) _ = b
-  testBit sb _ = error $ "Bits#testBit[Expr BoolSort] is only supported for constants. Given: " <> show sb
+  testBit _ _ = error "Bits#testBit[Expr BoolSort] is only supported for constants."
   {-# INLINE testBit #-}
   bitSizeMaybe _ = Just 1
   {-# INLINE bitSizeMaybe #-}
@@ -808,7 +803,7 @@
   rotateR b _ = b
   {-# INLINE rotateR #-}
   popCount (Constant (BoolValue b)) = if b then 1 else 0
-  popCount sb = error $ "Bits#popCount[Expr BoolSort] is only supported for constants. Given: " <> show sb
+  popCount _ = error "Bits#popCount[Expr BoolSort] is only supported for constants."
   {-# INLINE popCount #-}
 
 -- | This instance is __partial__ for 'testBit' and 'popCount', it's only intended for use with constants ('Constant').
@@ -826,7 +821,7 @@
   bit = Constant . BvValue . Bits.bit
   {-# INLINE bit #-}
   testBit (Constant (BvValue b)) i = Bits.testBit b i
-  testBit sb _ = error $ "Bits#testBit[Expr BvSort] is only supported for constants. Given: " <> show sb
+  testBit _ _ = error "Bits#testBit[Expr BvSort] is only supported for constants."
   {-# INLINE testBit #-}
   bitSizeMaybe _ = Just $ fromIntegral $ natVal $ Proxy @n
   {-# INLINE bitSizeMaybe #-}
@@ -847,7 +842,7 @@
   rotateR b i = BvRotR i b
   {-# INLINE rotateR #-}
   popCount (Constant (BvValue b)) = Bits.popCount b
-  popCount sb = error $ "Bits#popCount[Expr BvSort] is only supported for constants. Given: " <> show sb
+  popCount _ = error $ "Bits#popCount[Expr BvSort] is only supported for constants."
   {-# INLINE popCount #-}
 
 instance Semigroup (Expr StringSort) where
@@ -863,143 +858,6 @@
 instance IsString (Expr StringSort) where
   fromString = Constant . StringValue . pack
   {-# INLINE fromString #-}
-
-instance Render (SMTVar t) where
-  render v = "var_" <> intDec (coerce @(SMTVar t) @Int v)
-  {-# INLINE render #-}
-
-instance Render (Value t) where
-  render (IntValue x)   = render x
-  render (RealValue x)  = render x
-  render (BoolValue x)  = render x
-  render (BvValue   v)  = "#b" <> render v
-  render (ArrayValue arr) = case minViewWithKey (arr^.stored) of
-    Nothing -> constRender $ arr^.arrConst
-    Just ((k,v), stored')
-      | size (arr^.stored) > 1 -> render $ ArrStore (Constant (wrapValue (arr & stored .~ stored'))) (Constant (wrapValue k)) (Constant (wrapValue v))
-      | otherwise  -> constRender v
-    where
-      constRender v = "((as const " <> render (goSing arr) <> ") " <> render (wrapValue v) <> ")"
-      goSing :: forall k v. (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => ConstArray (HaskellType k) (HaskellType v) -> SSMTSort (ArraySort k v)
-      goSing _ = sortSing @(ArraySort k v)
-  render (StringValue x) = "\"" <> render x <> "\""
-
-instance KnownSMTSort t => Render (Expr t) where
-  render (Var v)      = render v
-  render (Constant c) = render c
-  render (Plus x y)   = renderBinary (case sortSing' x of SBvSort _ _ -> "bvadd" ; _ -> "+") x y
-  render (Minus x y)  = renderBinary (case sortSing' x of SBvSort _ _ -> "bvsub" ; _ -> "-") x y
-  render (Neg x)      = renderUnary  (case sortSing' x of SBvSort _ _ -> "bvneg" ; _ -> "-") x
-  render (Mul x y)    = renderBinary (case sortSing' x of SBvSort _ _ -> "bvmul" ; _ -> "*") x y
-  render (Abs x)      = renderUnary  "abs" x
-  render (Mod x y)    = renderBinary opStr x y
-    where
-      opStr = case sortSing' x of
-        SBvSort enc _ -> case bvEncSing' enc of
-          SUnsigned -> "bvurem"
-          SSigned -> "bvsmod"
-        _ -> "mod"
-  render (Rem x y)    = renderBinary opStr x y
-    where
-      opStr = case sortSing' x of
-        SBvSort enc _ -> case bvEncSing' enc of
-          SUnsigned -> "bvurem"
-          SSigned -> "bvsrem"
-        _ -> "rem"
-  render (IDiv x y)   = renderBinary opStr x y
-    where
-      opStr = case sortSing' x of
-        SBvSort enc _ -> case bvEncSing' enc of
-          SUnsigned -> "bvudiv"
-          SSigned -> "bvsdiv"
-        _ -> "div"
-  render (Div x y)    = renderBinary "/" x y
-  render (LTH x y)    = renderBinary opStr x y
-    where
-      opStr = case sortSing' x of
-        SBvSort enc _ -> case bvEncSing' enc of
-          SUnsigned -> "bvult"
-          SSigned -> "bvslt"
-        SStringSort -> "str.<"
-        _ -> "<"
-  render (LTHE x y)   = renderBinary opStr x y
-    where
-      opStr = case sortSing' x of
-        SBvSort enc _ -> case bvEncSing' enc of
-          SUnsigned -> "bvule"
-          SSigned -> "bvsle"
-        SStringSort -> "str.<="
-        _ -> "<="
-  render (EQU xs)     = renderNary "=" $ V.toList xs
-  render (Distinct xs)= renderNary "distinct" $ V.toList xs
-  render (GTHE x y)   = case sortSing' x of
-    SBvSort enc _ -> case bvEncSing' enc of
-      SUnsigned -> renderBinary "bvuge" x y
-      SSigned   -> renderBinary "bvsge" x y
-    SStringSort -> renderBinary "str.<=" y x
-    _           -> renderBinary ">=" x y
-  render (GTH x y)    = case sortSing' x of
-    SBvSort enc _ -> case bvEncSing' enc of
-      SUnsigned -> renderBinary "bvugt" x y
-      SSigned   -> renderBinary "bvsgt" x y
-    SStringSort -> renderBinary "str.<" y x
-    _           -> renderBinary ">" x y
-  render (Not x)      = renderUnary  (case sortSing' x of SBvSort _ _ -> "bvnot" ; _ -> "not") x
-  render (And x y)    = renderBinary (case sortSing' x of SBvSort _ _ -> "bvand" ; _ -> "and") x y
-  render (Or x y)     = renderBinary (case sortSing' x of SBvSort _ _ -> "bvor" ; _ -> "or") x y
-  render (Impl x y)   = renderBinary "=>" x y
-  render (Xor x y)    = renderBinary (case sortSing' x of SBvSort _ _ -> "bvxor" ; _ -> "xor") x y
-  render Pi           = "real.pi"
-  render (Sqrt x)     = renderUnary "sqrt" x
-  render (Exp x)      = renderUnary "exp" x
-  render (Sin x)      = renderUnary "sin" x
-  render (Cos x)      = renderUnary "cos" x
-  render (Tan x)      = renderUnary "tan" x
-  render (Asin x)     = renderUnary "arcsin" x
-  render (Acos x)     = renderUnary "arccos" x
-  render (Atan x)     = renderUnary "arctan" x
-  render (ToReal x)   = renderUnary "to_real" x
-  render (ToInt x)    = renderUnary "to_int" x
-  render (IsInt x)    = renderUnary "is_int" x
-  render (Ite p t f)  = renderTernary "ite" p t f
-  render (BvNand x y)       = renderBinary "bvnand" (render x) (render y)
-  render (BvNor x y)        = renderBinary "bvnor"  (render x) (render y)
-  render (BvShL x y)        = renderBinary "bvshl"  (render x) (render y)
-  render (BvLShR x y)       = renderBinary "bvlshr" (render x) (render y)
-  render (BvAShR x y)       = renderBinary "bvashr" (render x) (render y)
-  render (BvConcat x y)     = renderBinary "concat" (render x) (render y)
-  render (BvRotL i x)       = renderUnary (renderBinary "_" ("rotate_left"  :: Builder) (render $ toInteger i)) (render x)
-  render (BvRotR i x)       = renderUnary (renderBinary "_" ("rotate_right" :: Builder) (render $ toInteger i)) (render x)
-  render (ArrSelect a i)    = renderBinary  "select" (render a) (render i)
-  render (ArrStore a i v)   = renderTernary "store"  (render a) (render i) (render v)
-  render (StrConcat x y)        = renderBinary "str.++"  (render x) (render y)
-  render (StrLength x)          = renderUnary  "str.len" (render x)
-  render (StrAt x i)            = renderBinary "str.at"  (render x) (render i)
-  render (StrSubstring x i j)   = renderTernary "str.substr"  (render x) (render i) (render j)
-  render (StrPrefixOf x y)      = renderBinary "str.prefixof" (render x) (render y)
-  render (StrSuffixOf x y)      = renderBinary "str.suffixof" (render x) (render y)
-  render (StrContains x y)      = renderBinary "str.contains" (render x) (render y)
-  render (StrIndexOf x y i)     = renderTernary "str.indexof"     (render x) (render y) (render i)
-  render (StrReplace x y y')    = renderTernary "str.replace"     (render x) (render y) (render y')
-  render (StrReplaceAll x y y') = renderTernary "str.replace_all" (render x) (render y) (render y')
-  render (ForAll mQvar f) = renderQuantifier "forall" mQvar f
-  render (Exists mQvar f) = renderQuantifier "exists" mQvar f
-
-renderQuantifier :: forall t. KnownSMTSort t => Builder -> Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Builder
-renderQuantifier qname (Just qvar) f =
-  renderBinary
-    qname
-    ("(" <> renderUnary (render qvar) (sortSing @t) <> ")")
-    expr
-  where
-    expr = render $ f $ Var qvar
-renderQuantifier _ Nothing _ = mempty
-
-instance Show (Value t) where
-  show = toString . toLazyByteString . render
-
-instance KnownSMTSort t => Show (Expr t) where
-  show = toString . toLazyByteString . render
 
 type instance Index   (Expr StringSort) = Expr IntSort
 type instance IxValue (Expr StringSort) = Expr StringSort
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
@@ -8,8 +8,12 @@
 module Language.Hasmtlib.Type.OMT
 (
   -- * SoftFormula
+  -- ** Type
   SoftFormula(..)
 
+  -- ** Lens
+, formula, mWeight, mGroupId
+
   -- * Optimization targets
 , Minimize(..), Maximize(..)
 
@@ -23,7 +27,6 @@
 where
 
 import Language.Hasmtlib.Internal.Sharing
-import Language.Hasmtlib.Internal.Render
 import Language.Hasmtlib.Type.MonadSMT
 import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Option
@@ -42,7 +45,7 @@
   { _formula  :: Expr BoolSort    -- ^ The underlying soft formula
   , _mWeight  :: Maybe Double     -- ^ Weight of the soft formula
   , _mGroupId :: Maybe String     -- ^ Group-Id of the soft formula
-  } deriving Show
+  }
 $(makeLenses ''SoftFormula)
 
 -- | A newtype for numerical expressions that are target of a minimization.
@@ -108,22 +111,3 @@
     sm <- use (smt.sharingMode)
     sExpr <- runSharing sm expr
     modifying softFormulas (|> SoftFormula sExpr w gid)
-
-instance Render SoftFormula where
-  render sf = "(assert-soft " <> render (sf^.formula) <> " :weight " <> maybe "1" render (sf^.mWeight) <> renderGroupId (sf^.mGroupId) <> ")"
-    where
-      renderGroupId Nothing = mempty
-      renderGroupId (Just groupId) = " :id " <> render groupId
-
-instance KnownSMTSort t => Render (Minimize t) where
-  render (Minimize expr) = "(minimize " <> render expr <> ")"
-
-instance KnownSMTSort t => Render (Maximize t) where
-  render (Maximize expr) = "(maximize " <> render expr <> ")"
-
-instance RenderSeq OMT where
-  renderSeq omt =
-       renderSeq (omt^.smt)
-    <> fmap render (omt^.softFormulas)
-    <> fmap (\case SomeSMTSort minExpr -> render minExpr) (omt^.targetMinimize)
-    <> fmap (\case SomeSMTSort maxExpr -> render maxExpr) (omt^.targetMaximize)
diff --git a/src/Language/Hasmtlib/Type/Option.hs b/src/Language/Hasmtlib/Type/Option.hs
--- a/src/Language/Hasmtlib/Type/Option.hs
+++ b/src/Language/Hasmtlib/Type/Option.hs
@@ -3,9 +3,7 @@
 -}
 module Language.Hasmtlib.Type.Option where
 
-import Language.Hasmtlib.Internal.Render
 import Data.Data (Data)
-import Data.ByteString.Builder
 
 -- | Options for SMT-Solvers.
 data SMTOption =
@@ -14,9 +12,3 @@
   | Incremental   Bool              -- ^ Incremental solving
   | Custom String String            -- ^ Custom options. First String is the option, second its value.
   deriving (Show, Eq, Ord, Data)
-
-instance Render SMTOption where
-  render (PrintSuccess  b) = renderBinary "set-option" (":print-success"  :: Builder) b
-  render (ProduceModels b) = renderBinary "set-option" (":produce-models" :: Builder) b
-  render (Incremental   b) = renderBinary "set-option" (":incremental"    :: Builder) b
-  render (Custom k v)      = renderBinary "set-option" (":" <> render k) (render v)
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
@@ -15,14 +15,14 @@
   -- * Lens
 , lastPipeVarId, mPipeLogic
 , pipeSharingMode, pipeStableMap, incrSharedAuxs
-, pipeSolver, isDebugging
+, pipeSolver
 )
 where
 
 import Language.Hasmtlib.Internal.Sharing
 import Language.Hasmtlib.Internal.Render
+import Language.Hasmtlib.Type.Debugger
 import Language.Hasmtlib.Type.Expr
-import Language.Hasmtlib.Type.SMT
 import Language.Hasmtlib.Type.OMT (SoftFormula(..), Minimize(..), Maximize(..))
 import Language.Hasmtlib.Type.MonadSMT
 import Language.Hasmtlib.Type.SMTSort
@@ -36,12 +36,10 @@
 import Data.IntMap as IntMap (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)
 import System.Mem.StableName
 
@@ -52,11 +50,11 @@
 data Pipe = Pipe
   { _lastPipeVarId     :: {-# UNPACK #-} !Int                                 -- ^ Last Id assigned to a new var
   , _mPipeLogic        :: Maybe String                                        -- ^ Logic for the SMT-Solver
-  , _pipeSharingMode   :: !SharingMode                                         -- ^ How to share common expressions
+  , _pipeSharingMode   :: !SharingMode                                        -- ^ How to share common expressions
   , _pipeStableMap     :: !(HashMap (StableName ()) (SomeKnownSMTSort Expr))  -- ^ Mapping between a 'StableName' and it's 'Expr' we may share
   , _incrSharedAuxs    :: !(Seq (Seq (StableName ())))                        -- ^ Index of each 'Seq' ('StableName' ()) is incremental stack height where 'StableName' representing auxiliary var that has been shared
   , _pipeSolver        :: !B.Solver                                           -- ^ Active pipe to the backend
-  , _isDebugging       :: !Bool                                               -- ^ Flag if pipe shall debug
+  , _mPipeDebugger      :: Maybe (Debugger Pipe)                                 -- ^ Debugger for communication with the external solver
   }
 $(makeLenses ''Pipe)
 
@@ -67,7 +65,7 @@
     pipe <- get
     modifying (incrSharedAuxs._last) (|> sn)
     let cmd = renderAssert expr
-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd
+    liftIO $ maybe (return ()) (`debugAssert` cmd) (pipe^.mPipeDebugger)
     liftIO $ B.command_ (pipe^.pipeSolver) cmd
   setSharingMode sm = pipeSharingMode .= sm
 
@@ -79,7 +77,7 @@
     pipe <- get
     newVar <- smtvar' p
     let cmd = renderDeclareVar newVar
-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd
+    liftIO $ maybe (return ()) (`debugVar` cmd) (pipe^.mPipeDebugger)
     liftIO $ B.command_ (pipe^.pipeSolver) cmd
     return $ Var newVar
   {-# INLINEABLE var' #-}
@@ -91,45 +89,45 @@
       Nothing    -> return sExpr
       Just logic -> if "QF" `isPrefixOf` logic then return sExpr else quantify sExpr
     let cmd = renderAssert qExpr
-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd
+    liftIO $ maybe (return ()) (`debugAssert` cmd) (pipe^.mPipeDebugger)
     liftIO $ B.command_ (pipe^.pipeSolver) cmd
   {-# INLINEABLE assert #-}
 
   setOption opt = do
     pipe <- get
     let cmd = render opt
-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd
+    liftIO $ maybe (return ()) (`debugOption` cmd) (pipe^.mPipeDebugger)
     liftIO $ B.command_ (pipe^.pipeSolver) cmd
 
   setLogic l = do
     mPipeLogic ?= l
     pipe <- get
     let cmd = renderSetLogic (stringUtf8 l)
-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd
+    liftIO $ maybe (return ()) (`debugLogic` cmd) (pipe^.mPipeDebugger)
     liftIO $ B.command_ (pipe^.pipeSolver) cmd
 
 instance (MonadState Pipe m, MonadIO m) => MonadIncrSMT Pipe m where
   push = do
     pipe <- get
-    let cmd = "(push 1)"
-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd
+    let cmd = renderPush 1
+    liftIO $ maybe (return ()) (`debugPush` cmd) (pipe^.mPipeDebugger)
     liftIO $ B.command_ (pipe^.pipeSolver) cmd
     incrSharedAuxs <>= mempty
 
   pop = do
     pipe <- get
-    let cmd = "(pop 1)"
-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd
+    let cmd = renderPop 1
+    liftIO $ maybe (return ()) (`debugPop` cmd) (pipe^.mPipeDebugger)
     liftIO $ B.command_ (pipe^.pipeSolver) cmd
     forMOf_ (incrSharedAuxs._last.folded) pipe (\sn -> pipeStableMap.at sn .= Nothing)
     modifying incrSharedAuxs $ \case (auxs:>_) -> auxs ; auxs -> auxs
 
   checkSat = do
     pipe <- get
-    let cmd = "(check-sat)"
-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd
+    let cmd = renderCheckSat
+    liftIO $ maybe (return ()) (`debugCheckSat` cmd) (pipe^.mPipeDebugger)
     result <- liftIO $ B.command (pipe^.pipeSolver) cmd
-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn result
+    liftIO $ maybe (return ()) (`debugResultResponse` result) (pipe^.mPipeDebugger)
     case parseOnly resultParser (toStrict result) of
       Left e    -> liftIO $ do
         print result
@@ -138,10 +136,10 @@
 
   getModel = do
     pipe   <- get
-    let cmd = "(get-model)"
-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd
+    let cmd = renderGetModel
+    liftIO $ maybe (return ()) (`debugGetModel` cmd) (pipe^.mPipeDebugger)
     model <- liftIO $ B.command (pipe^.pipeSolver) cmd
-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn model
+    liftIO $ maybe (return ()) (`debugModelResponse` model) (pipe^.mPipeDebugger)
     case parseOnly anyModelParser (toStrict model) of
       Left e    -> liftIO $ do
         print model
@@ -151,10 +149,10 @@
   getValue :: forall t. KnownSMTSort t => Expr t -> m (Maybe (Decoded (Expr t)))
   getValue v@(Var x) = do
     pipe   <- get
-    let cmd = renderUnary "get-value" $ "(" <> render x <> ")"
-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd
+    let cmd = renderGetValue x
+    liftIO $ maybe (return ()) (`debugGetValue` cmd) (pipe^.mPipeDebugger)
     model <- liftIO $ B.command (pipe^.pipeSolver) cmd
-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn model
+    liftIO $ maybe (return ()) (`debugModelResponse` model) (pipe^.mPipeDebugger)
     case parseOnly (getValueParser @t x) (toStrict model) of
       Left e    -> liftIO $ do
         print model
@@ -175,7 +173,7 @@
     pipe <- get
     sExpr <- runSharing (pipe^.pipeSharingMode) expr
     let cmd = render $ Minimize sExpr
-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd
+    liftIO $ maybe (return ()) (`debugMinimize` cmd) (pipe^.mPipeDebugger)
     liftIO $ B.command_ (pipe^.pipeSolver) cmd
   {-# INLINEABLE minimize #-}
 
@@ -183,7 +181,7 @@
     pipe <- get
     sExpr <- runSharing (pipe^.pipeSharingMode) expr
     let cmd = render $ Maximize sExpr
-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd
+    liftIO $ maybe (return ()) (`debugMaximize` cmd) (pipe^.mPipeDebugger)
     liftIO $ B.command_ (pipe^.pipeSolver) cmd
   {-# INLINEABLE maximize #-}
 
@@ -191,6 +189,6 @@
     pipe <- get
     sExpr <- runSharing (pipe^.pipeSharingMode) expr
     let cmd = render $ SoftFormula sExpr w gid
-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd
+    liftIO $ maybe (return ()) (`debugAssertSoft` cmd) (pipe^.mPipeDebugger)
     liftIO $ B.command_ (pipe^.pipeSolver) cmd
   {-# INLINEABLE assertSoft #-}
diff --git a/src/Language/Hasmtlib/Type/Relation.hs b/src/Language/Hasmtlib/Type/Relation.hs
--- a/src/Language/Hasmtlib/Type/Relation.hs
+++ b/src/Language/Hasmtlib/Type/Relation.hs
@@ -61,7 +61,6 @@
 -- so @a@ and @b@ have to be instances of 'Ix',
 -- and both \(A\) and \(B\) are intervals.
 newtype Relation a b = Relation (Array (a, b) (Expr BoolSort))
-  deriving stock Show
 
 instance (Ix a, Ix b) => Codec (Relation a b) where
   type Decoded (Relation a b) = Array (a, b) Bool
diff --git a/src/Language/Hasmtlib/Type/SMT.hs b/src/Language/Hasmtlib/Type/SMT.hs
--- a/src/Language/Hasmtlib/Type/SMT.hs
+++ b/src/Language/Hasmtlib/Type/SMT.hs
@@ -13,14 +13,10 @@
 , lastVarId, vars, formulas
 , mlogic, options
 , sharingMode, Language.Hasmtlib.Type.SMT.stableMap
-
-  -- * Rendering
-, renderSetLogic, renderDeclareVar, renderAssert, renderVars
 )
 where
 
 import Language.Hasmtlib.Internal.Sharing
-import Language.Hasmtlib.Internal.Render
 import Language.Hasmtlib.Type.MonadSMT
 import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Option
@@ -30,7 +26,6 @@
 import Data.Coerce
 import Data.Sequence hiding ((|>), filter)
 import Data.Data (toConstr, showConstr)
-import Data.ByteString.Builder
 import Data.HashMap.Lazy (HashMap)
 import Control.Monad.State
 import Control.Lens hiding (List)
@@ -82,25 +77,3 @@
       eqCon l r = showConstr (toConstr l) == showConstr (toConstr r)
 
   setLogic l = mlogic ?= l
-
-instance RenderSeq SMT where
-  renderSeq smt =
-       fromList (render <$> smt^.options)
-       >< maybe mempty (singleton . renderSetLogic . stringUtf8) (smt^.mlogic)
-       >< renderVars (smt^.vars)
-       >< fmap renderAssert (smt^.formulas)
-
-renderSetLogic :: Builder -> Builder
-renderSetLogic = renderUnary "set-logic"
-
-renderDeclareVar :: forall t. KnownSMTSort t => SMTVar t -> Builder
-renderDeclareVar v = renderTernary "declare-fun" v ("()" :: Builder) (sortSing @t)
-{-# INLINEABLE renderDeclareVar #-}
-
-renderAssert :: Expr BoolSort -> Builder
-renderAssert = renderUnary "assert"
-{-# INLINEABLE renderAssert #-}
-
-renderVars :: Seq (SomeKnownSMTSort SMTVar) -> Seq Builder
-renderVars = fmap (\(SomeSMTSort v) -> renderDeclareVar v)
-{-# INLINEABLE renderVars #-}
diff --git a/src/Language/Hasmtlib/Type/SMTSort.hs b/src/Language/Hasmtlib/Type/SMTSort.hs
--- a/src/Language/Hasmtlib/Type/SMTSort.hs
+++ b/src/Language/Hasmtlib/Type/SMTSort.hs
@@ -25,12 +25,10 @@
 
 import Language.Hasmtlib.Internal.Constraint
 import Language.Hasmtlib.Type.Bitvec
-import Language.Hasmtlib.Internal.Render
 import Language.Hasmtlib.Type.ArrayMap
 import Data.GADT.Compare
 import Data.Kind
 import Data.Proxy
-import Data.ByteString.Builder
 import qualified Data.Text as Text
 import Control.Lens
 import GHC.TypeLits
@@ -135,12 +133,3 @@
 
 -- | An existential wrapper that hides some known 'SMTSort'.
 type SomeKnownSMTSort f = SomeSMTSort '[KnownSMTSort] f
-
-instance Render (SSMTSort t) where
-  render SBoolSort   = "Bool"
-  render SIntSort    = "Int"
-  render SRealSort   = "Real"
-  render (SBvSort _ p) = renderBinary "_" ("BitVec" :: Builder) (natVal p)
-  render (SArraySort k v) = renderBinary "Array" (sortSing' k) (sortSing' v)
-  render SStringSort   = "String"
-  {-# INLINEABLE render #-}
diff --git a/src/Language/Hasmtlib/Type/Solution.hs b/src/Language/Hasmtlib/Type/Solution.hs
--- a/src/Language/Hasmtlib/Type/Solution.hs
+++ b/src/Language/Hasmtlib/Type/Solution.hs
@@ -10,8 +10,8 @@
 -}
 module Language.Hasmtlib.Type.Solution
 (
-  -- * Solver
-  Solver, Result(..)
+  -- * Result
+  Result(..)
 
   -- * Solution
 , Solution
@@ -40,9 +40,6 @@
 import Data.Dependent.Map.Lens
 import Control.Lens
 
--- | Function that turns a state into a result and a solution.
-type Solver s m = s -> m (Result, Solution)
-
 -- | Results of check-sat commands.
 data Result = Unsat | Unknown | Sat deriving (Show, Eq, Ord)
 
@@ -50,15 +47,17 @@
 
 -- | Newtype for 'IntMap' 'Value' so we can use it as right-hand-side of 'DMap'.
 newtype IntValueMap t = IntValueMap (IntMap (Value t))
-  deriving stock Show
   deriving newtype (Semigroup, Monoid)
 
+deriving stock instance Show (Value t) => Show (IntValueMap t)
+
 -- | A solution for a single variable.
 data SMTVarSol (t :: SMTSort) = SMTVarSol
   { _solVar :: SMTVar t                       -- ^ A variable in the SMT-Problem
   , _solVal :: Value t                        -- ^ An assignment for this variable in a solution
-  } deriving Show
+  }
 $(makeLenses ''SMTVarSol)
+deriving stock instance Show (Value t) => Show (SMTVarSol t)
 
 -- | Alias class for constraint 'Ord' ('HaskellType' t)
 class Ord (HaskellType t) => OrdHaskellType t
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,16 +1,30 @@
+{-# LANGUAGE TemplateHaskell #-}
+
 {- |
 This module provides functions for having SMT-Problems solved by external solvers.
+
+The base type for every solver is the 'SolverConfig'. It describes where the solver executable is located and how it should behave.
+You can provide a time-out using the decorator 'timingout'.
+Another decorator - 'debugging' - allows you to debug all the information you want. The actual debuggers can be found in "Language.Hasmtlib.Type.Debugger".
 -}
 module Language.Hasmtlib.Type.Solver
   (
-  -- * WithSolver
-  WithSolver(..)
+  -- * Solver configuration
 
+  -- ** Type
+  SolverConfig(..)
+
+  -- ** Decoration
+  , debugging, timingout
+
+  -- ** Lens
+  , processConfig, mTimeout, mDebugger
+
   -- * Stateful solving
-  , solveWith
+  , Solver, solver, solveWith
 
   -- * Interactive solving
-  , interactiveWith, debugInteractiveWith
+  , interactiveWith
 
   -- ** Minimzation
   , solveMinimized
@@ -20,26 +34,111 @@
   )
 where
 
+import Language.Hasmtlib.Internal.Render
+import Language.Hasmtlib.Internal.Parser
 import Language.Hasmtlib.Type.MonadSMT
+import Language.Hasmtlib.Type.Debugger
 import Language.Hasmtlib.Type.Expr
 import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Type.Pipe
 import Language.Hasmtlib.Codec
+import Data.ByteString.Lazy hiding (singleton)
 import qualified SMTLIB.Backends as Backend
 import qualified SMTLIB.Backends.Process as Process
 import Data.Default
 import Data.Maybe
+import Data.Attoparsec.ByteString (parseOnly)
+import Control.Lens hiding (op)
+import Control.Monad
 import Control.Monad.State
+import Control.Monad.Trans.Control
+import System.Timeout.Lifted
 
--- | Data that can have a 'Backend.Solver' which may be debugged.
-class WithSolver a where
-  -- | Create a value with a 'Backend.Solver' and a 'Bool' for whether to debug the 'Backend.Solver'.
-  withSolver :: Backend.Solver -> Bool -> a
+-- | Function that turns a state into a 'Result' and a 'Solution'.
+type Solver s m = s -> m (Result, Solution)
 
-instance WithSolver Pipe where
-  withSolver = Pipe 0 Nothing def mempty mempty
+-- | Configuration for solver processes.
+data SolverConfig s = SolverConfig
+  { _processConfig  :: Process.Config         -- ^ The underlying config of the process
+  , _mTimeout       :: Maybe Int              -- ^ Timeout in microseconds
+  , _mDebugger      :: Maybe (Debugger s)     -- ^ Debugger for communication with external solver
+  }
+$(makeLenses ''SolverConfig)
 
+-- | Creates a 'Solver' which holds an external process with a SMT-Solver.
+--
+--   This will:
+--
+-- 1. Encode the SMT-problem,
+--
+-- 2. start a new external process for the SMT-Solver,
+--
+-- 3. send the problem to the SMT-Solver,
+--
+-- 4. wait for an answer and parse it,
+--
+-- 5. close the process and clean up all resources and
+--
+-- 6. return the decoded solution.
+solver :: (RenderProblem s, MonadIO m) => SolverConfig s -> Solver s m
+solver (SolverConfig cfg mTO debugger) s = do
+  liftIO $ Process.with cfg $ \handle -> do
+    maybe mempty (`debugState` s) debugger
+    pSolver <- Backend.initSolver Backend.Queuing $ Process.toBackend handle
+
+    let os   = renderOptions s
+        l    = renderLogic s
+        vs   = renderDeclareVars s
+        as   = renderAssertions s
+        sas  = renderSoftAssertions s
+        mins = renderMinimizations s
+        maxs = renderMaximizations s
+    maybe mempty (forM_ os . debugOption) debugger
+    forM_ os (Backend.command_ pSolver)
+    maybe mempty (`debugLogic` l) debugger
+    Backend.command_ pSolver l
+    maybe mempty (forM_ vs . debugVar) debugger
+    forM_ vs (Backend.command_ pSolver)
+    maybe mempty (forM_ as . debugAssert) debugger
+    forM_ as (Backend.command_ pSolver)
+    maybe mempty (forM_ sas . debugAssertSoft) debugger
+    forM_ sas (Backend.command_ pSolver)
+    maybe mempty (forM_ mins . debugMinimize) debugger
+    forM_ mins (Backend.command_ pSolver)
+    maybe mempty (forM_ maxs . debugMaximize) debugger
+    forM_ maxs (Backend.command_ pSolver)
+
+    let timingOut io = case mTO of
+          Nothing -> io
+          Just t -> fromMaybe "unknown" <$> timeout t io
+    resultResponse <- timingOut $ Backend.command pSolver renderCheckSat
+    maybe mempty (`debugResultResponse` resultResponse) debugger
+
+    modelResponse <- Backend.command pSolver renderGetModel
+    maybe mempty (`debugModelResponse` modelResponse) debugger
+
+    case parseOnly resultParser (toStrict resultResponse) of
+      Left e    -> fail e
+      Right res -> case res of
+        Unsat -> return (res, mempty)
+        _     -> case parseOnly anyModelParser (toStrict modelResponse) of
+          Left e    -> fail e
+          Right sol -> return (res, sol)
+
+-- | Decorates a 'SolverConfig' with a timeout. The timeout is given as an 'Int' which specifies
+--   after how many __microseconds__ the external solver process shall time out on @(check-sat)@.
+--
+--   When timing out, the 'Result' will always be 'Unknown'.
+--
+--   This uses 'timeout' internally.
+timingout :: Int -> SolverConfig s -> SolverConfig s
+timingout t cfg = cfg & mTimeout ?~ t
+
+-- | Decorates a 'SolverConfig' with a 'Debugger'.
+debugging :: Debugger s -> SolverConfig s -> SolverConfig s
+debugging debugger cfg = cfg & mDebugger ?~ debugger
+
 -- | @'solveWith' solver prob@ solves a SMT problem @prob@ with the given
 -- @solver@. It returns a pair consisting of:
 --
@@ -72,9 +171,9 @@
 --
 -- The solver will probably answer with @x := 1@.
 solveWith :: (Default s, Monad m, Codec a) => Solver s m -> StateT s m a -> m (Result, Maybe (Decoded a))
-solveWith solver m = do
+solveWith solving m = do
   (a, problem) <- runStateT m def
-  (result, solution) <- solver problem
+  (result, solution) <- solving problem
 
   return (result, decode solution a)
 
@@ -88,9 +187,7 @@
 --
 -- main :: IO ()
 -- main = do
---   cvc5Living <- interactiveSolver cvc5
---   interactiveWith @Pipe cvc5Living $ do
---     setOption $ Incremental True
+--   interactiveWith z3 $ do
 --     setOption $ ProduceModels True
 --     setLogic \"QF_LRA\"
 --
@@ -117,16 +214,16 @@
 --
 --   return ()
 -- @
-interactiveWith :: (WithSolver s, MonadIO m) => (Backend.Solver, Process.Handle) -> StateT s m () -> m ()
-interactiveWith (solver, handle) m = do
-  _ <- 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
+interactiveWith :: (MonadIO m, MonadBaseControl IO m) => SolverConfig Pipe -> StateT Pipe m a -> m (Maybe a)
+interactiveWith cfg m = do
+  handle <- liftIO $ Process.new $ cfg^.processConfig
+  processSolver <- liftIO $ Backend.initSolver Backend.Queuing $ Process.toBackend handle
+  let timingOut io = case cfg^.mTimeout of
+        Nothing -> Just <$> io
+        Just t -> timeout t io
+  ma <- timingOut $ runStateT m $ Pipe 0 Nothing def mempty mempty processSolver (cfg^.mDebugger)
   liftIO $ Process.close handle
+  return $ fmap fst ma
 
 -- | Solves the current problem with respect to a minimal solution for a given numerical expression.
 --