diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 02a04e27022ef3c5a8a9110c8f938a4e502452b5..bf6785e4b0ce2fcd4dd597d3c52733426f3e5d4e 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -41,7 +41,7 @@ object Rules {
     Unification.OccursCheck, // probably useless
     Disunification.Decomp,
     ADTDual,
-    //OnePoint,
+    OnePoint,
     Ground,
     CaseSplit,
     IndependentSplit,
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/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/runTests.sh b/testcases/repair/runTests.sh
index fb92991cba1b5b0725b794f6d8cfd6c14f95cd05..896054f51dc75131d690b14dfa00dd8a3a747c46 100755
--- a/testcases/repair/runTests.sh
+++ b/testcases/repair/runTests.sh
@@ -18,21 +18,22 @@ echo "#           Category,                 File,             function, p.S, fuS
 
 echo "=====================================================================" >> repair-report.txt
 
-./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 --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 --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 --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 --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
@@ -40,22 +41,22 @@ echo "=====================================================================" >>
 #./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=drop    testcases/repair/List/List4.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 --solvers=fairz3,enum --functions=drop    testcases/repair/List/List13.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=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
diff --git a/testcases/synthesis/etienne-thesis/BatchedQueue/Enqueue.scala b/testcases/synthesis/etienne-thesis/BatchedQueue/Enqueue.scala
index 87e030915986e5a4d9bd031011102e8d79126224..fe01946d158153d2dd9ae2a3be2234ee4cd18aa9 100644
--- a/testcases/synthesis/etienne-thesis/BatchedQueue/Enqueue.scala
+++ b/testcases/synthesis/etienne-thesis/BatchedQueue/Enqueue.scala
@@ -72,11 +72,17 @@ object BatchedQueue {
     def enqueue(v: T): Queue[T] = {
       require(invariant)
 
-      choose { (res: Queue[T]) =>
+      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])
+    }
+  }
+}