diff --git a/src/main/java/leon/codegen/runtime/LeonCodeGenEvaluationException.java b/src/main/java/leon/codegen/runtime/LeonCodeGenEvaluationException.java
new file mode 100644
index 0000000000000000000000000000000000000000..f4ba02da88eb58be609efdec67261b2bd76b8141
--- /dev/null
+++ b/src/main/java/leon/codegen/runtime/LeonCodeGenEvaluationException.java
@@ -0,0 +1,11 @@
+package leon.codegen.runtime;
+
+/** Such exceptions are thrown when the evaluator is asked to do something it
+ *  cannot do, for instance evaluating a `choose` expression. It should be
+ *  distinguished from `LeonCodeGenRuntimeException`s, which are thrown when
+ *  the evaluator runs into a runtime error (.get on an undefined map, etc.). */
+public class LeonCodeGenEvaluationException extends Exception {
+    public LeonCodeGenEvaluationException(String msg) {
+        super(msg);
+    }
+}
diff --git a/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeException.java b/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeException.java
index 39cb3bfc1f24379ea396e1d8fc66d79de67d8432..8a3e6b86adab93792c76cc282e48133a453c32e4 100644
--- a/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeException.java
+++ b/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeException.java
@@ -1,5 +1,7 @@
 package leon.codegen.runtime;
 
+/** Such exceptions are thrown when the evaluator encounters a runtime error,
+ *  for instance `.get` with an undefined key on a map. */
 public class LeonCodeGenRuntimeException extends Exception {
     public LeonCodeGenRuntimeException(String msg) {
         super(msg);
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 65eb475622018130be3eddbaf3e7e1d8de9c21f1..11e57f36e328139b633a2dd66668c5e6f13099b8 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -22,6 +22,7 @@ object CodeGeneration {
   private val MapClass       = "leon/codegen/runtime/Map"
   private val CaseClassClass = "leon/codegen/runtime/CaseClass"
   private val ErrorClass     = "leon/codegen/runtime/LeonCodeGenRuntimeException"
+  private val ImpossibleEvaluationClass = "leon/codegen/runtime/LeonCodeGenEvaluationException"
 
   def defToJVMName(p : Program, d : Definition) : String = "Leon$CodeGen$" + d.id.uniqueName
 
@@ -288,6 +289,12 @@ object CodeGeneration {
         ch << InvokeSpecial(ErrorClass, constructorName, "(Ljava/lang/String;)V")
         ch << ATHROW
 
+      case Choose(_, _) =>
+        ch << New(ImpossibleEvaluationClass) << DUP
+        ch << Ldc("Cannot execute choose.")
+        ch << InvokeSpecial(ImpossibleEvaluationClass, constructorName, "(Ljava/lang/String;)V")
+        ch << ATHROW
+
       case b if b.getType == BooleanType && canDelegateToMkBranch =>
         val fl = ch.getFreshLabel("boolfalse")
         val al = ch.getFreshLabel("boolafter")
diff --git a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
index 9b9702f31621c41d8f233c68690cc99d1ebe1356..c9f6bed912c88b5d101027efd0836e1ca6649e85 100644
--- a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
+++ b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
@@ -45,6 +45,9 @@ class CodeGenEvaluator(ctx : LeonContext, val unit : CompilationUnit) extends Ev
         // and the check above would fail.
         case t : Throwable if t.getClass.toString.endsWith("LeonCodeGenRuntimeException") => 
           EvaluationFailure(t.getMessage)
+
+        case t : Throwable if t.getClass.toString.endsWith("LeonCodeGenEvaluationException") => 
+          EvaluationError(t.getMessage)
       }
     })
   }
diff --git a/src/main/scala/leon/evaluators/DefaultEvaluator.scala b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
index a6998f10b2ee4807844be3c40b5487b925e1b045..9b0bbdc2e0f47c5f5b454b9c8d4580113e89afca 100644
--- a/src/main/scala/leon/evaluators/DefaultEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
@@ -284,6 +284,9 @@ class DefaultEvaluator(ctx : LeonContext, prog : Program) extends Evaluator(ctx,
           BooleanLiteral(newArgs.distinct.size == newArgs.size)
         } 
 
+        case Choose(_, _) =>
+          throw EvalError("Cannot evaluate choose.")
+
         case other => {
           context.reporter.error("Error: don't know how to handle " + other + " in Evaluator.")
           throw EvalError("Unhandled case in Evaluator : " + other) 
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index 2633a1b9c6c83ca9dc30a092599aa5b1a0c01a40..d832950cc131c84d874c299aa00e0df94719aefb 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -141,6 +141,19 @@ class EvaluatorsTests extends FunSuite {
     }
   }
 
+  private def checkEvaluatorError(evaluator : Evaluator, in : Expr) {
+    evaluator.eval(in) match {
+      case EvaluationFailure(msg) =>
+        throw new AssertionError("Evaluation of '%s' with evaluator '%s' should have produced an internal error, but it failed instead (%s).".format(in, evaluator.name, msg))
+
+      case EvaluationSuccessful(result) =>
+        throw new AssertionError("Evaluation of '%s' with evaluator '%s' should have produced an internal error, but it produced the result '%s' instead.".format(in, evaluator.name, result))
+
+      case EvaluationError(_) =>
+        // that's the desired outcome
+    }
+  }
+
   private def T = BooleanLiteral(true)
   private def F = BooleanLiteral(false)
   private def IL(i : Int) = IntLiteral(i)
@@ -357,4 +370,21 @@ class EvaluatorsTests extends FunSuite {
       checkComp(e, MapIsDefinedAt(mkCall("finite2"), IL(3)), F)
     }
   }
+
+  test("Misc") {
+    val p = """|object Program {
+               |  import leon.Utils._
+               |
+               |  def c(i : Int) : Int = choose { (j : Int) => j > i }
+               |}
+               |""".stripMargin
+
+    implicit val prog = parseString(p)
+
+    val evaluators = prepareEvaluators
+
+    for(e <- evaluators) {
+      checkEvaluatorError(e, mkCall("c", IL(42)))
+    }
+  }
 }