diff --git a/runTests.sh b/runTests.sh
index 938f44ba34fc9c5fd93edcc1d4c2ebcb603d9537..b124e9bd02c8d1b6c6cc0cb885843226872099d6 100755
--- a/runTests.sh
+++ b/runTests.sh
@@ -19,16 +19,18 @@ echo "#           Category,                 File,             function, p.S, fuS
 ./leon --repair --timeout=30 --solvers=fairz3:enum --functions=desugar  testcases/repair/Compiler/Compiler2.scala   | tee -a $fullLog
 ./leon --repair --timeout=30 --solvers=fairz3:enum --functions=desugar  testcases/repair/Compiler/Compiler3.scala   | tee -a $fullLog
 ./leon --repair --timeout=30 --solvers=fairz3:enum --functions=desugar  testcases/repair/Compiler/Compiler4.scala   | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=simplify testcases/repair/Compiler/Compiler5.scala   | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=desugar  testcases/repair/Compiler/Compiler5.scala   | tee -a $fullLog
 ./leon --repair --timeout=30 --solvers=fairz3:enum --functions=simplify testcases/repair/Compiler/Compiler6.scala   | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=simplify testcases/repair/Compiler/Compiler7.scala   | tee -a $fullLog
 
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge    testcases/repair/HeapSort/HeapSort3.scala   | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge    testcases/repair/HeapSort/HeapSort4.scala   | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge    testcases/repair/HeapSort/HeapSort5.scala   | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge    testcases/repair/HeapSort/HeapSort6.scala   | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge    testcases/repair/HeapSort/HeapSort7.scala   | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=insert   testcases/repair/HeapSort/HeapSort8.scala   | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=makeN    testcases/repair/HeapSort/HeapSort9.scala   | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge    testcases/repair/Heap/Heap3.scala        | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge    testcases/repair/Heap/Heap4.scala        | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge    testcases/repair/Heap/Heap5.scala        | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge    testcases/repair/Heap/Heap6.scala        | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge    testcases/repair/Heap/Heap7.scala        | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=insert   testcases/repair/Heap/Heap8.scala        | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=makeN    testcases/repair/Heap/Heap9.scala        | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge    testcases/repair/Heap/Heap10.scala       | tee -a $fullLog
 
 ./leon --repair --timeout=30 --solvers=fairz3:enum --functions=nnf      testcases/repair/PropLogic/PropLogic1.scala | tee -a $fullLog
 ./leon --repair --timeout=30 --solvers=fairz3:enum --functions=nnf      testcases/repair/PropLogic/PropLogic2.scala | tee -a $fullLog
@@ -47,6 +49,17 @@ echo "#           Category,                 File,             function, p.S, fuS
 ./leon --repair --timeout=30                       --functions=_find    testcases/repair/List/List9.scala           | tee -a $fullLog
 ./leon --repair --timeout=30 --solvers=fairz3:enum --functions=_size    testcases/repair/List/List10.scala          | tee -a $fullLog
 ./leon --repair --timeout=30 --solvers=fairz3:enum --functions=sum      testcases/repair/List/List11.scala          | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=_-       testcases/repair/List/List12.scala          | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=_drop    testcases/repair/List/List13.scala          | tee -a $fullLog
+
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=power    testcases/repair/Numerical/Numerical1.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=moddiv   testcases/repair/Numerical/Numerical3.scala | tee -a $fullLog
+
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=split    testcases/repair/MergeSort/MergeSort1.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge    testcases/repair/MergeSort/MergeSort2.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge    testcases/repair/MergeSort/MergeSort3.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge    testcases/repair/MergeSort/MergeSort4.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge    testcases/repair/MergeSort/MergeSort5.scala | tee -a $fullLog
 
 # Average results
 cat $log >> $summaryLog
diff --git a/src/main/scala/leon/repair/RepairResult.scala b/src/main/scala/leon/repair/RepairResult.scala
index 697434d6fbb78db68e534169bdff0b3f143bfb1d..463bdae3187bcc810e03eb296e210f5f65370fe5 100644
--- a/src/main/scala/leon/repair/RepairResult.scala
+++ b/src/main/scala/leon/repair/RepairResult.scala
@@ -39,7 +39,12 @@ case class RepairResult(f: File,
 
     val verified = repairTrusted.map(if (_) "\\chmark" else "").getOrElse("")
 
-    f"$benchCat%20s &  $benchName%20s & $benchFun%20s & $psize%4s & $fsize%3s & ${focusSize.getOrElse("")}%3s & ${repairSize.getOrElse("")}%3s & ${ts(initTime)} & ${ts(focusTime)} & ${ts(repairTime)} & $verified%7s \\\\ \n"
+    val repairTime2 = (focusTime, repairTime) match {
+      case (Some(t), Some(t2)) => Some(t + t2)
+      case _ => None
+    }
+
+    f"$benchCat%20s &  $benchName%20s & $benchFun%20s & $psize%4s & $fsize%3s & ${focusSize.getOrElse("")}%3s & ${repairSize.getOrElse("")}%3s & ${ts(initTime)} & ${ts(repairTime2)} & $verified%7s \\\\ \n"
   }
 }
 
diff --git a/testcases/repair/Compiler/Compiler5.scala b/testcases/repair/Compiler/Compiler5.scala
index 95003d1afe6e56bdf4ab42dbff6c24227f41abc2..3a605de3d6fee6d135da43793f440c0ac10f37f7 100644
--- a/testcases/repair/Compiler/Compiler5.scala
+++ b/testcases/repair/Compiler/Compiler5.scala
@@ -150,10 +150,10 @@ object Desugar {
     case Trees.LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
     case Trees.And  (lhs, rhs) => Ite(desugar(lhs), desugar(rhs), Literal(0)) 
     case Trees.Or   (lhs, rhs) => Ite(desugar(lhs), Literal(1), desugar(rhs))
-    case Trees.Not(e) => Ite(desugar(e), Literal(0), Literal(1))
+    case Trees.Not(e) => Ite(desugar(e), Literal(1), Literal(1)) //FIXME
     case Trees.Eq(lhs, rhs) =>
       Eq(desugar(lhs), desugar(rhs))
-    case Trees.Ite(cond, thn, els) => Ite(desugar(cond), desugar(thn), desugar(els))
+    case Trees.Ite(cond, thn, els) => Ite(desugar(cond), desugar(els), desugar(thn))//FIXME
     case Trees.IntLiteral(v)  => Literal(v)
     case Trees.BoolLiteral(b) => Literal(b2i(b))
   }} ensuring { res => 
@@ -202,7 +202,7 @@ object Simplifier {
     e match {
       case And(BoolLiteral(false), _)           => BoolLiteral(false)
       case Or(BoolLiteral(true), _)             => BoolLiteral(true)
-      case Plus(IntLiteral(a), IntLiteral(b))   => IntLiteral(a-b)
+      case Plus(IntLiteral(a), IntLiteral(b))   => IntLiteral(a+b)
       case Not(Not(Not(a)))                     => Not(a)
       case e => e
     }
diff --git a/testcases/repair/Compiler/Compiler6.scala b/testcases/repair/Compiler/Compiler6.scala
index 0e6364fc53ec7fd0e7f65c803980689ef310b600..95003d1afe6e56bdf4ab42dbff6c24227f41abc2 100644
--- a/testcases/repair/Compiler/Compiler6.scala
+++ b/testcases/repair/Compiler/Compiler6.scala
@@ -201,14 +201,12 @@ object Simplifier {
   def simplify(e: Expr): Expr = {
     e match {
       case And(BoolLiteral(false), _)           => BoolLiteral(false)
-      case Or(BoolLiteral(true), _)             => BoolLiteral(false)
-      case Plus(IntLiteral(a), IntLiteral(b))   => IntLiteral(a+b)
+      case Or(BoolLiteral(true), _)             => BoolLiteral(true)
+      case Plus(IntLiteral(a), IntLiteral(b))   => IntLiteral(a-b)
       case Not(Not(Not(a)))                     => Not(a)
       case e => e
     }
   } ensuring {
-    res => eval(res) == eval(e) && ((e, res) passes {
-      case Or(BoolLiteral(true), e) => BoolLiteral(true)
-    })
+    res => eval(res) == eval(e)
   }
 }
diff --git a/testcases/repair/Compiler/Compiler7.scala b/testcases/repair/Compiler/Compiler7.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0e6364fc53ec7fd0e7f65c803980689ef310b600
--- /dev/null
+++ b/testcases/repair/Compiler/Compiler7.scala
@@ -0,0 +1,214 @@
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon._
+
+object Trees {
+  abstract class Expr
+  case class Plus(lhs: Expr, rhs: Expr) extends Expr
+  case class Minus(lhs: Expr, rhs: Expr) extends Expr
+  case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+  case class And(lhs: Expr, rhs: Expr) extends Expr
+  case class Or(lhs: Expr, rhs: Expr) extends Expr
+  case class Not(e : Expr) extends Expr
+  case class Eq(lhs: Expr, rhs: Expr) extends Expr
+  case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+  case class IntLiteral(v: Int) extends Expr
+  case class BoolLiteral(b : Boolean) extends Expr
+}
+
+object Types {
+  abstract class Type
+  case object IntType extends Type
+  case object BoolType extends Type
+}
+
+
+object TypeChecker {
+  import Trees._
+  import Types._
+
+  def typeOf(e :Expr) : Option[Type] = e match {
+    case Plus(l,r) => (typeOf(l), typeOf(r)) match {
+      case (Some(IntType), Some(IntType)) => Some(IntType)
+      case _ => None()
+    }
+    case Minus(l,r) => (typeOf(l), typeOf(r)) match {
+      case (Some(IntType), Some(IntType)) => Some(IntType)
+      case _ => None()
+    }
+    case LessThan(l,r) => ( typeOf(l), typeOf(r)) match {
+      case (Some(IntType), Some(IntType)) => Some(BoolType)
+      case _ => None()
+    }
+    case And(l,r) => ( typeOf(l), typeOf(r)) match {
+      case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+      case _ => None()
+    }
+    case Or(l,r) => ( typeOf(l), typeOf(r)) match {
+      case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+      case _ => None()
+    }
+    case Not(e) => typeOf(e) match {
+      case Some(BoolType) => Some(BoolType)
+      case _ => None()
+    }
+    case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+      case (Some(t1), Some(t2)) if t1 == t2 => Some(BoolType)
+      case _ => None()
+    }
+    case Ite(c, th, el) => (typeOf(c), typeOf(th), typeOf(el)) match {
+      case (Some(BoolType), Some(t1), Some(t2)) if t1 == t2 => Some(t1)
+      case _ => None()
+    }
+    case IntLiteral(_) => Some(IntType)
+    case BoolLiteral(_) => Some(BoolType)
+  }
+
+  def typeChecks(e : Expr) = typeOf(e).isDefined
+}
+
+
+object Semantics {
+  import Trees._
+  import Types._
+  import TypeChecker._
+  
+  def semI(t : Expr) : Int = {
+    require( typeOf(t) == ( Some(IntType) : Option[Type] ))
+    t match {
+      case Plus(lhs , rhs) => semI(lhs) + semI(rhs)
+      case Minus(lhs , rhs) => semI(lhs) - semI(rhs)
+      case Ite(cond, thn, els) => 
+        if (semB(cond)) semI(thn) else semI(els)
+      case IntLiteral(v)   => v 
+    }
+  }
+
+  def semB(t : Expr) : Boolean = {
+    require( (Some(BoolType): Option[Type]) == typeOf(t))
+    t match {
+      case And(lhs, rhs ) => semB(lhs) && semB(rhs)
+      case Or(lhs , rhs ) => semB(lhs) || semB(rhs)
+      case Not(e) => !semB(e)
+      case LessThan(lhs, rhs) => semI(lhs) < semI(rhs)
+      case Ite(cond, thn, els) => 
+        if (semB(cond)) semB(thn) else semB(els)
+      case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+        case ( Some(IntType),  Some(IntType)  ) => semI(lhs) == semI(rhs)
+        case ( Some(BoolType), Some(BoolType) ) => semB(lhs) == semB(rhs)
+      }
+      case BoolLiteral(b) => b
+    }
+  }
+ 
+  def b2i(b : Boolean) = if (b) 1 else 0
+
+  @induct
+  def semUntyped( t : Expr) : Int = { t match {
+    case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
+    case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
+    case And  (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+    case Or(lhs, rhs ) =>
+      if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+    case Not(e) =>
+      b2i(semUntyped(e) == 0)
+    case LessThan(lhs, rhs) => 
+      b2i(semUntyped(lhs) < semUntyped(rhs))
+    case Eq(lhs, rhs) => 
+      b2i(semUntyped(lhs) == semUntyped(rhs))
+    case Ite(cond, thn, els) => 
+      if (semUntyped(cond) == 0) semUntyped(els) else semUntyped(thn)
+    case IntLiteral(v)  => v 
+    case BoolLiteral(b) => b2i(b)
+  }} ensuring { res => typeOf(t) match {
+    case Some(IntType)  => res == semI(t)
+    case Some(BoolType) => res == b2i(semB(t))
+    case None() => true
+  }}
+
+}
+
+
+object Desugar {
+  import Types._
+  import TypeChecker._
+  import Semantics.b2i
+
+  abstract class SimpleE 
+  case class Plus(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+  case class Neg(arg : SimpleE) extends SimpleE
+  case class Ite(cond : SimpleE, thn : SimpleE, els : SimpleE) extends SimpleE
+  case class Eq(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+  case class LessThan(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+  case class Literal(i : Int) extends SimpleE
+
+  @induct
+  def desugar(e : Trees.Expr) : SimpleE = { e match {
+    case Trees.Plus (lhs, rhs) => Plus(desugar(lhs), desugar(rhs))
+    case Trees.Minus(lhs, rhs) => Plus(desugar(lhs), Neg(desugar(rhs)))
+    case Trees.LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
+    case Trees.And  (lhs, rhs) => Ite(desugar(lhs), desugar(rhs), Literal(0)) 
+    case Trees.Or   (lhs, rhs) => Ite(desugar(lhs), Literal(1), desugar(rhs))
+    case Trees.Not(e) => Ite(desugar(e), Literal(0), Literal(1))
+    case Trees.Eq(lhs, rhs) =>
+      Eq(desugar(lhs), desugar(rhs))
+    case Trees.Ite(cond, thn, els) => Ite(desugar(cond), desugar(thn), desugar(els))
+    case Trees.IntLiteral(v)  => Literal(v)
+    case Trees.BoolLiteral(b) => Literal(b2i(b))
+  }} ensuring { res => 
+    sem(res) == Semantics.semUntyped(e)
+  }
+
+  def sem(e : SimpleE) : Int = e match {
+    case Plus (lhs, rhs) => sem(lhs) + sem(rhs)
+    case Ite(cond, thn, els) => if (sem(cond) != 0) sem(thn) else sem(els)
+    case Neg(arg) => -sem(arg) 
+    case Eq(lhs,rhs) => b2i(sem(lhs) == sem(rhs))
+    case LessThan(lhs, rhs) => b2i(sem(lhs) < sem(rhs))
+    case Literal(i) => i
+  }
+
+}
+
+object Evaluator {
+  import Trees._
+
+  def bToi(b: Boolean) = if (b) 1 else 0
+  def iTob(i: Int)     = i == 1
+
+  def eval(e: Expr): Int = {
+    e match {
+      case Plus(lhs, rhs)      => eval(lhs) + eval(rhs)
+      case Minus(lhs, rhs)     => eval(lhs) + eval(rhs)
+      case LessThan(lhs, rhs)  => bToi(eval(lhs) < eval(rhs))
+      case And(lhs, rhs)       => bToi(iTob(eval(lhs)) && iTob(eval(rhs)))
+      case Or(lhs, rhs)        => bToi(iTob(eval(lhs)) || iTob(eval(rhs)))
+      case Not(e)              => bToi(!iTob(eval(e)))
+      case Eq(lhs, rhs)        => bToi(eval(lhs) == eval(rhs))
+      case Ite(cond, thn, els) => if (iTob(eval(cond))) eval(thn) else eval(els)
+      case IntLiteral(v)       => v
+      case BoolLiteral(b)      => bToi(b)
+    }
+  }
+}
+
+object Simplifier {
+  import Trees._
+  import Evaluator._
+
+  @induct
+  def simplify(e: Expr): Expr = {
+    e match {
+      case And(BoolLiteral(false), _)           => BoolLiteral(false)
+      case Or(BoolLiteral(true), _)             => BoolLiteral(false)
+      case Plus(IntLiteral(a), IntLiteral(b))   => IntLiteral(a+b)
+      case Not(Not(Not(a)))                     => Not(a)
+      case e => e
+    }
+  } ensuring {
+    res => eval(res) == eval(e) && ((e, res) passes {
+      case Or(BoolLiteral(true), e) => BoolLiteral(true)
+    })
+  }
+}
diff --git a/testcases/repair/HeapSort/HeapSort.scala b/testcases/repair/Heap/Heap.scala
similarity index 100%
rename from testcases/repair/HeapSort/HeapSort.scala
rename to testcases/repair/Heap/Heap.scala
diff --git a/testcases/repair/HeapSort/HeapSort1.scala b/testcases/repair/Heap/Heap1.scala
similarity index 100%
rename from testcases/repair/HeapSort/HeapSort1.scala
rename to testcases/repair/Heap/Heap1.scala
diff --git a/testcases/repair/Heap/Heap10.scala b/testcases/repair/Heap/Heap10.scala
new file mode 100644
index 0000000000000000000000000000000000000000..27a75d344f8c4d7afb944b0cd7b07bbfd4e57587
--- /dev/null
+++ b/testcases/repair/Heap/Heap10.scala
@@ -0,0 +1,113 @@
+/* Copyright 2009-2013 EPFL, Lausanne
+ *
+ * Author: Ravi
+ * Date: 20.11.2013
+ **/
+
+import leon.collection._
+import leon._ 
+
+object HeapSort {
+ 
+  sealed abstract class Heap {
+    val rank : Int = this match {
+      case Leaf() => 0
+      case Node(_, l, r) => 
+        1 + max(l.rank, r.rank)
+    }
+    def content : Set[Int] = this match {
+      case Leaf() => Set[Int]()
+      case Node(v,l,r) => l.content ++ Set(v) ++ r.content
+    }
+  }
+  case class Leaf() extends Heap
+  case class Node(value:Int, left: Heap, right: Heap) extends Heap
+
+  def max(i1 : Int, i2 : Int) = if (i1 >= i2) i1 else i2
+
+  def hasHeapProperty(h : Heap) : Boolean = h match {
+    case Leaf() => true
+    case Node(v, l, r) => 
+      ( l match {
+        case Leaf() => true
+        case n@Node(v2,_,_) => v >= v2 && hasHeapProperty(n)
+      }) && 
+      ( r match {
+        case Leaf() => true
+        case n@Node(v2,_,_) => v >= v2 && hasHeapProperty(n)
+      })
+  }
+
+  def hasLeftistProperty(h: Heap) : Boolean = h match {
+    case Leaf() => true
+    case Node(_,l,r) => 
+      hasLeftistProperty(l) && 
+      hasLeftistProperty(r) && 
+      l.rank >= r.rank 
+  }
+
+  def heapSize(t: Heap): Int = { t match {
+    case Leaf() => 0
+    case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
+  }} ensuring(_ >= 0)
+
+  private def merge(h1: Heap, h2: Heap) : Heap = {
+    require(
+      hasLeftistProperty(h1) && hasLeftistProperty(h2) && 
+      hasHeapProperty(h1) && hasHeapProperty(h2)
+    )
+    (h1,h2) match {
+      case (Leaf(), _) => h1 // FIXME: swapped h1 and h2 between the cases
+      case (_, Leaf()) => h2 // FIXME
+      case (Node(v1, l1, r1), Node(v2, l2, r2)) =>
+        if(v1 >= v2)
+          makeN(v1, l1, merge(r1, h2))
+        else
+          makeN(v2, l2, merge(h1, r2))
+    }
+  } ensuring { res => 
+    hasLeftistProperty(res) && hasHeapProperty(res) &&
+    heapSize(h1) + heapSize(h2) == heapSize(res) &&
+    h1.content ++ h2.content == res.content 
+  }
+
+  private def makeN(value: Int, left: Heap, right: Heap) : Heap = {
+    require(
+      hasLeftistProperty(left) && hasLeftistProperty(right)
+    )
+    if(left.rank >= right.rank)
+      Node(value, left, right)
+    else
+      Node(value, right, left)
+  } ensuring { res =>
+    hasLeftistProperty(res)  }
+
+  def insert(element: Int, heap: Heap) : Heap = {
+    require(hasLeftistProperty(heap) && hasHeapProperty(heap))
+
+    merge(Node(element, Leaf(), Leaf()), heap)
+
+  } ensuring { res =>
+    hasLeftistProperty(res) && hasHeapProperty(res) &&
+    heapSize(res) == heapSize(heap) + 1 &&
+    res.content == heap.content ++ Set(element)
+  }
+
+  def findMax(h: Heap) : Option[Int] = {
+    h match {
+      case Node(m,_,_) => Some(m)
+      case Leaf() => None()
+    }
+  }
+
+  def removeMax(h: Heap) : Heap = {
+    require(hasLeftistProperty(h) && hasHeapProperty(h))
+    h match {
+      case Node(_,l,r) => merge(l, r)
+      case l => l
+    }
+  } ensuring { res =>
+    hasLeftistProperty(res) && hasHeapProperty(res)
+  }
+
+} 
diff --git a/testcases/repair/HeapSort/HeapSort2.scala b/testcases/repair/Heap/Heap2.scala
similarity index 100%
rename from testcases/repair/HeapSort/HeapSort2.scala
rename to testcases/repair/Heap/Heap2.scala
diff --git a/testcases/repair/HeapSort/HeapSort3.scala b/testcases/repair/Heap/Heap3.scala
similarity index 100%
rename from testcases/repair/HeapSort/HeapSort3.scala
rename to testcases/repair/Heap/Heap3.scala
diff --git a/testcases/repair/HeapSort/HeapSort4.scala b/testcases/repair/Heap/Heap4.scala
similarity index 100%
rename from testcases/repair/HeapSort/HeapSort4.scala
rename to testcases/repair/Heap/Heap4.scala
diff --git a/testcases/repair/HeapSort/HeapSort5.scala b/testcases/repair/Heap/Heap5.scala
similarity index 100%
rename from testcases/repair/HeapSort/HeapSort5.scala
rename to testcases/repair/Heap/Heap5.scala
diff --git a/testcases/repair/HeapSort/HeapSort6.scala b/testcases/repair/Heap/Heap6.scala
similarity index 100%
rename from testcases/repair/HeapSort/HeapSort6.scala
rename to testcases/repair/Heap/Heap6.scala
diff --git a/testcases/repair/HeapSort/HeapSort7.scala b/testcases/repair/Heap/Heap7.scala
similarity index 100%
rename from testcases/repair/HeapSort/HeapSort7.scala
rename to testcases/repair/Heap/Heap7.scala
diff --git a/testcases/repair/HeapSort/HeapSort8.scala b/testcases/repair/Heap/Heap8.scala
similarity index 100%
rename from testcases/repair/HeapSort/HeapSort8.scala
rename to testcases/repair/Heap/Heap8.scala
diff --git a/testcases/repair/HeapSort/HeapSort9.scala b/testcases/repair/Heap/Heap9.scala
similarity index 100%
rename from testcases/repair/HeapSort/HeapSort9.scala
rename to testcases/repair/Heap/Heap9.scala
diff --git a/testcases/repair/List/List12.scala b/testcases/repair/List/List12.scala
new file mode 100644
index 0000000000000000000000000000000000000000..63c1da6be5c444b13525c444dfb207ce1b976c5c
--- /dev/null
+++ b/testcases/repair/List/List12.scala
@@ -0,0 +1,424 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon.custom
+
+import leon._
+import leon.lang._
+import leon.annotation._
+
+sealed abstract class List0[T] {
+  def size: Int = (this match {
+    case Nil0() => 0
+    case Cons0(h, t) => 1 + t.size
+  }) ensuring (_ >= 0)
+
+  def content: Set[T] = this match {
+    case Nil0() => Set()
+    case Cons0(h, t) => Set(h) ++ t.content
+  }
+
+  def contains(v: T): Boolean = (this match {
+    case Cons0(h, t) if h == v => true
+    case Cons0(_, t) => t.contains(v)
+    case Nil0() => false
+  }) ensuring { res => res == (content contains v) }
+
+  def ++(that: List0[T]): List0[T] = (this match {
+    case Nil0() => that
+    case Cons0(x, xs) => Cons0(x, xs ++ that)
+  }) ensuring { res => (res.content == this.content ++ that.content) && (res.size == this.size + that.size)}
+
+  def head: T = {
+    require(this != Nil0[T]())
+    this match {
+      case Cons0(h, t) => h
+    }
+  }
+
+  def tail: List0[T] = {
+    require(this != Nil0[T]())
+    this match {
+      case Cons0(h, t) => t
+    }
+  }
+
+  def apply(index: Int): T = {
+    require(0 <= index && index < size)
+    if (index == 0) {
+      head
+    } else {
+       tail(index-1)
+    }
+  }
+
+  def ::(t:T): List0[T] = Cons0(t, this)
+
+  def :+(t:T): List0[T] = {
+    this match {
+      case Nil0() => Cons0(t, this)
+      case Cons0(x, xs) => Cons0(x, xs :+ (t))
+    }
+  } ensuring(res => (res.size == size + 1) && (res.content == content ++ Set(t)))
+
+  def reverse: List0[T] = {
+    this match {
+      case Nil0() => this
+      case Cons0(x,xs) => xs.reverse :+ x
+    }
+  } ensuring (res => (res.size == size) && (res.content == content))
+
+  def take(i: Int): List0[T] = (this, i) match {
+    case (Nil0(), _) => Nil0()
+    case (Cons0(h, t), i) =>
+      if (i == 0) {
+        Nil0()
+      } else {
+        Cons0(h, t.take(i-1))
+      }
+  }
+
+  def drop(i: Int): List0[T] = (this, i) match {
+    case (Nil0(), _) => Nil0()
+    case (Cons0(h, t), i) =>
+      if (i == 0) {
+        Cons0(h, t)
+      } else {
+        t.drop(i-1)
+      }
+  }
+
+  def slice(from: Int, to: Int): List0[T] = {
+    require(from < to && to < size && from >= 0)
+    drop(from).take(to-from)
+  }
+
+  def replace(from: T, to: T): List0[T] = this match {
+    case Nil0() => Nil0()
+    case Cons0(h, t) =>
+      val r = t.replace(from, to)
+      if (h == from) {
+        Cons0(to, r)
+      } else {
+        Cons0(h, r)
+      }
+  }
+
+  private def chunk0(s: Int, l: List0[T], acc: List0[T], res: List0[List0[T]], s0: Int): List0[List0[T]] = l match {
+    case Nil0() =>
+      if (acc.size > 0) {
+        res :+ acc
+      } else {
+        res
+      }
+    case Cons0(h, t) =>
+      if (s0 == 0) {
+        chunk0(s, l, Nil0(), res :+ acc, s)
+      } else {
+        chunk0(s, t, acc :+ h, res, s0-1)
+      }
+  }
+
+  def chunks(s: Int): List0[List0[T]] = {
+    require(s > 0)
+
+    chunk0(s, this, Nil0(), Nil0(), s)
+  }
+
+  def zip[B](that: List0[B]): List0[(T, B)] = (this, that) match {
+    case (Cons0(h1, t1), Cons0(h2, t2)) =>
+      Cons0((h1, h2), t1.zip(t2))
+    case (_) =>
+      Nil0()
+  }
+
+  def -(e: T): List0[T] = {
+    this match {
+      case Cons0(h, t) =>
+        if (e == h) {
+          t // FIXME
+        } else {
+          Cons0(h, t - e)
+        }
+      case Nil0() =>
+        Nil0()
+    }
+  } ensuring {
+    res => res.content == this.content -- Set(e)
+  }
+
+  def --(that: List0[T]): List0[T] = this match {
+    case Cons0(h, t) =>
+      if (that.contains(h)) {
+        t -- that
+      } else {
+        Cons0(h, t -- that)
+      }
+    case Nil0() =>
+      Nil0()
+  }
+
+  def &(that: List0[T]): List0[T] = this match {
+    case Cons0(h, t) =>
+      if (that.contains(h)) {
+        Cons0(h, t & that)
+      } else {
+        t & that
+      }
+    case Nil0() =>
+      Nil0()
+  }
+
+  def pad(s: Int, e: T): List0[T] = { (this, s) match {
+    case (_, s) if s <= 0 =>
+      this
+    case (Nil0(), s) =>
+      Cons0(e, Nil0().pad(s-1, e))
+    case (Cons0(h, t), s) =>
+      Cons0(h, t.pad(s, e))
+  }} ensuring { res =>
+    ((this,s,e), res) passes {
+      case (Cons0(a,Nil0()), 2, x) => Cons0(a, Cons0(x, Cons0(x, Nil0())))
+    }
+  }
+
+  def find(e: T): Option[Int] = this match {
+    case Nil0() => None()
+    case Cons0(h, t) =>
+      if (h == e) {
+        Some(0)
+      } else {
+        t.find(e) match {
+          case None()  => None()
+          case Some(i) => Some(i+1)
+        }
+      }
+  }
+
+  def init: List0[T] = (this match {
+    case Cons0(h, Nil0()) =>
+      Nil0[T]()
+    case Cons0(h, t) =>
+      Cons0[T](h, t.init)
+    case Nil0() =>
+      Nil0[T]()
+  }) ensuring ( (r: List0[T]) => ((r.size < this.size) || (this.size == 0)) )
+
+  def lastOption: Option[T] = this match {
+    case Cons0(h, t) =>
+      t.lastOption.orElse(Some(h))
+    case Nil0() =>
+      None()
+  }
+
+  def firstOption: Option[T] = this match {
+    case Cons0(h, t) =>
+      Some(h)
+    case Nil0() =>
+      None()
+  }
+
+  def unique: List0[T] = this match {
+    case Nil0() => Nil0()
+    case Cons0(h, t) =>
+      Cons0(h, t.unique - h)
+  }
+
+  def splitAt(e: T): List0[List0[T]] =  split(Cons0(e, Nil0()))
+
+  def split(seps: List0[T]): List0[List0[T]] = this match {
+    case Cons0(h, t) =>
+      if (seps.contains(h)) {
+        Cons0(Nil0(), t.split(seps))
+      } else {
+        val r = t.split(seps)
+        Cons0(Cons0(h, r.head), r.tail)
+      }
+    case Nil0() =>
+      Cons0(Nil0(), Nil0())
+  }
+
+  def count(e: T): Int = this match {
+    case Cons0(h, t) =>
+      if (h == e) {
+        1 + t.count(e)
+      } else {
+        t.count(e)
+      }
+    case Nil0() =>
+      0
+  }
+
+  def evenSplit: (List0[T], List0[T]) = {
+    val c = size/2
+    (take(c), drop(c))
+  }
+
+  def insertAt(pos: Int, l: List0[T]): List0[T] = {
+    if(pos < 0) {
+      insertAt(size + pos, l)
+    } else if(pos == 0) {
+      l ++ this
+    } else {
+      this match {
+        case Cons0(h, t) =>
+          Cons0(h, t.insertAt(pos-1, l))
+        case Nil0() =>
+          l
+      }
+    }
+  }
+
+  def replaceAt(pos: Int, l: List0[T]): List0[T] = {
+    if(pos < 0) {
+      replaceAt(size + pos, l)
+    } else if(pos == 0) {
+      l ++ this.drop(l.size)
+    } else {
+      this match {
+        case Cons0(h, t) =>
+          Cons0(h, t.replaceAt(pos-1, l))
+        case Nil0() =>
+          l
+      }
+    }
+  }
+
+  def rotate(s: Int): List0[T] = {
+    if (s < 0) {
+      rotate(size+s)
+    } else {
+      val s2 = s % size
+      drop(s2) ++ take(s2)
+    }
+  }
+
+  def isEmpty = this match { 
+    case Nil0() => true
+    case _ => false 
+  }
+
+}
+
+@ignore
+object List0 {
+  def apply[T](elems: T*): List0[T] = ???
+}
+
+@library
+object List0Ops {
+  def flatten[T](ls: List0[List0[T]]): List0[T] = ls match {
+    case Cons0(h, t) => h ++ flatten(t)
+    case Nil0() => Nil0()
+  }
+
+  def isSorted(ls: List0[Int]): Boolean = ls match {
+    case Nil0() => true
+    case Cons0(_, Nil0()) => true
+    case Cons0(h1, Cons0(h2, _)) if(h1 > h2) => false
+    case Cons0(_, t) => isSorted(t)
+  }
+
+  def sorted(ls: List0[Int]): List0[Int] = ls match {
+    case Cons0(h, t) => insSort(sorted(t), h)
+    case Nil0() => Nil0()
+  }
+
+  def insSort(ls: List0[Int], v: Int): List0[Int] = ls match {
+    case Nil0() => Cons0(v, Nil0())
+    case Cons0(h, t) =>
+      if (v <= h) {
+        Cons0(v, t)
+      } else {
+        Cons0(h, insSort(t, v))
+      }
+  }
+}
+
+
+case class Cons0[T](h: T, t: List0[T]) extends List0[T]
+case class Nil0[T]() extends List0[T]
+
+@library
+object List0Specs {
+  def snocIndex[T](l : List0[T], t : T, i : Int) : Boolean = {
+    require(0 <= i && i < l.size + 1)
+    // proof:
+    (l match {
+      case Nil0() => true
+      case Cons0(x, xs) => if (i > 0) snocIndex[T](xs, t, i-1) else true
+    }) &&
+    // claim:
+    ((l :+ t).apply(i) == (if (i < l.size) l(i) else t))
+  }.holds
+
+  def reverseIndex[T](l : List0[T], i : Int) : Boolean = {
+    require(0 <= i && i < l.size)
+    (l match {
+      case Nil0() => true
+      case Cons0(x,xs) => snocIndex(l, x, i) && reverseIndex[T](l,i)
+    }) &&
+    (l.reverse.apply(i) == l.apply(l.size - 1 - i))
+  }.holds
+
+  def appendIndex[T](l1 : List0[T], l2 : List0[T], i : Int) : Boolean = {
+    require(0 <= i && i < l1.size + l2.size)
+    (l1 match {
+      case Nil0() => true
+      case Cons0(x,xs) => if (i==0) true else appendIndex[T](xs,l2,i-1)
+    }) &&
+    ((l1 ++ l2).apply(i) == (if (i < l1.size) l1(i) else l2(i - l1.size)))
+  }.holds
+
+  def appendAssoc[T](l1 : List0[T], l2 : List0[T], l3 : List0[T]) : Boolean = {
+    (l1 match {
+      case Nil0() => true
+      case Cons0(x,xs) => appendAssoc(xs,l2,l3)
+    }) &&
+    (((l1 ++ l2) ++ l3) == (l1 ++ (l2 ++ l3)))
+  }.holds
+
+  def snocIsAppend[T](l : List0[T], t : T) : Boolean = {
+    (l match {
+      case Nil0() => true
+      case Cons0(x,xs) =>  snocIsAppend(xs,t)
+    }) &&
+    ((l :+ t) == l ++ Cons0[T](t, Nil0()))
+  }.holds
+
+  def snocAfterAppend[T](l1 : List0[T], l2 : List0[T], t : T) : Boolean = {
+    (l1 match {
+      case Nil0() => true
+      case Cons0(x,xs) =>  snocAfterAppend(xs,l2,t)
+    }) &&
+    ((l1 ++ l2) :+ t == (l1 ++ (l2 :+ t)))
+  }.holds
+
+  def snocReverse[T](l : List0[T], t : T) : Boolean = {
+    (l match {
+      case Nil0() => true
+      case Cons0(x,xs) => snocReverse(xs,t)
+    }) &&
+    ((l :+ t).reverse == Cons0(t, l.reverse))
+  }.holds
+
+  def reverseReverse[T](l : List0[T]) : Boolean = {
+    (l match {
+      case Nil0() => true
+      case Cons0(x,xs) => reverseReverse[T](xs) && snocReverse[T](xs.reverse, x)
+    }) &&
+    (l.reverse.reverse == l)
+  }.holds
+
+  //// my hand calculation shows this should work, but it does not seem to be found
+  //def reverseAppend[T](l1 : List0[T], l2 : List0[T]) : Boolean = {
+  //  (l1 match {
+  //    case Nil0() => true
+  //    case Cons0(x,xs) => {
+  //      reverseAppend(xs,l2) &&
+  //      snocAfterAppend[T](l2.reverse, xs.reverse, x) &&
+  //      l1.reverse == (xs.reverse :+ x)
+  //    }
+  //  }) &&
+  //  ((l1 ++ l2).reverse == (l2.reverse ++ l1.reverse))
+  //}.holds
+}
diff --git a/testcases/repair/List/List13.scala b/testcases/repair/List/List13.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4dc3f2177b30344665d1bb8fb34da38d77b31d17
--- /dev/null
+++ b/testcases/repair/List/List13.scala
@@ -0,0 +1,423 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon.custom
+
+import leon._
+import leon.lang._
+import leon.annotation._
+
+sealed abstract class List0[T] {
+  def size: Int = (this match {
+    case Nil0() => 0
+    case Cons0(h, t) => 1 + t.size
+  }) ensuring (_ >= 0)
+
+  def content: Set[T] = this match {
+    case Nil0() => Set()
+    case Cons0(h, t) => Set(h) ++ t.content
+  }
+
+  def contains(v: T): Boolean = (this match {
+    case Cons0(h, t) if h == v => true
+    case Cons0(_, t) => t.contains(v)
+    case Nil0() => false
+  }) ensuring { res => res == (content contains v) }
+
+  def ++(that: List0[T]): List0[T] = (this match {
+    case Nil0() => that
+    case Cons0(x, xs) => Cons0(x, xs ++ that)
+  }) ensuring { res => (res.content == this.content ++ that.content) && (res.size == this.size + that.size)}
+
+  def head: T = {
+    require(this != Nil0[T]())
+    this match {
+      case Cons0(h, t) => h
+    }
+  }
+
+  def tail: List0[T] = {
+    require(this != Nil0[T]())
+    this match {
+      case Cons0(h, t) => t
+    }
+  }
+
+  def apply(index: Int): T = {
+    require(0 <= index && index < size)
+    if (index == 0) {
+      head
+    } else {
+       tail(index-1)
+    }
+  }
+
+  def ::(t:T): List0[T] = Cons0(t, this)
+
+  def :+(t:T): List0[T] = {
+    this match {
+      case Nil0() => Cons0(t, this)
+      case Cons0(x, xs) => Cons0(x, xs :+ (t))
+    }
+  } ensuring(res => (res.size == size + 1) && (res.content == content ++ Set(t)))
+
+  def reverse: List0[T] = {
+    this match {
+      case Nil0() => this
+      case Cons0(x,xs) => xs.reverse :+ x
+    }
+  } ensuring (res => (res.size == size) && (res.content == content))
+
+  def take(i: Int): List0[T] = (this, i) match {
+    case (Nil0(), _) => Nil0()
+    case (Cons0(h, t), i) =>
+      if (i == 0) {
+        Nil0()
+      } else {
+        Cons0(h, t.take(i-1))
+      }
+  }
+
+  def drop(i: Int): List0[T] = { (this, i) match {
+    case (Nil0(), _) => Nil0()
+    case (Cons0(h, t), 0) =>
+      t // FIXME should be this
+    case (Cons0(_, t), i) =>
+      t.drop(i) //FIXME should be i-1
+  }} ensuring { res => ((this, i), res) passes { 
+    case (Cons0(_, Nil0()), 42) => Nil0()
+    case (l@Cons0(_, _), 0) => l
+    case (Cons0(a, Cons0(b, Nil0())), 1) => Cons0(b, Nil0())
+    case (Cons0(a, Cons0(b, Cons0(c, Nil0()))), 2) => Cons0(c, Nil0())
+  }}
+
+  def slice(from: Int, to: Int): List0[T] = {
+    require(from < to && to < size && from >= 0)
+    drop(from).take(to-from)
+  }
+
+  def replace(from: T, to: T): List0[T] = this match {
+    case Nil0() => Nil0()
+    case Cons0(h, t) =>
+      val r = t.replace(from, to)
+      if (h == from) {
+        Cons0(to, r)
+      } else {
+        Cons0(h, r)
+      }
+  }
+
+  private def chunk0(s: Int, l: List0[T], acc: List0[T], res: List0[List0[T]], s0: Int): List0[List0[T]] = l match {
+    case Nil0() =>
+      if (acc.size > 0) {
+        res :+ acc
+      } else {
+        res
+      }
+    case Cons0(h, t) =>
+      if (s0 == 0) {
+        chunk0(s, l, Nil0(), res :+ acc, s)
+      } else {
+        chunk0(s, t, acc :+ h, res, s0-1)
+      }
+  }
+
+  def chunks(s: Int): List0[List0[T]] = {
+    require(s > 0)
+
+    chunk0(s, this, Nil0(), Nil0(), s)
+  }
+
+  def zip[B](that: List0[B]): List0[(T, B)] = (this, that) match {
+    case (Cons0(h1, t1), Cons0(h2, t2)) =>
+      Cons0((h1, h2), t1.zip(t2))
+    case (_) =>
+      Nil0()
+  }
+
+  def -(e: T): List0[T] = this match {
+    case Cons0(h, t) =>
+      if (e == h) {
+        t - e
+      } else {
+        Cons0(h, t - e)
+      }
+    case Nil0() =>
+      Nil0()
+  }
+
+  def --(that: List0[T]): List0[T] = this match {
+    case Cons0(h, t) =>
+      if (that.contains(h)) {
+        t -- that
+      } else {
+        Cons0(h, t -- that)
+      }
+    case Nil0() =>
+      Nil0()
+  }
+
+  def &(that: List0[T]): List0[T] = this match {
+    case Cons0(h, t) =>
+      if (that.contains(h)) {
+        Cons0(h, t & that)
+      } else {
+        t & that
+      }
+    case Nil0() =>
+      Nil0()
+  }
+
+  def pad(s: Int, e: T): List0[T] = { (this, s) match {
+    case (_, s) if s <= 0 =>
+      this
+    case (Nil0(), s) =>
+      Cons0(e, Nil0().pad(s-1, e))
+    case (Cons0(h, t), s) =>
+      Cons0(h, t.pad(s, e))
+  }} ensuring { res =>
+    ((this,s,e), res) passes {
+      case (Cons0(a,Nil0()), 2, x) => Cons0(a, Cons0(x, Cons0(x, Nil0())))
+    }
+  }
+
+  def find(e: T): Option[Int] = this match {
+    case Nil0() => None()
+    case Cons0(h, t) =>
+      if (h == e) {
+        Some(0)
+      } else {
+        t.find(e) match {
+          case None()  => None()
+          case Some(i) => Some(i+1)
+        }
+      }
+  }
+
+  def init: List0[T] = (this match {
+    case Cons0(h, Nil0()) =>
+      Nil0[T]()
+    case Cons0(h, t) =>
+      Cons0[T](h, t.init)
+    case Nil0() =>
+      Nil0[T]()
+  }) ensuring ( (r: List0[T]) => ((r.size < this.size) || (this.size == 0)) )
+
+  def lastOption: Option[T] = this match {
+    case Cons0(h, t) =>
+      t.lastOption.orElse(Some(h))
+    case Nil0() =>
+      None()
+  }
+
+  def firstOption: Option[T] = this match {
+    case Cons0(h, t) =>
+      Some(h)
+    case Nil0() =>
+      None()
+  }
+
+  def unique: List0[T] = this match {
+    case Nil0() => Nil0()
+    case Cons0(h, t) =>
+      Cons0(h, t.unique - h)
+  }
+
+  def splitAt(e: T): List0[List0[T]] =  split(Cons0(e, Nil0()))
+
+  def split(seps: List0[T]): List0[List0[T]] = this match {
+    case Cons0(h, t) =>
+      if (seps.contains(h)) {
+        Cons0(Nil0(), t.split(seps))
+      } else {
+        val r = t.split(seps)
+        Cons0(Cons0(h, r.head), r.tail)
+      }
+    case Nil0() =>
+      Cons0(Nil0(), Nil0())
+  }
+
+  def count(e: T): Int = this match {
+    case Cons0(h, t) =>
+      if (h == e) {
+        1 + t.count(e)
+      } else {
+        t.count(e)
+      }
+    case Nil0() =>
+      0
+  }
+
+  def evenSplit: (List0[T], List0[T]) = {
+    val c = size/2
+    (take(c), drop(c))
+  }
+
+  def insertAt(pos: Int, l: List0[T]): List0[T] = {
+    if(pos < 0) {
+      insertAt(size + pos, l)
+    } else if(pos == 0) {
+      l ++ this
+    } else {
+      this match {
+        case Cons0(h, t) =>
+          Cons0(h, t.insertAt(pos-1, l))
+        case Nil0() =>
+          l
+      }
+    }
+  }
+
+  def replaceAt(pos: Int, l: List0[T]): List0[T] = {
+    if(pos < 0) {
+      replaceAt(size + pos, l)
+    } else if(pos == 0) {
+      l ++ this.drop(l.size)
+    } else {
+      this match {
+        case Cons0(h, t) =>
+          Cons0(h, t.replaceAt(pos-1, l))
+        case Nil0() =>
+          l
+      }
+    }
+  }
+
+  def rotate(s: Int): List0[T] = {
+    if (s < 0) {
+      rotate(size+s)
+    } else {
+      val s2 = s % size
+      drop(s2) ++ take(s2)
+    }
+  }
+
+  def isEmpty = this match { 
+    case Nil0() => true
+    case _ => false 
+  }
+
+}
+
+@ignore
+object List0 {
+  def apply[T](elems: T*): List0[T] = ???
+}
+
+@library
+object List0Ops {
+  def flatten[T](ls: List0[List0[T]]): List0[T] = ls match {
+    case Cons0(h, t) => h ++ flatten(t)
+    case Nil0() => Nil0()
+  }
+
+  def isSorted(ls: List0[Int]): Boolean = ls match {
+    case Nil0() => true
+    case Cons0(_, Nil0()) => true
+    case Cons0(h1, Cons0(h2, _)) if(h1 > h2) => false
+    case Cons0(_, t) => isSorted(t)
+  }
+
+  def sorted(ls: List0[Int]): List0[Int] = ls match {
+    case Cons0(h, t) => insSort(sorted(t), h)
+    case Nil0() => Nil0()
+  }
+
+  def insSort(ls: List0[Int], v: Int): List0[Int] = ls match {
+    case Nil0() => Cons0(v, Nil0())
+    case Cons0(h, t) =>
+      if (v <= h) {
+        Cons0(v, t)
+      } else {
+        Cons0(h, insSort(t, v))
+      }
+  }
+}
+
+
+case class Cons0[T](h: T, t: List0[T]) extends List0[T]
+case class Nil0[T]() extends List0[T]
+
+@library
+object List0Specs {
+  def snocIndex[T](l : List0[T], t : T, i : Int) : Boolean = {
+    require(0 <= i && i < l.size + 1)
+    // proof:
+    (l match {
+      case Nil0() => true
+      case Cons0(x, xs) => if (i > 0) snocIndex[T](xs, t, i-1) else true
+    }) &&
+    // claim:
+    ((l :+ t).apply(i) == (if (i < l.size) l(i) else t))
+  }.holds
+
+  def reverseIndex[T](l : List0[T], i : Int) : Boolean = {
+    require(0 <= i && i < l.size)
+    (l match {
+      case Nil0() => true
+      case Cons0(x,xs) => snocIndex(l, x, i) && reverseIndex[T](l,i)
+    }) &&
+    (l.reverse.apply(i) == l.apply(l.size - 1 - i))
+  }.holds
+
+  def appendIndex[T](l1 : List0[T], l2 : List0[T], i : Int) : Boolean = {
+    require(0 <= i && i < l1.size + l2.size)
+    (l1 match {
+      case Nil0() => true
+      case Cons0(x,xs) => if (i==0) true else appendIndex[T](xs,l2,i-1)
+    }) &&
+    ((l1 ++ l2).apply(i) == (if (i < l1.size) l1(i) else l2(i - l1.size)))
+  }.holds
+
+  def appendAssoc[T](l1 : List0[T], l2 : List0[T], l3 : List0[T]) : Boolean = {
+    (l1 match {
+      case Nil0() => true
+      case Cons0(x,xs) => appendAssoc(xs,l2,l3)
+    }) &&
+    (((l1 ++ l2) ++ l3) == (l1 ++ (l2 ++ l3)))
+  }.holds
+
+  def snocIsAppend[T](l : List0[T], t : T) : Boolean = {
+    (l match {
+      case Nil0() => true
+      case Cons0(x,xs) =>  snocIsAppend(xs,t)
+    }) &&
+    ((l :+ t) == l ++ Cons0[T](t, Nil0()))
+  }.holds
+
+  def snocAfterAppend[T](l1 : List0[T], l2 : List0[T], t : T) : Boolean = {
+    (l1 match {
+      case Nil0() => true
+      case Cons0(x,xs) =>  snocAfterAppend(xs,l2,t)
+    }) &&
+    ((l1 ++ l2) :+ t == (l1 ++ (l2 :+ t)))
+  }.holds
+
+  def snocReverse[T](l : List0[T], t : T) : Boolean = {
+    (l match {
+      case Nil0() => true
+      case Cons0(x,xs) => snocReverse(xs,t)
+    }) &&
+    ((l :+ t).reverse == Cons0(t, l.reverse))
+  }.holds
+
+  def reverseReverse[T](l : List0[T]) : Boolean = {
+    (l match {
+      case Nil0() => true
+      case Cons0(x,xs) => reverseReverse[T](xs) && snocReverse[T](xs.reverse, x)
+    }) &&
+    (l.reverse.reverse == l)
+  }.holds
+
+  //// my hand calculation shows this should work, but it does not seem to be found
+  //def reverseAppend[T](l1 : List0[T], l2 : List0[T]) : Boolean = {
+  //  (l1 match {
+  //    case Nil0() => true
+  //    case Cons0(x,xs) => {
+  //      reverseAppend(xs,l2) &&
+  //      snocAfterAppend[T](l2.reverse, xs.reverse, x) &&
+  //      l1.reverse == (xs.reverse :+ x)
+  //    }
+  //  }) &&
+  //  ((l1 ++ l2).reverse == (l2.reverse ++ l1.reverse))
+  //}.holds
+}
diff --git a/testcases/repair/MergeSort/MergeSort.scala b/testcases/repair/MergeSort/MergeSort.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d4a0f89e9acacd601766461f4090ce84692e32f4
--- /dev/null
+++ b/testcases/repair/MergeSort/MergeSort.scala
@@ -0,0 +1,54 @@
+import leon.collection._
+
+object MergeSort {
+
+  def split(l : List[Int]) : (List[Int],List[Int]) = { l match {
+    case Cons(a, Cons(b, t)) => 
+      val (rec1, rec2) = split(t)
+      (Cons(a, rec1), Cons(b, rec2))
+    case other => (other, Nil())
+  }} ensuring { res =>
+    val (l1, l2) = res
+    l1.size >= l2.size &&
+    l1.size <= l2.size + 1 &&
+    l1.size + l2.size == l.size &&
+    l1.content ++ l2.content == l.content
+  }
+
+  def isSorted(l : List[Int]) : Boolean = l match {
+    case Cons(x, t@Cons(y, _)) => x <= y && isSorted(t)
+    case _ => true
+  }
+
+  def merge(l1 : List[Int], l2 : List[Int]) : List[Int] = {
+    require(isSorted(l1) && isSorted(l2))
+    (l1, l2) match {
+      case (Cons(h1, t1), Cons(h2,t2)) => 
+        if (h1 <= h2) 
+          Cons(h1, merge(t1, l2))
+        else 
+          Cons(h2, merge(l1, t2))
+      case (Nil(), _) => l2
+      case (_, Nil()) => l1
+    }
+  } ensuring { res =>
+    isSorted(res) &&
+    res.size == l1.size + l2.size  &&
+    res.content == l1.content ++ l2.content
+  }
+
+  def mergeSort(l : List[Int]) : List[Int] = { l match {
+    case Nil() => l
+    case Cons(_, Nil()) => l
+    case other =>
+      val (l1, l2) = split(other)
+      merge(mergeSort(l1), mergeSort(l2))
+  }} ensuring { res =>
+    isSorted(res) &&
+    res.content == l.content &&
+    res.size == l.size
+  }
+}
+
+
+
diff --git a/testcases/repair/MergeSort/MergeSort1.scala b/testcases/repair/MergeSort/MergeSort1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f8515bade6e7084d3af05874b91893c6cb89f90f
--- /dev/null
+++ b/testcases/repair/MergeSort/MergeSort1.scala
@@ -0,0 +1,66 @@
+object MergeSort {
+
+  abstract class List {
+    def size : Int = this match {
+      case Nil() => 0
+      case Cons(_, tl) => 1 + tl.size
+    }
+    def content : Set[Int] = this match {
+      case Nil() => Set.empty[Int]
+      case Cons(hd, tl) => tl.content ++ Set(hd)
+    }
+  }
+
+  case class Nil() extends List
+  case class Cons(hd : Int, tl : List) extends List
+
+  def split(l : List) : (List,List) = { l match {
+    case Cons(a, Cons(b, t)) => 
+      val (rec1, rec2) = split(t)
+      (rec1, rec2) //FIXME forgot a and b
+    case other => (other, Nil())
+  }} ensuring { res =>
+    val (l1, l2) = res
+    l1.size >= l2.size &&
+    l1.size <= l2.size + 1 &&
+    l1.size + l2.size == l.size &&
+    l1.content ++ l2.content == l.content
+  }
+
+  def isSorted(l : List) : Boolean = l match {
+    case Cons(x, t@Cons(y, _)) => x <= y && isSorted(t)
+    case _ => true
+  }
+
+  def merge(l1 : List, l2 : List) : List = {
+    require(isSorted(l1) && isSorted(l2))
+    (l1, l2) match {
+      case (Cons(h1, t1), Cons(h2,t2)) => 
+        if (h1 <= h2) 
+          Cons(h1, merge(t1, l2))
+        else 
+          Cons(h2, merge(l1, t2))
+      case (Nil(), _) => l2
+      case (_, Nil()) => l1
+    }
+  } ensuring { res =>
+    isSorted(res) &&
+    res.size == l1.size + l2.size  &&
+    res.content == l1.content ++ l2.content
+  }
+
+  def mergeSort(l : List) : List = { l match {
+    case Nil() => l
+    case Cons(_, Nil()) => l
+    case other =>
+      val (l1, l2) = split(other)
+      merge(mergeSort(l1), mergeSort(l2))
+  }} ensuring { res =>
+    isSorted(res) &&
+    res.content == l.content &&
+    res.size == l.size
+  }
+}
+
+
+
diff --git a/testcases/repair/MergeSort/MergeSort2.scala b/testcases/repair/MergeSort/MergeSort2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d9966ecdc70e8200e318580999169059fb7fed98
--- /dev/null
+++ b/testcases/repair/MergeSort/MergeSort2.scala
@@ -0,0 +1,54 @@
+import leon.collection._
+
+object MergeSort {
+
+  def split(l : List[Int]) : (List[Int],List[Int]) = { l match {
+    case Cons(a, Cons(b, t)) => 
+      val (rec1, rec2) = split(t)
+      (Cons(a, rec1), Cons(b, rec2))
+    case other => (other, Nil())
+  }} ensuring { res =>
+    val (l1, l2) = res
+    l1.size >= l2.size &&
+    l1.size <= l2.size + 1 &&
+    l1.size + l2.size == l.size &&
+    l1.content ++ l2.content == l.content
+  }
+
+  def isSorted(l : List[Int]) : Boolean = l match {
+    case Cons(x, t@Cons(y, _)) => x <= y && isSorted(t)
+    case _ => true
+  }
+
+  def merge(l1 : List[Int], l2 : List[Int]) : List[Int] = {
+    require(isSorted(l1) && isSorted(l2))
+    (l1, l2) match {
+      case (Cons(h1, t1), Cons(h2,t2)) => 
+        if (h1 <= h2) 
+          Cons(h1, merge(t1, l2))
+        else 
+          Cons(h1, merge(l1, t2)) // FIXME h1 instead of h2
+      case (Nil(), _) => l2
+      case (_, Nil()) => l1
+    }
+  } ensuring { res =>
+    isSorted(res) &&
+    res.size == l1.size + l2.size  &&
+    res.content == l1.content ++ l2.content
+  }
+
+  def mergeSort(l : List[Int]) : List[Int] = { l match {
+    case Nil() => l
+    case Cons(_, Nil()) => l
+    case other =>
+      val (l1, l2) = split(other)
+      merge(mergeSort(l1), mergeSort(l2))
+  }} ensuring { res =>
+    isSorted(res) &&
+    res.content == l.content &&
+    res.size == l.size
+  }
+}
+
+
+
diff --git a/testcases/repair/MergeSort/MergeSort3.scala b/testcases/repair/MergeSort/MergeSort3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7da332e56aa1f7d6f4feb56f03c80813c6bd09ee
--- /dev/null
+++ b/testcases/repair/MergeSort/MergeSort3.scala
@@ -0,0 +1,54 @@
+import leon.collection._
+
+object MergeSort {
+
+  def split(l : List[Int]) : (List[Int],List[Int]) = { l match {
+    case Cons(a, Cons(b, t)) => 
+      val (rec1, rec2) = split(t)
+      (Cons(a, rec1), Cons(b, rec2))
+    case other => (other, Nil())
+  }} ensuring { res =>
+    val (l1, l2) = res
+    l1.size >= l2.size &&
+    l1.size <= l2.size + 1 &&
+    l1.size + l2.size == l.size &&
+    l1.content ++ l2.content == l.content
+  }
+
+  def isSorted(l : List[Int]) : Boolean = l match {
+    case Cons(x, t@Cons(y, _)) => x <= y && isSorted(t)
+    case _ => true
+  }
+
+  def merge(l1 : List[Int], l2 : List[Int]) : List[Int] = {
+    require(isSorted(l1) && isSorted(l2))
+    (l1, l2) match {
+      case (Cons(h1, t1), Cons(h2,t2)) => 
+        if (h1 >= h2) // FIXME: should be <=
+          Cons(h1, merge(t1, l2))
+        else 
+          Cons(h2, merge(l1, t2))
+      case (Nil(), _) => l2
+      case (_, Nil()) => l1
+    }
+  } ensuring { res =>
+    isSorted(res) &&
+    res.size == l1.size + l2.size  &&
+    res.content == l1.content ++ l2.content
+  }
+
+  def mergeSort(l : List[Int]) : List[Int] = { l match {
+    case Nil() => l
+    case Cons(_, Nil()) => l
+    case other =>
+      val (l1, l2) = split(other)
+      merge(mergeSort(l1), mergeSort(l2))
+  }} ensuring { res =>
+    isSorted(res) &&
+    res.content == l.content &&
+    res.size == l.size
+  }
+}
+
+
+
diff --git a/testcases/repair/MergeSort/MergeSort4.scala b/testcases/repair/MergeSort/MergeSort4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..93872082dce48f13acc28034ca6787f554170ba5
--- /dev/null
+++ b/testcases/repair/MergeSort/MergeSort4.scala
@@ -0,0 +1,54 @@
+import leon.collection._
+
+object MergeSort {
+
+  def split(l : List[Int]) : (List[Int],List[Int]) = { l match {
+    case Cons(a, Cons(b, t)) => 
+      val (rec1, rec2) = split(t)
+      (Cons(a, rec1), Cons(b, rec2))
+    case other => (other, Nil())
+  }} ensuring { res =>
+    val (l1, l2) = res
+    l1.size >= l2.size &&
+    l1.size <= l2.size + 1 &&
+    l1.size + l2.size == l.size &&
+    l1.content ++ l2.content == l.content
+  }
+
+  def isSorted(l : List[Int]) : Boolean = l match {
+    case Cons(x, t@Cons(y, _)) => x <= y && isSorted(t)
+    case _ => true
+  }
+
+  def merge(l1 : List[Int], l2 : List[Int]) : List[Int] = {
+    require(isSorted(l1) && isSorted(l2))
+    (l1, l2) match {
+      case (Cons(h1, t1), Cons(h2,t2)) => 
+        if (h1 <= h2) 
+          Cons(h1, merge(t1, l2))
+        else 
+          merge(l1, t2) // FIXME missing Cons(h2
+      case (Nil(), _) => l2
+      case (_, Nil()) => l1
+    }
+  } ensuring { res =>
+    isSorted(res) &&
+    res.size == l1.size + l2.size  &&
+    res.content == l1.content ++ l2.content
+  }
+
+  def mergeSort(l : List[Int]) : List[Int] = { l match {
+    case Nil() => l
+    case Cons(_, Nil()) => l
+    case other =>
+      val (l1, l2) = split(other)
+      merge(mergeSort(l1), mergeSort(l2))
+  }} ensuring { res =>
+    isSorted(res) &&
+    res.content == l.content &&
+    res.size == l.size
+  }
+}
+
+
+
diff --git a/testcases/repair/MergeSort/MergeSort5.scala b/testcases/repair/MergeSort/MergeSort5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a04a0f491eb8fe6ec1d85bdaf9280c3190d365f2
--- /dev/null
+++ b/testcases/repair/MergeSort/MergeSort5.scala
@@ -0,0 +1,54 @@
+import leon.collection._
+
+object MergeSort {
+
+  def split(l : List[Int]) : (List[Int],List[Int]) = { l match {
+    case Cons(a, Cons(b, t)) => 
+      val (rec1, rec2) = split(t)
+      (Cons(a, rec1), Cons(b, rec2))
+    case other => (other, Nil())
+  }} ensuring { res =>
+    val (l1, l2) = res
+    l1.size >= l2.size &&
+    l1.size <= l2.size + 1 &&
+    l1.size + l2.size == l.size &&
+    l1.content ++ l2.content == l.content
+  }
+
+  def isSorted(l : List[Int]) : Boolean = l match {
+    case Cons(x, t@Cons(y, _)) => x <= y && isSorted(t)
+    case _ => true
+  }
+
+  def merge(l1 : List[Int], l2 : List[Int]) : List[Int] = {
+    require(isSorted(l1) && isSorted(l2))
+    (l1, l2) match {
+      case (Nil(), _) => l1 // FIXME should be l2
+      case (_, Nil()) => l1
+      case (Cons(h1, t1), Cons(h2,t2)) => 
+        if (h1 <= h2) 
+          Cons(h1, merge(t1, l2))
+        else 
+          Cons(h1, merge(l1, t2)) // FIXME should be h2
+    }
+  } ensuring { res =>
+    isSorted(res) &&
+    res.size == l1.size + l2.size  &&
+    res.content == l1.content ++ l2.content
+  }
+
+  def mergeSort(l : List[Int]) : List[Int] = { l match {
+    case Nil() => l
+    case Cons(_, Nil()) => l
+    case other =>
+      val (l1, l2) = split(other)
+      merge(mergeSort(l1), mergeSort(l2))
+  }} ensuring { res =>
+    isSorted(res) &&
+    res.content == l.content &&
+    res.size == l.size
+  }
+}
+
+
+
diff --git a/testcases/repair/MergeSort/repairs.last b/testcases/repair/MergeSort/repairs.last
new file mode 100644
index 0000000000000000000000000000000000000000..cbb39c41a4c3152a77203d261b0a4bc1a94e2cf5
--- /dev/null
+++ b/testcases/repair/MergeSort/repairs.last
@@ -0,0 +1,4 @@
+           MergeSort,     MergeSort1.scala,                merge, 705,  20,   5,  1081,  1324, 37526,      
+           MergeSort,     MergeSort3.scala,                merge, 705,  20,  14,   941,  1299, 47637,      
+           MergeSort,     MergeSort4.scala,            mergeSort, 704,  21,   4,   965,  4481, 37402,      
+           MergeSort,     MergeSort5.scala,                split, 169,  21,   3,   975,  1445,  6971,      
diff --git a/testcases/repair/Numerical/Numerical.scala b/testcases/repair/Numerical/Numerical.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1175da9cec6017d69ea1e1ba46ef0877b0be9ea9
--- /dev/null
+++ b/testcases/repair/Numerical/Numerical.scala
@@ -0,0 +1,54 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+import leon._
+import leon.lang._
+import leon.annotation._
+
+object Numerical {
+  def power(base: Int, p: Int): Int = {
+    require(p >= 0)
+    if (p == 0) {
+      1
+    } else if (p%2 == 0) {
+      power(base*base, p/2)
+    } else {
+      base*power(base, p-1)
+    }
+  } ensuring {
+    res => ((base, p), res) passes {
+      case (_, 0) => 1
+      case (b, 1) => b
+      case (2, 7) => 128
+      case (2, 10) => 1024
+    }
+  }
+
+  def gcd(a: Int, b: Int): Int = {
+    require(a > 0 && b > 0);
+
+    if (a == b) {
+      a
+    } else if (a > b) {
+      gcd(a-b, b)
+    } else {
+      gcd(a, b-a)
+    }
+  } ensuring {
+    res => (a%res == 0) && (b%res == 0) && (((a,b), res) passes {
+      case (468, 24) => 12
+    })
+  }
+
+  def moddiv(a: Int, b: Int): (Int, Int) = {
+    require(a >= 0 && b > 0);
+    if (b > a) {
+      (a, 0)
+    } else {
+      val (r1, r2) = moddiv(a-b, b)
+      (r1, r2+1)
+    }
+  } ensuring {
+    res =>  b*res._2 + res._1 == a
+  }
+
+}
diff --git a/testcases/repair/Numerical/Numerical1.scala b/testcases/repair/Numerical/Numerical1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4f1a32f8b1c45cbf343deba21035497342b515a1
--- /dev/null
+++ b/testcases/repair/Numerical/Numerical1.scala
@@ -0,0 +1,53 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+import leon._
+import leon.lang._
+import leon.annotation._
+
+object Numerical {
+  def power(base: Int, p: Int): Int = {
+    require(p >= 0)
+    if (p == 0) {
+      1
+    } else if (p%2 == 0) {
+      power(base*base, p/2)
+    } else {
+      power(base, p-1) // fixme: Missing base*
+    }
+  } ensuring {
+    res => ((base, p), res) passes {
+      case (_, 0) => 1
+      case (b, 1) => b
+      case (2, 7) => 128
+      case (2, 10) => 1024
+    }
+  }
+
+  def gcd(a: Int, b: Int): Int = {
+    require(a > 0 && b > 0);
+
+    if (a == b) {
+      a
+    } else if (a > b) {
+      gcd(a-b, b)
+    } else {
+      gcd(a, b-a)
+    }
+  } ensuring {
+    res => (a%res == 0) && (b%res == 0) && (((a,b), res) passes {
+      case (468, 24) => 12
+    })
+  }
+
+  def moddiv(a: Int, b: Int): (Int, Int) = {
+    require(a >= 0 && b > 0);
+    if (b > a) {
+      (a, 0)
+    } else {
+      val (r1, r2) = moddiv(a-b, b)
+      (r1, r2+1)
+    }
+  } ensuring {
+    res =>  b*res._2 + res._1 == a
+  }
+}
diff --git a/testcases/repair/Numerical/Numerical2.scala b/testcases/repair/Numerical/Numerical2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ec191f681f128d52fa63438f32d9124b6fcffaf6
--- /dev/null
+++ b/testcases/repair/Numerical/Numerical2.scala
@@ -0,0 +1,43 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+import leon._
+import leon.lang._
+import leon.annotation._
+
+object Numerical {
+  def power(base: Int, p: Int): Int = {
+    require(p >= 0)
+    if (p == 0) {
+      1
+    } else if (p%2 == 0) {
+      power(base*base, p/2)
+    } else {
+      base*power(base, p-1)
+    }
+  } ensuring {
+    res => ((base, p), res) passes {
+      case (_, 0) => 1
+      case (b, 1) => b
+      case (2, 7) => 128
+      case (2, 10) => 1024
+    }
+  }
+
+  def gcd(a: Int, b: Int): Int = {
+    require(a > 0 && b > 0);
+
+    if (a == b) {
+      1 // fixme: should be a
+    } else if (a > b) {
+      gcd(a-b, b)
+    } else {
+      gcd(a, b-a)
+    }
+  } ensuring {
+    res => (a%res == 0) && (b%res == 0) && (((a,b), res) passes {
+      case (120, 24) => 12
+      case (5, 7)    => 1
+      case (5, 5)    => 5
+    })
+  }
+}
diff --git a/testcases/repair/Numerical/Numerical3.scala b/testcases/repair/Numerical/Numerical3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4f782cab34f390c9a05d7362c2beeaa86718c911
--- /dev/null
+++ b/testcases/repair/Numerical/Numerical3.scala
@@ -0,0 +1,53 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+import leon._
+import leon.lang._
+import leon.annotation._
+
+object Numerical {
+  def power(base: Int, p: Int): Int = {
+    require(p >= 0)
+    if (p == 0) {
+      1
+    } else if (p%2 == 0) {
+      power(base*base, p/2)
+    } else {
+      base*power(base, p-1)
+    }
+  } ensuring {
+    res => ((base, p), res) passes {
+      case (_, 0) => 1
+      case (b, 1) => b
+      case (2, 7) => 128
+      case (2, 10) => 1024
+    }
+  }
+
+  def gcd(a: Int, b: Int): Int = {
+    require(a > 0 && b > 0);
+
+    if (a == b) {
+      a
+    } else if (a > b) {
+      gcd(a-b, b)
+    } else {
+      gcd(a, b-a)
+    }
+  } ensuring {
+    res => (a%res == 0) && (b%res == 0) && (((a,b), res) passes {
+      case (468, 24) => 12
+    })
+  }
+
+  def moddiv(a: Int, b: Int): (Int, Int) = {
+    require(a >= 0 && b > 0);
+    if (b > a) {
+      (1, 0) // fixme: should be (a, 0)
+    } else {
+      val (r1, r2) = moddiv(a-b, b)
+      (r1, r2+1)
+    }
+  } ensuring {
+    res =>  b*res._2 + res._1 == a
+  }
+}