From 3fedbb9f65688784a93281a38c70994fbe70aae8 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 9 Apr 2025 07:43:20 -0400
Subject: [PATCH 1/2] Whitespace only

---
 lib/Language/ASL.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/lib/Language/ASL.hs b/lib/Language/ASL.hs
index cbe939b..d345c34 100644
--- a/lib/Language/ASL.hs
+++ b/lib/Language/ASL.hs
@@ -198,7 +198,7 @@ simulateFunction symCfg crucFunc = genSimulation symCfg crucFunc extractResult
                 (CS.regValue re)
                 WI.NeverUnfold
               checkClosedTerm allArgBvs (CS.regValue re)
-              
+
               return $ fn
           | otherwise -> X.throwIO (UnexpectedReturnType btr)
 
@@ -398,7 +398,7 @@ data SimulationException = SimulationTimeout (Some AC.SomeFunctionSignature)
 
 instance PP.Pretty SimulationException where
   pPrint e = case e of
-    
+
     SimulationTimeout (Some fs) -> PP.text "SimulationTimeout:" PP.<+> PP.text (show fs)
     SimulationAbort (Some fs) msg ->
       PP.text "SimulationAbort:" PP.<+> PP.text (T.unpack msg) PP.<+> PP.text (show fs)

From ce6564eb2fba075b7d08108bbd5d89404ca3f4fb Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 9 Apr 2025 07:41:37 -0400
Subject: [PATCH 2/2] Bump submodules, adapt to changes in
 GaloisInc/crucible#1331

This bumps the following submodules:

* `crucible`, to bring in the changes from
  https://github.com/GaloisInc/crucible/pull/1331 (the primary purpose of this
  patch)
* `what4`, which is necessary to stay in sync with `crucible`.

https://github.com/GaloisInc/crucible/pull/1331 adds a new field to
`AbortedExit`, which `asl-translator` pattern-matches on in `Language.ASL`. As
such, this patch also makes a minor code change to keep that particular bit of
code compiling.
---
 lib/Language/ASL.hs | 2 +-
 submodules/crucible | 2 +-
 submodules/what4    | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/lib/Language/ASL.hs b/lib/Language/ASL.hs
index d345c34..1a2679a 100644
--- a/lib/Language/ASL.hs
+++ b/lib/Language/ASL.hs
@@ -428,7 +428,7 @@ showExpr e = PP.text (LPP.renderString (LPP.layoutPretty opts (WI.printSymExpr e
 showAbortedResult :: CS.AbortedResult c d -> T.Text
 showAbortedResult ar = case ar of
   CS.AbortedExec reason _ -> T.pack $ show reason
-  CS.AbortedExit code -> T.pack $ show code
+  CS.AbortedExit code _ -> T.pack $ show code
   CS.AbortedBranch _ _ res' res'' -> "BRANCH: " <> showAbortedResult res' <> "\n" <> showAbortedResult res''
 
 
diff --git a/submodules/crucible b/submodules/crucible
index e861406..f91cfe0 160000
--- a/submodules/crucible
+++ b/submodules/crucible
@@ -1 +1 @@
-Subproject commit e86140641260b00f64fdbd51d73d48d766c55bdf
+Subproject commit f91cfe0d4746728b098c12516862714fcc5628ce
diff --git a/submodules/what4 b/submodules/what4
index 494ac64..43553b9 160000
--- a/submodules/what4
+++ b/submodules/what4
@@ -1 +1 @@
-Subproject commit 494ac6416ed01eab6ae5d1be427d0aaae4c4bb91
+Subproject commit 43553b9205b8748f2fc3b56e86697ec663211f39