From b57fc9714f80c102a8edc69dadd85cbdf2465c52 Mon Sep 17 00:00:00 2001 From: Sam Balco Date: Mon, 12 Aug 2024 10:47:12 +0100 Subject: [PATCH 1/2] Set user supplied value when checking the SMT prelude --- booster/library/Booster/SMT/Interface.hs | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/booster/library/Booster/SMT/Interface.hs b/booster/library/Booster/SMT/Interface.hs index be2612635c..5b5e10d3bd 100644 --- a/booster/library/Booster/SMT/Interface.hs +++ b/booster/library/Booster/SMT/Interface.hs @@ -157,14 +157,12 @@ translatePrelude def = checkPrelude :: Log.LoggerMIO io => SMT io () checkPrelude = do - -- set large default timeout value for checking the prelude - setTimeout defaultSMTOptions.timeout + -- set the user defined timeout for queries + setTimeout ctxt.options.timeout Log.logMessage ("Checking definition prelude" :: Text) ctxt <- SMT get -- send the commands from the definition's SMT prelude check <- mapM_ runCmd ctxt.prelude >> runCmd CheckSat - -- set user defined timeout value for the general queries - setTimeout ctxt.options.timeout case check of Sat -> pure () other -> do From 6e9911efaa22ab59b7d378c9748e14f7c801eac7 Mon Sep 17 00:00:00 2001 From: Sam Balco Date: Mon, 12 Aug 2024 11:02:07 +0100 Subject: [PATCH 2/2] fix --- booster/library/Booster/SMT/Interface.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/booster/library/Booster/SMT/Interface.hs b/booster/library/Booster/SMT/Interface.hs index 5b5e10d3bd..40452e08ff 100644 --- a/booster/library/Booster/SMT/Interface.hs +++ b/booster/library/Booster/SMT/Interface.hs @@ -157,10 +157,10 @@ translatePrelude def = checkPrelude :: Log.LoggerMIO io => SMT io () checkPrelude = do + ctxt <- SMT get -- set the user defined timeout for queries setTimeout ctxt.options.timeout Log.logMessage ("Checking definition prelude" :: Text) - ctxt <- SMT get -- send the commands from the definition's SMT prelude check <- mapM_ runCmd ctxt.prelude >> runCmd CheckSat case check of