diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,9 @@
 # Revision history for crucible-symio
 
+## 0.1.1 -- 2024-08-30
+
+* Add support for GHC 9.8
+
 ## 0.1 -- 2024-02-05
 
 * First version. Released on an unsuspecting world.
diff --git a/crucible-symio.cabal b/crucible-symio.cabal
--- a/crucible-symio.cabal
+++ b/crucible-symio.cabal
@@ -6,7 +6,7 @@
   reading and writing symbolic data. An example use case would be to support verifying
   programs that e.g., use configuration files or accept input from files.
 name:                crucible-symio
-version:             0.1
+version:             0.1.1
 license:             BSD-3-Clause
 license-file:        LICENSE
 author:              Daniel Matichuk
@@ -21,7 +21,7 @@
   subdir:   crucible-symio
 
 common shared
-  build-depends:       base >=4.12 && <4.19,
+  build-depends:       base >=4.12 && <4.20,
                        aeson,
                        bv-sized,
                        bytestring,
@@ -63,7 +63,7 @@
   main-is: TestMain.hs
   hs-source-dirs: tests, src
   ghc-options: -Wall -Wcompat
-  build-depends: base >=4.12 && <4.19,
+  build-depends: base >=4.12 && <4.20,
                  what4,
                  crucible,
                  crucible-symio,
diff --git a/tests/TestMain.hs b/tests/TestMain.hs
--- a/tests/TestMain.hs
+++ b/tests/TestMain.hs
@@ -27,6 +27,7 @@
 import           Control.Lens ( (^.) )
 
 import           Control.Monad (foldM )
+import           Control.Monad.Except (runExceptT)
 import           Control.Monad.IO.Class (liftIO)
 import qualified Data.Map as Map
 import qualified Data.Parameterized.Context as Ctx
@@ -42,6 +43,7 @@
 import qualified Test.Tasty as T
 import qualified Test.Tasty.HUnit as T
 
+import qualified Lang.Crucible.Backend.Prove as CB
 import qualified Lang.Crucible.Backend.Simple as CB
 import qualified Lang.Crucible.Backend as CB
 import qualified Lang.Crucible.CFG.Core as CC
@@ -50,13 +52,14 @@
 import qualified Lang.Crucible.Simulator.OverrideSim as CSO
 import qualified Lang.Crucible.FunctionHandle as CFH
 import qualified Lang.Crucible.Simulator.GlobalState as CGS
+import qualified Lang.Crucible.Utils.Seconds as Sec
+import qualified Lang.Crucible.Utils.Timeout as CTO
 
 import qualified What4.Interface as W4
 import qualified What4.Expr as WE
 import qualified What4.Config as W4C
 import qualified What4.Solver.Yices as W4Y
 import qualified What4.Solver.Adapter as WSA
-import qualified What4.SatResult as W4R
 import qualified What4.Partial as W4
 
 import qualified What4.CachedArray as CA
@@ -133,29 +136,24 @@
         _ -> do
           putStrLn $ showF p
           T.assertFailure "Partial Result"
-  obligations <- CB.getProofObligations bak
-  mapM_ (proveGoal sym W4Y.yicesAdapter) (maybe [] CB.goalsToList obligations)
 
-
-proveGoal ::
-  (sym ~ WE.ExprBuilder t st fs) =>
-  CB.IsSymInterface sym =>
-  sym ->
-  WSA.SolverAdapter st ->
-  CB.ProofGoal (CB.Assumptions sym) (CB.Assertion sym) ->
-  IO ()
-proveGoal sym adapter (CB.ProofGoal asms goal) = do
-  let goalPred = goal ^. CB.labeledPred
-  asmsPred <- CB.assumptionsPred sym asms
-  notgoal <- W4.notPred sym goalPred
-  WSA.solver_adapter_check_sat adapter sym WSA.defaultLogData [notgoal, asmsPred] $ \sr ->
-    case sr of
-      W4R.Unsat _ -> return ()
-      W4R.Unknown -> T.assertFailure "Inconclusive"
-      W4R.Sat _ -> do
+  let timeout = CTO.Timeout (Sec.secondsFromInt 5)
+  let prover = CB.offlineProver timeout sym WSA.defaultLogData W4Y.yicesAdapter
+  let strat = CB.ProofStrategy prover CB.failFast
+  merr <- runExceptT $ CB.proveCurrentObligations bak strat $ CB.ProofConsumer $ \obligation ->
+    \case
+      CB.Proved {} -> return ()
+      CB.Unknown {} -> T.assertFailure "Inconclusive"
+      CB.Disproved  _ _ -> do
+        CB.ProofGoal asms goal <- pure obligation
+        asmsPred <- CB.assumptionsPred sym asms
+        let goalPred = goal ^. CB.labeledPred
         putStrLn (showF asmsPred)
         putStrLn (showF goalPred)
         T.assertFailure "Assertion Failure"
+  case merr of
+    Left CTO.TimedOut -> T.assertFailure "Timeout"
+    Right () -> pure ()
 
 showAbortedResult :: CS.AbortedResult c d -> String
 showAbortedResult ar = case ar of