Skip to content

Commit 82e07ab

Browse files
Merge pull request #2545 from ucsd-progsys/fd/constraints-on-failure
Print the amount of checked constraints when verification fails
2 parents a45a500 + 73685d6 commit 82e07ab

File tree

1 file changed

+2
-2
lines changed
  • liquidhaskell-boot/src/Language/Haskell/Liquid/UX

1 file changed

+2
-2
lines changed

liquidhaskell-boot/src/Language/Haskell/Liquid/UX/CmdLine.hs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -842,9 +842,9 @@ resDocs k (F.Crash xs s) =
842842
orHeader = text "LIQUID: ERROR:" <+> text s
843843
, orMessages = map (cErrToSpanned k . errToFCrash) xs
844844
}
845-
resDocs k (F.Unsafe _ xs) =
845+
resDocs k (F.Unsafe stats xs) =
846846
OutputResult {
847-
orHeader = text "LIQUID: UNSAFE"
847+
orHeader = text $ "LIQUID: UNSAFE (" <> show (Solver.numChck stats) <> " constraints checked)"
848848
, orMessages = map (cErrToSpanned k) (nub xs)
849849
}
850850

0 commit comments

Comments
 (0)