diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index fb818f1a40b48b5ce134da986e5724ddccb854cb..b1b34a54851d1c5138e93e6c02b4ca5b1471e4fa 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -290,7 +290,7 @@ object Constructors {
     */
   // @mk I simplified that because it seemed dangerous and unnessecary
   def equality(a: Expr, b: Expr) = {
-    if (a.isInstanceOf[Terminal] && !isPurelyFunctional(a) && a == b ) {
+    if (a.isInstanceOf[Terminal] && isPurelyFunctional(a) && a == b ) {
       BooleanLiteral(true)
     } else  {
       Equals(a, b)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 357c72861ac541466400df920e77ce714921abfb..bc926449cdba9384329745fff4d5d480c2aa2291 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -219,7 +219,7 @@ object ExprOps extends GenTreeOps[Expr] {
       case CaseClassSelector(cct, cc: CaseClass, id) =>
         Some(caseClassSelector(cct, cc, id))
 
-      case IfExpr(c, thenn, elze) if (thenn == elze) && !isPurelyFunctional(c) =>
+      case IfExpr(c, thenn, elze) if (thenn == elze) && isPurelyFunctional(c) =>
         Some(thenn)
 
       case IfExpr(c, BooleanLiteral(true), BooleanLiteral(false)) =>
@@ -333,10 +333,10 @@ object ExprOps extends GenTreeOps[Expr] {
   def simplifyLets(expr: Expr) : Expr = {
     def simplerLet(t: Expr) : Option[Expr] = t match {
 
-      case letExpr @ Let(i, t: Terminal, b) if !isPurelyFunctional(t) =>
+      case letExpr @ Let(i, t: Terminal, b) if isPurelyFunctional(t) =>
         Some(replaceFromIDs(Map(i -> t), b))
 
-      case letExpr @ Let(i,e,b) if !isPurelyFunctional(e) =>
+      case letExpr @ Let(i,e,b) if isPurelyFunctional(e) =>
         val occurrences = count {
           case Variable(`i`) => 1
           case _ => 0
@@ -350,7 +350,7 @@ object ExprOps extends GenTreeOps[Expr] {
           None
         }
 
-      case LetPattern(patt, e0, body) if !isPurelyFunctional(e0) =>
+      case LetPattern(patt, e0, body) if isPurelyFunctional(e0) =>
         // Will turn the match-expression with a single case into a list of lets.
 
         // Just extra safety...
@@ -991,8 +991,8 @@ object ExprOps extends GenTreeOps[Expr] {
     */
   def isPurelyFunctional(e: Expr): Boolean = {
     exists {
-      case _ : Error | _ : Choose | _: Hole | _: WithOracle => true
-      case _ => false
+      case _ : Error | _ : Choose | _: Hole | _: WithOracle => false
+      case _ => true
     }(e)
   }
 
diff --git a/src/test/scala/leon/integration/purescala/SimplifyPathsSuite.scala b/src/test/scala/leon/integration/purescala/SimplifyPathsSuite.scala
index a560f9ca4cd97f38f65c91e8c04a1a39c7dbd336..bd477c54a30bbd3dbeb938db0566d166ad498f5a 100644
--- a/src/test/scala/leon/integration/purescala/SimplifyPathsSuite.scala
+++ b/src/test/scala/leon/integration/purescala/SimplifyPathsSuite.scala
@@ -86,4 +86,16 @@ class SimplifyPathsSuite extends LeonTestSuite {
     val out = simplifyPaths(ctx, in)
     assert(out === exp)
   }
+
+  test("Simplify Paths 04 - error - 1") { ctx =>
+    val in = And(Error(BooleanType, ""), aV)
+    val out = simplifyPaths(ctx, in)
+    assert(out === in)
+  }
+
+  test("Simplify Paths 05 - error - 2") { ctx =>
+    val in = And(BooleanLiteral(false), Error(BooleanType, ""))
+    val out = simplifyPaths(ctx, in)
+    assert(out === BooleanLiteral(false))
+  }
 }