From 840e99f56383d45ef17df5489167931804022b54 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Fri, 26 Sep 2014 11:56:32 -0700 Subject: [PATCH] Pass 'verbose' flag through to SBV for :prove and :sat This addresses issue #17. --- src/Cryptol/Symbolic.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Cryptol/Symbolic.hs b/src/Cryptol/Symbolic.hs index 55b6f7d9..9d5c0fc2 100644 --- a/src/Cryptol/Symbolic.hs +++ b/src/Cryptol/Symbolic.hs @@ -86,12 +86,13 @@ satProve isSat (proverName, useSolverIte, verbose) edecls mfile (expr, schema) = case proverName of "any" -> SBV.sbvAvailableSolvers _ -> return [(lookupProver proverName) { smtFile = mfile }] + let provers' = [ p { SBV.timing = verbose, SBV.verbose = verbose } | p <- provers ] let tyFn = if isSat then existsFinType else forallFinType let runProver fn tag e = do when verbose $ liftIO $ putStrLn $ "Trying proof with " ++ intercalate ", " (map show provers) - (firstProver, res) <- fn provers e + (firstProver, res) <- fn provers' e when verbose $ liftIO $ putStrLn $ "Got result from " ++ show firstProver return (tag res)