diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 1b5a4bb9f351b841a3c2d2f4e9a90c56ab4e5d51..c3cc7809ddd02637e3fbc9240a870413e3bd2cf4 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -7,6 +7,7 @@ object TreeOps {
   import Common._
   import TypeTrees._
   import Definitions._
+  import xlang.Trees.LetDef
   import Trees._
   import Extractors._
 
@@ -1131,6 +1132,23 @@ object TreeOps {
   def simplifyTautologies(solver : Solver)(expr : Expr) : Expr = {
     def pre(e : Expr) = e match {
 
+      case LetDef(fd, expr) if fd.hasPrecondition =>
+       val pre = fd.precondition.get 
+
+        solver.solve(pre) match {
+          case Some(true)  =>
+            fd.precondition = None
+            
+          case Some(false) => solver.solve(Not(pre)) match {
+            case Some(true) =>
+              fd.precondition = Some(BooleanLiteral(false))
+            case _ =>
+          }
+          case None =>
+        }
+
+        e
+
       case IfExpr(cond, then, elze) => 
         try {
           solver.solve(cond) match {