diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 4b960a043d2baf82b96a05a7133bf05faf6fafe6..6a4981997d0032f16011f3ca7189d632aba331e5 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -280,7 +280,27 @@ object Constructors {
     if (a == b && isDeterministic(a)) {
       BooleanLiteral(true)
     } else  {
-      Equals(a, b)
+      (a, b) match {
+        case (a: Literal[_], b: Literal[_]) =>
+          if (a.value == b.value) {
+            BooleanLiteral(true)
+          } else {
+            BooleanLiteral(false)
+          }
+
+        case _ =>
+          Equals(a, b)
+      }
+    }
+  }
+
+  def assertion(c: Expr, err: Option[String], res: Expr) = {
+    if (c == BooleanLiteral(true)) {
+      res
+    } else if (c == BooleanLiteral(false)) {
+      Error(res.getType, err.getOrElse("Assertion failed"))
+    } else {
+      Assert(c, err, res)
     }
   }
 
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 4959ae799c8f34b25dbdf1cac812ef8d954b4717..6523a1104127c174edf5c1e9d994be27b797d421 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -2,9 +2,11 @@
 
 package leon
 package repair
-  
+
+import purescala.Common._
 import purescala.Definitions._
 import purescala.Expressions._
+import purescala.Extractors._
 import purescala.ExprOps._
 import purescala.Types._
 import purescala.DefOps._
@@ -98,6 +100,60 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
             bh.write()
           }
 
+          reporter.ifDebug { printer =>
+            import java.io.FileWriter
+            import java.text.SimpleDateFormat
+            import java.util.Date
+
+            val categoryName = fd.getPos.file.toString.split("/").dropRight(1).lastOption.getOrElse("?")
+            val benchName = categoryName+"."+fd.id.name
+
+            val defs = visibleFunDefsFromMain(program).collect {
+              case fd: FunDef => 1 + fd.params.size + formulaSize(fd.fullBody)
+            }
+
+            val pSize = defs.sum;
+            val fSize = formulaSize(fd.body.get)
+
+            def localizedExprs(n: graph.Node): List[Expr] = {
+              n match {
+                case on: graph.OrNode =>
+                  on.selected.map(localizedExprs).flatten
+                case an: graph.AndNode if an.ri.rule == Focus =>
+                  an.selected.map(localizedExprs).flatten
+                case an: graph.AndNode =>
+                  val TopLevelAnds(clauses) = an.p.ws
+
+                  val res = clauses.collect {
+                    case Guide(expr) => expr
+                  }
+
+                  res.toList
+              }
+            }
+
+            val locSize = localizedExprs(search.g.root).map(formulaSize).sum;
+
+            val (solSize, proof) = solutions.headOption match {
+              case Some((sol, trusted)) =>
+                val solExpr = sol.toSimplifiedExpr(ctx, program)
+                val totalSolSize = formulaSize(solExpr)
+                (locSize+totalSolSize-fSize, if (trusted) "$\\chmark$" else "")
+              case _ =>
+                (0, "X")
+            }
+
+            val date = new SimpleDateFormat("yyyy-MM-dd HH:mm:ss").format(new Date())
+
+            val fw = new java.io.FileWriter("repair-report.txt", true)
+
+            try {
+              fw.write(f"$date:  $benchName%-30s & $pSize%4d & $fSize%4d & $locSize%4d & $solSize%4d & ${timeTests/1000.0}%2.1f &  ${timeSynth/1000.0}%2.1f & $proof%7s \\\\\n")
+            } finally {
+              fw.close
+            }
+          }(DebugSectionReport)
+
           if (synth.settings.generateDerivationTrees) {
             val dot = new DotGenerator(search.g)
             dot.writeFile("derivation"+ dotGenIds.nextGlobal + ".dot")
diff --git a/src/main/scala/leon/synthesis/ConversionPhase.scala b/src/main/scala/leon/synthesis/ConversionPhase.scala
index d5f4e842f698e54d353d4170c1591073debefd5e..a2fa94ea9ade148ebf331b6c75d4833e3c0ea8a0 100644
--- a/src/main/scala/leon/synthesis/ConversionPhase.scala
+++ b/src/main/scala/leon/synthesis/ConversionPhase.scala
@@ -188,6 +188,8 @@ object ConversionPhase extends UnitPhase[Program] {
 
     // extract spec from chooses at the top-level
     fullBody match {
+      case Require(_, Choose(spec)) =>
+        withPostcondition(fullBody, Some(spec))
       case Choose(spec) =>
         withPostcondition(fullBody, Some(spec))
       case _ =>
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 51a5a15ec12700d48ccd054665189372110e01e1..bf6785e4b0ce2fcd4dd597d3c52733426f3e5d4e 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -41,10 +41,12 @@ object Rules {
     Unification.OccursCheck, // probably useless
     Disunification.Decomp,
     ADTDual,
-    //OnePoint,
+    OnePoint,
     Ground,
     CaseSplit,
+    IndependentSplit,
     IfSplit,
+    InputSplit,
     UnusedInput,
     EquivalentInputs,
     UnconstrainedOutput,
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 72cfffec3f8ef3fd8a526d778fda1f26a9ec1a41..b9ba6df1f688e01edf631e995ba2f8623bcfc5fe 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -6,6 +6,7 @@ package synthesis
 import purescala.ExprOps._
 
 import purescala.ScalaPrinter
+import leon.utils._
 import purescala.Definitions.{Program, FunDef}
 import leon.utils.ASCIIHelpers
 
@@ -20,12 +21,11 @@ object SynthesisPhase extends TransformationPhase {
   val optDerivTrees  = LeonFlagOptionDef( "derivtrees", "Generate derivation trees", false)
 
   // CEGIS options
-  val optCEGISShrink     = LeonFlagOptionDef( "cegis:shrink",     "Shrink non-det programs when tests pruning works well",  true)
   val optCEGISOptTimeout = LeonFlagOptionDef( "cegis:opttimeout", "Consider a time-out of CE-search as untrusted solution", true)
   val optCEGISVanuatoo   = LeonFlagOptionDef( "cegis:vanuatoo",   "Generate inputs using new korat-style generator",       false)
 
   override val definedOptions : Set[LeonOptionDef[Any]] =
-    Set(optManual, optCostModel, optDerivTrees, optCEGISShrink, optCEGISOptTimeout, optCEGISVanuatoo)
+    Set(optManual, optCostModel, optDerivTrees, optCEGISOptTimeout, optCEGISVanuatoo)
 
   def processOptions(ctx: LeonContext): SynthesisSettings = {
     val ms = ctx.findOption(optManual)
@@ -57,7 +57,6 @@ object SynthesisPhase extends TransformationPhase {
       manualSearch = ms,
       functions = ctx.findOption(SharedOptions.optFunctions) map { _.toSet },
       cegisUseOptTimeout = ctx.findOption(optCEGISOptTimeout),
-      cegisUseShrink = ctx.findOption(optCEGISShrink),
       cegisUseVanuatoo = ctx.findOption(optCEGISVanuatoo)
     )
   }
@@ -74,21 +73,25 @@ object SynthesisPhase extends TransformationPhase {
 
       val synthesizer = new Synthesizer(ctx, program, ci, options)
 
-      val (search, solutions) = synthesizer.validate(synthesizer.synthesize(), allowPartial = true)
+      val to = new TimeoutFor(ctx.interruptManager)
 
-      try {
-        if (options.generateDerivationTrees) {
-          val dot = new DotGenerator(search.g)
-          dot.writeFile("derivation"+dotGenIds.nextGlobal+".dot")
-        }
+      to.interruptAfter(options.timeoutMs) {
+        val (search, solutions) = synthesizer.validate(synthesizer.synthesize(), allowPartial = true)
+
+        try {
+          if (options.generateDerivationTrees) {
+            val dot = new DotGenerator(search.g)
+            dot.writeFile("derivation"+dotGenIds.nextGlobal+".dot")
+          }
 
-        val (sol, _) = solutions.head
+          val (sol, _) = solutions.head
 
-        val expr = sol.toSimplifiedExpr(ctx, program)
-        fd.body = fd.body.map(b => replace(Map(ci.source -> expr), b))
-        functions += fd
-      } finally {
-        synthesizer.shutdown()
+          val expr = sol.toSimplifiedExpr(ctx, program)
+          fd.body = fd.body.map(b => replace(Map(ci.source -> expr), b))
+          functions += fd
+        } finally {
+          synthesizer.shutdown()
+        }
       }
     }
 
diff --git a/src/main/scala/leon/synthesis/SynthesisSettings.scala b/src/main/scala/leon/synthesis/SynthesisSettings.scala
index 9d227bdb611f2ca44eb70a95ce52bc506712e160..5202818e18765ebf4086ef41d1685967a14940d0 100644
--- a/src/main/scala/leon/synthesis/SynthesisSettings.scala
+++ b/src/main/scala/leon/synthesis/SynthesisSettings.scala
@@ -17,7 +17,6 @@ case class SynthesisSettings(
   
   // Cegis related options
   cegisUseOptTimeout: Option[Boolean] = None,
-  cegisUseShrink: Option[Boolean]     = None,
   cegisUseVanuatoo: Option[Boolean]   = None
 
 )
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 35fdfb845ae0a5de611ab3a01a3111005aff7a05..bafed6ec2bab51539bfc0547563bbad2aeea873e 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -8,6 +8,7 @@ import purescala.ExprOps._
 import purescala.DefOps._
 import purescala.ScalaPrinter
 import solvers._
+import leon.utils._
 
 import scala.concurrent.duration._
 
@@ -34,9 +35,10 @@ class Synthesizer(val context : LeonContext,
     }
   }
 
-  def synthesize(): (Search, Stream[Solution]) = {
+  private var lastTime: Long = 0
 
-    reporter.ifDebug { printer => 
+  def synthesize(): (Search, Stream[Solution]) = {
+    reporter.ifDebug { printer =>
       printer(problem.eb.asString("Tests available for synthesis")(context))
     }
 
@@ -47,8 +49,12 @@ class Synthesizer(val context : LeonContext,
     val sols = s.search(sctx)
 
     val diff = t.stop()
+
+    lastTime = diff
+
     reporter.info("Finished in "+diff+"ms")
 
+
     (s, sols)
   }
 
@@ -62,6 +68,43 @@ class Synthesizer(val context : LeonContext,
         validateSolution(s, sol, 5.seconds)
     }
 
+    // Print out report for synthesis, if necessary
+    reporter.ifDebug { printer =>
+      import java.io.FileWriter
+      import java.text.SimpleDateFormat
+      import java.util.Date
+
+      val categoryName = ci.fd.getPos.file.toString.split("/").dropRight(1).lastOption.getOrElse("?")
+      val benchName = categoryName+"."+ci.fd.id.name
+      var time = lastTime/1000.0;
+
+      val defs = visibleDefsFrom(ci.fd)(program).collect {
+        case cd: ClassDef => 1 + cd.fields.size
+        case fd: FunDef => 1 + fd.params.size + formulaSize(fd.fullBody)
+      }
+
+      val psize = defs.sum;
+
+
+      val (size, calls, proof) = result.headOption match {
+        case Some((sol, trusted)) =>
+          val expr = sol.toSimplifiedExpr(context, program)
+          (formulaSize(expr), functionCallsOf(expr).size, if (trusted) "$\\surd$" else "")
+        case _ =>
+          (0, 0, "X")
+      }
+
+      val date = new SimpleDateFormat("yyyy-MM-dd HH:mm:ss").format(new Date())
+
+      val fw = new java.io.FileWriter("synthesis-report.txt", true)
+
+      try {
+        fw.write(f"$date:  $benchName%-50s & $psize%4d & $size%4d & $calls%4d & $proof%7s & $time%2.1f \\\\\n")
+      } finally {
+        fw.close
+      }
+    }(DebugSectionReport)
+
     (s, if (result.isEmpty && allowPartial) {
       List((new PartialSolution(s.g, true).getSolution, false)).toStream
     } else {
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 5d06aa76a3c1186e806edf605431643e6b2a9359..4f03c9bed6ca7c7ce5338d04283483ab9f348890 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -45,14 +45,10 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
     // CEGIS Flags to activate or deactivate features
     val useOptTimeout    = sctx.settings.cegisUseOptTimeout.getOrElse(true)
     val useVanuatoo      = sctx.settings.cegisUseVanuatoo.getOrElse(false)
-    val useShrink        = sctx.settings.cegisUseShrink.getOrElse(false)
 
     // Limits the number of programs CEGIS will specifically validate individually
     val validateUpTo     = 3
 
-    // Shrink the program when the ratio of passing cases is less than the threshold
-    val shrinkThreshold  = 1.0/2
-
     val interruptManager = sctx.context.interruptManager
 
     val params = getParams(sctx, p)
@@ -67,9 +63,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
 
       val grammar = SizeBoundedGrammar(params.grammar)
 
-      def rootLabel(tpe: TypeTree) = SizedLabel(params.rootLabel(tpe), termSize)
-
-      def xLabels = p.xs.map(x => rootLabel(x.getType))
+      def rootLabel = SizedLabel(params.rootLabel(tupleTypeWrap(p.xs.map(_.getType))), termSize)
 
       var nAltsCache = Map[SizedLabel[T], Int]()
 
@@ -84,7 +78,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
       }
 
       def allProgramsCount(): Int = {
-        xLabels.map(countAlternatives).product
+        countAlternatives(rootLabel)
       }
 
       /**
@@ -108,7 +102,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
 
 
       // C identifiers corresponding to p.xs
-      private var rootCs: Seq[Identifier]    = Seq()
+      private var rootC: Identifier    = _
 
       private var bs: Set[Identifier]        = Set()
 
@@ -179,9 +173,9 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
 
         val cGen = new CGenerator()
 
-        rootCs = for (l <- xLabels) yield {
-          val c = cGen.getNext(l)
-          defineCTreeFor(l, c)
+        rootC = {
+          val c = cGen.getNext(rootLabel)
+          defineCTreeFor(rootLabel, c)
           c
         }
 
@@ -244,7 +238,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
           }
         }
 
-        allProgramsFor(rootCs)
+        allProgramsFor(Seq(rootC))
       }
 
       private def debugCTree(cTree: Map[Identifier, Seq[(Identifier, Seq[Expr] => Expr, Seq[Identifier])]],
@@ -299,11 +293,11 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
           cToFd(c).fullBody = body
         }
 
-        // Top-level expression for rootCs
-        val expr = tupleWrap(rootCs.map { c =>
-          val fd = cToFd(c)
+        // Top-level expression for rootC
+        val expr = {
+          val fd = cToFd(rootC)
           FunctionInvocation(fd.typed, fd.params.map(_.toVariable))
-        })
+        }
 
         (expr, cToFd.values.toSeq)
       }
@@ -441,7 +435,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
           }
         }
 
-        tupleWrap(rootCs.map(c => getCValue(c)))
+        getCValue(rootC)
       }
 
       /**
@@ -521,7 +515,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
         val bvs = if (isMinimal) {
           bs
         } else {
-          rootCs.flatMap(filterBTree).toSet
+          filterBTree(rootC)
         }
 
         excludedPrograms += bvs
@@ -829,14 +823,13 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
 
                     if (nPassing <= validateUpTo) {
                       // All programs failed verification, we filter everything out and unfold
-                      //ndProgram.shrinkTo(Set(), unfolding == maxUnfoldings)
                       doFilter     = false
                       skipCESearch = true
                     }
                 }
               }
 
-              if (doFilter && !(nPassing < nInitial * shrinkThreshold && useShrink)) {
+              if (doFilter) {
                 sctx.reporter.debug("Excluding "+wrongPrograms.size+" programs")
                 wrongPrograms.foreach {
                   ndProgram.excludeProgram(_, true)
diff --git a/src/main/scala/leon/synthesis/rules/DetupleInput.scala b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
index ed68fbfac84543b1922b44cb91273043756b3cb1..2ae2b1d5d0292a6ed725055e61b1b4af4100a63c 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleInput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
@@ -30,20 +30,28 @@ case object DetupleInput extends NormalizingRule("Detuple In") {
      * into a list of fresh typed identifiers, the tuple of these new identifiers,
      * and the mapping of those identifiers to their respective expressions.
      */
-    def decompose(id: Identifier): (List[Identifier], Expr, Map[Identifier, Expr]) = id.getType match {
+    def decompose(id: Identifier): (List[Identifier], Expr, Map[Identifier, Expr], Expr => Seq[Expr]) = id.getType match {
       case cct @ CaseClassType(ccd, _) if !ccd.isAbstract =>
         val newIds = cct.fields.map{ vd => FreshIdentifier(vd.id.name, vd.getType, true) }
 
         val map = (ccd.fields zip newIds).map{ case (vd, nid) => nid -> caseClassSelector(cct, Variable(id), vd.id) }.toMap
 
-        (newIds.toList, CaseClass(cct, newIds.map(Variable)), map)
+        val tMap: (Expr => Seq[Expr]) = {
+          case CaseClass(ccd, fields) => fields
+        }
+
+        (newIds.toList, CaseClass(cct, newIds.map(Variable)), map, tMap)
 
       case TupleType(ts) =>
         val newIds = ts.zipWithIndex.map{ case (t, i) => FreshIdentifier(id.name+"_"+(i+1), t, true) }
 
         val map = newIds.zipWithIndex.map{ case (nid, i) => nid -> TupleSelect(Variable(id), i+1) }.toMap
 
-        (newIds.toList, tupleWrap(newIds.map(Variable)), map)
+        val tMap: (Expr => Seq[Expr]) = {
+          case Tuple(fields) => fields
+        }
+
+        (newIds.toList, tupleWrap(newIds.map(Variable)), map, tMap)
 
       case _ => sys.error("woot")
     }
@@ -55,9 +63,11 @@ case object DetupleInput extends NormalizingRule("Detuple In") {
 
       var reverseMap = Map[Identifier, Expr]()
 
+      var ebMapInfo = Map[Identifier, Expr => Seq[Expr]]()
+
       val subAs = p.as.map { a =>
         if (isDecomposable(a)) {
-          val (newIds, expr, map) = decompose(a)
+          val (newIds, expr, map, tMap) = decompose(a)
 
           subProblem = subst(a -> expr, subProblem)
           subPc      = subst(a -> expr, subPc)
@@ -65,12 +75,25 @@ case object DetupleInput extends NormalizingRule("Detuple In") {
 
           reverseMap ++= map
 
+          ebMapInfo += a -> tMap
+
           newIds
         } else {
           List(a)
         }
       }
 
+      var eb = p.qeb.mapIns { info =>
+        List(info.flatMap { case (id, v) =>
+          ebMapInfo.get(id) match {
+            case Some(m) =>
+              m(v)
+            case None =>
+              List(v)
+          }
+        })
+      }
+
       val newAs = subAs.flatten
 
       // Recompose CaseClasses and Tuples.
@@ -101,7 +124,7 @@ case object DetupleInput extends NormalizingRule("Detuple In") {
         case other => other
       }
       
-      val sub = Problem(newAs, subWs, subPc, subProblem, p.xs)
+      val sub = Problem(newAs, subWs, subPc, subProblem, p.xs, eb)
 
       val s = {substAll(reverseMap, _:Expr)} andThen { simplePostTransform(recompose) }
      
diff --git a/src/main/scala/leon/synthesis/rules/IndependentSplit.scala b/src/main/scala/leon/synthesis/rules/IndependentSplit.scala
new file mode 100644
index 0000000000000000000000000000000000000000..72be06b9cff76a63ced4506ef086a58622326bef
--- /dev/null
+++ b/src/main/scala/leon/synthesis/rules/IndependentSplit.scala
@@ -0,0 +1,80 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package synthesis
+package rules
+
+import leon.utils._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Extractors._
+import purescala.Constructors._
+import purescala.Common._
+import purescala.Types.CaseClassType
+
+case object IndependentSplit extends NormalizingRule("IndependentSplit") {
+  def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
+    val TopLevelAnds(clauses) = and(p.pc, p.phi)
+
+    var independentClasses = Set[Set[Identifier]]()
+
+    // We group connect variables together
+    for(c <- clauses) {
+      val vs = variablesOf(c)
+
+      var newClasses = Set[Set[Identifier]]()
+
+      var thisClass = vs
+
+      for (cl <- independentClasses) {
+        if ((cl & vs).nonEmpty) {
+          thisClass ++= cl
+        } else {
+          newClasses += cl
+        }
+      }
+
+      independentClasses = newClasses + thisClass
+    }
+
+    val outClasses = independentClasses.map(cl => cl & p.xs.toSet).filter(_.nonEmpty)
+
+    if (outClasses.size > 1) {
+
+      val TopLevelAnds(phiClauses) = p.phi
+
+      val subs = (for (cl <- outClasses.toList) yield {
+        val xs = p.xs.filter(cl)
+
+        if (xs.nonEmpty) {
+          val phi = andJoin(phiClauses.filter(c => (variablesOf(c) & cl).nonEmpty))
+
+          val xsToRemove = p.xs.filterNot(cl).toSet
+
+          val eb = p.qeb.removeOuts(xsToRemove)
+
+          Some(p.copy(phi = phi, xs = xs, eb = eb))
+        } else {
+          None
+        }
+      }).flatten
+
+      val onSuccess: List[Solution] => Option[Solution] = { sols =>
+
+        val infos = subs.map(_.xs).zip(sols.map(_.term))
+
+        val term = infos.foldLeft(tupleWrap(p.xs.map(_.toVariable))) {
+          case (expr, (xs, term)) =>
+            letTuple(xs, term, expr)
+        }
+
+        Some(Solution(andJoin(sols.map(_.pre)), sols.map(_.defs).flatten.toSet, term, sols.forall(_.isTrusted)))
+      }
+
+
+      List(decomp(subs, onSuccess, "Independent Clusters"))
+    } else {
+      Nil
+    }
+  }
+}
diff --git a/src/main/scala/leon/synthesis/rules/InputSplit.scala b/src/main/scala/leon/synthesis/rules/InputSplit.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4b9ffef53793528b628b41485c0a9156e171f188
--- /dev/null
+++ b/src/main/scala/leon/synthesis/rules/InputSplit.scala
@@ -0,0 +1,49 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package synthesis
+package rules
+
+import leon.purescala.Common.Identifier
+import purescala.Expressions._
+import purescala.Extractors._
+import purescala.ExprOps._
+import purescala.Constructors._
+import purescala.Types._
+
+import solvers._
+
+import scala.concurrent.duration._
+
+case object InputSplit extends Rule("In. Split") {
+  def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
+    p.as.filter(_.getType == BooleanType).flatMap { a =>
+        def getProblem(v: Boolean): Problem = {
+          def replaceA(e: Expr) = replaceFromIDs(Map(a -> BooleanLiteral(v)), e)
+
+          p.copy(
+            as  = p.as.filterNot(_ == a),
+            ws  = replaceA(p.ws),
+            pc  = replaceA(p.pc),
+            phi = replaceA(p.phi),
+            eb  = p.qeb.removeIns(Set(a))
+          )
+        }
+
+        val sub1 = getProblem(true)
+        val sub2 = getProblem(false)
+
+        val onSuccess: List[Solution] => Option[Solution] = {
+          case List(s1, s2) =>
+            Some(Solution(or(and(Equals(Variable(a), BooleanLiteral(true)), s1.pre), 
+                             and(Equals(Variable(a), BooleanLiteral(false)), s2.pre)),
+                          s1.defs ++ s2.defs, 
+                          IfExpr(Variable(a), s1.term, s2.term), s1.isTrusted && s2.isTrusted))
+          case _ =>
+            None
+        }
+
+      Some(decomp(List(sub1, sub2), onSuccess, s"Split on '$a'"))
+    }
+  }
+}
diff --git a/src/main/scala/leon/utils/DebugSections.scala b/src/main/scala/leon/utils/DebugSections.scala
index c18881e47f23fd9c5503320888158cc38f68b10d..a0b790243a6dc309953d07ba02d504e463185880 100644
--- a/src/main/scala/leon/utils/DebugSections.scala
+++ b/src/main/scala/leon/utils/DebugSections.scala
@@ -23,6 +23,7 @@ case object DebugSectionLeon         extends DebugSection("leon",         1 << 1
 case object DebugSectionXLang        extends DebugSection("xlang",        1 << 12)
 case object DebugSectionTypes        extends DebugSection("types",        1 << 13)
 case object DebugSectionIsabelle     extends DebugSection("isabelle",     1 << 14)
+case object DebugSectionReport       extends DebugSection("report",       1 << 15)
 
 object DebugSections {
   val all = Set[DebugSection](
@@ -40,6 +41,7 @@ object DebugSections {
     DebugSectionLeon,
     DebugSectionXLang,
     DebugSectionTypes,
-    DebugSectionIsabelle
+    DebugSectionIsabelle,
+    DebugSectionReport
   )
 }
diff --git a/src/main/scala/leon/verification/InjectAsserts.scala b/src/main/scala/leon/verification/InjectAsserts.scala
index 418da12eb62e1fb1ead33bc0317da9ceb9662e28..a2ba463a6519a4c10e224c583263b805b4f660d7 100644
--- a/src/main/scala/leon/verification/InjectAsserts.scala
+++ b/src/main/scala/leon/verification/InjectAsserts.scala
@@ -42,34 +42,34 @@ object InjectAsserts extends SimpleLeonPhase[Program, Program] {
                      ).setPos(e))
 
         case e @ Division(_, d)  =>
-          Some(Assert(Not(Equals(d, InfiniteIntegerLiteral(0))),
+          Some(assertion(not(equality(d, InfiniteIntegerLiteral(0))),
                       Some("Division by zero"),
                       e
                      ).setPos(e))
         case e @ Remainder(_, d)  =>
-          Some(Assert(Not(Equals(d, InfiniteIntegerLiteral(0))),
+          Some(assertion(not(equality(d, InfiniteIntegerLiteral(0))),
                       Some("Remainder by zero"),
                       e
                      ).setPos(e))
         case e @ Modulo(_, d)  =>
-          Some(Assert(Not(Equals(d, InfiniteIntegerLiteral(0))),
+          Some(assertion(not(equality(d, InfiniteIntegerLiteral(0))),
                       Some("Modulo by zero"),
                       e
                      ).setPos(e))
 
         case e @ BVDivision(_, d)  =>
-          Some(Assert(Not(Equals(d, IntLiteral(0))),
+          Some(assertion(not(equality(d, IntLiteral(0))),
                       Some("Division by zero"),
                       e
                      ).setPos(e))
         case e @ BVRemainder(_, d)  =>
-          Some(Assert(Not(Equals(d, IntLiteral(0))),
+          Some(assertion(not(equality(d, IntLiteral(0))),
                       Some("Remainder by zero"),
                       e
                      ).setPos(e))
 
         case e @ RealDivision(_, d)  =>
-          Some(Assert(Not(Equals(d, FractionalLiteral(0, 1))),
+          Some(assertion(not(equality(d, FractionalLiteral(0, 1))),
                       Some("Division by zero"),
                       e
                      ).setPos(e))
diff --git a/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala b/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala
index a8927f360e817d10761723c8a4b7e9085bf0738d..aa00e12d446e1b11984f741500279a5647cfe426 100644
--- a/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala
@@ -10,14 +10,11 @@ object PropositionalLogic {
   case class Or(lhs: Formula, rhs: Formula) extends Formula
   case class Implies(lhs: Formula, rhs: Formula) extends Formula
   case class Not(f: Formula) extends Formula
-  case class Literal(id: Int) extends Formula
+  case class Literal(id: BigInt) extends Formula
 
   def simplify(f: Formula): Formula = (f match {
-    case And(lhs, rhs) => And(simplify(lhs), simplify(rhs))
-    case Or(lhs, rhs) => Or(simplify(lhs), simplify(rhs))
     case Implies(lhs, rhs) => Or(Not(simplify(lhs)), simplify(rhs))
-    case Not(f) => Not(simplify(f))
-    case Literal(_) => f
+    case _ => f
   }) ensuring(isSimplified(_))
 
   def isSimplified(f: Formula): Boolean = f match {
@@ -28,18 +25,6 @@ object PropositionalLogic {
     case Literal(_) => true
   }
 
-  def nnf(formula: Formula): Formula = (formula match {
-    case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
-    case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
-    case Implies(lhs, rhs) => Implies(nnf(lhs), nnf(rhs))
-    case Not(And(lhs, rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs)))
-    case Not(Or(lhs, rhs)) => And(nnf(Not(lhs)), nnf(Not(rhs)))
-    case Not(Implies(lhs, rhs)) => And(nnf(lhs), nnf(Not(rhs)))
-    case Not(Not(f)) => nnf(f)
-    case Not(Literal(_)) => formula
-    case Literal(_) => formula
-  }) ensuring(isNNF(_))
-
   def isNNF(f: Formula): Boolean = f match {
     case And(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
     case Or(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
@@ -49,39 +34,14 @@ object PropositionalLogic {
     case Literal(_) => true
   }
 
-  def vars(f: Formula): Set[Int] = {
-    require(isNNF(f))
-    f match {
-      case And(lhs, rhs) => vars(lhs) ++ vars(rhs)
-      case Or(lhs, rhs) => vars(lhs) ++ vars(rhs)
-      case Implies(lhs, rhs) => vars(lhs) ++ vars(rhs)
-      case Not(Literal(i)) => Set[Int](i)
-      case Literal(i) => Set[Int](i)
-    }
-  }
-
-  def fv(f : Formula) = { vars(nnf(f)) }
 
   // @induct
   // def wrongCommutative(f: Formula) : Boolean = {
   //   nnf(simplify(f)) == simplify(nnf(f))
   // }.holds
 
-  @induct
-  def simplifyBreaksNNF(f: Formula) : Boolean = {
+ def simplifyBreaksNNF(f: Formula) : Boolean = {
     require(isNNF(f))
     isNNF(simplify(f))
   }.holds
-
-  @induct
-  def nnfIsStable(f: Formula) : Boolean = {
-    require(isNNF(f))
-    nnf(f) == f
-  }.holds
-
-  @induct
-  def simplifyIsStable(f: Formula) : Boolean = {
-    require(isSimplified(f))
-    simplify(f) == f
-  }.holds
 }
diff --git a/testcases/repair/Compiler/Compiler4.scala b/testcases/repair/Compiler/Compiler4.scala
index f49670ddc31632343fea32f1b8d39ca288f214d4..6323496df930172e84b71bf5c55006eb33767c6a 100644
--- a/testcases/repair/Compiler/Compiler4.scala
+++ b/testcases/repair/Compiler/Compiler4.scala
@@ -150,7 +150,7 @@ 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(1), Literal(1)) // FIMXE should be 0
+    case Trees.Not(e) => Ite(desugar(e), Literal(1), Literal(1)) // FIXME should be 0
     case Trees.Eq(lhs, rhs) =>
       Eq(desugar(lhs), desugar(rhs))
     case Trees.Ite(cond, thn, els) => Ite(desugar(cond), desugar(thn), desugar(els))
diff --git a/testcases/repair/Compiler/Compiler6.scala b/testcases/repair/Compiler/Compiler6.scala
index 44bf523ec7aff63376ba24312594045296536dcf..dc633b1ae3d4d929e262ea44d6466a41ee4babf0 100644
--- a/testcases/repair/Compiler/Compiler6.scala
+++ b/testcases/repair/Compiler/Compiler6.scala
@@ -207,6 +207,8 @@ object Simplifier {
       case e => e
     }
   } ensuring {
-    res => eval(res) == eval(e)
+    res => eval(res) == eval(e) && ((e, res) passes {
+      case Plus(IntLiteral(BigInt(0)), IntLiteral(a)) => IntLiteral(a)
+    })
   }
 }
diff --git a/testcases/repair/Heap/Heap3.scala b/testcases/repair/Heap/Heap3.scala
index 3305b5d15a0731bd3aeaa1269c2404807f49a266..8e3013399534679c58221bd4d5547a14a76d9b57 100644
--- a/testcases/repair/Heap/Heap3.scala
+++ b/testcases/repair/Heap/Heap3.scala
@@ -51,7 +51,7 @@ object Heaps {
     case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
   }} ensuring(_ >= 0)
 
-  private def merge(h1: Heap, h2: Heap) : Heap = {
+  def merge(h1: Heap, h2: Heap) : Heap = {
     require(
       hasLeftistProperty(h1) && hasLeftistProperty(h2) && 
       hasHeapProperty(h1) && hasHeapProperty(h2)
diff --git a/testcases/repair/List/List13.scala b/testcases/repair/List/List13.scala
index 914f0caacd49b42448ec428df24af6ea155c53d2..1093efc3dc951ee8307c2257d8dcec2d154c9ecd 100644
--- a/testcases/repair/List/List13.scala
+++ b/testcases/repair/List/List13.scala
@@ -78,14 +78,22 @@ sealed abstract class List[T] {
       }
   }
 
-  def drop(i: BigInt): List[T] = (this, i) match {
-    case (Nil(), _) => Nil()
-    case (Cons(h, t), i) =>
-      if (i == 0) {
-        Cons(h, t)
-      } else {
-        t.drop(i) // FIXME Should be -1
-      }
+  def drop(i: BigInt): List[T] = {
+    require(i >= 0)
+    (this, i) match {
+      case (Nil(), _) => Nil[T]()
+      case (Cons(h, t), i) =>
+        if (i == 0) {
+          Cons[T](h, t)
+        } else {
+          t.drop(i) // FIXME Should be -1
+        }
+    }
+  } ensuring { (res: List[T]) =>
+    ((this, i), res) passes {
+      case (Cons(a, Cons(b, Nil())), BigInt(1)) => Cons(b, Nil())
+      case (Cons(a, Cons(b, Nil())), BigInt(2)) => Nil()
+    }
   }
 
   def slice(from: BigInt, to: BigInt): List[T] = {
diff --git a/testcases/repair/List/List4.scala b/testcases/repair/List/List4.scala
index b6cb5e276741be29d86da86b7c43cbe7e1639c62..1ee180b3331e9cc51df34207b8ab5b6fec9b710b 100644
--- a/testcases/repair/List/List4.scala
+++ b/testcases/repair/List/List4.scala
@@ -78,16 +78,18 @@ sealed abstract class List[T] {
       }
   }
 
-  def drop(i: BigInt): List[T] = { (this, i) match {
-    case (Nil(), _) => Nil[T]()
-    case (Cons(h, t), i) =>
-      // FIXME
-      //if (i == 0) {
-      //  Cons(h, t)
-      //} else {
-        t.drop(i-1)
-      //}
-  }} ensuring { ((this, i), _) passes { 
+  def drop(i: BigInt): List[T] = {
+    (this, i) match {
+      case (Nil(), _) => Nil[T]()
+      case (Cons(h, t), i) =>
+        // FIXME
+        if (i != 0) {
+          Cons(h, t)
+        } else {
+          t.drop(i-1)
+        }
+    }
+  } ensuring { ((this, i), _) passes { 
     case (Cons(_, Nil()), BigInt(42)) => Nil()
     case (l@Cons(_, _), BigInt(0)) => l
     case (Cons(a, Cons(b, Nil())), BigInt(1)) => Cons(b, Nil())
diff --git a/testcases/repair/List/List5.scala b/testcases/repair/List/List5.scala
index 743cced6533536eac8c03bbc3f2381378b8190b8..f13f91da3d55d7cdcf0eb0d3ef41027e1a8e94d8 100644
--- a/testcases/repair/List/List5.scala
+++ b/testcases/repair/List/List5.scala
@@ -97,11 +97,11 @@ sealed abstract class List[T] {
     case Nil() => Nil[T]()
     case Cons(h, t) =>
       val r = t.replace(from, to)
-      //if (h == from) { FIXME
-      //  Cons(to, r)
-      //} else {
+      if (h != from) { // FIXME
+        Cons(to, r)
+      } else {
         Cons(h, r)
-      //}
+      }
   }} ensuring { res => 
     (((this.content -- Set(from)) ++ (if (this.content contains from) Set(to) else Set[T]())) == res.content) &&
     res.size == this.size
diff --git a/testcases/repair/List/List7.scala b/testcases/repair/List/List7.scala
index 7eef0585e9cb467f75da05fdb7957db4f9838afa..41972f4cefffa0bd63245856b2d31b0cfe241c10 100644
--- a/testcases/repair/List/List7.scala
+++ b/testcases/repair/List/List7.scala
@@ -191,7 +191,7 @@ sealed abstract class List[T] {
       }
   }} ensuring { res =>
     if (this.content contains e) {
-      res.isDefined && this.size > res.get && this.apply(res.get) == e
+      res.isDefined && this.size > res.get && this.apply(res.get) == e && res.get >= 0
     } else {
       res.isEmpty
     }
diff --git a/testcases/repair/List/List8.scala b/testcases/repair/List/List8.scala
index faf7571e9582f652e3ba494b11eb34c5923d4dac..02f5294c26e7f3b4f29e307db07186927bfff82c 100644
--- a/testcases/repair/List/List8.scala
+++ b/testcases/repair/List/List8.scala
@@ -191,7 +191,7 @@ sealed abstract class List[T] {
       }
   }} ensuring { res =>
     if (this.content contains e) {
-      res.isDefined && this.size > res.get && this.apply(res.get) == e
+      res.isDefined && this.size > res.get && this.apply(res.get) == e && res.get >= 0
     } else {
       res.isEmpty
     }
diff --git a/testcases/repair/List/List9.scala b/testcases/repair/List/List9.scala
index 12a8152b1701fe993f36c33392eebda724ec4aad..104e2ecabdfa0ac8bef8cc179ff68acc1a7c6ccc 100644
--- a/testcases/repair/List/List9.scala
+++ b/testcases/repair/List/List9.scala
@@ -191,7 +191,7 @@ sealed abstract class List[T] {
       }
   }} ensuring { res =>
     if (this.content contains e) {
-      res.isDefined && this.size > res.get && this.apply(res.get) == e
+      res.isDefined && this.size > res.get && this.apply(res.get) == e && res.get >= 0
     } else {
       res.isEmpty
     }
diff --git a/testcases/repair/MergeSort/MergeSort1.scala b/testcases/repair/MergeSort/MergeSort1.scala
index 88b0319086023675c766cf8f6c74ccd420d2a182..340dfbc46077306b64752e73cebeb725ef40a781 100644
--- a/testcases/repair/MergeSort/MergeSort1.scala
+++ b/testcases/repair/MergeSort/MergeSort1.scala
@@ -5,7 +5,7 @@ object MergeSort {
   def split(l : List[BigInt]) : (List[BigInt],List[BigInt]) = { l match {
     case Cons(a, Cons(b, t)) => 
       val (rec1, rec2) = split(t)
-      (rec1, rec2) // FIXME: Forgot a,b
+      (rec1, Cons(b, rec2)) // FIXME: Forgot a
     case other => (other, Nil[BigInt]())
   }} ensuring { res =>
     val (l1, l2) = res
diff --git a/testcases/repair/runTests.sh b/testcases/repair/runTests.sh
index 55ca5cdf9f74828855e9ce85eb8aa18bf8ba3169..896054f51dc75131d690b14dfa00dd8a3a747c46 100755
--- a/testcases/repair/runTests.sh
+++ b/testcases/repair/runTests.sh
@@ -15,53 +15,56 @@ echo "################################" >> $summaryLog
 echo "#           Category,                 File,             function, p.S, fuS, foS,   Tms,   Fms,   Rms, verif?" >> $summaryLog
 
 #All benchmarks:
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=desugar  testcases/repair/Compiler/Compiler1.scala   | tee -a $fullLog
-./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=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/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
+echo "=====================================================================" >> repair-report.txt
 
-./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
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=nnf      testcases/repair/PropLogic/PropLogic3.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=nnf      testcases/repair/PropLogic/PropLogic4.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=nnf      testcases/repair/PropLogic/PropLogic5.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar  testcases/repair/Compiler/Compiler1.scala   | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar  testcases/repair/Compiler/Compiler2.scala   | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar  testcases/repair/Compiler/Compiler3.scala   | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar  testcases/repair/Compiler/Compiler4.scala   | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar  testcases/repair/Compiler/Compiler5.scala   | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=simplify testcases/repair/Compiler/Compiler6.scala   | tee -a $fullLog
 
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=pad     testcases/repair/List/List1.scala           | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=++      testcases/repair/List/List2.scala           | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=:+      testcases/repair/List/List3.scala           | tee -a $fullLog
-./leon --repair --timeout=30                       --functions=drop    testcases/repair/List/List4.scala           | tee -a $fullLog
-./leon --repair --timeout=30                       --functions=replace testcases/repair/List/List5.scala           | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=count   testcases/repair/List/List6.scala           | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=find    testcases/repair/List/List7.scala           | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=find    testcases/repair/List/List8.scala           | tee -a $fullLog
-./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 --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge    testcases/repair/Heap/Heap3.scala        | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge    testcases/repair/Heap/Heap4.scala        | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge    testcases/repair/Heap/Heap5.scala        | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge    testcases/repair/Heap/Heap6.scala        | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge    testcases/repair/Heap/Heap7.scala        | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge    testcases/repair/Heap/Heap10.scala       | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=insert   testcases/repair/Heap/Heap8.scala        | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=makeN    testcases/repair/Heap/Heap9.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
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=nnf      testcases/repair/PropLogic/PropLogic1.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=nnf      testcases/repair/PropLogic/PropLogic2.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=nnf      testcases/repair/PropLogic/PropLogic3.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=nnf      testcases/repair/PropLogic/PropLogic4.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=nnf      testcases/repair/PropLogic/PropLogic5.scala | tee -a $fullLog
+
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=pad     testcases/repair/List/List1.scala           | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=++      testcases/repair/List/List2.scala           | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=:+      testcases/repair/List/List3.scala           | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30                       --functions=replace testcases/repair/List/List5.scala           | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=count   testcases/repair/List/List6.scala           | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=find    testcases/repair/List/List7.scala           | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=find    testcases/repair/List/List8.scala           | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30                       --functions=find    testcases/repair/List/List9.scala           | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=size    testcases/repair/List/List10.scala          | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=sum     testcases/repair/List/List11.scala          | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=-       testcases/repair/List/List12.scala          | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30                       --functions=drop    testcases/repair/List/List4.scala           | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=drop    testcases/repair/List/List13.scala          | tee -a $fullLog
+
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=power    testcases/repair/Numerical/Numerical1.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=moddiv   testcases/repair/Numerical/Numerical3.scala | tee -a $fullLog
+
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=split    testcases/repair/MergeSort/MergeSort1.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge    testcases/repair/MergeSort/MergeSort2.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge    testcases/repair/MergeSort/MergeSort3.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge    testcases/repair/MergeSort/MergeSort4.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge    testcases/repair/MergeSort/MergeSort5.scala | tee -a $fullLog
 
 # Average results
-cat $log >> $summaryLog
-awk '{ total1 += $7; total2 += $8; total3 += $9; count++ } END { printf "#%74s Avg: %5d, %5d, %5d\n\n", "", total1/count, total2/count, total3/count }' $log >> $summaryLog
+#cat $log >> $summaryLog
+#awk '{ total1 += $7; total2 += $8; total3 += $9; count++ } END { printf "#%74s Avg: %5d, %5d, %5d\n\n", "", total1/count, total2/count, total3/count }' $log >> $summaryLog
 
diff --git a/testcases/synthesis/etienne-thesis/AddressBook/Make.scala b/testcases/synthesis/etienne-thesis/AddressBook/Make.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1fd12466c2c6f932f776c893a66e1a290d2212ca
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/AddressBook/Make.scala
@@ -0,0 +1,53 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object AddressBookMake {
+
+  case class Address[A](info: A, priv: Boolean)
+
+  sealed abstract class AddressList[A] {
+    def size: BigInt = {
+      this match {
+        case Nil() => BigInt(0)
+        case Cons(head, tail) => BigInt(1) + tail.size
+      }
+    } ensuring { res => res >= 0 }
+
+    def content: Set[Address[A]] = this match {
+      case Nil() => Set[Address[A]]()
+      case Cons(addr, l1) => Set(addr) ++ l1.content
+    }
+  }
+
+  case class Cons[A](a: Address[A], tail: AddressList[A]) extends AddressList[A]
+  case class Nil[A]() extends AddressList[A]
+
+  def allPersonal[A](l: AddressList[A]): Boolean = l match {
+    case Nil() => true
+    case Cons(a, l1) =>
+      if (a.priv) allPersonal(l1)
+      else false
+  }
+
+  def allBusiness[A](l: AddressList[A]): Boolean = l match {
+    case Nil() => true
+    case Cons(a, l1) =>
+      if (a.priv) false
+      else allBusiness(l1)
+  }
+
+  case class AddressBook[A](business: AddressList[A], personal: AddressList[A]) {
+    def size: BigInt = business.size + personal.size
+
+    def content: Set[Address[A]] = business.content ++ personal.content
+
+    def invariant = {
+      allPersonal(personal) && allBusiness(business)
+    }
+  }
+
+  def makeAddressBook[A](as: AddressList[A]): AddressBook[A] = {
+    choose( (res: AddressBook[A]) => res.content == as.content && res.invariant )
+  }
+}
diff --git a/testcases/synthesis/etienne-thesis/AddressBook/Merge.scala b/testcases/synthesis/etienne-thesis/AddressBook/Merge.scala
new file mode 100644
index 0000000000000000000000000000000000000000..92a5b5bfef213e35c4f2a76bbbc9f295e406d1f4
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/AddressBook/Merge.scala
@@ -0,0 +1,69 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object AddressBookMake {
+
+  case class Address[A](info: A, priv: Boolean)
+
+  sealed abstract class AddressList[A] {
+    def size: BigInt = {
+      this match {
+        case Nil() => BigInt(0)
+        case Cons(head, tail) => BigInt(1) + tail.size
+      }
+    } ensuring { res => res >= 0 }
+
+    def content: Set[Address[A]] = this match {
+      case Nil() => Set[Address[A]]()
+      case Cons(addr, l1) => Set(addr) ++ l1.content
+    }
+
+    def ++(that: AddressList[A]): AddressList[A] = {
+      this match {
+        case Cons(h, t) => Cons(h, t ++ that)
+        case Nil() => that
+      }
+    } ensuring {
+      res => res.content == this.content ++ that.content
+    }
+  }
+
+  case class Cons[A](a: Address[A], tail: AddressList[A]) extends AddressList[A]
+  case class Nil[A]() extends AddressList[A]
+
+  def allPersonal[A](l: AddressList[A]): Boolean = l match {
+    case Nil() => true
+    case Cons(a, l1) =>
+      if (a.priv) allPersonal(l1)
+      else false
+  }
+
+  def allBusiness[A](l: AddressList[A]): Boolean = l match {
+    case Nil() => true
+    case Cons(a, l1) =>
+      if (a.priv) false
+      else allBusiness(l1)
+  }
+
+  case class AddressBook[A](business: AddressList[A], personal: AddressList[A]) {
+    def size: BigInt = business.size + personal.size
+
+    def content: Set[Address[A]] = business.content ++ personal.content
+
+    @inline
+    def invariant = {
+      allPersonal(personal) && allBusiness(business)
+    }
+  }
+
+  def merge[A](a1: AddressBook[A], a2: AddressBook[A]): AddressBook[A] = {
+    require(a1.invariant && a2.invariant)
+
+    choose( (res: AddressBook[A]) =>
+      res.personal.content == (a1.personal.content ++ a2.personal.content) &&
+      res.business.content == (a1.business.content ++ a2.business.content) &&
+      res.invariant
+    )
+  }
+}
diff --git a/testcases/synthesis/etienne-thesis/BatchedQueue/Dequeue.scala b/testcases/synthesis/etienne-thesis/BatchedQueue/Dequeue.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c44fc062847b9af2264a9b3bba05186a313ab36b
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/BatchedQueue/Dequeue.scala
@@ -0,0 +1,80 @@
+import leon.lang._
+import leon.lang.synthesis._
+
+object BatchedQueue {
+  sealed abstract class List[T] {
+    def content: Set[T] = {
+      this match {
+        case Cons(h, t) => Set(h) ++ t.content
+        case Nil() => Set()
+      }
+    }
+
+    def size: BigInt = {
+      this match {
+        case Cons(h, t) => BigInt(1) + t.size
+        case Nil() => BigInt(0)
+      }
+    } ensuring { _ >= 0 }
+
+    def reverse: List[T] = {
+      this match {
+        case Cons(h, t) => t.reverse.append(Cons(h, Nil[T]()))
+        case Nil() => Nil[T]()
+      }
+    } ensuring { res =>
+      this.content == res.content
+    }
+
+    def append(r: List[T]): List[T] = {
+      this match {
+        case Cons(h, t) => Cons(h, t.append(r))
+        case Nil() => r
+      }
+    }
+
+    def isEmpty: Boolean = {
+      this == Nil[T]()
+    }
+
+    def tail: List[T] = {
+      require(this != Nil[T]())
+      this match {
+        case Cons(h, t) => t
+      }
+    }
+
+    def head: T = {
+      require(this != Nil[T]())
+      this match {
+        case Cons(h, t) => h
+      }
+    }
+  }
+
+  case class Cons[T](h: T, t: List[T]) extends List[T]
+  case class Nil[T]() extends List[T]
+
+  case class Queue[T](f: List[T], r: List[T]) {
+    def content: Set[T] = f.content ++ r.content
+    def size: BigInt = f.size + r.size
+
+    def isEmpty: Boolean = f.isEmpty && r.isEmpty
+
+    def invariant: Boolean = {
+      (f.isEmpty) ==> (r.isEmpty)
+    }
+
+    def toList: List[T] = f.append(r.reverse)
+
+    def dequeue: Queue[T] = {
+      require(invariant && !isEmpty)
+
+      choose { (res: Queue[T]) =>
+        res.size == size-1 && res.toList == this.toList.tail && res.invariant
+      }
+    }
+  }
+
+  val test = Queue[BigInt](Cons(42, Nil()), Nil()).dequeue
+}
diff --git a/testcases/synthesis/etienne-thesis/BatchedQueue/Enqueue.scala b/testcases/synthesis/etienne-thesis/BatchedQueue/Enqueue.scala
new file mode 100644
index 0000000000000000000000000000000000000000..fe01946d158153d2dd9ae2a3be2234ee4cd18aa9
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/BatchedQueue/Enqueue.scala
@@ -0,0 +1,88 @@
+import leon.lang._
+import leon.lang.synthesis._
+
+object BatchedQueue {
+  sealed abstract class List[T] {
+    def content: Set[T] = {
+      this match {
+        case Cons(h, t) => Set(h) ++ t.content
+        case Nil() => Set()
+      }
+    }
+
+    def size: BigInt = {
+      this match {
+        case Cons(h, t) => BigInt(1) + t.size
+        case Nil() => BigInt(0)
+      }
+    } ensuring { _ >= 0 }
+
+    def reverse: List[T] = {
+      this match {
+        case Cons(h, t) => t.reverse.append(Cons(h, Nil[T]()))
+        case Nil() => Nil[T]()
+      }
+    } ensuring { res =>
+      this.content == res.content
+    }
+
+    def append(r: List[T]): List[T] = {
+      this match {
+        case Cons(h, t) => Cons(h, t.append(r))
+        case Nil() => r
+      }
+    }
+
+    def tail: List[T] = {
+      require(this != Nil[T]())
+      this match {
+        case Cons(h, t) => t
+      }
+    }
+
+    def head: T = {
+      require(this != Nil[T]())
+      this match {
+        case Cons(h, t) => h
+      }
+    }
+
+    def last: T = {
+      require(this != Nil[T]())
+      this match {
+        case Cons(h, Nil()) => h
+        case Cons(h, t) => t.last
+      }
+    }
+  }
+
+  case class Cons[T](h: T, t: List[T]) extends List[T]
+  case class Nil[T]() extends List[T]
+
+  case class Queue[T](f: List[T], r: List[T]) {
+    def content: Set[T] = f.content ++ r.content
+    def size: BigInt = f.size + r.size
+
+    def invariant: Boolean = {
+      (f == Nil[T]()) ==> (r == Nil[T]())
+    }
+
+    def toList: List[T] = f.append(r.reverse)
+
+    def enqueue(v: T): Queue[T] = {
+      require(invariant)
+
+      f match {
+        case Cons(h, t) =>
+          Queue(f, Cons(v, r))
+        case Nil() =>
+          Queue(Cons(v, f), Nil())
+      }
+
+    } ensuring { (res: Queue[T]) =>
+        res.invariant &&
+        res.toList.last == v &&
+        res.content == this.content ++ Set(v)
+    }
+  }
+}
diff --git a/testcases/synthesis/etienne-thesis/Compiler/Desugar.scala b/testcases/synthesis/etienne-thesis/Compiler/Desugar.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2684c71b2b8bbc9e5fe6cc307899ca7b92d366b4
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/Compiler/Desugar.scala
@@ -0,0 +1,118 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon._
+
+object Compiler {
+  abstract class Expr
+  case class Plus(lhs: Expr, rhs: Expr) extends Expr
+  case class Minus(lhs: Expr, rhs: Expr) extends Expr
+  case class UMinus(e: Expr) extends Expr
+  case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+  case class And(lhs: Expr, rhs: Expr) extends Expr
+  case class Implies(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 BoolLiteral(b : Boolean) extends Expr
+  case class IntLiteral(i: BigInt) extends Expr
+
+  abstract class Value
+  case class BoolValue(b: Boolean) extends Value
+  case class IntValue(i: BigInt) extends Value
+  case object Error extends Value
+
+  def eval(e: Expr): Value = e match {
+    case Plus(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => IntValue(il+ir)
+        case _ => Error
+      }
+
+    case Minus(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => IntValue(il-ir)
+        case _ => Error
+      }
+
+    case UMinus(l) =>
+      eval(l) match {
+        case IntValue(b) => IntValue(-b)
+        case _ => Error
+      }
+
+    case LessThan(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => BoolValue(il < ir)
+        case _ => Error
+      }
+
+    case And(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(false) => b
+        case b: BoolValue =>
+          eval(r)
+        case _ =>
+          Error
+      }
+
+    case Or(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(true) =>
+          b
+        case b: BoolValue =>
+          eval(r)
+        case _ =>
+          Error
+      }
+
+    case Implies(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(true) =>
+          eval(r)
+        case b @ BoolValue(false) =>
+          BoolValue(true)
+        case _ => Error
+      }
+
+    case Not(l) =>
+      eval(l) match {
+        case BoolValue(b) => BoolValue(!b)
+        case _ => Error
+      }
+
+    case Eq(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir))   => BoolValue(il == ir)
+        case (BoolValue(il), BoolValue(ir)) => BoolValue(il == ir)
+        case _ => Error
+      }
+
+    case Ite(c, t, e) =>
+      eval(c) match {
+        case BoolValue(true) => eval(t)
+        case BoolValue(false) => eval(t)
+        case _ => Error
+      }
+
+    case IntLiteral(l)  => IntValue(l)
+    case BoolLiteral(b) => BoolValue(b)
+  }
+
+  def rewriteMinus(in: Minus): Expr = {
+    choose{ (out: Expr) =>
+      eval(in) == eval(out) && !(out.isInstanceOf[Minus])
+    }
+  }
+
+  def rewriteImplies(in: Implies): Expr = {
+    choose{ (out: Expr) =>
+      eval(in) == eval(out) && !(out.isInstanceOf[Implies])
+    }
+  }
+
+
+  def plop(x: Expr) = {
+    eval(x) == Error//eval(Not(IntLiteral(BigInt(2))))
+  }.holds
+}
diff --git a/testcases/synthesis/etienne-thesis/Compiler/DesugarImplies.scala b/testcases/synthesis/etienne-thesis/Compiler/DesugarImplies.scala
new file mode 100644
index 0000000000000000000000000000000000000000..de5c544ff368043ca7847376af8cd9ae6b513f4d
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/Compiler/DesugarImplies.scala
@@ -0,0 +1,144 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon._
+
+object Compiler {
+  abstract class Expr
+  case class Plus(lhs: Expr, rhs: Expr) extends Expr
+  case class Minus(lhs: Expr, rhs: Expr) extends Expr
+  case class UMinus(e: Expr) extends Expr
+  case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+  case class And(lhs: Expr, rhs: Expr) extends Expr
+  case class Implies(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 BoolLiteral(b : Boolean) extends Expr
+  case class IntLiteral(i: BigInt) extends Expr
+
+  def exists(e: Expr, f: Expr => Boolean): Boolean = {
+    f(e) || (e match {
+      case Plus(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Minus(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case LessThan(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case And(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Or(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Implies(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Eq(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Ite(c, t, e) => exists(c, f) || exists(t, f) || exists(e, f)
+      case Not(e) => exists(e, f)
+      case UMinus(e) => exists(e, f)
+      case _ => false
+    })
+  }
+
+  abstract class Value
+  case class BoolValue(b: Boolean) extends Value
+  case class IntValue(i: BigInt) extends Value
+  case object Error extends Value
+
+  def eval(e: Expr): Value = e match {
+    case Plus(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => IntValue(il+ir)
+        case _ => Error
+      }
+
+    case Minus(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => IntValue(il-ir)
+        case _ => Error
+      }
+
+    case UMinus(l) =>
+      eval(l) match {
+        case IntValue(b) => IntValue(-b)
+        case _ => Error
+      }
+
+    case LessThan(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => BoolValue(il < ir)
+        case _ => Error
+      }
+
+    case And(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(false) => b
+        case b: BoolValue =>
+          eval(r)
+        case _ =>
+          Error
+      }
+
+    case Or(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(true) =>
+          b
+        case b: BoolValue =>
+          eval(r)
+        case _ =>
+          Error
+      }
+
+    case Implies(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(true) =>
+          eval(r)
+        case b @ BoolValue(false) =>
+          BoolValue(true)
+        case _ => Error
+      }
+
+    case Not(l) =>
+      eval(l) match {
+        case BoolValue(b) => BoolValue(!b)
+        case _ => Error
+      }
+
+    case Eq(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir))   => BoolValue(il == ir)
+        case (BoolValue(il), BoolValue(ir)) => BoolValue(il == ir)
+        case _ => Error
+      }
+
+    case Ite(c, t, e) =>
+      eval(c) match {
+        case BoolValue(true) => eval(t)
+        case BoolValue(false) => eval(t)
+        case _ => Error
+      }
+
+    case IntLiteral(l)  => IntValue(l)
+    case BoolLiteral(b) => BoolValue(b)
+  }
+
+
+  //def desugar(e: Expr): Expr = {
+  //  choose{ (out: Expr) =>
+  //    eval(e) == eval(out) && !exists(out, f => f.isInstanceOf[Implies])
+  //  }
+  //}
+
+  def desugar(e: Expr): Expr = {
+    e match {
+      case Plus(lhs, rhs) => Plus(desugar(lhs), desugar(rhs))
+      case Minus(lhs, rhs) => Minus(desugar(lhs), desugar(rhs))
+      case LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
+      case And(lhs, rhs) => And(desugar(lhs), desugar(rhs))
+      case Or(lhs, rhs) => Or(desugar(lhs), desugar(rhs))
+      case Implies(lhs, rhs) => //Implies(desugar(lhs), desugar(rhs))
+        Or(Not(desugar(lhs)), desugar(rhs))
+      case Eq(lhs, rhs) => Eq(desugar(lhs), desugar(rhs))
+      case Ite(c, t, e) => Ite(desugar(c), desugar(t), desugar(e))
+      case Not(e) => Not(desugar(e))
+      case UMinus(e) => UMinus(desugar(e))
+      case e => e
+    }
+  } ensuring { out =>
+    //eval(e) == eval(out) && 
+    !exists(out, f => f.isInstanceOf[Implies])
+  }
+}
diff --git a/testcases/synthesis/etienne-thesis/Compiler/RewriteImplies.scala b/testcases/synthesis/etienne-thesis/Compiler/RewriteImplies.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4b50b9cbe34043f65d1a8feeaadac929822e6c70
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/Compiler/RewriteImplies.scala
@@ -0,0 +1,124 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon._
+
+object Compiler {
+  abstract class Expr
+  case class Plus(lhs: Expr, rhs: Expr) extends Expr
+  case class Minus(lhs: Expr, rhs: Expr) extends Expr
+  case class UMinus(e: Expr) extends Expr
+  case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+  case class And(lhs: Expr, rhs: Expr) extends Expr
+  case class Implies(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 BoolLiteral(b : Boolean) extends Expr
+  case class IntLiteral(i: BigInt) extends Expr
+
+  def exists(e: Expr, f: Expr => Boolean): Boolean = {
+    f(e) || (e match {
+      case Plus(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Minus(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case LessThan(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case And(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Or(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Implies(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Eq(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Ite(c, t, e) => exists(c, f) || exists(t, f) || exists(e, f)
+      case Not(e) => exists(e, f)
+      case UMinus(e) => exists(e, f)
+      case _ => false
+    })
+  }
+
+  abstract class Value
+  case class BoolValue(b: Boolean) extends Value
+  case class IntValue(i: BigInt) extends Value
+  case object Error extends Value
+
+  def eval(e: Expr): Value = e match {
+    case Plus(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => IntValue(il+ir)
+        case _ => Error
+      }
+
+    case Minus(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => IntValue(il-ir)
+        case _ => Error
+      }
+
+    case UMinus(l) =>
+      eval(l) match {
+        case IntValue(b) => IntValue(-b)
+        case _ => Error
+      }
+
+    case LessThan(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => BoolValue(il < ir)
+        case _ => Error
+      }
+
+    case And(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(false) => b
+        case b: BoolValue =>
+          eval(r)
+        case _ =>
+          Error
+      }
+
+    case Or(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(true) =>
+          b
+        case b: BoolValue =>
+          eval(r)
+        case _ =>
+          Error
+      }
+
+    case Implies(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(true) =>
+          eval(r)
+        case b @ BoolValue(false) =>
+          BoolValue(true)
+        case _ => Error
+      }
+
+    case Not(l) =>
+      eval(l) match {
+        case BoolValue(b) => BoolValue(!b)
+        case _ => Error
+      }
+
+    case Eq(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir))   => BoolValue(il == ir)
+        case (BoolValue(il), BoolValue(ir)) => BoolValue(il == ir)
+        case _ => Error
+      }
+
+    case Ite(c, t, e) =>
+      eval(c) match {
+        case BoolValue(true) => eval(t)
+        case BoolValue(false) => eval(t)
+        case _ => Error
+      }
+
+    case IntLiteral(l)  => IntValue(l)
+    case BoolLiteral(b) => BoolValue(b)
+  }
+
+
+  def desugar(in: Expr): Expr = {
+    choose{ (out: Expr) =>
+      eval(in) == eval(out) && !(out.isInstanceOf[Implies])
+    }
+  }
+}
diff --git a/testcases/synthesis/etienne-thesis/Compiler/RewriteMinus.scala b/testcases/synthesis/etienne-thesis/Compiler/RewriteMinus.scala
new file mode 100644
index 0000000000000000000000000000000000000000..de2fa4360de5fa899110b43c171e592be5282803
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/Compiler/RewriteMinus.scala
@@ -0,0 +1,107 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon._
+
+object Compiler {
+  abstract class Expr
+  case class Plus(lhs: Expr, rhs: Expr) extends Expr
+  case class Minus(lhs: Expr, rhs: Expr) extends Expr
+  case class UMinus(e: Expr) extends Expr
+  case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+  case class And(lhs: Expr, rhs: Expr) extends Expr
+  case class Implies(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 BoolLiteral(b : Boolean) extends Expr
+  case class IntLiteral(i: BigInt) extends Expr
+
+  abstract class Value
+  case class BoolValue(b: Boolean) extends Value
+  case class IntValue(i: BigInt) extends Value
+  case object Error extends Value
+
+  def eval(e: Expr): Value = e match {
+    case Plus(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => IntValue(il+ir)
+        case _ => Error
+      }
+
+    case Minus(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => IntValue(il-ir)
+        case _ => Error
+      }
+
+    case UMinus(l) =>
+      eval(l) match {
+        case IntValue(b) => IntValue(-b)
+        case _ => Error
+      }
+
+    case LessThan(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => BoolValue(il < ir)
+        case _ => Error
+      }
+
+    case And(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(false) => b
+        case b: BoolValue =>
+          eval(r)
+        case _ =>
+          Error
+      }
+
+    case Or(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(true) =>
+          b
+        case b: BoolValue =>
+          eval(r)
+        case _ =>
+          Error
+      }
+
+    case Implies(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(true) =>
+          eval(r)
+        case b @ BoolValue(false) =>
+          BoolValue(true)
+        case _ => Error
+      }
+
+    case Not(l) =>
+      eval(l) match {
+        case BoolValue(b) => BoolValue(!b)
+        case _ => Error
+      }
+
+    case Eq(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir))   => BoolValue(il == ir)
+        case (BoolValue(il), BoolValue(ir)) => BoolValue(il == ir)
+        case _ => Error
+      }
+
+    case Ite(c, t, e) =>
+      eval(c) match {
+        case BoolValue(true) => eval(t)
+        case BoolValue(false) => eval(t)
+        case _ => Error
+      }
+
+    case IntLiteral(l)  => IntValue(l)
+    case BoolLiteral(b) => BoolValue(b)
+  }
+
+  def rewriteMinus(in: Minus): Expr = {
+    choose{ (out: Expr) =>
+      eval(in) == eval(out) && !(out.isInstanceOf[Minus])
+    }
+  }
+}
diff --git a/testcases/synthesis/etienne-thesis/List/Delete.scala b/testcases/synthesis/etienne-thesis/List/Delete.scala
index 46f0710878d25a30e679f034ff07f985078950d1..30716c5919256f052d0a0e741a147d30c5bc82fa 100644
--- a/testcases/synthesis/etienne-thesis/List/Delete.scala
+++ b/testcases/synthesis/etienne-thesis/List/Delete.scala
@@ -7,7 +7,7 @@ object Delete {
   case class Cons(head: BigInt, tail: List) extends List
   case object Nil extends List
 
-  def size(l: List) : BigInt = (l match {
+  def size(l: List): BigInt = (l match {
     case Nil => BigInt(0)
     case Cons(_, t) => BigInt(1) + size(t)
   }) ensuring(res => res >= 0)
@@ -17,25 +17,10 @@ object Delete {
     case Cons(i, t) => Set(i) ++ content(t)
   }
 
-  def insert(in1: List, v: BigInt): List = {
-    Cons(v, in1)
-  } ensuring { content(_) == content(in1) ++ Set(v) }
-
-  //def delete(in1: List, v: BigInt): List = {
-  //  in1 match {
-  //    case Cons(h,t) =>
-  //      if (h == v) {
-  //        delete(t, v)
-  //      } else {
-  //        Cons(h, delete(t, v))
-  //      }
-  //    case Nil =>
-  //      Nil
-  //  }
-  //} ensuring { content(_) == content(in1) -- Set(v) }
-
-  def delete(in1: List, v: BigInt) = choose {
+  def delete(in: List, v: BigInt) = {
+    ???[List]
+  } ensuring {
     (out : List) =>
-      content(out) == content(in1) -- Set(v)
+      content(out) == content(in) -- Set(v)
   }
 }
diff --git a/testcases/synthesis/etienne-thesis/SortedList/Delete.scala b/testcases/synthesis/etienne-thesis/SortedList/Delete.scala
new file mode 100644
index 0000000000000000000000000000000000000000..788f232d35449cff75ac27442ce7e9cb50f42391
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/SortedList/Delete.scala
@@ -0,0 +1,34 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListDelete {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List): BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  def isSorted(list: List): Boolean = list match {
+    case Nil => true
+    case Cons(_, Nil) => true
+    case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+    case Cons(_, xs) => isSorted(xs)
+  }
+
+  def delete(in: List, v: BigInt) = {
+    require(isSorted(in))
+
+    choose( (res : List) =>
+        (content(res) == content(in) -- Set(v)) && isSorted(res)
+    )
+  }
+}
diff --git a/testcases/synthesis/etienne-thesis/SortedList/Diff.scala b/testcases/synthesis/etienne-thesis/SortedList/Diff.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d391b85ba60e2b405530ddb45b40d94071263725
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/SortedList/Diff.scala
@@ -0,0 +1,53 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListDiff {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List): BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  def isSorted(list: List): Boolean = list match {
+    case Nil => true
+    case Cons(_, Nil) => true
+    case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+    case Cons(_, xs) => isSorted(xs)
+  }
+
+  def delete(in1: List, v: BigInt): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h,t) =>
+        if (h < v) {
+          Cons(h, delete(t, v))
+        } else if (h == v) {
+          delete(t, v)
+        } else {
+          in1
+        }
+      case Nil =>
+        Nil
+    }
+  } ensuring { res => content(res) == content(in1) -- Set(v) && isSorted(res) }
+
+
+  def diff(in1: List, in2: List) = {
+    require(isSorted(in1) && isSorted(in2))
+
+    choose {
+      (out : List) =>
+        (content(out) == content(in1) -- content(in2)) && isSorted(out)
+    }
+  }
+
+}
diff --git a/testcases/synthesis/etienne-thesis/SortedList/Insert.scala b/testcases/synthesis/etienne-thesis/SortedList/Insert.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0bf80d1e99cef290e602b0da905d6966713c77b7
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/SortedList/Insert.scala
@@ -0,0 +1,34 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListInsert {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List): BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  def isSorted(list: List): Boolean = list match {
+    case Nil => true
+    case Cons(_, Nil) => true
+    case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+    case Cons(_, xs) => isSorted(xs)
+  }
+
+  def insert(in1: List, v: BigInt): List = {
+    require(isSorted(in1))
+
+    choose { (out : List) =>
+      (content(out) == content(in1) ++ Set(v)) && isSorted(out)
+    }
+  }
+}
diff --git a/testcases/synthesis/etienne-thesis/SortedList/InsertAlways.scala b/testcases/synthesis/etienne-thesis/SortedList/InsertAlways.scala
new file mode 100644
index 0000000000000000000000000000000000000000..73e0b240d776780fab6ac8091a8f0c925c56e695
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/SortedList/InsertAlways.scala
@@ -0,0 +1,34 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListInsertAlways {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List): BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  def isSorted(list: List): Boolean = list match {
+    case Nil => true
+    case Cons(_, Nil) => true
+    case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+    case Cons(_, xs) => isSorted(xs)
+  }
+
+  def insertAlways(in1: List, v: BigInt) = {
+    require(isSorted(in1))
+
+    choose{ (out : List) =>
+      (content(out) == content(in1) ++ Set(v)) && isSorted(out) && size(out) == size(in1) + 1
+    }
+  }
+}
diff --git a/testcases/synthesis/etienne-thesis/SortedList/InsertionSort.scala b/testcases/synthesis/etienne-thesis/SortedList/InsertionSort.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0752ad33fe2249de829d7180e6facaab8fb6e160
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/SortedList/InsertionSort.scala
@@ -0,0 +1,49 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListInsertionSort {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List): BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  def isSorted(list: List): Boolean = list match {
+    case Nil => true
+    case Cons(_, Nil) => true
+    case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+    case Cons(_, xs) => isSorted(xs)
+  }
+
+  def insert(in1: List, v: BigInt): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h, t) =>
+        if (v < h) {
+          Cons(v, in1)
+        } else if (v == h) {
+          in1
+        } else {
+          Cons(h, insert(t, v))
+        }
+      case Nil =>
+        Cons(v, Nil)
+    }
+
+  } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
+
+  def insertionSort(in1: List): List = {
+    choose { (out: List) =>
+      content(out) == content(in1) && isSorted(out)
+    }
+  }
+}
diff --git a/testcases/synthesis/etienne-thesis/SortedList/Union.scala b/testcases/synthesis/etienne-thesis/SortedList/Union.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d3f11adcccc07e44d1b82c1c6aed7144cb30523c
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/SortedList/Union.scala
@@ -0,0 +1,51 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListUnion {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List): BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  def isSorted(list: List): Boolean = list match {
+    case Nil => true
+    case Cons(_, Nil) => true
+    case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+    case Cons(_, xs) => isSorted(xs)
+  }
+
+  def insert(in1: List, v: BigInt): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h, t) =>
+        if (v < h) {
+          Cons(v, in1)
+        } else if (v == h) {
+          in1
+        } else {
+          Cons(h, insert(t, v))
+        }
+      case Nil =>
+        Cons(v, Nil)
+    }
+
+  } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
+
+  def union(in1: List, in2: List) = {
+    require(isSorted(in1) && isSorted(in2))
+    choose {
+      (out : List) =>
+       (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+    }
+  }
+}
diff --git a/testcases/synthesis/etienne-thesis/StrictSortedList/Delete.scala b/testcases/synthesis/etienne-thesis/StrictSortedList/Delete.scala
new file mode 100644
index 0000000000000000000000000000000000000000..23999d96c3577b80b00b252e0c07509f4b4b2176
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/StrictSortedList/Delete.scala
@@ -0,0 +1,34 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object StrictSortedListDelete {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List): BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  def isSorted(list: List): Boolean = list match {
+    case Nil => true
+    case Cons(_, Nil) => true
+    case Cons(x1, Cons(x2, _)) if(x1 >= x2) => false
+    case Cons(_, xs) => isSorted(xs)
+  }
+
+  def delete(in: List, v: BigInt) = {
+    require(isSorted(in))
+
+    choose( (res : List) =>
+        (content(res) == content(in) -- Set(v)) && isSorted(res)
+    )
+  }
+}
diff --git a/testcases/synthesis/etienne-thesis/StrictSortedList/Insert.scala b/testcases/synthesis/etienne-thesis/StrictSortedList/Insert.scala
new file mode 100644
index 0000000000000000000000000000000000000000..65f3c01f9d7b7d8d45136196a6289088df46fa22
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/StrictSortedList/Insert.scala
@@ -0,0 +1,34 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object StrictSortedListInsert {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List): BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  def isSorted(list: List): Boolean = list match {
+    case Nil => true
+    case Cons(_, Nil) => true
+    case Cons(x1, Cons(x2, _)) if(x1 >= x2) => false
+    case Cons(_, xs) => isSorted(xs)
+  }
+
+  def insert(in1: List, v: BigInt): List = {
+    require(isSorted(in1))
+
+    choose { (out : List) =>
+      (content(out) == content(in1) ++ Set(v)) && isSorted(out)
+    }
+  }
+}
diff --git a/testcases/synthesis/etienne-thesis/StrictSortedList/Union.scala b/testcases/synthesis/etienne-thesis/StrictSortedList/Union.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c10ed419d3c2cc4fefc9690efb37bc723799ef1c
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/StrictSortedList/Union.scala
@@ -0,0 +1,51 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object StrictSortedListUnion {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List): BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  def isSorted(list: List): Boolean = list match {
+    case Nil => true
+    case Cons(_, Nil) => true
+    case Cons(x1, Cons(x2, _)) if(x1 >= x2) => false
+    case Cons(_, xs) => isSorted(xs)
+  }
+
+  def insert(in1: List, v: BigInt): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h, t) =>
+        if (v < h) {
+          Cons(v, in1)
+        } else if (v == h) {
+          in1
+        } else {
+          Cons(h, insert(t, v))
+        }
+      case Nil =>
+        Cons(v, Nil)
+    }
+
+  } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
+
+  def union(in1: List, in2: List) = {
+    require(isSorted(in1) && isSorted(in2))
+    choose {
+      (out : List) =>
+       (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+    }
+  }
+}
diff --git a/testcases/synthesis/etienne-thesis/UnaryNumerals/Add.scala b/testcases/synthesis/etienne-thesis/UnaryNumerals/Add.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a34d1834fbb5cc2418ca830c5576e64d74169b4f
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/UnaryNumerals/Add.scala
@@ -0,0 +1,21 @@
+import leon.lang._
+import leon.lang.synthesis._
+
+object UnaryNumeralsAdd {
+  sealed abstract class Num
+  case object Z extends Num
+  case class  S(pred: Num) extends Num
+
+  def value(n: Num): BigInt = {
+    n match {
+      case Z => BigInt(0)
+      case S(p) => BigInt(1) + value(p)
+    }
+  } ensuring (_ >= 0)
+
+  def add(x: Num, y: Num): Num = {
+    choose { (r : Num) =>
+      value(r) == value(x) + value(y)
+    }
+  }
+}
diff --git a/testcases/synthesis/etienne-thesis/UnaryNumerals/Distinct.scala b/testcases/synthesis/etienne-thesis/UnaryNumerals/Distinct.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4287378d1f95225e4ff1ffae57b2d0579d72c3a5
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/UnaryNumerals/Distinct.scala
@@ -0,0 +1,30 @@
+import leon.lang._
+import leon.lang.synthesis._
+
+object UnaryNumeralsDistinct {
+  sealed abstract class Num
+  case object Z extends Num
+  case class  S(pred: Num) extends Num
+
+  def value(n: Num): BigInt = {
+    n match {
+      case Z => BigInt(0)
+      case S(p) => BigInt(1) + value(p)
+    }
+  } ensuring (_ >= 0)
+
+  def add(x: Num, y: Num): Num = {
+    x match {
+      case S(p) => S(add(p, y))
+      case Z => y
+    }
+  } ensuring { (r : Num) =>
+    value(r) == value(x) + value(y)
+  }
+
+  def distinct(x: Num, y: Num): Num = {
+    choose { (r : Num) =>
+      r != x && r != y
+    }
+  }
+}
diff --git a/testcases/synthesis/etienne-thesis/UnaryNumerals/Mult.scala b/testcases/synthesis/etienne-thesis/UnaryNumerals/Mult.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bfa39365e8a8b35555ddc2265f40c775251b8d17
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/UnaryNumerals/Mult.scala
@@ -0,0 +1,30 @@
+import leon.lang._
+import leon.lang.synthesis._
+
+object UnaryNumeralsMult {
+  sealed abstract class Num
+  case object Z extends Num
+  case class  S(pred: Num) extends Num
+
+  def value(n: Num): BigInt = {
+    n match {
+      case Z => BigInt(0)
+      case S(p) => BigInt(1) + value(p)
+    }
+  } ensuring (_ >= 0)
+
+  def add(x: Num, y: Num): Num = {
+    x match {
+      case S(p) => S(add(p, y))
+      case Z => y
+    }
+  } ensuring { (r : Num) =>
+    value(r) == value(x) + value(y)
+  }
+
+  def mult(x: Num, y: Num): Num = {
+    choose { (r : Num) =>
+      value(r) == value(x) * value(y)
+    }
+  }
+}
diff --git a/testcases/synthesis/etienne-thesis/run.sh b/testcases/synthesis/etienne-thesis/run.sh
new file mode 100755
index 0000000000000000000000000000000000000000..ee64d86702076bf5ff909c3437f321498a2afe68
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/run.sh
@@ -0,0 +1,43 @@
+#!/bin/bash
+
+function run {
+    cmd="./leon --debug=report --timeout=30 --synthesis $1"
+    echo "Running " $cmd
+    echo "------------------------------------------------------------------------------------------------------------------"
+    $cmd;
+}
+
+echo "==================================================================================================================" >> synthesis-report.txt
+# These are all the benchmarks included in my thesis
+# List
+run testcases/synthesis/etienne-thesis/List/Insert.scala
+run testcases/synthesis/etienne-thesis/List/Delete.scala
+run testcases/synthesis/etienne-thesis/List/Union.scala
+run testcases/synthesis/etienne-thesis/List/Diff.scala
+run testcases/synthesis/etienne-thesis/List/Split.scala
+
+# SortedList
+run testcases/synthesis/etienne-thesis/SortedList/Insert.scala
+run testcases/synthesis/etienne-thesis/SortedList/InsertAlways.scala
+run testcases/synthesis/etienne-thesis/SortedList/Delete.scala
+run testcases/synthesis/etienne-thesis/SortedList/Union.scala
+run testcases/synthesis/etienne-thesis/SortedList/Diff.scala
+run testcases/synthesis/etienne-thesis/SortedList/InsertionSort.scala
+
+# StrictSortedList
+run testcases/synthesis/etienne-thesis/StrictSortedList/Insert.scala
+run testcases/synthesis/etienne-thesis/StrictSortedList/Delete.scala
+run testcases/synthesis/etienne-thesis/StrictSortedList/Union.scala
+
+# UnaryNumerals
+run testcases/synthesis/etienne-thesis/UnaryNumerals/Add.scala
+run testcases/synthesis/etienne-thesis/UnaryNumerals/Distinct.scala
+run testcases/synthesis/etienne-thesis/UnaryNumerals/Mult.scala
+
+# BatchedQueue
+#run testcases/synthesis/etienne-thesis/BatchedQueue/Enqueue.scala
+run testcases/synthesis/etienne-thesis/BatchedQueue/Dequeue.scala
+
+# AddressBook
+#run testcases/synthesis/etienne-thesis/AddressBook/Make.scala
+run testcases/synthesis/etienne-thesis/AddressBook/Merge.scala