diff --git a/refinement/src/Data/Macaw/Refinement/Path.hs b/refinement/src/Data/Macaw/Refinement/Path.hs
index 569f9587..c5da2728 100644
--- a/refinement/src/Data/Macaw/Refinement/Path.hs
+++ b/refinement/src/Data/Macaw/Refinement/Path.hs
@@ -4,6 +4,7 @@ module Data.Macaw.Refinement.Path
   ( FuncBlockPath(..)
   , buildFuncPath
   , pathDepth
+  , pathForwardTrails
   , pathTo
   , takePath
   )
@@ -161,3 +162,32 @@ takePath n (Path blkid anc loop) =
 pathDepth :: FuncBlockPath arch -> Int
 pathDepth (Path _ [] _) = 0
 pathDepth (Path _ anc _) = 1 + maximum (pathDepth <$> anc)
+
+
+-- | Converts a Path tree into a list of the distinct paths, where
+-- each path is represented by a list of block IDs in the order that
+-- they would be executed (i.e. the back-path is converted to a
+-- forward-chain list.
+--
+-- For example:
+--
+-- > Path 1
+-- >   [ Path 2 [ Path 3 ] []
+-- >   , Path 4 [ Path 5 [ Path 6 [] []
+-- >                     , Path 7 [ Path 3 [] []] []
+-- >                     ] []
+-- >            ] []
+-- >   ] []
+--
+-- Is converted to:
+--
+-- >  [ [ 3, 2, 1 ]
+-- >  , [ 6, 5, 4, 1 ]
+-- >  , [ 3, 7, 5, 4, 1 ]
+-- >  ]
+--
+pathForwardTrails :: FuncBlockPath arch -> [ [BlockIdentifier arch] ]
+pathForwardTrails (Path i [] _) = [[i]]
+pathForwardTrails (Path i anc _) = let ft = concatMap pathForwardTrails anc
+                                       appendTo v l = l <> [v]
+                                   in map (appendTo i) ft
diff --git a/refinement/src/Data/Macaw/Refinement/UnknownTransfer.hs b/refinement/src/Data/Macaw/Refinement/UnknownTransfer.hs
index ba7b966e..c37c6d8d 100644
--- a/refinement/src/Data/Macaw/Refinement/UnknownTransfer.hs
+++ b/refinement/src/Data/Macaw/Refinement/UnknownTransfer.hs
@@ -130,8 +130,11 @@ import Data.Macaw.Discovery.State ( DiscoveryFunInfo
                                   , parsedBlocks
                                   , stmtsTerm
                                   )
-import Data.Macaw.Refinement.FuncBlockUtils ( BlockIdentifier, blockID, funForBlock, getBlock )
-import Data.Macaw.Refinement.Path ( FuncBlockPath(..), buildFuncPath, pathDepth, pathTo, takePath )
+import Data.Macaw.Refinement.FuncBlockUtils ( BlockIdentifier, blockID
+                                            , funForBlock, getBlock )
+import Data.Macaw.Refinement.Path ( FuncBlockPath(..)
+                                  , buildFuncPath, pathDepth, pathForwardTrails
+                                  , pathTo, takePath )
 import qualified Data.Macaw.Symbolic as MS
 import Data.Map (Map)
 import Data.Maybe
@@ -278,21 +281,16 @@ refinePath inpDS path maxlevel numlevels prevResult =
                        then return bestResult
                        else refinePath inpDS path maxlevel nextlevel bestResult
 
-data Equation arch = Equation (DiscoveryState arch) (Some (ParsedBlock arch))
+data Equation arch = Equation (DiscoveryState arch) [[Some (ParsedBlock arch)]]
 type Solution arch = [ArchSegmentOff arch]  -- identified transfers
 
 equationFor :: DiscoveryState arch -> FuncBlockPath arch -> Equation arch
-equationFor inpDS (Path bid anc _loop) =
-  let curBlk = getBlock inpDS bid
-  in case curBlk of
-       Nothing -> error "did not find requested block in discovery results!" -- internal
-       Just b ->
-         if null anc
-         then Equation inpDS b
-         else undefined
-              -- Should linearly combine the anc statements with the
-              -- current block's statements and asserts that state that
-              -- the IP from one to the next is expected.
+equationFor inpDS p =
+  let pTrails = pathForwardTrails p
+      pTrailBlocks = map (getBlock inpDS) <$> pTrails
+  in if and (any (not . isJust) <$> pTrailBlocks)
+     then error "did not find requested block in discovery results!" -- internal
+       else Equation inpDS (catMaybes <$> pTrailBlocks)
 
 solve :: ( MS.SymArchConstraints arch
          , 16 <= MC.ArchAddrWidth arch
@@ -401,6 +399,21 @@ initRegs arch_vals sym ip_val = do
     (MS.updateReg arch_vals) reg_struct MC.ip_reg ip_val
 
 smtSolveTransfer
+  :: forall arch t solver fp m
+   . ( MS.SymArchConstraints arch
+     , C.IsSymInterface (C.OnlineBackend t solver fp)
+     , W.OnlineSolver t solver
+     , MonadIO m
+     )
+  => RefinementContext arch t solver fp
+  -> DiscoveryState arch
+  -> [[Some (ParsedBlock arch)]]
+  -> m [ArchSegmentOff arch]
+smtSolveTransfer rc ds blockPaths =
+  -- wrong thing: fix the handling of blockPaths
+  smtSolveTransfer' rc ds $ head $ head blockPaths
+
+smtSolveTransfer'
   :: forall arch t solver fp m
    . ( MS.SymArchConstraints arch
      , C.IsSymInterface (C.OnlineBackend t solver fp)
@@ -411,7 +424,7 @@ smtSolveTransfer
   -> DiscoveryState arch
   -> Some (ParsedBlock arch)
   -> m [ArchSegmentOff arch]
-smtSolveTransfer RefinementContext{..} discovery_state (Some block) = do
+smtSolveTransfer' RefinementContext{..} discovery_state (Some block) = do
   let arch = Proxy @arch
   block_ip_val <- case MC.segoffAsAbsoluteAddr (pblockAddr block) of
     Just addr -> liftIO $ LLVM.llvmPointer_bv symbolicBackend