GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-17 13:01:31 +03:00
Code Issues Projects Releases Wiki Activity

Adopt LeventErkok's suggestion from #435

Browse Source 
Closes #435.
This commit is contained in:
Aaron Tomb 2017-07-21 12:58:05 -07:00
parent 2885d469da
commit 2fd6599e0b
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Cryptol/Symbolic.hs
View File

@ -213,7 +213,7 @@ satProve ProverCommand {..} =
[] -> return $ ThmResult (unFinType <$> ts) [] -> return $ ThmResult (unFinType <$> ts)
-- otherwise something is wrong -- otherwise something is wrong
_ -> return $ ProverError (rshow results) _ -> 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 | otherwise = show . SBV.ThmResult . head
boom = panic "Cryptol.Symbolic.sat" boom = panic "Cryptol.Symbolic.sat"
[ "attempted to evaluate bogus boolean for pretty-printing" ] [ "attempted to evaluate bogus boolean for pretty-printing" ]