diff --git a/src/Pate/Equivalence.hs b/src/Pate/Equivalence.hs
index f9e2f69b..a1f81ccc 100644
--- a/src/Pate/Equivalence.hs
+++ b/src/Pate/Equivalence.hs
@@ -87,6 +87,7 @@ import qualified What4.PredMap as WPM
 import qualified Pate.ExprMappable as PEM
 
 import           Pate.TraceTree
+import Data.Data (Typeable)
 
 data EquivalenceStatus =
     Equivalent
@@ -384,6 +385,7 @@ memPreCondToPred ::
   forall sym arch v.
   IsSymInterface sym =>
   MM.RegisterInfo (MM.ArchReg arch) =>
+  Typeable arch =>
   sym ->
   SimScope sym arch v ->
   MemRegionEquality sym arch ->
diff --git a/src/Pate/Equivalence/Error.hs b/src/Pate/Equivalence/Error.hs
index 2b124f71..e001f97d 100644
--- a/src/Pate/Equivalence/Error.hs
+++ b/src/Pate/Equivalence/Error.hs
@@ -158,6 +158,7 @@ data InnerEquivalenceError arch
   | FailedToResolveAddress (MM.MemWord (MM.ArchAddrWidth arch))
   | forall tp. FailedToGroundExpr (SomeExpr tp)
   | OrphanedSingletonAnalysis (PB.FunPair arch)
+  | RequiresInvalidPointerOps
 
 data SomeExpr tp = forall sym. W4.IsExpr (W4.SymExpr sym) => SomeExpr (W4.SymExpr sym tp)
 
diff --git a/src/Pate/ExprMappable.hs b/src/Pate/ExprMappable.hs
index 3738171f..ef674027 100644
--- a/src/Pate/ExprMappable.hs
+++ b/src/Pate/ExprMappable.hs
@@ -32,6 +32,8 @@ module Pate.ExprMappable (
   , PartialF(..)
   , toPartialSeq
   , updateFilterSeq
+  , ExprMapFElems(..)
+
   ) where
 
 import qualified Control.Monad.IO.Class as IO
@@ -57,6 +59,11 @@ import qualified Pate.Parallel as Par
 import Unsafe.Coerce(unsafeCoerce)
 import Lang.Crucible.Simulator.SymSequence
 import Data.Maybe (fromMaybe)
+import qualified Lang.Crucible.Utils.MuxTree as MT
+import Data.Parameterized.Map (MapF)
+import qualified Data.Parameterized.TraversableF as TF
+import Data.Text
+import Control.Monad (forM)
 
 -- Expression binding
 
@@ -351,4 +358,27 @@ updateFilterSeq sym f_ s_ = evalWithFreshCache f s_
 
 
 instance ExprMappable sym () where
-  mapExpr _sym _f _e = pure ()
\ No newline at end of file
+  mapExpr _sym _f _e = pure ()
+
+instance ExprMappable sym Text where
+  mapExpr _ _ = return
+
+instance (Ord f, ExprMappable sym f) => ExprMappable sym (MT.MuxTree sym f) where
+  mapExpr sym (f :: forall tp. WI.SymExpr sym tp -> m (WI.SymExpr sym tp)) mt = do
+    go (MT.viewMuxTree @sym mt)
+    where
+      go :: WI.IsExprBuilder sym => [(f, WI.Pred sym)] -> m (MT.MuxTree sym f)
+      go [] = error "Unexpected empty Mux Tree"
+      go [(a,_p)] = MT.toMuxTree sym <$> mapExpr sym f a
+      go ((a, p):xs) = do
+        a' <- MT.toMuxTree sym <$> mapExpr sym f a
+        x <- go xs
+        p' <- f p
+        IO.liftIO $ MT.mergeMuxTree sym p' a' x
+
+-- | Wrapper for 'MapF' indicating that only the elements of the map should be
+--   traversed with 'mapExpr'
+newtype ExprMapFElems a b = ExprMapFElems { unExprMapFElems :: (MapF a b) }
+
+instance (forall tp. ExprMappable sym (f tp)) => ExprMappable sym (ExprMapFElems a f) where
+  mapExpr sym f (ExprMapFElems m) = ExprMapFElems <$> TF.traverseF (mapExpr sym f) m
\ No newline at end of file
diff --git a/src/Pate/MemCell.hs b/src/Pate/MemCell.hs
index d23442bc..74153ffe 100644
--- a/src/Pate/MemCell.hs
+++ b/src/Pate/MemCell.hs
@@ -40,6 +40,7 @@ import qualified Pate.ExprMappable as PEM
 import qualified Pate.Memory.MemTrace as PMT
 import qualified What4.ExprHelpers as WEH
 import qualified What4.PredMap as WPM
+import Data.Data (Typeable)
 
 -- | A pointer with an attached width, representing the size of the "cell" in bytes.
 -- It represents a discrete read or write, used as the key when forming a 'Pate.Equivalence.MemPred'
@@ -144,8 +145,10 @@ readMemCell sym mem cell@(MemCell{}) = do
 
 -- FIXME: this currently drops the region due to weaknesses in the memory model
 writeMemCell ::
+  forall sym arch w.
   IsSymInterface sym =>
   MC.RegisterInfo (MC.ArchReg arch) =>
+  Typeable arch =>
   sym ->
   -- | write condition
   WI.Pred sym ->
@@ -155,7 +158,7 @@ writeMemCell ::
   IO (PMT.MemTraceState sym (MC.ArchAddrWidth arch))
 writeMemCell sym cond mem cell@(MemCell{}) valPtr = do
   let repr = MC.BVMemRepr (cellWidth cell) (cellEndian cell)
-  PMT.writeMemState sym cond mem (cellPtr cell) repr valPtr
+  PMT.writeMemState @_ @arch sym cond mem (cellPtr cell) repr valPtr
 
 instance PEM.ExprMappable sym (MemCell sym arch w) where
   mapExpr sym f (MemCell ptr w end) = do
diff --git a/src/Pate/Memory/MemTrace.hs b/src/Pate/Memory/MemTrace.hs
index 1b8a3698..115d23b5 100644
--- a/src/Pate/Memory/MemTrace.hs
+++ b/src/Pate/Memory/MemTrace.hs
@@ -71,6 +71,11 @@ module Pate.Memory.MemTrace
 , PtrAssertions
 , doStaticRead
 , doStaticReadAddr
+, TraceEvent(..)
+, RegOp(..)
+, memFullSeq
+, addRegEvent
+, ppPtr'
 ) where
 
 import Unsafe.Coerce
@@ -96,7 +101,7 @@ import           Data.Parameterized.Classes
 import qualified Data.Parameterized.Context as Ctx
 
 import qualified Data.Macaw.Types as MT
-import Data.Macaw.CFG.AssignRhs (ArchAddrWidth, MemRepr(..))
+import Data.Macaw.CFG.AssignRhs (ArchAddrWidth, MemRepr(..), ArchReg)
 import Data.Macaw.Memory
            (AddrWidthRepr(..), Endianness(..), MemWidth
            , addrWidthClass, addrWidthRepr, addrWidthNatRepr, memWidthNatRepr
@@ -149,6 +154,11 @@ import qualified Pate.ExprMappable as PEM
 import           What4.ExprHelpers ( integerToNat )
 import qualified What4.ExprHelpers as WEH
 import qualified Pate.Memory as PM
+import Data.Macaw.CFG (ArchSegmentOff, RegisterInfo, ip_reg, MemAddr (MemAddr))
+import qualified Pate.SimulatorRegisters as PSr
+import Data.Data (Typeable, eqT)
+import Data.Maybe (mapMaybe)
+import qualified Data.Parameterized.TraversableF as TF
 
 ------
 -- * Undefined pointers
@@ -592,7 +602,7 @@ mkUndefinedPtrOps sym = do
 -- memory operations without trying to carefully guess the results of
 -- performing them.
 macawTraceExtensions ::
-  (IsSymInterface sym, SymArchConstraints arch, sym ~ ExprBuilder t st fs) =>
+  (Typeable arch, IsSymInterface sym, SymArchConstraints arch, sym ~ ExprBuilder t st fs) =>
   MacawArchEvalFn p sym (MemTrace arch) arch ->
   MacawSyscallModel sym arch ->
   GlobalVar (MemTrace arch) ->
@@ -633,10 +643,17 @@ data MemOp sym ptrW where
     Endianness ->
     MemOp sym ptrW
 
+ppPtr' :: IsExpr (SymExpr sym) => LLVMPtr sym arch -> Doc ann
+ppPtr' ptr@(LLVMPointer r off) 
+  | BaseBVRepr w <- exprType off
+  = case (asNat r, asBV off) of
+  (Just 1, Just off') -> "Stack Slot:" <+> viaShow (BV.asSigned w off')
+  _ -> ppPtr ptr
+
 prettyMemOp :: IsExpr (SymExpr sym) => MemOp sym ptrW -> Doc ann
 prettyMemOp (MemOp ptr dir cond _sz val _end) =
   viaShow dir <+>
-  ppPtr ptr <+>
+  ppPtr' ptr <+>
   (case dir of Read -> "->" ; Write -> "<-") <+>
   ppPtr val <+>
   case cond of
@@ -711,6 +728,22 @@ instance OrdF (SymExpr sym) => Ord (MemOp sym ptrW) where
         (toOrdering $ compareF vo1 vo2) <>
         compare end1 end2
 
+data RegOp sym arch =
+  RegOp (MapF.MapF (ArchReg arch) (PSr.MacawRegEntry sym))
+
+instance PEM.ExprMappable sym (RegOp sym arch) where
+  mapExpr sym f (RegOp m) = (RegOp . PEM.unExprMapFElems) <$> PEM.mapExpr sym f (PEM.ExprMapFElems m)
+
+-- | Used for presenting counter-examples that contain all register updates
+data TraceEvent sym arch =
+    RegOpEvent { traceInstr :: MuxTree sym (Maybe (ArchSegmentOff arch, Text)), _traceRegOp :: RegOp sym arch }
+  | TraceMemEvent { traceInstr :: MuxTree sym (Maybe (ArchSegmentOff arch, Text)), _traceMemEvent :: MemEvent sym (ArchAddrWidth arch)}
+
+instance PEM.ExprMappable sym (TraceEvent sym arch) where
+  mapExpr sym f e = case e of
+    RegOpEvent i rop -> RegOpEvent <$> PEM.mapExpr sym f i <*> PEM.mapExpr sym f rop
+    TraceMemEvent i mop -> TraceMemEvent <$> PEM.mapExpr sym f i <*> PEM.mapExpr sym f mop
+
 data MemEvent sym ptrW where
   MemOpEvent :: MemOp sym ptrW -> MemEvent sym ptrW
   SyscallEvent :: forall sym ptrW w.
@@ -761,8 +794,41 @@ addExternalCallEvent ::
 addExternalCallEvent sym nm data_ mem = do
   let
     event = ExternalCallEvent nm data_
-  memSeq' <- consSymSequence sym event (memSeq mem)
-  return $ mem { memSeq = memSeq' }
+  addMemEvent sym event mem
+
+addMemEvent ::
+  IsExprBuilder sym =>
+  OrdF (SymExpr sym) =>
+  sym ->
+  MemEvent sym ptrW ->
+  MemTraceImpl sym ptrW ->
+  IO (MemTraceImpl sym ptrW)
+addMemEvent sym ev mem = do
+  let i = memCurrentInstr mem
+  seq' <- liftIO (consSymSequence sym ev (memSeq mem))
+  fs <- case memFullSeq_  mem of
+    MemTraceFullSeq px s -> 
+      MemTraceFullSeq px <$> liftIO (consSymSequence sym (TraceMemEvent i ev) s)
+  return mem { memSeq = seq', memFullSeq_ = fs }
+
+addRegEvent ::
+  forall sym arch ptrW.
+  IsExprBuilder sym =>
+  ArchAddrWidth arch ~ ptrW =>
+  Typeable arch =>
+  sym ->
+  RegOp sym arch ->
+  MemTraceImpl sym ptrW ->
+  IO (MemTraceImpl sym ptrW)
+addRegEvent sym rop mem = do
+  let i = memCurrentInstr mem
+  fs <- case memFullSeq_  mem of
+    MemTraceFullSeq (px :: Proxy arch') s -> case eqT @arch @arch' of
+      Just Refl -> 
+        MemTraceFullSeq px <$> liftIO (consSymSequence sym (RegOpEvent i rop) s)
+      Nothing -> error "addRegEvent: unexpected arch mismatch"
+  return mem { memFullSeq_ = fs }
+
 
 prettyMemEvent :: (MemWidth ptrW, IsExpr (SymExpr sym)) => MemEvent sym ptrW -> Doc ann
 prettyMemEvent (MemOpEvent op) = prettyMemOp op
@@ -787,6 +853,9 @@ data MemTraceImpl sym ptrW = MemTraceImpl
   -- ^ The "base" memory loaded with the binary. We use this to directly service concrete
   --   reads from read-only memory. INVARIANT: we only mux together memories that were
   --   derived from the same initial memory, so we can assume the base memories are identical.
+  , memFullSeq_ :: MemTraceFullSeq sym ptrW
+  -- ^ Full sequence of register and memory operations since the start of the block
+
   }
 
 data MemTraceState sym ptrW = MemTraceState
@@ -796,6 +865,36 @@ data MemTraceState sym ptrW = MemTraceState
 
 type MemTraceSeq sym ptrW = SymSequence sym (MemEvent sym ptrW)
 
+--   FIXME: existentially-quantified 'arch' parameter is a workaround for the
+--   fact that only 'ptrW' is available in 'MemTraceImpl'
+data MemTraceFullSeq sym ptrW = 
+  forall arch. (Typeable arch, ptrW ~ ArchAddrWidth arch, RegisterInfo (ArchReg arch)) => 
+    MemTraceFullSeq (Proxy arch) (SymSequence sym (TraceEvent sym arch)) 
+
+instance PEM.ExprMappable sym (MemTraceFullSeq sym ptrW) where
+  mapExpr sym f (MemTraceFullSeq px s) = MemTraceFullSeq px <$> PEM.mapExpr sym f s
+
+memFullSeq ::
+  forall sym arch.
+  Typeable arch =>
+  MemTraceImpl sym (ArchAddrWidth arch) -> 
+  SymSequence sym (TraceEvent sym arch)
+memFullSeq mem | MemTraceFullSeq (_ :: Proxy arch2) s <- memFullSeq_ mem =
+  case eqT @arch @arch2 of
+    Just Refl -> s
+    Nothing -> error "memFullSeq: unexpected architecture"
+
+muxFullSeq :: 
+  sym ->
+  Pred sym ->
+  MemTraceFullSeq sym ptrW ->
+  MemTraceFullSeq sym ptrW ->
+  IO (MemTraceFullSeq sym ptrW)
+muxFullSeq sym p (MemTraceFullSeq (px :: Proxy arch1) a) (MemTraceFullSeq (_ :: Proxy arch2) b) = 
+  case eqT @arch1 @arch2 of
+    Just Refl -> MemTraceFullSeq px <$> muxSymSequence sym p a b
+    Nothing -> fail "muxFullSeq: incompatible architectures"
+
 -- | A map from pointers (a region integer combined with a pointer-width bitvector)
 -- to bytes, representing the contents of memory at the given pointer.
 type MemTraceArrBytes sym ptrW = MemArrBase sym ptrW (BaseBVType 8)
@@ -827,7 +926,9 @@ mkMemTraceVar ::
 mkMemTraceVar ha = freshGlobalVar ha (pack "llvm_memory_trace") knownRepr
 
 initMemTrace ::
-  forall sym ptrW.
+  forall sym arch ptrW.
+  ptrW ~ ArchAddrWidth arch =>
+  (Typeable arch, SymArchConstraints arch) =>
   IsSymExprBuilder sym =>
   sym ->
   Memory ptrW ->
@@ -837,12 +938,14 @@ initMemTrace sym baseMem Addr32 = do
   arrBytes <- ioFreshConstant sym "InitMemBytes" knownRepr
   arrRegions <- ioFreshConstant sym "InitMemRegions" knownRepr
   sq <- nilSymSequence sym
-  return $ MemTraceImpl sq (MemTraceState arrBytes arrRegions) (toMuxTree sym Nothing) baseMem
+  fullsq <- MemTraceFullSeq (Proxy @arch) <$> nilSymSequence sym
+  return $ MemTraceImpl sq (MemTraceState arrBytes arrRegions) (toMuxTree sym Nothing) baseMem fullsq
 initMemTrace sym baseMem Addr64 = do
   arrBytes <- ioFreshConstant sym "InitMemBytes" knownRepr
   arrRegions <- ioFreshConstant sym "InitMemRegions" knownRepr
   sq <- nilSymSequence sym
-  return $ MemTraceImpl sq (MemTraceState arrBytes arrRegions) (toMuxTree sym Nothing) baseMem
+  fullsq <- MemTraceFullSeq (Proxy @arch) <$> nilSymSequence sym
+  return $ MemTraceImpl sq (MemTraceState arrBytes arrRegions) (toMuxTree sym Nothing) baseMem fullsq
 
 
 mkMemoryBinding ::
@@ -870,10 +973,10 @@ instance IsExprBuilder sym => IntrinsicClass sym "memory_trace" where
     memArrBytes'   <- baseTypeIte sym p (memArrBytes $ memState t) (memArrBytes $ memState f)
     memArrRegions'   <- baseTypeIte sym p (memArrRegions $ memState t) (memArrRegions $ memState f)
     memInstr' <- mergeMuxTree sym p (memCurrentInstr t) (memCurrentInstr f)
-
+    memFullSeq' <- muxFullSeq sym p (memFullSeq_ t) (memFullSeq_ f)
     -- NB, we assume that the "base" memories are always the same, so we can arbitrarily choose
     -- one to use.
-    return $ MemTraceImpl memSeq' (MemTraceState memArrBytes' memArrRegions') memInstr' (memBaseMemory t)
+    return $ MemTraceImpl memSeq' (MemTraceState memArrBytes' memArrRegions') memInstr' (memBaseMemory t) memFullSeq'
 
   muxIntrinsic _ _ _ _ _ _ _ = error "Unexpected operands in memory_trace mux"
 
@@ -886,7 +989,7 @@ memTraceIntrinsicTypes = id
 type MacawTraceEvalStmtFunc p sym arch = MacawEvalStmtFunc (MacawStmtExtension arch) p sym (MacawExt arch)
 
 execMacawStmtExtension ::
-  forall p sym arch t st fs. (IsSymInterface sym, SymArchConstraints arch, sym ~ ExprBuilder t st fs) =>
+  forall p sym arch t st fs. (Typeable arch, IsSymInterface sym, SymArchConstraints arch, sym ~ ExprBuilder t st fs) =>
   MacawArchEvalFn p sym (MemTrace arch) arch ->
   UndefinedPtrOps sym ->
   MacawSyscallModel sym arch ->
@@ -927,12 +1030,22 @@ execMacawStmtExtension (MacawArchEvalFn archStmtFn) mkundef syscallModel mvar gl
 
     MacawArchStmtExtension archStmt -> archStmtFn mvar globs archStmt
 
-    MacawArchStateUpdate{} -> \cst -> pure ((), cst)
+    MacawArchStateUpdate _ upds -> liftToCrucibleState mvar $ \(sym :: sym) -> do
+      let upds' = TF.fmapF (\(MS.MacawCrucibleValue x) -> PSr.MacawRegEntry @_ @sym (regType x) (regValue x)) upds
+      mem <- get
+      mem' <- liftIO $ addRegEvent sym (RegOp upds') mem
+      put mem'
+      return ()
+
     MacawInstructionStart baddr iaddr dis ->
       case incSegmentOff baddr (memWordToUnsigned iaddr) of
         Just off ->
-          liftToCrucibleState mvar $ \sym ->
-            modify (\mem -> mem{ memCurrentInstr = toMuxTree sym (Just (off,dis)) })
+          liftToCrucibleState mvar $ \sym -> do
+            mem <- get
+            off_ptr <- liftIO $ segOffToPtr sym off
+            mem' <- liftIO $ addRegEvent @_ @arch sym (RegOp (MapF.singleton ip_reg (PSr.MacawRegEntry (LLVMPointerRepr knownRepr) off_ptr))) mem
+            put $ mem'{ memCurrentInstr = toMuxTree sym (Just (off,dis)) }
+
         Nothing ->
           panic Verifier "execMacawExteions: MacawInstructionStart"
                     [ "MemorySegmentOff out of range"
@@ -1059,8 +1172,8 @@ applySyscallModel
         do -- emit a syscall event that just captures the offset value of the r0 register
            mem <- readGlobal mvar
            let i = memCurrentInstr mem
-           seq' <- liftIO (consSymSequence sym (SyscallEvent i off) (memSeq mem))
-           writeGlobal mvar mem{ memSeq = seq' }
+           mem' <- liftIO (addMemEvent sym (SyscallEvent i off) mem)
+           writeGlobal mvar mem'
 
         -- return the registers r0 and r1 unchanged, assume we have no memory effects (!)
         return (Ctx.Empty :> RV (regValue r0) :> RV (regValue r1))
@@ -1524,6 +1637,9 @@ doStaticReadAddr mem addr w end = do
 -- | Compute the updated memory state resulting from writing a value to the given address, without
 -- accumulating any trace information.
 writeMemState ::
+  forall sym arch ptrW ty.
+  ptrW ~ ArchAddrWidth arch =>
+  (Typeable arch, RegisterInfo (ArchReg arch)) =>
   IsSymInterface sym =>
   MemWidth ptrW =>
   sym ->
@@ -1535,8 +1651,9 @@ writeMemState ::
   IO (MemTraceState sym ptrW)
 writeMemState sym cond memSt ptr repr val = do
   sq <- nilSymSequence sym
-  let mem = MemTraceImpl sq memSt (toMuxTree sym Nothing) (emptyMemory (addrWidthRepr Proxy))
-  MemTraceImpl _ memSt' _ _ <- execStateT (doMemOpInternal sym Write (Conditional cond) (addrWidthRepr mem) ptr val repr) mem
+  fullsq <- MemTraceFullSeq (Proxy @arch) <$> nilSymSequence sym
+  let mem = MemTraceImpl sq memSt (toMuxTree sym Nothing) (emptyMemory (addrWidthRepr Proxy)) fullsq
+  MemTraceImpl _ memSt' _ _ _ <- execStateT (doMemOpInternal sym Write (Conditional cond) (addrWidthRepr mem) ptr val repr) mem
   return memSt'
 
 -- | Write to the memory array and set the dirty bits on
@@ -1614,8 +1731,8 @@ doMemOpInternal sym dir cond ptrW = go where
       -> addrWidthsArePositive ptrW $ do
 
       do mem <- get
-         seq' <- liftIO (consSymSequence sym (MemOpEvent (MemOp ptr dir cond byteWidth regVal endianness)) (memSeq mem))
-         put mem{ memSeq = seq' }
+         mem' <- liftIO (addMemEvent sym (MemOpEvent (MemOp ptr dir cond byteWidth regVal endianness)) mem)
+         put mem'
 
       case dir of
         Read -> return ()
@@ -1918,6 +2035,21 @@ memEqAtRegion sym stackRegion mem1 mem2 = do
   regionsEq <- isEq sym mem1StackRegions mem2StackRegions
   andPred sym bytesEq regionsEq
 
+segOffToPtr ::
+  forall sym ptrW.
+  IsExprBuilder sym =>
+  MemWidth ptrW =>
+  sym ->
+  MemSegmentOff ptrW ->
+  IO (LLVMPtr sym ptrW)
+segOffToPtr sym off = do
+  -- we assume a distinct region for all executable code
+  region <- natLit sym 0
+  let MemAddr _base offset = segoffAddr off
+  liftIO $ do
+    let ptrW = memWidthNatRepr @ptrW
+    ptrOffset <- bvLit sym ptrW (BV.mkBV ptrW (toInteger offset))
+    pure (LLVMPointer region ptrOffset)
 
 -- | Memory states are exactly equivalent.
 memEqExact ::
@@ -1976,15 +2108,17 @@ instance PEM.ExprMappable sym a => PEM.ExprMappable sym (SymSequence sym a) wher
             ys' <- rec ys
             IO.liftIO $ muxSymSequence sym p' xs' ys'
 
+instance PEM.ExprMappable sym (MemSegmentOff w) where
+  mapExpr _ _ = return
+
 
 instance PEM.ExprMappable sym (MemTraceImpl sym w) where
   mapExpr sym f mem = do
     memSeq' <- PEM.mapExpr sym f (memSeq mem)
     memState' <- PEM.mapExpr sym f $ memState mem
-    let memInstr' =  memCurrentInstr mem -- TODO? rewrite the mux tree?
-                                         -- I expect it to basically never be interesting
-                                         -- to do this...
-    return $ MemTraceImpl memSeq' memState' memInstr' (memBaseMemory mem)
+    memInstr' <- PEM.mapExpr sym f $ memCurrentInstr mem
+    memFullSeq' <- PEM.mapExpr sym f $ memFullSeq_ mem
+    return $ MemTraceImpl memSeq' memState' memInstr' (memBaseMemory mem) memFullSeq'
 
 instance PEM.ExprMappable sym (MemTraceState sym w) where
   mapExpr _sym f memSt = do
diff --git a/src/Pate/Monad.hs b/src/Pate/Monad.hs
index e17c8a84..0393efad 100644
--- a/src/Pate/Monad.hs
+++ b/src/Pate/Monad.hs
@@ -157,6 +157,7 @@ import qualified Data.Macaw.BinaryLoader as MBL
 
 import qualified What4.Expr as WE
 import qualified What4.Expr.GroundEval as W4G
+import qualified What4.Expr.Builder as W4B
 import qualified What4.Interface as W4
 import qualified What4.SatResult as W4R
 import qualified What4.Symbol as WS
@@ -582,7 +583,7 @@ withFreshVars blocks f = do
     mkMem bin = do
       binCtx <- getBinCtx' bin
       let baseMem = MBL.memoryImage $ PMC.binary binCtx
-      withSymIO $ \sym -> MT.initMemTrace sym baseMem (MM.addrWidthRepr (Proxy @(MM.ArchAddrWidth arch)))
+      withSymIO $ \sym -> MT.initMemTrace @_ @arch sym baseMem (MM.addrWidthRepr (Proxy @(MM.ArchAddrWidth arch)))
 
     mkStackBase :: forall bin v. PBi.WhichBinaryRepr bin -> EquivM_ sym arch (StackBase sym arch v)
     mkStackBase bin = withSymIO $ \sym -> freshStackBase sym bin (Proxy @arch)
diff --git a/src/Pate/SimulatorRegisters.hs b/src/Pate/SimulatorRegisters.hs
index 7276a591..bcceead7 100644
--- a/src/Pate/SimulatorRegisters.hs
+++ b/src/Pate/SimulatorRegisters.hs
@@ -74,10 +74,10 @@ data MacawRegVar sym (tp :: MT.Type) where
     , macawVarBVs :: Ctx.Assignment (WI.SymExpr sym) (CrucBaseTypes (MS.ToCrucibleType tp))
     } -> MacawRegVar sym tp
 
-instance (WI.IsExpr (WI.SymExpr sym), PC.ShowF (WI.SymExpr sym)) => Show (MacawRegEntry sym tp) where
+instance (WI.IsExpr (WI.SymExpr sym)) => Show (MacawRegEntry sym tp) where
   show (MacawRegEntry repr v) = case repr of
-    CLM.LLVMPointerRepr{} | CLM.LLVMPointer rg bv <- v -> show (WI.printSymNat rg) ++ "+" ++ PC.showF bv
-    CT.BoolRepr -> PC.showF v
+    CLM.LLVMPointerRepr{} | CLM.LLVMPointer rg bv <- v -> show (WI.printSymNat rg) ++ "+" ++ show (WI.printSymExpr bv)
+    CT.BoolRepr -> show (WI.printSymExpr v)
     CT.StructRepr Ctx.Empty -> "()"
     _ -> "macawRegEntry: unsupported"
 
diff --git a/src/Pate/Verification/StrongestPosts.hs b/src/Pate/Verification/StrongestPosts.hs
index a1374c97..e55cff8f 100644
--- a/src/Pate/Verification/StrongestPosts.hs
+++ b/src/Pate/Verification/StrongestPosts.hs
@@ -1552,14 +1552,16 @@ equivalentSequences' sym cache = \xs ys -> loop [xs] [ys]
        liftIO $ W4.andPred sym eq1 eq2
 
 instance ValidSymArch sym arch => IsTraceNode '(sym,arch) "totality" where
-  type TraceNodeType '(sym,arch) "totality" = TotalityResult (MM.ArchAddrWidth arch)
+  type TraceNodeType '(sym,arch) "totality" = TotalityResult sym arch
   prettyNode () r = case r of
     CasesTotal -> "Cases total"
     TotalityCheckingError msg -> "Error:" <+> PP.pretty msg
-    TotalityCheckCounterexample (TotalityCounterexample (oIP,oEnd,oInstr) (pIP,pEnd,pInstr)) -> PP.vsep $
+    TotalityCheckCounterexample ocex (TotalityCounterexample (oIP,oEnd,oInstr) (pIP,pEnd,pInstr)) -> PP.vsep $
       ["Found extra exit while checking totality:"
       , PP.pretty (showHex oIP "") <+> PP.pretty (PPI.ppExitCase oEnd) <+> PP.pretty (show oInstr)
       , PP.pretty (showHex pIP "") <+> PP.pretty (PPI.ppExitCase pEnd) <+> PP.pretty (show pInstr)
+      , ""
+      , PP.pretty ocex
       ]
   nodeTags = [(Summary, \_ r -> case r of
                    CasesTotal -> "Total"
@@ -1589,7 +1591,7 @@ checkTotality bPair bundle preD exits gr =
            do let msg' = ("Error while checking totality! " ++ msg)
               err <- emitError' (PEE.TotalityError msg')
               return (Nothing, recordMiscAnalysisError gr (GraphNode bPair) err)
-         TotalityCheckCounterexample cex@(TotalityCounterexample (oIP,oEnd,oInstr) (pIP,pEnd,pInstr)) ->
+         TotalityCheckCounterexample _ cex@(TotalityCounterexample (oIP,oEnd,oInstr) (pIP,pEnd,pInstr)) ->
            do traceBundle bundle $ unlines
                 ["Found extra exit while checking totality:"
                 , showHex oIP "" ++ " " ++ PPI.ppExitCase oEnd ++ " " ++ show oInstr
@@ -1598,10 +1600,10 @@ checkTotality bPair bundle preD exits gr =
               
               return (Just cex, gr)
 
-data TotalityResult ptrW
+data TotalityResult sym arch
   = CasesTotal
   | TotalityCheckingError String
-  | TotalityCheckCounterexample (TotalityCounterexample ptrW)
+  | TotalityCheckCounterexample (CE.TraceEvents sym arch) (TotalityCounterexample (MM.ArchAddrWidth arch))
 
 {-
 -- TODO: use solver to resolve classifier errors by comparing
@@ -1701,7 +1703,7 @@ doCheckTotality :: forall sym arch v.
   SimBundle sym arch v ->
   AbstractDomain sym arch v -> 
   [PPa.PatchPair (PB.BlockTarget arch)] ->
-  EquivM sym arch (TotalityResult (MM.ArchAddrWidth arch))
+  EquivM sym arch (TotalityResult sym arch)
 doCheckTotality bundle _preD exits =
   withSym $ \sym ->
     do
@@ -1728,7 +1730,9 @@ doCheckTotality bundle _preD exits =
        goalSat "doCheckTotality" asm $ \res -> case res of
          Unsat _ -> return CasesTotal
          Unknown -> return (TotalityCheckingError "UNKNOWN result when checking totality")
-         Sat evalFn' -> withGroundEvalFn evalFn' $ \evalFn -> do
+         Sat evalFn' -> do
+           ocex <- getTraceFromModel evalFn' bundle
+           withGroundEvalFn evalFn' $ \evalFn -> do
            -- We found an execution that does not correspond to one of the
            -- executions listed above, so compute the counterexample.
            --
@@ -1748,13 +1752,14 @@ doCheckTotality bundle _preD exits =
                 case iPV of
                   Just val -> return $ (Just (val, blockEndCase, instr))
                   Nothing -> return $ Nothing
+              
               case result of
                 PPa.PatchPairC (Just ores) (Just pres) ->
-                  return (TotalityCheckCounterexample
+                  return (TotalityCheckCounterexample ocex
                     (TotalityCounterexample ores pres))
                 PPa.PatchPairSingle _ (Const (Just r)) ->
                   --FIXME: update the type to use PatchPairC
-                  return (TotalityCheckCounterexample
+                  return (TotalityCheckCounterexample ocex
                     (TotalityCounterexample r r))
                 _ -> return (TotalityCheckingError ("IP register had unexpected type"))
 
@@ -1906,12 +1911,13 @@ triageBlockTarget scope bundle' currBlock st d blkts = do
     mrets <- PPa.toMaybeCases <$> 
       PPa.forBinsF (\bin -> PB.targetReturn <$> PPa.get bin blkts)
     case (combineCases ecase1 ecase2,mrets) of
-      (Nothing,_) -> handleDivergingPaths scope currBlock st d blkts
-      (_,PPa.PatchPairMismatch{}) -> handleDivergingPaths scope currBlock st d blkts
-      _ | isMismatchedStubs stubPair -> handleDivergingPaths scope currBlock st d blkts
+      (Nothing,_) -> handleDivergingPaths scope bundle' currBlock st d blkts
+      (_,PPa.PatchPairMismatch{}) -> handleDivergingPaths scope bundle' currBlock st d blkts
+      _ | isMismatchedStubs stubPair -> handleDivergingPaths scope bundle' currBlock st d blkts
       (Just ecase, PPa.PatchPairJust rets) -> fmap (updateBranchGraph st blkts) $ do
         let pPair = TF.fmapF PB.targetCall blkts
         bundle <- PD.associateFrames bundle' ecase (hasStub stubPair)
+        getSomeGroundTrace bundle >>= emitTrace @"trace_events"
         traceBundle bundle ("  Return target " ++ show rets)
         ctx <- view PME.envCtxL
         let isEquatedCallSite = any (PB.matchEquatedAddress pPair) (PMC.equatedFunctions ctx)
@@ -1922,6 +1928,7 @@ triageBlockTarget scope bundle' currBlock st d blkts = do
 
       (Just ecase, PPa.PatchPairNothing) -> fmap (updateBranchGraph st blkts) $ do
         bundle <- PD.associateFrames bundle' ecase (hasStub stubPair)
+        getSomeGroundTrace bundle >>= emitTrace @"trace_events"
         case ecase of
           MCS.MacawBlockEndReturn -> handleReturn scope bundle currBlock d gr
           _ -> do
@@ -2224,12 +2231,13 @@ singletonBundle bin (SimBundle in_ out_) =
 handleDivergingPaths ::
   HasCallStack =>
   PS.SimScope sym arch v ->
+  SimBundle sym arch v ->
   NodeEntry arch {- ^ current entry point -} ->
   BranchState sym arch ->
   AbstractDomain sym arch v {- ^ current abstract domain -}  ->
   PPa.PatchPair (PB.BlockTarget arch) {- ^ next entry point -} ->
   EquivM sym arch (BranchState sym arch)  
-handleDivergingPaths scope currBlock st dom blkt = fnTrace "handleDivergingPaths" $ do
+handleDivergingPaths scope bundle currBlock st dom blkt = fnTrace "handleDivergingPaths" $ do
   let gr0 = branchGraph st
   let mchoice = branchDesyncChoice st
   priority <- thisPriority
@@ -2255,15 +2263,21 @@ handleDivergingPaths scope currBlock st dom blkt = fnTrace "handleDivergingPaths
       a <- case mchoice of
         Just DeferDecision -> return DeferDecision
         Just ChooseSyncPoint -> return DeferDecision
-        _ -> choose @"()" msg $ \choice -> do
-          -- default choice
-          choice "Ignore divergence (admit a non-total result)" () $ return AdmitNonTotal
-
-          choice "Assert divergence is infeasible" () $ return (IsInfeasible ConditionAsserted)
-          choice "Assume divergence is infeasible" () $ return (IsInfeasible ConditionAssumed)
-          choice "Remove divergence in equivalence condition" () $ return (IsInfeasible ConditionEquiv)
-          choice "Choose synchronization points" () $ return ChooseSyncPoint
-          choice "Defer decision" () $ return DeferDecision
+        _ -> do
+          () <- withTracing @"message" "Equivalence Counter-example" $ withSym $ \sym -> do
+            -- we've already introduced the path condition here, so we just want to see how we got here
+            res <- getSomeGroundTrace bundle
+            emitTrace @"trace_events" res
+            return ()
+          choose @"()" msg $ \choice -> do
+            -- default choice
+            choice "Ignore divergence (admit a non-total result)" () $ return AdmitNonTotal
+
+            choice "Assert divergence is infeasible" () $ return (IsInfeasible ConditionAsserted)
+            choice "Assume divergence is infeasible" () $ return (IsInfeasible ConditionAssumed)
+            choice "Remove divergence in equivalence condition" () $ return (IsInfeasible ConditionEquiv)
+            choice "Choose synchronization points" () $ return ChooseSyncPoint
+            choice "Defer decision" () $ return DeferDecision
       
       let st' = st { branchDesyncChoice = Just a }
       case a of
@@ -2272,7 +2286,7 @@ handleDivergingPaths scope currBlock st dom blkt = fnTrace "handleDivergingPaths
         ChooseSyncPoint -> do
           pg1 <- chooseSyncPoint divergeNode pg
           pg2 <- updateCombinedSyncPoint divergeNode pg1
-          handleDivergingPaths scope currBlock (st'{ branchGraph = pg2 }) dom blkt
+          handleDivergingPaths scope bundle currBlock (st'{ branchGraph = pg2 }) dom blkt
         IsInfeasible condK -> do
           gr2 <- pruneCurrentBranch scope (divergeNode, GraphNode currBlockO) condK pg
           gr3 <- pruneCurrentBranch scope (divergeNode, GraphNode currBlockP) condK gr2
diff --git a/src/Pate/Verification/StrongestPosts/CounterExample.hs b/src/Pate/Verification/StrongestPosts/CounterExample.hs
index 5e0d0165..b4605c99 100644
--- a/src/Pate/Verification/StrongestPosts/CounterExample.hs
+++ b/src/Pate/Verification/StrongestPosts/CounterExample.hs
@@ -6,10 +6,11 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE TypeApplications #-}
-
+{-# LANGUAGE ScopedTypeVariables #-}
 
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RankNTypes #-}
 
 module Pate.Verification.StrongestPosts.CounterExample
   ( TotalityCounterexample(..)
@@ -20,6 +21,11 @@ module Pate.Verification.StrongestPosts.CounterExample
   , groundObservableSequence
   , groundMuxTree
   , groundMemEvent
+  , ppTraceEvents
+  , TraceEvents(..)
+  , groundTraceEvent
+  , groundTraceEventSequence
+  , groundRegOp
   ) where
 
 
@@ -49,6 +55,12 @@ import qualified What4.Interface as W4
 import qualified Data.Parameterized.TraversableFC as TFC
 import qualified Lang.Crucible.LLVM.MemModel as CLM
 import           Lang.Crucible.Simulator.SymSequence
+import qualified Lang.Crucible.Types as CT
+import qualified Data.Parameterized.TraversableF as TF
+import qualified What4.Concrete as W4
+import Data.Functor.Const
+import qualified Data.Parameterized.Map as MapF
+import Data.Maybe (mapMaybe)
 
 -- | A totality counterexample represents a potential control-flow situation that represents
 --   desynchronization of the original and patched program. The first tuple represents
@@ -115,16 +127,7 @@ instance (PA.ValidArch arch, PSo.ValidSym sym) => IsTraceNode '(sym,arch) "obser
   type TraceNodeType '(sym,arch) "observable_result" = ObservableCheckResult sym arch
   prettyNode () = \case
     ObservableCheckEq -> "Observably Equivalent"
-    ObservableCheckCounterexample (ObservableCounterexample regsCE oSeq pSeq) -> PP.vsep $ 
-       ["Observable Inequivalence Detected:"
-       -- FIXME: this is useful but needs better presentation
-       , "== Diverging Registers =="
-       , prettyRegsCE regsCE
-       , "== Original sequence =="
-       ] ++ (map MT.prettyMemEvent oSeq) ++
-       [ "== Patched sequence ==" ]
-       ++ (map MT.prettyMemEvent pSeq)
-
+    ObservableCheckCounterexample ocex -> ppObservableCounterexample ocex 
     ObservableCheckError msg -> PP.vsep $
       [ "Error during observability check"
       , PP.pretty msg
@@ -137,6 +140,25 @@ instance (PA.ValidArch arch, PSo.ValidSym sym) => IsTraceNode '(sym,arch) "obser
       | tag <- [Simplified, Summary, JSONTrace]
     ]
 
+ppObservableCounterexample ::
+  PA.ValidArch arch =>
+  PSo.ValidSym sym =>
+  ObservableCounterexample sym arch ->
+  PP.Doc a
+ppObservableCounterexample (ObservableCounterexample regsCE oSeq pSeq) = PP.vsep $ 
+  ["Observable Inequivalence Detected:"
+  -- FIXME: this is useful but needs better presentation
+  , "== Diverging Registers =="
+  , prettyRegsCE regsCE
+  , "== Original sequence =="
+  ] ++ (map MT.prettyMemEvent oSeq) ++
+  [ "== Patched sequence ==" ]
+  ++ (map MT.prettyMemEvent pSeq)
+
+
+instance (PA.ValidArch arch, PSo.ValidSym sym) => PP.Pretty (ObservableCounterexample sym arch) where
+  pretty = ppObservableCounterexample
+
 groundObservableSequence ::
   (sym ~ W4.ExprBuilder t st fs, 1 <= ptrW) =>
   sym ->
@@ -189,4 +211,156 @@ groundMuxTree sym evalFn = MT.collapseMuxTree sym ite
   where
     ite p x y =
       do b <- W4.groundEval evalFn p
-         if b then return x else return y
\ No newline at end of file
+         if b then return x else return y
+
+data TraceEvents sym arch =
+  TraceEvents (PPa.PatchPairC (MT.RegOp sym arch, [TraceEventGroup sym arch]))
+
+data TraceEventGroup sym arch =
+  TraceEventGroup (Maybe (MM.ArchSegmentOff arch)) [MT.TraceEvent sym arch]
+
+ppRegOp :: forall sym arch ann. (PA.ValidArch arch, PSo.ValidSym sym) => MT.RegOp sym arch -> [PP.Doc ann]
+ppRegOp (MT.RegOp m) = mapMaybe (\(MapF.Pair r v) -> 
+  case PA.displayRegister r of
+  PA.Normal pr -> Just $ PP.pretty pr <+> "<-" <+> (prettyVal v)
+  _ | Just Refl <- testEquality MM.ip_reg r -> Just $ "pc" <+> "<-" <+> (prettyVal v)
+  _ -> Nothing) (MapF.toList m)
+  where
+    prettyVal :: forall tp. PSR.MacawRegEntry sym tp -> PP.Doc ann
+    prettyVal r = case PSR.macawRegRepr r of
+      CLM.LLVMPointerRepr{} -> MT.ppPtr' (PSR.macawRegValue r)
+      _ -> PP.pretty $ show r
+
+
+ppTraceEvent :: (PA.ValidArch arch, PSo.ValidSym sym) => MT.TraceEvent sym arch -> [PP.Doc ann]
+ppTraceEvent ev = case ev of
+  MT.RegOpEvent _ rop -> ppRegOp rop
+  MT.TraceMemEvent _ mev -> [MT.prettyMemEvent mev]
+
+ppTraceEventGroup ::
+  PA.ValidArch arch =>
+  PSo.ValidSym sym =>
+  TraceEventGroup sym arch ->
+  Maybe (PP.Doc a)  
+ppTraceEventGroup evg = case evg of
+  (TraceEventGroup (Just addr) evs) -> Just $ case concat (map ppTraceEvent evs) of
+    [] -> PP.parens (PP.viaShow addr)
+    [pretty_ev] -> PP.parens (PP.viaShow addr) <+> pretty_ev
+    pretty_evs -> PP.parens (PP.viaShow addr) <> PP.line <> PP.indent 2 (PP.vsep pretty_evs)
+  (TraceEventGroup Nothing evs) -> case concat (map ppTraceEvent evs) of
+    [] -> Nothing
+    [pretty_ev] -> Just pretty_ev
+    pretty_evs -> Just $ PP.indent 2 (PP.vsep pretty_evs)
+
+instance (PSo.ValidSym sym, PA.ValidArch arch) => IsTraceNode '(sym,arch) "trace_events" where
+  type TraceNodeType '(sym,arch) "trace_events" = TraceEvents sym arch
+  prettyNode () = ppTraceEvents
+  nodeTags = 
+    map (\tag -> (tag, \_ (TraceEvents evs) -> 
+      "Event Trace:" PP.<+> PPa.ppPatchPair' (\(Const (_init_regs, s)) -> 
+        ppTraceEventSummary s) evs))
+    [Summary, Simplified]
+
+ppTraceEventSummary ::
+  forall sym arch a.
+  PA.ValidArch arch =>
+  [TraceEventGroup sym arch] -> 
+  PP.Doc a
+ppTraceEventSummary [] = ""
+ppTraceEventSummary (t:tr) = case (t, last tr) of
+  (TraceEventGroup Nothing _, _) -> ppTraceEventSummary tr
+  (TraceEventGroup (Just addr_head) _, TraceEventGroup (Just addr_last) _) ->
+    PP.viaShow addr_head PP.<+> ".." <+> PP.viaShow addr_last
+  _ -> ""
+
+ppTraceEvents ::
+  PA.ValidArch arch =>
+  PSo.ValidSym sym =>
+  TraceEvents sym arch ->
+  PP.Doc a
+ppTraceEvents (TraceEvents tr) = case tr of
+  PPa.PatchPairOriginal (Const (init_regsO, trO)) -> 
+    PP.vsep $ [ "== Initial Registers ==" ] ++ ppRegOp init_regsO ++ mapMaybe ppTraceEventGroup trO
+  PPa.PatchPairPatched (Const (init_regsP, trP)) -> 
+    PP.vsep $ [ "== Initial Registers ==" ] ++ ppRegOp init_regsP ++ mapMaybe ppTraceEventGroup trP
+  PPa.PatchPairC (init_regsO, trO) (init_regsP, trP) -> PP.vsep $ 
+       [ "== Initial Original Registers ==" ]
+    ++ ppRegOp init_regsO
+    ++ [ "== Original sequence ==" ]
+    ++ mapMaybe ppTraceEventGroup trO
+    ++ [ "== Initial Patched Registers ==" ]
+    ++ ppRegOp init_regsP
+    ++ [ "== Patched sequence ==" ]
+    ++ mapMaybe ppTraceEventGroup trP
+
+instance (PA.ValidArch arch, PSo.ValidSym sym) => PP.Pretty (TraceEvents sym arch) where
+  pretty = ppTraceEvents
+
+groundRegOp ::
+  (sym ~ W4.ExprBuilder t st fs) =>
+  1 <= MM.ArchAddrWidth arch =>
+  sym ->
+  W4.GroundEvalFn t ->
+  MT.RegOp sym arch ->
+  IO (MT.RegOp sym arch)
+groundRegOp sym evalFn (MT.RegOp m) = 
+  MT.RegOp <$> TF.traverseF (groundRegEntry sym evalFn) m
+
+groundRegEntry :: 
+  (sym ~ W4.ExprBuilder t st fs) =>
+  sym ->
+  W4.GroundEvalFn t ->
+  PSR.MacawRegEntry sym tp ->
+  IO (PSR.MacawRegEntry sym tp)  
+groundRegEntry sym evalFn (PSR.MacawRegEntry repr v) = PSR.MacawRegEntry repr <$> case repr of
+  CLM.LLVMPointerRepr{} -> CLM.concPtr sym (\x -> W4.groundEval evalFn x) v
+  CT.BoolRepr -> W4.groundEval evalFn v >>= (W4.concreteToSym sym . W4.ConcreteBool)
+  _ -> return v
+
+groundTraceEvent ::
+  (sym ~ W4.ExprBuilder t st fs) =>
+  1 <= MM.ArchAddrWidth arch =>
+  sym ->
+  W4.GroundEvalFn t ->
+  MT.TraceEvent sym arch ->
+  IO (MT.TraceEvent sym arch)
+groundTraceEvent sym evalFn = \case
+  MT.RegOpEvent i rop -> MT.RegOpEvent <$> (MT.toMuxTree sym <$> groundMuxTree sym evalFn i) <*> groundRegOp sym evalFn rop
+  MT.TraceMemEvent i mop -> MT.TraceMemEvent <$> (MT.toMuxTree sym <$> groundMuxTree sym evalFn i)  <*> groundMemEvent sym evalFn mop
+
+
+dropPCReg :: PA.ValidArch arch => MT.TraceEvent sym arch -> MT.TraceEvent sym arch
+dropPCReg = \case
+  MT.RegOpEvent i (MT.RegOp m) -> MT.RegOpEvent i (MT.RegOp (MapF.delete (MM.ip_reg) m))
+  x -> x
+
+-- NB: events are reversed in the ground list so they appear in the natural order 
+-- (i.e. first event is the head of the list)
+groundTraceEventSequence ::
+  forall sym arch t st fs. 
+  (sym ~ W4.ExprBuilder t st fs) =>
+  PA.ValidArch arch =>
+  sym ->
+  W4.GroundEvalFn t ->
+  SymSequence sym (MT.TraceEvent sym arch) ->
+  IO [TraceEventGroup sym arch]
+groundTraceEventSequence sym evalFn s = do
+  l <- reverse <$> concreteizeSymSequence (\p -> W4.groundEval evalFn p) return s
+  go Nothing [] l
+  where
+    go :: Maybe (MM.ArchSegmentOff arch) -> [MT.TraceEvent sym arch] -> [MT.TraceEvent sym arch] -> IO [TraceEventGroup sym arch]
+    go last_instr ground_evs [] = return $ [TraceEventGroup last_instr (reverse ground_evs)]
+    go last_instr ground_evs (e1 : evs) = do
+      e1_instr <- fmap fst <$> groundMuxTree sym evalFn (MT.traceInstr e1)
+      e1_ground <- groundTraceEvent sym evalFn e1
+      case last_instr == e1_instr of
+        True -> go last_instr (e1_ground : ground_evs) evs
+        False -> do
+          evs' <- go e1_instr [e1_ground] evs
+          case ground_evs of
+            [] -> return evs'
+            _ -> do
+              let ground_evs' = case evs' of
+                    (_ : _) | Just{} <- e1_instr -> map dropPCReg ground_evs
+                    _ -> ground_evs
+              return $ (TraceEventGroup last_instr (reverse ground_evs') : evs')
diff --git a/src/Pate/Verification/Validity.hs b/src/Pate/Verification/Validity.hs
index 5648ef72..776099b4 100644
--- a/src/Pate/Verification/Validity.hs
+++ b/src/Pate/Verification/Validity.hs
@@ -45,6 +45,7 @@ import qualified Pate.Memory.MemTrace as MT
 
 import qualified What4.ExprHelpers as WEH
 import qualified Data.BitVector.Sized as BV
+import qualified Pate.ExprMappable as PEM
 
 validInitState ::
   forall sym arch v.
@@ -112,9 +113,10 @@ validRegister mblockStart entry r = withSym $ \sym -> do
 
 
 collectPointerAssertions ::
-  forall sym arch tp.
-  W4.SymExpr sym tp ->
-  EquivM sym arch (W4.SymExpr sym tp, AssumptionSet sym)
+  forall sym arch f.
+  PEM.ExprMappable sym f =>
+  f ->
+  EquivM sym arch (f, AssumptionSet sym)
 collectPointerAssertions outer = withSym $ \sym -> do
   ptrAsserts <- CMR.asks envPtrAssertions
   cache <- W4B.newIdxCache
@@ -135,4 +137,4 @@ collectPointerAssertions outer = withSym $ \sym -> do
           if (W4B.nonceExprApp a0) == a0' then return e'
           else (liftIO $ W4B.sbNonceExpr sym a0')
         _ -> return e'
-  runWriterT $ go outer
+  runWriterT $ PEM.mapExpr sym go outer
diff --git a/src/Pate/Verification/Widening.hs b/src/Pate/Verification/Widening.hs
index ae3a86a9..b533a33f 100644
--- a/src/Pate/Verification/Widening.hs
+++ b/src/Pate/Verification/Widening.hs
@@ -29,7 +29,8 @@ module Pate.Verification.Widening
   , addRefinementChoice
   , traceEqCond
   , InteractiveBundle(..)
-  , getCounterExample
+  , getSomeGroundTrace
+  , getTraceFromModel
   ) where
 
 import           GHC.Stack
@@ -113,6 +114,7 @@ import Data.Kind (Type)
 import qualified Data.Aeson as JSON
 import qualified Prettyprinter as PP
 import qualified What4.Expr.GroundEval as W4
+import qualified Lang.Crucible.Utils.MuxTree as MT
 
 -- | Generate a fresh abstract domain value for the given graph node.
 --   This should represent the most information we can ever possibly
@@ -473,31 +475,51 @@ addRefinementChoice nd gr0 = withTracing @"message" "Modify Proof Node" $ do
       choice "Clear work list (unsafe!)" $ \_ gr4 ->
         return $ emptyWorkList gr4
 
+getSomeGroundTrace ::
+  SimBundle sym arch v ->
+  EquivM sym arch (CE.TraceEvents sym arch)
+getSomeGroundTrace bundle = withSym $ \sym -> do
+  (_, ptrAsserts) <- PVV.collectPointerAssertions bundle
+  
+  -- try to ground the model with a zero stack base, so calculated stack offsets
+  -- are the same as stack slots
+  stacks_zero <- PPa.catBins $ \bin -> do
+    in_ <- PPa.get bin (PS.simIn bundle)
+    let stackbase = PS.unSE $ PS.simStackBase (PS.simInState in_) 
+    zero <- liftIO $ W4.bvLit sym CT.knownRepr (BVS.mkBV CT.knownRepr 0)
+    PAs.fromPred <$> (liftIO $ W4.isEq sym zero stackbase)
+  
+  ptrAsserts_pred <- PAs.toPred sym (stacks_zero <> ptrAsserts)
+  -- first we try to see if we can make a model that doesn't
+  -- involve any invalid pointer operations
+  mevs <- goalSat "getCounterExample" ptrAsserts_pred $ \res -> case res of
+    Unsat _ -> emitWarning PEE.RequiresInvalidPointerOps >> return Nothing
+    Unknown -> emitWarning PEE.RequiresInvalidPointerOps >> return Nothing
+    Sat evalFn -> Just <$> getTraceFromModel evalFn bundle
+  case mevs of
+    Just evs -> return evs
+    -- otherwise, just try to get any model
+    Nothing -> goalSat "getCounterExample" (W4.truePred sym) $ \res -> case res of
+      Unsat _ -> throwHere PEE.InvalidSMTModel
+      Unknown -> throwHere PEE.InconclusiveSAT
+      Sat evalFn -> getTraceFromModel evalFn bundle
 
 -- | Compute a counter-example for a given predicate
-getCounterExample ::
+getTraceFromModel ::
+  forall sym arch v.
+  SymGroundEvalFn sym ->
   SimBundle sym arch v ->
-  W4.Pred sym -> 
-  EquivM sym arch (CE.ObservableCheckResult sym arch)
-getCounterExample bundle p = withSym $ \sym -> do
-  evs <- PPa.forBinsC $ \bin -> do
-    out <- PPa.get bin (PS.simOut bundle)
-    let mem = PS.simOutMem out
-    liftIO (MT.observableEvents sym (\_ -> return $ W4.truePred sym) mem)
-  not_p <- liftIO $ W4.notPred sym p
-  goalSat "getCounterExample" not_p $ \res -> case res of
-    Unsat _ -> return CE.ObservableCheckEq
-    Unknown -> return (CE.ObservableCheckError "UNKNOWN result when checking observable sequences")
-    Sat evalFn' -> CE.ObservableCheckCounterexample <$> do
-      -- FIXME: counter-example should use patchpair
-      let join_ce (r,s) (r',s') =
-            return $ ObservableCounterexample (CE.RegsCounterExample r r') s s'
-      PPa.joinPatchPred join_ce $ \bin -> do
-        in_ <- PPa.get bin (PS.simIn bundle)
-        sym_seq <- PPa.getC bin evs
-        ground_regs <- MM.traverseRegsWith (\_ -> PEM.mapExpr sym (\x -> concretizeWithModel evalFn' x)) (PS.simInRegs in_)
-        ground_seq <- withGroundEvalFn evalFn' $ \evalFn -> reverse <$> CE.groundObservableSequence sym evalFn sym_seq
-        return (ground_regs, ground_seq)
+  EquivM sym arch (CE.TraceEvents sym arch)
+getTraceFromModel evalFn' bundle = fmap CE.TraceEvents $ withSym $ \sym -> PPa.forBinsC $ \bin -> do
+  out <- PPa.get bin (PS.simOut bundle)
+  in_ <- PPa.get bin (PS.simIn bundle)
+  let mem = PS.simOutMem out
+  withGroundEvalFn evalFn' $ \evalFn -> do
+    evs <- CE.groundTraceEventSequence sym evalFn (MT.memFullSeq @_ @arch mem)
+    let in_regs = PS.simInRegs in_
+    ground_rop <- CE.groundRegOp sym evalFn (MT.RegOp (MM.regStateMap in_regs))
+    -- create a dummy initial register op representing the initial values
+    return (ground_rop, evs)
 
 applyDomainRefinements ::
   PS.SimScope sym arch v ->
@@ -1348,8 +1370,13 @@ widenPostcondition scope bundle preD postD0 = do
       eqPost <- liftIO $ PEq.getPostdomain sym scope bundle eqCtx (PAD.absDomEq preD) (PAD.absDomEq postD0)
       eqPost_pred <- liftIO $ postCondPredicate sym eqPost
       withTracing @"message" "Equivalence Counter-example" $ do
-        res <- getCounterExample bundle eqPost_pred
-        emitTrace @"observable_result" res
+        not_eqPost_pred <- liftIO $ W4.notPred sym eqPost_pred
+        mres <- withSatAssumption (PAs.fromPred not_eqPost_pred) $ do
+          res <- getSomeGroundTrace bundle
+          emitTrace @"trace_events" res
+        case mres of
+          Just () -> return ()
+          Nothing -> emitWarning (PEE.WideningError "Couldn't find widening counter-example")
         return r
     _ -> return r
  where