From 2fd6599e0b791c76aa1da83901442f8ca23b7ce9 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 21 Jul 2017 12:58:05 -0700 Subject: [PATCH] Adopt LeventErkok's suggestion from #435 Closes #435. --- src/Cryptol/Symbolic.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Cryptol/Symbolic.hs b/src/Cryptol/Symbolic.hs index c0d292b1..6996b5be 100644 --- a/src/Cryptol/Symbolic.hs +++ b/src/Cryptol/Symbolic.hs @@ -213,7 +213,7 @@ satProve ProverCommand {..} = [] -> return $ ThmResult (unFinType <$> ts) -- otherwise something is wrong _ -> return $ ProverError (rshow results) - where rshow | isSat = show . SBV.AllSatResult . (boom,boom,) + where rshow | isSat = show . SBV.AllSatResult . (False,boom,) | otherwise = show . SBV.ThmResult . head boom = panic "Cryptol.Symbolic.sat" [ "attempted to evaluate bogus boolean for pretty-printing" ]