Small cleanups in prover backends

GaloisInc · Jun 14, 2021 · 5aa184b · 5aa184b
1 parent 7467745
commit 5aa184b
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 6 deletions.
diff --git a/src/SAWScript/Prover/Exporter.hs b/src/SAWScript/Prover/Exporter.hs
@@ -156,8 +156,9 @@ withABCVerilog baseName t buildCmd =
 -- file.
 writeAIG_SATviaVerilog :: FilePath -> SATQuery -> TopLevel ()
 writeAIG_SATviaVerilog f query =
-  getSharedContext >>= \sc ->
-  writeAIGviaVerilog f =<< liftIO (satQueryAsTerm sc query)
+  do sc <- getSharedContext
+     t <- liftIO (satQueryAsTerm sc query)
+     writeAIGviaVerilog f t
 
 -- | Write a @Term@ representing a an arbitrary function to an AIG file
 -- by using ABC to convert a Verilog file.
@@ -170,8 +171,9 @@ writeAIGviaVerilog aigFile t =
 -- file.
 writeCNF_SATviaVerilog :: FilePath -> SATQuery -> TopLevel ()
 writeCNF_SATviaVerilog f query =
-  getSharedContext >>= \sc ->
-  writeCNFviaVerilog f =<< liftIO (satQueryAsTerm sc query)
+  do sc <- getSharedContext
+     t <- liftIO (satQueryAsTerm sc query)
+     writeCNFviaVerilog f t
 
 -- | Write a @Term@ representing a an arbitrary function to a CNF file
 -- by using ABC to convert a Verilog file.

diff --git a/src/SAWScript/Prover/SBV.hs b/src/SAWScript/Prover/SBV.hs
@@ -35,8 +35,8 @@ proveUnintSBV ::
   TopLevel (Maybe CEX, SolverStats)
     -- ^ (example/counter-example, solver statistics)
 proveUnintSBV conf unintSet timeout goal =
-  getSharedContext >>= \sc ->
-  io $ proveUnintSBVIO sc conf unintSet timeout goal
+  do sc <- getSharedContext
+     io $ proveUnintSBVIO sc conf unintSet timeout goal
 
 proveUnintSBVIO ::
   SharedContext ->