diff --git a/src/Pate/Equivalence/Error.hs b/src/Pate/Equivalence/Error.hs
index c671699d..4140e0d1 100644
--- a/src/Pate/Equivalence/Error.hs
+++ b/src/Pate/Equivalence/Error.hs
@@ -27,7 +27,9 @@ module Pate.Equivalence.Error (
   , isRecoverable
   , isTracedWhenWarning
   , loaderError
-  , someExpr) where
+  , someExpr
+  , PairGraphErr(..)
+  ) where
 
 import qualified Control.Exception as X
 import           Data.Maybe ( catMaybes )
@@ -160,6 +162,10 @@ data InnerEquivalenceError arch
   | forall tp. FailedToGroundExpr (SomeExpr tp)
   | OrphanedSingletonAnalysis (PB.FunPair arch)
   | RequiresInvalidPointerOps
+  | PairGraphError PairGraphErr
+
+data PairGraphErr = PairGraphErr String
+  deriving Show
 
 data SomeExpr tp = forall sym. W4.IsExpr (W4.SymExpr sym) => SomeExpr (W4.SymExpr sym tp)
 
diff --git a/src/Pate/Monad.hs b/src/Pate/Monad.hs
index ba2f677e..52a9edc7 100644
--- a/src/Pate/Monad.hs
+++ b/src/Pate/Monad.hs
@@ -1319,7 +1319,12 @@ traceBundle bundle msg = do
   let bp = TF.fmapF (Const . PB.concreteAddress . simInBlock) (simIn bundle)
   emitEvent (PE.ProofTraceEvent callStack bp (T.pack msg))
 
-fnTrace :: String -> EquivM_ sym arch a -> EquivM_ sym arch a
+fnTrace :: 
+  forall k e m a.
+  IsTreeBuilder k e m =>
+  TraceNodeType k "function_name" ->
+  m a ->
+  m a
 fnTrace nm f = withTracing @"function_name" nm f
 
 --------------------------------------
diff --git a/src/Pate/PatchPair.hs b/src/Pate/PatchPair.hs
index c69fa60b..0d2ef51e 100644
--- a/src/Pate/PatchPair.hs
+++ b/src/Pate/PatchPair.hs
@@ -48,6 +48,7 @@ module Pate.PatchPair (
   , view
   , asTuple
   , fromTuple
+  , fromMaybes
   , ppEq
   , LiftF(..)
   , PatchPairF
@@ -96,6 +97,8 @@ import Control.Monad.Identity
 import Pate.TraceTree
 import qualified What4.JSON as W4S
 import What4.JSON
+import Control.Monad.State.Strict (StateT (..), put)
+import qualified Control.Monad.State.Strict as CMS
 
 -- | A pair of values indexed based on which binary they are associated with (either the
 --   original binary or the patched binary).
@@ -172,6 +175,14 @@ instance Monad m => PatchPairM (MaybeT m) where
     Just ra -> return $ Just ra
     Nothing -> b
 
+instance PatchPairM m => PatchPairM (StateT s m) where
+  throwPairErr = lift $ throwPairErr
+  catchPairErr a b = do
+    s <- CMS.get
+    (x, s') <- lift $ catchPairErr (runStateT a s) (runStateT b s)
+    put s'
+    return x
+
 liftPairErr :: PatchPairM m => Maybe a -> m a
 liftPairErr (Just a) = return a
 liftPairErr Nothing = throwPairErr
@@ -204,6 +215,15 @@ asTuple pPair = case pPair of
 fromTuple :: (tp PB.Original, tp PB.Patched) -> PatchPair tp
 fromTuple (vO,vP) = PatchPair vO vP
 
+fromMaybes :: PatchPairM m => (Maybe (tp PB.Original), Maybe (tp PB.Patched)) -> m (PatchPair tp)
+fromMaybes = \case
+  (Just vO,Just vP) -> return $ PatchPair vO vP
+  (Just vO, Nothing) -> return $ PatchPairSingle PB.OriginalRepr vO
+  (Nothing, Just vP) -> return $ PatchPairSingle PB.PatchedRepr vP
+  (Nothing, Nothing) -> throwPairErr
+
+
+
 -- | Set the value in the given 'PatchPair' according to the given 'PB.WhichBinaryRepr'
 --   Raises 'pairErr' if the given 'PatchPair' does not contain a value for the given binary.
 set :: HasCallStack => PatchPairM m => PB.WhichBinaryRepr bin -> (forall tp. PatchPair tp -> tp bin -> m (PatchPair tp))
diff --git a/src/Pate/TraceTree.hs b/src/Pate/TraceTree.hs
index 6a0f0598..84f97a73 100644
--- a/src/Pate/TraceTree.hs
+++ b/src/Pate/TraceTree.hs
@@ -151,6 +151,7 @@ import qualified Control.Concurrent as IO
 import qualified System.IO as IO
 import Data.Maybe (catMaybes)
 import Control.Concurrent (threadDelay)
+import Control.Monad.State.Strict (StateT (..), MonadState (..))
 
 data TraceTag =
     Summary
@@ -1023,6 +1024,14 @@ instance Monad m => MonadTreeBuilder k (NoTreeBuilder k m) where
   getTreeBuilder = return $ noTreeBuilder
   withTreeBuilder _ = id
 
+instance MonadTreeBuilder k m => MonadTreeBuilder k (StateT s m) where
+  getTreeBuilder = lift $ getTreeBuilder
+  withTreeBuilder tb f = do
+    s <- get
+    (a,s') <- lift $ withTreeBuilder tb (runStateT f s)
+    put s'
+    return a
+
 noTracing :: NoTreeBuilder k m a -> m a
 noTracing (NoTreeBuilder f) = f
 
diff --git a/src/Pate/Verification/PairGraph.hs b/src/Pate/Verification/PairGraph.hs
index a82abf8f..edff93a6 100644
--- a/src/Pate/Verification/PairGraph.hs
+++ b/src/Pate/Verification/PairGraph.hs
@@ -16,11 +16,18 @@
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
 
 module Pate.Verification.PairGraph
   ( Gas(..)
   , initialGas
   , PairGraph
+  , PairGraphM
+  , runPairGraphM
+  , execPairGraphM
+  , evalPairGraphM
   , maybeUpdate
   , AbstractDomain
   , initialDomain
@@ -41,6 +48,7 @@ module Pate.Verification.PairGraph
   , initDomain
   , pairGraphComputeVerdict
   , getCurrentDomain
+  , getCurrentDomainM
   , considerObservableEvent
   , considerDesyncEvent
   , recordMiscAnalysisError
@@ -64,11 +72,10 @@ module Pate.Verification.PairGraph
   , dropReturns
   , dropPostDomains
   , markEdge
-  , getSyncPoint
-  , asSyncPoint
+  , getSyncPoints
   , getBackEdgesFrom
-  , setSyncPoint
-  , getCombinedSyncPoint
+  , addSyncNode
+  , getCombinedSyncPoints
   , combineNodes
   , NodePriority(..)
   , addToWorkList
@@ -106,12 +113,28 @@ module Pate.Verification.PairGraph
   , shouldAddPathCond
   , maybeUpdate'
   , hasSomeCondition
-  , propagateOnce, getPropagationKind, propagateAction) where
+  , propagateOnce
+  , getPropagationKind
+  , propagateAction
+  , getSyncAddress
+  , setSyncAddress
+  , checkForNodeSync
+  , checkForReturnSync
+  ) where
 
 import           Prettyprinter
 
-import           Control.Monad (foldM, guard)
+import           Control.Monad (foldM, guard, join, void, forM)
 import           Control.Monad.IO.Class
+import           Control.Monad.Reader (local, MonadReader (ask))
+import           Control.Monad.State.Strict (StateT (..), MonadState (..), MonadTrans (..), execStateT, modify, State, execState, gets)
+import           Control.Monad.Catch (MonadCatch, MonadThrow, MonadMask)
+import           Control.Monad.Error (MonadError (..))
+import           Control.Monad.Trans.Maybe (MaybeT(..) )
+import           Control.Monad.Except (ExceptT )
+import           Control.Monad.Trans.Except (runExceptT)
+import           Control.Monad.Trans.State.Strict (runState)
+
 import qualified Control.Lens as L
 import           Control.Lens ( (&), (.~), (^.), (%~) )
 import           Data.Kind (Type)
@@ -126,6 +149,7 @@ import qualified Data.Set as Set
 import           Data.Word (Word32)
 import qualified Lumberjack as LJ
 
+import           Data.Parameterized (Some(..), Pair (..))
 import qualified Data.Parameterized.TraversableF as TF
 import qualified Data.RevMap as RevMap
 import           Data.RevMap (RevMap)
@@ -147,21 +171,24 @@ import qualified Pate.Verification.Domain as PVD
 import qualified Pate.SimState as PS
 
 
-import           Pate.Verification.PairGraph.Node ( GraphNode(..), NodeEntry, NodeReturn, pattern GraphNodeEntry, pattern GraphNodeReturn, rootEntry, nodeBlocks, rootReturn, nodeFuns, graphNodeBlocks, getDivergePoint, divergePoint, mkNodeEntry, mkNodeReturn, nodeContext, isSingleNode )
+import           Pate.Verification.PairGraph.Node ( GraphNode(..), NodeEntry, NodeReturn, pattern GraphNodeEntry, pattern GraphNodeReturn, rootEntry, nodeBlocks, rootReturn, nodeFuns, graphNodeBlocks, getDivergePoint, divergePoint, mkNodeEntry, mkNodeReturn, nodeContext, isSingleNode, isSingleNodeEntry, isSingleReturn )
 import           Pate.Verification.StrongestPosts.CounterExample ( TotalityCounterexample(..), ObservableCounterexample(..) )
 
 import qualified Pate.Verification.AbstractDomain as PAD
 import           Pate.Verification.AbstractDomain ( AbstractDomain, AbstractDomainSpec )
 import           Pate.TraceTree
 import qualified Pate.Binary as PBi
-import Data.Parameterized (Some(..), Pair (..))
-import Control.Applicative (Const(..), (<|>))
+
+import           Control.Applicative (Const(..), Alternative(..)) 
 import qualified Control.Monad.IO.Unlift as IO
-import Pate.Solver (ValidSym)
-import Control.Monad.Reader (local, MonadReader (ask))
-import SemMC.Formula.Env (SomeSome(..))
+import           Pate.Solver (ValidSym)
+
+import           SemMC.Formula.Env (SomeSome(..))
 import qualified Pate.Location as PL
 import qualified Pate.ExprMappable as PEM
+import qualified Pate.Address as PAd
+import Data.Foldable (find)
+
 
 -- | Gas is used to ensure that our fixpoint computation terminates
 --   in a reasonable amount of time.  Gas is expended each time
@@ -282,6 +309,53 @@ data PairGraph sym arch =
       !(Map (GraphNode arch) [DomainRefinement sym arch])
   }
 
+
+
+newtype PairGraphM sym arch a = PairGraphT { unpgT :: ExceptT PEE.PairGraphErr (State (PairGraph sym arch)) a }
+  deriving (Functor
+           , Applicative
+           , Monad
+           , MonadState (PairGraph sym arch)
+           , MonadError PEE.PairGraphErr
+           )
+
+instance PPa.PatchPairM (PairGraphM sym arch) where
+  throwPairErr = throwError $ PEE.PairGraphErr "PatchPair"
+  catchPairErr f hdl = catchError f $ \case
+    PEE.PairGraphErr "PatchPair" -> hdl
+    e -> throwError e
+
+instance Alternative (PairGraphM sym arch) where
+  a <|> b = catchError a $ \_ -> b
+  empty = throwError $ PEE.PairGraphErr "No more alternatives"
+
+instance MonadFail (PairGraphM sym arch) where
+  fail msg = throwError $ PEE.PairGraphErr ("fail: " ++ msg)
+
+runPairGraphM :: PairGraph sym arch -> PairGraphM sym arch a -> Either PEE.PairGraphErr (a, PairGraph sym arch)
+runPairGraphM pg f = case runState (runExceptT (unpgT f)) pg of
+  (Left err, _) -> Left err
+  (Right a, pg') -> Right (a, pg')
+
+execPairGraphM :: PairGraph sym arch -> PairGraphM sym arch a -> Either PEE.PairGraphErr (PairGraph sym arch)
+execPairGraphM pg f  = case runPairGraphM pg f of
+  Left err -> Left err
+  Right (_,pg') -> Right pg'
+
+evalPairGraphM :: PairGraph sym arch -> PairGraphM sym arch a -> Either PEE.PairGraphErr a
+evalPairGraphM pg f  = case runPairGraphM pg f of
+  Left err -> Left err
+  Right (a,_) -> Right a
+
+lookupPairGraph ::
+  forall sym arch b.
+  (PairGraph sym arch -> Map (GraphNode arch) b) -> 
+  GraphNode arch ->
+  PairGraphM sym arch b
+lookupPairGraph f node = do
+  m <- gets f
+  pgMaybe "missing node entry" $ Map.lookup node m
+
 data ConditionKind = 
     ConditionAsserted
   | ConditionAssumed
@@ -416,7 +490,16 @@ data ActionQueue sym arch =
 
 
 data SyncPoint arch =
-  SyncPoint { syncNodes :: PPa.PatchPairC (GraphNode arch) }
+  SyncPoint
+    -- each side of the analysis independently defines a set of
+    -- graph nodes, representing CFARs that can terminate
+    -- respectively on the cut addresses
+    -- The "merge" nodes are the cross product of these, since we
+    -- must assume that any combination of exits is possible
+    -- during the single-sided analysis
+    { syncStartNodes :: PPa.PatchPairC (Set (GraphNode arch))
+    , syncCutAddresses :: PPa.PatchPairC (PAd.ConcreteAddress arch) 
+    }
 
 ppProgramDomains ::
   forall sym arch a.
@@ -494,6 +577,14 @@ getCurrentDomain ::
   Maybe (AbstractDomainSpec sym arch)
 getCurrentDomain pg nd = Map.lookup nd (pairGraphDomains pg)
 
+getCurrentDomainM ::
+  GraphNode arch ->
+  PairGraphM sym arch (AbstractDomainSpec sym arch)
+getCurrentDomainM nd = do
+  pg <- get
+  Just spec <- return $ getCurrentDomain pg nd
+  return spec
+
 getEdgesFrom ::
   PairGraph sym arch ->
   GraphNode arch ->
@@ -918,52 +1009,53 @@ addReturnVector gr funPair retPair priority =
 
     wl = RevMap.insertWith (min) (ReturnNode funPair) priority (pairGraphWorklist gr)
 
+pgMaybe :: String -> Maybe a -> PairGraphM sym arch a
+pgMaybe _ (Just a) = return a
+pgMaybe msg Nothing = throwError $ PEE.PairGraphErr msg
 
-getSyncPoint ::
-  PairGraph sym arch ->
+getSyncPoints ::
+  forall sym arch bin.
   PBi.WhichBinaryRepr bin ->
   GraphNode arch ->
-  Maybe (GraphNode arch)
-getSyncPoint gr bin nd = case Map.lookup nd (pairGraphSyncPoints gr) of
-  Just (SyncPoint syncPair) -> PPa.getC bin syncPair
-  Nothing -> Nothing
+  PairGraphM sym arch (Set (GraphNode arch))
+getSyncPoints bin nd = do
+  (SyncPoint syncPair _) <- lookupPairGraph @sym pairGraphSyncPoints nd
+  PPa.getC bin syncPair
+
+getSyncAddress ::
+  forall sym arch bin.
+  PBi.WhichBinaryRepr bin ->
+  GraphNode arch ->
+  PairGraphM sym arch (PAd.ConcreteAddress arch)
+getSyncAddress bin nd = do
+  (SyncPoint _ addrPair) <- lookupPairGraph @sym pairGraphSyncPoints nd
+  PPa.getC bin addrPair
 
 updateSyncPoint ::
-  PairGraph sym arch ->
+  forall sym arch.
   GraphNode arch -> 
   (SyncPoint arch -> SyncPoint arch) ->
-  PairGraph sym arch
-updateSyncPoint pg nd f = case getDivergePoint nd of
-  Just divergePoint | Just sync <- asSyncPoint pg nd -> 
-    pg { pairGraphSyncPoints = Map.insert divergePoint (f sync) (pairGraphSyncPoints pg)}
-  _ -> pg
-
-asSyncPoint ::
-  PairGraph sym arch ->
-  GraphNode arch ->
-  Maybe (SyncPoint arch)
-asSyncPoint pg nd = do
-  divergeNode <- getDivergePoint nd
-  Some bin <- singleNodeRepr nd
-  sync@(SyncPoint syncPair) <- Map.lookup divergeNode (pairGraphSyncPoints pg)
-  nd' <- PPa.getC bin syncPair
-  case nd == nd' of
-    True -> return sync
-    False -> Nothing
-
--- | If both sides of the sync point are defined, returns
---   the merged node for them
-getCombinedSyncPoint ::
-  PairGraph sym arch ->
+  PairGraphM sym arch ()
+updateSyncPoint nd f = do
+  dp <- pgMaybe "missing diverge point" $ getDivergePoint nd
+  sp <- lookupPairGraph pairGraphSyncPoints dp
+  modify $ \pg -> 
+    pg { pairGraphSyncPoints = Map.insert dp (f sp) (pairGraphSyncPoints pg)}
+
+-- | Returns all discovered merge points from the given diverge point
+getCombinedSyncPoints ::
+  forall sym arch.
   GraphNode arch ->
-  Maybe (GraphNode arch, SyncPoint arch)
-getCombinedSyncPoint gr ndDiv = do
-  sync@(SyncPoint syncPair) <- Map.lookup ndDiv (pairGraphSyncPoints gr)
-  case syncPair of
-    PPa.PatchPairSingle{} -> Nothing
-    PPa.PatchPairC ndO ndP -> case combineNodes ndO ndP of
-      Just mergedNode -> Just (mergedNode, sync)
-      Nothing -> panic Verifier "getCombinedSyncPoint" ["Unexpected sync nodes"]
+  PairGraphM sym arch ([((GraphNode arch, GraphNode arch), GraphNode arch)], SyncPoint arch)
+getCombinedSyncPoints ndDiv = do
+  sync@(SyncPoint syncSet _) <- lookupPairGraph @sym pairGraphSyncPoints ndDiv
+  case syncSet of
+    PPa.PatchPairC ndsO ndsP -> do
+      all_pairs <- forM (Set.toList $ Set.cartesianProduct ndsO ndsP) $ \(ndO, ndP) -> do
+        combined <- pgMaybe "failed to combine nodes" $ combineNodes ndO ndP
+        return $ ((ndO, ndP), combined)
+      return (all_pairs, sync)
+    _ -> return ([], sync)
 
 -- | Compute a merged node for two diverging nodes
 -- FIXME: do we need to support mismatched node kinds here?
@@ -996,25 +1088,40 @@ singleNodeRepr nd = case graphNodeBlocks nd of
   PPa.PatchPairSingle bin _ -> return $ Some bin
   PPa.PatchPair{} -> Nothing
 
-setSyncPoint ::
-  PPa.PatchPairM m =>
-  PairGraph sym arch ->
+addSyncNode ::
+  forall sym arch.
   GraphNode arch {- ^ The divergent node -}  ->
-  GraphNode arch {- ^ The sync node -} ->
-  m (PairGraph sym arch)
-setSyncPoint pg ndDiv ndSync = do
-  fmap PPa.someC $ PPa.forBinsC $ \bin -> do
-    -- check which binary these nodes are for
-    _ <- PPa.get bin (graphNodeBlocks ndDiv)
-    _ <- PPa.get bin (graphNodeBlocks ndSync)
-    let ndSync' = PPa.PatchPairSingle bin (Const ndSync)
-    case Map.lookup ndDiv (pairGraphSyncPoints pg) of
-      Just (SyncPoint sp) -> do
-        sp' <- PPa.update sp $ \bin' -> PPa.get bin' ndSync'
-        return $ pg { pairGraphSyncPoints = Map.insert ndDiv (SyncPoint sp') (pairGraphSyncPoints pg) }
-      Nothing -> do
-        let sp = PPa.mkSingle bin (Const ndSync)
-        return $ pg {pairGraphSyncPoints = Map.insert ndDiv (SyncPoint sp) (pairGraphSyncPoints pg) }
+  GraphNode arch {- ^ the sync node -} ->
+  PairGraphM sym arch ()
+addSyncNode ndDiv ndSync = do
+  Pair bin _ <- PPa.asSingleton (graphNodeBlocks ndSync)
+  let ndSync' = PPa.PatchPairSingle bin (Const ndSync)
+  (SyncPoint sp addrs) <- lookupPairGraph @sym pairGraphSyncPoints ndDiv
+  sp' <- PPa.update sp $ \bin' -> do
+    s <- PPa.getC bin' ndSync'
+    case PPa.getC bin' sp of
+      Nothing -> return $ (Const (Set.singleton s))
+      Just s' -> return $ (Const (Set.insert s s'))
+  modify $ \pg -> pg { pairGraphSyncPoints = Map.insert ndDiv (SyncPoint sp' addrs) (pairGraphSyncPoints pg) }
+
+tryPG :: PairGraphM sym arch a -> PairGraphM sym arch (Maybe a)
+tryPG f = catchError (Just <$> f) (\_ -> return Nothing)
+
+setSyncAddress ::
+  forall sym arch bin.
+  GraphNode arch {- ^ The divergent node -}  ->
+  PBi.WhichBinaryRepr bin ->
+  PAd.ConcreteAddress arch ->
+  PairGraphM sym arch ()
+setSyncAddress ndDiv bin syncAddr = do
+  let syncAddr' = PPa.PatchPairSingle bin (Const syncAddr)
+  tryPG (lookupPairGraph @sym pairGraphSyncPoints ndDiv) >>= \case
+    Just (SyncPoint sp addrs) -> do
+      addrs' <- PPa.update addrs $ \bin' -> PPa.get bin' syncAddr'
+      modify $ \pg -> pg{ pairGraphSyncPoints = Map.insert ndDiv (SyncPoint sp addrs') (pairGraphSyncPoints pg) }
+    Nothing -> do
+      let sp = PPa.mkPair bin (Const Set.empty) (Const Set.empty)
+      modify $ \pg -> pg{pairGraphSyncPoints = Map.insert ndDiv (SyncPoint sp syncAddr') (pairGraphSyncPoints pg) }
 
 -- | Add a node back to the worklist to be re-analyzed if there is
 --   an existing abstract domain for it. Otherwise return Nothing.
@@ -1233,8 +1340,47 @@ runPendingActions lens edge result pg = do
     False -> return Nothing
 
 
-
-
-
-
-
+-- If the given node is single-sided, check if any of the exits
+-- match the given synchronization point for the diverge point of this node.
+-- 
+-- We can restrict our search to just the block exits because we already
+-- defined the synchronization point as a cut point for code discovery.
+-- This means that any CFAR which can reach the sync point will necessarily
+-- have one block exit that jumps to it, regardless of where it is
+-- in a basic block.
+checkForNodeSync ::
+  NodeEntry arch ->
+  [(PPa.PatchPair (PB.BlockTarget arch))] ->
+  PairGraphM sym arch Bool
+checkForNodeSync ne targets_pairs = fmap (fromMaybe False) $ tryPG $ do
+  Just (Some bin) <- return $ isSingleNodeEntry ne
+
+  Just dp <- return $ getDivergePoint (GraphNode ne)
+  syncPoints <- getSyncPoints bin dp
+  syncAddr <- getSyncAddress bin dp
+  thisAddr <- fmap PB.concreteAddress $ PPa.get bin (nodeBlocks ne)
+  -- if this node is already defined as sync point then we don't
+  -- have to check anything else
+  if | Set.member (GraphNode ne) syncPoints -> return True
+    -- similarly if this is exactly the sync address then we should
+    -- stop the single-sided analysis
+     | thisAddr == syncAddr -> return True
+     | otherwise -> do
+          targets <- mapM (PPa.get bin) targets_pairs
+          let matchTarget btgt = case btgt of
+                 PB.BlockTarget{} -> PB.targetRawPC btgt == syncAddr
+                 _ -> False
+          return $ isJust $ find matchTarget targets
+
+-- Same as 'checkForNodeSync' but considers a single outgoing edge from
+-- a function return.
+checkForReturnSync ::
+  NodeReturn arch ->
+  NodeEntry arch ->
+  PairGraphM sym arch Bool
+checkForReturnSync nr ne = fmap (fromMaybe False) $ tryPG $ do
+  Just (Some bin) <- return $ isSingleReturn nr
+  Just dp <- return $ getDivergePoint (ReturnNode nr)
+  syncAddr <- getSyncAddress bin dp
+  blk <- PPa.get bin (nodeBlocks ne)
+  return $ PB.concreteAddress blk == syncAddr
\ No newline at end of file
diff --git a/src/Pate/Verification/PairGraph/Node.hs b/src/Pate/Verification/PairGraph/Node.hs
index dd651e68..089de9f3 100644
--- a/src/Pate/Verification/PairGraph/Node.hs
+++ b/src/Pate/Verification/PairGraph/Node.hs
@@ -40,6 +40,8 @@ module Pate.Verification.PairGraph.Node (
   , toSingleNode
   , toSingleGraphNode
   , isSingleNode
+  , isSingleNodeEntry
+  , isSingleReturn
   , splitGraphNode
   , getDivergePoint
   , eqUptoDivergePoint
diff --git a/src/Pate/Verification/StrongestPosts.hs b/src/Pate/Verification/StrongestPosts.hs
index 85dfb87a..00e064c6 100644
--- a/src/Pate/Verification/StrongestPosts.hs
+++ b/src/Pate/Verification/StrongestPosts.hs
@@ -17,6 +17,8 @@
 {-# LANGUAGE QuantifiedConstraints #-}
 
 {-# OPTIONS_GHC -fno-warn-orphans #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE FunctionalDependencies #-}
 
 module Pate.Verification.StrongestPosts
   ( pairGraphComputeFixpoint
@@ -25,13 +27,15 @@ module Pate.Verification.StrongestPosts
 
 import           GHC.Stack ( HasCallStack )
 
+import           Control.Applicative
 import qualified Control.Concurrent.MVar as MVar
 import           Control.Lens ( view, (^.) )
 import           Control.Monad (foldM, forM, unless, void, when)
 import           Control.Monad.IO.Class
 import qualified Control.Monad.IO.Unlift as IO
 import           Control.Monad.Reader (asks, local)
-import           Control.Monad.Except (catchError)
+import           Control.Monad.Except (catchError, throwError)
+import           Control.Monad.State.Strict  (get, StateT, runStateT, put, execStateT, modify)
 import           Control.Monad.Trans (lift)
 import           Numeric (showHex)
 import           Prettyprinter
@@ -41,7 +45,7 @@ import qualified Data.ByteString as BS
 import qualified Data.ByteString.Char8 as BSC
 import qualified Data.Map as Map
 import qualified Data.Set as Set
-import           Data.List (findIndex)
+import           Data.List (findIndex, find)
 import           Data.Maybe (mapMaybe, catMaybes)
 import           Data.Proxy
 import           Data.Functor.Const
@@ -111,7 +115,7 @@ import qualified Pate.Verification.ConditionalEquiv as PVC
 import qualified Pate.Verification.Simplify as PSi
 
 import           Pate.Verification.PairGraph
-import           Pate.Verification.PairGraph.Node ( GraphNode(..), NodeEntry, mkNodeEntry, mkNodeReturn, nodeBlocks, addContext, returnToEntry, graphNodeBlocks, returnOfEntry, NodeReturn (nodeFuns), toSingleReturn, rootEntry, rootReturn, getDivergePoint, toSingleNode, mkNodeEntry', functionEntryOf, eqUptoDivergePoint, toSingleGraphNode )
+import           Pate.Verification.PairGraph.Node ( GraphNode(..), NodeEntry, mkNodeEntry, mkNodeReturn, nodeBlocks, addContext, returnToEntry, graphNodeBlocks, returnOfEntry, NodeReturn (nodeFuns), toSingleReturn, rootEntry, rootReturn, getDivergePoint, toSingleNode, mkNodeEntry', functionEntryOf, eqUptoDivergePoint, toSingleGraphNode, isSingleNodeEntry, divergePoint, isSingleReturn )
 import           Pate.Verification.Widening
 import qualified Pate.Verification.AbstractDomain as PAD
 import Data.Monoid (All(..), Any (..))
@@ -126,6 +130,7 @@ import qualified Data.Macaw.BinaryLoader as MBL
 import What4.Partial (justPartExpr)
 import qualified Data.Aeson as JSON
 
+
 -- Overall module notes/thoughts
 --
 -- Currently, we are making rather limited use
@@ -367,29 +372,58 @@ handleDanglingReturns fnPairs pg = do
          
   foldM go pg single_rets 
 
+-- FIXME: move this to Pate.Monad
+-- Helper functions for bringing PairGraphM operations and EquivM operations into the same monad
+
 
+withPG :: 
+  PairGraph sym arch -> 
+  StateT (PairGraph sym arch) (EquivM_ sym arch) a ->
+  EquivM sym arch (a, PairGraph sym arch)
+withPG pg f = runStateT f pg 
+
+withPG_ :: 
+  PairGraph sym arch -> 
+  StateT (PairGraph sym arch) (EquivM_ sym arch) a ->
+  EquivM sym arch (PairGraph sym arch)
+withPG_ pg f = execStateT f pg 
+
+liftPG :: PairGraphM sym arch a -> StateT (PairGraph sym arch) (EquivM_ sym arch) a
+liftPG f = do
+  pg <- get
+  case runPairGraphM pg f of
+    Left err -> lift $ throwHere $ PEE.PairGraphError err
+    Right (a,pg') -> do
+      put pg'
+      return a
+
+catchPG :: PairGraphM sym arch a -> StateT (PairGraph sym arch) (EquivM_ sym arch) (Maybe a)
+catchPG f = do
+  pg <- get
+  case runPairGraphM pg f of
+    Left{} -> return Nothing
+    Right (a,pg') -> do
+      put pg'
+      return $ Just a
+
+liftEqM :: 
+  (PairGraph sym arch -> EquivM_ sym arch (PairGraph sym arch)) -> 
+  StateT (PairGraph sym arch) (EquivM_ sym arch) ()
+liftEqM f = do
+  s <- get
+  s' <- lift $ f s
+  put s'
 
--- If the given 'GraphNode' is a synchronization point (i.e. it has
--- a corresponding synchronization edge), then we need to pop it from
--- the worklist and instead enqueue the corresponding biprogram nodes
 handleSyncPoint ::
-  PairGraph sym arch ->
   GraphNode arch ->
-  PAD.AbstractDomainSpec sym arch ->
-  EquivM sym arch (Maybe (PairGraph sym arch))
-handleSyncPoint pg nd _spec = case getDivergePoint nd of
-  -- not a diverging node
-  Nothing -> return Nothing
-  Just divergeNode -> do
-    Just (Some bin) <- return $ singleNodeRepr nd
-    case getSyncPoint pg bin divergeNode of
-      Just sync  -> do
-        case nd == sync of
-          True -> Just <$> updateCombinedSyncPoint divergeNode pg
-           -- We have a sync node but it hasn't been processed yet, so continue execution
-          False -> return Nothing
-      Nothing -> return Nothing
-
+  PairGraph sym arch ->
+  EquivM sym arch (PairGraph sym arch)
+handleSyncPoint nd pg = withPG_ pg $ do
+  divergeNode <- liftPG $ do
+    Just divergeNode <- return $ getDivergePoint nd
+    addSyncNode divergeNode nd
+    return divergeNode
+  liftEqM $ updateCombinedSyncPoint divergeNode
 
 addressOfNode ::
   GraphNode arch ->
@@ -420,26 +454,25 @@ chooseDesyncPoint ::
   EquivM sym arch (PairGraph sym arch)
 chooseDesyncPoint nd pg0 = do
   divergePair@(PPa.PatchPairC divergeO divergeP) <- PPa.forBinsC $ \bin -> do
-    let ret = case nd of
-          GraphNode ne -> returnOfEntry ne
-          ReturnNode nr -> nr
     blk <- PPa.get bin (graphNodeBlocks nd)
     pblks <- PD.lookupBlocks blk
-    retSingle <- toSingleReturn bin nd ret
     divergeSingle <- toSingleGraphNode bin nd
-    return $ (retSingle, divergeSingle, Some blk, pblks)
-  (sync, Some syncBin) <- pickCutPoint syncMsg
+    return $ (divergeSingle, Some blk, pblks)
+  (_, Some syncBin) <- pickCutPoint syncMsg
     [divergeO, divergeP]
   let otherBin = PBi.flipRepr syncBin
-
-  -- Introducing a cut-point is a stateful operation, as it modifies
-  -- the underlying ParsedFunctionMap to change the behavior of the disassembler
-  case sync of
-    GraphNode{} -> do
+  diverge <- PPa.getC otherBin divergePair
+  _ <- pickCutPoint syncMsg [diverge]
+  return pg0  
+  {-
+  choose @"()" "Choose corresponding point?" $ \choice -> do
+    choice "Yes" () $ do
+      let otherBin = PBi.flipRepr syncBin
       diverge <- PPa.getC otherBin divergePair
       _ <- pickCutPoint syncMsg [diverge]
       return pg0
-    _ -> return pg0
+    choice "No" () $ return pg0
+  -}
   where
     syncMsg = "Choose a desynchronization point:"
 
@@ -451,30 +484,25 @@ chooseSyncPoint ::
   EquivM sym arch (PairGraph sym arch)
 chooseSyncPoint nd pg0 = do
   divergePair@(PPa.PatchPairC divergeO divergeP) <- PPa.forBinsC $ \bin -> do
-    let ret = case nd of
-          GraphNode ne -> returnOfEntry ne
-          ReturnNode nr -> nr
     blk <- PPa.get bin (graphNodeBlocks nd)
     pblks <- PD.lookupBlocks blk
-    retSingle <- toSingleReturn bin nd ret
     divergeSingle <- toSingleGraphNode bin nd
-    return $ (retSingle, divergeSingle, Some blk, pblks)
+    return $ (divergeSingle, Some blk, pblks)
   (sync, Some syncBin) <- pickCutPoint syncMsg
     [divergeO, divergeP]
   let otherBin = PBi.flipRepr syncBin
-  pg1 <- setSyncPoint pg0 nd sync
-
-  case sync of
-    GraphNode{} -> do
-      diverge <- PPa.getC otherBin divergePair
-      syncOther <- fst <$> pickCutPoint syncMsg [diverge]
-      setSyncPoint pg1 nd syncOther
-    ReturnNode{} -> do
-      (retSingle, _, _, _) <- PPa.getC otherBin divergePair
-      setSyncPoint pg1 nd (ReturnNode retSingle)
+  
+  addr <- PB.concreteAddress <$> PPa.get syncBin (nodeBlocks sync)
+  withPG_ pg0 $ do 
+    liftPG $ setSyncAddress nd syncBin addr
+    diverge <- PPa.getC otherBin divergePair
+    syncOther <- lift $ fst <$> pickCutPoint syncMsg [diverge]
+    addrOther <- PB.concreteAddress <$> PPa.get otherBin (nodeBlocks syncOther) 
+    liftPG $ setSyncAddress nd otherBin addrOther
   where
     syncMsg = "Choose a synchronization point:"
 
+
 {-
 guessDivergence ::
   GraphNode arch {- divergence point -} -> 
@@ -521,31 +549,19 @@ getIntermediateAddrs pb =
 --   to the next CFAR (i.e. splits a CFAR in two at the given address)
 pickCutPoint ::
   String ->
-  [(NodeReturn arch, GraphNode arch, Some (PB.ConcreteBlock arch), PD.ParsedBlocks arch)] -> 
-  EquivM sym arch (GraphNode arch, Some PBi.WhichBinaryRepr)
+  [(GraphNode arch, Some (PB.ConcreteBlock arch), PD.ParsedBlocks arch)] -> 
+  EquivM sym arch (NodeEntry arch, Some PBi.WhichBinaryRepr)
 pickCutPoint msg inputs = do
-  (sync, Some bin, maddr) <- choose @"node" msg $ \choice -> do
-    forM_ inputs $ \(retSingle, divergeSingle, Some blk, PD.ParsedBlocks pblks) -> do
+  (sync, Some bin, (addr, Some blk)) <- choose @"node" msg $ \choice -> do
+    forM_ inputs $ \(divergeSingle, Some blk, PD.ParsedBlocks pblks) -> do
       let bin = PB.blockBinRepr blk
       forM_ pblks $ \pblk -> forM_ (getIntermediateAddrs pblk) $ \addr -> do
         -- FIXME: block entry kind is unused at the moment?
         let concBlk = PB.mkConcreteBlock blk PB.BlockEntryJump addr
         let node = mkNodeEntry' divergeSingle (PPa.mkSingle bin concBlk)
         choice "" (GraphNode node) $ do
-          
-          return (GraphNode node, Some bin, Just (addr, Some concBlk))
-      choice "" (ReturnNode retSingle) $ return (ReturnNode retSingle, Some bin, Nothing)
-  case maddr of
-    Just (addr, Some blk) -> do
-      _ <- addIntraBlockCut addr blk
-      -- this is a heuristic that attempts to capture the fact that
-      -- the patched binary likely has additional control flow that we
-      -- want to analyze as part of the synchronization block, but only
-      -- up to exactly the instruction where control flow re-synchronizes
-      case bin of
-        PBi.OriginalRepr -> cutAfterAddress addr blk
-        PBi.PatchedRepr -> return ()
-    Nothing -> return ()
+          return (node, Some bin, (addr, Some concBlk))
+  _ <- addIntraBlockCut addr blk
   return (sync, Some bin)
 
 -- | Add an intra-block cut to *both* binaries after the given address.
@@ -600,15 +616,77 @@ handleSyncPoint pg (ReturnNode nd) spec = case nodeFuns nd of
     Nothing -> return Nothing
 -}
 
-
-
--- FIXME: this is pretty brittle, as it makes a bunch of assumptions about
--- the graph state
+-- Connects the terminal nodes of any single-sided analysis to "merge" nodes
+-- Notably a single divergence may give rise to multiple synchronization points,
+-- since multiple CFARs may terminate at the provided address
+-- To address this we take the cartesian product of all original vs. patched sync points
+-- and create merge nodes for all of them
 updateCombinedSyncPoint ::
   GraphNode arch {- ^ diverging node -} ->
   PairGraph sym arch ->
   EquivM sym arch (PairGraph sym arch)
-updateCombinedSyncPoint divergeNode pg = fnTrace "updateCombinedSyncPoint" $ case getCombinedSyncPoint pg divergeNode of
+updateCombinedSyncPoint divergeNode pg_top = fnTrace "updateCombinedSyncPoint" $ withPG_ pg_top $ do
+  priority <- lift $ thisPriority
+  syncsO_ <- fmap Set.toList $ liftPG $ getSyncPoints PBi.OriginalRepr divergeNode
+  syncsP_ <- fmap Set.toList $ liftPG $ getSyncPoints PBi.PatchedRepr divergeNode
+
+  -- collect all sync points that have been found and that have a pre-domain
+  syncsO <- fmap catMaybes $ mapM (\nd -> catchPG $ fmap (nd,) $ getCurrentDomainM nd) syncsO_
+  syncsP <- fmap catMaybes $ mapM (\nd -> catchPG $ fmap (nd,) $ getCurrentDomainM nd) syncsP_
+
+  case syncsO of
+    -- We have not completed a single-sided analysis for the
+    -- Original binary.
+    -- We re-schedule the diverge node and any ancestors of discovered Original sync points.
+    -- This is needed to handle cases where the single-sided nodes have been dropped from
+    -- the graph as a result of some other operation (e.g. introducing an assertion).
+    -- In the case where the first Original single-sided node is dropped, this ensures that it is
+    -- re-scheduled by re-processing the divergence point.
+    [] -> withTracing @"message" "Missing Original sync point" $ do
+        divergeNodeO <- toSingleGraphNode PBi.OriginalRepr divergeNode
+        liftPG $ do
+          modify $ queueNode (priority PriorityDomainRefresh) divergeNodeO
+          -- also re-queue the ancestors of any known sync points that are missing domains
+          forM_ syncsO_ $ \syncO -> do
+            modify $ queueAncestors (priority PriorityHandleDesync) syncO
+    -- We have at least one completed one-sided analysis for the Original binary.
+    -- The convention is that we find at least one Original sync point before
+    -- moving on to the Patched one-sided analysis.
+    -- We artifically connect the post-domain of each Original one-sided analysis to the
+    -- pre-domain of the start of the Patched one-sided analysis. This ensures that any
+    -- assertions are carried forward to the Patched analysis.
+    _:_ -> do
+      (catchPG $ getCurrentDomainM divergeNode) >>= \case
+        Nothing -> liftPG $ modify $ queueNode (priority PriorityHandleDesync) divergeNode
+        Just dom_spec -> do
+          divergeNodeY <- toSingleGraphNode PBi.PatchedRepr divergeNode
+          fmap (\x -> PS.viewSpecBody x PS.unWS) $ PS.forSpec dom_spec $ \scope dom -> fmap PS.WithScope $ do
+            domP <- lift $ PAD.singletonDomain PBi.PatchedRepr dom
+            bundle <- lift $ noopBundle scope (graphNodeBlocks divergeNodeY)
+            forM_ syncsO $ \(syncO, _) -> do
+              liftPG $ (void $ getCurrentDomainM divergeNodeY) 
+                  <|> (modify $ \pg -> updateDomain' pg syncO divergeNodeY (PS.mkSimSpec scope domP) (priority PriorityWidening))
+              liftEqM $ \pg -> withPredomain scope bundle domP $ withConditionsAssumed scope syncO pg $
+                widenAlongEdge scope bundle syncO domP pg divergeNodeY
+
+      -- Finally, if we have any Patched one-sided results, we take all combinations
+      -- of Original and Patched sync points and connect them to a "combined" two-sided node
+      -- that contains the intersection of their pre-domains.
+      -- From this combined node, normal two-sided analysis can continue.
+      let syncPairs = [ (x,y) | x <- syncsO, y <- syncsP ]
+      forM_ syncPairs $ \((syncO, domO_spec), (syncP, domP_spec)) -> do
+        combinedNode <- liftPG $ do
+          Just combinedNode <- return $ combineNodes syncO syncP
+          return combinedNode
+        liftEqM $ mergeDualNodes syncO syncP domO_spec domP_spec combinedNode
+
+
+{-
+fnTrace "updateCombinedSyncPoint" $ do
+  runMaybeT $ do
+    getCombinedSyncPoint divergeNode
+
+  case getCombinedSyncPoint pg divergeNode of
   Nothing -> do
     emitTrace @"message" ("No sync node found for: " ++ show divergeNode)
     return pg
@@ -643,6 +721,7 @@ updateCombinedSyncPoint divergeNode pg = fnTrace "updateCombinedSyncPoint" $ cas
         priority <- thisPriority
         divergeNodeO <- toSingleGraphNode PBi.OriginalRepr divergeNode
         return $ queueNode (priority PriorityDomainRefresh) divergeNodeO $ queueAncestors (priority PriorityHandleDesync) syncO pg
+-}
 
 {-
 -- | Connect two nodes with a no-op
@@ -745,17 +824,15 @@ pairGraphComputeFixpoint entries gr_init = do
             True -> do
               emitTrace @"priority" priority
               atPriority priority (Just (show nd)) $ do
-                handleSyncPoint gr1 nd preSpec >>= \case
-                  Just gr2 -> return gr2
-                  Nothing -> PS.viewSpec preSpec $ \scope d -> do
-                    d' <- asks (PCfg.cfgStackScopeAssume . envConfig) >>= \case
-                      True -> strengthenStackDomain scope d
-                      False -> return d
-                    withAssumptionSet (PS.scopeAsm scope) $ do
-                      gr2 <- addRefinementChoice nd gr1
-                      gr3 <- visitNode scope nd d' gr2
-                      emitEvent $ PE.VisitedNode nd
-                      return gr3
+                PS.viewSpec preSpec $ \scope d -> do
+                  d' <- asks (PCfg.cfgStackScopeAssume . envConfig) >>= \case
+                    True -> strengthenStackDomain scope d
+                    False -> return d
+                  withAssumptionSet (PS.scopeAsm scope) $ do
+                    gr2 <- addRefinementChoice nd gr1
+                    gr3 <- visitNode scope nd d' gr2
+                    emitEvent $ PE.VisitedNode nd
+                    return gr3
         go gr4
     
     go_outer :: PairGraph sym arch -> EquivM_ sym arch (PairGraph sym arch)
@@ -1043,17 +1120,17 @@ withConditionsAssumed scope node gr0 f = do
     go condK g =
       withSatConditionAssumed scope node condK gr0 g
 
+
 processBundle ::
   forall sym arch v.
   PS.SimScope sym arch v ->
   NodeEntry arch ->
   SimBundle sym arch v ->
   AbstractDomain sym arch v ->
+  [(PPa.PatchPair (PB.BlockTarget arch))] ->
   PairGraph sym arch ->
   EquivM sym arch (PairGraph sym arch)
-processBundle scope node bundle d gr0 = do
-  exitPairs <- PD.discoverPairs bundle
-
+processBundle scope node bundle d exitPairs gr0 = do
   gr1 <- checkObservables node bundle d gr0
 
   -- Follow all the exit pairs we found
@@ -1182,7 +1259,15 @@ visitNode scope (GraphNode node@(nodeBlocks -> bPair)) d gr0 =
             Just gr3 -> do
               priority <- thisPriority
               return $ queueNode (priority PriorityHandleActions) (GraphNode node) gr3
-            Nothing -> withConditionsAssumed scope (GraphNode node) gr0 $ processBundle scope node bundle d gr2
+            Nothing -> withConditionsAssumed scope (GraphNode node) gr0 $ do
+              exitPairs <- PD.discoverPairs bundle
+              -- if a sync point is reachable then we don't want to do
+              -- further analysis, since we want to instead treat this
+              -- node as a merge point
+              withPG_ gr2 $ do
+                (liftPG $ checkForNodeSync node exitPairs) >>= \case
+                  True -> liftEqM $ handleSyncPoint (GraphNode node)
+                  False -> liftEqM $ processBundle scope node bundle d exitPairs 
 
 visitNode scope (ReturnNode fPair) d gr0 =  do
   -- propagate the abstract domain of the return node to
@@ -1204,7 +1289,10 @@ visitNode scope (ReturnNode fPair) d gr0 =  do
           priority <- thisPriority
           return $ queueNode (priority PriorityHandleActions) (ReturnNode fPair) gr1      
         Nothing -> withTracing @"message" "Toplevel Return" $ do
-          withConditionsAssumed scope (ReturnNode fPair) gr0' $ 
+          withConditionsAssumed scope (ReturnNode fPair) gr0' $ do
+            case isSingleReturn fPair of
+              Just{} -> void $ emitError' $ PEE.OrphanedSingletonAnalysis (nodeFuns fPair)
+              Nothing -> return ()
             return gr0'
 
    -- Here, we're using a bit of a trick to propagate abstract domain information to call sites.
@@ -1212,7 +1300,7 @@ visitNode scope (ReturnNode fPair) d gr0 =  do
    -- using the ordinary widening machinery.
 
 
-  processReturn gr0' node@(nodeBlocks -> ret) = withPair ret $ withAbsDomain node d gr0 $ do
+  processReturn gr0' node@(nodeBlocks -> ret) = do
     let
       vars = PS.scopeVars scope
       varsSt = TF.fmapF PS.simVarState vars
@@ -1233,12 +1321,13 @@ visitNode scope (ReturnNode fPair) d gr0 =  do
             -- TODO: formally we could just check the event sequence once for the return node
             -- (rather than once for each return edge)
             -- but it would require some refactoring to make the types match up correctly
-            gr1' <- checkObservables node bundle d gr0'
-    --        traceBundle bundle "== bundle asm =="
-    --        traceBundle bundle (show (W4.printSymExpr asm))
-            widenAlongEdge scope bundle (ReturnNode fPair) d gr1' (GraphNode node)
-
-
+            withPG_ gr0' $ do
+              liftEqM $ checkObservables node bundle d
+              liftEqM $ \pg -> widenAlongEdge scope bundle (ReturnNode fPair) d pg (GraphNode node)
+              (liftPG $ checkForReturnSync fPair node) >>= \case
+                True -> liftEqM $ handleSyncPoint (GraphNode node)
+                False -> return ()
+                
 -- | Construct a "dummy" simulation bundle that basically just
 --   immediately returns the prestate as the poststate.
 --   This is used to compute widenings that propagate abstract domain
@@ -2295,11 +2384,16 @@ handleDivergingPaths scope bundle currBlock st dom blkt = fnTrace "handleDivergi
   priority <- thisPriority
   currBlockO <- toSingleNode PBi.OriginalRepr currBlock
   currBlockP <- toSingleNode PBi.PatchedRepr currBlock
-
-  case (getSyncPoint gr0 PBi.OriginalRepr (GraphNode currBlock), getSyncPoint gr0 PBi.PatchedRepr (GraphNode currBlock)) of
-    (Just{},Just{}) -> do
+  
+  -- check if we already have defined a sync address for this divergence
+  let hasSyncPoints = execPairGraphM gr0 $ do
+        _ <- getSyncAddress PBi.OriginalRepr (GraphNode currBlock)
+        _ <- getSyncAddress PBi.PatchedRepr (GraphNode currBlock)
+        return ()
+
+  case hasSyncPoints of
+    Right{} -> do
       bundleO <- noopBundle scope (nodeBlocks currBlockO)
-
       atPriority (raisePriority (priority PriorityHandleDesync)) Nothing $ do
         -- we arbitrarily pick the original program to perform the first step of
         -- the analysis
@@ -2308,7 +2402,7 @@ handleDivergingPaths scope bundle currBlock st dom blkt = fnTrace "handleDivergi
         gr1 <- withTracing @"node" (GraphNode currBlockO) $ 
           widenAlongEdge scope bundleO (GraphNode currBlock) dom gr0 (GraphNode currBlockO)
         return $ updateBranchGraph st blkt gr1
-    _ -> do
+    Left{} -> do
       let divergeNode = GraphNode currBlock
       let pg = gr0
       let msg = "Control flow desynchronization found at: " ++ show divergeNode
@@ -2427,6 +2521,7 @@ handleJump ::
 handleJump scope bundle currBlock d gr nextNode =
   widenAlongEdge scope bundle (GraphNode currBlock) d gr (GraphNode nextNode)
 
+
 mkSimBundle ::
   forall sym arch v.
   PairGraph sym arch ->
diff --git a/tests/aarch32/desync-defer.pate b/tests/aarch32/desync-defer.pate
index f9be70a1..9bbb9948 100644
--- a/tests/aarch32/desync-defer.pate
+++ b/tests/aarch32/desync-defer.pate
@@ -10,9 +10,8 @@ Function Entry "f" (0x10158)
 
         ...
         Choose a desynchronization point:
-            > 0x1016c (original)
-            > 0x1016c (patched)
-            // 0x1070 - should be this, but the splitting for desync points is incorrect
+            > 0x10170 (original)
+            > 0x10170 (patched)
 
 0x10170 [ via: "f" (0x10158) <- "_start" (0x10218) (original) vs. "_start" (0x10214) (patched) ]
     ...
@@ -24,9 +23,22 @@ Function Entry "f" (0x10158)
         ...
         Choose a synchronization point:
             > 0x10188 (original)
-            > 0x10178 (patched)
+            > 0x10170 (patched)
 
 0x101e8 (original) vs. 0x101d8 (patched)
+    ...
+    Return (original) vs. Call to: "g"
+        ...
+        ...
+        > Choose desynchronization points
+        
+        ...
+        Choose a desynchronization point:
+            > 0x101f4 (original)
+            > 0x101e4 (patched)
+
+
+0x101f4 (original) vs. 0x101e4 (patched)
     ...
     Return (original) vs. Call to: "g"
         ...
@@ -35,9 +47,11 @@ Function Entry "f" (0x10158)
 
         ...
         Choose a synchronization point:
-            > Return "f" (0x10158)
-            // applies to both original and patched
+            > 0x101f4 (original)
+            > 0x101ec (patched)
+
+
 
 Verification Finished
 Continue verification?
-    > Finish and view final result
+    > Finish and view final result
\ No newline at end of file
diff --git a/tests/aarch32/scripted/challenge10.pate b/tests/aarch32/scripted/challenge10.pate
index dae6b326..1bf6c3e9 100644
--- a/tests/aarch32/scripted/challenge10.pate
+++ b/tests/aarch32/scripted/challenge10.pate
@@ -1,7 +1,20 @@
 Choose Entry Point
     > Function Entry "transport_handler" (segment1+0x400c)
 
+
 segment1+0x4114 [ via: "transport_handler" (segment1+0x400c) ]
+    ...
+    Call to: "puts" (segment1+0x33ac) Returns to: "transport_handler" (segment1+0x41b8) (original) vs. Call to: segment1+0x3dd24 Returns to: "transport_handler" (segment1+0x3dd44) (patched)
+        ...
+            ...
+            > Choose desynchronization points
+
+            Choose a desynchronization point:
+                > segment1+0x4120 (original)
+                > segment1+0x4120 (patched)
+
+
+segment1+0x4120 [ via: "transport_handler" (segment1+0x400c) ]
     ...
     Call to: "puts" (segment1+0x33ac) Returns to: "transport_handler" (segment1+0x41b8) (original) vs. Call to: segment1+0x3dd24 Returns to: "transport_handler" (segment1+0x3dd44) (patched)
         ...
@@ -9,10 +22,10 @@ segment1+0x4114 [ via: "transport_handler" (segment1+0x400c) ]
             > Choose synchronization points
 
             Choose a synchronization point:
-                > segment1+0x3dd44 (patched)
-                > segment1+0x4128 (original)
+                > segment1+0x412a (patched)
+                > segment1+0x412a (original)
 
-segment1+0x4128 (original) vs. segment1+0x3dd44 (patched) [ via: "transport_handler" (segment1+0x400c) ]
+segment1+0x4120 (original) vs. segment1+0x3dd44 (patched) [ via: "transport_handler" (segment1+0x400c) ]
     ...
         Call to: "puts" (segment1+0x33ac) Returns to: "transport_handler" (segment1+0x41b8) (original) vs. Jump to: "transport_handler" (segment1+0x412a) (patched)
             ...
diff --git a/tests/aarch32/unequal/desync-defer.pate b/tests/aarch32/unequal/desync-defer.pate
index f9be70a1..9bbb9948 100644
--- a/tests/aarch32/unequal/desync-defer.pate
+++ b/tests/aarch32/unequal/desync-defer.pate
@@ -10,9 +10,8 @@ Function Entry "f" (0x10158)
 
         ...
         Choose a desynchronization point:
-            > 0x1016c (original)
-            > 0x1016c (patched)
-            // 0x1070 - should be this, but the splitting for desync points is incorrect
+            > 0x10170 (original)
+            > 0x10170 (patched)
 
 0x10170 [ via: "f" (0x10158) <- "_start" (0x10218) (original) vs. "_start" (0x10214) (patched) ]
     ...
@@ -24,9 +23,22 @@ Function Entry "f" (0x10158)
         ...
         Choose a synchronization point:
             > 0x10188 (original)
-            > 0x10178 (patched)
+            > 0x10170 (patched)
 
 0x101e8 (original) vs. 0x101d8 (patched)
+    ...
+    Return (original) vs. Call to: "g"
+        ...
+        ...
+        > Choose desynchronization points
+        
+        ...
+        Choose a desynchronization point:
+            > 0x101f4 (original)
+            > 0x101e4 (patched)
+
+
+0x101f4 (original) vs. 0x101e4 (patched)
     ...
     Return (original) vs. Call to: "g"
         ...
@@ -35,9 +47,11 @@ Function Entry "f" (0x10158)
 
         ...
         Choose a synchronization point:
-            > Return "f" (0x10158)
-            // applies to both original and patched
+            > 0x101f4 (original)
+            > 0x101ec (patched)
+
+
 
 Verification Finished
 Continue verification?
-    > Finish and view final result
+    > Finish and view final result
\ No newline at end of file