From a7e09a68e90b81fbc428d2acf655b25a21298584 Mon Sep 17 00:00:00 2001
From: Gergo ERDI <gergo@erdi.hu>
Date: Wed, 16 Oct 2024 17:14:58 +0800
Subject: [PATCH] Only produce `.smt2` files when the `save` flag is turned on

(See https://github.com/ucsd-progsys/liquidhaskell/issues/2357)
---
 src/Language/Fixpoint/Smt/Interface.hs | 22 ++++++++++++----------
 1 file changed, 12 insertions(+), 10 deletions(-)

diff --git a/src/Language/Fixpoint/Smt/Interface.hs b/src/Language/Fixpoint/Smt/Interface.hs
index 2642c6335..4bc0dc6f9 100644
--- a/src/Language/Fixpoint/Smt/Interface.hs
+++ b/src/Language/Fixpoint/Smt/Interface.hs
@@ -60,11 +60,7 @@ module Language.Fixpoint.Smt.Interface (
     ) where
 
 import           Language.Fixpoint.Types.Config ( SMTSolver (..)
-                                                , Config
-                                                , solver
-                                                , smtTimeout
-                                                , gradual
-                                                , stringTheory)
+                                                , Config (solver, smtTimeout, gradual, stringTheory, save))
 import qualified Language.Fixpoint.Misc          as Misc
 import           Language.Fixpoint.Types.Errors
 import           Language.Fixpoint.Utils.Files
@@ -240,12 +236,18 @@ negativeP
 makeContext :: Config -> FilePath -> IO Context
 --------------------------------------------------------------------------
 makeContext cfg f
-  = do createDirectoryIfMissing True $ takeDirectory smtFile
-       hLog <- openFile smtFile WriteMode
-       hSetBuffering hLog $ BlockBuffering $ Just $ 1024 * 1024 * 64
-       me   <- makeContext' cfg $ Just hLog
+  = do mb_hLog <- if not (save cfg) then pure Nothing else do
+           createDirectoryIfMissing True $ takeDirectory smtFile
+           hLog <- openFile smtFile WriteMode
+           hSetBuffering hLog $ BlockBuffering $ Just $ 1024 * 1024 * 64
+           return $ Just hLog
+       me   <- makeContext' cfg mb_hLog
        pre  <- smtPreamble cfg (solver cfg) me
-       mapM_ (\l -> SMTLIB.Backends.command_ (ctxSolver me) l >> BS.hPutBuilder hLog l >> LBS.hPutStr hLog "\n") pre
+       forM_ pre $ \line -> do
+           SMTLIB.Backends.command_ (ctxSolver me) line
+           forM_ mb_hLog $ \hLog -> do
+               BS.hPutBuilder hLog line
+               LBS.hPutStr hLog "\n"
        return me
     where
        smtFile = extFileName Smt2 f