new reporter message for missing measure (#1589)

epfl-lara · Oct 11, 2024 · bd9da42 · bd9da42
1 parent fbdd54b
commit bd9da42
Showing 1 changed file with 7 additions and 2 deletions.
diff --git 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")