diff --git a/kore/src/ErrorContext.hs b/kore/src/ErrorContext.hs
new file mode 100644
index 0000000000..f13a6346e0
--- /dev/null
+++ b/kore/src/ErrorContext.hs
@@ -0,0 +1,61 @@
+{- |
+Copyright   : (c) Runtime Verification, 2020
+License     : NCSA
+
+-}
+
+module ErrorContext
+    ( ErrorContext (..)
+    , withErrorContext
+    ) where
+
+import Prelude
+
+import Control.Exception
+    ( Exception (..)
+    , SomeException
+    , mapException
+    )
+import Data.String
+    ( fromString
+    )
+import Data.Typeable
+    ( Typeable
+    )
+
+import Pretty
+    ( Pretty
+    )
+import qualified Pretty
+
+data ErrorContext where
+    ErrorContext
+        :: (Pretty context, Show context)
+        => String  -- ^ A brief message (one line) introducing the context.
+        -> context  -- ^ Some 'Pretty'-printable data for context.
+        -> SomeException  -- ^ The error itself.
+        -> ErrorContext
+    deriving (Typeable)
+
+deriving instance Show ErrorContext
+
+instance Pretty ErrorContext where
+    pretty (ErrorContext intro context someException) =
+        Pretty.vsep
+        [ fromString intro
+        , Pretty.indent 4 (Pretty.pretty context)
+        , Pretty.prettyException someException
+        ]
+
+instance Exception ErrorContext where
+    displayException = show . Pretty.pretty
+
+{- | Compute a value, putting error messages in context.
+ -}
+withErrorContext
+    :: (Pretty context, Show context)
+    => String
+    -> context
+    -> a  -- ^ The value computed.
+    -> a
+withErrorContext intro context = mapException (ErrorContext intro context)
diff --git a/kore/src/Kore/Internal/Condition.hs b/kore/src/Kore/Internal/Condition.hs
index 0ca4c0f406..2d4b619f15 100644
--- a/kore/src/Kore/Internal/Condition.hs
+++ b/kore/src/Kore/Internal/Condition.hs
@@ -37,6 +37,7 @@ module Kore.Internal.Condition
 
 import Prelude.Kore
 
+import ErrorContext
 import Kore.Attribute.Pattern.FreeVariables
     ( freeVariables
     , isFreeVariable
@@ -182,11 +183,15 @@ The 'normalized' part becomes the normalized 'substitution', while the
 
  -}
 fromNormalizationSimplified
-    :: InternalVariable variable
+    :: HasCallStack
+    => InternalVariable variable
     => Normalization variable
     -> Condition variable
-fromNormalizationSimplified Normalization { normalized, denormalized } =
+fromNormalizationSimplified
+    normalization@Normalization { normalized, denormalized }
+  =
     predicate' <> substitution'
+    & withErrorContext "while normalizing substitution" normalization
   where
     predicate' =
         Conditional.fromPredicate
@@ -195,7 +200,7 @@ fromNormalizationSimplified Normalization { normalized, denormalized } =
         $ Substitution.wrap denormalized
     substitution' =
         Conditional.fromSubstitution
-        $ Substitution.unsafeWrap (Substitution.assignmentToPair <$> normalized)
+        $ Substitution.unsafeWrapFromAssignments normalized
     markSimplifiedIfChildrenSimplified childrenList result =
         Predicate.setSimplified childrenSimplified result
       where
diff --git a/kore/src/Kore/Internal/Substitution.hs b/kore/src/Kore/Internal/Substitution.hs
index c53471a529..21bb72e016 100644
--- a/kore/src/Kore/Internal/Substitution.hs
+++ b/kore/src/Kore/Internal/Substitution.hs
@@ -69,6 +69,7 @@ import qualified Data.Set as Set
 import qualified Generics.SOP as SOP
 import qualified GHC.Generics as GHC
 
+import ErrorContext
 import Kore.Attribute.Pattern.FreeVariables as FreeVariables
 import qualified Kore.Attribute.Pattern.Simplified as Attribute
     ( Simplified (..)
@@ -92,7 +93,12 @@ import Kore.TopBottom
     ( TopBottom (..)
     )
 import Kore.Unparser
-    ( unparseToString
+    ( Unparse
+    , unparse
+    , unparseToString
+    )
+import Pretty
+    ( Pretty
     )
 import qualified Pretty
 import qualified SQL
@@ -118,6 +124,14 @@ instance NFData variable => NFData (Assignment variable)
 
 instance Hashable variable => Hashable (Assignment variable)
 
+instance (Ord variable, Unparse variable) => Pretty (Assignment variable) where
+    pretty Assignment_ { assignedVariable, assignedTerm } =
+        Pretty.vsep
+        [ Pretty.hsep ["assigned variable:", unparse assignedVariable]
+        , "assigned term:"
+        , Pretty.indent 4 (unparse assignedTerm)
+        ]
+
 -- | Smart constructor for 'Assignment'. It enforces the invariant
 -- that for variable renaming, the smaller variable will be on the
 -- left of the substitution.
@@ -419,7 +433,7 @@ wrap xs = Substitution xs
 -- this unless you are sure you need it.
 unsafeWrap
     :: HasCallStack
-    => Ord variable
+    => InternalVariable variable
     => [(SomeVariable variable, TermLike variable)]
     -> Substitution variable
 unsafeWrap =
@@ -436,7 +450,9 @@ unsafeWrap =
         & assert (not $ any depends $ Map.keys subst)
         -- and if this is an element variable substitution, the substitution
         -- must be defined.
+        -- TODO (thomas.tuegel): isBottom -> isDefinedPattern
         & assert (not $ isElementVariable var && isBottom termLike)
+        & withErrorContext "while wrapping substitution" (assign var termLike)
       where
         Variable { variableName } = var
         occurs = TermLike.hasFreeVariable variableName
@@ -444,7 +460,8 @@ unsafeWrap =
             TermLike.hasFreeVariable variableName' termLike
 
 unsafeWrapFromAssignments
-    :: Ord variable
+    :: HasCallStack
+    => InternalVariable variable
     => [Assignment variable]
     -> Substitution variable
 unsafeWrapFromAssignments =
@@ -678,6 +695,23 @@ instance Semigroup (Normalization variable) where
 instance Monoid (Normalization variable) where
     mempty = Normalization mempty mempty
 
+instance InternalVariable variable => Pretty (Normalization variable) where
+    pretty Normalization { normalized, denormalized } =
+        Pretty.vsep
+        [ "normalized:"
+        , (Pretty.indent 4 . Pretty.vsep) (map prettyPair normalized)
+        , "denormalized:"
+        , (Pretty.indent 4 . Pretty.vsep) (map prettyPair denormalized)
+        ]
+      where
+        prettyPair assignment =
+            Pretty.vsep
+            [ "variable:"
+            , Pretty.indent 4 (unparse $ assignedVariable assignment)
+            , "term:"
+            , Pretty.indent 4 (unparse $ assignedTerm assignment)
+            ]
+
 mkNormalization
     :: InternalVariable variable
     => [(SomeVariable variable, TermLike variable)]
diff --git a/kore/src/Pretty.hs b/kore/src/Pretty.hs
index 35734eeb4d..5d0a81fe1a 100644
--- a/kore/src/Pretty.hs
+++ b/kore/src/Pretty.hs
@@ -11,10 +11,18 @@ module Pretty
     , renderString
     , renderIO
     , hPutDoc, putDoc
+    , prettyException
     ) where
 
 import Prelude.Kore
 
+import Control.Exception
+    ( Exception
+    , displayException
+    )
+import Data.String
+    ( fromString
+    )
 import Data.Text
     ( Text
     )
@@ -52,3 +60,8 @@ flattenSimpleDocStream = worker
 
 renderText :: SimpleDocStream ann -> Text
 renderText = renderStrict
+
+{- | Display an 'Exception' nicely for the user.
+ -}
+prettyException :: Exception exn => exn -> Doc ann
+prettyException = vsep . map fromString . lines . displayException