From 1f28ecbf26a8a3aa631f56138b87254772a56c63 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 10 Jun 2015 17:35:25 +0200
Subject: [PATCH] Prioritize displaying invalid instead of unknown
---
.../leon/test/verification/VerificationRegression.scala | 8 +++++---
1 file changed, 5 insertions(+), 3 deletions(-)
diff --git a/src/test/scala/leon/test/verification/VerificationRegression.scala b/src/test/scala/leon/test/verification/VerificationRegression.scala
index 9a84322f7..5b559d5b5 100644
--- a/src/test/scala/leon/test/verification/VerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/VerificationRegression.scala
@@ -81,9 +81,11 @@ trait VerificationRegression extends LeonTestSuite {
override def run(testName: Option[String], args: Args): Status = {
forEachFileIn("valid") { output =>
val Output(report, reporter) = output
- for ((vc, vr) <- report.vrs if (!vr.isValid)) {
- val status = if (vr.isInvalid) "invalid" else "inconclusive"
- fail(s"The following verification condition was $status: $vc @${vc.getPos}")
+ for ((vc, vr) <- report.vrs if (vr.isInvalid)) {
+ fail(s"The following verification condition was invalid: $vc @${vc.getPos}")
+ }
+ for ((vc, vr) <- report.vrs if (vr.isInconclusive)) {
+ fail(s"The following verification condition was inconclusive: $vc @${vc.getPos}")
}
reporter.terminateIfError()
}
--
GitLab