From 5eac0ae159e5047b3cec4b0d3d0c10ee9d738ae7 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 25 Sep 2015 10:23:26 +0200
Subject: [PATCH] more req constructor

---
 src/main/scala/leon/purescala/ExprOps.scala | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 6a8c9ac57..836282b09 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)
-- 
GitLab