diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 03f4222cd0f8cba5937d93d616e171aaf2cb58ac..65eb475622018130be3eddbaf3e7e1d8de9c21f1 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -70,7 +70,7 @@ object CodeGeneration {
     ch.freeze
   }
 
-  private[codegen] def mkExpr(e : Expr, ch : CodeHandler)(implicit env : CompilationEnvironment) {
+  private[codegen] def mkExpr(e : Expr, ch : CodeHandler, canDelegateToMkBranch : Boolean = true)(implicit env : CompilationEnvironment) {
     e match {
       case Variable(id) =>
         val slot = slotFor(id)
@@ -288,14 +288,11 @@ object CodeGeneration {
         ch << InvokeSpecial(ErrorClass, constructorName, "(Ljava/lang/String;)V")
         ch << ATHROW
 
-      // WARNING !!! See remark at the end of mkBranch ! The two functions are 
-      // mutually recursive and will loop if none supports some Boolean construct !
-      case b if b.getType == BooleanType =>
-        // println("Don't know how to mkExpr for " + b)
+      case b if b.getType == BooleanType && canDelegateToMkBranch =>
         val fl = ch.getFreshLabel("boolfalse")
         val al = ch.getFreshLabel("boolafter")
         ch << Ldc(1)
-        mkBranch(b, al, fl, ch)
+        mkBranch(b, al, fl, ch, canDelegateToMkExpr = false)
         ch << Label(fl) << POP << Ldc(0) << Label(al)
 
       case _ => throw CompilationException("Unsupported expr. : " + e) 
@@ -363,7 +360,7 @@ object CodeGeneration {
     }
   }
 
-  private[codegen] def mkBranch(cond : Expr, then : String, elze : String, ch : CodeHandler)(implicit env : CompilationEnvironment) {
+  private[codegen] def mkBranch(cond : Expr, then : String, elze : String, ch : CodeHandler, canDelegateToMkExpr : Boolean = true)(implicit env : CompilationEnvironment) {
     cond match {
       case BooleanLiteral(true) =>
         ch << Goto(then)
@@ -405,7 +402,9 @@ object CodeGeneration {
         }
 
       case Iff(l,r) =>
-        mkBranch(Equals(l, r), then, elze, ch)
+        mkExpr(l, ch)
+        mkExpr(r, ch)
+        ch << If_ICmpEq(then) << Goto(elze)
 
       case LessThan(l,r) =>
         mkExpr(l, ch)
@@ -427,12 +426,11 @@ object CodeGeneration {
         mkExpr(r, ch)
         ch << If_ICmpGe(then) << Goto(elze) 
 
-      // WARNING !!! mkBranch delegates to mkExpr, and mkExpr delegates to mkBranch !
-      // That means, between the two of them, they'd better know what to generate !
-      case other =>
-        // println("Don't know how to mkBranch for " + other)
-        mkExpr(other, ch)
+      case other if canDelegateToMkExpr =>
+        mkExpr(other, ch, canDelegateToMkBranch = false)
         ch << IfEq(elze) << Goto(then)
+
+      case other => throw CompilationException("Unsupported branching expr. : " + other) 
     }
   }
 
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index 1d2d690bc4b3a423778f503a3aaf9fd9e4c2905b..2633a1b9c6c83ca9dc30a092599aa5b1a0c01a40 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -193,6 +193,8 @@ class EvaluatorsTests extends FunSuite {
                |def and2(x : Boolean, y : Boolean) : Boolean = !(!x || !y)
                |def or2(x : Boolean, y : Boolean)  : Boolean = !(!x && !y)
                |def safe(n : Int) : Boolean = (n != 0 && (1/n == n))
+               |def mkTrue() : Boolean = true
+               |def mkFalse() : Boolean = false
                |}""".stripMargin
 
     implicit val prog = parseString(p)
@@ -221,7 +223,18 @@ class EvaluatorsTests extends FunSuite {
       checkComp(e, mkCall("safe", IL(2)), F)
 
       // This one needs short-circuit.
-      checkComp(e, mkCall("safe", IL(0)), F) 
+      checkComp(e, mkCall("safe", IL(0)), F)
+
+      // We use mkTrue/mkFalse to avoid automatic simplifications.
+      checkComp(e, Iff(mkCall("mkTrue"),  mkCall("mkTrue")),  T)
+      checkComp(e, Iff(mkCall("mkTrue"),  mkCall("mkFalse")), F)
+      checkComp(e, Iff(mkCall("mkFalse"), mkCall("mkTrue")),  F)
+      checkComp(e, Iff(mkCall("mkFalse"), mkCall("mkFalse")), T)
+
+      checkComp(e, Implies(mkCall("mkTrue"),  mkCall("mkTrue")),  T)
+      checkComp(e, Implies(mkCall("mkTrue"),  mkCall("mkFalse")), F)
+      checkComp(e, Implies(mkCall("mkFalse"), mkCall("mkTrue")),  T)
+      checkComp(e, Implies(mkCall("mkFalse"), mkCall("mkFalse")), T)
     }
   }