diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 07bdeb6ca6c83ef6f92491bb942495756fd33f03..d941f1c0edc81b9501eb557e87405e6b7add14fd 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -132,7 +132,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
 
             val (solSize, proof) = solutions.headOption match {
               case Some((sol, trusted)) =>
-                val solExpr = sol.toSimplifiedExpr(ctx, program)
+                val solExpr = sol.toSimplifiedExpr(ctx, program, fd)
                 val totalSolSize = formulaSize(solExpr)
                 (locSize+totalSolSize-fSize, if (trusted) "$\\chmark$" else "")
               case _ =>
@@ -162,7 +162,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
             reporter.info(ASCIIHelpers.title("Repair successful:"))
             for ( ((sol, isTrusted), i) <- solutions.zipWithIndex) {
               reporter.info(ASCIIHelpers.subTitle("Solution "+(i+1)+ (if(isTrusted) "" else " (untrusted)" ) + ":"))
-              val expr = sol.toSimplifiedExpr(ctx, synth.program)
+              val expr = sol.toSimplifiedExpr(ctx, synth.program, fd)
               reporter.info(expr.asString(program)(ctx))
             }
           }
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index d57045254ae56997ef089c57b2b906898a52921e..fd7d3fb6a52d95588c577d754fbcf5e2da91b20d 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -54,8 +54,8 @@ class Solution(val pre: Expr, val defs: Set[FunDef], val term: Expr, val isTrust
   }
 
 
-  def toSimplifiedExpr(ctx: LeonContext, p: Program): Expr = {
-    Simplifiers.bestEffort(ctx, p)(toExpr)
+  def toSimplifiedExpr(ctx: LeonContext, p: Program, within: FunDef): Expr = {
+    withoutSpec(Simplifiers.bestEffort(ctx, p)(req(within.precOrTrue, toExpr))).get
   }
 }
 
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index ad309905eac073d364580169ff962a9a24f763d9..f40117cf140fadc374364bd9037478c64136ac03 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -89,7 +89,7 @@ object SynthesisPhase extends UnitPhase[Program] {
           }
 
           solutions.headOption foreach { case (sol, _) =>
-            val expr = sol.toSimplifiedExpr(ctx, program)
+            val expr = sol.toSimplifiedExpr(ctx, program, ci.fd)
             fd.body = fd.body.map(b => replace(Map(ci.source -> expr), b))
             functions += fd
           }
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 624ec5eaaf0e9f717111fdb1df9d645a14f3599f..c81b045d09c1aeccf8e2381afe9d14cb9a11db33 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -97,7 +97,7 @@ class Synthesizer(val context : LeonContext,
 
       val (size, calls, proof) = result.headOption match {
         case Some((sol, trusted)) =>
-          val expr = sol.toSimplifiedExpr(context, program)
+          val expr = sol.toSimplifiedExpr(context, program, ci.fd)
           val pr = trusted match {
             case Some(true) => "✓"
             case Some(false) => "✗"
@@ -165,7 +165,7 @@ class Synthesizer(val context : LeonContext,
   def solutionToProgram(sol: Solution): (Program, List[FunDef]) = {
     // We replace the choose with the body of the synthesized solution
 
-    val solutionExpr = sol.toSimplifiedExpr(context, program)
+    val solutionExpr = sol.toSimplifiedExpr(context, program, ci.fd)
 
     val (npr, fdMap) = replaceFunDefs(program)({
       case fd if fd eq ci.fd =>
diff --git a/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala b/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
index cedfa529f3770581eb2541a13c37df18e8c371ba..da7f51f4fff9905542af4bfa471792da5ae86a20 100644
--- a/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
+++ b/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
@@ -40,7 +40,6 @@ class StablePrintingSuite extends LeonRegressionSuite {
       EquivalentInputs,
       UnconstrainedOutput,
       OptimisticGround,
-      EqualitySplit,
       InequalitySplit,
       rules.Assert,
       DetupleOutput,
@@ -115,7 +114,7 @@ class StablePrintingSuite extends LeonRegressionSuite {
                   case RuleExpanded(sub) =>
                     a.onSuccess(sub.map(Solution.choose)) match {
                       case Some(sol) =>
-                        val result = sol.toSimplifiedExpr(ctx, pgm)
+                        val result = sol.toSimplifiedExpr(ctx, pgm, ci.fd)
 
                         val newContent = new FileInterface(ctx.reporter).substitute(j.content, ci.source, (indent: Int) => {
                           val p = new ScalaPrinter(PrinterOptions(), Some(pgm))