Skip to content
Snippets Groups Projects
Unverified Commit bd9da422 authored by Samuel Chassot's avatar Samuel Chassot Committed by GitHub
Browse files

new reporter message for missing measure (#1589)

parent fbdd54bb
No related branches found
No related tags found
No related merge requests found
......@@ -379,8 +379,13 @@ trait VerificationChecker { self =>
reporter.warning(vc.getPos, " => INVALID")
reason match {
case VCStatus.CounterExample(cex) =>
reporter.warning("Found counter-example:")
reporter.warning(" " + cex.asString.replaceAll("\n", "\n "))
vc.kind match {
case VCKind.MeasureMissing =>
reporter.warning("Measure is missing, cannot check termination")
case _ =>
reporter.warning("Found counter-example:")
reporter.warning(" " + cex.asString.replaceAll("\n", "\n "))
}
case VCStatus.Unsatisfiable =>
reporter.warning("Property wasn't satisfiable")
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment