diff --git a/src/main/scala/leon/utils/ASCIITable.scala b/src/main/scala/leon/utils/ASCIITable.scala index 4d32206ad70af1df6916e9fdd11e0f5f3095d9ce..60a94703361dfb6b19925a39cc1f0286c70f4ab4 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 27e25e6613362c4d3106278b36c5bb7c416fab82..b6522f5a687d4ad17cac5d37ad58e16608993e5c 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) ))