From ee70f7adff3323df5c385a40bb7896407fb2b8bf Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 17 Dec 2015 10:48:29 +0100
Subject: [PATCH] Adjust benchmarks a bit
---
src/main/scala/leon/repair/Repairman.scala | 2 +-
testcases/repair/List/List8.scala | 2 +-
testcases/repair/List/List9.scala | 2 +-
testcases/repair/MergeSort/MergeSort1.scala | 2 +-
4 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 374136471..72f3b09e8 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -147,7 +147,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
val fw = new java.io.FileWriter("repair-report.txt", true)
try {
- fw.write(f"$date: $benchName%-50s & $pSize%4d & $fSize%4d & $locSize%4d & $solSize%4d & ${timeTests/1000.0}%.2f & & ${timeSynth/1000.0}%.2f & $proof%7s \\\\\n")
+ fw.write(f"$date: $benchName%-30s & $pSize%4d & $fSize%4d & $locSize%4d & $solSize%4d & ${timeTests/1000.0}%.2f & & ${timeSynth/1000.0}%.2f & $proof%7s \\\\\n")
} finally {
fw.close
}
diff --git a/testcases/repair/List/List8.scala b/testcases/repair/List/List8.scala
index faf7571e9..02f5294c2 100644
--- a/testcases/repair/List/List8.scala
+++ b/testcases/repair/List/List8.scala
@@ -191,7 +191,7 @@ sealed abstract class List[T] {
}
}} ensuring { res =>
if (this.content contains e) {
- res.isDefined && this.size > res.get && this.apply(res.get) == e
+ res.isDefined && this.size > res.get && this.apply(res.get) == e && res.get >= 0
} else {
res.isEmpty
}
diff --git a/testcases/repair/List/List9.scala b/testcases/repair/List/List9.scala
index 12a8152b1..104e2ecab 100644
--- a/testcases/repair/List/List9.scala
+++ b/testcases/repair/List/List9.scala
@@ -191,7 +191,7 @@ sealed abstract class List[T] {
}
}} ensuring { res =>
if (this.content contains e) {
- res.isDefined && this.size > res.get && this.apply(res.get) == e
+ res.isDefined && this.size > res.get && this.apply(res.get) == e && res.get >= 0
} else {
res.isEmpty
}
diff --git a/testcases/repair/MergeSort/MergeSort1.scala b/testcases/repair/MergeSort/MergeSort1.scala
index 88b031908..340dfbc46 100644
--- a/testcases/repair/MergeSort/MergeSort1.scala
+++ b/testcases/repair/MergeSort/MergeSort1.scala
@@ -5,7 +5,7 @@ object MergeSort {
def split(l : List[BigInt]) : (List[BigInt],List[BigInt]) = { l match {
case Cons(a, Cons(b, t)) =>
val (rec1, rec2) = split(t)
- (rec1, rec2) // FIXME: Forgot a,b
+ (rec1, Cons(b, rec2)) // FIXME: Forgot a
case other => (other, Nil[BigInt]())
}} ensuring { res =>
val (l1, l2) = res
--
GitLab