GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2025-01-07 08:19:12 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' into rec-upd

Browse Source
This commit is contained in:
Iavor Diatchki 2019-02-17 18:51:20 -08:00
commit 1b780c21e1
1 changed files with 4 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
src/Cryptol/Symbolic.hs
View File

@ -20,7 +20,7 @@ import Control.Monad.IO.Class
import Control.Monad (replicateM, when, zipWithM, foldM)
import Control.Monad.Writer (WriterT, runWriterT, tell, lift)
import Data.List (intercalate, genericLength)
import Data.IORef(IORef)
import Data.IORef(IORef,writeIORef)
import qualified Control.Exception as X
import qualified Data.SBV.Dynamic as SBV
@ -176,6 +176,9 @@ satProve ProverCommand {..} =
lPutStrLn $ "Trying proof with " ++
intercalate ", " (map (show . SBV.name . SBV.solver) provers)
(firstProver, timeElapsed, res) <- M.io (fn provers' e)
-- NOTE: It would appear that the ref does not contain the elaspsed
-- time but rahter some sort of small value, so we write it here.
liftIO $ writeIORef pcProverStats timeElapsed
when pcVerbose $
lPutStrLn $ "Got result from " ++ show firstProver ++
", time: " ++ showTDiff timeElapsed