diff --git a/core/src/main/scala/stainless/evaluators/Evaluator.scala b/core/src/main/scala/stainless/evaluators/Evaluator.scala
index ad3fb1e1ea..d05c80606d 100644
--- a/core/src/main/scala/stainless/evaluators/Evaluator.scala
+++ b/core/src/main/scala/stainless/evaluators/Evaluator.scala
@@ -8,9 +8,15 @@ import inox.evaluators.DeterministicEvaluator
 object optCodeGen extends inox.FlagOptionDef("codegen", false)
 
 object Evaluator {
+  val RecursiveEvaluatorName: String = "default recursive evaluator"
+  val CodeGenEvaluatorName: String = "codegen evaluator"
+  var kind: String = RecursiveEvaluatorName
   def apply(p: StainlessProgram, ctx: inox.Context):
-            DeterministicEvaluator { val program: p.type } = {
-    if (ctx.options.findOptionOrDefault(optCodeGen)) CodeGenEvaluator(p, ctx)
-    else RecursiveEvaluator(p, ctx)
+        DeterministicEvaluator { val program: p.type } =
+  {
+     if (ctx.options.findOptionOrDefault(optCodeGen)) {
+      kind = CodeGenEvaluatorName
+      CodeGenEvaluator(p, ctx)
+    } else RecursiveEvaluator(p, ctx)
   }
 }
diff --git a/core/src/main/scala/stainless/evaluators/EvaluatorComponent.scala b/core/src/main/scala/stainless/evaluators/EvaluatorComponent.scala
index 915ea1c270..4b41533e77 100644
--- a/core/src/main/scala/stainless/evaluators/EvaluatorComponent.scala
+++ b/core/src/main/scala/stainless/evaluators/EvaluatorComponent.scala
@@ -93,7 +93,11 @@ class EvaluatorRun(override val pipeline: extraction.StainlessPipeline)
     }
 
     // Build an evaluator once and only if there is something to evaluate
-    lazy val evaluator = p.getSemantics.getEvaluator
+    lazy val evaluator = {
+      val e = p.getSemantics.getEvaluator
+      reporter.info(s"using ${Evaluator.kind}")
+      e
+    }
 
     // Evaluate an expression, logging events
     def evaluate(title: String, e: Expr): Either[String, Expr] = evaluator eval e match {
diff --git a/core/src/main/scala/stainless/evaluators/RecursiveEvaluator.scala b/core/src/main/scala/stainless/evaluators/RecursiveEvaluator.scala
index a44fb35f6a..16d1c25110 100644
--- a/core/src/main/scala/stainless/evaluators/RecursiveEvaluator.scala
+++ b/core/src/main/scala/stainless/evaluators/RecursiveEvaluator.scala
@@ -3,6 +3,7 @@
 package stainless
 package evaluators
 
+
 trait RecursiveEvaluator extends inox.evaluators.RecursiveEvaluator {
   val program: Program
 
@@ -11,11 +12,31 @@ trait RecursiveEvaluator extends inox.evaluators.RecursiveEvaluator {
   import program.trees._
   import program.symbols._
 
+  import inox.utils.Position
+
+  def showPredicateFailure(kind: String, pred: Expr, err: Option[String])(implicit rctx: RC): Unit = {
+    val msg = (err match {
+      case Some(m) => m + ": "
+      case None => ""
+    }) + pred.asString
+    reporter.info(s"${Position.smartPos(pred.getPos)} ${kind} failure of ${msg}")
+    reporter.info(s"Relevant variables at ${kind} failure point:")
+    val m = rctx.mappings
+    val fvs = exprOps.variablesOf(pred)
+    def showBinding(v: Variable): String = {
+      "  " + v.id.asString + " -> " + m.get(v.toVal).getOrElse("?").toString
+    }
+    val fvDump: String = fvs.map(showBinding).mkString("\n")
+    reporter.info(fvDump)
+  }
+
+  
   override def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = expr match {
     case Require(pred, body) =>
-      if (!ignoreContracts && e(pred) != BooleanLiteral(true))
-        throw RuntimeError("Requirement did not hold @" + expr.getPos)
-      e(body)
+      if (!ignoreContracts && e(pred) != BooleanLiteral(true)) {
+        showPredicateFailure("require", pred, None)
+        throw RuntimeError("Requirement did not hold @" + Position.smartPos(expr.getPos))
+      } else e(body)
 
     case en @ Ensuring(body, pred) =>
       e(en.toAssert)
@@ -24,9 +45,10 @@ trait RecursiveEvaluator extends inox.evaluators.RecursiveEvaluator {
       e(body)
 
     case Assert(pred, err, body) =>
-      if (!ignoreContracts && e(pred) != BooleanLiteral(true))
-        throw RuntimeError(err.getOrElse("Assertion failed @" + expr.getPos))
-      e(body)
+      if (!ignoreContracts && e(pred) != BooleanLiteral(true)) {
+        showPredicateFailure("assertion", pred, err)
+        throw RuntimeError(err.getOrElse("Assertion failed @" + Position.smartPos(pred.getPos)))
+      } else e(body)
 
     case MatchExpr(scrut, cases) =>
       val rscrut = e(scrut)