Fix runtests/ add List benchmarks

runTests.sh

@@ -13,24 +13,35 @@ echo "################################" >> $fullLog
 echo "#           Category,                 File,             function,   S, f.S,   Tms,   Fms,   Rms, verif?" >> $fullLog
 
 #All benchmarks:
-./leon --repair --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar1.scala
-./leon --repair --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar2.scala
-./leon --repair --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar3.scala
-./leon --repair --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar4.scala
-
-./leon --repair --solvers=fairz3:enum --functions=merge   testcases/repair/HeapSort/HeapSort3.scala
-./leon --repair --solvers=fairz3:enum --functions=merge   testcases/repair/HeapSort/HeapSort4.scala
-./leon --repair --solvers=fairz3:enum --functions=merge   testcases/repair/HeapSort/HeapSort8.scala
-./leon --repair --solvers=fairz3:enum --functions=merge   testcases/repair/HeapSort/HeapSort6.scala
-./leon --repair --solvers=fairz3:enum --functions=merge   testcases/repair/HeapSort/HeapSort7.scala
-./leon --repair --solvers=fairz3:enum --functions=insert  testcases/repair/HeapSort/HeapSort5.scala
-./leon --repair --solvers=fairz3:enum --functions=makeN   testcases/repair/HeapSort/HeapSort9.scala
-
-./leon --repair --solvers=fairz3:enum --functions=nnf     testcases/repair/PropLogic/PropLogic1.scala 
-./leon --repair --solvers=fairz3:enum --functions=nnf     testcases/repair/PropLogic/PropLogic2.scala 
-./leon --repair --solvers=fairz3:enum --functions=nnf     testcases/repair/PropLogic/PropLogic3.scala 
-./leon --repair --solvers=fairz3:enum --functions=nnf     testcases/repair/PropLogic/PropLogic4.scala 
-./leon --repair --solvers=fairz3:enum --functions=nnf     testcases/repair/PropLogic/PropLogic5.scala 
+./leon --repair --solvers=fairz3:enum --functions=desugar  testcases/repair/Desugar/Desugar1.scala
+./leon --repair --solvers=fairz3:enum --functions=desugar  testcases/repair/Desugar/Desugar2.scala
+./leon --repair --solvers=fairz3:enum --functions=desugar  testcases/repair/Desugar/Desugar3.scala
+./leon --repair --solvers=fairz3:enum --functions=desugar  testcases/repair/Desugar/Desugar4.scala
+
+./leon --repair --solvers=fairz3:enum --functions=merge    testcases/repair/HeapSort/HeapSort3.scala
+./leon --repair --solvers=fairz3:enum --functions=merge    testcases/repair/HeapSort/HeapSort4.scala
+./leon --repair --solvers=fairz3:enum --functions=merge    testcases/repair/HeapSort/HeapSort5.scala
+./leon --repair --solvers=fairz3:enum --functions=merge    testcases/repair/HeapSort/HeapSort6.scala
+./leon --repair --solvers=fairz3:enum --functions=merge    testcases/repair/HeapSort/HeapSort7.scala
+./leon --repair --solvers=fairz3:enum --functions=insert   testcases/repair/HeapSort/HeapSort8.scala
+./leon --repair --solvers=fairz3:enum --functions=makeN    testcases/repair/HeapSort/HeapSort9.scala
+
+./leon --repair --solvers=fairz3:enum --functions=nnf      testcases/repair/PropLogic/PropLogic1.scala 
+./leon --repair --solvers=fairz3:enum --functions=nnf      testcases/repair/PropLogic/PropLogic2.scala 
+./leon --repair --solvers=fairz3:enum --functions=nnf      testcases/repair/PropLogic/PropLogic3.scala 
+./leon --repair --solvers=fairz3:enum --functions=nnf      testcases/repair/PropLogic/PropLogic4.scala 
+./leon --repair --solvers=fairz3:enum --functions=nnf      testcases/repair/PropLogic/PropLogic5.scala 
+
+./leon --repair --solvers=fairz3:enum --functions=_pad     testcases/repair/List/List1.scala
+./leon --repair --solvers=fairz3:enum --functions=_ap      testcases/repair/List/List3.scala
+./leon --repair                       --functions=_drop    testcases/repair/List/List4.scala
+./leon --repair                       --functions=_replace testcases/repair/List/List5.scala
+./leon --repair --solvers=fairz3:enum --functions=_count   testcases/repair/List/List6.scala
+./leon --repair --solvers=fairz3:enum --functions=_find    testcases/repair/List/List7.scala
+./leon --repair --solvers=fairz3:enum --functions=_find    testcases/repair/List/List8.scala
+./leon --repair                       --functions=_find    testcases/repair/List/List9.scala
+./leon --repair --solvers=fairz3:enum --functions=_size    testcases/repair/List/List10.scala
+./leon --repair --solvers=fairz3:enum --functions=sum      testcases/repair/List/List11.scala
 
 # Average results
 cat $log >> $fullLog

testcases/repair/List/List4.scala

@@ -82,9 +82,9 @@ sealed abstract class List0[T] {
     case (Cons0(h, t), i) =>
       t.drop(i-1) //FIXME missing if-split
   }} ensuring { res => ((this, i), res) passes { 
-    case (l@Cons0(_, Nil0()), 42) => l
-    case (Cons0(a, t), 0) => t
-    case (Cons0(a, Cons0(b, Nil0())), 1) => Cons0(a, Nil0())
+    case (Cons0(_, Nil0()), 42) => Nil0()
+    case (l@Cons0(_, _), 0) => l
+    case (Cons0(a, Cons0(b, Nil0())), 1) => Cons0(b, Nil0())
   }}
 
   def slice(from: Int, to: Int): List0[T] = {

testcases/repair/List/List5.scala

@@ -97,7 +97,9 @@ sealed abstract class List0[T] {
     case Cons0(h, t) =>
       val r = t.replace(from, to)
       Cons0(to, r) // FIXME
-  }} ensuring { res => (res.content == this.content -- Set(from) ++ Set(to)) && res.size == this.size 
+  }} ensuring { res => 
+    (if(this.contains(from)) res.contains(to) else true) && 
+    !res.contains(from) && res.size == this.size 
   }
 
   private def chunk0(s: Int, l: List0[T], acc: List0[T], res: List0[List0[T]], s0: Int): List0[List0[T]] = l match {