diff --git a/src/main/scala/leon/evaluators/Evaluator.scala b/src/main/scala/leon/evaluators/Evaluator.scala
index e5e6fd1a760399665cf3d2fb6962a7b27c95faca..50f28a451d9376ec2deabfcc9c4d448aa5365ff0 100644
--- a/src/main/scala/leon/evaluators/Evaluator.scala
+++ b/src/main/scala/leon/evaluators/Evaluator.scala
@@ -59,8 +59,8 @@ trait DeterministicEvaluator extends Evaluator {
         case Right(errorMessage) =>
           val m = mapping.filter { case (k, v) => purescala.ExprOps.isValue(v) }
           super.eval(expr, m) match {
-            case res@evaluators.EvaluationResults.Successful(result) => res
-            case _ => evaluators.EvaluationResults.EvaluatorError(errorMessage)
+            case res@EvaluationResults.Successful(result) => res
+            case _ => EvaluationResults.EvaluatorError(errorMessage)
           }
       }
     }
@@ -73,7 +73,8 @@ trait DeterministicEvaluator extends Evaluator {
     } else {
       _evalEnv(mapping) match {
         case Left(m) => m
-        case Right(msg) => mapping.filter(x => purescala.ExprOps.isValue(x._2)).toMap
+        case Right(msg) =>
+          mapping.filter(x => purescala.ExprOps.isValue(x._2)).toMap
       }
     }
   }
@@ -83,7 +84,7 @@ trait DeterministicEvaluator extends Evaluator {
   private def _evalEnv(mapping: Iterable[(Identifier, Expr)]): Either[Map[Identifier, Value], String] = {
     val (evaled, nonevaled) = mapping.partition{ case (id, expr) => purescala.ExprOps.isValue(expr)}
     var f= nonevaled.toSet
-    var mBuilder = collection.mutable.ListBuffer[(Identifier, Value)]() ++= evaled
+    var mBuilder = scala.collection.mutable.ListBuffer[(Identifier, Value)]() ++= evaled
     var changed = true
     while(f.nonEmpty && changed) {
       changed = false
@@ -100,7 +101,7 @@ trait DeterministicEvaluator extends Evaluator {
     if(!changed) {
       val str = "In the context " + mapping + ",\n" +
       (for((i, v) <- f) yield {
-        s"eval(${v}) returned the error: " + eval(v, mBuilder.toMap)
+        s"eval($v) returned the error: " + eval(v, mBuilder.toMap)
       }).mkString("\n")
       Right(str)
     } else Left(mBuilder.toMap)
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index b58861a2e8527e5844037a50132d1ee771b5bdb4..e1786d1f082c5fceb2b72440d5217e4f624753f9 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -69,6 +69,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
 
     case Let(i,ex,b) =>
       val first = e(ex)
+      //println(s"Eval $i to $first")
       e(b)(rctx.withNewVar(i, first), gctx)
 
     case Assert(cond, oerr, body) =>
@@ -131,6 +132,8 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
 
       val evArgs = args map e
 
+      //println(s"calling ${tfd.id} with $evArgs")
+
       // build a mapping for the function...
       val frame = rctx.withNewVars(tfd.paramSubst(evArgs))
 
@@ -155,6 +158,8 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
         e(body)(frame, gctx)
       }
 
+      //println(s"Gave $callResult")
+
       tfd.postcondition match  {
         case Some(post) =>
           e(application(post, Seq(callResult)))(frame, gctx) match {