diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 68161e9e4e93600f2df7be787b9db8f4af796e3c..b532c2e7ca48607d06dcfbe392642a1b5982835a 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -34,6 +34,7 @@ object Main {
     Logger.debug("Default action on program: " + program, 3, "main")
     val passManager = new PassManager(Seq(ArrayTransformation, EpsilonElimination, ImperativeCodeElimination, /*UnitElimination,*/ FunctionClosure, FunctionHoisting, Simplificator))
     val program2 = passManager.run(program)
+    assert(program2.isPure)
     val analysis = new Analysis(program2, reporter)
     analysis.analyse
   }
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index 6b9ef14e5d419082c8901fd2bef62121ec150a76..70ad6d68f23ae28eb35ef916a18525975692ae5b 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -830,6 +830,10 @@ trait CodeExtraction extends Extractors {
         }
         case ExIfThenElse(t1,t2,t3) => {
           val r1 = rec(t1)
+          if(containsLetDef(r1)) {
+            unit.error(t1.pos, "Condition of if-then-else expression should not contain nested function definition")
+            throw ImpureCodeEncounteredException(t1)
+          }
           val r2 = rec(t2)
           val r3 = rec(t3)
           IfExpr(r1, r2, r3).setType(leastUpperBound(r2.getType, r3.getType))
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index df83d6b197faee4ec2a398987268a4d46afd0b50..f73530c40f116add5cfbb1fa4b511c82d3c17d55 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -53,6 +53,7 @@ object Definitions {
     def isCatamorphism(f1: FunDef) = mainObject.isCatamorphism(f1)
     def caseClassDef(name: String) = mainObject.caseClassDef(name)
     def allIdentifiers : Set[Identifier] = mainObject.allIdentifiers + id
+    def isPure: Boolean = definedFunctions.forall(fd => fd.body.forall(Trees.isPure) && fd.precondition.forall(Trees.isPure) && fd.postcondition.forall(Trees.isPure))
   }
 
   /** Objects work as containers for class definitions, functions (def's) and
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 93bf6fd97268f1e95cdca875edc7e39c58040eb0..5dc158b42c94a08b7fc38167bfb69b97f902369a 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -816,13 +816,18 @@ object Trees {
     searchAndReplaceDFS(applyToTree)(expr)
   }
 
-  //checking whether the expr is pure, that is do not contains any non-pure construct: assign, while and blocks
+  //checking whether the expr is pure, that is do not contains any non-pure construct: assign, while, blocks, array, ...
+  //this is expected to be true when entering the "backend" of Leon
   def isPure(expr: Expr): Boolean = {
     def convert(t: Expr) : Boolean = t match {
       case Block(_, _) => false
       case Assignment(_, _) => false
       case While(_, _) => false
       case LetVar(_, _, _) => false
+      case LetDef(_, _) => false
+      case ArrayUpdate(_, _, _) => false
+      case ArrayFill(_, _) => false
+      case Epsilon(_) => false
       case _ => true
     }
     def combine(b1: Boolean, b2: Boolean) = b1 && b2
@@ -831,6 +836,10 @@ object Trees {
       case Assignment(_, _) => false
       case While(_, _) => false
       case LetVar(_, _, _) => false
+      case LetDef(_, _) => false
+      case ArrayUpdate(_, _, _) => false
+      case ArrayFill(_, _) => false
+      case Epsilon(_) => false
       case _ => b
     }
     treeCatamorphism(convert, combine, compute, expr)