Skip to content
Snippets Groups Projects
Commit dcc76606 authored by Manos Koukoutos's avatar Manos Koukoutos
Browse files

make test messages a little clearer

parent 46b4a943
No related branches found
No related tags found
No related merge requests found
...@@ -4,6 +4,7 @@ package leon.test.verification ...@@ -4,6 +4,7 @@ package leon.test.verification
import leon._ import leon._
import leon.test._ import leon.test._
import leon.verification.VCStatus._
import leon.verification.VerificationReport import leon.verification.VerificationReport
import leon.purescala.Definitions.Program import leon.purescala.Definitions.Program
...@@ -79,10 +80,9 @@ trait VerificationRegression extends LeonTestSuite { ...@@ -79,10 +80,9 @@ trait VerificationRegression extends LeonTestSuite {
override def run(testName: Option[String], args: Args): Status = { override def run(testName: Option[String], args: Args): Status = {
forEachFileIn("valid") { output => forEachFileIn("valid") { output =>
val Output(report, reporter) = output val Output(report, reporter) = output
for ((vc, vr) <- report.vrs) { for ((vc, vr) <- report.vrs if (!vr.isValid)) {
if (!vr.isValid) { val status = if (vr.isInvalid) "invalid" else "inconclusive"
fail("The following verification condition was invalid: " + vc.toString + " @" + vc.getPos) fail(s"The following verification condition was $status: $vc @${vc.getPos}")
}
} }
reporter.terminateIfError() reporter.terminateIfError()
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment