Skip to content

Commit

Permalink
SMTLib2: only send exit command if solver process is active
Browse files Browse the repository at this point in the history
this avoids issues where the solver process was
killed via `What4.Protocol.Online.killSolver`
(e.g. due to a forced timeout)
  • Loading branch information
danmatichuk committed Feb 26, 2025
1 parent ebf9ac0 commit 41c395d
Showing 1 changed file with 5 additions and 2 deletions.
7 changes: 5 additions & 2 deletions what4/src/What4/Protocol/SMTLib2.hs
Original file line number Diff line number Diff line change
Expand Up @@ -1647,8 +1647,11 @@ startSolver solver ack setup tmout feats strictOpt auxOutput sym = do
shutdownSolver
:: SMTLib2GenericSolver a => a -> SolverProcess t (Writer a) -> IO (Exit.ExitCode, Lazy.Text)
shutdownSolver _solver p = do
-- Tell solver to exit
writeExit (solverConn p)
-- Tell solver to exit, if the process is still running
status <- Streams.getProcessExitCode (solverHandle p)
case status of
Just _ -> return ()
Nothing -> writeExit (solverConn p)
txt <- readAllLines (solverStderr p)
stopHandleReader (solverStderr p)
ec <- solverCleanupCallback p
Expand Down

0 comments on commit 41c395d

Please sign in to comment.