diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 6a8c9ac57aa2dbd14773c8c420189526e3b5802e..836282b09fbb25f62866b8ae8c9236436ed29006 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1839,8 +1839,8 @@ object ExprOps {
     */
   def withPrecondition(expr: Expr, pred: Option[Expr]): Expr = (pred, expr) match {
     case (Some(newPre), Require(pre, b))              => req(newPre, b)
-    case (Some(newPre), Ensuring(Require(pre, b), p)) => Ensuring(Require(newPre, b), p)
-    case (Some(newPre), Ensuring(b, p))               => Ensuring(Require(newPre, b), p)
+    case (Some(newPre), Ensuring(Require(pre, b), p)) => Ensuring(req(newPre, b), p)
+    case (Some(newPre), Ensuring(b, p))               => Ensuring(req(newPre, b), p)
     case (Some(newPre), b)                            => req(newPre, b)
     case (None, Require(pre, b))                      => b
     case (None, Ensuring(Require(pre, b), p))         => Ensuring(b, p)