diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 4e32e619b3f6e8dac3d4e3b1a91a12254856968e..3139208d7af193da40f391b0cd7cea799fb8d8db 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -7,6 +7,7 @@ import purescala.Common._
 import purescala.Definitions._
 import purescala.Trees._
 import purescala.TypeTrees._
+import codegen.runtime.LeonCodeGenRuntimeMonitor
 
 import cafebabe._
 import cafebabe.AbstractByteCodes._
@@ -120,7 +121,7 @@ class CompilationUnit(val ctx: LeonContext,
   // Currently, this method is only used to prepare arguments to reflective calls.
   // This means it is safe to return AnyRef (as opposed to primitive types), because
   // reflection needs this anyway.
-  private[codegen] def exprToJVM(e: Expr): AnyRef = e match {
+  private[codegen] def exprToJVM(e: Expr)(implicit monitor : LeonCodeGenRuntimeMonitor): AnyRef = e match {
     case IntLiteral(v) =>
       new java.lang.Integer(v)
 
@@ -131,12 +132,13 @@ class CompilationUnit(val ctx: LeonContext,
       e
 
     case Tuple(elems) =>
-      tupleConstructor.newInstance(elems.map(exprToJVM).toArray).asInstanceOf[AnyRef]
+      tupleConstructor.newInstance(elems.map(exprToJVM _).toArray).asInstanceOf[AnyRef]
 
     case CaseClass(cct, args) =>
       caseClassConstructor(cct.classDef) match {
         case Some(cons) =>
-          cons.newInstance(args.map(exprToJVM).toArray : _*).asInstanceOf[AnyRef]
+          val realArgs = if (params.requireMonitor) monitor +: args.map(exprToJVM _) else  args.map(exprToJVM _)
+          cons.newInstance(realArgs.toArray : _*).asInstanceOf[AnyRef]
         case None =>
           ctx.reporter.fatalError("Case class constructor not found?!?")
       }
@@ -148,7 +150,7 @@ class CompilationUnit(val ctx: LeonContext,
 
     // Just slightly overkill...
     case _ =>
-      compileExpression(e, Seq()).evalToJVM(Seq())
+      compileExpression(e, Seq()).evalToJVM(Seq(),monitor)
   }
 
   // Note that this may produce untyped expressions! (typically: sets, maps)
diff --git a/src/main/scala/leon/codegen/CompiledExpression.scala b/src/main/scala/leon/codegen/CompiledExpression.scala
index 1bc72443b7521ae121199028ae14ece23c98eead..08a8c3b5b21d0e4d45bbbab7949ad5e331ce4342 100644
--- a/src/main/scala/leon/codegen/CompiledExpression.scala
+++ b/src/main/scala/leon/codegen/CompiledExpression.scala
@@ -14,11 +14,12 @@ import cafebabe.ByteCodes._
 import cafebabe.ClassFileTypes._
 import cafebabe.Flags._
 
-import runtime.LeonCodeGenRuntimeMonitor
+import runtime.{LeonCodeGenRuntimeMonitor => LM }
 
 import java.lang.reflect.InvocationTargetException
 
 class CompiledExpression(unit: CompilationUnit, cf: ClassFile, expression : Expr, argsDecl: Seq[Identifier]) {
+
   private lazy val cl = unit.loader.loadClass(cf.className)
   private lazy val meth = cl.getMethods()(0)
 
@@ -26,15 +27,15 @@ class CompiledExpression(unit: CompilationUnit, cf: ClassFile, expression : Expr
 
   private val params = unit.params
 
-  def argsToJVM(args: Seq[Expr]): Seq[AnyRef] = {
-    args.map(unit.exprToJVM)
+  def argsToJVM(args: Seq[Expr], monitor: LM): Seq[AnyRef] = {
+    args.map(unit.exprToJVM(_)(monitor))
   }
 
-  def evalToJVM(args: Seq[AnyRef]): AnyRef = {
+  def evalToJVM(args: Seq[AnyRef], monitor: LM): AnyRef = {
     assert(args.size == argsDecl.size)
 
     val realArgs = if (params.requireMonitor) {
-      new LeonCodeGenRuntimeMonitor(params.maxFunctionInvocations) +: args
+      monitor +: args
     } else {
       args
     }
@@ -48,9 +49,9 @@ class CompiledExpression(unit: CompilationUnit, cf: ClassFile, expression : Expr
 
   // This may throw an exception. We unwrap it if needed.
   // We also need to reattach a type in some cases (sets, maps).
-  def evalFromJVM(args: Seq[AnyRef]) : Expr = {
+  def evalFromJVM(args: Seq[AnyRef], monitor: LM) : Expr = {
     try {
-      val result = unit.jvmToExpr(evalToJVM(args))
+      val result = unit.jvmToExpr(evalToJVM(args, monitor))
       if(!result.isTyped) {
         result.setType(exprType)
       }
@@ -62,7 +63,9 @@ class CompiledExpression(unit: CompilationUnit, cf: ClassFile, expression : Expr
 
   def eval(args: Seq[Expr]) : Expr = {
     try {
-      evalFromJVM(argsToJVM(args))
+      val monitor = 
+        new LM(params.maxFunctionInvocations)
+      evalFromJVM(argsToJVM(args, monitor),monitor)
     } catch {
       case ite : InvocationTargetException => throw ite.getCause()
     }
diff --git a/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala b/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
index ea1c685eb2e482c911bc4a39e6849107073cbfa4..2a129e34f74a328c137a0dca8ac0b478ab84f7ae 100644
--- a/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
+++ b/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
@@ -70,7 +70,7 @@ object ChooseEntryPoint {
           ctx.reporter.debug("Synthesis took "+total+"ms")
           ctx.reporter.debug("Finished synthesis with "+leonRes.asString(ctx))
 
-          unit.exprToJVM(leonRes)
+          unit.exprToJVM(leonRes)(new LeonCodeGenRuntimeMonitor(unit.params.maxFunctionInvocations))
         case Some(false) =>
           throw new LeonCodeGenRuntimeException("Constraint is UNSAT")
         case _ =>
diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index 284a050099bcf7137c17a54d2f635d28b90ac7de..1dbb5caa3bba8ac814ea9bd7d1374f30771c5cc7 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -11,6 +11,7 @@ import purescala.TypeTrees._
 import purescala.Extractors.TopLevelAnds
 
 import codegen.CompilationUnit
+import codegen.runtime.LeonCodeGenRuntimeMonitor
 import vanuatoo.{Pattern => VPattern, _}
 
 import evaluators._
@@ -189,9 +190,10 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
 
       Some((args : Tuple) => {
         try {
-          val jvmArgs = ce.argsToJVM(Seq(args))
+          val monitor = new LeonCodeGenRuntimeMonitor(unit.params.maxFunctionInvocations)
+          val jvmArgs = ce.argsToJVM(Seq(args), monitor )
 
-          val result  = ce.evalFromJVM(jvmArgs)
+          val result  = ce.evalFromJVM(jvmArgs, monitor)
 
           // jvmArgs is getting updated by evaluating
           val pattern = valueToPattern(jvmArgs(0), ttype)