Skip to content

Commit 8fc07af

Browse files
Set user supplied value when checking the SMT prelude in booster (#4030)
Followup to #4017 addressing a potential issue I noticed whilst refactoring the SMT interface in booster. Namely, we set the hard-coded timeout value when checking the consistency of the prelude, before setting the user supplied value for general queries. This PR instead just sets the user supplied timeout value before checking the prelude.
1 parent 9f70027 commit 8fc07af

File tree

1 file changed

+3
-5
lines changed

1 file changed

+3
-5
lines changed

booster/library/Booster/SMT/Interface.hs

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -157,14 +157,12 @@ translatePrelude def =
157157

158158
checkPrelude :: Log.LoggerMIO io => SMT io ()
159159
checkPrelude = do
160-
-- set large default timeout value for checking the prelude
161-
setTimeout defaultSMTOptions.timeout
162-
Log.logMessage ("Checking definition prelude" :: Text)
163160
ctxt <- SMT get
161+
-- set the user defined timeout for queries
162+
setTimeout ctxt.options.timeout
163+
Log.logMessage ("Checking definition prelude" :: Text)
164164
-- send the commands from the definition's SMT prelude
165165
check <- mapM_ runCmd ctxt.prelude >> runCmd CheckSat
166-
-- set user defined timeout value for the general queries
167-
setTimeout ctxt.options.timeout
168166
case check of
169167
Sat -> pure ()
170168
other -> do

0 commit comments

Comments
 (0)