From bd9da422b498af3bb7e542c44d5286057be1236b Mon Sep 17 00:00:00 2001 From: Samuel Chassot <14821693+samuelchassot@users.noreply.github.com> Date: Fri, 11 Oct 2024 18:51:18 +0200 Subject: [PATCH] new reporter message for missing measure (#1589) --- .../stainless/verification/VerificationChecker.scala | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) 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")