Merge branch 'main' into sam/set

epfl-lara · Oct 14, 2024 · 4d18542 · 4d18542
2 parents d0dc10d + bd9da42
commit 4d18542
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")