diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 22697b7dfd130b97eb671331afb7d1aebabdd686..9d347eccf8797ec3157929f5a58796ffaaae7cad 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -394,7 +394,12 @@ object Constructors {
     } else {
       IsInstanceOf(expr, tpe)
     }
+  }
 
+  def req(pred: Expr, body: Expr) = pred match {
+    case BooleanLiteral(true)  => body
+    case BooleanLiteral(false) => Error(body.getType, "Precondition failed")
+    case _ => Require(pred, body)
   }
 
 }
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 91d36d7a9ea16b1d1b125ca075f039b8471d6ca2..484b468bab701df3f6d557e0c562194d09ee324e 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1741,10 +1741,10 @@ object ExprOps {
     * @see [[Expressions.Require]]
     */
   def withPrecondition(expr: Expr, pred: Option[Expr]): Expr = (pred, expr) match {
-    case (Some(newPre), Require(pre, b))              => Require(newPre, b)
+    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), b)                            => Require(newPre, b)
+    case (Some(newPre), b)                            => req(newPre, b)
     case (None, Require(pre, b))                      => b
     case (None, Ensuring(Require(pre, b), p))         => Ensuring(b, p)
     case (None, b)                                    => b