diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 583296566..de9d740ae 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -30,7 +30,8 @@ object Main {
       invariant.engine.InferInvariantsPhase,
       laziness.LazinessEliminationPhase,
       genc.GenerateCPhase,
-      genc.CFileOutputPhase
+      genc.CFileOutputPhase,
+      comparison.ComparisonPhase
     )
   }
 
@@ -59,9 +60,11 @@ object Main {
     val optInferInv    = LeonFlagOptionDef("inferInv",    "Infer invariants from (instrumented) the code",             false)
     val optLazyEval    = LeonFlagOptionDef("lazy",        "Handles programs that may use the 'lazy' construct",        false)
     val optGenc        = LeonFlagOptionDef("genc",        "Generate C code",                                           false)
+    val optComparison  = LeonFlagOptionDef("compare", "Compare the targeted program to the Leon exemple suit", false)
+
 
     override val definedOptions: Set[LeonOptionDef[Any]] =
-      Set(optTermination, optRepair, optSynthesis, optIsabelle, optNoop, optHelp, optEval, optVerify, optInstrument, optInferInv, optLazyEval, optGenc)
+      Set(optTermination, optRepair, optSynthesis, optIsabelle, optNoop, optHelp, optEval, optVerify, optInstrument, optInferInv, optLazyEval, optGenc, optComparison)
   }
 
   lazy val allOptions: Set[LeonOptionDef[Any]] = allComponents.flatMap(_.definedOptions)
@@ -177,6 +180,8 @@ object Main {
     val instrumentF = ctx.findOptionOrDefault(optInstrument)
     val lazyevalF = ctx.findOptionOrDefault(optLazyEval)
     val analysisF = verifyF && terminationF
+    val comparisonF = ctx.findOptionOrDefault(optComparison)
+
     // Check consistency in options
 
     if (helpF) {
@@ -206,6 +211,7 @@ object Main {
         else if (instrumentF) InstrumentationPhase andThen FileOutputPhase
         else if (gencF) GenerateCPhase andThen CFileOutputPhase
         else if (lazyevalF) LazinessEliminationPhase
+        else if (comparisonF) comparison.ComparisonPhase andThen PrintReportPhase
         else verification
       }
 
@@ -217,6 +223,7 @@ object Main {
   private var hasFatal = false
 
   def main(args: Array[String]) {
+
     val argsl = args.toList
 
     // Process options
diff --git a/src/main/scala/leon/comparison/Comparator.scala b/src/main/scala/leon/comparison/Comparator.scala
new file mode 100644
index 000000000..f3badba75
--- /dev/null
+++ b/src/main/scala/leon/comparison/Comparator.scala
@@ -0,0 +1,14 @@
+package leon.comparison
+
+import leon.LeonContext
+import leon.purescala.Expressions.Expr
+
+/**
+  * Created by joachimmuth on 04.05.16.
+  */
+trait Comparator {
+  val name: String
+
+  def compare(exprCorpus: Expr, expr: Expr)(implicit context: LeonContext): (Double, String)
+
+}
diff --git a/src/main/scala/leon/comparison/ComparatorClassList.scala b/src/main/scala/leon/comparison/ComparatorClassList.scala
new file mode 100644
index 000000000..399c934a6
--- /dev/null
+++ b/src/main/scala/leon/comparison/ComparatorClassList.scala
@@ -0,0 +1,65 @@
+package leon.comparison
+
+import leon.{GlobalOptions, LeonContext, utils}
+import leon.comparison.Utils._
+import leon.purescala.Expressions._
+
+/**
+  * Created by joachimmuth on 02.05.16.
+  *
+  * This method shares similarities with the ComparatorByList.
+  * We keep the idea of comparing a list of expressions (disregarding their order), but now, instead of comparing
+  * two expressions (i.e. tree) we will extract the type of each expression.
+  *
+  * x match {
+  * case 1 => 'a'
+  * case 2 => 'b'
+  * }
+  *
+  * ComparatorByList -> {complete match, leaf(a), leaf(b)}
+  * ComparatorByListType -> {node(match), leaf(a), leaf(b)}
+  *
+  * x match {
+  * case 1 => 'a'
+  * case 2 => 'c'
+  * }
+  *
+  * ComparatorByList -> similarity 33%
+  * ComparatorByListType -> similarity 66%
+  */
+object ComparatorClassList extends Comparator {
+  val name = "ClassList"
+
+  def compare(exprCorpus: Expr, expr: Expr)(implicit context: LeonContext) = {
+    implicit val debugSection = utils.DebugSectionComparison
+    val listClassesA = collectClass(exprCorpus)
+    val listClassesB = collectClass(expr)
+
+    val similarExpr: Int = pairsOfSimilarExp(listClassesA, listClassesB)
+
+    val score = Utils.matchScore(similarExpr, listClassesA.size, listClassesB.size)
+
+    if (context.findOption(GlobalOptions.optDebug).isDefined) {
+      context.reporter.debug("-----------")
+      context.reporter.debug("COMPARATOR " + name)
+      context.reporter.debug("Expressions: \n" + expr + exprCorpus)
+      context.reporter.debug("List of classes: \n" + listClassesB + listClassesA)
+      context.reporter.debug("-----------")
+    }
+
+    (score, "")
+  }
+
+
+  def pairsOfSimilarExp(listExprCorpus: List[Class[_]], listExpr: List[Class[_]]): Int = {
+    def helper(listExprCorpus: List[Class[_]], listExpr: List[Class[_]], acc: Int): Int =
+      listExpr match {
+        case Nil => acc
+        case x :: xs if listExprCorpus.contains(x) => helper(listExprCorpus diff List(x), xs, acc + 1)
+        case x :: xs => helper(listExprCorpus, xs, acc)
+      }
+
+    helper(listExprCorpus, listExpr, 0)
+  }
+
+}
diff --git a/src/main/scala/leon/comparison/ComparatorClassTree.scala b/src/main/scala/leon/comparison/ComparatorClassTree.scala
new file mode 100644
index 000000000..8b2b039e2
--- /dev/null
+++ b/src/main/scala/leon/comparison/ComparatorClassTree.scala
@@ -0,0 +1,182 @@
+package leon.comparison
+
+import leon.{GlobalOptions, LeonContext, utils}
+import leon.comparison.Utils._
+import leon.purescala.Expressions._
+
+
+/**
+  * Created by joachimmuth on 12.05.16.
+  *
+  * Go through both trees in parallel and compare each expression based on its class. Try to find the biggest
+  * common tree.
+  *
+  * Procedure:
+  * - Find all possible pair of roots. Then consider all children of both roots, and check which are
+  * similar.
+  * - Consider all possible combinations of children and repeat the same operation on them.
+  * - Pick the biggest tree in the list of all possible similar tree
+  * - Remove the tree overlapping the one chosen, and search if it exists an other common tree. Repeat.
+  * - End with all common and exclusive common tree shared by trees A and B
+  *
+  * The MatchScore is calculated with the size of the common tree, compared with the sizes of trees A and B.
+  */
+object ComparatorClassTree extends Comparator {
+  val name: String = "ClassTree"
+
+
+  def compare(exprCorpus: Expr, expr: Expr)(implicit context: LeonContext) = {
+    implicit val debugSection = utils.DebugSectionComparison
+    val roots = possibleRoots(exprCorpus, expr)
+
+    val trees = roots.flatMap(possibleTrees(_))
+    val exclusives = exclusivesTrees(trees)
+    val sum = exclusives.foldLeft(0)((acc, tree) => acc + tree.size)
+
+    val listClassesA = collectClass(exprCorpus)
+    val listClassesB = collectClass(expr)
+
+    val score = matchScore(sum, listClassesA.size, listClassesB.size)
+
+    if (context.findOption(GlobalOptions.optDebug).isDefined) {
+      context.reporter.debug("---------------------")
+      context.reporter.debug("COMPARATOR " + name)
+      context.reporter.debug("Expressions: \n" + exprCorpus + expr)
+      context.reporter.debug("Common Tree: \n" + exclusives)
+      context.reporter.debug("---------------------")
+    }
+
+    (score, "")
+  }
+
+  /**
+    * Extract all non-overlapping trees, in size order
+    *
+    * @param trees
+    * @return
+    */
+  def exclusivesTrees(trees: List[FuncTree[(Expr, Expr)]]): List[FuncTree[(Expr, Expr)]] = trees match {
+    case Nil => Nil
+    case x :: xs =>
+      val biggest = trees.sortBy(-_.size).head
+      val rest = trees.filter(tree => flatList(tree).intersect(flatList(biggest)).isEmpty)
+      List(biggest) ++ exclusivesTrees(rest)
+  }
+
+  def flatList(tree: FuncTree[(Expr, Expr)]): List[Expr] = tree.toList.flatMap(p => List(p._1, p._2))
+
+  /**
+    * list of all similar pair of expressions, based on classes.
+    *
+    * @param exprCorpus
+    * @param expr
+    * @return
+    */
+  def possibleRoots(exprCorpus: Expr, expr: Expr): List[(Expr, Expr)] = {
+    val expressionsA = collectExpr(exprCorpus)
+    val expressionsB = collectExpr(expr)
+
+    val pairOfPossibleRoots = for {
+      exprA <- expressionsA
+      exprB <- expressionsB
+      if areSimilar(exprA.getClass, exprB.getClass)
+    } yield {
+      (exprA, exprB)
+    }
+
+    pairOfPossibleRoots
+  }
+
+
+  /**
+    * With a pair of roots, find all children and find all combination of matching children in order to create a list
+    * of all possible matching tree. Then recursively call itself on each pair of children.
+    *
+    * @param pair of matching root
+    * @return ether a Leaf or a List of all possible similar trees starting with this pair of roots
+    */
+  def possibleTrees(pair: (Expr, Expr)): List[FuncTree[(Expr, Expr)]] = {
+    val exprA = pair._1
+    val exprB = pair._2
+    val childrenA = getChildren(exprA)
+    val childrenB = getChildren(exprB)
+
+
+    val pairOfMatchingChildren = findPairOfMatchingChildren(childrenA, childrenB)
+    val combinationOfChildren = combineChildren(pairOfMatchingChildren)
+
+
+    if (pairOfMatchingChildren.isEmpty) {
+      List(FuncTree(pair, List()))
+    } else {
+      combinationOfChildren.foldLeft(List(): List[FuncTree[(Expr, Expr)]])(
+        (listOfTree, children) => listOfTree ++ treesWithChildCombination(pair, children.map(p => possibleTrees(p)))
+      )
+    }
+  }
+
+  def findPairOfMatchingChildren(childrenA: List[Expr], childrenB: List[Expr]): List[(Expr, Expr)] = {
+    for {
+      childA <- childrenA
+      childB <- childrenB
+      if areSimilar(childA.getClass, childB.getClass)
+    } yield {
+      (childA, childB)
+    }
+  }
+
+  /** All possible combination of pairs of children, given the condition that one child can only be used once.
+    *
+    * IMPROVEMENT: Here, it would be possible to already filter some cases.
+    * When we do the combination, we try all cases, using one pair of matching, two, three, ... we could only keep the
+    * ones using maximum of possible children, as we only want the biggest tree.
+    *
+    * @param pairs
+    * @return
+    */
+  def combineChildren(pairs: List[(Expr, Expr)]): List[List[(Expr, Expr)]] = {
+    combine(pairs).filterNot(p => isSameChildUsedTwice(p)).toList
+  }
+
+  def isSameChildUsedTwice(list: List[(Expr, Expr)]): Boolean = {
+    list.map(_._1).distinct.size != list.size ||
+      list.map(_._2).distinct.size != list.size
+  }
+
+  def combine(in: List[(Expr, Expr)]): Seq[List[(Expr, Expr)]] = {
+    for {
+      len <- 1 to in.length
+      combinations <- in combinations len
+    } yield combinations
+  }
+
+  /**
+    * As we recursively call the method, children will create list of possibilities, as the root does. All this possible
+    * combination need to be transformed into a list of complete tree.
+    *
+    * Technically, we have a combination of Children that return each a list of possible trees. So the upper-level tree
+    * (whom root is named pair) can have all possible combination of theses lists as children.
+    *
+    * @param pair
+    * @param listChildren
+    * @return
+    */
+  def treesWithChildCombination(pair: (Expr, Expr), listChildren: List[List[FuncTree[(Expr, Expr)]]]): List[FuncTree[(Expr, Expr)]] = {
+    def combine(list: List[List[FuncTree[(Expr, Expr)]]]): List[List[FuncTree[(Expr, Expr)]]] = list match {
+      case Nil => List(Nil)
+      case x :: xs =>
+        for {
+          j <- combine(xs)
+          i <- x
+        } yield i :: j
+    }
+
+    combine(listChildren).map(children => FuncTree(pair, children))
+  }
+
+
+  def areSimilar(getClass: Class[_ <: Expr], getClass1: Class[_ <: Expr]) = {
+    getClass == getClass1
+  }
+
+}
diff --git a/src/main/scala/leon/comparison/ComparatorDirectScoreTree.scala b/src/main/scala/leon/comparison/ComparatorDirectScoreTree.scala
new file mode 100644
index 000000000..5575cef94
--- /dev/null
+++ b/src/main/scala/leon/comparison/ComparatorDirectScoreTree.scala
@@ -0,0 +1,199 @@
+package leon.comparison
+
+import leon.{GlobalOptions, LeonContext, utils}
+import leon.comparison.Scores._
+import leon.comparison.Utils._
+import leon.purescala.Expressions._
+
+/**
+  * Created by joachimmuth on 02.06.16.
+  *
+  * Travers in parallel two trees. Instead of comparing Class like in ClassTree, we directly compute a score of the pair
+  * like in ScoreTree. This allow the most flexible comparison.
+  *
+  */
+object ComparatorDirectScoreTree extends Comparator {
+  override val name: String = "DirectScoreTree"
+
+
+  override def compare(exprCorpus: Expr, expr: Expr)(implicit context: LeonContext): (Double, String) = {
+    implicit val debugSection = utils.DebugSectionComparison
+    val roots = possibleRoots(exprCorpus, expr)
+    val trees = roots.flatMap(possibleTrees(_))
+    if (trees.isEmpty) return (0.0, "")
+
+    val (bestTree, score) = selectBestTree(trees, exprCorpus, expr)
+
+    if (context.findOption(GlobalOptions.optDebug).isDefined) {
+      context.reporter.debug("---------------------")
+      context.reporter.debug("COMPARATOR " + name)
+      context.reporter.debug("Expressions: \n" + exprCorpus + expr)
+      context.reporter.debug("Common Tree: \n" + bestTree)
+      context.reporter.debug("---------------------")
+    }
+
+    (score, " (" + bestTree.size + ")")
+  }
+
+
+  /**
+    * Define whether a pair of expressions worth be combined (i.e its score is above 0.0%)
+    * This is kind of a local optimization, instead of creating all possibles trees (what would be enormous).
+    * The threshold can be modified.
+    *
+    * @param exprsA
+    * @param exprsB
+    * @return
+    */
+  def pairAndScoreExpr(exprsA: List[Expr], exprsB: List[Expr]): List[Value] = {
+    val pairOfExprs = for {
+      exprA <- exprsA
+      exprB <- exprsB
+      score = computeScore(exprA, exprB)
+      if score > 0.0
+    } yield {
+      Value(exprA, exprB, score)
+    }
+
+    pairOfExprs
+  }
+
+  def possibleRoots(exprA: Expr, exprB: Expr): List[Value] = {
+    val exprsA = collectExpr(exprA)
+    val exprsB = collectExpr(exprB)
+
+    pairAndScoreExpr(exprsA, exprsB)
+  }
+
+  def matchChildren(childrenA: List[Expr], childrenB: List[Expr]): List[Value] =
+    pairAndScoreExpr(childrenA, childrenB)
+
+
+  /**
+    * With a pair of roots, find all children and find all combination of matching children in order to create a list
+    * of all possible matching tree. Then recursively call itself on each pair of children.
+    *
+    * @param value of root
+    * @return ether a Leaf or a List of all possible similar trees starting with this pair of roots
+    */
+  def possibleTrees(value: Value): List[FuncTree[Value]] = {
+    val exprA = value.a
+    val exprB = value.b
+    val childrenA = getChildren(exprA)
+    val childrenB = getChildren(exprB)
+
+
+    val pairOfMatchingChildren = matchChildren(childrenA, childrenB)
+    val combinationOfChildren = combineChildren(pairOfMatchingChildren)
+
+
+    if (pairOfMatchingChildren.isEmpty) {
+      List(FuncTree(value, List()))
+    } else {
+      combinationOfChildren.foldLeft(List(): List[FuncTree[Value]])(
+        (listOfTrees, children) => listOfTrees ++ flatCombination(value, children.map(p => possibleTrees(p)))
+      )
+    }
+  }
+
+
+  /**
+    * Distributes score computation according to expressions
+    *
+    * Allow some flexibilities, we can even compare two different expressions and give it a non-zero score.
+    * We can also go though some expression to compare deeper proprieties, like:
+    * - order in if-else statement (TO DO)
+    * - exclusiveness of MatchCases in a case-match statement (TO DO)
+    * - value of the expression
+    * - ...
+    *
+    * @param exprA
+    * @param exprB
+    * @return
+    */
+  def computeScore(exprA: Expr, exprB: Expr): Double = (exprA, exprB) match {
+    case (x, y: Choose) => 0.1
+    case (x: MatchExpr, y: MatchExpr) => scoreMatchExpr(x, y)
+    case (x: CaseClass, y: CaseClass) => scoreCaseClass(x, y)
+    case (x, y) if x.getClass == y.getClass =>
+      1.0
+    case _ => 0.0
+  }
+
+
+  /** All possible combination of pairs of children, given the condition that one child can only be used once.
+    *
+    * @param pairs
+    * @return
+    */
+  def combineChildren(pairs: List[Value]): List[List[Value]] = {
+    combine(pairs).filterNot(p => isSameChildUsedTwice(p)).toList
+  }
+
+  def isSameChildUsedTwice(list: List[Value]): Boolean = {
+    list.map(_.a).distinct.size != list.size ||
+      list.map(_.b).distinct.size != list.size
+  }
+
+  def combine[T](in: List[T]): Seq[List[T]] = {
+    for {
+      len <- 1 to in.length
+      combinations <- in combinations len
+    } yield combinations
+  }
+
+
+  /**
+    * Intuition: As we recursively call the method, children will create list of possibilities, as the root does.
+    * All this possible combination need to be transformed into a list of complete tree.
+    *
+    * Technical: we have a combination of Children that return each a list of possible trees. So the upper-level tree
+    * (whom root is named pair) can have all possible combination of theses lists as children.
+    *
+    * @param value of root, in our case type is : (Expr, Expr, Double) i.e.
+    * @param listChildren
+    * @return
+    */
+  def flatCombination[T](value: T, listChildren: List[List[FuncTree[T]]]): List[FuncTree[T]] = {
+    def combine(list: List[List[FuncTree[T]]]): List[List[FuncTree[T]]] = list match {
+      case Nil => List(Nil)
+      case x :: xs =>
+        for {
+          j <- combine(xs)
+          i <- x
+        } yield i :: j
+    }
+
+    combine(listChildren).map(children => FuncTree(value, children))
+  }
+
+  /**
+    * Normalize a score of the tree
+    *
+    * Must pay attention to the fact that small trees will always be chosen. To balance that: consider the size of the
+    * tree and the size of the compared expression to create a "weight".
+    *
+    * @param tree
+    * @return
+    */
+
+  def normalizedScoreTree(tree: FuncTree[Value], exprA: Expr, exprB: Expr): Double = {
+    val scoreTree = geometricMean(tree)
+    val sizeA = collectExpr(exprA).size.toDouble
+    val sizeB = collectExpr(exprB).size.toDouble
+    val weight = (1 / Math.max(sizeA, sizeB)) * tree.size.toDouble
+
+    scoreTree * weight
+  }
+
+  def geometricMean(tree: FuncTree[Value]): Double =
+    Math.pow(tree.toList.foldLeft(1.0)((acc, tree) => acc * tree.score), 1 / tree.size.toDouble)
+
+  def selectBestTree(trees: List[FuncTree[Value]], exprCorpus: Expr, expr: Expr) = {
+    val biggest = trees.sortBy(t => -normalizedScoreTree(t, exprCorpus, expr)).head
+    val score = normalizedScoreTree(biggest, exprCorpus, expr)
+    (biggest, score)
+  }
+
+
+}
diff --git a/src/main/scala/leon/comparison/ComparatorExprList.scala b/src/main/scala/leon/comparison/ComparatorExprList.scala
new file mode 100644
index 000000000..36c9144e4
--- /dev/null
+++ b/src/main/scala/leon/comparison/ComparatorExprList.scala
@@ -0,0 +1,92 @@
+package leon.comparison
+
+import leon.{GlobalOptions, LeonContext, utils}
+import leon.comparison.Utils._
+import leon.purescala.Expressions.{CaseClassPattern, _}
+
+/**
+  * Created by joachimmuth on 25.04.16.
+  *
+  * This way of basic comparison flat both functional trees into lists and compare them in every possible combination.
+  *
+  * The easy-to-understand way of working provides a point of comparison for further advanced method.
+  *
+  * For clarity, we always pass "corpus function" first in argument
+  */
+object ComparatorExprList extends Comparator {
+  val name = "ExprList"
+
+  def compare(exprCorpus: Expr, expr: Expr)(implicit context: LeonContext) = {
+    implicit val debugSection = utils.DebugSectionComparison
+    val exprsA = collectExpr(exprCorpus)
+    val exprsB = collectExpr(expr)
+
+    val numberOfSimilarExpr: Int = pairsOfSimilarExp(exprsA, exprsB)
+
+    val score = Utils.matchScore(numberOfSimilarExpr, exprsA.size, exprsB.size)
+
+    if (context.findOption(GlobalOptions.optDebug).isDefined) {
+      context.reporter.debug("---------------------")
+      context.reporter.debug("COMPARATOR " + name)
+      context.reporter.debug("Expressions: \n" + exprCorpus + "\n" + expr)
+      context.reporter.debug("similar expr: \n" + numberOfSimilarExpr)
+      context.reporter.debug("---------------------")
+    }
+
+    (score, "")
+  }
+
+
+  def pairsOfSimilarExp(exprsCorpus: List[Expr], exprs: List[Expr]): Int = {
+    val normalizedExprsA = exprsCorpus.map(normalizeStructure(_))
+    val normalizedExprsB = exprs.map(normalizeStructure(_))
+
+    normalizedExprsA.intersect(normalizedExprsB).size
+  }
+
+
+  /**
+    * TO BE DELETED ???
+    * --> used in ScoreTree method ???
+    *
+    * Extract a map from a PatternMatch function (match...case) in order to be comparable without caring about the
+    * order
+    * (waring: this comparison make sense only if the MatchCases are exclusives)
+    *
+    * e.g : list match {
+    * case x::y::xs => foo(x, y) ++ recursion(xs)
+    * case x::xs => Nil
+    * }
+    *
+    * is not equal to:
+    *
+    * list match {
+    * case x::xs => Nil
+    * case x::y::xs => foo(x, y) ++ recursion(xs)
+    * }
+    *
+    * @param matchCases
+    * @return
+    */
+  def extractPatternMatchMap(matchCases: Seq[MatchCase]) = {
+    matchCases.map(a => a.pattern match {
+      case InstanceOfPattern(_, ct) => (ct.classDef -> a.rhs)
+      case CaseClassPattern(_, ct, _) => (ct.classDef -> a.rhs)
+      case _ => (a.pattern -> a.rhs)
+    }).toMap
+  }
+
+
+  def extractValueMatchMap(matchCases: Seq[MatchCase]) = {
+    matchCases.map(a => a.pattern -> a.rhs).toMap
+  }
+
+  // IDEE: comparer les types plutôt que les pattern complet des match case, et éventuellement oublié les optGuard
+  def compareExpr(exprA: Expr, exprB: Expr): Boolean = {
+    val normalizedExprA = normalizeStructure(exprA)
+    val normalizedExprB = normalizeStructure(exprB)
+
+    normalizedExprA == normalizedExprB
+  }
+
+}
diff --git a/src/main/scala/leon/comparison/ComparatorScoreTree.scala b/src/main/scala/leon/comparison/ComparatorScoreTree.scala
new file mode 100644
index 000000000..bf8dcb108
--- /dev/null
+++ b/src/main/scala/leon/comparison/ComparatorScoreTree.scala
@@ -0,0 +1,213 @@
+package leon.comparison
+
+import leon.{GlobalOptions, LeonContext, utils}
+import leon.comparison.Utils._
+import leon.purescala.Common.Tree
+import leon.purescala.Definitions.{CaseClassDef, ClassDef}
+import leon.purescala.Expressions._
+import leon.purescala.Types.{ClassType, TypeTree}
+
+/**
+  * Created by joachimmuth on 19.05.16.
+  *
+  * This give a score to the biggest common tree found by ClassTree.
+  * A common tree is composed by pair of expression (A, B) which have the same type, but are maybe not perfectly
+  * equivalent.
+  *
+  * ScoreTree take each pair and compute a score for it, then make a geometrical mean over all these scores.
+  * (The mean "balances" the fact that a big tree will always have a poorer score than a little)
+  *
+  * IMPORTANT: ScoreTree scores an already chosen common Tree, coming from ComparatorClassTree. A frequent 100% score
+  * doesn't mean that FunDef match at 100%, but that the elements of this common Tree match at 100%
+  *
+  */
+object ComparatorScoreTree extends Comparator {
+  override val name: String = "ScoreTree"
+
+  def compare(exprCorpus: Expr, expr: Expr)(implicit context: LeonContext): (Double, String) = {
+    implicit val debugSection = utils.DebugSectionComparison
+    val pairOfRoots = ComparatorClassTree.possibleRoots(exprCorpus, expr)
+    val allPossibleTrees = pairOfRoots flatMap ComparatorClassTree.possibleTrees
+    if (allPossibleTrees == Nil) return (0.0, "")
+
+    val biggest = allPossibleTrees.sortBy(-_.size).head
+    val score: Double = computeScore(biggest)
+    val normalizedScore = normalize(score, biggest.size)
+
+    if (context.findOption(GlobalOptions.optDebug).isDefined) {
+      context.reporter.debug("---------------------")
+      context.reporter.debug("COMPARATOR " + name)
+      context.reporter.debug("Expressions: \n" + exprCorpus + "\n" + expr)
+      context.reporter.debug("Biggest: \n" + biggest)
+      context.reporter.debug("Score: \n" + score)
+      context.reporter.debug("---------------------")
+    }
+
+    (normalizedScore, "")
+  }
+
+  /**
+    * Geometric mean of obtained score, to balance the difference between small and big tree.
+    *
+    * @param score
+    * @param n : size of tree
+    * @return
+    */
+  def normalize(score: Double, n: Int) = Math.pow(score, 1 / n.toDouble)
+
+
+  /**
+    * Give a score to each pair of expression. In combination with "normalize" function, do a Geometric Mean on this
+    * score. They all have the same weight.
+    *
+    * @param tree
+    * @return
+    */
+  def computeScore(tree: FuncTree[(Expr, Expr)]): Double = {
+    // we treat each type differently with its proper scorer
+    val score = tree.value match {
+      case (x: MatchExpr, y: MatchExpr) => scoreMatchExpr(x, y)
+      case (x: CaseClass, y: CaseClass) => scoreCaseClass(x, y)
+      case _ => 1.0
+
+    }
+
+    // if tree is a node, recursively travers children. If it is a leaf, just return the score
+    // we process a geometrical mean
+    tree.children.foldLeft(score)((acc, child) => acc * computeScore(child))
+  }
+
+  /**
+    * Compare only the MatchCases conditions
+    *
+    * @return
+    */
+  def scoreMatchExpr(x: MatchExpr, y: MatchExpr): Double = {
+    def scoreMatchCase(casesA: Seq[MatchCase], casesB: Seq[MatchCase]): Double = {
+      val mapCasesA = toMap(casesA)
+      val mapCasesB = toMap(casesB)
+      scoreMapMatchCase(mapCasesA, mapCasesB)
+    }
+
+    /**
+      * Compare the map containing the MatchCases
+      * NOW: just check how many similar key they have
+      * NEXT: take into account the order; some MatchCase can be non exclusive, meaning that it "eats" the next one:
+      * case x if x < 4 => ...
+      * case x if x < 10 => ...
+      * doesn't have the same meaning if inverted.
+      *
+      * NEXT: take into account invoked expression
+      *
+      * @param mapCasesA
+      * @param mapCasesB
+      * @return
+      */
+    def scoreMapMatchCase(mapCasesA: Map[Tree, Expr], mapCasesB: Map[Tree, Expr]): Double = {
+      val all = mapCasesA.keys.size + mapCasesB.keys.size.toDouble
+      val diff = ((mapCasesA.keySet -- mapCasesB.keySet) ++ (mapCasesB.keySet -- mapCasesA.keySet)).size.toDouble
+      (all - diff) / all
+    }
+
+    def toMap(cases: Seq[MatchCase]) = {
+      cases.map(a => a.pattern match {
+        case InstanceOfPattern(_, ct) => ct -> a.rhs
+        case CaseClassPattern(_, ct, _) => ct -> a.rhs
+        case _ => a.pattern -> a.rhs
+      }).toMap
+    }
+
+    scoreMatchCase(x.cases, y.cases)
+  }
+
+
+  /**
+    * One hard piece is to compare two case clase, because it cannot be normalized like value
+    *
+    * @return
+    */
+
+  def scoreClassDef(classA: ClassDef, classB: ClassDef): Double = {
+    (classA, classB) match {
+      case (a, b) if (a.isAbstract && b.isAbstract) =>
+        if (a.knownCCDescendants.size == b.knownCCDescendants.size) 1.0
+        else 0.0
+      case (a: CaseClassDef, b: CaseClassDef) =>
+        scoreCaseClassDef(a, b)
+      case _ => 0.0
+
+    }
+  }
+
+  def compareTypeTree(typeA: TypeTree, typeB: TypeTree): Double = (typeA, typeB) match {
+    case (a: ClassType, b: ClassType) => scoreClassDef(a.classDef, b.classDef)
+    case _ => 0.0
+  }
+
+  def scoreCaseClass(a: CaseClass, b: CaseClass): Double = {
+    scoreCaseClassDef(a.ct.classDef, b.ct.classDef)
+  }
+
+
+  /**
+    * Compare two CaseClass definition taking into account different parameter:
+    * - the number of arguments of it's own type
+    * - the number of arguments of it's parent type
+    * - the other arguments of primitive types
+    *
+    * NEXT: take into account matching between parents
+    * NEXT: take into account others parameters ?
+    *
+    * @param a
+    * @param b
+    * @return
+    */
+  def scoreCaseClassDef(a: CaseClassDef, b: CaseClassDef): Double = {
+    val ownTypeA: Int = argumentsOfOwnType(a)
+    val ownTypeB: Int = argumentsOfOwnType(b)
+    val scoreOwnType = percent(ownTypeA, ownTypeB)
+
+    val parentTypeA: Int = argumentsOfParentType(a)
+    val parentTypeB: Int = argumentsOfParentType(b)
+    val scoreParentType = percent(parentTypeA, parentTypeB)
+
+    val otherTypeA = a.fields.map(_.getType).filterNot(_.isInstanceOf[ClassDef])
+    val otherTypeB = b.fields.map(_.getType).filterNot(_.isInstanceOf[ClassDef])
+    val scoreOtherType = scoreSeqType(otherTypeA, otherTypeB)
+
+    // arithmetic mean instead of geometric, we don't want to have 0.0% if one of these criteria don't match
+    val score: Double = mean(List(scoreOwnType, scoreParentType, scoreOtherType))
+
+    score
+  }
+
+
+  def scoreSeqType(a: Seq[TypeTree], b: Seq[TypeTree]): Double = {
+    val intersect = a.intersect(b).size
+    matchScore(intersect, a.size, b.size)
+  }
+
+  /**
+    * Count how many occurrences of its own type appear in its arguments
+    * (to be improved if multiples types)
+    *
+    * @param a the case class
+    * @return
+    */
+  def argumentsOfOwnType(a: CaseClassDef): Int =
+    a.fields.map(_.getType).count(a.tparams.map(_.tp.getType).contains(_))
+
+
+  /**
+    * Count how many occurrences of its parent type appear in its arguments
+    *
+    * @param a
+    * @return
+    */
+  def argumentsOfParentType(a: CaseClassDef): Int = a match {
+    case _ if a.hasParent => a.fields.map(_.getType).count(_ == a.parent.get.getType)
+    case _ => 0
+  }
+
+
+}
diff --git a/src/main/scala/leon/comparison/ComparisonCorpus.scala b/src/main/scala/leon/comparison/ComparisonCorpus.scala
new file mode 100644
index 000000000..2af98860c
--- /dev/null
+++ b/src/main/scala/leon/comparison/ComparisonCorpus.scala
@@ -0,0 +1,55 @@
+package leon.comparison
+
+import java.io.File
+import java.nio.file.{Paths, Files}
+
+import leon.LeonContext
+import leon.frontends.scalac.ExtractionPhase
+import leon.purescala.Definitions.{FunDef, Program}
+import leon.utils.PreprocessingPhase
+
+
+/**
+  * Created by joachimmuth on 24.03.16.
+  *
+  * Extract list of all FunDef existing in the objects of the targeted folder.
+  * Typically the folder is "comparison-base" (chosen in ComparisonPhase).
+  */
+case class ComparisonCorpus(ctx: LeonContext, folder: String) {
+
+  val program: Program = extraction(recursiveListFilesInString(folder))
+  val funDefs: List[FunDef] = ComparisonPhase.getFunDef(ctx, program)
+
+  def extraction(files: List[String]): _root_.leon.purescala.Definitions.Program = {
+    val extraction = ExtractionPhase andThen new PreprocessingPhase(false)
+    val (_, prog) = extraction.run(ctx, files)
+    prog
+  }
+
+  def recursiveListFiles(f: File): List[File] = {
+    if (!(f.isDirectory || f.isFile)) {
+      ctx.reporter.error("Path " + f + " is neither a file nor a directory.")
+      ctx.reporter.error("Program aborted")
+      java.lang.System.exit(0)
+    }
+
+    if (f.isDirectory) {
+      val (files, dirs) = f.listFiles().toList.partition(_.isFile)
+      files ++ dirs.filter(_.isDirectory).flatMap(recursiveListFiles)
+    } else {
+      List(f)
+    }
+  }
+
+  def recursiveListFilesInString(f: String): List[String] = {
+    if (!Files.exists(Paths.get(f))) {
+      ctx.reporter.error("Path of corpus folder doesn't exist: " + f)
+      ctx.reporter.error("Program aborted")
+      java.lang.System.exit(0)
+    }
+    val file = new File(f)
+    recursiveListFiles(file).map(f => f.getCanonicalPath)
+  }
+
+
+}
diff --git a/src/main/scala/leon/comparison/ComparisonPhase.scala b/src/main/scala/leon/comparison/ComparisonPhase.scala
new file mode 100644
index 000000000..116abb34d
--- /dev/null
+++ b/src/main/scala/leon/comparison/ComparisonPhase.scala
@@ -0,0 +1,101 @@
+package leon
+package comparison
+
+import leon.purescala.Definitions._
+import leon.purescala.Expressions._
+import leon.comparison.Utils._
+import leon.utils.DebugSection
+
+/**
+  * Created by joachimmuth on 23.03.16.
+  */
+object ComparisonPhase extends SimpleLeonPhase[Program, ComparisonReport] {
+
+  override val description: String = "Comparison phase between input program and Leon example suite"
+  override val name: String = "Comparison"
+
+  val comparators: List[Comparator] = List(
+    ComparatorExprList,
+    ComparatorClassList,
+    ComparatorClassTree,
+    ComparatorScoreTree,
+    ComparatorDirectScoreTree
+  )
+
+  val comparatorsNames = comparators map (_.name)
+
+  override def apply(ctx: LeonContext, program: Program): ComparisonReport = {
+    implicit val context = ctx
+
+
+    val corpus = ComparisonCorpus(ctx, "testcases/comparison/corpus")
+    val funDefsCorpus = corpus.funDefs
+    val funDefs = getFunDef(ctx, program)
+
+
+    // contain pair of function compared and score given by each comparator
+    // a space is let for a comment string, for example size of common tree for DirectScoreTree comparator
+    val comparison = combinationOfFunDef(funDefsCorpus, funDefs)
+
+    val autocompletedHoles =
+      funDefs filter hasHole map (fun => Completor.suggestCompletion(fun, corpus))
+
+    ComparisonReport(ctx, program, corpus, comparatorsNames, comparison, autocompletedHoles)
+  }
+
+
+  /**
+    * Compare each function from corpus to argument program
+    *
+    * @param funDefsCorpus
+    * @param funDefs
+    * @return
+    */
+  def combinationOfFunDef(funDefsCorpus: List[FunDef], funDefs: List[FunDef])
+                         (implicit context: LeonContext) = {
+
+    for {
+      funDef <- funDefs
+      funDefCorpus <- funDefsCorpus
+      scores = comparators map (_.compare(funDefCorpus.body.get, funDef.body.get))
+      if scores.map(_._1) exists (_ > 0.0)
+    } yield {
+      (funDef, funDefCorpus, scores)
+    }
+  }
+
+  /**
+    * Method inspired from VerficationPhase
+    * A filter with undesirable FunDef added
+    * Ensure that every FunDef has a body
+    *
+    * @param ctx
+    * @param program
+    * @return
+    */
+  def getFunDef(ctx: LeonContext, program: Program): List[FunDef] = {
+    def excludeByDefault(fd: FunDef): Boolean = fd.annotations contains "library"
+    val filterFuns: Option[Seq[String]] = ctx.findOption(GlobalOptions.optFunctions)
+    val fdFilter = {
+      import OptionsHelpers._
+
+      filterInclusive(filterFuns.map(fdMatcher(program)), Some(excludeByDefault _))
+    }
+
+    val funDefs = program.definedFunctions.filter(fdFilter).sortWith((fd1, fd2) => fd1.getPos < fd2.getPos).tail
+
+    funDefs filter { f =>
+      f.qualifiedName(program) != "Ensuring.ensuring" &&
+        f.qualifiedName(program) != "WebPage.apply" &&
+        f.qualifiedName(program) != "Style" &&
+        hasBody(f)
+    }
+  }
+
+  def hasBody(funDef: FunDef): Boolean = funDef.body match {
+    case Some(b) => true
+    case None => false
+  }
+
+
+}
diff --git a/src/main/scala/leon/comparison/ComparisonReport.scala b/src/main/scala/leon/comparison/ComparisonReport.scala
new file mode 100644
index 000000000..31515d7c6
--- /dev/null
+++ b/src/main/scala/leon/comparison/ComparisonReport.scala
@@ -0,0 +1,126 @@
+package leon.comparison
+
+import leon.LeonContext
+import leon.purescala.Definitions.{FunDef, Program}
+import leon.purescala.Expressions.Expr
+import leon.utils.ASCIIHelpers._
+import leon.utils.Report
+
+import scala.reflect.quasiquotes.Holes
+
+/**
+  * Created by joachimmuth on 23.03.16.
+  *
+  */
+case class ComparisonReport(
+                             ctx: LeonContext,
+                             program: Program,
+                             base: ComparisonCorpus,
+                             comparatorsName: List[String],
+                             listFD: List[(FunDef, FunDef, List[(Double, String)])],
+                             holes: List[(FunDef, Option[FunDef], Option[Expr])]) extends Report {
+
+
+  def summaryString: String = {
+
+    // some information about the rendered table
+    //    ctx.reporter.info("argument program: name of compared function and its size")
+    //    ctx.reporter.info("base: name of function extracted from our corpus and its size")
+    //    ctx.reporter.info("ExprList: compare each expression subtree one by one and count number of exact match" +
+    //    "compared with total number of expression in both function")
+    //    ctx.reporter.info("ClassList: compare each type of expressions one by one and count number of exact" +
+    //    "match compared with total number of expression in both functions")
+    //    ctx.reporter.info("ClassTree: Find the biggest common tree based on type of expression, and count its size" +
+    //    "compared with size of both functions")
+    //    ctx.reporter.info("ScoreTree: Compute a score for the found ClassTree")
+    //    ctx.reporter.info("DirectScoreTree: Find the biggest common tree based directly on a score method, and give the" +
+    //    "score next to the size of both function and the size of the tree.")
+
+
+    // report table
+    var t = Table("Comparison Summary")
+
+    t += Row(
+      Seq(
+        Cell("argument program"),
+        Cell("size"),
+        Cell("base"),
+        Cell("size")
+      ) ++
+        comparatorsName.map(p => Cell(p))
+    )
+
+    t += Separator
+
+    t ++= listFD.map(
+      fd => Row(
+        Seq(
+          Cell(fd._1.qualifiedName(program)),
+          Cell(size(fd._1)),
+          Cell(fd._2.qualifiedName(base.program)),
+          Cell(size(fd._2))
+        ) ++
+          fd._3.map(p => Cell(percentage(p._1) + " " + p._2))
+      )
+    )
+
+    val warningScoreTree: String = "IMPORTANT: ScoreTree scores an already chosen common Tree, coming" +
+      " from ComparatorClassTree (i.e. the biggest). \n" +
+      "A frequent 100% score does not mean that FunDef match at 100%, " +
+      "but that the elements of this common Tree match at 100% \n"
+
+    val noteParenthesis: String = "NOTE: In parenthesis are the sizes of trees and the size of common trees in case of" +
+      "DirectScore"
+
+
+    // report completion holes
+    var stringHole: String = ""
+
+    if (holes.nonEmpty) {
+      var reportHoles: Table = Table("Completion of Holes")
+
+      reportHoles += Row(Seq(
+        Cell("Incomplete function"),
+        Cell("Corpus function used to complete it")
+      ))
+
+      reportHoles += Separator
+
+      reportHoles ++= holes.map(
+        h => Row(Seq(
+          Cell(h._1.qualifiedName(program)),
+          Cell(handleOptionFD(h._2, base.program))
+        ))
+      )
+
+      stringHole += reportHoles.render + "\n"
+      stringHole += holes.map(p => printFilledHoles(p._1, p._3)).mkString("")
+    }
+
+    t.render + "\n" + warningScoreTree + "\n" + stringHole
+  }
+
+  private def percentage(d: Double): String = new java.text.DecimalFormat("#.##").format(d * 100) ++ "%"
+
+  private def size(f: FunDef): String = "(" + Utils.collectExpr(f.body.get).size + ")"
+
+  def handleOptionFD(f: Option[FunDef], program: Program): String = f match {
+    case Some(funDef) => funDef.qualifiedName(program)
+    case None => "no matching funDef found"
+  }
+
+  def printFilledHoles(incompleteFun: FunDef, completedExpr: Option[Expr]): String = completedExpr match {
+    case None => ""
+    case Some(expr) =>
+      "\n================================================\n" +
+        "Incomplete function " + incompleteFun.qualifiedName(program) + " was:\n" +
+        "================================================\n" +
+        incompleteFun.body.get.toString + "\n" +
+        "==============================\n" +
+        "Function is now completed as :\n" +
+        "==============================\n" +
+        expr.toString + "\n"
+  }
+
+
+}
diff --git a/src/main/scala/leon/comparison/Completor.scala b/src/main/scala/leon/comparison/Completor.scala
new file mode 100644
index 000000000..d98bd01e3
--- /dev/null
+++ b/src/main/scala/leon/comparison/Completor.scala
@@ -0,0 +1,138 @@
+package leon.comparison
+
+import leon.LeonContext
+import leon.purescala.Definitions.FunDef
+import leon.purescala.Expressions._
+import leon.comparison.Utils._
+import leon.comparison.ComparatorDirectScoreTree._
+import leon.purescala.ExprOps
+
+/**
+  * Created by joachimmuth on 08.06.16.
+  *
+  * Consider a holed function and try to find the best match (if there is some!) between this and one of the function
+  * existing in the corpus.
+  *
+  * To do so, we use a similar method as ComparatorDirectScoreTree were we create all possible common tree shared by
+  * two functions. As ComparatorDirectScoreTree creates pair of expression based on their score, we only need to do a
+  * little modification in order to consider the Hole as a possible match, based on their type.
+  * We choose then the function with the common tree having the higher score.
+  *
+  * We use this corpus function to fill the hole, and we replace the hole by the matching expression in the common tree.
+  *
+  * We return the holed function, the corpus function used to complete it, and the completed function (if there is some).
+  *
+  * IMPORTANT: at the moment the object if implemented to handle one and only one hole
+  */
+object Completor {
+
+  case class Suggestion(expr: Option[Expr])
+
+
+  def suggestCompletion(funDef: FunDef, corpus: ComparisonCorpus)(implicit context: LeonContext):
+  (FunDef, Option[FunDef], Option[Expr]) = {
+    val expr = funDef.body.get
+
+    // for each function of corpus, search all roots of common tree that include the hole
+    val funDefAndRoots = corpus.funDefs map (f => (f, possibleRootsWithHoles(f, expr)))
+
+    // for each function of corpus, search all common tree respective to these roots
+    // (filter only the ones containing the hole)
+    val funDefAndTrees = funDefAndRoots map { p =>
+      (p._1, p._2 flatMap possibleTrees filter hasHole)
+    }
+
+    // if no function match, return None
+    if (funDefAndTrees.isEmpty)
+      return (funDef, None, None)
+
+    val suggestion = selectBestSuggestion(expr, funDefAndTrees)
+
+    suggestion match {
+      case None => (funDef, None, None)
+      case Some(pair) => (funDef, Some(pair._1), Some(fillHole(expr, pair._2)))
+    }
+  }
+
+
+  def possibleRootsWithHoles(funDefCorpus: FunDef, expr: Expr): List[Value] =
+    possibleRoots(funDefCorpus.body.get, expr) filter (e => Utils.hasHole(e.b))
+
+  def getBody(funDef: FunDef): Expr = funDef.body.get
+
+  def hasHole(tree: FuncTree[Value]): Boolean = {
+    tree.toList map (p => p.b) exists (e => e.isInstanceOf[Choose])
+  }
+
+
+  /**
+    * select the best suggestion to fill the hole i.e. the common tree having the higher score between all the common
+    * trees and all the function of corpus
+    *
+    * @param funDefAndTrees
+    * @return
+    */
+  def selectBestSuggestion(expr: Expr, funDefAndTrees: List[(FunDef, List[FuncTree[Value]])]):
+  Option[(FunDef, Expr)] = {
+    val funDefAndBestTree = funDefAndTrees map { p =>
+      (p._1, selectBestTreeOption(p._2, expr, getBody(p._1)))
+    }
+
+    selectBestFun(funDefAndBestTree) match {
+      case None => None
+      case Some(pair) => Some(pair._1, findPairOfTheHole(pair._2))
+    }
+  }
+
+  def selectBestTreeOption(list: List[FuncTree[Value]], exprA: Expr, exprB: Expr): Option[(FuncTree[Value], Double)] = list match {
+    case Nil => None
+    case x :: xs => Some(selectBestTree(list, exprA, exprB))
+  }
+
+  def selectBestFun(list: List[(FunDef, Option[(FuncTree[Value], Double)])]): Option[(FunDef, FuncTree[Value])] = {
+    val listWithScore = list filterNot (p => p._2.isEmpty)
+
+    listWithScore match {
+      case Nil => None
+      case x :: xs => {
+        val best = listWithScore.sortBy(p => -p._2.get._2).head
+        Some(best._1, best._2.get._1)
+      }
+    }
+  }
+
+  def scoreOptionTree(tree: Option[FuncTree[Value]]): Double = tree match {
+    case None => 0.0
+    case Some(t) => geometricMean(t)
+  }
+
+
+  /**
+    * Find in common tree the value that paired the hole and the expression from the corpus. The hole will be filled
+    * with this hole
+    *
+    * @param tree
+    * @return
+    */
+  def findPairOfTheHole(tree: FuncTree[Value]): Expr =
+    (tree.toList filter (p => p.b.isInstanceOf[Choose])).head.a
+
+  /**
+    * Travers recursively the tree until finding the hole and replace it by
+    * the wished expression.
+    *
+    * @param exprToFill
+    * @param corpus
+    * @return
+    */
+  def fillHole(exprToFill: Expr, corpus: Expr): Expr = {
+    val filledTree = ExprOps.preMap {
+      case Choose(expr) => Some(corpus)
+      case _ => None
+    }(exprToFill)
+
+    filledTree
+  }
+
+
+}
diff --git a/src/main/scala/leon/comparison/FuncTree.scala b/src/main/scala/leon/comparison/FuncTree.scala
new file mode 100644
index 000000000..0d7744cca
--- /dev/null
+++ b/src/main/scala/leon/comparison/FuncTree.scala
@@ -0,0 +1,17 @@
+package leon.comparison
+
+/**
+  * Created by joachimmuth on 12.05.16.
+  *
+  * Basic class just to allow easy store of expressions-tree
+  */
+
+case class FuncTree[T](value: T, children: List[FuncTree[T]]) {
+  def isLeaf: Boolean = children.isEmpty
+
+  def isNode: Boolean = !isLeaf
+
+  def size: Int = 1 + children.foldLeft(0)((acc, child) => acc + child.size)
+
+  def toList: List[T] = value +: children.flatMap(child => child.toList)
+}
diff --git a/src/main/scala/leon/comparison/Scores.scala b/src/main/scala/leon/comparison/Scores.scala
new file mode 100644
index 000000000..4dfea3bc4
--- /dev/null
+++ b/src/main/scala/leon/comparison/Scores.scala
@@ -0,0 +1,150 @@
+package leon.comparison
+
+import leon.comparison.Utils._
+import leon.purescala.Common.Tree
+import leon.purescala.Definitions.{CaseClassDef, ClassDef}
+import leon.purescala.Expressions.{CaseClassPattern, _}
+import leon.purescala.Types.{ClassType, TypeTree}
+
+/**
+  * Created by joachimmuth on 02.06.16.
+  *
+  * This object contains all the scoring method to handle different cases
+  */
+object Scores {
+
+  /**
+    * compare only the MatchCases conditions, not the returned value, which are compared through main compareExp
+    * function
+    *
+    * @return
+    */
+  def scoreMatchExpr(x: MatchExpr, y: MatchExpr): Double = {
+    def scoreMatchCase(casesB: Seq[MatchCase], cases: Seq[MatchCase]): Double = {
+      val mapCasesB = toMap(casesB)
+      val mapCases = toMap(cases)
+      scoreMapMatchCase(mapCasesB, mapCases)
+    }
+
+    /**
+      * Compare the map containing the MatchCases
+      * NOW: just check how many similar key they have
+      * NEXT: take into account the order; some MatchCase can be non exclusive, meaning that it "eats" the next one:
+      * case x if x < 4 => ...
+      * case x if x < 10 => ...
+      * doesn't have the same meaning if inverted.
+      *
+      * NEXT: take into account invoked expression
+      *
+      * @param mapCasesB
+      * @param mapCases
+      * @return
+      */
+    def scoreMapMatchCase(mapCasesB: Map[Tree, Expr], mapCases: Map[Tree, Expr]): Double = {
+      val all = mapCasesB.keys.size + mapCases.keys.size.toDouble
+      val diff = ((mapCasesB.keySet -- mapCases.keySet) ++ (mapCases.keySet -- mapCasesB.keySet)).size.toDouble
+      (all - diff) / all
+    }
+
+    def toMap(cases: Seq[MatchCase]) = {
+      cases.map(a => a.pattern match {
+        case InstanceOfPattern(_, ct) => ct -> a.rhs
+        case CaseClassPattern(_, ct, _) => ct -> a.rhs
+        case _ => a.pattern -> a.rhs
+      }).toMap
+    }
+
+    scoreMatchCase(x.cases, y.cases)
+  }
+
+
+  /**
+    * One hard piece is to compare two case clase, because it cannot be normalized like value
+    *
+    * @return
+    */
+
+  def scoreClassDef(classA: ClassDef, classB: ClassDef): Double = {
+    (classA, classB) match {
+      case (a, b) if (a.isAbstract && b.isAbstract) =>
+        if (a.knownCCDescendants.size == b.knownCCDescendants.size) 1.0
+        else 0.0
+      case (a: CaseClassDef, b: CaseClassDef) =>
+        scoreCaseClassDef(a, b)
+      case _ => 0.0
+
+    }
+  }
+
+  def compareTypeTree(typeA: TypeTree, typeB: TypeTree): Double = (typeA, typeB) match {
+    case (a: ClassType, b: ClassType) => scoreClassDef(a.classDef, b.classDef)
+    case _ => 0.0
+  }
+
+  def scoreCaseClass(a: CaseClass, b: CaseClass): Double = {
+    scoreCaseClassDef(a.ct.classDef, b.ct.classDef)
+  }
+
+
+  /**
+    * Compare two CaseClass definition taking into account different parameter:
+    * - the number of arguments of it's own type
+    * - the number of arguments of it's parent type
+    * - the other arguments of primitive types
+    *
+    * NEXT: take into account matching between parents
+    * NEXT: take into account others parameters ?
+    *
+    * @param a
+    * @param b
+    * @return
+    */
+  def scoreCaseClassDef(a: CaseClassDef, b: CaseClassDef): Double = {
+    val ownTypeA: Int = argumentsOfOwnType(a)
+    val ownTypeB: Int = argumentsOfOwnType(b)
+    val scoreOwnType = percent(ownTypeA, ownTypeB)
+
+    val parentTypeA: Int = argumentsOfParentType(a)
+    val parentTypeB: Int = argumentsOfParentType(b)
+    val scoreParentType = percent(parentTypeA, parentTypeB)
+
+    val otherTypeA = a.fields.map(_.getType).filterNot(_.isInstanceOf[ClassDef])
+    val otherTypeB = b.fields.map(_.getType).filterNot(_.isInstanceOf[ClassDef])
+    val scoreOtherType = scoreSeqType(otherTypeA, otherTypeB)
+
+    // arithmetic mean instead of geometric, we don't want to have 0.0% if one of these criteria don't match
+    val score: Double = mean(List(scoreOwnType, scoreParentType, scoreOtherType))
+
+    score
+  }
+
+
+  def scoreSeqType(a: Seq[TypeTree], b: Seq[TypeTree]): Double = {
+    val intersect = a.intersect(b).size
+    matchScore(intersect, a.size, b.size)
+  }
+
+  /**
+    * Count how many occurrences of its own type appear in its arguments
+    * (to be improved if multiples types)
+    *
+    * @param a the case class
+    * @return
+    */
+  def argumentsOfOwnType(a: CaseClassDef): Int =
+    a.fields.map(_.getType).count(a.tparams.map(_.tp.getType).contains(_))
+
+
+  /**
+    * Count how many occurrences of its parent type appear in its arguments
+    *
+    * @param a
+    * @return
+    */
+  def argumentsOfParentType(a: CaseClassDef): Int = a match {
+    case _ if a.hasParent => a.fields.map(_.getType).count(_ == a.parent.get.getType)
+    case _ => 0
+  }
+
+
+}
diff --git a/src/main/scala/leon/comparison/Utils.scala b/src/main/scala/leon/comparison/Utils.scala
new file mode 100644
index 000000000..2000f0922
--- /dev/null
+++ b/src/main/scala/leon/comparison/Utils.scala
@@ -0,0 +1,243 @@
+package leon.comparison
+
+import leon.purescala.Common.Identifier
+import leon.purescala.Definitions.FunDef
+import leon.purescala.ExprOps
+import leon.purescala.ExprOps._
+import leon.purescala.Expressions._
+
+/**
+  * Created by joachimmuth on 25.04.16.
+  */
+object Utils {
+
+  case class Value(a: Expr, b: Expr, score: Double)
+
+  def hasHole(funDef: FunDef): Boolean =
+    hasHole(funDef.body.get)
+
+  def hasHole(expr: Expr): Boolean =
+    collectExpr(expr) exists (e => e.isInstanceOf[Hole] || e.isInstanceOf[Choose])
+
+  /**
+    * Method to handle update made recently that changed argument and output of ExprOps.normalizeStructure
+    *
+    * @param expr
+    * @return
+    */
+  def normalizeStructure(expr: Expr): Expr = {
+    val allVars: Seq[Identifier] = fold[Seq[Identifier]] {
+      (expr, idSeqs) => idSeqs.foldLeft(expr match {
+        case Lambda(args, _) => args.map(_.id)
+        case Forall(args, _) => args.map(_.id)
+        case LetDef(fds, _) => fds.flatMap(_.paramIds)
+        case Let(i, _, _) => Seq(i)
+        case MatchExpr(_, cses) => cses.flatMap(_.pattern.binders)
+        case Passes(_, _, cses) => cses.flatMap(_.pattern.binders)
+        case Variable(id) => Seq(id)
+        case _ => Seq.empty[Identifier]
+      })((acc, seq) => acc ++ seq)
+    }(expr).distinct
+
+    ExprOps.normalizeStructure(allVars, expr)._2
+  }
+
+
+  def percent(a: Int, b: Int): Double = {
+    if (a == 0 && b == 0) 1.0
+    else if (a == 0 || b == 0) 0.0
+    else Math.min(a.toDouble / b.toDouble, b.toDouble / a.toDouble)
+  }
+
+  def matchScore(a: Int, option1: Int, option2: Int): Double =
+    Math.min(percent(a, option1), percent(a, option2))
+
+
+  /**
+    * Arithmetic means
+    */
+  def mean(a: Double): Double = a
+
+  def mean(a: Double, b: Double): Double = (a + b) / 2
+
+  def mean(a: Double, b: Double, c: Double): Double = (a + b + c) / 3
+
+  def mean(a: Double, b: Double, c: Double, d: Double): Double = (a + b + c + d) / 4
+
+  def mean(list: List[Double]): Double = list.foldLeft(0.0)(_ + _) / list.size.toDouble
+
+
+  /**
+    * Use GenTreeOps.fold to travers tree and collect attribute of their expression.
+    *
+    * No use of GenTreeOps.collect because we DO want to preserve duplicate element (GenTreeOps.collect return a
+    * Set, which doesn't)
+    * @param expr
+    * @return
+    */
+  def collectClass(expr: Expr): List[Class[_]] = {
+    val listClass: Seq[Class[_]] = ExprOps.fold{
+      (expr, seq: Seq[Seq[Class[_]]]) => seq.flatten :+ expr.getClass
+    }(expr)
+
+    listClass.toList
+  }
+
+
+  def collectExpr(expr: Expr): List[Expr] = {
+    val listExpr: Seq[Expr] = ExprOps.fold{
+      (expr, seq: Seq[Seq[Expr]]) => seq.flatten :+ expr
+    }(expr)
+
+    listExpr.toList
+  }
+
+  /**
+    * Give a list of all children of one parent. Why do we need to use "traverse" function to get them? Because
+    * there is a lot of possible CaseClass extending Expr, and we want to deal with any of them.
+    *
+    * @param expr
+    * @return
+    */
+  def getChildren(expr: Expr): List[Expr] =
+    traverse(expr)(expr => Nil)(expr => List(expr))
+
+
+  /**
+    * Main function allowing to traverse a tree. This function is made in a way to be the more generic possible,
+    * letting choose how we deal with the parent (the current Expr) and its children.
+    *
+    * The function "collect" derives from it, by choosing "onChild" to be a recursive call.
+    * The function "getChild" also derives from it, by doing nothing with the parent and adding the children to the
+    * list, but without recursion.
+    *
+    * As we can see, this function allow to do a lot of things and can be used in the future to test new configuration
+    *
+    * @param expr     the parent of the tree we want to traverse. Never forget, we use the term "parent" but expr contains
+    *                 all the tree
+    * @param onParent function applied to this parent. It can neglect it (expr => Nil), store it (expr => List(expr))
+    *                 or store one of its parameter (expr => List(expr.getClass))
+    * @param onChild  function applied to the children expression of "expr". It can be recursive (as in "collect"
+    *                 function) or can store some information about it (as in "getChildren)
+    * @tparam T the type of the returned list we want to get after traversing the tree
+    * @return a list containing all the chosen values stored by both function "onParent" and "onChildren"
+    */
+  def traverse[T](expr: Expr)(onParent: Expr => List[T])(onChild: Expr => List[T]): List[T] = expr match {
+    case Require(pred, body) => onParent(expr) ++ onChild(pred) ++ onChild(body)
+    case Ensuring(body, pred) => onParent(expr) ++ onChild(body) ++ onChild(pred)
+    case Assert(pred, _, body) => onParent(expr) ++ onChild(pred) ++ onChild(body)
+    case Let(binder, value, body) => onParent(expr) ++ onChild(value) ++ onChild(body)
+
+    // how to handle fds (function definition) ??
+    case LetDef(fds, body) => onParent(expr) ++ onChild(body)
+
+    case Application(callee, args) => onParent(expr) ++ onChild(callee) ++ args.flatMap(onChild(_))
+    case Lambda(_, body) => onParent(expr) ++ onChild(expr)
+    case Forall(_, body) => onParent(expr) ++ onChild(body)
+    case FunctionInvocation(_, args) =>
+      onParent(expr)
+    case IfExpr(cond, thenn, elze) => onParent(expr) ++ onChild(cond) ++ onChild(thenn) ++ onChild(elze)
+
+    // we don't list the scrutinee
+    // method cases.expression return both optGuard and rhs
+    case MatchExpr(scrutinee, cases) =>
+      onParent(expr) ++ cases.flatMap(m => m.expressions.flatMap(e => onChild(e)))
+
+    case CaseClass(_, args) => onParent(expr) ++ args.flatMap(onChild(_))
+    case CaseClassSelector(_, caseClass, _) =>
+      onParent(expr) ++ onChild(caseClass)
+    case Equals(lhs, rhs) =>
+      onParent(expr) ++ onChild(lhs) ++ onChild(rhs)
+
+    /* Propositional logic */
+    case And(exprs) =>
+      onParent(expr) ++ exprs.flatMap(onChild(_))
+    case Or(exprs) =>
+      onParent(expr) ++ exprs.flatMap(onChild(_))
+    case Implies(lhs, rhs) => onParent(expr) ++ onChild(lhs) ++ onChild(rhs)
+    case Not(argExpr) =>
+      onParent(expr) ++ onChild(argExpr)
+
+    case IsInstanceOf(argExpr, _) =>
+      onParent(expr) ++ onChild(argExpr)
+    case AsInstanceOf(argExpr, _) =>
+      onParent(expr) ++ onChild(argExpr)
+
+    /* Integer arithmetic */
+    case Plus(lhs, rhs) => onParent(expr) ++ onChild(lhs) ++ onChild(rhs)
+    case Minus(lhs, rhs) =>
+      onParent(expr) ++ onChild(lhs) ++ onChild(rhs)
+    case UMinus(argExpr) =>
+      onParent(expr) ++ onChild(argExpr)
+    case Times(lhs, rhs) =>
+      onParent(expr) ++ onChild(lhs) ++ onChild(rhs)
+    case Division(lhs, rhs) => onParent(expr) ++ onChild(lhs) ++ onChild(rhs)
+    case Remainder(lhs, rhs) =>
+      onParent(expr) ++ onChild(lhs) ++ onChild(rhs)
+    case Modulo(lhs, rhs) => onParent(expr) ++ onChild(lhs) ++ onChild(rhs)
+    case GreaterThan(lhs, rhs) =>
+      onParent(expr) ++ onChild(lhs) ++ onChild(rhs)
+    case GreaterEquals(lhs, rhs) => onParent(expr) ++ onChild(lhs) ++ onChild(rhs)
+    case LessThan(lhs, rhs) =>
+      onParent(expr) ++ onChild(lhs) ++ onChild(rhs)
+    case LessEquals(lhs, rhs) =>
+      onParent(expr) ++ onChild(lhs) ++ onChild(rhs)
+
+    /* Real arithmetic */
+    case RealPlus(lhs, rhs) => onParent(expr) ++ onChild(lhs) ++ onChild(rhs)
+    case RealMinus(lhs, rhs) => onParent(expr) ++ onChild(lhs) ++ onChild(rhs)
+    case RealDivision(lhs, rhs) =>
+      onParent(expr) ++ onChild(lhs) ++ onChild(rhs)
+    case RealTimes(lhs, rhs) => onParent(expr) ++ onChild(lhs) ++ onChild(rhs)
+    case RealUMinus(argExpr) =>
+      onParent(expr) ++ onChild(argExpr)
+
+    /* Tuple operations */
+    case Tuple(exprs) => onParent(expr) ++ exprs.flatMap(onChild(_))
+    case TupleSelect(tuple, _) =>
+      onParent(expr) ++ onChild(tuple)
+
+    /* Set operations */
+    case FiniteSet(elements, _) => onParent(expr) ++ elements.flatMap(onChild(_))
+    case ElementOfSet(element, set) =>
+      onParent(expr) ++ onChild(element) ++ onChild(set)
+    case SetCardinality(set) => onParent(expr) ++ onChild(set)
+    case SubsetOf(set1, set2) => onParent(expr) ++ onChild(set1) ++ onChild(set2)
+    case SetIntersection(set1, set2) =>
+      onParent(expr) ++ onChild(set1) ++ onChild(set2)
+    case SetUnion(set1, set2) =>
+      onParent(expr) ++ onChild(set1) ++ onChild(set2)
+    case SetDifference(set1, set2) => onParent(expr) ++ onChild(set1) ++ onChild(set2)
+
+    /* Map operations */
+    case FiniteMap(pairs, _, _) =>
+      onParent(expr) ++ pairs.toList.flatMap(t => onChild(t._1) ++ onChild(t._2))
+    case MapApply(map, key) => onParent(expr) ++ onChild(map) ++ onChild(key)
+    case MapUnion(map1, map2) => onParent(expr) ++ onChild(map1) ++ onChild(map2)
+    case MapDifference(map, keys) => onParent(expr) ++ onChild(map) ++ onChild(keys)
+    case MapIsDefinedAt(map, key) => onParent(expr) ++ onChild(map) ++ onChild(key)
+
+    /* Array operations */
+    case ArraySelect(array, index) => onParent(expr) ++ onChild(array) ++ onChild(index)
+    case ArrayUpdated(array, index, newValue) =>
+      onParent(expr) ++ onChild(array) ++ onChild(index) ++ onChild(newValue)
+    case ArrayLength(array) => onParent(expr) ++ onChild(array)
+    case NonemptyArray(elems, defaultLength) => onParent(expr) ++ elems.flatMap(t => onChild(t._2))
+    case EmptyArray(_) => onParent(expr)
+
+    /* Holes */
+    case Choose(pred) => onParent(expr)
+    //case Hole(_, alts) => onParent(expr) ++ alts.flatMap(onChild(_))
+
+
+    // default value for any easy-to-handled or Terminal expression
+    // including: NoTree, Error, Variable, MethodInvocation, This, all Literal, ConverterToString
+    // leave aside (at least for the moment): String Theory, BitVector Operation, Special trees for synthesis (holes, ...)
+    case x if x.isInstanceOf[Expr] => onParent(expr)
+
+    //default value for error handling, should never reach that
+    case _ => Nil
+  }
+
+
+}
diff --git a/src/main/scala/leon/utils/DebugSections.scala b/src/main/scala/leon/utils/DebugSections.scala
index 7e454e7ea..8877d8870 100644
--- a/src/main/scala/leon/utils/DebugSections.scala
+++ b/src/main/scala/leon/utils/DebugSections.scala
@@ -25,6 +25,7 @@ case object DebugSectionTypes        extends DebugSection("types",        1 << 1
 case object DebugSectionIsabelle     extends DebugSection("isabelle",     1 << 14)
 case object DebugSectionReport       extends DebugSection("report",       1 << 15)
 case object DebugSectionGenC         extends DebugSection("genc",         1 << 16)
+case object DebugSectionComparison   extends DebugSection("comparison",   1 << 17)
 
 object DebugSections {
   val all = Set[DebugSection](
@@ -44,6 +45,7 @@ object DebugSections {
     DebugSectionTypes,
     DebugSectionIsabelle,
     DebugSectionReport,
-    DebugSectionGenC
+    DebugSectionGenC,
+    DebugSectionComparison
   )
 }
diff --git a/src/sphinx/installation.rst b/src/sphinx/installation.rst
index b4deaf194..964378eba 100644
--- a/src/sphinx/installation.rst
+++ b/src/sphinx/installation.rst
@@ -222,3 +222,95 @@ but instead
 
  package leon.test.myTestPackage
 
+
+
+
+
+Using Leon in IntelliJ
+----------------------
+
+You can maybe encounter some problems installing Leon, because of the various dependencies needed.
+Here is a step-by-step guide having as a goal to help you to install your first Leon project and to be sure that every
+dependency is present and correctly linked.
+
+The advantage of using IntelliJ IDEA is that it provides a Scala plugin which allows you to directly import SBT project
+into it.
+
+**Installation:**
+
+* `SBT 0.13.x <http://www.scala-sbt.org/>`_ (as described above)
+* `IntelliJ IDEA <https://www.jetbrains.com/idea/download/>`_
+* Leon project files, available in GitHub (as described above)
+* Java SE Development Kit 8 or 7 (as described above)
+* Support for at least one external solver (See :ref:`smt-solvers`)
+
+**Setup STB in your project:**
+
+Leon requires the Build class, which is a class created by SBT in its folder *target* when you compile your project the
+first time. Also, it will be comfortable to run Leon through terminal command, in order to easily specify arguments.
+We will resolve both of theses things running the command:
+
+.. code-block:: bash
+
+ $ sbt clean compile
+ $ sbt package script
+
+This will create the *leon* executable file that you can now use typing ```./leon```. You are not required to recompile
+this file after modifying your project, because *leon* file is actually a script that modifies the
+scala compiler, giving it the path to Leon, and then compile the file you specified. You can open *leon*
+in terminal ```cat leon``` to realize that.
+
+**Setup IntelliJ:**
+
+IntelliJ provides a Scala plugin. It will normally offer to install it by its own the first time you load a scala file,
+anyway we suggest you install it manually before starting. Doing so will allow you to use sbt wizard import
+in the next step.
+
+In *Preferences -> Plugins* search for *Scala* and install it.
+
+**Import Leon:**
+
+Use the *New project from existing sources...* (*Import project* in welcome window) wizard of IntelliJ to import Leon.
+Select the *SBT* external model and let
+IntelliJ install it with the default options. Specify the Java SDK 1.8. When choosing the modules to import, only
+select *Leon* and *Leon-build*
+(maybe called *root* and *root-build*), we will import the other modules later manually.
+
+You would now see only the *Leon* module in the IntelliJ project explorer. If you see *bonsai* or *smt-lib*, just
+delete them.
+
+**Setup dependencies:**
+
+By right-clicking on Leon, choose *Open Module Setting*. Here you will set all the dependencies, in the so-named tab. If
+SBT import tool worked well, you will see all needed dependencies present in your list and we will enable some of them.
+Anyway, if some of them are not present (which happened to me), you can add it by your own clicking
+``` "+" --> Add jar or folder --> ... ```. I will specify the path where you can find each dependency.
+
+Enable:
+
+* scala-smt-lib (can be found at ~/.sbt/0.13/staging/.../scala-smtlib/target/scala-2.11/classes)
+* bonsai (can be found at ~/.sbt/0.13/stagging/.../bonsai/target/scala-2.11/classes)
+* libisabel
+* libisabel-setub
+* scala-lang:... (enable all of them) (can be found at ~/.ivy2/cache/org.scala-lang/...)
+* scalatest
+
+If project has no SDK, add Java Library 1.8 (JDK 1.8)
+
+The scala-lang:scala-library and scala-lang:scala-compiler must stand for the scala SDK provided by intelliJ, so
+normally you haven't to add it. Anyway, if you encounter some problems, download it at with "+" -> Library -> Global Library
+-> New Library and select the latest *Ivy* available. Ensure you have at least Scala 2.11 and NOT 2.10. Ensure also that
+this added scala SDK is listed BELOW the scala-lang provided by SBT, so it has lower priority.
+
+*.sbt* and *.ivy2* are folders created by SBT and are placed in your home folder.
+
+If you find that some other modules are required to your project, feel free to add them but keep them below the ones
+described in the priority list.
+
+**Check your installation:**
+
+*Make* the project in IntelliJ and try running it on some test files, like
+
+.. code-block:: bash
+
+ $ ./leon testcases/verification/datastructures/AssociativeList.scala
diff --git a/testcases/comparison/corpus/ClassBase.scala b/testcases/comparison/corpus/ClassBase.scala
new file mode 100644
index 000000000..1402b3ecc
--- /dev/null
+++ b/testcases/comparison/corpus/ClassBase.scala
@@ -0,0 +1,73 @@
+import leon.annotation._
+import leon.lang._
+import leon.collection._
+
+
+object ClassBase {
+
+
+  def match_value(x: Int): Char = x match {
+    case 1 => 'a'
+    case 2 => 'b'
+  }
+
+  def inversed_match_value(x: Int): Char = x match {
+    case 2 => 'b'
+    case 1 => 'a'
+  }
+
+
+
+  def encapsulated_match_value(x: Int): Char = x match {
+    case x2 if x2 < 10 =>
+      x2 match {
+        case 1 => 'a'
+        case 2 => 'b'
+      }
+    case _ => 'z'
+  }
+
+  def large_match_value(x:Int): Char = x match {
+    case 1 => 'a'
+    case 2 => 'b'
+    case 3 => 'c'
+    case 4 => 'd'
+  }
+
+  def match_with_val(x:Int): Char = {
+    val somme = x match {
+      case 1 => 'a'
+      case 2 => 'c'
+    }
+
+    if (somme == 'a') 'a' else 'b'
+  }
+
+  def dummy_replace(x: BigInt, list: List[Char], char: Char): List[Char] = {
+    val size = list.size
+    val ret: List[Char] = if (x < 0 || x > size) {
+      list
+    } else {
+      val before: List[Char] = list.take(x)
+      val after: List[Char] = list.drop(x+1)
+      before ++ List(char) ++ after
+    }
+
+    ret
+  }
+
+  case class B(x: Int) extends A
+  case class C(x: Int, y: Int) extends A
+  abstract class A
+
+  def class_B(x: Int): B = B(x)
+
+  def class_C(x:Int, y: Int): C = C(x, y)
+
+
+
+
+
+
+
+}
diff --git a/testcases/comparison/to-compare/ClassToCompare.scala b/testcases/comparison/to-compare/ClassToCompare.scala
new file mode 100644
index 000000000..c175f4e1d
--- /dev/null
+++ b/testcases/comparison/to-compare/ClassToCompare.scala
@@ -0,0 +1,63 @@
+import leon.annotation._
+import leon.lang._
+import leon.collection._
+import leon.lang.synthesis._
+
+
+object ClassToCompare {
+
+
+  def match_value(x: Int): Char = x match {
+    case 1 => 'a'
+    case 2 => 'b'
+  }
+
+  case class B(x: Int) extends A
+  abstract class A
+
+  def class_B(x: Int): B = B(x)
+
+  def hole_match_value(x:Int): Char = x match {
+    case 1 => 'a'
+    case 2 => ??? [Char]
+  }
+
+  def hole_large_match_value(x:Int): Char = x match {
+    case 1 => 'a'
+    case 2 => 'b'
+    case 3 => ??? [Char]
+    case 4 => 'd'
+  }
+
+  def hole_encapsulated_match_value(x: Int): Char = x match {
+    case x2 if x2 < 10 =>
+      x2 match {
+        case 1 => ??? [Char]
+        case 2 => 'b'
+      }
+    case _ => 'z'
+  }
+
+  def hole_that_doesnt_match(x: Int, y: Int): Char ={
+    if (x > y) 'x'
+    else ??? [Char]
+  }
+
+  def hole_match_val(x:Int): Char = {
+    val somme: Char = ??? [Char]
+
+    if (somme == 'a') 'a' else 'b'
+  }
+
+  def hole_replace(x: BigInt, list: List[Char], char: Char): List[Char] = {
+    val size = list.size
+    val ret: List[Char] = if (x < 0 || x > size) {
+      list
+    } else {
+      ??? [List[Char]]
+    }
+    ret
+  }
+
+
+}
\ No newline at end of file