diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index c6a8cd06..486a9c14 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -68,8 +68,13 @@ jobs:
 
       - name: Install SMT solvers
         run: |
+          echo "${{ secrets.MATHSAT_INSTALL_DEPLOY_KEY }}" >> mathsat_id_ed25519
+          chmod 400 mathsat_id_ed25519
+          ssh-agent bash -c 'ssh-add mathsat_id_ed25519; git clone git@github.com:NethermindEth/mathsat-install.git'
+          cp mathsat-install/install-mathsat.sh ./scripts/ci/install-mathsat.sh
           sh ./scripts/ci/install-z3-linux-amd64.sh
           sh ./scripts/ci/install-cvc5-linux.sh
+          sh ./scripts/ci/install-mathsat.sh
 
       - uses: actions/setup-python@v4
         with:
diff --git a/README.md b/README.md
index 310fc461..3c40df93 100644
--- a/README.md
+++ b/README.md
@@ -1037,6 +1037,45 @@ please open an issue!
 Horus does not yet fully support account contracts compiled with the
 `--account_contract` CLI flag.
 
+#### Why am I seeing `Unexpected annotation type` or `annotation is not allowed here` in my commented-out code?
+
+This can sometimes happen when you comment-out a function, but not its
+annotations (which are themselves already comments). It can also happen when
+you comment out a decorator, like `@external` (because then it looks like a
+Horus annotation: `// @external`).
+
+Make sure to add another set of `///` characters in front of any annotations
+that were associated with your commented-out function. Suppose we want to
+comment out an annotated function like this:
+```cairo
+// @pre x == 0
+// @post 0 == 1
+@external
+func f(x : felt) -> felt {
+    return 0;
+}
+```
+
+Instead of:
+```cairo
+// @pre x == 0
+// @post 0 == 1
+// @external
+// func f(x : felt) -> felt {
+//     return 0;
+// }
+```
+
+Try:
+```cairo
+/// // @pre x == 0
+/// // @post 0 == 1
+/// @external
+/// func f(x : felt) -> felt {
+///     return 0;
+}
+```
+
 
 ## Usage
 
@@ -1478,6 +1517,89 @@ Apart from `GlobalL`, there are several other sub-DSLs, which include:
   for a given module.
 * `PreprocessorL` -- preprocesses and runs SMT queries.
 
+### `CairoSemanticsL`
+
+As mentioned above, the purpose of the `CairoSemanticsL` eDSL is to construct
+the set of constraints which we will eventually transform into a solver query.
+
+At the time of writing, this is represented in a record type called
+`ConstraintsState`, which looks like this:
+
+```haskell
+data ConstraintsState = ConstraintsState
+  { cs_memoryVariables :: [MemoryVariable]
+  , cs_asserts :: [(AssertionBuilder, AssertionType)]
+  , cs_expects :: [(Expr TBool, AssertionType)]
+  , cs_nameCounter :: Int
+  , cs_callStack :: CallStack
+  }
+```
+
+So the asserts and expects are basically boolean expressions, and the
+preconditions and postconditions are encoded here. We have a list of memory
+variables as well. A memory variable is defined as follows:
+
+```haskell
+data MemoryVariable = MemoryVariable
+  { mv_varName :: Text
+  , mv_addrName :: Text
+  , mv_addrExpr :: Expr TFelt
+  }
+  deriving (Show)
+```
+
+We have a variable name, an address name, and an address expression, which
+is a felt. This is just an association between some variable name and an
+address in memory, along with its contents.
+
+When we print a memory variable, we see something like this:
+```console
+MEM!27 : (ap!<112=addr/root>@5 + 35)
+```
+The `27` in `MEM!27` is just a way to identify distinct memory variables. The
+`ap` stands for [allocation
+pointer](https://starknet.io/docs/how_cairo_works/cairo_intro.html#registers),
+and this indicates that this is the address in memory of some felt pushed on to
+the stack within a function body. The `@5` indicates the AP tracking group of
+this memory variable. The `+ 35` is the offset, specifically the offset from
+the beginning of the function context. Thus, an offset of `+ 0` indicates the
+first thing pushed onto the memory stack within that context.
+
+Here's an example:
+```cairo
+func foo:
+  [ap] = 0, ap++;  // <- this will be <foo/root>@x + 0
+  [ap] = 42, ap++; // <- this will be <foo/root>@x + 1
+  call bar;        // <- ^ now we're fp<bar/foo/root> + 0 and e.g. fp<bar/foo/root< - 3 = <foo/root>@x + 1 (remember call pushes 2 things on the stack)
+```
+
+The stuff in angle brackets, `<112=addr/root>`, is the current execution
+context, i.e. the stack frame. Each function call gets its own stack frame. The
+`addr/root` part is a representation of the call stack itself, where `root` is
+the execution context of top-level functions and subsequent stack frames are
+prepended, delimited with a `/`. The `112` is the program counter value, which
+tells us the instruction at which the current function was invoked.
+
+For example, consider:
+```cairo
+func foo [inlinable]             		root
+func bar [inlinable]
+
+func baz:
+  call bar -- inlining, push bar -> bar/root
+    ... (body of bar)
+    ret                 pop      -> root
+  ...
+  call foo -- inlining, push foo -> foo/root
+    ... (body of foo)
+    ret                 pop      -> root
+  ...
+```
+
+The stuff in the right-hand column is the context we're executing within. So
+when you refer to memory cells that have `<foo/root>`, you're referring to them
+from within the inlined function `foo`.
+
 ### Glossary
 
 * **contract** - a Starknet smart contract.
diff --git a/horus-check.cabal b/horus-check.cabal
index 86b33512..ed0bdaa7 100644
--- a/horus-check.cabal
+++ b/horus-check.cabal
@@ -85,6 +85,7 @@ library
       Horus.Preprocessor
       Horus.Preprocessor.Runner
       Horus.Preprocessor.Solvers
+      Horus.SMTHygiene
       Horus.SW.Builtin
       Horus.SW.CairoType
       Horus.SW.CairoType.JSON
diff --git a/src/Horus/CFGBuild.hs b/src/Horus/CFGBuild.hs
index 4899a61c..49317aa6 100644
--- a/src/Horus/CFGBuild.hs
+++ b/src/Horus/CFGBuild.hs
@@ -13,6 +13,7 @@ module Horus.CFGBuild
   , mkInv
   , Vertex (..)
   , getVerts
+  , isOptimising
   , isPreCheckingVertex
   )
 where
@@ -81,6 +82,9 @@ data Vertex = Vertex
   }
   deriving (Show)
 
+isOptimising :: Vertex -> Bool
+isOptimising = isJust . v_preCheckedF
+
 instance Eq Vertex where
   (==) lhs rhs = v_name lhs == v_name rhs
 
@@ -273,7 +277,7 @@ addArcsFrom inlinables prog rows seg@(Segment s) vFrom
     -- in which Pre(G) is assumed to hold at the PC of the G call site, as it will have
     -- been checked by the module induced by the ghost vertex.
     ghostV <- addOptimisingVertex (nextSegmentLabel seg) callee
-    pre <- maybe (mkPre Expr.True) mkPre . fs'_pre <$> getFuncSpec callee
+    pre <- maybe (mkPre Expr.True) (mkPre . fst) . fs'_pre <$> getFuncSpec callee
 
     -- Important note on the way we deal with logical variables. These are @declare-d and
     -- their values can be bound in preconditions. They generate existentials which only occur
@@ -333,7 +337,7 @@ addAssertions inlinables identifiers = do
               (Nothing, Nothing) ->
                 when (fu_pc f `Set.notMember` Set.map sf_pc inlinables) $
                   for_ retVs (`addAssertion` mkPost Expr.True)
-              _ -> for_ retVs (`addAssertion` maybe (mkPost Expr.True) mkPost post)
+              _ -> for_ retVs (`addAssertion` maybe (mkPost Expr.True) (mkPost . fst) post)
     ILabel pc ->
       whenJustM (getInvariant idName) $ \inv ->
         getSalientVertex pc >>= (`addAssertion` mkInv inv)
diff --git a/src/Horus/CairoSemantics.hs b/src/Horus/CairoSemantics.hs
index a3f58856..de8fcf37 100644
--- a/src/Horus/CairoSemantics.hs
+++ b/src/Horus/CairoSemantics.hs
@@ -41,7 +41,7 @@ import Horus.Expr.Vars
   , pattern StorageVar
   )
 import Horus.Expr.Vars qualified as Vars
-import Horus.FunctionAnalysis (ScopedFunction (sf_pc))
+import Horus.FunctionAnalysis (ScopedFunction (sf_pc, sf_scopedName))
 import Horus.Instruction
   ( ApUpdate (..)
   , Instruction (..)
@@ -53,18 +53,20 @@ import Horus.Instruction
   , getNextPcInlinedWithFallback
   , isCall
   , isRet
+  , toSemiAsmUnsafe
   , uncheckedCallDestination
   )
 import Horus.Label (Label (..), tShowLabel)
 import Horus.Module (Module (..), apEqualsFp, isPreChecking)
 import Horus.Program (ApTracking (..))
+import Horus.SMTHygiene (AssertionMisc, commentAbove, commentBelow, commentRight, emptyMisc, magicHygieneConstant)
 import Horus.SW.Builtin (Builtin, BuiltinOffsets (..))
 import Horus.SW.Builtin qualified as Builtin (name)
 import Horus.SW.FuncSpec (FuncSpec (..), FuncSpec', toFuncSpec)
 import Horus.SW.ScopedName (ScopedName)
 import Horus.SW.ScopedName qualified as ScopedName (fromText)
 import Horus.SW.Storage (Storage)
-import Horus.SW.Storage qualified as Storage (equivalenceExpr)
+import Horus.SW.Storage qualified as Storage
 import Horus.Util (enumerate, safeLast, tShow, whenJust, whenJustM)
 
 data MemoryVariable = MemoryVariable
@@ -78,10 +80,11 @@ data AssertionType
   = PreAssertion
   | PostAssertion
   | InstructionSemanticsAssertion
+  | ApConstraintAssertion
   deriving (Eq, Show)
 
 data CairoSemanticsF a
-  = Assert' (Expr TBool) AssertionType a
+  = Assert' (Expr TBool) AssertionType AssertionMisc a
   | Expect' (Expr TBool) AssertionType a
   | DeclareMem (Expr TFelt) (Expr TFelt -> a)
   | DeclareLocalMem (Expr TFelt) (MemoryVariable -> a)
@@ -89,6 +92,7 @@ data CairoSemanticsF a
   | GetBuiltinOffsets Label Builtin (Maybe BuiltinOffsets -> a)
   | GetCallee LabeledInst (ScopedFunction -> a)
   | GetFuncSpec ScopedFunction (FuncSpec' -> a)
+  | GetCurrentF (ScopedFunction -> a)
   | GetFunPc Label (Label -> a)
   | GetInlinable (Set.Set ScopedFunction -> a)
   | GetMemVars ([MemoryVariable] -> a)
@@ -109,8 +113,8 @@ deriving instance Functor CairoSemanticsF
 
 type CairoSemanticsL = F CairoSemanticsF
 
-assert' :: AssertionType -> Expr TBool -> CairoSemanticsL ()
-assert' assType a = liftF (Assert' a assType ())
+assert' :: AssertionType -> AssertionMisc -> Expr TBool -> CairoSemanticsL ()
+assert' assType misc a = liftF (Assert' a assType misc ())
 
 expect' :: Expr TBool -> CairoSemanticsL ()
 expect' a = liftF (Expect' a PostAssertion ())
@@ -127,6 +131,9 @@ getBuiltinOffsets l b = liftF (GetBuiltinOffsets l b id)
 getCallee :: LabeledInst -> CairoSemanticsL ScopedFunction
 getCallee call = liftF (GetCallee call id)
 
+getCurrentF :: CairoSemanticsL ScopedFunction
+getCurrentF = liftF (GetCurrentF id)
+
 getFuncSpec :: ScopedFunction -> CairoSemanticsL FuncSpec'
 getFuncSpec name = liftF (GetFuncSpec name id)
 
@@ -162,10 +169,27 @@ getStorage :: CairoSemanticsL Storage
 getStorage = liftF (GetStorage id)
 
 assert :: Expr TBool -> CairoSemanticsL ()
-assert a = assert' InstructionSemanticsAssertion =<< memoryRemoval a
+assert a = assert' InstructionSemanticsAssertion emptyMisc =<< memoryRemoval a
+
+_assertWithComment :: Expr TBool -> Text -> CairoSemanticsL ()
+_assertWithComment a text =
+  assert' InstructionSemanticsAssertion (commentRight text emptyMisc) =<< memoryRemoval a
+
+assertWithComment' :: Expr TBool -> AssertionMisc -> CairoSemanticsL ()
+assertWithComment' a misc =
+  assert' InstructionSemanticsAssertion misc =<< memoryRemoval a
+
+_assertPre :: Expr TBool -> CairoSemanticsL ()
+_assertPre = assertPreWithComment' emptyMisc
 
-assertPre :: Expr TBool -> CairoSemanticsL ()
-assertPre a = assert' PreAssertion =<< memoryRemoval a
+commentHere' :: Text -> CairoSemanticsL ()
+commentHere' = assertWithComment' magicHygieneConstant . flip commentRight emptyMisc
+
+assertApConstraint :: Expr TBool -> CairoSemanticsL ()
+assertApConstraint a = assert' ApConstraintAssertion emptyMisc =<< memoryRemoval a
+
+assertPreWithComment' :: AssertionMisc -> Expr TBool -> CairoSemanticsL ()
+assertPreWithComment' misc a = assert' PreAssertion misc =<< memoryRemoval a
 
 expect :: Expr TBool -> CairoSemanticsL ()
 expect a = expect' =<< memoryRemoval a
@@ -289,7 +313,7 @@ moduleEndAp mdl =
  contain a storage update.
 -}
 encodeModule :: Module -> CairoSemanticsL ()
-encodeModule mdl@(Module (FuncSpec pre post storage) instrs oracle _ _ mbPreCheckedFuncWithCallStack) = do
+encodeModule mdl@(Module (FuncSpec (pre, preDesc) (post, _) storage) instrs oracle _ _ mbPreCheckedFuncWithCallStack) = do
   enableStorage
   fp <- getFp
   apEnd <- moduleEndAp mdl
@@ -297,7 +321,9 @@ encodeModule mdl@(Module (FuncSpec pre post storage) instrs oracle _ _ mbPreChec
 
   apStart <- moduleStartAp mdl
   assert (fp .<= apStart)
-  assertPre =<< prepare' apStart fp (pre .&& apEqualsFp)
+  assertPreWithComment' (commentAbove ("Module pre: " <> preDesc) emptyMisc)
+    =<< prepare' apStart fp (pre .&& apEqualsFp)
+
   -- The last FP might be influenced in the optimizing case, we need to grab it as propagated
   -- by the encoding of the semantics of the call.
   lastFp <-
@@ -406,19 +432,23 @@ mkInstructionConstraints ::
   Map (NonEmpty Label, Label) Bool ->
   (Int, LabeledInst) ->
   CairoSemanticsL (Maybe (Expr TFelt))
-mkInstructionConstraints instrs mbPreCheckedFuncWithCallStack jnzOracle (idx, lInst@(pc, Instruction{..})) = do
+mkInstructionConstraints instrs mbPreCheckedFuncWithCallStack jnzOracle (idx, lInst@(pc, inst@Instruction{..})) = do
   fp <- getFp
   dst <- prepare pc fp (memory (regToVar i_dstRegister + fromInteger i_dstOffset))
   case i_opCode of
     Call -> mkCallConstraints pc nextPc fp mbPreCheckedFuncWithCallStack =<< getCallee lInst
-    AssertEqual -> getRes fp lInst >>= \res -> assert (res .== dst) $> Nothing
+    AssertEqual ->
+      getRes fp lInst >>= \res ->
+        assertWithComment' (res .== dst) (commentRight (toSemiAsmUnsafe inst) emptyMisc) $> Nothing
     Nop -> do
       stackTrace <- getOracle
       case jnzOracle Map.!? (stackTrace, pc) of
         Just False -> assert (dst .== 0) $> Nothing
         Just True -> assert (dst ./= 0) $> Nothing
         Nothing -> pure Nothing
-    Ret -> pop $> Nothing
+    Ret -> do
+      currentF <- getCurrentF
+      commentHere' ("Inlining ended: " <> tShow (sf_scopedName currentF)) >> pop $> Nothing
  where
   nextPc = getNextPcInlinedWithFallback instrs idx
 
@@ -435,7 +465,10 @@ mkCallConstraints pc nextPc fp mbPreCheckedFuncWithCallStack f = do
   nextAp <- prepare pc calleeFp (Vars.fp .== Vars.ap + 2)
   saveOldFp <- prepare pc fp (memory Vars.ap .== Vars.fp)
   setNextPc <- prepare pc fp (memory (Vars.ap + 1) .== fromIntegral (unLabel nextPc))
-  assert (Expr.and [nextAp, saveOldFp, setNextPc])
+  canInline <- isInlinable f
+  assertWithComment'
+    (Expr.and [nextAp, saveOldFp, setNextPc])
+    (commentAbove (describeCall canInline <> tShow (sf_scopedName f)) emptyMisc)
   push stackFrame
   -- Considering we have already pushed the stackFrame by now, we need to make sure that either
   -- the function is inlinable and we'll encounter a 'ret', or we need to pop right away
@@ -448,7 +481,7 @@ mkCallConstraints pc nextPc fp mbPreCheckedFuncWithCallStack f = do
     -- of the function being invoked must not be considered.
     guardWith (isInlinable f) (pure Nothing) $ do
       -- An inlined function will have a 'ret' at some point, do not pop here.
-      (FuncSpec pre post storage) <- getFuncSpec f <&> toFuncSpec
+      (FuncSpec (pre, preDesc) (post, postDesc) storage) <- getFuncSpec f <&> toFuncSpec
       let pre' = suffixLogicalVariables lvarSuffix pre
           post' = suffixLogicalVariables lvarSuffix post
       preparedPre <- prepare nextPc calleeFp =<< storageRemoval pre'
@@ -462,13 +495,22 @@ mkCallConstraints pc nextPc fp mbPreCheckedFuncWithCallStack f = do
       -- However, pre will be checked in a separate 'optimising' module and we can therefore simply
       -- assert it holds here. If it does not, the corresponding pre-checking module will fail,
       -- thus failing the judgement for the entire function.
-      assert preparedPre
-      assert preparedPost
+      assertWithComment'
+        preparedPre
+        (commentAbove ("Pre of: " <> functionName <> " | " <> preDesc) emptyMisc)
+      assertWithComment'
+        preparedPost
+        ( commentBelow
+            ("Finished abstracting function: " <> functionName)
+            (commentAbove ("Post of: " <> functionName <> " | " <> postDesc) emptyMisc)
+        )
       pure Nothing
  where
   lvarSuffix = "+" <> tShowLabel pc
   calleePc = sf_pc f
   stackFrame = (pc, calleePc)
+  functionName = tShow (sf_scopedName f)
+  describeCall inl = if inl then "Inlining function: " else "Abstracting function: "
   -- Determine whether the current function matches the function being optimised exactly -
   -- this necessitates comparing execution traces.
   isModuleCheckingPre = do
@@ -498,15 +540,15 @@ mkApConstraints apEnd insts = do
       ap2 <- getAp pcNext
       fp <- getFp
       getApIncrement fp lInst >>= \case
-        Just apIncrement -> assert (ap1 + apIncrement .== ap2)
-        Nothing | not isNewStackframe -> assert (ap1 .< ap2)
+        Just apIncrement -> assertApConstraint (ap1 + apIncrement .== ap2)
+        Nothing | not isNewStackframe -> assertApConstraint (ap1 .< ap2)
         Nothing -> pure ()
   lastAp <- getAp lastPc
   when (isRet lastInst) pop
   fp <- getFp
   getApIncrement fp lastLInst >>= \case
-    Just lastApIncrement -> assert (lastAp + lastApIncrement .== apEnd)
-    Nothing -> assert (lastAp .< apEnd)
+    Just lastApIncrement -> assertApConstraint (lastAp + lastApIncrement .== apEnd)
+    Nothing -> assertApConstraint (lastAp .< apEnd)
  where
   lastLInst@(lastPc, lastInst) = NonEmpty.last insts
 
diff --git a/src/Horus/CairoSemantics/Runner.hs b/src/Horus/CairoSemantics/Runner.hs
index 6ed768a8..c5578c8d 100644
--- a/src/Horus/CairoSemantics/Runner.hs
+++ b/src/Horus/CairoSemantics/Runner.hs
@@ -16,22 +16,23 @@ import Control.Monad.Reader
   , asks
   , runReaderT
   )
-import Control.Monad.State (MonadState (get), State, runState)
+import Control.Monad.State (MonadState (get), State, gets, runState)
 import Data.Foldable (toList)
 import Data.Function ((&))
 import Data.Functor (($>))
+import Data.List (partition)
 import Data.List qualified as List (find, tails)
-import Data.Map qualified as Map (map, null, unionWith)
+import Data.Map qualified as Map
 import Data.Maybe (mapMaybe)
 import Data.Singletons (sing)
 import Data.Some (foldSome)
 import Data.Text (Text)
 import Data.Text qualified as Text (intercalate)
-import Lens.Micro (Lens', (%~), (<&>), (^.))
+import Lens.Micro (Lens', (%~), (<&>), (^.), _1, _2)
 import Lens.Micro.GHC ()
 import Lens.Micro.Mtl (use, (%=), (.=), (<%=))
 
-import Horus.CairoSemantics (AssertionType (PreAssertion), CairoSemanticsF (..), CairoSemanticsL, MemoryVariable (..))
+import Horus.CairoSemantics (AssertionType (ApConstraintAssertion, PreAssertion), CairoSemanticsF (..), CairoSemanticsL, MemoryVariable (..))
 import Horus.CallStack (CallStack, digestOfCallStack, pop, push, reset, stackTrace, top)
 import Horus.Command.SMT qualified as Command
 import Horus.ContractInfo (ContractInfo (..))
@@ -43,6 +44,7 @@ import Horus.Expr.Type (STy (..))
 import Horus.Expr.Util (gatherNonStdFunctions)
 import Horus.Expr.Vars (prime, rcBound)
 import Horus.FunctionAnalysis (ScopedFunction (sf_scopedName))
+import Horus.SMTHygiene (AssertionMisc, commentBelow, encodeRestriction, withEmptyMisc)
 import Horus.SW.Builtin qualified as Builtin (rcBound)
 import Horus.SW.Storage (Storage)
 import Horus.SW.Storage qualified as Storage (read)
@@ -61,7 +63,7 @@ builderToAss mv (ExistentialAss f) = f mv
 -- inlined.
 data ConstraintsState = ConstraintsState
   { cs_memoryVariables :: [MemoryVariable]
-  , cs_asserts :: [(AssertionBuilder, AssertionType)]
+  , cs_asserts :: [(AssertionBuilder, AssertionType, AssertionMisc)]
   , cs_expects :: [(Expr TBool, AssertionType)]
   , cs_nameCounter :: Int
   , cs_callStack :: CallStack
@@ -70,7 +72,7 @@ data ConstraintsState = ConstraintsState
 csMemoryVariables :: Lens' ConstraintsState [MemoryVariable]
 csMemoryVariables lMod g = fmap (\x -> g{cs_memoryVariables = x}) (lMod (cs_memoryVariables g))
 
-csAsserts :: Lens' ConstraintsState [(AssertionBuilder, AssertionType)]
+csAsserts :: Lens' ConstraintsState [(AssertionBuilder, AssertionType, AssertionMisc)]
 csAsserts lMod g = fmap (\x -> g{cs_asserts = x}) (lMod (cs_asserts g))
 
 csExpects :: Lens' ConstraintsState [(Expr TBool, AssertionType)]
@@ -121,7 +123,7 @@ interpret :: forall a. CairoSemanticsL a -> Impl a
 interpret = iterM exec
  where
   exec :: CairoSemanticsF (Impl a) -> Impl a
-  exec (Assert' a assType cont) = eConstraints . csAsserts %= ((QFAss a, assType) :) >> cont
+  exec (Assert' a assType misc cont) = eConstraints . csAsserts %= ((QFAss a, assType, misc) :) >> cont
   exec (Expect' a assType cont) = eConstraints . csExpects %= ((a, assType) :) >> cont
   exec (DeclareMem address cont) = do
     memVars <- use (eConstraints . csMemoryVariables)
@@ -151,6 +153,10 @@ interpret = iterM exec
   exec (GetCallee inst cont) = do
     ci <- ask
     ci_getCallee ci inst >>= cont
+  exec (GetCurrentF cont) = do
+    (_, calledF) <- gets $ top . (^. csCallStack) . e_constraints
+    ci <- ask
+    cont (ci_functions ci Map.! calledF)
   exec (GetFuncSpec name cont) = do
     ci <- ask
     ci_getFuncSpec ci name & cont
@@ -200,9 +206,9 @@ debugFriendlyModel ConstraintsState{..} =
       [ ["# Memory"]
       , memoryPairs
       , ["# Assert"]
-      , map (pprExpr . builderToAss cs_memoryVariables . fst) cs_asserts
+      , map (pprExpr . builderToAss cs_memoryVariables . (^. _1)) cs_asserts
       , ["# Expect"]
-      , map (pprExpr . fst) cs_expects
+      , map (pprExpr . (^. _1)) cs_expects
       ]
  where
   memoryPairs =
@@ -222,10 +228,10 @@ restrictMemTail (mv0 : rest) =
 
 makeModel :: Bool -> ConstraintsState -> Integer -> Text
 makeModel checkPreOnly ConstraintsState{..} fPrime =
-  Text.intercalate "\n" (decls <> map (Command.assert fPrime) restrictions)
+  Text.intercalate "\n" (decls <> map (encodeRestriction fPrime) restrictions)
  where
   functions =
-    toList (foldMap gatherNonStdFunctions generalRestrictions <> gatherNonStdFunctions prime)
+    toList (foldMap (gatherNonStdFunctions . fst) generalRestrictions <> gatherNonStdFunctions prime)
   decls = map (foldSome Command.declare) functions
   rangeRestrictions = mapMaybe (foldSome restrictRange) functions
   memRestrictions = concatMap restrictMemTail (List.tails cs_memoryVariables)
@@ -233,17 +239,32 @@ makeModel checkPreOnly ConstraintsState{..} fPrime =
     [Expr.const mv_addrName .== mv_addrExpr | MemoryVariable{..} <- cs_memoryVariables]
 
   -- If checking @pre only, only take `PreAssertion`s, no postconditions.
-  allowedAsserts = if checkPreOnly then filter ((== PreAssertion) . snd) cs_asserts else cs_asserts
+  allowedAsserts = if checkPreOnly then filter ((== PreAssertion) . (^. _2)) cs_asserts else cs_asserts
   allowedExpects = if checkPreOnly then [] else cs_expects
 
+  allowedAssertsWithApRegion = delineateApAssertions allowedAsserts
+
   generalRestrictions =
     concat
-      [ memRestrictions
-      , addrRestrictions
-      , map (builderToAss cs_memoryVariables . fst) allowedAsserts
-      , [Expr.not (Expr.and (map fst allowedExpects)) | not (null allowedExpects)]
+      [ sansMiscInfo memRestrictions
+      , sansMiscInfo addrRestrictions
+      , [(builderToAss cs_memoryVariables builder, misc) | (builder, _, misc) <- allowedAssertsWithApRegion]
+      , sansMiscInfo [Expr.not (Expr.and (map (^. _1) allowedExpects)) | not (null allowedExpects)]
       ]
-  restrictions = rangeRestrictions <> generalRestrictions
+  restrictions = sansMiscInfo rangeRestrictions <> generalRestrictions
+
+  sansMiscInfo = map withEmptyMisc
+
+  delineateApAssertions asserts =
+    let (anteAp, postAp) = partition ((/= ApConstraintAssertion) . (^. _2)) asserts
+     in commentRegion anteAp "Begin AP constraints." ++ commentRegion postAp "End AP constraints."
+   where
+    commentRegion region msg =
+      if null region
+        then region
+        else
+          let (ass, assType, assMisc) = last region
+           in init region ++ [(ass, assType, commentBelow msg assMisc)]
 
   restrictRange :: forall ty. Function ty -> Maybe (Expr TBool)
   restrictRange (Function name) = case sing @ty of
diff --git a/src/Horus/Command/SMT.hs b/src/Horus/Command/SMT.hs
index 9da35af2..552be86c 100644
--- a/src/Horus/Command/SMT.hs
+++ b/src/Horus/Command/SMT.hs
@@ -1,7 +1,7 @@
-module Horus.Command.SMT (declare, assert) where
+module Horus.Command.SMT (declare, assert, comment) where
 
 import Data.List.NonEmpty (NonEmpty (..))
-import Data.Text (Text, pack)
+import Data.Text (Text, pack, unpack)
 import SimpleSMT qualified as SMT
 import Text.Printf (printf)
 
@@ -10,6 +10,7 @@ import Horus.Expr.SMT qualified as Expr (toSMT)
 import Horus.Expr.Std (Function (..))
 import Horus.Expr.Type (Ty (..))
 import Horus.Expr.Type.SMT qualified as Ty (toSMT)
+import SimpleSMT (SExpr (Atom))
 
 declare :: forall ty. Function ty -> Text
 declare (Function name) = pack (printf "(declare-fun %s (%s) %s)" name args res)
@@ -20,3 +21,6 @@ declare (Function name) = pack (printf "(declare-fun %s (%s) %s)" name args res)
 
 assert :: Integer -> Expr TBool -> Text
 assert fPrime e = pack (printf "(assert %s)" (SMT.showsSExpr (Expr.toSMT fPrime e) ""))
+
+comment :: Text -> Text
+comment text = pack (printf "; %s" (SMT.showsSExpr (Atom (unpack text)) ""))
diff --git a/src/Horus/Expr.hs b/src/Horus/Expr.hs
index da4e9599..cc935cf9 100644
--- a/src/Horus/Expr.hs
+++ b/src/Horus/Expr.hs
@@ -343,9 +343,7 @@ a .>= b = function ">=" a b
 
 infix 4 .==
 (.==) :: Expr TFelt -> Expr TFelt -> Expr TBool
-a .== b
-  | a == b = True
-  | otherwise = function "=" a b
+a .== b = function "=" a b
 
 infix 4 ./=
 (./=) :: Expr TFelt -> Expr TFelt -> Expr TBool
diff --git a/src/Horus/FunctionAnalysis.hs b/src/Horus/FunctionAnalysis.hs
index a283f2ee..b9ace7de 100644
--- a/src/Horus/FunctionAnalysis.hs
+++ b/src/Horus/FunctionAnalysis.hs
@@ -17,6 +17,9 @@ module Horus.FunctionAnalysis
   , isAuxFunc
   , scopedFOfPc
   , uncheckedScopedFOfPc
+  , functionsOf
+  , callgraph
+  , graphOfCG
   )
 where
 
@@ -25,7 +28,7 @@ import Control.Monad (liftM2, (<=<))
 import Data.Array (assocs)
 import Data.Coerce (coerce)
 import Data.Function ((&))
-import Data.Graph (Graph, Vertex, graphFromEdges', reachable)
+import Data.Graph (Graph, Vertex, graphFromEdges, reachable)
 import Data.List (foldl', sort, union)
 import Data.Map qualified as Map
   ( Map
@@ -109,8 +112,8 @@ cgMbInsertArc (CG verts arcs) (fro, to) =
     then Nothing
     else Just . CG verts $ Map.insertWith (++) fro [to] arcs
 
-graphOfCG :: CG -> (Graph, Vertex -> (Label, Label, [Label]))
-graphOfCG cg = graphFromEdges' . map named . Map.assocs $ cg_arcs cg
+graphOfCG :: CG -> (Graph, Vertex -> (Label, Label, [Label]), Label -> Maybe Vertex)
+graphOfCG cg = graphFromEdges . map named . Map.assocs $ cg_arcs cg
  where
   named (fro, tos) = (fro, fro, tos)
 
@@ -121,7 +124,7 @@ cycles g = map fst . filter (uncurry reachableSet) $ assocs g
 
 cyclicVerts :: CG -> [Label]
 cyclicVerts cg =
-  let (graph, vertToNode) = graphOfCG cg
+  let (graph, vertToNode, _) = graphOfCG cg
    in map ((\(lbl, _, _) -> lbl) . vertToNode) (cycles graph)
 
 pcToFunOfProg :: Program -> Map.Map Label ScopedFunction
@@ -243,6 +246,11 @@ isNotAnnotated cd = not . maybe False isAnnotated' . labelOfIdent
 wrapperScope :: Text
 wrapperScope = "__wrappers__"
 
+-- Identify decorator-generated wrapper functions.
+--
+-- If you write e.g. @extern, this means can be called externally, generates a
+-- wrapper function. We *don't* want to verify wrapper functions, so we want to
+-- be able to identify and exclude these.
 isWrapper :: ScopedFunction -> Bool
 isWrapper f = outerScope (sf_scopedName f) == wrapperScope
  where
@@ -271,18 +279,13 @@ isGeneratedName fname cd = fname `elem` generatedNames
 isSvarFunc :: ScopedName -> ContractDefinition -> Bool
 isSvarFunc fname cd = isGeneratedName fname cd || fname `elem` [fStorageRead, fStorageWrite]
 
-fHash2 :: ScopedName
-fHash2 = ScopedName ["starkware", "cairo", "common", "hash", "hash2"]
-
-fAssert250bit :: ScopedName
-fAssert250bit = ScopedName ["starkware", "cairo", "common", "math", "assert_250_bit"]
-
-fNormalizeAddress :: ScopedName
-fNormalizeAddress = ScopedName ["starkware", "starknet", "common", "storage", "normalize_address"]
-
 isAuxFunc :: ScopedFunction -> ContractDefinition -> Bool
 isAuxFunc (ScopedFunction fname _) cd =
   isSvarFunc fname cd || fname `elem` [fHash2, fAssert250bit, fNormalizeAddress]
+ where
+  fHash2 = ScopedName ["starkware", "cairo", "common", "hash", "hash2"]
+  fAssert250bit = ScopedName ["starkware", "cairo", "common", "math", "assert_250_bit"]
+  fNormalizeAddress = ScopedName ["starkware", "starknet", "common", "storage", "normalize_address"]
 
 sizeOfCall :: Int
 sizeOfCall = 2
@@ -302,11 +305,15 @@ inlinableFuns rows prog cd =
   idents = p_identifiers prog
   functions = functionsOf rows prog
   notIsAnnotated sf = maybe False (isNotAnnotated cd) . Map.lookup (sf_scopedName sf) $ idents
+
+  -- Annotated *later* by horus-checker because they come from e.g. the
+  -- standard library. These are things with default specs.
   notIsAnnotatedLater f = sf_scopedName f `notElem` map fst stdSpecsList
   localCycles = Map.map (cyclicVerts . jumpgraph)
-  isAcylic cyclicFuns f cyclicLbls = f `notElem` cyclicFuns && null cyclicLbls
+  isAcyclic cyclicFuns f cyclicLbls = f `notElem` cyclicFuns && null cyclicLbls
+  -- The functions that contain neither global nor local cycles.
   inlinable =
-    Map.keys . Map.filterWithKey (isAcylic . cyclicVerts $ callgraph (Map.mapKeys sf_pc functions)) $
+    Map.keys . Map.filterWithKey (isAcyclic . cyclicVerts $ callgraph (Map.mapKeys sf_pc functions)) $
       Map.mapKeys sf_pc (localCycles functions)
 
 uninlinableFuns :: [LabeledInst] -> Program -> ContractDefinition -> Map.Map ScopedFunction [LabeledInst]
diff --git a/src/Horus/Global.hs b/src/Horus/Global.hs
index d902ec10..d65df13f 100644
--- a/src/Horus/Global.hs
+++ b/src/Horus/Global.hs
@@ -16,10 +16,12 @@ import Control.Monad (when)
 import Control.Monad.Except (MonadError (..))
 import Control.Monad.Free.Church (F, liftF)
 import Data.Foldable (for_)
-import Data.List (groupBy)
-import Data.Maybe (fromMaybe)
+import Data.Graph (reachable)
+import Data.List (groupBy, partition)
+import Data.Map qualified as Map
+import Data.Maybe (fromJust, fromMaybe)
 import Data.Set (Set, singleton, toAscList, (\\))
-import Data.Set qualified as Set (map)
+import Data.Set qualified as Set (fromList, map, member)
 import Data.Text (Text, unpack)
 import Data.Text qualified as Text (isPrefixOf)
 import Data.Traversable (for)
@@ -37,7 +39,7 @@ import Horus.CairoSemantics.Runner
 import Horus.CallStack (CallStack, initialWithFunc)
 import Horus.Expr qualified as Expr
 import Horus.Expr.Util (gatherLogicalVariables)
-import Horus.FunctionAnalysis (ScopedFunction (ScopedFunction, sf_pc), isWrapper)
+import Horus.FunctionAnalysis (ScopedFunction (ScopedFunction, sf_pc), callgraph, functionsOf, graphOfCG, isWrapper)
 import Horus.Logger qualified as L (LogL, logDebug, logError, logInfo, logWarning)
 import Horus.Module (Module (..), ModuleL, gatherModules, getModuleNameParts)
 import Horus.Preprocessor (HorusResult (..), PreprocessorL, SolverResult (..), goalListToTextList, optimizeQuery, solve)
@@ -49,6 +51,7 @@ import Horus.SW.Identifier (Function (..))
 import Horus.SW.ScopedName (ScopedName ())
 import Horus.SW.Std (trustedStdFuncs)
 import Horus.Util (tShow, whenJust)
+import Lens.Micro ((^.), _3)
 
 data Config = Config
   { cfg_verbose :: Bool
@@ -271,7 +274,7 @@ removeMathSAT m run = do
   instUsesLvars i = falseIfError $ do
     callee <- getCallee i
     spec <- getFuncSpec callee
-    let lvars = gatherLogicalVariables (fromMaybe Expr.True (fs'_pre spec))
+    let lvars = gatherLogicalVariables . fst $ fromMaybe (Expr.True, "True") (fs'_pre spec)
     pure (not (null lvars))
 
   falseIfError a = a `catchError` const (pure False)
@@ -329,6 +332,7 @@ collapseAllUnsats infos@(SolvingInfo _ funcName result _ _ : _)
 
 {- | Return a solution of SMT queries corresponding with the contract.
 
+
   For the purposes of reporting results,
   we also remember which SMT query corresponding to a function was inlined.
 -}
@@ -336,6 +340,10 @@ solveContract :: GlobalL [SolvingInfo]
 solveContract = do
   lInstructions <- getLabelledInstructions
   inlinables <- getInlinables
+  -- We take a function that was inlined away, pretend it is *not* inlinable,
+  -- since want to do analysis on it in isolation, which we must do for every
+  -- function. And we do this because we want a judgement for each so that we
+  -- don't propagate errors upward when we inline stuff.
   cfg <- runCFGBuildL $ buildCFG lInstructions inlinables
   verbosePrint cfg
 
@@ -343,7 +351,8 @@ solveContract = do
   let fs = toAscList inlinables
   cfgs <- for fs $ \f -> runCFGBuildL (buildCFG lInstructions $ inlinables \\ singleton f)
   for_ cfgs verbosePrint
-  modules <- concat <$> for ((cfg, isStandardSource inlinables) : zip cfgs (map (==) fs)) makeModules
+  sources <- userAnnotatedSources inlinables lInstructions
+  modules <- concat <$> for ((cfg, (`elem` sources)) : zip cfgs (map (==) fs)) makeModules
 
   identifiers <- getIdentifiers
   let isUntrusted :: Module -> Bool
@@ -359,8 +368,22 @@ solveContract = do
     )
       infos
  where
-  isStandardSource :: Set ScopedFunction -> ScopedFunction -> Bool
-  isStandardSource inlinables f = f `notElem` inlinables && not (isWrapper f)
+  userAnnotatedSources :: Set ScopedFunction -> [LabeledInst] -> GlobalL (Set ScopedFunction)
+  userAnnotatedSources inlinableFs rows =
+    getProgram >>= \prog ->
+      let functionsWithBodies = functionsOf rows prog
+          functions = Map.keys functionsWithBodies
+          (cg, vToLbl, lblToV) = graphOfCG . callgraph . Map.mapKeys sf_pc $ functionsWithBodies
+          (wrapperFunctions, nonwrapperFunctions) = partition isWrapper functions
+          reachableLabelsFromWrappers =
+            Set.fromList
+              . concatMap (concatMap ((^. _3) . vToLbl) . reachable cg . fromJust . lblToV . sf_pc)
+              $ wrapperFunctions
+          calledByWrappers =
+            Set.fromList
+              [ sf | sf <- functions, sf_pc sf `Set.member` reachableLabelsFromWrappers
+              ]
+       in pure (Set.fromList nonwrapperFunctions \\ inlinableFs \\ calledByWrappers)
 
   sameFuncName :: SolvingInfo -> SolvingInfo -> Bool
   sameFuncName (SolvingInfo _ nameA _ _ _) (SolvingInfo _ nameB _ _ _) = nameA == nameB
diff --git a/src/Horus/Instruction.hs b/src/Horus/Instruction.hs
index 973f8fb8..1273c2f9 100644
--- a/src/Horus/Instruction.hs
+++ b/src/Horus/Instruction.hs
@@ -245,7 +245,7 @@ toSemiAsm Instruction{..} = do
   withRes f = fmap f getRes
   dst = mem (printReg i_dstRegister `add` i_dstOffset)
   mbApPP = case i_apUpdate of
-    Add1 -> "; ap++"
+    Add1 -> ", ap++"
     _ -> ""
   getRes = case i_resLogic of
     Op1 -> pure op1
diff --git a/src/Horus/JSON/Util.hs b/src/Horus/JSON/Util.hs
index e21b1550..7e9f003b 100644
--- a/src/Horus/JSON/Util.hs
+++ b/src/Horus/JSON/Util.hs
@@ -31,5 +31,5 @@ instance Typeable a => FromJSON (HSourcedSExpr a) where
     HSourcedSExpr
       <$> do
         sourceLst <- v .: "source"
-        pure $ Text.intercalate "\n" sourceLst
+        pure $ Text.intercalate " | " sourceLst
       <*> v .: "sexpr"
diff --git a/src/Horus/Module.hs b/src/Horus/Module.hs
index 900463c9..fab39bba 100644
--- a/src/Horus/Module.hs
+++ b/src/Horus/Module.hs
@@ -189,7 +189,7 @@ descrOfOracle oracle =
 getModuleNameParts :: Identifiers -> Module -> (Text, Text, Text, Text)
 getModuleNameParts idents (Module spec prog oracle calledF _ mbPreCheckedFuncAndCallStack) =
   case beginOfModule prog of
-    Nothing -> ("", "empty: " <> pprExpr post, "", "")
+    Nothing -> ("", "empty: " <> pprExpr (fst post), "", "")
     Just label ->
       let scopedNames = labelNamesOfPc idents label
           isFloatingLabel = label /= calledF
@@ -248,12 +248,12 @@ throw t = liftF' (Throw t)
 catch :: ModuleL a -> (Error -> ModuleL a) -> ModuleL a
 catch m h = liftF' (Catch m h id)
 
-data SpecBuilder = SBRich | SBPlain (Expr TBool)
+data SpecBuilder = SBRich | SBPlain (Expr TBool, Text)
 
 extractPlainBuilder :: FuncSpec -> ModuleL SpecBuilder
-extractPlainBuilder (FuncSpec pre _ storage)
+extractPlainBuilder (FuncSpec (pre, preDesc) _ storage)
   | not (null storage) = throwError EInvariantWithSVarUpdateSpec
-  | otherwise = pure (SBPlain (pre .&& (ap .== fp)))
+  | otherwise = pure (SBPlain (pre .&& (ap .== fp), preDesc))
 
 gatherModules :: CFG -> [(Function, ScopedName, FuncSpec)] -> ModuleL ()
 gatherModules cfg = traverse_ $ \(f, _, spec) -> gatherFromSource cfg f spec
@@ -323,18 +323,18 @@ visit cfg fSpec function oracle callstack acc builder v@(Vertex _ label preCheck
   visitLoop SBRich = extractPlainBuilder fSpec >>= visitLoop
   visitLoop (SBPlain pre)
     | null assertions = throwError (ELoopNoInvariant label)
-    | otherwise = emit pre (Expr.and assertions)
+    | otherwise = emit pre (Expr.and assertions, "")
 
   visitLinear :: SpecBuilder -> ModuleL ()
   visitLinear SBRich
-    | onFinalNode = emit (fs_pre fSpec) (Expr.and $ map snd (cfg_assertions cfg ^. ix v))
+    | onFinalNode = emit (fs_pre fSpec) (Expr.and $ map snd (cfg_assertions cfg ^. ix v), "")
     | null assertions = visitArcs cfg fSpec function callstack' oracle' acc builder v
     | otherwise = extractPlainBuilder fSpec >>= visitLinear
   visitLinear (SBPlain pre)
     | null assertions = visitArcs cfg fSpec function callstack' oracle' acc builder v
     | otherwise = do
-        emit pre (Expr.and assertions)
-        visitArcs cfg fSpec function callstack' Map.empty [] (SBPlain (Expr.and assertions)) v
+        emit pre (Expr.and assertions, "")
+        visitArcs cfg fSpec function callstack' Map.empty [] (SBPlain (Expr.and assertions, "")) v
 
   callstack' = case f of
     Nothing -> callstack
@@ -349,7 +349,7 @@ visit cfg fSpec function oracle callstack acc builder v@(Vertex _ label preCheck
   preCheckingStackFrame = (fCallerPc, uncheckedCallDestination labelledCall)
   preCheckingContext = (push preCheckingStackFrame callstack',) <$> preCheckedF
 
-  emit :: Expr TBool -> Expr TBool -> ModuleL ()
+  emit :: (Expr TBool, Text) -> (Expr TBool, Text) -> ModuleL ()
   emit pre post = emitModule (Module spec acc oracle' pc (callstack', label) preCheckingContext)
    where
     pc = fu_pc function
diff --git a/src/Horus/SMTHygiene.hs b/src/Horus/SMTHygiene.hs
new file mode 100644
index 00000000..e505817e
--- /dev/null
+++ b/src/Horus/SMTHygiene.hs
@@ -0,0 +1,54 @@
+module Horus.SMTHygiene
+  ( AssertionMisc (..)
+  , emptyMisc
+  , commentAbove
+  , commentBelow
+  , commentRight
+  , encodeRestriction
+  , withEmptyMisc
+  , magicHygieneConstant
+  )
+where
+
+import Data.Text (Text, intercalate)
+import Horus.Command.SMT qualified as Command
+import Horus.Expr
+
+data AssertionMisc = AssertionMisc
+  { am_textAbove :: [Text]
+  , am_textBelow :: [Text]
+  , am_textRight :: [Text]
+  }
+
+emptyMisc :: AssertionMisc
+emptyMisc = AssertionMisc [] [] []
+
+withEmptyMisc :: Expr a -> (Expr a, AssertionMisc)
+withEmptyMisc = (,emptyMisc)
+
+commentAbove :: Text -> AssertionMisc -> AssertionMisc
+commentAbove comment am = am{am_textAbove = am_textAbove am ++ [comment]}
+
+commentBelow :: Text -> AssertionMisc -> AssertionMisc
+commentBelow comment am = am{am_textBelow = am_textBelow am ++ [comment]}
+
+commentRight :: Text -> AssertionMisc -> AssertionMisc
+commentRight comment am = am{am_textRight = am_textRight am ++ [comment]}
+
+-- We need a unique-enough Expr.True to identify assertions that only exists to carry comments
+magicHygieneConstant :: Expr TBool
+magicHygieneConstant = 24601 .== 24601
+
+encodeRestriction :: Integer -> (Expr TBool, AssertionMisc) -> Text
+encodeRestriction prime (expr, AssertionMisc{..}) =
+  indentGroup (map Command.comment am_textAbove)
+    <> indentNewlinePretty am_textAbove
+    <> assertNotMagic expr
+    <> indentNear (map Command.comment am_textRight)
+    <> indentNewlinePretty am_textBelow
+    <> indentGroup (map Command.comment am_textBelow)
+ where
+  indentGroup = intercalate "\n"
+  indentNear = intercalate " | "
+  indentNewlinePretty comments = if null comments then "" else "\n"
+  assertNotMagic e = if e == magicHygieneConstant then "" else Command.assert prime expr
diff --git a/src/Horus/SW/FuncSpec.hs b/src/Horus/SW/FuncSpec.hs
index 7a64c5ca..b1169fa1 100644
--- a/src/Horus/SW/FuncSpec.hs
+++ b/src/Horus/SW/FuncSpec.hs
@@ -3,6 +3,7 @@ module Horus.SW.FuncSpec (FuncSpec (..), emptyFuncSpec, emptyFuncSpec', FuncSpec
 import Data.Aeson (FromJSON (..), withObject, (.:))
 import Data.Coerce (coerce)
 import Data.Maybe (fromMaybe)
+import Data.Text (Text)
 
 import Horus.Expr (Expr, Ty (..))
 import Horus.Expr qualified as Expr
@@ -11,14 +12,19 @@ import Horus.SW.Storage (Storage)
 import Horus.SW.Storage qualified as Storage (parse)
 
 data FuncSpec = FuncSpec
-  { fs_pre :: Expr TBool
-  , fs_post :: Expr TBool
+  { fs_pre :: (Expr TBool, Text)
+  , fs_post :: (Expr TBool, Text)
   , fs_storage :: Storage
   }
   deriving stock (Show)
 
 emptyFuncSpec :: FuncSpec
-emptyFuncSpec = FuncSpec{fs_pre = Expr.True, fs_post = Expr.True, fs_storage = mempty}
+emptyFuncSpec =
+  FuncSpec
+    { fs_pre = (Expr.True, "True")
+    , fs_post = (Expr.True, "True")
+    , fs_storage = mempty
+    }
 
 {- | A version of `FuncSpec` that distinguishes omitted preconditions and
  postconditions from trivial ones.
@@ -28,8 +34,8 @@ emptyFuncSpec = FuncSpec{fs_pre = Expr.True, fs_post = Expr.True, fs_storage = m
  `Nothing`.
 -}
 data FuncSpec' = FuncSpec'
-  { fs'_pre :: Maybe (Expr TBool)
-  , fs'_post :: Maybe (Expr TBool)
+  { fs'_pre :: Maybe (Expr TBool, Text)
+  , fs'_post :: Maybe (Expr TBool, Text)
   , fs'_storage :: Storage
   }
 
@@ -39,17 +45,20 @@ emptyFuncSpec' = FuncSpec'{fs'_pre = Nothing, fs'_post = Nothing, fs'_storage =
 toFuncSpec :: FuncSpec' -> FuncSpec
 toFuncSpec FuncSpec'{..} =
   FuncSpec
-    { fs_pre = fromMaybe Expr.True fs'_pre
-    , fs_post = fromMaybe Expr.True fs'_post
+    { fs_pre = fromMaybe (Expr.True, "True") fs'_pre
+    , fs_post = fromMaybe (Expr.True, "True") fs'_post
     , fs_storage = fs'_storage
     }
 
 instance FromJSON FuncSpec where
   parseJSON = withObject "FuncSpec" $ \v ->
     FuncSpec
-      <$> fmap (elimHSExpr . hss_hsexpr) (v .: "pre")
-      <*> fmap (elimHSExpr . hss_hsexpr) (v .: "post")
+      <$> fmap (\x -> (elimHSExpr (hss_hsexpr x), normalize (hss_source x))) (v .: "pre")
+      <*> fmap (\x -> (elimHSExpr (hss_hsexpr x), normalize (hss_source x))) (v .: "post")
       <*> (Storage.parse =<< (v .: "storage_update"))
+   where
+    normalize "" = "True"
+    normalize x = x
 
 elimHSExpr :: HSExpr a -> Expr a
 elimHSExpr = coerce
diff --git a/src/Horus/SW/Std.hs b/src/Horus/SW/Std.hs
index 90bc356b..9b68d442 100644
--- a/src/Horus/SW/Std.hs
+++ b/src/Horus/SW/Std.hs
@@ -17,7 +17,7 @@ stdSpecs :: Map ScopedName FuncSpec
 stdSpecs = Map.fromList stdSpecsList
 
 mkReadSpec :: ScopedName -> Int -> FuncSpec
-mkReadSpec name arity = emptyFuncSpec{fs_post = memory (ap - 1) .== var}
+mkReadSpec name arity = emptyFuncSpec{fs_post = (memory (ap - 1) .== var, "Reading: " <> tShow name)}
  where
   offsets = [-3 - arity + 1 .. -3]
   args = [memory (fp + fromIntegral offset) | offset <- offsets]
@@ -40,6 +40,8 @@ trustedStdFuncs =
   , "starkware.cairo.common.math.assert_le_felt"
   ]
 
+-- TODO(chore): Fill in 'Text' representation of the specs.
+
 {- | A lexicographically sorted by fs_name list of specifications of
  standard library functions.
 
@@ -54,21 +56,21 @@ stdSpecsList =
     , emptyFuncSpec
         { fs_post =
             let diff = memory (fp - 3) - memory (fp - 4)
-             in 0 .<= diff .&& diff .< rcBound
+             in (0 .<= diff .&& diff .< rcBound, "")
         }
     )
   ,
     ( "starkware.cairo.common.math.assert_le_felt"
-    , emptyFuncSpec{fs_post = memory (fp - 4) .<= memory (fp - 3)}
+    , emptyFuncSpec{fs_post = (memory (fp - 4) .<= memory (fp - 3), "")}
     )
   ,
     ( "starkware.cairo.common.math.assert_nn"
-    , emptyFuncSpec{fs_post = 0 .<= memory (fp - 3) .&& memory (fp - 3) .< rcBound}
+    , emptyFuncSpec{fs_post = (0 .<= memory (fp - 3) .&& memory (fp - 3) .< rcBound, "")}
     )
   ,
     ( "starkware.cairo.common.math.assert_nn_le"
     , emptyFuncSpec
-        { fs_post = 0 .<= memory (fp - 4) .&& memory (fp - 4) .<= memory (fp - 3)
+        { fs_post = (0 .<= memory (fp - 4) .&& memory (fp - 4) .<= memory (fp - 3), "")
         }
     )
   ,
@@ -78,7 +80,7 @@ stdSpecsList =
             let low = memory (ap - 1)
                 high = memory (ap - 2)
                 v = memory (fp - 3)
-             in low .== v `Expr.mod` rcBound .&& high .== v `Expr.div` rcBound
+             in (low .== v `Expr.mod` rcBound .&& high .== v `Expr.div` rcBound, "")
         }
     )
   ,
@@ -86,13 +88,15 @@ stdSpecsList =
     , let (value, div') = (memory (fp - 4), memory (fp - 3))
           (q, r) = (memory (ap - 2), memory (ap - 1))
        in emptyFuncSpec
-            { fs_pre = ExitField (0 .< div' .&& div' * rcBound .<= prime)
+            { fs_pre = (ExitField (0 .< div' .&& div' * rcBound .<= prime), "")
             , fs_post =
-                Expr.and
-                  [ 0 .<= q .&& q .< rcBound
-                  , 0 .<= r .&& r .< div'
-                  , value .== q * div' + r
-                  ]
+                ( Expr.and
+                    [ 0 .<= q .&& q .< rcBound
+                    , 0 .<= r .&& r .< div'
+                    , value .== q * div' + r
+                    ]
+                , ""
+                )
             }
     )
   ,
@@ -101,48 +105,52 @@ stdSpecsList =
         { fs_post =
             let diff = memory (fp - 3) - memory (fp - 4)
                 res = memory (ap - 1)
-             in Expr.ite
-                  (0 .<= diff .&& diff .< rcBound)
-                  (res .== 1)
-                  (res .== 0)
+             in ( Expr.ite
+                    (0 .<= diff .&& diff .< rcBound)
+                    (res .== 1)
+                    (res .== 0)
+                , ""
+                )
         }
     )
   ,
     ( "starkware.cairo.common.math_cmp.is_nn"
     , emptyFuncSpec
         { fs_post =
-            Expr.ite
-              (0 .<= memory (fp - 3) .&& memory (fp - 3) .< rcBound)
-              (memory (ap - 1) .== 1)
-              (memory (ap - 1) .== 0)
+            ( Expr.ite
+                (0 .<= memory (fp - 3) .&& memory (fp - 3) .< rcBound)
+                (memory (ap - 1) .== 1)
+                (memory (ap - 1) .== 0)
+            , ""
+            )
         }
     )
   ,
     ( "starkware.cairo.lang.compiler.lib.registers.get_ap"
-    , emptyFuncSpec{fs_post = memory (ap - 1) .== fp - 2}
+    , emptyFuncSpec{fs_post = (memory (ap - 1) .== fp - 2, "")}
     )
   ,
     ( "starkware.cairo.lang.compiler.lib.registers.get_fp_and_pc"
     , emptyFuncSpec
-        { fs_post = memory (ap - 2) .== memory (fp - 2) .&& memory (ap - 1) .== memory (fp - 1)
+        { fs_post = (memory (ap - 2) .== memory (fp - 2) .&& memory (ap - 1) .== memory (fp - 1), "")
         }
     )
   ,
     ( "starkware.starknet.common.syscalls.get_block_timestamp"
     , emptyFuncSpec
-        { fs_post = memory (ap - 1) .== blockTimestamp
+        { fs_post = (memory (ap - 1) .== blockTimestamp, "")
         }
     )
   ,
     ( "starkware.starknet.common.syscalls.get_caller_address"
     , emptyFuncSpec
-        { fs_post = memory (ap - 1) .== callerAddress
+        { fs_post = (memory (ap - 1) .== callerAddress, "")
         }
     )
   ,
     ( "starkware.starknet.common.syscalls.get_contract_address"
     , emptyFuncSpec
-        { fs_post = memory (ap - 1) .== contractAddress
+        { fs_post = (memory (ap - 1) .== contractAddress, "")
         }
     )
   ]
diff --git a/tests/resources/bats-template b/tests/resources/bats-template
index e4da0475..db4506cc 100644
--- a/tests/resources/bats-template
+++ b/tests/resources/bats-template
@@ -26,7 +26,7 @@ test_case() {
     temp_file="${base}.temp"
 
     horus-compile "$test_file" --output "$compiled_file" --spec_output "$spec_file"
-    stack run horus-check "$compiled_file" "$spec_file" -- -s cvc5 -s z3 -t 100000 &> "$temp_file" || true
+    stack run horus-check "$compiled_file" "$spec_file" -- -s cvc5 -s mathsat -s z3 -t 100000 &> "$temp_file" || true
     compare "${gold_file}" "${temp_file}"
     rm "$compiled_file"
     rm "$spec_file"
diff --git a/tests/resources/golden/extern_remove_dirty.cairo b/tests/resources/golden/extern_remove_dirty.cairo
new file mode 100644
index 00000000..0c2eb3e9
--- /dev/null
+++ b/tests/resources/golden/extern_remove_dirty.cairo
@@ -0,0 +1,12 @@
+%lang starknet
+
+@external
+func f() -> (array_len : felt, array : felt*) {
+    alloc_locals;
+    // An array of felts.
+    local felt_array: felt*;
+    assert felt_array[0] = 0;
+    assert felt_array[1] = 1;
+    assert felt_array[2] = 2;
+    return (array_len=3, array=felt_array);
+}
\ No newline at end of file
diff --git a/tests/resources/golden/extern_remove_dirty.gold b/tests/resources/golden/extern_remove_dirty.gold
new file mode 100644
index 00000000..8cfd00e4
--- /dev/null
+++ b/tests/resources/golden/extern_remove_dirty.gold
@@ -0,0 +1,2 @@
+f [inlined]
+Verified
\ No newline at end of file
diff --git a/tests/resources/golden/pre_fancy.cairo b/tests/resources/golden/pre_fancy.cairo
new file mode 100644
index 00000000..e1954d79
--- /dev/null
+++ b/tests/resources/golden/pre_fancy.cairo
@@ -0,0 +1,17 @@
+// @pre token == 0 or token == 1
+// @post (token == 0 and $Return.t == 1) or (token == 1 and $Return.t == 0)
+func get_opposite_token(token: felt) -> (t: felt) {
+  if (token == 0) {
+      return (t=1);
+  } else {
+      return (t=0);
+  }
+}
+
+// @pre token == 0 or token == 1
+// @post $Return.res == token
+func bar(token) -> (res: felt) {
+let (a) = get_opposite_token(token);
+let (b) = get_opposite_token(a);
+return (res=b);
+}
\ No newline at end of file
diff --git a/tests/resources/golden/pre_fancy.gold b/tests/resources/golden/pre_fancy.gold
new file mode 100644
index 00000000..f46c6c2e
--- /dev/null
+++ b/tests/resources/golden/pre_fancy.gold
@@ -0,0 +1,7 @@
+
+bar
+Verified
+
+get_opposite_token
+Verified
+