diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index 51e68ca13ecddbfcd9910071bce5bbe4ec860a2c..2a221536f36cb0aafa69b3c3ccfcd180c2326241 100644
--- a/src/main/scala/leon/synthesis/Heuristics.scala
+++ b/src/main/scala/leon/synthesis/Heuristics.scala
@@ -228,7 +228,7 @@ class ADTInduction(synth: Synthesizer) extends Rule("ADT Induction", synth, 80)
 
             val subProblem = Problem(inputs ::: residualArgs, And(p.c :: postFs), subPhi, p.xs)
 
-            (subProblem, subPre, recCalls)
+            (subProblem, subPre, ccd, newIds, recCalls)
           case _ =>
             sys.error("Woops, non case-class as descendent")
         }
@@ -237,42 +237,22 @@ class ADTInduction(synth: Synthesizer) extends Rule("ADT Induction", synth, 80)
           case sols =>
             var globalPre = List[Expr]()
 
-            for ((sol, (problem, pre, calls)) <- (sols zip subProblemsInfo)) {
+            val cases = for ((sol, (problem, pre, ccd, ids, calls)) <- (sols zip subProblemsInfo)) yield {
               globalPre ::= And(pre, sol.pre)
 
+              val caze = CaseClassPattern(None, ccd, ids.map(id => WildcardPattern(Some(id))))
+              SimpleCase(caze, calls.foldLeft(sol.term){ case (t, (binders, call)) => LetTuple(binders, call, t) })
             }
 
             val funPre = subst(origId -> Variable(inductOn), Or(globalPre))
-            val outerPre = funPre
-            /*
-            solPre ::= And(pre, sol.pre)
+            val outerPre = Or(globalPre)
 
-            val preIn = Or(Seq(And(Equals(Variable(inductOn), IntLiteral(0)),      base.pre),
-                               And(GreaterThan(Variable(inductOn), IntLiteral(0)), gt.pre),
-                               And(LessThan(Variable(inductOn), IntLiteral(0)),    lt.pre)))
-            val preOut = subst(inductOn -> Variable(origId), preIn)
+            newFun.body = Some(MatchExpr(Variable(inductOn), cases))
 
-            val newFun = new FunDef(FreshIdentifier("rec", true), tpe, Seq(VarDecl(inductOn, inductOn.getType)))
-            newFun.precondition = Some(preIn)
-            newFun.postcondition = Some(And(Equals(ResultVariable(), Tuple(p.xs.map(Variable(_)))), p.phi))
-
-            newFun.body = Some(
-              IfExpr(Equals(Variable(inductOn), IntLiteral(0)),
-                base.toExpr,
-              IfExpr(GreaterThan(Variable(inductOn), IntLiteral(0)),
-                LetTuple(postXs, FunctionInvocation(newFun, Seq(Minus(Variable(inductOn), IntLiteral(1)))), gt.toExpr)
-              , LetTuple(postXs, FunctionInvocation(newFun, Seq(Plus(Variable(inductOn), IntLiteral(1)))), lt.toExpr)))
-            )
-
-
-            Solution(preOut, base.defs++gt.defs++lt.defs+newFun, FunctionInvocation(newFun, Seq(Variable(origId))))
-            */
-            Solution.none
+            Solution(Or(globalPre), sols.flatMap(_.defs).toSet+newFun, FunctionInvocation(newFun, p.as.map(Variable(_))))
         }
 
-        println(subProblemsInfo)
-
-        RuleInapplicable
+        HeuristicStep(synth, p, subProblemsInfo.map(_._1).toList, onSuccess)
       } else {
         RuleInapplicable
       }
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index e34db5cdfe86fe3a41faeb584abf5e0378147f61..52443ab53df3157c73e14d3b33236001a6982f27 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -7,7 +7,7 @@ import leon.purescala.Common._
 // Defines a synthesis triple of the form:
 // ⟦ as ⟨ C | phi ⟩ xs ⟧
 case class Problem(as: List[Identifier], c: Expr, phi: Expr, xs: List[Identifier]) {
-  override def toString = "⟦ "+as.mkString(";")+" ⟨ "+c+" | "+phi+" ⟩ "+xs.mkString(";")+" ⟧ "
+  override def toString = "⟦ "+as.mkString(";")+", "+c+" ==> ⟨ "+phi+" ⟩ "+xs.mkString(";")+" ⟧ "
 
   val complexity: ProblemComplexity = ProblemComplexity(this)
 }
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 70bfbea92737651e26904e7663086eacc22762c6..216da2afb587c7045b2dbfc02a1fa8acc3064a7f 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -24,8 +24,8 @@ object Rules {
     new OptimisticGround(_),
     new EqualitySplit(_),
     new CEGIS(_),
-    new Assert(_)
-    //new IntegerEquation(_)
+    new Assert(_),
+    new IntegerEquation(_)
   )
 }
 
@@ -517,7 +517,7 @@ class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", syn
   }
 }
 
-class EqualitySplit(synth: Synthesizer) extends Rule("Eq. Split.", synth, 10) {
+class EqualitySplit(synth: Synthesizer) extends Rule("Eq. Split.", synth, 90) {
   def applyOn(task: Task): RuleResult = {
     val p = task.problem