diff --git a/arch/Pate/PPC.hs b/arch/Pate/PPC.hs
index cf5287b6..96190675 100644
--- a/arch/Pate/PPC.hs
+++ b/arch/Pate/PPC.hs
@@ -273,7 +273,7 @@ argumentMapping :: (1 <= SP.AddrWidth v) => PVO.ArgumentMapping (PPC.AnyPPC v)
 argumentMapping = undefined
 
 
-specializedBufferWrite :: forall arch v. (arch ~ PPC.AnyPPC v, 16 <= SP.AddrWidth v, MS.SymArchConstraints arch) => PA.StubOverride arch
+specializedBufferWrite :: forall arch v. (arch ~ PPC.AnyPPC v, PA.ValidArch (PPC.AnyPPC v)) => PA.StubOverride arch
 specializedBufferWrite = 
     PA.mkEventOverride "CFE_SB_TransmitBuffer" mkEvent 0x30 (gpr 3) (gpr 3)
     where
@@ -294,7 +294,7 @@ specializedBufferWrite =
         WI.baseTypeIte sym is_expect expect_value' zero
 
 -- FIXME: flags to make it equal?
-specializeSocketRead :: forall arch v. (Typeable arch, arch ~ PPC.AnyPPC v, 16 <= SP.AddrWidth v, MS.SymArchConstraints arch) => PA.StubOverride arch
+specializeSocketRead :: forall arch v. (arch ~ PPC.AnyPPC v, PA.ValidArch (PPC.AnyPPC v)) => PA.StubOverride arch
 specializeSocketRead = 
     PA.mkReadOverride "OS_SocketRecvFrom" (PPa.PatchPairSingle PB.PatchedRepr (Const f)) addrs lengths (gpr 3) (gpr 4) (gpr 5) (gpr 3)
     where
@@ -308,7 +308,7 @@ specializeSocketRead =
       f = PA.modifyConcreteChunk MC.BigEndian WI.knownNat (0x300 :: Integer) 2 4
 
 -- FIXME: clagged directly from ARM, registers may not be correct
-stubOverrides :: (Typeable (PPC.AnyPPC v), MS.SymArchConstraints (PPC.AnyPPC v), 1 <= SP.AddrWidth v, 16 <= SP.AddrWidth v) => PA.ArchStubOverrides (PPC.AnyPPC v)
+stubOverrides :: PA.ValidArch (PPC.AnyPPC v) => PA.ArchStubOverrides (PPC.AnyPPC v)
 stubOverrides = PA.ArchStubOverrides (PA.mkDefaultStubOverride "__pate_stub" r3 ) $ \fs ->
   lookup (PBl.fnSymBase fs) override_list
   where
diff --git a/pate_binja/pate.py b/pate_binja/pate.py
index e342a94b..bec7e13d 100644
--- a/pate_binja/pate.py
+++ b/pate_binja/pate.py
@@ -617,9 +617,7 @@ def processFinalResult(self, traceConstraints: Optional[list[tuple[TraceVar, str
             if not lastTopLevelResult:
                 out.write(f'No equivalence conditions found\n')
             else:
-                eqStatus = lastTopLevelResult.get('content', {}).get('eq_status')
-                out.write(f'Equivalence status: {eqStatus}\n')
-                out.write('\n')
+
                 eqconds = lastTopLevelResult.get('content', {}).get('eq_conditions', {}).get('map')
                 if eqconds:
                     # Found eq conditions
@@ -639,9 +637,9 @@ def processFinalResult(self, traceConstraints: Optional[list[tuple[TraceVar, str
 
                         # print('CFAR id:', node_id)
 
-                        out.write(f'Equivalence condition for {node_id}\n')
+                        out.write(f'Equivalence condition for {node_id}:\n')
                         pprint_symbolic(out, predicate)
-                        out.write('\n')
+                        out.write('\n\n')
 
                         # out.write('\nTrace True\n')
                         # pprint_node_event_trace(trace_true, 'True Trace', out=out)
@@ -656,7 +654,10 @@ def processFinalResult(self, traceConstraints: Optional[list[tuple[TraceVar, str
                     ect.trace_false = False
                     ect.traceConstraints = traceConstraints
                     ect.predicate = ect.unconstrainedPredicate
-
+                
+                eqStatus = lastTopLevelResult.get('content', {}).get('eq_status').get('message')
+                out.write(f'Equivalence status: {eqStatus}\n')
+                
             self.user.show_message(out.getvalue())
         if self.last_cfar_graph:
             self.user.show_cfar_graph(self.last_cfar_graph)
@@ -1504,7 +1505,7 @@ def pprint_node_event_trace_domain(trace, pre: str = '', out: IO = sys.stdout):
     # possibly not obvious why a given trace violates the post-condition, which is why I
     # think we included it in the first place.
     if not (postcond):
-        out.write(f'{pre}No Post Condition.\n')
+        out.write(f'{pre}')
         return
 
     if precond:
@@ -1615,6 +1616,8 @@ def pprint_mem_op(mem_op: dict, pre: str = '', out: IO = sys.stdout, prune_zero:
 def pretty_call_arg(arg):
     if isinstance(arg, dict) and 'data_expr' in arg:
         return str(arg['data_expr'])
+    elif isinstance(arg, dict) and 'pointer' in arg:
+      return (get_value_id(arg['pointer']))
     else:
         return str(arg)
 
diff --git a/pate_binja/view.py b/pate_binja/view.py
index 88de9620..4cb760f8 100644
--- a/pate_binja/view.py
+++ b/pate_binja/view.py
@@ -457,7 +457,7 @@ def setTracePosVsNeg(self, posTrace: Optional[dict], negTrace: Optional[dict], b
             self.traceDiff.clear('None')
             return
 
-        self._setDomainText('NA')
+        self._setDomainText('')
 
         pw: Optional[PateWidget] = getAncestorInstanceOf(self, PateWidget)
 
@@ -552,7 +552,18 @@ def __init__(self, cfarNode,
         self.eqCondField.setReadOnly(True)
         self.eqCondField.setMaximumBlockCount(1000)
         eqCondBoxLayout = QVBoxLayout()
-        eqCondBoxLayout.addWidget(QLabel("Programs behave equivalently when:"))
+        label_prefix = ''
+        match label:
+          case 'Asserted Condition':
+            label_prefix = 'Asserted precondition'
+          case 'Assumed Condition':
+            label_prefix = 'Assumed precondition'
+          case 'Equivalence Condition':
+            label_prefix = 'Assumed equivalence condition'
+          case _:
+            label_prefix = 'Precondition'
+
+        eqCondBoxLayout.addWidget(QLabel(f'{label_prefix} (assuming all ancestor preconditions):'))
         eqCondBoxLayout.addWidget(self.eqCondField)
         eqCondBox = QWidget()
         eqCondBox.setLayout(eqCondBoxLayout)
@@ -570,8 +581,8 @@ def __init__(self, cfarNode,
         # Diff Mode Control
         diffModeLabel = QLabel("Difference mode:")
         self.diffModeComboBox = QComboBox()
-        self.diffModeComboBox.addItem("Original VS Patched")
-        self.diffModeComboBox.addItem("Equivalent VS Different")
+        self.diffModeComboBox.addItem("Original vs. Patched")
+        self.diffModeComboBox.addItem("Condition assumed TRUE vs. FALSE")
         self.diffModeComboBox.currentTextChanged.connect(self.diffModeChanged)
         diffModeBoxLayout = QHBoxLayout()
         diffModeBoxLayout.addWidget(diffModeLabel)
@@ -638,14 +649,14 @@ def updateFromCfarNode(self):
                 else:
                     out.write('\nEquivalence condition unsatisfiable with user-supplied constraints.\n')
             else:
-                out.write('\nNo user-supplied trace constraints.\n')
+                out.write('')
             self.eqCondField.appendPlainText(out.getvalue())
-        if self.diffModeComboBox.currentText() == "Original VS Patched":
+        if self.diffModeComboBox.currentText() == "Original vs. Patched":
             # Original VS Patch Diff Mode
             self.trueTraceWidget.setTrace(self.conditionTrace.trace_true)
-            self.trueTraceLabel.setText('Trace showing EQUIVALENT behaviour, original vs patched:')
+            self.trueTraceLabel.setText('Trace assuming above condition is TRUE, original vs. patched:')
             self.falseTraceWidget.setTrace(self.conditionTrace.trace_false)
-            self.falseTraceLabel.setText('Trace showing DIFFERENT behaviour, original vs patched:')
+            self.falseTraceLabel.setText('Trace assuming above condition is FALSE, original vs. patched:')
         else:
             # Positive VS Negative Diff Mode
             # TODO: What about conditions in this mode? Drop?
@@ -672,9 +683,9 @@ def updateFromCfarNode(self):
                 pbv = None
 
             self.trueTraceWidget.setTracePosVsNeg(originalPosTrace, originalNegTrace, pbv)
-            self.trueTraceLabel.setText('Trace showing original program, EQUIVALENT vs DIFFERENT behaviour:')
+            self.trueTraceLabel.setText('Trace for original, assuming above condition is TRUE vs. FALSE:')
             self.falseTraceWidget.setTracePosVsNeg(patchedPosTrace, patchedNegTrace, obv)
-            self.falseTraceLabel.setText('Trace showing patched program, EQUIVALENT vs DIFFERENT behaviour:')
+            self.falseTraceLabel.setText('Trace for patched, assuming above condition is TRUE vs. FALSE:')
 
     def diffModeChanged(self, text):
         print('Difference mode:', self.diffModeComboBox.currentText())
diff --git a/src/Pate/Arch.hs b/src/Pate/Arch.hs
index dabc7b47..1675855a 100644
--- a/src/Pate/Arch.hs
+++ b/src/Pate/Arch.hs
@@ -128,6 +128,7 @@ import Data.Maybe
 import Pate.Memory
 import qualified Pate.ExprMappable as PEM
 import Control.Monad (forM)
+import qualified Pate.Pointer as Ptr
 
 -- | The type of architecture-specific dedicated registers
 --
@@ -341,20 +342,18 @@ defaultStubOverride va = let ArchStubOverrides _default _ = validArchStubOverrid
 --   restrictions on the size of regions.
 mkMallocOverride ::
   forall arch.
-  16 <= MC.ArchAddrWidth arch =>
-  MS.SymArchConstraints arch =>
+  ValidArch arch =>
   MC.ArchReg arch (MT.BVType (MC.ArchAddrWidth arch)) {- ^ length argument (unused currently ) -} ->
   MC.ArchReg arch (MT.BVType (MC.ArchAddrWidth arch)) {- ^ register for fresh pointer -} ->
   StubOverride arch
 mkMallocOverride _rLen rOut = mkStubOverride $ \sym st -> do
   (fresh_ptr, st') <- freshAlloc sym Nothing st
-  return (st' { PS.simRegs = ((PS.simRegs st) & (MC.boundValue rOut) .~ fresh_ptr) })
+  updateRegister sym rOut fresh_ptr st'
 
 mkMallocOverride' ::
   forall arch.
   16 <= MC.ArchAddrWidth arch =>
-  MS.SymArchConstraints arch =>
-  Typeable arch =>
+  ValidArch arch =>
   Maybe (MemLocation (MC.ArchAddrWidth arch)) ->
   MC.ArchReg arch (MT.BVType (MC.ArchAddrWidth arch)) {- ^ write fresh pointer here -} ->
   MC.ArchReg arch (MT.BVType (MC.ArchAddrWidth arch)) {- ^ register for fresh pointer -} ->
@@ -382,7 +381,7 @@ mkMallocOverride' bufOverride rPtrLoc rOut = StubOverride $ \sym archInfo _wsolv
     nullPtr <- IO.liftIO $ CLM.mkNullPointer sym w_mem
 
     ptr' <- IO.liftIO $ PMT.muxPtr sym alloc_success (PSR.macawRegValue fresh_ptr) nullPtr
-    return (st' { PS.simRegs = ((PS.simRegs st) & (MC.boundValue rOut) .~ (PSR.ptrToEntry ptr')) })
+    updateRegister sym rOut (PSR.ptrToEntry ptr') st'
 
   -- | Return a freshly-allocated pointer with an optional region override.
 --   New max region is set to the given region + 1 if it is greater than the current max
@@ -422,17 +421,15 @@ freshAlloc sym mregion st = do
 --  but provably equal between the programs provided they happen in the same order.
 mkClockOverride ::
   forall arch.
-  16 <= MC.ArchAddrWidth arch =>
-  MS.SymArchConstraints arch =>
+  ValidArch arch =>
   MC.ArchReg arch (MT.BVType (MC.ArchAddrWidth arch)) {- ^ return register -} ->
   StubOverride arch
 mkClockOverride rOut = StubOverride $ \sym _ _ -> do
   let w = MC.memWidthNatRepr @(MC.ArchAddrWidth arch)
   fresh_bv <- W4.freshConstant sym (W4.safeSymbol "current_time") (W4.BaseBVRepr w)
   return $ StateTransformer $ \st -> do
-    zero_nat <- W4.natLit sym 0
-    let ptr = PSR.ptrToEntry (CLM.LLVMPointer zero_nat fresh_bv)
-    return (st { PS.simRegs = ((PS.simRegs st) & (MC.boundValue rOut) .~ ptr) })
+    val <- PSR.bvToEntry sym fresh_bv
+    updateRegister sym rOut val st
 
 applyConcreteOverride :: 
   LCB.IsSymInterface sym =>
@@ -456,7 +453,7 @@ applyConcreteOverride sym bin overridePair e = case PPa.getC bin overridePair of
 mkObservableOverride ::
   forall arch.
   16 <= MC.ArchAddrWidth arch =>
-  MS.SymArchConstraints arch =>
+  ValidArch arch =>
   T.Text {- ^ name of call -} ->
   MC.ArchReg arch (MT.BVType (MC.ArchAddrWidth arch)) {- ^ return -} ->
   [MC.ArchReg arch (MT.BVType (MC.ArchAddrWidth arch))] {- ^ args -} ->
@@ -475,17 +472,15 @@ mkObservableOverride nm return_reg arg_regs = StubOverride $ \sym _archInfo _wso
     bv_fn <- W4U.mkUninterpretedSymFn sym ("written_" ++ show nm) reprsCtx (W4.BaseBVRepr w_mem)
 
     let mem = PS.simMem st
-    mem' <- PMT.addExternalCallEvent sym nm argsCtx mem
-    let st' = st { PS.simMem = mem' }
-    zero_nat <- W4.natLit sym 0
+    mem' <- PMT.addExternalCallEvent sym nm argsCtx True mem 
     fresh_bv <- W4.applySymFn sym bv_fn argsCtx
-    let ptr = PSR.ptrToEntry (CLM.LLVMPointer zero_nat fresh_bv)
-    return (st' { PS.simRegs = ((PS.simRegs st') & (MC.boundValue return_reg) .~ ptr ) })
+    val <- PSR.bvToEntry sym fresh_bv
+    updateRegister sym return_reg val (st { PS.simMem = mem' })
 
 mkEventOverride ::
   forall arch ptrW.
   16 <= MC.ArchAddrWidth arch =>
-  MS.SymArchConstraints arch =>
+  ValidArch arch =>
   ptrW ~ (MC.ArchAddrWidth arch) =>
   T.Text {- ^ name of call -} ->
   (forall sym. LCB.IsSymInterface sym => sym -> PMT.MemChunk sym ptrW -> IO (W4.SymBV sym ptrW)) {- ^ compute return value for read chunk -} ->
@@ -507,10 +502,9 @@ mkEventOverride nm readChunk len buf_reg rOut = StubOverride $ \(sym :: sym) _ar
   len_sym <- W4.bvLit sym ptrW (BVS.mkBV ptrW (fromIntegral len))
   bytes_chunk <- PMT.readChunk sym (PMT.memState mem) buf_ptr len_sym
   written <- readChunk sym bytes_chunk
-  mem' <- PMT.addExternalCallEvent sym nm (Ctx.empty Ctx.:> written) mem
-  result <- PSR.bvToEntry sym written 
-  return (st' { PS.simMem = mem', PS.simRegs = ((PS.simRegs st) & (MC.boundValue rOut) .~ result ) })
-
+  mem' <- PMT.addExternalCallEvent sym nm (Ctx.empty Ctx.:> written) True mem
+  result <- PSR.bvToEntry sym written
+  updateRegister sym rOut result (st' { PS.simMem = mem' })
 
 newtype MemChunkModify ptrW =
   MemChunkModify { mkMemChunk :: (forall sym. LCB.IsSymInterface sym => sym -> PMT.MemChunk sym ptrW -> IO (PMT.MemChunk sym ptrW)) }
@@ -616,8 +610,7 @@ resolveMemLocation sym mem endianness loc  = case loc of
 mkReadOverride ::
   forall arch.
   16 <= MC.ArchAddrWidth arch =>
-  MS.SymArchConstraints arch =>
-  Typeable arch =>
+  ValidArch arch =>
   T.Text {- ^ name of call -} ->
   PPa.PatchPairC (MemChunkModify (MC.ArchAddrWidth arch)) {- ^ mutator for incoming symbolic data -} ->
   PPa.PatchPairC (Maybe (MemLocation (MC.ArchAddrWidth arch))) {- ^ concrete override for buffer address (pointer to buffer pointer) -} ->
@@ -711,7 +704,7 @@ mkReadOverride nm chunkOverrides bufferOverrides lenOverrides src_reg buf_reg le
 readTransformer ::
   forall sym arch bin v.
   16 <= MC.ArchAddrWidth arch =>
-  MS.SymArchConstraints arch =>
+  ValidArch arch =>
   LCB.IsSymInterface sym =>
   sym ->
   MI.ArchitectureInfo arch ->
@@ -736,17 +729,16 @@ readTransformer sym archInfo _src_val buf rOut cond chunk st = do
   zero <- IO.liftIO $ W4.bvLit sym ptrW (BVS.zero ptrW)
   -- either the chunk is written or it's not and we return zero bytes written
   written <- IO.liftIO $ W4.baseTypeIte sym cond (PMT.memChunkLen chunk) zero
-  zero_nat <- IO.liftIO $ W4.natLit sym 0
-  let written_result = PSR.ptrToEntry (CLM.LLVMPointer zero_nat written)
+  written_result <- PSR.bvToEntry sym written
   -- FIXME: currently these are all unsigned values, but likely this return value will be treated as signed
   -- where negative values represent different error conditions
-  return (st { PS.simMem = mem', PS.simRegs = ((PS.simRegs st) & (MC.boundValue rOut) .~ written_result ) })
+  updateRegister sym rOut written_result (st { PS.simMem = mem' })
 
 --  SymExpr sym (BaseArrayType (Ctx.EmptyCtx Ctx.::> BaseBVType ptrW) (BaseBVType 8))
 mkWriteOverride ::
   forall arch.
   16 <= MC.ArchAddrWidth arch =>
-  MS.SymArchConstraints arch =>
+  ValidArch arch =>
   T.Text {- ^ name of call -} ->
   MC.ArchReg arch (MT.BVType (MC.ArchAddrWidth arch)) {- ^ fd -} ->
   MC.ArchReg arch (MT.BVType (MC.ArchAddrWidth arch)) {- ^ buf -} ->
@@ -770,7 +762,7 @@ mkWriteOverride nm fd_reg buf_reg flen rOut = StubOverride $ \sym archInfo wsolv
         -- endianness doesn't really matter, as long as we're consistent
         let memrepr = MC.BVMemRepr w (MI.archEndianness archInfo)
         (CLM.LLVMPointer region val_bv) <- PMT.readMemState sym (PMT.memState mem) (PMT.memBaseMemory mem) buf_ptr memrepr
-        mem' <- PMT.addExternalCallEvent sym nm (Ctx.empty Ctx.:> fd_bv Ctx.:> val_bv Ctx.:> W4.natToIntegerPure region) mem
+        mem' <- PMT.addExternalCallEvent sym nm (Ctx.empty Ctx.:> fd_bv Ctx.:> val_bv Ctx.:> W4.natToIntegerPure region) True mem
         -- globally-unique
         bv_fn <- W4U.mkUninterpretedSymFn sym (show nm ++ "sz") (Ctx.empty Ctx.:> (W4.exprType val_bv)) (W4.BaseBVRepr w_mem)
         sz <- W4.applySymFn sym bv_fn (Ctx.empty Ctx.:> val_bv)
@@ -793,21 +785,31 @@ mkWriteOverride nm fd_reg buf_reg flen rOut = StubOverride $ \sym archInfo wsolv
         sz <- W4.applySymFn sym bv_fn (Ctx.empty Ctx.:> len_bv Ctx.:> first_byte Ctx.:> last_byte)
         return $ (st { PS.simMem = mem' },sz)
 
-    zero_nat <- W4.natLit sym 0
     -- we're returning a symbolic result representing the number of bytes written, so
     -- we clamp this explicitly to the given write length
     zero_ptr <- W4.bvLit sym w_mem (BVS.mkBV w_mem 0)
     sz_is_bounded <- W4.bvUle sym len_bv' sz
     bounded_sz <- W4.baseTypeIte sym sz_is_bounded sz zero_ptr
-    let ptr = PSR.ptrToEntry (CLM.LLVMPointer zero_nat bounded_sz)
-    return (st' { PS.simRegs = ((PS.simRegs st') & (MC.boundValue rOut) .~ ptr ) })
-
+    val <- IO.liftIO $ PSR.bvToEntry sym bounded_sz
+    updateRegister sym rOut val st'
 
+updateRegister ::
+  IO.MonadIO m =>
+  LCB.IsSymInterface sym =>
+  ValidArch arch =>
+  sym ->
+  MC.ArchReg arch (MT.BVType (MC.ArchAddrWidth arch)) ->
+  PSR.MacawRegEntry sym (MT.BVType (MC.ArchAddrWidth arch)) ->
+  PS.SimState sym arch bin v ->
+  m (PS.SimState sym arch bin v)
+updateRegister sym rOut val st = do
+  mem' <- IO.liftIO $ PMT.addRegEvent sym (PMT.RegOp $ MapF.singleton rOut val) (PS.simMem st)
+  return (st { PS.simRegs = ((PS.simRegs st) & (MC.boundValue rOut) .~ val), PS.simMem = mem' }) 
 
 -- | Default override returns the same arbitrary value for both binaries
 mkDefaultStubOverride ::
   forall arch.
-  MS.SymArchConstraints arch =>
+  ValidArch arch =>
   String -> 
   MC.ArchReg arch (MT.BVType (MC.ArchAddrWidth arch)) {- ^ return register -} ->
   StubOverride arch
@@ -815,26 +817,25 @@ mkDefaultStubOverride nm rOut = StubOverride $ \sym _ _ -> do
   let w = MC.memWidthNatRepr @(MC.ArchAddrWidth arch)
   fresh_bv <- W4.freshConstant sym (W4.safeSymbol nm) (W4.BaseBVRepr w)
   return $ StateTransformer $ \st -> do
-    zero_nat <- W4.natLit sym 0
-    let ptr = PSR.ptrToEntry (CLM.LLVMPointer zero_nat fresh_bv)
-    return (st { PS.simRegs = ((PS.simRegs st) & (MC.boundValue rOut) .~ ptr) })
+    val <- PSR.bvToEntry sym fresh_bv
+    updateRegister sym rOut val st
 
 -- | Default override returns the same arbitrary value for both binaries
 mkArgPassthroughOverride ::
   forall arch.
-  MS.SymArchConstraints arch =>
+  ValidArch arch =>
   MC.ArchReg arch (MT.BVType (MC.ArchAddrWidth arch)) {- ^ argument register -} ->
   MC.ArchReg arch (MT.BVType (MC.ArchAddrWidth arch)) {- ^ return register -} ->
   StubOverride arch
-mkArgPassthroughOverride rArg rOut = StubOverride $ \_ _ _ -> return $ StateTransformer $ \st -> do
+mkArgPassthroughOverride rArg rOut = StubOverride $ \sym _ _ -> return $ StateTransformer $ \st -> do
   let arg = (PS.simRegs st) ^. MC.boundValue rArg
-  return (st { PS.simRegs = ((PS.simRegs st) & (MC.boundValue rOut) .~ arg) })
+  updateRegister sym rOut arg st
 
 -- | Default override returns the same arbitrary value for both binaries, based on the input
 --   registers
 mkDefaultStubOverrideArg ::
   forall arch.
-  MS.SymArchConstraints arch =>
+  ValidArch arch =>
   String ->
   [Some (MC.ArchReg arch)] {- ^ argument registers -} ->
   MC.ArchReg arch (MT.BVType (MC.ArchAddrWidth arch)) {- ^ return register -} ->
@@ -843,27 +844,37 @@ mkDefaultStubOverrideArg nm rArgs rOut = StubOverride $ \sym _ _ -> do
   let w = MC.memWidthNatRepr @(MC.ArchAddrWidth arch)
 
   return $ StateTransformer $ \st -> do
-    zero_nat <- W4.natLit sym 0
-    vals <- mapM (\(Some r) -> getType sym (PS.simRegs st ^. MC.boundValue r)) rArgs
-    Some vals_ctx <- return $ Ctx.fromList vals
+    datas <- concat <$> mapM (\(Some r) -> getType sym (PS.simRegs st ^. MC.boundValue r)) rArgs
+    dataExprs <- PEM.foldExpr sym (\e_ es_ -> return (Some e_:es_)) datas [] 
+    Some vals_ctx <- return $ Ctx.fromList (reverse dataExprs)
     -- globally unique function
     result_fn <- W4U.mkUninterpretedSymFn sym nm (TFC.fmapFC W4.exprType vals_ctx) (W4.BaseBVRepr w)
     fresh_bv <- W4.applySymFn sym result_fn vals_ctx
-    let ptr = PSR.ptrToEntry (CLM.LLVMPointer zero_nat fresh_bv)
-    return (st { PS.simRegs = ((PS.simRegs st) & (MC.boundValue rOut) .~ ptr) })
+    let mem0 = PS.simMem st
+    -- add unobservable event, so this call appears in the trace
+    mem1 <- case fromRegisterDisplay (displayRegister rOut) of
+      Just rOutNm -> do
+        -- TODO: this is a quick solution to indicate where the result of
+        -- the call was saved. Ideally there would be a formal slot in the
+        -- event to store this information.
+        let nm' = rOutNm ++ " <- " ++ nm
+        IO.liftIO $ PMT.addMemEvent sym (PMT.ExternalCallEventHidden (T.pack nm') datas) mem0
+      Nothing -> IO.liftIO $ PMT.addMemEvent sym (PMT.ExternalCallEventHidden (T.pack nm) datas) mem0
+    val <- IO.liftIO $ PSR.bvToEntry sym fresh_bv
+    updateRegister sym rOut val (st { PS.simMem = mem1 })
+
   where
     getType :: 
       W4.IsExprBuilder sym => 
       sym -> 
       PSR.MacawRegEntry sym tp -> 
-      IO (Some (W4.SymExpr sym))
-    getType sym r = case PSR.macawRegRepr r of
-      CLM.LLVMPointerRepr{} -> do
-        let CLM.LLVMPointer reg off = PSR.macawRegValue r
-        let iRegion = W4.natToIntegerPure reg
-        Some <$> W4.mkStruct sym (Ctx.empty Ctx.:> iRegion Ctx.:> off)
-      LCT.BoolRepr -> return $ Some $ PSR.macawRegValue r
-      LCT.StructRepr Ctx.Empty -> Some <$> W4.mkStruct sym Ctx.empty
+      IO [PMT.ExternalCallData sym (MC.ArchAddrWidth arch)]
+    getType _sym r = case PSR.macawRegRepr r of
+      CLM.LLVMPointerRepr{} -> 
+        return $ [PMT.ExternalCallDataPointer (Ptr.fromLLVMPointer $ PSR.macawRegValue r )]
+
+      LCT.BoolRepr -> return $ [PMT.ExternalCallDataExpr $ PSR.macawRegValue r]
+      LCT.StructRepr Ctx.Empty -> return []
       x -> error $ "mkDefaultStubOverrideArg: unsupported type" ++ show x
 
 -- | No-op stub
diff --git a/src/Pate/Equivalence.hs b/src/Pate/Equivalence.hs
index 3f97dbc9..c97ecd23 100644
--- a/src/Pate/Equivalence.hs
+++ b/src/Pate/Equivalence.hs
@@ -54,6 +54,7 @@ module Pate.Equivalence
 
 import           Control.Lens hiding ( op, pre, (.=) )
 import           Control.Monad ( foldM )
+import qualified Prettyprinter as PP
 import           Data.Parameterized.Classes
 import           Data.Parameterized.Some
 import qualified Data.Parameterized.TraversableF as TF
@@ -93,17 +94,18 @@ import           What4.JSON ((.=))
 
 data EquivalenceStatus =
     Equivalent
-  | Inequivalent
+  | Inequivalent [String]
   | ConditionallyEquivalent
-  | Errored PEE.EquivalenceError
+  | Errored [PEE.EquivalenceError]
 
 deriving instance Show EquivalenceStatus
 
 instance Semigroup EquivalenceStatus where
   Errored err <> _ = Errored err
   _ <> Errored err = Errored err
-  Inequivalent <> _ = Inequivalent
-  _ <> Inequivalent = Inequivalent
+  Inequivalent msg1 <> Inequivalent msg2 = Inequivalent (msg1 ++ msg2)
+  Inequivalent msg1 <> _ = Inequivalent msg1
+  _ <> Inequivalent msg2 = Inequivalent msg2
   ConditionallyEquivalent <> _ = ConditionallyEquivalent
   _ <> ConditionallyEquivalent = ConditionallyEquivalent
   Equivalent <> Equivalent = Equivalent
@@ -111,13 +113,21 @@ instance Semigroup EquivalenceStatus where
 instance Monoid EquivalenceStatus where
   mempty = Equivalent
 
-instance IsTraceNode k "equivalence_result" where
-  type TraceNodeType k "equivalence_result" = EquivalenceStatus
-  prettyNode () = \case
+instance PP.Pretty EquivalenceStatus where
+  pretty = \case
     Equivalent -> "Binaries are observably equivalent"
-    Inequivalent -> "Binaries are not observably equivalent"
+    Inequivalent msgs -> "Binaries are not observably equivalent" <> case msgs of
+      [] -> ""
+      _ -> ": " <> PP.hsep (map PP.pretty msgs)
     ConditionallyEquivalent -> "Binaries are conditionally, observably equivalent"
-    Errored{} -> "Analysis failure due to error"
+    Errored errs -> "Analysis failure due to error" <> case errs of
+      [] -> ""
+      [err] -> ": " <> PP.pretty err
+      _ -> "s: " <> PP.vsep (map PP.pretty errs)
+
+instance IsTraceNode k "equivalence_result" where
+  type TraceNodeType k "equivalence_result" = EquivalenceStatus
+  prettyNode () = PP.pretty
   nodeTags = mkTags @k @"equivalence_result" [Summary, Simplified]
 
 ---------------------------------------
diff --git a/src/Pate/EventTrace.hs b/src/Pate/EventTrace.hs
index 4c12e644..c52dc4c8 100644
--- a/src/Pate/EventTrace.hs
+++ b/src/Pate/EventTrace.hs
@@ -32,6 +32,8 @@ symbolic execution.
 
 module Pate.EventTrace
 ( MemEvent(..)
+, pattern ExternalCallEvent
+, pattern ExternalCallEventHidden
 , MemOp(..)
 , MemOpCondition(..)
 , MemOpDirection(..)
@@ -69,7 +71,7 @@ import qualified Data.Parameterized.Context as Ctx
 
 import           What4.Interface hiding ( integerToNat )
 
-import           Lang.Crucible.LLVM.MemModel (LLVMPtr, pattern LLVMPointer, ppPtr)
+import           Lang.Crucible.LLVM.MemModel (LLVMPtr, pattern LLVMPointer, ppPtr )
 import           Lang.Crucible.Utils.MuxTree ( MuxTree, viewMuxTree )
 import           Lang.Crucible.Simulator.SymSequence ( SymSequence(..), muxSymSequence, evalWithFreshCache, nilSymSequence, consSymSequence, appendSymSequence, isNilSymSequence, traverseSymSequence )
 
@@ -297,27 +299,40 @@ data MemEvent sym ptrW where
     SymBV sym w
       {- ^ Value of r0 during this syscall -} ->
     MemEvent sym ptrW
-  ExternalCallEvent :: forall sym ptrW.
+  ExternalCallEventGen :: forall sym ptrW.
     Text ->
     [ExternalCallData sym ptrW] {- ^ relevant data for this visible call -} ->
+    Bool {- ^ true if this external call is considered observable -} ->
     MemEvent sym ptrW
 
+pattern ExternalCallEvent :: Text -> [ExternalCallData sym ptrW] -> MemEvent sym ptrW
+pattern ExternalCallEvent nm args = ExternalCallEventGen nm args True
+
+pattern ExternalCallEventHidden :: Text -> [ExternalCallData sym ptrW] -> MemEvent sym ptrW
+pattern ExternalCallEventHidden nm args = ExternalCallEventGen nm args False
+
+{-# COMPLETE  MemOpEvent, SyscallEvent, ExternalCallEvent, ExternalCallEventHidden #-}
+
 data ExternalCallData sym ptrW =
     forall tp. ExternalCallDataExpr (SymExpr sym tp)
+  | forall w. 1 <= w => ExternalCallDataPointer (Ptr.Pointer sym w)
   | ExternalCallDataChunk (MemChunk sym ptrW)
 
 instance PEM.ExprMappable sym (ExternalCallData sym ptrW) where
   mapExpr sym f = \case
     ExternalCallDataExpr e -> ExternalCallDataExpr <$> f e
+    ExternalCallDataPointer ptr -> ExternalCallDataPointer <$> PEM.mapExpr sym f ptr
     ExternalCallDataChunk c -> ExternalCallDataChunk <$> PEM.mapExpr sym f c
 
 instance PEM.ExprFoldable sym (ExternalCallData sym ptrW) where
   foldExpr sym f ec b = case ec of
     ExternalCallDataExpr e -> f e b
+    ExternalCallDataPointer ptr -> PEM.foldExpr sym f ptr b
     ExternalCallDataChunk c -> PEM.foldExpr sym f c b
 
 instance W4S.SerializableExprs sym => W4S.W4Serializable sym (ExternalCallData sym ptrW) where
   w4Serialize (ExternalCallDataExpr e) = W4S.object ["data_expr" .== e]
+  w4Serialize (ExternalCallDataPointer ptr) = W4S.object ["pointer" .== ptr]
   w4Serialize (ExternalCallDataChunk c) = W4S.object ["mem_chunk" .= c]
 
 instance OrdF (SymExpr sym) => Eq (ExternalCallData sym ptrW) where
@@ -326,8 +341,18 @@ instance OrdF (SymExpr sym) => Eq (ExternalCallData sym ptrW) where
 instance OrdF (SymExpr sym) => Ord (ExternalCallData sym ptrW) where
   compare (ExternalCallDataExpr e1) (ExternalCallDataExpr e2) = toOrdering $ compareF e1 e2
   compare (ExternalCallDataChunk c1) (ExternalCallDataChunk c2) = compare c1 c2
+  compare (ExternalCallDataPointer ptr1) (ExternalCallDataPointer ptr2) = 
+    toOrdering $  compareF ptr1 ptr2
+
+  compare (ExternalCallDataExpr{}) (ExternalCallDataPointer{}) = LT
   compare (ExternalCallDataExpr{}) (ExternalCallDataChunk{}) = LT
+
+  compare (ExternalCallDataPointer{}) (ExternalCallDataExpr{}) = GT
+  compare (ExternalCallDataPointer{}) (ExternalCallDataChunk{}) = LT
+
   compare (ExternalCallDataChunk{}) (ExternalCallDataExpr{})  = GT
+  compare (ExternalCallDataChunk{}) (ExternalCallDataPointer{})  = GT
+
 
 groundExternalCallData ::
   forall sym ptrW t st fs. sym ~ W4B.ExprBuilder t st fs =>
@@ -340,6 +365,7 @@ groundExternalCallData sym evalFn = \case
   ExternalCallDataExpr e -> ExternalCallDataExpr <$> do
     e_g <- W4G.groundEval evalFn e
     PVC.symbolicFromConcrete sym e_g e
+  ExternalCallDataPointer ptr -> ExternalCallDataPointer <$> Ptr.groundPtr sym evalFn ptr
   ExternalCallDataChunk (MemChunk mem base len) -> ExternalCallDataChunk <$> do
     let ptrW = memWidthNatRepr @ptrW
     base_g <- W4G.groundEval evalFn base
@@ -370,6 +396,8 @@ compareExternalCallData ::
 compareExternalCallData sym ec1 ec2 = case (ec1, ec2) of
   (ExternalCallDataExpr e1, ExternalCallDataExpr e2) | Just Refl <- testEquality (exprType e1) (exprType e2) ->
     isEq sym e1 e2
+  (ExternalCallDataPointer ptr1, ExternalCallDataPointer ptr2) ->
+    Ptr.ptrEq sym ptr1 ptr2
   (ExternalCallDataChunk (MemChunk mem1 base1 len1), ExternalCallDataChunk (MemChunk mem2 base2 len2)) -> do
     len_eq <- isEq sym len1 len2
     let ptrW = MC.memWidthNatRepr @ptrW
@@ -408,6 +436,7 @@ printExternalCallData ::
   ExternalCallData sym ptrW ->
   Doc a
 printExternalCallData (ExternalCallDataExpr e) = printSymExpr e
+printExternalCallData (ExternalCallDataPointer ptr) = pretty ptr
 printExternalCallData (ExternalCallDataChunk (MemChunk mem1 base1 len1)) =
   "TODO print mem chunk: " <+> printSymExpr mem1 <+> printSymExpr base1 <+> printSymExpr len1
 
@@ -524,18 +553,18 @@ instance OrdF (SymExpr sym) => Ord (MemEvent sym ptrW) where
   compare a b = case (a,b) of
     (MemOpEvent op1, MemOpEvent op2) -> compare op1 op2
     (SyscallEvent mt1 bv1, SyscallEvent mt2 bv2) -> compareTrees mt1 mt2 <> (toOrdering $ compareF bv1 bv2)
-    (ExternalCallEvent nm1 vs1, ExternalCallEvent nm2 vs2) -> 
-      compare nm1 nm2 <> (compare vs1 vs2)
+    (ExternalCallEventGen nm1 vs1 obs1, ExternalCallEventGen nm2 vs2 obs2) -> 
+      compare nm1 nm2 <> (compare vs1 vs2) <> compare obs1 obs2
     (MemOpEvent{}, _) -> GT
-    (SyscallEvent{}, ExternalCallEvent{}) -> GT
-    (ExternalCallEvent{}, _) -> LT
+    (SyscallEvent{}, ExternalCallEventGen{}) -> GT
+    (ExternalCallEventGen{}, _) -> LT
     (SyscallEvent{}, MemOpEvent{}) -> LT
 
 instance W4S.SerializableExprs sym => W4S.W4Serializable sym (MemEvent sym ptrW) where
   w4Serialize = \case
     MemOpEvent mop -> W4S.object ["mem_op" .= mop]
     SyscallEvent i r0 -> W4S.object ["syscall" .= i, "r0" .== r0]
-    ExternalCallEvent nm bvs -> W4S.object ["external_call" .= nm, "args" .= bvs]
+    ExternalCallEventGen nm bvs obs -> W4S.object ["external_call" .= nm, "args" .= bvs, "observable" .= obs]
 
 prettyMemEvent :: (MemWidth ptrW, IsExpr (SymExpr sym)) => MemEvent sym ptrW -> Doc ann
 prettyMemEvent (MemOpEvent op) = prettyMemOp op
@@ -544,7 +573,7 @@ prettyMemEvent (SyscallEvent i v) =
     [(Just (addr, dis), _)] -> "Syscall At:" <+> viaShow addr <+> pretty dis <> line <> printSymExpr v
     _ -> "Syscall" <+> printSymExpr v
 prettyMemEvent (ExternalCallEvent nm vs) = "External Call At:" <+> pretty nm <+> vsep (map printExternalCallData vs)
-
+prettyMemEvent (ExternalCallEventHidden nm vs) = "Unobservable External Call At:" <+> pretty nm <+> vsep (map printExternalCallData vs)
 
 instance (MemWidth ptrW, IsExpr (SymExpr sym)) => Pretty (MemEvent sym ptrW) where
   pretty ev = prettyMemEvent ev
@@ -555,14 +584,14 @@ instance PEM.ExprMappable sym (MemEvent sym w) where
     SyscallEvent i arg -> SyscallEvent i <$> f arg
     -- MuxTree is unmodified since it has no symbolic expressions
     -- FIXME: shouldn't we still check the booleans?
-    ExternalCallEvent nm vs -> ExternalCallEvent nm <$> PEM.mapExpr sym f vs
+    ExternalCallEventGen nm vs obs -> ExternalCallEventGen nm <$> PEM.mapExpr sym f vs <*> pure obs
 
 instance PEM.ExprFoldable sym (MemEvent sym w) where
   foldExpr sym f ev b = case ev of
     MemOpEvent op -> PEM.foldExpr sym f op b
     -- FIXME: see above
     SyscallEvent _i arg -> f arg b
-    ExternalCallEvent _nm vs -> PEM.foldExpr sym f vs b
+    ExternalCallEventGen _nm vs _obs -> PEM.foldExpr sym f vs b
 
 filterEvent ::
   IsExprBuilder sym =>
@@ -575,7 +604,7 @@ filterEvent sym f x = case x of
     SyscallEvent{} -> return $ (Nothing, truePred sym)
     -- always include external call events
     ExternalCallEvent{} -> return $ (Nothing, truePred sym)
-    
+    ExternalCallEventHidden{} -> return $ (Nothing, falsePred sym)
     -- Include memory operations only if they acutally
     -- happen (their condition is true) and if they are
     -- deemed observable by the given filtering function.
diff --git a/src/Pate/Loader.hs b/src/Pate/Loader.hs
index 0892d2ff..a1aa265d 100644
--- a/src/Pate/Loader.hs
+++ b/src/Pate/Loader.hs
@@ -112,7 +112,7 @@ runEquivVerification validArch@(PA.SomeValidArch {}) loadErrs (Logger logAct con
     (e : es) -> LJ.writeLog logAct (PE.HintErrorsBSI (e DLN.:| es))
     _ -> return ()
   st <- (CME.runExceptT $ PV.verifyPairs validArch logAct original patched dcfg pd) >>= \case
-    Left err -> return $ PEq.Errored err
+    Left err -> return $ PEq.Errored [err]
     Right st -> return st
   -- Shut down the logger cleanly (if we can - the interactive logger will be
   -- persistent until the user kills it)
@@ -131,7 +131,7 @@ liftToEquivStatus ::
 liftToEquivStatus cfg f = do
   v <- CME.runExceptT (CMW.runWriterT (CMR.runReaderT f (elfLoaderConfig cfg)))
   case v of
-    Left err -> return $ PEq.Errored (PEE.loaderError err)
+    Left err -> return $ PEq.Errored [PEE.loaderError err]
     Right (b, _) -> return b
 
 -- | Given a patch configuration, check that
diff --git a/src/Pate/Memory/MemTrace.hs b/src/Pate/Memory/MemTrace.hs
index 3198cb72..5d08d950 100644
--- a/src/Pate/Memory/MemTrace.hs
+++ b/src/Pate/Memory/MemTrace.hs
@@ -67,6 +67,7 @@ module Pate.Memory.MemTrace
 , prettyMemTraceSeq
 , addExternalCallEvent
 , addExternalCallWrite
+, addMemEvent
 , SymBV'(..)
 , getPtrAssertion
 , PtrAssertions
@@ -641,11 +642,12 @@ addExternalCallEvent ::
   sym ->
   Text {- ^ name of the external call -} ->
   Ctx.Assignment (SymExpr sym) ctx {- ^ data relevant to the call -} ->
+  Bool {- ^ true if this call is considered observable -} ->
   MemTraceImpl sym ptrW ->
   IO (MemTraceImpl sym ptrW)
-addExternalCallEvent sym nm data_ mem = do
+addExternalCallEvent sym nm data_ obs mem = do
   let
-    event = ExternalCallEvent nm (TFC.toListFC ExternalCallDataExpr data_)
+    event = ExternalCallEventGen nm (TFC.toListFC ExternalCallDataExpr data_) obs
   addMemEvent sym event mem
 
 addExternalCallWrite ::
diff --git a/src/Pate/Pointer.hs b/src/Pate/Pointer.hs
index 064c34e5..4e5cffae 100644
--- a/src/Pate/Pointer.hs
+++ b/src/Pate/Pointer.hs
@@ -23,6 +23,8 @@ module Pate.Pointer
   , withWidth
   , asConcrete
   , traverseAsPtr
+  , ptrEq
+  , groundPtr
   ) where
 
 import Data.UnwrapType
@@ -42,6 +44,10 @@ import qualified Lang.Crucible.LLVM.MemModel as CLM
 import qualified Data.Aeson as JSON
 import Data.Aeson ((.=))
 import qualified Pate.ExprMappable as PEM
+import qualified What4.ExprHelpers as WEH
+import qualified What4.Expr.Builder as W4B
+import qualified What4.Expr.GroundEval as W4G
+import qualified Pate.Verification.Concretize as PVC
 
 
 newtype Pointer sym w = PointerC { unPtr :: (CLM.LLVMPtr sym w) }
@@ -84,6 +90,14 @@ asConcrete (Pointer reg off) = case (W4.asNat reg, W4.asConcrete off) of
   (Just reg_c, Just (W4.ConcreteBV _ off_c)) -> Just (reg_c, off_c)
   _ -> Nothing
 
+groundPtr :: forall sym ptrW t st fs. sym ~ W4B.ExprBuilder t st fs =>
+  sym ->
+  W4G.GroundEvalFn t ->
+  Pointer sym ptrW ->
+  IO (Pointer sym ptrW)
+groundPtr sym evalFn ptr = 
+  PEM.mapExpr sym (\e -> W4G.groundEval evalFn e >>= \gv -> PVC.symbolicFromConcrete sym gv e) ptr
+
 width :: W4.IsExpr (W4.SymExpr sym) => Pointer sym w -> W4.NatRepr w
 width ptr = withWidth ptr id
 
@@ -93,6 +107,17 @@ withWidth (Pointer _ off) f | W4.BaseBVRepr w <- W4.exprType off = f w
 traverseAsPtr :: Applicative t => CLM.LLVMPtr sym w1 -> (Pointer sym w1 -> t (Pointer sym w2)) -> t (CLM.LLVMPtr sym w2)
 traverseAsPtr ptr f = unPtr <$> f (PointerC ptr)
 
+-- | True iff the pointers are the same width and have the same region/offset
+ptrEq :: W4.IsExprBuilder sym => sym -> Pointer sym w1 -> Pointer sym w2 -> IO (W4.Pred sym)
+ptrEq sym ptr1@(Pointer reg1 off1) ptr2@(Pointer reg2 off2) =
+  case testEquality (width ptr1) (width ptr2) of
+    Just Refl -> do
+      regsEq <- W4.natEq sym reg1 reg2
+      W4.BaseBVRepr{} <- return $ W4.exprType off1
+      offsEq <- W4.bvEq sym off1 off2
+      W4.andPred sym regsEq offsEq
+    Nothing -> return $ W4.falsePred sym
+
 instance TestEquality (W4.SymExpr sym) => TestEquality (Pointer sym) where
   testEquality (Pointer reg1 off1) (Pointer reg2 off2) = case (reg1 == reg2, testEquality off1 off2) of
     (True, Just Refl) -> Just Refl
@@ -115,5 +140,8 @@ instance W4S.SerializableExprs sym => W4S.W4Serializable sym (Pointer sym w) whe
 
 instance W4S.SerializableExprs sym => W4S.W4SerializableF sym (Pointer sym) where
 
+instance PEM.ExprMappable sym (Pointer sym w) where
+  mapExpr sym f (PointerC llvmptr) = PointerC <$> WEH.mapExprPtr sym f llvmptr
+
 instance PEM.ExprFoldable sym (Pointer sym w) where
   foldExpr _sym f (Pointer reg1 off1) b = f (W4.natToIntegerPure reg1) b >>= f off1
\ No newline at end of file
diff --git a/src/Pate/Verification/Concretize.hs b/src/Pate/Verification/Concretize.hs
index 6caff863..0fea5c1b 100644
--- a/src/Pate/Verification/Concretize.hs
+++ b/src/Pate/Verification/Concretize.hs
@@ -189,4 +189,10 @@ symbolicFromConcrete sym gv e = case WI.exprType e of
   WI.BaseBoolRepr -> let (Concretize _ _ _ inject) = concreteBool in inject sym gv
   WI.BaseIntegerRepr -> let (Concretize _ _ _ inject) = concreteInteger in inject sym gv
   WI.BaseBVRepr w -> let (Concretize _ _ _ inject) = concreteBV w in inject sym gv
+  WI.BaseStructRepr{} -> do
+    es <- Ctx.traverseWithIndex 
+      (\idx_ (WEG.GVW gv_) -> 
+        WI.structField sym e idx_ >>= \e_ -> symbolicFromConcrete sym gv_ e_) 
+      gv
+    WI.mkStruct sym es
   _ -> return e
diff --git a/src/Pate/Verification/PairGraph.hs b/src/Pate/Verification/PairGraph.hs
index ec7a40b5..73477850 100644
--- a/src/Pate/Verification/PairGraph.hs
+++ b/src/Pate/Verification/PairGraph.hs
@@ -151,6 +151,7 @@ import           Control.Monad.Trans.Except (runExceptT)
 import           Control.Monad.Trans.State.Strict (runState)
 import           Control.Monad.Trans.Writer hiding (tell)
 import           Control.Monad.Writer
+import           Data.List (intercalate)
 
 import qualified Control.Lens as L
 import           Control.Lens ( (&), (.~), (^.), (%~) )
@@ -1238,28 +1239,44 @@ reportAnalysisErrors logAction gr =
 -- | After computing the dataflow fixpoint, examine the generated
 --   error reports to determine an overall verdict for the programs.
 pairGraphComputeVerdict ::
+  forall sym arch.
+  PA.ValidArch arch =>
   PairGraph sym arch ->
   PE.EquivalenceStatus
 pairGraphComputeVerdict gr =
-  if Map.null (pairGraphObservableReports gr) &&
-     Map.null (pairGraphDesyncReports gr) &&
-     not (unsolvedAsserts gr) &&
-     Set.null (pairGraphGasExhausted gr) then
-    case filter (\(_,condK) -> case condK of {ConditionEquiv{} -> True; _ -> False}) (Map.keys (pairGraphConditions gr)) of
+  let 
+     
+    ineq :: String -> [GraphNode arch] -> PE.EquivalenceStatus
+    ineq header vals = PE.Inequivalent 
+      [header ++ " " ++ intercalate ", " (map (\nd -> show $ tracePrettyNode nd "") vals) ++ "."]
+  
+    obsStat = case Map.keys (pairGraphObservableReports gr) of
+      [] -> mempty
+      obs -> ineq "Observable differences at:" $ map GraphNode obs
+    desyncStat = case Map.keys (pairGraphDesyncReports gr) of
+      [] -> mempty
+      desync -> ineq "Control flow desynchronization at:" $ map GraphNode desync
+    assertStat = case unsolvedAsserts gr of
+      [] -> mempty
+      asserts -> ineq "Failed to discharge assertion at:"  asserts
+    gasStat = case Set.toList (pairGraphGasExhausted gr) of
+      [] -> mempty
+      exhausts -> ineq "Ran out of gas while widening equivalence domains for:" exhausts
+    condStat = case filter (\(_,condK) -> case condK of {ConditionEquiv{} -> True; _ -> False}) (Map.keys (pairGraphConditions gr)) of
       [] -> PE.Equivalent
       _ -> PE.ConditionallyEquivalent
-  else
-    PE.Inequivalent
+  in mconcat [obsStat, desyncStat, assertStat, gasStat, condStat]
 
+-- TODO: note where assertion was originally made, rather than the root node
 unsolvedAsserts ::
-  PairGraph sym arch -> Bool
+  PairGraph sym arch -> [GraphNode arch]
 unsolvedAsserts pg = 
   let 
     cond_nodes = Map.keys (pairGraphConditions pg)
     go (nd, condK) = case condK of
-      ConditionAsserted{} -> isRootNode nd
-      _ -> False
-  in any go cond_nodes
+      ConditionAsserted{} | isRootNode nd -> Just nd
+      _ -> Nothing
+  in mapMaybe go cond_nodes
 
 -- | Drop the given node from the work queue if it is queued.
 --   Otherwise do nothing.
diff --git a/src/Pate/Verification/PairGraph/Node.hs b/src/Pate/Verification/PairGraph/Node.hs
index 2d324a0b..5feb48eb 100644
--- a/src/Pate/Verification/PairGraph/Node.hs
+++ b/src/Pate/Verification/PairGraph/Node.hs
@@ -74,6 +74,7 @@ module Pate.Verification.PairGraph.Node (
   , withKnownBin
   , toTwoSidedNode
   , asSingleNode
+  , tracePrettyNode
   ) where
 
 import           Prettyprinter ( Pretty(..), sep, (<+>), Doc )
diff --git a/src/Pate/Verification/StrongestPosts.hs b/src/Pate/Verification/StrongestPosts.hs
index 5888587e..0dd0a449 100644
--- a/src/Pate/Verification/StrongestPosts.hs
+++ b/src/Pate/Verification/StrongestPosts.hs
@@ -88,6 +88,7 @@ import qualified Pate.Discovery as PD
 import qualified Pate.Discovery.ParsedFunctions as PD
 import qualified Pate.Config as PCfg
 import qualified Pate.Equivalence as PE
+import qualified Pate.Equivalence as PEq
 import qualified Pate.Equivalence.RegisterDomain as PER
 import qualified Pate.Equivalence.EquivalenceDomain as PEq
 import qualified Pate.Equivalence.MemoryDomain as PEm
@@ -181,7 +182,7 @@ runVerificationLoop ::
 runVerificationLoop env pPairs = do
   result <- runEquivM env doVerify
   case result of
-    Left err -> return (PE.Errored err, mempty)
+    Left err -> return (PE.Errored [err], mempty)
     Right r -> return r
  where
    doVerify :: EquivM sym arch (PE.EquivalenceStatus, PESt.EquivalenceStatistics)
@@ -193,7 +194,7 @@ runVerificationLoop env pPairs = do
             -- Report a summary of any errors we found during analysis
             pg1 <- handleDanglingReturns pPairs pg
             reportAnalysisErrors (envLogger env) pg1
-            return $ pairGraphComputeVerdict pg1) (pure . PE.Errored)
+            return $ pairGraphComputeVerdict pg1) (\err -> return $ PE.Errored [err])
 
           emitEvent (PE.StrongestPostOverallResult result)
 
@@ -627,7 +628,7 @@ initSingleSidedDomain sne pg0 = withRepr bin $ withRepr (PBi.flipRepr bin) $ wit
 
     let do_widen binds pg = fnTrace "do_widen" $ do
           atPriority (raisePriority pr) (Just "Starting Split Analysis") $  do
-            pg2 <- propagateOne scope bundle [ConditionAssumed, ConditionEquiv] nd nd_single ConditionAsserted pg >>= \case
+            pg2 <- propagateOne scope bundle [ConditionAssumed, ConditionEquiv] dom nd nd_single ConditionAsserted pg >>= \case
               (ConditionNotPropagated, pg1) -> return pg1
               (ConditionPropagated preconds, pg1) -> foldM (\pg_ condK -> rewrite_cond condK binds pg_) pg1 (ConditionAsserted:preconds) 
               (ConditionInfeasible, pg1) -> rewrite_cond ConditionAsserted binds pg1
@@ -824,7 +825,7 @@ mergeSingletons sneO sneP pg = fnTrace "mergeSingletons" $ withSym $ \sym -> do
               let nd = GraphNode $ singleToNodeEntry sne
               let scope = singleBundleScope sbundle
 
-              liftEqM $ \pg_ -> propagateOne scope  (singleBundle sbundle) [ConditionAssumed, ConditionEquiv] nd syncNode ConditionAsserted pg_ >>= \case
+              liftEqM $ \pg_ -> propagateOne scope  (singleBundle sbundle) [ConditionAssumed, ConditionEquiv] (singleBundleDomain sbundle) nd syncNode ConditionAsserted pg_ >>= \case
                 (ConditionNotPropagated, _) -> 
                   -- bindings already assumed above
                   return (W4.truePred sym, pg_)
@@ -1130,8 +1131,16 @@ toConditionTraces scope bundle p mtraceT mtraceF = withSym $ \sym -> do
     return (fp,v)
   return (ConditionTraces p mtraceT mtraceF fpvs, eenv)
 
-instance W4S.W4Serializable sym (PE.EquivalenceStatus) where
-  w4Serialize st = W4S.w4SerializeString st
+instance W4S.W4Serializable sym (PEq.EquivalenceStatus) where
+  w4Serialize st = do
+    let (simple :: String) = case st of
+          PEq.Equivalent -> "Equivalent"
+          PEq.Inequivalent{} -> "Inequivalent"
+          PEq.ConditionallyEquivalent -> "ConditionallyEquivalent"
+          PEq.Errored{} -> "Errored"
+    simpleJSON <- W4S.w4SerializeString simple
+    message <- W4S.w4SerializeString (PP.pretty st)
+    W4S.object [ "simple" W4S..= simpleJSON, "message" W4S..= message ]
 
 instance (PA.ValidArch arch, PSo.ValidSym sym) => W4S.W4Serializable sym (FinalResult sym arch) where
   w4Serialize (FinalResult st obs conds) = do
@@ -1986,7 +1995,7 @@ doCheckObservables scope ne bundle preD pg = case PS.simOut bundle of
                   choice "Assert difference is infeasible (defer proof)" () $ return $ Just (ConditionAsserted, RefineUsingExactEquality, PriorityDeferredPropagation)
                   choice "Assert difference is infeasible (prove immediately)" () $ return $ Just (ConditionAsserted, RefineUsingExactEquality, PriorityPropagation)
                   choice "Assume difference is infeasible" () $ return $ Just (ConditionAssumed, RefineUsingExactEquality, PriorityDeferredPropagation)
-                  choice "Avoid difference with equivalence condition" () $ return $ Just (ConditionEquiv, RefineUsingExactEquality, PriorityDeferredPropagation)
+                  choice "Avoid difference with equivalence condition" () $ return $ Just (ConditionEquiv, RefineUsingExactEquality, PriorityPropagation)
                   choice "Avoid difference with path-sensitive equivalence condition" () $ return $ Just (ConditionEquiv, RefineUsingIntraBlockPaths, PriorityPropagation)
               False -> return Nothing
 
@@ -2118,8 +2127,9 @@ equivalentSequences' sym cache = \xs ys -> loop [xs] [ys]
          liftIO $ W4.bvEq sym x y
        _ -> return (W4.falsePred sym)
 
-  eqEvent (MT.ExternalCallEvent nmx x) (MT.ExternalCallEvent nmy y)
+  eqEvent (MT.ExternalCallEventGen nmx x obsx) (MT.ExternalCallEventGen nmy y obsy)
     | nmx == nmy
+    , obsx == obsy
     = IO.liftIO $  do
       ps <- mapM (\(x_,y_) -> ET.compareExternalCallData sym x_ y_) (zip x y)
       foldM (W4.andPred sym) (W4.truePred sym) ps
diff --git a/src/Pate/Verification/StrongestPosts/CounterExample.hs b/src/Pate/Verification/StrongestPosts/CounterExample.hs
index a50570cd..1336a4e2 100644
--- a/src/Pate/Verification/StrongestPosts/CounterExample.hs
+++ b/src/Pate/Verification/StrongestPosts/CounterExample.hs
@@ -210,9 +210,9 @@ groundMemEvent sym evalFn (MT.SyscallEvent i x) =
   do i' <- MT.toMuxTree sym <$> groundMuxTree sym evalFn i
      x' <- W4.bvLit sym (W4.bvWidth x) =<< W4.groundEval evalFn x
      return (MT.SyscallEvent i' x')
-groundMemEvent sym evalFn (MT.ExternalCallEvent nm xs) = do
+groundMemEvent sym evalFn (MT.ExternalCallEventGen nm xs obs) = do
   xs' <- mapM (MT.groundExternalCallData sym evalFn) xs
-  return (MT.ExternalCallEvent nm xs')
+  return (MT.ExternalCallEventGen nm xs' obs)
 
 groundMemOp ::
   (sym ~ W4.ExprBuilder t st fs, 1 <= ptrW) =>
diff --git a/src/Pate/Verification/Widening.hs b/src/Pate/Verification/Widening.hs
index 62072f30..b228f186 100644
--- a/src/Pate/Verification/Widening.hs
+++ b/src/Pate/Verification/Widening.hs
@@ -931,12 +931,13 @@ propagateOne ::
   PS.SimScope sym arch v ->
   SimBundle sym arch v ->
   [ConditionKind] -> {- ^ weaken the propagated condition with assumptions -}
+  AbstractDomain sym arch v -> {- ^ predomain -}
   GraphNode arch {- ^ from -} ->
   GraphNode arch {- ^ to -} ->
   ConditionKind ->
   PairGraph sym arch ->
   EquivM sym arch (PropagateCase, PairGraph sym arch)
-propagateOne scope bundle preconds from to condK gr0 = withSym $ \sym -> case getCondition gr0 to condK of
+propagateOne scope bundle preconds preD from to condK gr0 = withSym $ \sym -> case getCondition gr0 to condK of
   Nothing -> do
     emitTrace @"debug" "No condition to propagate"
     return (ConditionNotPropagated, gr0)
@@ -954,15 +955,36 @@ propagateOne scope bundle preconds from to condK gr0 = withSym $ \sym -> case ge
     cond_pred <- PEC.toPred sym cond
 
     goalTimeout <- CMR.asks (PC.cfgGoalTimeout . envConfig)
-    isPredSat' goalTimeout cond_pred >>= \case
+    mcond_res <- isPredSat' goalTimeout cond_pred
+    mcheck_propagate <- case mcond_res of
       Just False -> do
         emitTrace @"message" "Condition is infeasible, dropping branch."
         gr1 <- pruneCurrentBranch scope (from,to) condK gr0
-        return (ConditionInfeasible, gr1)
-      _ | not (shouldPropagate (getPropagationKind gr0 to condK)) -> do
-        emitTrace @"debug" "Condition not propagated"
-        return (ConditionNotPropagated, gr0)
-      _ -> do
+        return $ Just (ConditionInfeasible, gr1)
+      _ -> case shouldPropagate (getPropagationKind gr0 to condK) of
+        True -> return Nothing
+        False -> do
+          eqCtx <- equivalenceContext
+          (postAsm_1:postAsms_rest) <- mapM (\condK_ -> getEquivPostCondition scope bundle to condK_ gr0) [minBound..maxBound]
+          postAsm <- PEC.toPred sym =<< foldM (PEC.merge sym) postAsm_1 postAsms_rest
+
+          eqPost_eq <- liftIO $ PEq.getPostdomain sym scope bundle eqCtx (PAD.absDomEq preD) (universalDomain sym)
+          eqPost_pred <- IO.liftIO $ postCondPredicate sym eqPost_eq
+          not_eqPost <- liftIO $ W4.notPred sym eqPost_pred
+          (withSatAssumption (PAs.fromPred postAsm) $ isPredSat' goalTimeout not_eqPost) >>= \case
+            Just (Just False) -> do
+              -- post-domain assumes exact equality, so we stop propagating assumed conditions
+              emitTrace @"debug" "Condition not propagated"
+              return $ Just (ConditionNotPropagated, gr0)
+            _ -> do
+              withTracing @"debug" "Non-trivial equivalence post-domain:" $ 
+                emitTrace @"expr" (Some eqPost_pred) 
+              -- domain is non-trivial, so we propagate the assumption backwards since
+              -- it may strengthen the condition
+              return Nothing
+    case mcheck_propagate of
+      Just res -> return res
+      Nothing -> do
         not_cond <- liftIO $ W4.notPred sym cond_pred
         isPredSat' goalTimeout not_cond >>= \case
           -- equivalence condition for this path holds, we 
@@ -1016,11 +1038,12 @@ propagateCondition ::
   forall sym arch v.
   PS.SimScope sym arch v ->
   SimBundle sym arch v ->
+  AbstractDomain sym arch v -> {- ^ predomain -}
   GraphNode arch {- ^ from -} ->
   GraphNode arch {- ^ to -} ->
   PairGraph sym arch ->
   EquivM sym arch (PropagateCase, PairGraph sym arch)
-propagateCondition scope bundle from to gr0 = fnTrace "propagateCondition" $ do
+propagateCondition scope bundle preD from to gr0 = fnTrace "propagateCondition" $ do
   priority <- thisPriority
   (pcases, gr1) <- go [] [ConditionAssumed, ConditionEquiv, ConditionAsserted] gr0
   let used = nub $ foldr (\pc used_ -> case pc of ConditionPropagated used' -> used_ ++ used'; _ -> used) [] pcases
@@ -1059,7 +1082,7 @@ propagateCondition scope bundle from to gr0 = fnTrace "propagateCondition" $ do
   where
     go _ [] gr = return ([],gr)
     go preconds (condK:conds) gr =  do
-      (pcase, gr') <- propagateOne scope bundle preconds from to condK gr
+      (pcase, gr') <- propagateOne scope bundle preconds preD from to condK gr
       case pcase of
         -- we need to collect any non-propagated conditions so that
         -- propagated conditions are weakened with them
@@ -1112,7 +1135,7 @@ widenAlongEdge ::
 widenAlongEdge scope bundle from d gr0 to = withSym $ \sym -> do
   gr1 <- addRefinementChoice to gr0
   priority <- thisPriority
-  propagateCondition scope bundle from to gr1 >>= \case
+  propagateCondition scope bundle d from to gr1 >>= \case
     (ConditionPropagated{}, gr2) -> do
       -- since this 'to' edge has propagated backwards
       -- an equivalence condition, we need to restart the analysis
diff --git a/src/What4/JSON.hs b/src/What4/JSON.hs
index 7df96aae..a48ea157 100644
--- a/src/What4/JSON.hs
+++ b/src/What4/JSON.hs
@@ -60,6 +60,7 @@ import qualified Data.Aeson as JSON
 import qualified Data.Aeson.Types as JSON
 import qualified Data.BitVector.Sized as BVS
 import qualified Numeric as N
+import           Data.List ( intercalate )
 
 import           Data.Parameterized.Some (Some(..))
 
@@ -236,6 +237,10 @@ instance sym ~ W4B.ExprBuilder t fs scope => W4Serializable sym (W4B.Expr t tp)
         v <- case W4.asConcrete e' of
           Just (W4.ConcreteInteger i) -> return $ JSON.toJSON i
           Just (W4.ConcreteBool b) -> return $ JSON.toJSON b
+          Just (W4.ConcreteStruct cs) ->
+            let 
+              strs = TFC.toListFC (\c -> show (W4.ppConcrete c)) cs
+            in return $ JSON.String (T.pack ("(" ++ intercalate ", " strs ++ ")"))
           Just{} -> return $ JSON.String (T.pack (show (W4.printSymExpr e')))
           _ -> do
             sym <- asks w4sSym
diff --git a/tests/TestBase.hs b/tests/TestBase.hs
index 0b863df2..e0836182 100644
--- a/tests/TestBase.hs
+++ b/tests/TestBase.hs
@@ -232,7 +232,7 @@ doTest mwb cfg _sv fp = do
     PEq.Equivalent -> case sv of
       ShouldVerify -> return ()
       _ -> failTest "Unexpectedly proved equivalence."
-    PEq.Inequivalent -> case sv of
+    PEq.Inequivalent{} -> case sv of
       ShouldVerify -> failTest "Failed to prove equivalence."
       ShouldNotVerify -> return ()
       ShouldConditionallyVerify -> failTest "Failed to prove conditional equivalence."
diff --git a/tests/integration/packet-mod/Makefile b/tests/integration/packet-mod/Makefile
index f642c668..72de8971 100644
--- a/tests/integration/packet-mod/Makefile
+++ b/tests/integration/packet-mod/Makefile
@@ -35,4 +35,4 @@ run: packet.original.exe packet.patched.exe packet.pate
 	$(PATE) --original packet.original.exe --patched packet.patched.exe -s parse_packet --script packet.pate
 
 run-bad: packet.original.exe packet.patched-bad.exe packet.pate
-	$(PATE) --original packet.original.exe --patched packet.patched-bad.exe -s parse_packet --script packet.pate
\ No newline at end of file
+	$(PATE) --original packet.original.exe --patched packet.patched-bad.exe -s parse_packet --script packet-bad.pate
\ No newline at end of file
diff --git a/tests/integration/packet-mod/packet-bad.pate b/tests/integration/packet-mod/packet-bad.pate
new file mode 100644
index 00000000..9488123f
--- /dev/null
+++ b/tests/integration/packet-mod/packet-bad.pate
@@ -0,0 +1,21 @@
+Choose Entry Point
+  > Function Entry "parse_packet"
+
+segment1+0x5e8
+  ...
+    Call to: "printf"
+    ...
+    Handle observable difference:
+      > Avoid difference with equivalence condition
+
+segment1+0x5f8 [ via: "log_info" (segment1+0x584)
+  ...
+    Call to: "printf"
+    ...
+    Handle observable difference:
+      > Assert difference is infeasible (prove immediately) 
+
+
+Verification Finished
+Continue verification?
+    > Finish and view final result
diff --git a/tests/integration/packet-mod/packet.c b/tests/integration/packet-mod/packet.c
index 90266c10..6e5fe404 100644
--- a/tests/integration/packet-mod/packet.c
+++ b/tests/integration/packet-mod/packet.c
@@ -10,7 +10,7 @@ int check_crc(uint16_t crc, void *data) { return (crc == 0); }
 
 
 #pragma noinline
-void log_info(int log_msg, uint8_t value) {
+void log_info(int log_msg, int value) {
   switch (log_msg) {
     case LOG_MAX_SIZE:
       print("[INFO] Max packet size: ");
diff --git a/tests/integration/packet-mod/packet.pate b/tests/integration/packet-mod/packet.pate
index e5af54e9..c6ac9150 100644
--- a/tests/integration/packet-mod/packet.pate
+++ b/tests/integration/packet-mod/packet.pate
@@ -8,14 +8,6 @@ segment1+0x5e8
     Handle observable difference:
       > Avoid difference with equivalence condition
 
-
-segment1+0x5f8 [ via: "log_info" (segment1+0x584) <- "parse_data"
-  ...
-    Call to: "printf"
-    ...
-    Handle observable difference:
-      > Assert difference is infeasible (prove immediately)
-
 Verification Finished
 Continue verification?
     > Finish and view final result
\ No newline at end of file
diff --git a/tests/integration/packet/packet.exp b/tests/integration/packet/packet.exp
index 94fb572b..15ee87e2 100755
--- a/tests/integration/packet/packet.exp
+++ b/tests/integration/packet/packet.exp
@@ -38,6 +38,8 @@ expect "Handle observable difference:"
 expect "4: Avoid difference with equivalence condition"
 expect "?>"
 send "4\r"
+send "top\r"
+send "wait\r"
 
 expect "Continue verification?"
 expect "0: Finish and view final result"
@@ -53,29 +55,29 @@ expect "Waiting for constraints.."
 # error about a missing identifier. The target expression should be the one that ends in 
 # something like: 'select v35113 (bvSum cr5O_offset@34733:bv 0x2:[32]))'
 
-send "input \"\[ \[ { \\\"var\\\" : { \\\"symbolic_ident\\\" : 17460 }, \\\"op\\\" : \\\"EQ\\\", \\\"const\\\" : \\\"128\\\"} \] \]\"\r"
+send "input \"\[ \[ { \\\"var\\\" : { \\\"symbolic_ident\\\" : 11458 }, \\\"op\\\" : \\\"EQ\\\", \\\"const\\\" : \\\"128\\\"} \] \]\"\r"
 
 expect "Regenerate result with new trace constraints?"
 expect "1: False"
 send "1\r"
 
 
-expect "20: Final Result"
+expect "30: Final Result"
 expect ">"
-send "20\r"
+send "30\r"
 
 expect "0: Assumed Equivalence Conditions"
-expect "2: Binaries are conditionally, observably equivalent"
+expect "3: Binaries are conditionally, observably equivalent"
 expect ">"
 send "0\r"
 
 # Inspect the specific equivalence condition
 
-expect "0: segment1+0x71c \\\[ via: \"parse_packet\" (segment1+0x590) \\\]"
+expect "1: segment1+0x71c \\\[ via: \"parse_packet\" (segment1+0x590) \\\]"
 expect ">"
-send "0\r"
+send "1\r"
 
-expect -re {3: \(Predicate\) let -- segment1\+0x754.. in not \(and v(\d)+ \(not v(\d)+\)\)}
+expect -re {3: \(Predicate\) let -- segment1\+0x734.. in not \(and v(\d)+ \(not v(\d)+\)\)}
 expect ">"
 send "3\r"
 
@@ -88,18 +90,18 @@ expect ">"
 send "up\r"
 expect ">"
 send "up\r"
-expect "5: Assumed Equivalence Conditions"
+expect "6: Assumed Equivalence Conditions"
 expect ">"
-send "5\r"
+send "6\r"
 
-expect "0: segment1+0x71c \\\[ via: \"parse_packet\" (segment1+0x590) \\\]"
+expect "1: segment1+0x71c \\\[ via: \"parse_packet\" (segment1+0x590) \\\]"
 expect ">"
-send "0\r"
+send "1\r"
 
 expect "5: Simplified Predicate"
 send "5\r"
 
-expect "0: eq 0x0:\\\[8\\\] (select (select cInitMemBytes@49845:a 0) 0x11044:\\\[32\\\])"
+expect -re {0: let -- segment1\+0x734.. in not \(and v(\d)+ \(not v(\d)+\)\)}
 
 send "\x04" ; # Ctrl-D (EOF)