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

This should correct issue #572

Browse Source 
We should leave the ticket open until we figure out if this is actually
a bug in SBV, as the API it exposes is quite odd.
This commit is contained in:
Iavor Diatchki 2019-02-14 14:11:40 -08:00
parent fd67463b2b
commit ff81ea4095
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