diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala index 3741364715598495cb180731a42fda9f123da3f2..72f3b09e886f51c8c1868d87606f451167115605 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 faf7571e9582f652e3ba494b11eb34c5923d4dac..02f5294c26e7f3b4f29e307db07186927bfff82c 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 12a8152b1701fe993f36c33392eebda724ec4aad..104e2ecabdfa0ac8bef8cc179ff68acc1a7c6ccc 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 88b0319086023675c766cf8f6c74ccd420d2a182..340dfbc46077306b64752e73cebeb725ef40a781 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