diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -94,6 +94,8 @@
   ```haskell
       cvc5Living <- interactiveSolver cvc5
       interactiveWith cvc5Living $ do
+        setLogic "QF_LIA"    
+        setOption $ ProduceModels True
         x <- var @IntSort
         assert $ x === 42
         result <- checkSat
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:               1.0.1
+version:               1.0.2
 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.
@@ -59,7 +59,7 @@
                      , text                         >= 2.0.2  && < 3
                      , data-default                 >= 0.7.1  && < 1
                      , lens                         >= 5      && < 6
-                     , smtlib-backends              >= 0.3    && < 1
+                     , smtlib-backends              >= 0.4    && < 1
                      , smtlib-backends-process      >= 0.3    && < 1
                      , utf8-string                  >= 1.0.2  && < 2
                      , bitvec                       >= 1.1.5  && < 2
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
@@ -13,18 +13,20 @@
 -- | A 'MonadState' that holds an SMT-Problem.
 class MonadState s m => MonadSMT s m where
   -- | Construct a variable.
-  -- 
+  --   This is mainly intended for internal use.
+  --   In the API use 'var'' instead.
+  --   
   -- @
   -- x :: SMTVar RealType <- smtvar' (Proxy @RealType)
   -- @
-  smtvar'    :: forall t. KnownSMTSort t => Proxy t -> m (SMTVar t)
+  smtvar' :: forall t. KnownSMTSort t => Proxy t -> m (SMTVar t)
   
   -- | Construct a variable as expression.
   -- 
   -- @
   -- x :: Expr RealType <- var' (Proxy @RealType)
   -- @
-  var'       :: forall t. KnownSMTSort t => Proxy t -> m (Expr t)
+  var' :: forall t. KnownSMTSort t => Proxy t -> m (Expr t)
 
   -- | Assert a boolean expression.
   -- 
@@ -32,7 +34,7 @@
   -- x :: Expr IntType <- var @IntType
   -- assert $ x + 5 === 42
   -- @
-  assert    :: Expr BoolSort -> m ()
+  assert :: Expr BoolSort -> m ()
 
   -- | Set an SMT-Solver-Option.
   -- 
@@ -44,9 +46,9 @@
   -- | Set the logic for the SMT-Solver to use.
   -- 
   -- @
-  -- setLogic "QF_LRA"
+  -- setLogic \"QF_LRA\"
   -- @
-  setLogic  :: String -> m ()
+  setLogic :: String -> m ()
 
 -- | Wrapper for 'var'' which hides the 'Proxy'.
 var :: forall t s m. (KnownSMTSort t, MonadSMT s m) => m (Expr t)
@@ -54,8 +56,8 @@
 {-# INLINE var #-}
 
 -- | Wrapper for 'smtvar'' which hides the 'Proxy'.
--- | This is mainly intended for internal use.
--- | In the API use 'var' instead.
+--   This is mainly intended for internal use.
+--   In the API use 'var' instead.
 smtvar :: forall t s m. (KnownSMTSort t, MonadSMT s m) => m (SMTVar t)
 smtvar = smtvar' (Proxy @t)
 {-# INLINE smtvar #-}
@@ -116,10 +118,10 @@
   --
   -- @
   -- x <- var @RealSort
-  -- y <- var @RealSort
+  -- y <- var
   -- assert $ x >? y && y <? (-1)
   -- res <- checkSat
-  -- case checkSat of
+  -- case res of
   --   Unsat -> print "Unsat. Cannot get model."
   --   r     -> do
   --     model <- getModel
@@ -134,7 +136,7 @@
   -- x <- var @RealSort
   -- assert $ x >? 10
   -- res <- checkSat
-  -- case checkSat of
+  -- case res of
   --   Unsat -> print "Unsat. Cannot get value for 'x'."
   --   r     -> do
   --     x' <- getValue x
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
@@ -27,7 +27,7 @@
 $(makeLenses ''SMT)
 
 instance Default SMT where
-  def = SMT 0 mempty mempty mempty mempty
+  def = SMT 0 mempty mempty mempty [ProduceModels True]
 
 instance MonadState SMT m => MonadSMT SMT m where
   smtvar' _ = fmap coerce $ lastVarId <+= 1
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
@@ -10,7 +10,7 @@
 import Data.Default
 import Control.Monad.State
 
--- | Data that can have a 'B.Solver'
+-- | Data that can have a 'B.Solver'.
 class WithSolver a where
   withSolver :: B.Solver -> a
 
@@ -36,7 +36,7 @@
 -- main :: IO ()
 -- main = do
 --   res <- solveWith (solver cvc5) $ do
---     setLogic "QF_LIA"
+--     setLogic \"QF_LIA\"
 -- 
 --     x <- var @IntSort
 -- 
@@ -59,14 +59,14 @@
 -- 
 -- @
 -- import Language.Hasmtlib
--- import Data.Proxy
 -- import Control.Monad.IO.Class
 -- 
 -- main :: IO ()
 -- main = do
 --   cvc5Living <- interactiveSolver cvc5
 --   interactiveWith cvc5Living $ do
---     setLogic "QF_LIA"
+--     setOption $ ProduceModels True
+--     setLogic \"QF_LIA\"
 -- 
 --     x <- var @IntSort
 --