From bde52498f19e9918c96eb34598645ac7c8cae352 Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Wed, 9 Jul 2014 16:09:55 +0200
Subject: [PATCH] Fix error and show position in reports
---
src/main/scala/leon/utils/ASCIITable.scala | 4 ++--
src/main/scala/leon/verification/VerificationReport.scala | 3 ++-
2 files changed, 4 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/utils/ASCIITable.scala b/src/main/scala/leon/utils/ASCIITable.scala
index 4d32206ad..60a947033 100644
--- a/src/main/scala/leon/utils/ASCIITable.scala
+++ b/src/main/scala/leon/utils/ASCIITable.scala
@@ -11,10 +11,10 @@ object ASCIITables {
var constraints = Map[(Int, Int), Int]()
var cellsPerRow = 0
- for((r, i) <- rows.zipWithIndex) r match {
+ for((r, j) <- rows.zipWithIndex) r match {
case r @ Row(cells) =>
if (cellsPerRow > 0) {
- assert(r.cellsSize == cellsPerRow, "Row $i has incompatible number of virtual cells (${r.cellsSize} v.s. $cellsPerRow")
+ assert(r.cellsSize == cellsPerRow, s"Row $j has incompatible number of virtual cells (${r.cellsSize} v.s. $cellsPerRow")
} else {
cellsPerRow = r.cellsSize
constraints += (0, cellsPerRow-1) -> 80
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index 27e25e661..b6522f5a6 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -29,6 +29,7 @@ class VerificationReport(val fvcs: Map[FunDef, List[VerificationCondition]]) {
Row(Seq(
Cell(vc.funDef.id.toString),
Cell(vc.kind.name),
+ Cell(vc.getPos),
Cell(vc.status),
Cell(vc.tacticStr),
Cell(vc.solverStr),
@@ -39,7 +40,7 @@ class VerificationReport(val fvcs: Map[FunDef, List[VerificationCondition]]) {
t += Separator
t += Row(Seq(
- Cell(f"total: $totalConditions%-4d valid: $totalValid%-4d invalid: $totalInvalid%-4d unknown $totalUnknown%-4d", 5),
+ Cell(f"total: $totalConditions%-4d valid: $totalValid%-4d invalid: $totalInvalid%-4d unknown $totalUnknown%-4d", 6),
Cell(f"$totalTime%7.3f", align = Right)
))
--
GitLab