diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 228158152b81609e1531a4f7674549bdcb170313..c24201f719ea0b365c08ffef7afafaafd29dd72f 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1003,8 +1003,8 @@ object ExprOps extends GenTreeOps[Expr] {
     postMap(transform, applyRec = true)(expr)
   }
 
-  def simplifyPaths(sf: SolverFactory[Solver], initC: List[Expr] = Nil): Expr => Expr = {
-    new SimplifierWithPaths(sf, initC).transform
+  def simplifyPaths(sf: SolverFactory[Solver], initPC: Path = Path.empty): Expr => Expr = {
+    new SimplifierWithPaths(sf, initPC).transform
   }
 
   trait Traverser[T] {
@@ -1020,7 +1020,7 @@ object ExprOps extends GenTreeOps[Expr] {
   }
 
   trait CollectorWithPaths[T] extends TransformerWithPC with Traverser[Seq[T]] {
-    protected val initPath: Seq[Expr] = Nil
+    protected val initPath: Path = Path.empty
 
     private var results: Seq[T] = Nil
 
@@ -1040,11 +1040,11 @@ object ExprOps extends GenTreeOps[Expr] {
 
     def traverse(e: Expr): Seq[T] = traverse(e, initPath)
 
-    def traverse(e: Expr, init: Expr): Seq[T] = traverse(e, Seq(init))
+    def traverse(e: Expr, init: Expr): Seq[T] = traverse(e, Path(init))
 
-    def traverse(e: Expr, init: Seq[Expr]): Seq[T] = {
+    def traverse(e: Expr, init: Path): Seq[T] = {
       results = Nil
-      rec(e, Path(init))
+      rec(e, init)
       results
     }
   }
@@ -1765,7 +1765,7 @@ object ExprOps extends GenTreeOps[Expr] {
 
           val newFd = fdOuter.duplicate()
 
-          val simp = Simplifiers.bestEffort(ctx, p) _
+          val simp = Simplifiers.bestEffort(ctx, p)((_: Expr))
 
           newFd.body          = fdInner.body.map(b => simplePreTransform(pre)(b))
           newFd.precondition  = mergePre(fdOuter.precondition, fdInner.precondition).map(simp)
@@ -2127,7 +2127,7 @@ object ExprOps extends GenTreeOps[Expr] {
   }
 
 
-  def simpleCorrectnessCond(e: Expr, path: List[Expr], sf: SolverFactory[Solver]): Expr = {
+  def simpleCorrectnessCond(e: Expr, path: Path, sf: SolverFactory[Solver]): Expr = {
     simplifyPaths(sf, path)(
       andJoin( collectCorrectnessConditions(e) map { _._2 } )
     )
diff --git a/src/main/scala/leon/purescala/SimplifierWithPaths.scala b/src/main/scala/leon/purescala/SimplifierWithPaths.scala
index b6cf9e65730ff0a2806ff8633cd096eec52293c8..ad56da7f47131cbf9a0a2cdbd0fa6edb0c3e243b 100644
--- a/src/main/scala/leon/purescala/SimplifierWithPaths.scala
+++ b/src/main/scala/leon/purescala/SimplifierWithPaths.scala
@@ -10,7 +10,7 @@ import Extractors._
 import Constructors._
 import solvers._
 
-class SimplifierWithPaths(sf: SolverFactory[Solver], override val initPath: List[Expr] = Nil) extends TransformerWithPC {
+class SimplifierWithPaths(sf: SolverFactory[Solver], val initPath: Path = Path.empty) extends TransformerWithPC {
 
   val solver = SimpleSolverAPI(sf)
 
diff --git a/src/main/scala/leon/purescala/TransformerWithPC.scala b/src/main/scala/leon/purescala/TransformerWithPC.scala
index 53e67568477a94305b077d87e0c6827172717d89..95b2c89d4bb976f20b9ab628131fee53a4d7dbf1 100644
--- a/src/main/scala/leon/purescala/TransformerWithPC.scala
+++ b/src/main/scala/leon/purescala/TransformerWithPC.scala
@@ -3,12 +3,10 @@
 package leon
 package purescala
 
-import Common._
 import Expressions._
 import Constructors._
 import Extractors._
 import ExprOps._
-import Types._
 
 /** Traverses/ transforms expressions with path condition awareness.
   *
@@ -19,7 +17,7 @@ import Types._
 abstract class TransformerWithPC extends Transformer {
 
   /** The initial path condition */
-  protected val initPath: Seq[Expr]
+  protected val initPath: Path
 
   protected def rec(e: Expr, path: Path): Expr = e match {
     case Let(i, v, b) =>
@@ -108,7 +106,7 @@ abstract class TransformerWithPC extends Transformer {
   }
 
   def transform(e: Expr): Expr = {
-    rec(e, Path(initPath))
+    rec(e, initPath)
   }
 }
 
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index bb0b047fd72cc7a46ddefebd0fe35cd173721425..ec009623d0f930464d0947369986a7c0f7b8f475 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -9,6 +9,7 @@ import purescala.Types.{TypeTree,TupleType}
 import purescala.Definitions._
 import purescala.ExprOps._
 import purescala.Constructors._
+import purescala.Path
 
 import leon.utils.Simplifiers
 
@@ -55,7 +56,7 @@ class Solution(val pre: Expr, val defs: Set[FunDef], val term: Expr, val isTrust
 
 
   def toSimplifiedExpr(ctx: LeonContext, p: Program, within: FunDef): Expr = {
-    withoutSpec(Simplifiers.bestEffort(ctx, p)(req(within.precOrTrue, toExpr))).get
+    Simplifiers.bestEffort(ctx, p)(toExpr, Path(within.precOrTrue))
   }
 }
 
diff --git a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
index 90c4ecbb382db36b4bb653d62e2b206cfa3c1e7b..65e5dd1acffe5bafbdcd9a5edbac52d2af600e66 100644
--- a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
+++ b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
@@ -16,7 +16,7 @@ import purescala.Types.CaseClassType
 case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
   def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
 
-    val simplifier = Simplifiers.bestEffort(hctx, hctx.program) _
+    val simplifier = Simplifiers.bestEffort(hctx, hctx.program)(_:Expr, p.pc)
 
     var subst = Map.empty[Identifier, Expr]
     var reverseSubst = Map.empty[Identifier, Expr]
diff --git a/src/main/scala/leon/utils/Simplifiers.scala b/src/main/scala/leon/utils/Simplifiers.scala
index 6fdcbc9da79101bbcacee65e3c16af637c9699b6..d1fe992821c17e2a5b4676e537b41a90297aaf03 100644
--- a/src/main/scala/leon/utils/Simplifiers.scala
+++ b/src/main/scala/leon/utils/Simplifiers.scala
@@ -7,16 +7,17 @@ import purescala.Definitions._
 import purescala.Expressions._
 import purescala.ExprOps._
 import purescala.ScopeSimplifier
+import purescala.Path
 import solvers._
 
 object Simplifiers {
   
-  def bestEffort(ctx: LeonContext, p: Program)(e: Expr): Expr = {
+  def bestEffort(ctx: LeonContext, p: Program)(e: Expr, pc: Path = Path.empty): Expr = {
     val solverf = SolverFactory.uninterpreted(ctx, p)
 
     try {
       val simplifiers = (simplifyLets _).
-        andThen(simplifyPaths(solverf)).
+        andThen(simplifyPaths(solverf, pc)).
         andThen(simplifyArithmetic).
         andThen(evalGround(ctx, p)).
         andThen(normalizeExpression)