diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index d9e3127880a66adcb825ee9e3ac7d77260825fc6..f715bf109d598abcbb860021b1c73b131a23e58a 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1810,7 +1810,7 @@ object ExprOps extends GenTreeOps[Expr] {
     * @see [[Expressions.Require]]
     */
   def withPath(expr: Expr, path: Path): Expr = expr match {
-    case Let(i, e, b) => Let(i, e, withPath(b, path))
+    case Let(i, e, b) => withPath(b, path withBinding (i -> e))
     case Require(pre, b) => path specs (b, pre)
     case Ensuring(Require(pre, b), post) => path specs (b, pre, post)
     case Ensuring(b, post) => path specs (b, post = post)
diff --git a/src/main/scala/leon/purescala/Path.scala b/src/main/scala/leon/purescala/Path.scala
index 3d3f329e7c5abaf7b491ae5b7037497eb02558b3..1ce4e13eb3d06185b8e0ef212a313a89e283f928 100644
--- a/src/main/scala/leon/purescala/Path.scala
+++ b/src/main/scala/leon/purescala/Path.scala
@@ -78,7 +78,13 @@ class Path private[purescala](
     val (outers, rest) = elements.span(_.isLeft)
     val cond = fold[Expr](BooleanLiteral(true), let, Constructors.and(_, _))(rest)
 
-    def wrap(e: Expr) = fold[Expr](e, let, (_, res) => res)(rest)
+    def wrap(e: Expr): Expr = {
+      val bindings = rest.collect { case Left((id, e)) => id -> e }
+      val idSubst = bindings.map(p => p._1 -> p._1.freshen).toMap
+      val substMap = idSubst.mapValues(_.toVariable)
+      val replace = replaceFromIDs(substMap, _: Expr)
+      bindings.foldRight(replace(e)) { case ((id, e), b) => let(idSubst(id), replace(e), b) }
+    }
 
     val req = Require(Constructors.and(cond, wrap(pre)), wrap(body))
     val full = post match {