diff --git a/solutions/src/2024/16.hs b/solutions/src/2024/16.hs
index 9d6e05c..fc49e81 100644
--- a/solutions/src/2024/16.hs
+++ b/solutions/src/2024/16.hs
@@ -92,7 +92,7 @@ main =
                   ++ [(   1, (p', v)) | let p' = p + v, open ! p']
         isEnd (p, _) = p == end
 
-        (cost, ends, preds) = shortestPath (start, east) step isEnd
+        Just (cost, ends, preds) = shortestPath (start, east) step isEnd
         nodesOnShortestPaths = Set.map fst (fillN (preds Map.!) ends)
 
     print cost
@@ -101,19 +101,19 @@ main =
 -- | Main loop for a shortest-path implementation that computes the cost of the shortest path.
 shortestPath ::
   Ord a =>
-  a                      {- ^ initial node -} ->
-  (a -> [(Int, a)])      {- ^ successors of a node -} ->
-  (a -> Bool)            {- ^ predicate for the destination -} ->
-  (Int, [a], Map a [a])  {- ^ cost, reached end states, predecessors -}
+  a                           {- ^ initial node -} ->
+  (a -> [(Int, a)])           {- ^ successors of a node -} ->
+  (a -> Bool)                 {- ^ predicate for the destination -} ->
+  Maybe (Int, [a], Map a [a]) {- ^ cost, reached end states, predecessors -}
 shortestPath start step isEnd = go Map.empty (IntMap.singleton 0 (Map.singleton start []))
   where
     addWork q (k, v) = IntMap.insertWith (Map.unionWith (++)) k v q
     go seen q =
       case IntMap.minViewWithKey q of
-        Nothing -> error "no solution"
+        Nothing -> Nothing
         Just ((cost, states), q1)
           | null done -> go seen' q2
-          | otherwise -> (cost, done, seen')
+          | otherwise -> Just (cost, done, seen')
           where
             -- remove all the states at this cost that we've seen at a lower cost
             states' = Map.difference states seen
diff --git a/solutions/src/2024/17.hs b/solutions/src/2024/17.hs
index e63117d..12e9783 100644
--- a/solutions/src/2024/17.hs
+++ b/solutions/src/2024/17.hs
@@ -1,4 +1,4 @@
-{-# Language QuasiQuotes, BlockArguments, ImportQualifiedPost #-}
+{-# Language QuasiQuotes, BlockArguments, ImportQualifiedPost, LambdaCase #-}
 {-|
 Module      : Main
 Description : Day 17 solution
@@ -9,15 +9,14 @@ Maintainer  : emertens@gmail.com
 <https://adventofcode.com/2024/day/17>
 
 -}
-module Main where
+module Main (main) where
 
 import Advent (format)
 import Data.List (intercalate)
 import Data.SBV
-    ( Word64, optLexicographic, free, minimize, sShiftRight,
-      (.==), (./=), shiftR, xor, (.&.),
-      SWord64, constrain,
-      Symbolic, getModelValue)
+    (Word64, SWord64, SBool,
+     (.==), (./=), (.&.), (.&&), sShiftRight, shiftR, xor,
+     optLexicographic, free, minimize, constrain, getModelValue)
 
 -- | >>> :main
 -- 2,7,4,7,2,1,7,5,1
@@ -30,47 +29,41 @@ main =
       Register C: %u%n
       %n
       Program: %u&,%n|]
-    
-    putStrLn (intercalate "," (map show (run program 0 a b c)))
+
+    putStrLn (intercalate "," (map show (run (Machine a b c) program)))
 
     res <- optLexicographic
-      do a  <- free "a" :: Symbolic SWord64    
-         minimize "smallest" a 
-         direct a program
+      do a2 <- free "a"
+         minimize "smallest" a2
+         constrain (part2 a2 program)
     case getModelValue "a" res of
       Just x -> print (x :: Word64)
       Nothing -> fail "no solution"
 
-run :: [Int] -> Int -> Int -> Int -> Int -> [Int]
-run pgm ip a b c =
-  let combo 0 = 0
-      combo 1 = 1
-      combo 2 = 2
-      combo 3 = 3
-      combo 4 = a
-      combo 5 = b
-      combo 6 = c in
-  case drop ip pgm of
-    0 : x : _ -> run pgm (ip+2) (a `shiftR` combo x) b c
-    1 : x : _ -> run pgm (ip+2) a (b `xor` x) c
-    2 : x : _ -> run pgm (ip+2) a (combo x .&. 7) c
-    3 : x : _ | a == 0    -> run pgm (ip+2) a b c
-              | otherwise -> run pgm x a b c
-    4 : _ : _ -> run pgm (ip+2) a (b `xor` c) c
-    5 : x : _ -> combo x .&. 7 : run pgm (ip+2) a b c
-    6 : x : _ -> run pgm (ip+2) a (a `shiftR` combo x) c
-    7 : x : _ -> run pgm (ip+2) a b (a `shiftR` combo x)
-    _ -> []
+data Machine = Machine { rA, rB, rC :: !Int }
+
+run :: Machine -> [Int] -> [Int]
+run m0 pgm = go m0 pgm
+  where
+    go m = \case
+      0 : x : ip' -> go m{ rA = rA m `shiftR` combo x } ip'
+      1 : x : ip' -> go m{ rB = rB m `xor`          x } ip'
+      2 : x : ip' -> go m{ rB = combo x .&. 7         } ip'
+      3 : x : ip' -> go m (if rA m == 0 then ip' else drop x pgm)
+      4 : _ : ip' -> go m{ rB = rB m `xor`    rC m    } ip'
+      5 : x : ip' -> combo x .&. 7 : go m ip'
+      6 : x : ip' -> go m{ rB = rA m `shiftR` combo x } ip'
+      7 : x : ip' -> go m{ rC = rA m `shiftR` combo x } ip'
+      _           -> []
+      where
+        combo = \case
+          0 -> 0; 1 -> 1; 2 -> 2; 3 -> 3
+          4 -> rA m; 5 -> rB m; 6 -> rC m
+          _ -> error "invalid combo operand"
 
-direct :: SWord64 -> [Int] -> Symbolic ()
-direct a [] = constrain (a .== 0)
-direct a (o:os) =
-  do constrain (a ./= 0)
-     b <- pure (a .&. 7)
-     b <- pure (b `xor` 2)
-     c <- pure (a `sShiftRight` b)
-     b <- pure (b `xor` c)
-     b <- pure (b `xor` 3)
-     constrain ((b .&. 7) .== fromIntegral o)
-     a <- pure (a `shiftR` 3)
-     direct a os
+part2 :: SWord64 -> [Int] -> SBool
+part2 a []     = a .== 0
+part2 a (o:os) = a ./= 0 .&& b2 .== fromIntegral o .&& part2 (a `shiftR` 3) os
+  where
+    b1 = a .&. 7 `xor` 2
+    b2 = (a `sShiftRight` b1 `xor` b1 `xor` 3) .&. 7