diff --git a/core/src/main/scala/stainless/verification/VerificationChecker.scala b/core/src/main/scala/stainless/verification/VerificationChecker.scala index 5ca539e9d..5cbded36a 100644 --- a/core/src/main/scala/stainless/verification/VerificationChecker.scala +++ b/core/src/main/scala/stainless/verification/VerificationChecker.scala @@ -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")