diff --git a/src/test/scala/leon/test/LeonTestSuite.scala b/src/test/scala/leon/test/LeonTestSuite.scala
index a5c94e9ab4bea038e51b8fe3e3d131263325ed2d..8fb87c5723c5d52a000a1eab4a3a49a6802bcf6d 100644
--- a/src/test/scala/leon/test/LeonTestSuite.scala
+++ b/src/test/scala/leon/test/LeonTestSuite.scala
@@ -116,6 +116,7 @@ trait LeonTestSuite extends FunSuite with Timeouts with BeforeAndAfterEach {
           case fe: LeonFatalError =>
           testContext.reporter match {
             case sr: TestSilentReporter =>
+              sr.lastErrors ++= fe.msg
               throw new TestFailedException(sr.lastErrors.mkString("\n"), fe, 5)
           }
         }
diff --git a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
index f2bfc13743573cf79a8b85e841a40b9d2f5c4783..55902fa9e6e0a863c6fa6ef49443e2b56cd14d84 100644
--- a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
@@ -45,10 +45,12 @@ class PureScalaVerificationRegression extends VerificationRegression {
   
   forEachFileIn("valid") { output =>
     val Output(report, reporter) = output
-    assert(report.totalConditions === report.totalValid,
-           "All verification conditions ("+report.totalConditions+") should be valid.")
-    assert(reporter.errorCount === 0)
-    assert(reporter.warningCount === 0)
+    for (vc <- report.conditions) {
+      if (vc.value != Some(true)) {
+        fail("The following verification condition was invalid: " + vc.toString + " @" + vc.getPos)
+      }
+    }
+    reporter.terminateIfError()
   }
 
   forEachFileIn("invalid") { output =>
@@ -57,8 +59,6 @@ class PureScalaVerificationRegression extends VerificationRegression {
            "There should be at least one invalid verification condition.")
     assert(report.totalUnknown === 0,
            "There should not be unknown verification conditions.")
-    assert(reporter.errorCount >= report.totalInvalid)
-    assert(reporter.warningCount === 0)
   }
 
 }
diff --git a/src/test/scala/leon/test/verification/VerificationRegression.scala b/src/test/scala/leon/test/verification/VerificationRegression.scala
index fdef260910bf65dea6cd1675c35f5b66923d8a6d..286fa774d6a178ed414925c4ebe23a1723538d13 100644
--- a/src/test/scala/leon/test/verification/VerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/VerificationRegression.scala
@@ -31,21 +31,23 @@ trait VerificationRegression extends LeonTestSuite {
   val pipeFront: Pipeline[Program, Program]
   val pipeBack : Pipeline[Program, VerificationReport]
 
-  private def mkTest(files: List[String], leonOptions : Seq[String])(block: Output=>Unit) = {
+  private def mkTest(files: List[String])(block: Output=>Unit) = {
     val extraction = 
       ExtractionPhase andThen
       PreprocessingPhase andThen
       pipeFront
 
-    val ast = extraction.run(createLeonContext((files ++ leonOptions):_*))(files)
+    val ast = extraction.run(createLeonContext(files:_*))(files)
     val programs = {
       val (user, lib) = ast.units partition { _.isMainUnit }
       user map { u => Program(u.id.freshen, u :: lib) }
     }
-    for (p <- programs; displayName = p.id.name) test(f"${nextInt()}%3d: $displayName ${leonOptions.mkString(" ")}") {
-      val ctx = createLeonContext(leonOptions:_*)
-      val report = pipeBack.run(ctx)(p)
-      block(Output(report, ctx.reporter))
+    for (p <- programs; options <- optionVariants) {
+      test(f"${nextInt()}%3d: ${p.id.name} ${options.mkString(" ")}") {
+        val ctx = createLeonContext(options: _*)
+        val report = pipeBack.run(ctx)(p)
+        block(Output(report, ctx.reporter))
+      }
     }
   }
 
@@ -59,9 +61,7 @@ trait VerificationRegression extends LeonTestSuite {
 
     val files = fs map { _.getPath }
 
-    for (options <- optionVariants) { 
-      mkTest(files, options)(block)
-    }
+    mkTest(files)(block)
   }