diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 88f1679bceda88c4d535e2f5e51b18d7e5b1b1cb..1eac956d238a9256d42277c3b15aae0e8b884672 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -25,9 +25,11 @@ import scala.collection.JavaConverters._
 import java.lang.reflect.Constructor
 
 import synthesis.Problem
+import evaluators._
 
 class CompilationUnit(val ctx: LeonContext,
                       val program: Program,
+                      val bank: EvaluationBank = new EvaluationBank,
                       val params: CodeGenParams = CodeGenParams.default) extends CodeGeneration {
 
 
diff --git a/src/main/scala/leon/codegen/runtime/Monitor.scala b/src/main/scala/leon/codegen/runtime/Monitor.scala
index e4a0afa66a578cd19bce0e83e66c626d9399c5a6..cdab9cc0e714982a664f3f8f644e5c2082845e9a 100644
--- a/src/main/scala/leon/codegen/runtime/Monitor.scala
+++ b/src/main/scala/leon/codegen/runtime/Monitor.scala
@@ -22,6 +22,7 @@ import scala.concurrent.duration._
 import solvers.SolverFactory
 import solvers.unrolling.UnrollingProcedure
 
+import evaluators._
 import synthesis._
 
 abstract class Monitor {
@@ -85,7 +86,7 @@ class StdMonitor(unit: CompilationUnit, invocationsMax: Int, bodies: ScalaMap[Id
   def invariantCheck(obj: AnyRef, tpeIdx: Int): Boolean = {
     val tpe = unit.runtimeIdToTypeMap(tpeIdx)
     val cc = unit.jvmToValue(obj, tpe).asInstanceOf[LeonCaseClass]
-    val result = evaluators.Evaluator.invariantCheck(cc)
+    val result = unit.bank.invariantCheck(cc)
     if (result.isFailure) throw new LeonCodeGenRuntimeException("ADT invariant failed @" + cc.ct.classDef.invariant.get.getPos)
     else result.isRequired
   }
@@ -93,7 +94,7 @@ class StdMonitor(unit: CompilationUnit, invocationsMax: Int, bodies: ScalaMap[Id
   def invariantResult(obj: AnyRef, tpeIdx: Int, result: Boolean): Unit = {
     val tpe = unit.runtimeIdToTypeMap(tpeIdx)
     val cc = unit.jvmToValue(obj, tpe).asInstanceOf[LeonCaseClass]
-    evaluators.Evaluator.invariantResult(cc, result)
+    unit.bank.invariantResult(cc, result)
     if (!result) throw new LeonCodeGenRuntimeException("ADT invariant failed @" + cc.ct.classDef.invariant.get.getPos)
   }
 
@@ -137,7 +138,7 @@ class StdMonitor(unit: CompilationUnit, invocationsMax: Int, bodies: ScalaMap[Id
     } else {
       val tStart = System.currentTimeMillis
 
-      val solverf = SolverFactory.getFromSettings(ctx, program).withTimeout(10.second)
+      val solverf = SolverFactory.getEvalSolver(ctx, program, unit.bank).withTimeout(10.second)
       val solver = solverf.getNewSolver()
 
       val newTypes = tps.toSeq.map(unit.runtimeIdToTypeMap(_))
@@ -222,7 +223,7 @@ class StdMonitor(unit: CompilationUnit, invocationsMax: Int, bodies: ScalaMap[Id
     } else {
       val tStart = System.currentTimeMillis
 
-      val solverf = SolverFactory.getFromSettings(ctx, program).withTimeout(.5.second)
+      val solverf = SolverFactory.getEvalSolver(ctx, program, unit.bank).withTimeout(.5.second)
       val solver = solverf.getNewSolver()
 
       val newTypes = tps.toSeq.map(unit.runtimeIdToTypeMap(_))
diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index 6e13cb030ad7df32b6a5ec1543e6d2c80915903d..ccba55af919489697d9d9e6a3aa59768d29dbab2 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -18,8 +18,8 @@ import vanuatoo.{Pattern => VPattern, _}
 
 import evaluators._
 
-class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
-  val unit = new CompilationUnit(ctx, p, CodeGenParams.default.copy(doInstrument = true))
+class VanuatooDataGen(ctx: LeonContext, p: Program, bank: EvaluationBank = new EvaluationBank) extends DataGenerator {
+  val unit = new CompilationUnit(ctx, p, bank, CodeGenParams.default.copy(doInstrument = true))
 
   val ints = (for (i <- Set(0, 1, 2, 3)) yield {
     i -> Constructor[Expr, TypeTree](List(), Int32Type, s => IntLiteral(i), ""+i)
diff --git a/src/main/scala/leon/evaluators/AngelicEvaluator.scala b/src/main/scala/leon/evaluators/AngelicEvaluator.scala
index 8230aa85845d35e0113aec976800cbe5a5f49799..26db1865b824d2fe9bae2efe3b937bb913385d72 100644
--- a/src/main/scala/leon/evaluators/AngelicEvaluator.scala
+++ b/src/main/scala/leon/evaluators/AngelicEvaluator.scala
@@ -9,11 +9,13 @@ import EvaluationResults._
 
 class AngelicEvaluator(underlying: NDEvaluator)
   extends Evaluator(underlying.context, underlying.program)
-  with DeterministicEvaluator
-{
+     with DeterministicEvaluator {
+
   val description: String = "angelic evaluator"
   val name: String = "Interpreter that returns the first solution of a non-deterministic program"
 
+  val bank = new EvaluationBank
+
   def eval(expr: Expr, model: Model): EvaluationResult = underlying.eval(expr, model) match {
     case Successful(Stream(h, _*)) =>
       Successful(h)
@@ -26,11 +28,13 @@ class AngelicEvaluator(underlying: NDEvaluator)
 
 class DemonicEvaluator(underlying: NDEvaluator)
   extends Evaluator(underlying.context, underlying.program)
-  with DeterministicEvaluator
-{
+     with DeterministicEvaluator {
+
   val description: String = "demonic evaluator"
   val name: String = "Interpreter that demands an underlying non-deterministic program has unique solution"
 
+  val bank = new EvaluationBank
+
   def eval(expr: Expr, model: Model): EvaluationResult = underlying.eval(expr, model) match {
     case Successful(Stream(h)) =>
       Successful(h)
diff --git a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
index 8521094fababa7b0679dee1bc84691a22048e822..74df09badc4cd7058a8ee152ee614ea35c1fde78 100644
--- a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
+++ b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
@@ -14,14 +14,16 @@ import codegen.CodeGenParams
 import leon.codegen.runtime.LeonCodeGenRuntimeException
 import leon.codegen.runtime.LeonCodeGenEvaluationException
 
-class CodeGenEvaluator(ctx: LeonContext, val unit : CompilationUnit) extends Evaluator(ctx, unit.program) with DeterministicEvaluator {
+class CodeGenEvaluator(ctx: LeonContext, val unit: CompilationUnit) extends Evaluator(ctx, unit.program) with DeterministicEvaluator {
 
   val name = "codegen-eval"
   val description = "Evaluator for PureScala expressions based on compilation to JVM"
 
+  val bank = unit.bank
+
   /** Another constructor to make it look more like other `Evaluator`s. */
-  def this(ctx : LeonContext, prog : Program, params: CodeGenParams = CodeGenParams.default) {
-    this(ctx, new CompilationUnit(ctx, prog, params))
+  def this(ctx: LeonContext, prog: Program, bank: EvaluationBank = new EvaluationBank, params: CodeGenParams = CodeGenParams.default) {
+    this(ctx, new CompilationUnit(ctx, prog, bank, params))
   }
 
   private def compileExpr(expression: Expr, args: Seq[Identifier]): Option[CompiledExpression] = {
diff --git a/src/main/scala/leon/evaluators/DefaultEvaluator.scala b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
index b62446c8d1916537afb315dcac7e88c69b707e21..90fb4e0b91ebe303874f9a173adc8a137af8414d 100644
--- a/src/main/scala/leon/evaluators/DefaultEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
@@ -5,7 +5,7 @@ package evaluators
 
 import purescala.Definitions.Program
 
-class DefaultEvaluator(ctx: LeonContext, prog: Program)
-  extends RecursiveEvaluator(ctx, prog, 50000)
-  with HasDefaultGlobalContext
-  with HasDefaultRecContext
+class DefaultEvaluator(ctx: LeonContext, prog: Program, bank: EvaluationBank = new EvaluationBank)
+  extends RecursiveEvaluator(ctx, prog, bank, 50000)
+     with HasDefaultGlobalContext
+     with HasDefaultRecContext
diff --git a/src/main/scala/leon/evaluators/DualEvaluator.scala b/src/main/scala/leon/evaluators/DualEvaluator.scala
index a59559185cf1b2fde266dfc20b5802867d9444a1..a99f4d4773d70f35fc981d41908f59f35856c2be 100644
--- a/src/main/scala/leon/evaluators/DualEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DualEvaluator.scala
@@ -11,15 +11,19 @@ import purescala.Types._
 import codegen._
 import codegen.runtime.{StdMonitor, Monitor}
 
-class DualEvaluator(ctx: LeonContext, prog: Program, params: CodeGenParams)
-  extends RecursiveEvaluator(ctx, prog, params.maxFunctionInvocations)
-  with HasDefaultGlobalContext {
+class DualEvaluator(
+  ctx: LeonContext,
+  prog: Program,
+  bank: EvaluationBank = new EvaluationBank,
+  params: CodeGenParams = CodeGenParams.default
+) extends RecursiveEvaluator(ctx, prog, params.maxFunctionInvocations)
+   with HasDefaultGlobalContext {
 
   type RC = DualRecContext
   def initRC(mappings: Map[Identifier, Expr]): RC = DualRecContext(mappings)
   implicit val debugSection = utils.DebugSectionEvaluation
 
-  val unit = new CompilationUnit(ctx, prog, params)
+  val unit = new CompilationUnit(ctx, prog, bank, params)
 
   var monitor: Monitor = new StdMonitor(unit, params.maxFunctionInvocations, Map())
 
diff --git a/src/main/scala/leon/evaluators/Evaluator.scala b/src/main/scala/leon/evaluators/Evaluator.scala
index 9f7f0fbe2d85c44e28bbd160f03daa242d2c41a4..de666f389dd4f8ea64af18b7a11a3ce0cc7b3b3c 100644
--- a/src/main/scala/leon/evaluators/Evaluator.scala
+++ b/src/main/scala/leon/evaluators/Evaluator.scala
@@ -48,6 +48,8 @@ abstract class Evaluator(val context: LeonContext, val program: Program) extends
 
 trait DeterministicEvaluator extends Evaluator {
   type Value = Expr
+
+  val bank: EvaluationBank
   
   /**Evaluates the environment first, resolving non-cyclic dependencies, and then evaluate the expression */
   override def eval(expr: Expr, mapping: Map[Identifier, Expr]) : EvaluationResult = {
@@ -63,7 +65,7 @@ trait DeterministicEvaluator extends Evaluator {
         }
     })
   }
-  
+
   /** Returns an evaluated environment. If it fails, removes all non-values from the environment. */
   def evalEnv(mapping: Iterable[(Identifier, Expr)]): Map[Identifier, Value] = {
     if(mapping.forall{ case (key, value) => purescala.ExprOps.isValue(value) }) {
@@ -107,9 +109,9 @@ trait NDEvaluator extends Evaluator {
   type Value = Stream[Expr]
 }
 
-object Evaluator {
+class EvaluationBank {
 
-  /* Global set that tracks checked case-class invariants
+  /* Shared set that tracks checked case-class invariants
    *
    * Checking case-class invariants can require invoking a solver
    * on a ground formula that contains a reference to `this` (the
@@ -118,9 +120,10 @@ object Evaluator {
    * will again contain the constructor for the current case-class.
    * This will create an invariant-checking loop.
    *
-   * To avoid this problem, we introduce a global set of invariants
-   * that have already been checked. This set is used by all
-   * evaluators to determine whether the invariant of a given case
+   * To avoid this problem, we introduce a set of invariants
+   * that have already been checked that is shared between related
+   * solvers and evaluators. This set is used by the evaluators to
+   * determine whether the invariant of a given case
    * class should be checked.
    */
   private val checkCache: MutableMap[CaseClass, CheckStatus] = MutableMap.empty
@@ -168,5 +171,4 @@ object Evaluator {
   def invariantResult(cc: CaseClass, success: Boolean): Unit = synchronized {
     checkCache(cc) = Complete(success)
   }
-
 }
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 75194a83ff93a26a13839b6bdf30af5f12d85a56..db18be70ef483f4e9ec138a8a40a90c3a78b21d1 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -20,10 +20,13 @@ import scala.collection.mutable.{Map => MutableMap}
 import scala.concurrent.duration._
 import org.apache.commons.lang3.StringEscapeUtils
 
-abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int)
+abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, val bank: EvaluationBank, maxSteps: Int)
   extends ContextualEvaluator(ctx, prog, maxSteps)
      with DeterministicEvaluator {
 
+  def this(ctx: LeonContext, prog: Program, maxSteps: Int) =
+    this(ctx, prog, new EvaluationBank, maxSteps)
+
   val name = "evaluator"
   val description = "Recursive interpreter for PureScala expressions"
 
@@ -210,13 +213,13 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
 
     case CaseClass(cct, args) =>
       val cc = CaseClass(cct, args.map(e))
-      val check = Evaluator.invariantCheck(cc)
+      val check = bank.invariantCheck(cc)
       if (check.isFailure) {
         throw RuntimeError("ADT invariant violation for " + cct.classDef.id.asString + " reached in evaluation.: " + cct.invariant.get.asString)
       } else if (check.isRequired) {
         e(FunctionInvocation(cct.invariant.get, Seq(cc))) match {
           case BooleanLiteral(success) =>
-            Evaluator.invariantResult(cc, success)
+            bank.invariantResult(cc, success)
             if (!success)
               throw RuntimeError("ADT invariant violation for " + cct.classDef.id.asString + " reached in evaluation.: " + cct.invariant.get.asString)
           case other =>
@@ -615,7 +618,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
           newOptions.exists(no => opt.optionDef == no.optionDef)
         } ++ newOptions)
 
-        val solverf = SolverFactory.getFromSettings(newCtx, program).withTimeout(1.second)
+        val solverf = SolverFactory.getEvalSolver(newCtx, program, bank).withTimeout(1.second)
         val solver  = solverf.getNewSolver()
 
         try {
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 1c49aad0553657f5cda18c745071ee54458ec1e2..08496783ff9a38537362c7bd8591106433f12cb7 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -227,7 +227,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
     val maxEnumerated = 1000
     val maxValid      = 400
 
-    val evaluator = new CodeGenEvaluator(ctx, program, CodeGenParams.default)
+    val evaluator = new CodeGenEvaluator(ctx, program)
 
     val inputsToExample: Seq[Expr] => Example = { ins =>
       evaluator.eval(functionInvocation(fd, ins)) match {
diff --git a/src/main/scala/leon/solvers/EvaluatingSolver.scala b/src/main/scala/leon/solvers/EvaluatingSolver.scala
index 835d352ed7fe544b2f22c109bf3b3c6ca47d6315..0930478d8356ef05dde8e4401a8e1593040a4563 100644
--- a/src/main/scala/leon/solvers/EvaluatingSolver.scala
+++ b/src/main/scala/leon/solvers/EvaluatingSolver.scala
@@ -12,10 +12,23 @@ trait EvaluatingSolver extends Solver {
 
   val useCodeGen: Boolean
 
-  lazy val evaluator: DeterministicEvaluator =
-    if (useCodeGen) {
-      new CodeGenEvaluator(context, program)
+  private var _bank: EvaluationBank = new EvaluationBank
+  private var _evaluator: DeterministicEvaluator = _
+
+  def evaluator: DeterministicEvaluator = {
+    if (_evaluator eq null) _evaluator = if (useCodeGen) {
+      new CodeGenEvaluator(context, program, bank)
     } else {
-      new DefaultEvaluator(context, program)
+      new DefaultEvaluator(context, program, bank)
     }
+    _evaluator
+  }
+
+  def bank: EvaluationBank = _bank
+  def setBank(bank: EvaluationBank): this.type = {
+    _bank = bank
+    _evaluator = null
+    this
+  }
 }
+
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index f2cddbf38cd0f6a2fc9237062623d7b292c262d1..bf7e392a7e56b5739e5281cd1d00d811fb127a12 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -75,6 +75,14 @@ object SolverFactory {
     }
   }
 
+  def getEvalSolver(ctx: LeonContext, program: Program, bank: evaluators.EvaluationBank): SolverFactory[EvaluatingSolver with TimeoutSolver] = {
+    val factory = getFromSettings(ctx, program)
+    SolverFactory(factory.name, () => factory.getNewSolver() match {
+      case ev: EvaluatingSolver => ev.setBank(bank)
+      case s => ctx.reporter.fatalError("Cannot use non-evaluating solver " + s + " for evaluation")
+    })
+  }
+
   private def showSolvers(ctx: LeonContext) = {
     ctx.reporter.error(availableSolversPretty)
     ctx.reporter.fatalError("Aborting Leon...")
diff --git a/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
index 03431b57720647b4017c3857d6146a615cc679b4..690f0dc2d7bfaef7b7587ea471b4bd6bf8f580ff 100644
--- a/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
@@ -215,7 +215,7 @@ trait AbstractUnrollingSolver[T]
     val newExpr = model.toSeq.foldLeft(expr){
       case (e, (k, v)) => let(k, v, e)
     }
-    
+
     evaluator.eval(newExpr) match {
       case EvaluationResults.Successful(BooleanLiteral(true)) =>
         reporter.debug("- Model validated.")
diff --git a/src/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala
index 52756108c029ff7fcad5d0f2a0e6aaceb3d6770c..08f6513ba0f084cf0e90e1eb11ccacdd2f3a2d4b 100644
--- a/src/main/scala/leon/synthesis/ExamplesFinder.scala
+++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala
@@ -119,7 +119,7 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
   def generateForPC(ids: List[Identifier], pc: Expr, ctx: LeonContext, maxValid: Int = 400, maxEnumerated: Int = 1000): ExamplesBank = {
     //println(program.definedClasses)
 
-    val evaluator = new CodeGenEvaluator(ctx, program, CodeGenParams.default)
+    val evaluator = new CodeGenEvaluator(ctx, program)
     val datagen   = new GrammarDataGen(evaluator, ValueGrammar)
     val solverF   = SolverFactory.getFromSettings(ctx, program)
     val solverDataGen = new SolverDataGen(ctx, program, solverF)
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 933ae752b19eff0ff816718ef7e6c4ee79560f22..1b5c9e948ee9a7080da3f7348a018742047e31e3 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -798,7 +798,7 @@ abstract class CEGISLike(name: String) extends Rule(name) {
             if (useVanuatoo) {
               new VanuatooDataGen(hctx, hctx.program).generateFor(p.as, p.pc.toClause, nTests, 3000).map(InExample)
             } else {
-              val evaluator = new DualEvaluator(hctx, hctx.program, CodeGenParams.default)
+              val evaluator = new DualEvaluator(hctx, hctx.program)
               new GrammarDataGen(evaluator, ValueGrammar).generateFor(p.as, p.pc.toClause, nTests, 1000).map(InExample)
             }
           }
diff --git a/src/main/scala/leon/synthesis/rules/unused/BottomUpTegis.scala b/src/main/scala/leon/synthesis/rules/unused/BottomUpTegis.scala
index 9f5dff95eed832330677112833987e32da01c35f..212ba7f6ae73746eaf14b2c32e7fe2f3b9cff244 100644
--- a/src/main/scala/leon/synthesis/rules/unused/BottomUpTegis.scala
+++ b/src/main/scala/leon/synthesis/rules/unused/BottomUpTegis.scala
@@ -41,7 +41,7 @@ abstract class BottomUpTEGISLike(name: String) extends Rule(name) {
           val evalParams            = CodeGenParams.default.copy(maxFunctionInvocations = 2000)
           //val evaluator             = new CodeGenEvaluator(sctx.context, sctx.program, evalParams)
           //val evaluator             = new DefaultEvaluator(sctx.context, sctx.program)
-          val evaluator             = new DualEvaluator(hctx, hctx.program, evalParams)
+          val evaluator             = new DualEvaluator(hctx, hctx.program, params = evalParams)
 
           val grammar               = getGrammar(hctx, p)
 
diff --git a/src/main/scala/leon/synthesis/rules/unused/TEGISLike.scala b/src/main/scala/leon/synthesis/rules/unused/TEGISLike.scala
index ee49610d06a4070154df5bfb744925121754f054..fc36521ff86564e9502eb5ec7aea751700f0bc8e 100644
--- a/src/main/scala/leon/synthesis/rules/unused/TEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/unused/TEGISLike.scala
@@ -43,7 +43,7 @@ abstract class TEGISLike(name: String) extends Rule(name) {
         val inputGenerator: Iterator[Seq[Expr]] = if (useVanuatoo) {
           new VanuatooDataGen(hctx, hctx.program).generateFor(p.as, p.pc.toClause, nTests, 3000)
         } else {
-          val evaluator = new DualEvaluator(hctx, hctx.program, CodeGenParams.default)
+          val evaluator = new DualEvaluator(hctx, hctx.program)
           new GrammarDataGen(evaluator, ValueGrammar).generateFor(p.as, p.pc.toClause, nTests, 1000)
         }
 
@@ -63,7 +63,7 @@ abstract class TEGISLike(name: String) extends Rule(name) {
         if (gi.nonEmpty) {
 
           val evalParams = CodeGenParams.default.copy(maxFunctionInvocations = 2000)
-          val evaluator  = new DualEvaluator(hctx, hctx.program, evalParams)
+          val evaluator  = new DualEvaluator(hctx, hctx.program, params = evalParams)
 
           val enum = new MemoizedEnumerator[Label, Expr, ProductionRule[Label, Expr]](grammar.getProductions)
 
diff --git a/src/test/scala/leon/integration/evaluators/CodegenEvaluatorSuite.scala b/src/test/scala/leon/integration/evaluators/CodegenEvaluatorSuite.scala
index 8882238999acebde711027ec6a8b1db152813b20..e0e1b2b85b35b03170660730c41ea06183eaaf0a 100644
--- a/src/test/scala/leon/integration/evaluators/CodegenEvaluatorSuite.scala
+++ b/src/test/scala/leon/integration/evaluators/CodegenEvaluatorSuite.scala
@@ -330,7 +330,7 @@ class CodegenEvaluatorSuite extends LeonTestSuiteWithProgram with helpers.Expres
     val testName = f"$name%-20s $opts%-18s"
 
     test("Evaluation of "+testName) { implicit fix =>
-      val eval = new CodeGenEvaluator(fix._1, fix._2, CodeGenParams(
+      val eval = new CodeGenEvaluator(fix._1, fix._2, params = CodeGenParams(
         maxFunctionInvocations = if (requireMonitor) 1000 else -1, // Monitor calls and abort execution if more than X calls
         checkContracts = true,      // Generate calls that checks pre/postconditions
         doInstrument = doInstrument // Instrument reads to case classes (mainly for vanuatoo)
diff --git a/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala b/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
index bf828a9fb07ae255ad78c7ab71f3e76eb7cee02e..e0c1537166cdca38c05c430df0f6bd3e5a5621d0 100644
--- a/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
+++ b/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
@@ -399,7 +399,7 @@ class EvaluatorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL {
   }
 
   test("Infinite Recursion") { implicit fix =>
-    val e = new CodeGenEvaluator(fix._1, fix._2, CodeGenParams.default.copy(maxFunctionInvocations = 32))
+    val e = new CodeGenEvaluator(fix._1, fix._2, params = CodeGenParams.default.copy(maxFunctionInvocations = 32))
 
     eval(e, fcall("Recursion.c")(i(42))).failed
   }