diff --git a/core/src/main/scala/stainless/Component.scala b/core/src/main/scala/stainless/Component.scala
index a09a5f2551..e72d41114f 100644
--- a/core/src/main/scala/stainless/Component.scala
+++ b/core/src/main/scala/stainless/Component.scala
@@ -31,6 +31,20 @@ object optFunctions extends inox.OptionDef[Seq[String]] {
   val usageRhs = "f1,f2,..."
 }
 
+object optCompareFuns extends inox.OptionDef[Seq[String]] {
+  val name = "comparefuns"
+  val default = Seq[String]()
+  val parser = inox.OptionParsers.seqParser(inox.OptionParsers.stringParser)
+  val usageRhs = "f1,f2,..."
+}
+
+object optModels extends inox.OptionDef[Seq[String]] {
+  val name = "models"
+  val default = Seq[String]()
+  val parser = inox.OptionParsers.seqParser(inox.OptionParsers.stringParser)
+  val usageRhs = "f1,f2,..."
+}
+
 trait ComponentRun { self =>
   val component: Component
   val trees: ast.Trees
diff --git a/core/src/main/scala/stainless/MainHelpers.scala b/core/src/main/scala/stainless/MainHelpers.scala
index 239e0902a9..52291c3310 100644
--- a/core/src/main/scala/stainless/MainHelpers.scala
+++ b/core/src/main/scala/stainless/MainHelpers.scala
@@ -25,6 +25,8 @@ trait MainHelpers extends inox.MainHelpers { self =>
     optVersion -> Description(General, "Display the version number"),
     optConfigFile -> Description(General, "Path to configuration file, set to false to disable (default: stainless.conf or .stainless.conf)"),
     optFunctions -> Description(General, "Only consider functions f1,f2,..."),
+    optCompareFuns -> Description(General, "Only consider functions f1,f2,... for equivalence checking"),
+    optModels -> Description(General, "Consider functions f1, f2, ... as model functions for equivalence checking"),
     extraction.utils.optDebugObjects -> Description(General, "Only print debug output for functions/adts named o1,o2,..."),
     extraction.utils.optDebugPhases -> Description(General, {
       "Only print debug output for phases p1,p2,...\nAvailable: " +
@@ -166,6 +168,10 @@ trait MainHelpers extends inox.MainHelpers { self =>
 
       import ctx.{ reporter, timers }
 
+      if (extraction.trace.Trace.optionsError) {
+        reporter.fatalError(s"Equivalence checking for --comparefuns and --models only works in batched mode.")
+      }
+
       if (!useParallelism) {
         reporter.warning(s"Parallelism is disabled.")
       }
diff --git a/core/src/main/scala/stainless/Report.scala b/core/src/main/scala/stainless/Report.scala
index 389d4bb4b0..bc27de3512 100644
--- a/core/src/main/scala/stainless/Report.scala
+++ b/core/src/main/scala/stainless/Report.scala
@@ -101,6 +101,18 @@ trait AbstractReport[SelfType <: AbstractReport[SelfType]] { self: SelfType =>
     case Level.Error   => Console.RED
   }
 
+  def hasError(identifier: Identifier)(implicit ctx: inox.Context): Boolean = {
+    annotatedRows.exists(elem => elem match {
+      case RecordRow(id, pos, level, extra, time) => level == Level.Error && id == identifier
+    })
+  }
+
+  def hasUnknown(identifier: Identifier)(implicit ctx: inox.Context): Boolean = {
+    annotatedRows.exists(elem => elem match {
+      case RecordRow(id, pos, level, extra, time) => level == Level.Warning && id == identifier
+    })
+  }
+
   // Emit the report table, with all VCs when full is true, otherwise only with unknown/invalid VCs.
   private def emitTable(full: Boolean)(implicit ctx: inox.Context): Table = {
     val rows  = processRows(full)
diff --git a/core/src/main/scala/stainless/extraction/trace/Trace.scala b/core/src/main/scala/stainless/extraction/trace/Trace.scala
index 45f12f58fb..45780489b6 100644
--- a/core/src/main/scala/stainless/extraction/trace/Trace.scala
+++ b/core/src/main/scala/stainless/extraction/trace/Trace.scala
@@ -4,18 +4,13 @@ package stainless
 package extraction
 package trace
 
-trait Trace extends CachingPhase with SimpleFunctions with IdentitySorts { self =>
+import stainless.utils.CheckFilter
+
+trait Trace extends CachingPhase with IdentityFunctions with IdentitySorts { self =>
   val s: Trees
   val t: termination.Trees
   import s._
 
-  override protected final val funCache = new ExtractionCache[s.FunDef, FunctionResult]({(fd, symbols) => 
-    FunctionKey(fd) + SetKey(
-      symbols.dependencies(fd.id)
-        .flatMap(id => symbols.lookupFunction(id))
-    )
-  })
-
   override protected type TransformerContext = s.Symbols
   override protected def getContext(symbols: s.Symbols) = symbols
 
@@ -24,110 +19,278 @@ trait Trace extends CachingPhase with SimpleFunctions with IdentitySorts { self
     override val t: self.t.type = self.t
   }
 
-  override protected def extractFunction(symbols: Symbols, fd: FunDef): t.FunDef = {
+  override protected def extractSymbols(context: TransformerContext, symbols: s.Symbols): t.Symbols = {
     import symbols._
-    var funInv: Option[FunctionInvocation] = None
+    import exprOps._
+
+    if (Trace.getModels.isEmpty) {
+      val models = symbols.functions.values.toList.filter(elem => !elem.flags.exists(_.name == "library") &&
+        isModel(elem.id)).map(elem => elem.id)
+      Trace.setModels(models)
+      Trace.nextModel
+    }
+
+    if (Trace.getFunctions.isEmpty) {
+      val functions = symbols.functions.values.toList.filter(elem => !elem.flags.exists(_.name == "library") &&
+        shouldBeChecked(elem.id)).map(elem => elem.id)
+      Trace.setFunctions(functions)
+      Trace.nextFunction
+    }
+
+    def generateEqLemma: Option[s.FunDef] = {
+      def equivalenceChek(fd1: s.FunDef, fd2: s.FunDef): s.FunDef = {
+        val id = FreshIdentifier(CheckFilter.fixedFullName(fd1.id)+"$"+CheckFilter.fixedFullName(fd2.id))
+
+        val newParams = fd1.params.map{param => param.freshen}
+        val newParamVars = newParams.map{param => param.toVariable}
+        val newParamTypes = fd1.tparams.map{tparam => tparam.freshen}
+        val newParamTps = newParamTypes.map{tparam => tparam.tp}
+
+        val body = s.UnitLiteral()
+        val returnType = s.UnitType()
+
+        val specsMap = (fd1.params zip newParamVars).toMap
+        val specs = BodyWithSpecs(fd1.fullBody).specs.filter(s => s.kind == LetKind || s.kind == PreconditionKind) 
+        val pre = specs.map(spec => spec match {
+          case Precondition(cond) => Precondition(exprOps.replaceFromSymbols(specsMap, cond))
+          case LetInSpec(vd, expr) => LetInSpec(vd, exprOps.replaceFromSymbols(specsMap, expr))
+        })
+
+        val res = s.ValDef.fresh("res", s.UnitType())
+        val cond = s.Equals(s.FunctionInvocation(fd1.id, newParamTps, newParamVars), s.FunctionInvocation(fd2.id, newParamTps, newParamVars))
+        val post = Postcondition(Lambda(Seq(res), cond))
+
+        val withPre = exprOps.reconstructSpecs(pre, Some(body), s.UnitType())
+        val fullBody = BodyWithSpecs(withPre).withSpec(post).reconstructed
+
+        val flags: Seq[s.Flag] = Seq(s.Derived(fd1.id), s.Annotation("traceInduct",List(StringLiteral(fd1.id.name))))
 
-    if(fd.flags.exists(elem => elem.name == "traceInduct")) {
+        new s.FunDef(id, newParamTypes, newParams, returnType, fullBody, flags)
+      }
+
+      (Trace.getModel, Trace.getFunction) match {
+        case (Some(model), Some(function)) => {
+          val m = symbols.functions(model)
+          val f = symbols.functions(function)
+          if (m.params.size == f.params.size) {
+            val newFun = equivalenceChek(m, f)
+            Some(newFun)
+          }
+          else {
+            Trace.resetTrace
+            None
+          }
+        }
+        case _ => None
+      }
+    }
+
+    val functions = generateEqLemma match {
+      case Some(lemma) => lemma +: symbols.functions.values.toList
+      case None => symbols.functions.values.toList
+    }
+
+    val inductFuns = functions.toList.flatMap(fd => if (fd.flags.exists(elem => elem.name == "traceInduct")) {
+      //find the model for fd
+      var funInv: Option[s.FunctionInvocation] = None
       fd.flags.filter(elem => elem.name == "traceInduct").head match {
-        case Annotation("traceInduct", fun) => {
-          exprOps.preTraversal {
-            case _ if funInv.isDefined => // do nothing
-            case fi @ FunctionInvocation(tfd, _, args) if symbols.isRecursive(tfd) && (fun.contains(StringLiteral(tfd.name)) || fun.contains(StringLiteral("")))
-            => {
-                  val paramVars = fd.params.map(_.toVariable)
-                  val argCheck = args.forall(paramVars.contains) && args.toSet.size == args.size
-                  if (argCheck) 
-                    funInv = Some(fi)
-                }
+        case s.Annotation("traceInduct", fun) => {
+          BodyWithSpecs(fd.fullBody).getSpec(PostconditionKind) match {
+            case Some(Postcondition(post)) => 
+              s.exprOps.preTraversal {
+                case _ if funInv.isDefined => // do nothing
+                case fi @ s.FunctionInvocation(tfd, _, args) if symbols.isRecursive(tfd) && (fun.contains(StringLiteral(tfd.name)) || fun.contains(StringLiteral("")))
+                => {
+                      val paramVars = fd.params.map(_.toVariable)
+                      val argCheck = args.forall(paramVars.contains) && args.toSet.size == args.size
+                      if (argCheck) funInv = Some(fi)
+                    }
+                case _ => 
+              }(post)
             case _ => 
-          }(fd.fullBody)
+          }
         }
       }
-    }
 
-    val result: FunDef = (funInv match {
-      case None => fd
-      case Some(finv) => createTactFun(symbols, fd, finv)
-    })
+      funInv match {
+        case Some(finv) => {
+          // make a helper lemma:
+          val helper = inductPattern(symbols, symbols.functions(finv.id), fd).setPos(fd.getPos)
 
-    identity.transform(result.copy(flags = result.flags filterNot (f => f == TraceInduct)))    
+          // transform the main lemma
+          val proof = FunctionInvocation(helper.id, fd.tparams.map(_.tp), fd.params.map(_.toVariable))
+          val body = Let(s.ValDef.fresh("ind$proof", helper.returnType), proof, exprOps.withoutSpecs(fd.fullBody).get)
+          val withPre = exprOps.reconstructSpecs(BodyWithSpecs(fd.fullBody).specs, Some(body), fd.returnType)
+          val lemma = fd.copy(
+            fullBody = BodyWithSpecs(withPre).reconstructed,
+            flags = (s.Derived(fd.id) +: s.Derived(finv.id) +: (fd.flags.filterNot(f => f.name == "traceInduct"))).distinct
+          ).copiedFrom(fd).setPos(fd.getPos)
+
+          Trace.setTrace(lemma.id)
+          Trace.setProof(helper.id)
+          List(helper, lemma)
+        }
+        case None => {
+          val lemma = fd.copy(
+            flags = (s.Derived(fd.id) +: (fd.flags.filterNot(f => f.name == "traceInduct")))
+          ).copiedFrom(fd).setPos(fd.getPos)
+          Trace.setTrace(lemma.id)
+          List(lemma)
+        }
+      }
+    } else List())
+
+    val extractedSymbols = super.extractSymbols(context, symbols)
+    
+    val extracted = t.NoSymbols
+      .withSorts(extractedSymbols.sorts.values.toSeq)
+      .withFunctions(extractedSymbols.functions.values.filterNot(fd => fd.flags.exists(elem => elem.name == "traceInduct")).toSeq)
+
+    registerFunctions(extracted, inductFuns.map(fun => identity.transform(fun)))
   }
-  
-  private def createTactFun(symbols: Symbols, function: FunDef, finv: FunctionInvocation): FunDef = {
+
+  def inductPattern(symbols: s.Symbols, model: FunDef, lemma: FunDef) = {
     import symbols._
+    import exprOps._
 
-    val callee: FunDef = symbols.functions.filter(elem => elem._2.id == finv.id).head._2
-
-    def inductPattern(e: Expr): Expr = {
-      e match {
-        case IfExpr(c, th, el) =>
-          andJoin(Seq(inductPattern(c), IfExpr(c, inductPattern(th), inductPattern(el))))
-        case MatchExpr(scr, cases) =>
-          val scrpat = inductPattern(scr)
-          val casePats = cases.map {
-            case MatchCase(pat, optGuard, rhs) =>
-              val guardPat = optGuard.toSeq.map(inductPattern _)
-              (guardPat, MatchCase(pat, optGuard, inductPattern(rhs)))
-          }
-          val pats = scrpat +: casePats.flatMap(_._1) :+ MatchExpr(scr, casePats.map(_._2))
-          andJoin(pats)
-        case Let(i, v, b) =>
-          andJoin(Seq(inductPattern(v), Let(i, v, inductPattern(b))))
-        case FunctionInvocation(tfd, _, args) =>
-          val argPattern = andJoin(args.map(inductPattern))
-          if (tfd == callee.id) { // self recursive call ?
-            // create a tactFun invocation to mimic the recursion pattern
-            val paramVars = function.params.map(_.toVariable)
-            val paramIndex = paramVars.zipWithIndex.toMap
-            val framePositions = finv.args.zipWithIndex.collect {
-              case (v: Variable, i) if paramVars.contains(v) => (v, i)
-            }.toMap
-            val footprint = paramVars.filterNot(framePositions.keySet.contains)
-            val indexedFootprint = footprint.map { a => paramIndex(a) -> a }.toMap
-            // create a tactFun invocation to mimic the recursion pattern
-            val indexedArgs = framePositions.map {
-              case (f, i) => paramIndex(f) -> args(i)
-            }.toMap ++ indexedFootprint
-            val recArgs = (0 until indexedArgs.size).map(indexedArgs)
-            val recCall = FunctionInvocation(function.id, function.typeArgs, recArgs)
-
-            andJoin(Seq(argPattern, recCall))
-          } else {
-            argPattern
-          }
-        case Operator(args, op) =>
-          // conjoin all the expressions and return them
-          andJoin(args.map(inductPattern))
+    val id = FreshIdentifier(lemma.id+"$induct")
+
+    val newParams = model.params.map{param => param.freshen}
+    val newParamVars = newParams.map{param => param.toVariable}
+    val newParamTypes = model.tparams.map{tparam => tparam.freshen}
+    val newParamTps = newParamTypes.map{tparam => tparam.tp}
+
+    val returnType = model.returnType
+    val flags = Seq(s.Derived(lemma.id), s.Derived(model.id))
+
+    val body = FunctionInvocation(model.id, newParamTps, newParamVars)
+    val indPattern = new s.FunDef(id, newParamTypes, newParams, returnType, body, flags)
+
+    val fi = FunctionInvocation(model.id, newParamTps, newParamVars)
+
+    class Specializer(
+      origFd: FunDef,
+      newId: Identifier,
+      vsubst: Map[Identifier, Expr]
+    ) extends s.SelfTreeTransformer {
+
+      override def transform(expr: s.Expr): t.Expr = expr match {
+        case v: Variable =>
+          vsubst.getOrElse(v.id, super.transform(v))
+
+        case fi: FunctionInvocation if fi.id == origFd.id =>
+          val fi1 = FunctionInvocation(newId, tps = fi.tps, args = fi.args)
+          super.transform(fi1.copiedFrom(fi))
+
+        case _ => super.transform(expr)
       }
     }
 
-    val argsMap = callee.params.map(_.toVariable).zip(finv.args).toMap
-    val tparamMap = callee.typeArgs.zip(finv.tfd.tps).toMap
-    val inlinedBody = typeOps.instantiateType(exprOps.replaceFromSymbols(argsMap, callee.body.get), tparamMap)
-    val inductScheme = inductPattern(inlinedBody)
+    val subst = (model.params.map(_.id) zip fi.args).toMap
+    val specializer = new Specializer(model, indPattern.id, subst)
+    
+    val fullBodySpecialized = specializer.transform(exprOps.withoutSpecs(model.fullBody).get)
+
+    val specsMap = (lemma.params zip newParamVars).toMap ++ (model.params zip newParamVars).toMap
+    val specs = BodyWithSpecs(model.fullBody).specs ++ BodyWithSpecs(lemma.fullBody).specs.filterNot(_.kind == MeasureKind)
+
+    val pre = specs.filterNot(_.kind == PostconditionKind).map(spec => spec match {
+      case Precondition(cond) => Precondition(exprOps.replaceFromSymbols(specsMap, cond)).setPos(spec)
+      case LetInSpec(vd, expr) => LetInSpec(vd, exprOps.replaceFromSymbols(specsMap, expr)).setPos(spec)
+      case Measure(measure) => Measure(exprOps.replaceFromSymbols(specsMap, measure)).setPos(spec)
+      case s => context.reporter.fatalError(s"Unsupported specs: $s")
+    })
+
+    val withPre = exprOps.reconstructSpecs(pre, Some(fullBodySpecialized), indPattern.returnType)
+
+    val speccedLemma = BodyWithSpecs(lemma.fullBody).addPost
+    val speccedOrig = BodyWithSpecs(model.fullBody).addPost
+    val postLemma = speccedLemma.getSpec(PostconditionKind).map(post => exprOps.replaceFromSymbols(specsMap, post.expr))
+    val postOrig = speccedOrig.getSpec(PostconditionKind).map(post => exprOps.replaceFromSymbols(specsMap, post.expr))
+    
+    (postLemma, postOrig) match {
+      case (Some(Lambda(Seq(res1), cond1)), Some(Lambda(Seq(res2), cond2))) => 
+        val res = ValDef.fresh("res", indPattern.returnType)
+        val freshCond1 = exprOps.replaceFromSymbols(Map(res1 -> res.toVariable), cond1)
+        val freshCond2 = exprOps.replaceFromSymbols(Map(res2 -> res.toVariable), cond2)
+        val cond = andJoin(Seq(freshCond1, freshCond2))
+        val post = Postcondition(Lambda(Seq(res), cond))
 
-    val prevBody = function.fullBody match {
-      case Ensuring(body, pred) => body
-      case _ => function.fullBody
+        indPattern.copy(
+          fullBody = BodyWithSpecs(withPre).withSpec(post).reconstructed
+        ).copiedFrom(indPattern)
     }
 
-    // body, pre and post for the tactFun
+  }
 
-    val body = andJoin(Seq(inductScheme, prevBody))
-    val precondition = function.precondition
-    val postcondition = function.postcondition
- 
-    val bodyPre = exprOps.withPrecondition(body, precondition)
-    val bodyPost = exprOps.withPostcondition(bodyPre,postcondition)
+  type Path = Seq[String]
 
-    function.copy(function.id, function.tparams, function.params, function.returnType, bodyPost, function.flags)
+  private lazy val pathsOpt: Option[Seq[Path]] = context.options.findOption(optCompareFuns) map { functions =>
+    functions map CheckFilter.fullNameToPath
   }
 
-}
+  private lazy val pathsOptModels: Option[Seq[Path]] = context.options.findOption(optModels) map { functions =>
+    functions map CheckFilter.fullNameToPath
+  }
 
+  private def shouldBeChecked(fid: Identifier): Boolean = shouldBeChecked(pathsOpt, fid)
+  private def isModel(fid: Identifier): Boolean = shouldBeChecked(pathsOptModels, fid)
+
+  private def shouldBeChecked(paths: Option[Seq[Path]], fid: Identifier): Boolean = paths match {
+    case None => false
+
+    case Some(paths) =>
+      // Support wildcard `_` as specified in the documentation.
+      // A leading wildcard is always assumed.
+      val path: Path = CheckFilter.fullNameToPath(CheckFilter.fixedFullName(fid))
+      paths exists { p =>
+        if (p endsWith Seq("_")) path containsSlice p.init
+        else path endsWith p
+      }
+  }
+
+}
 
 object Trace {
+  var clusters: Map[Identifier, List[Identifier]] = Map()
+  var errors: List[Identifier] = List()
+  var unknowns: List[Identifier] = List()
+  var wrong: List[Identifier] = List() //bad signature
+
+  def optionsError(implicit ctx: inox.Context): Boolean = 
+    !ctx.options.findOptionOrDefault(frontend.optBatchedProgram) && 
+    (!ctx.options.findOptionOrDefault(optModels).isEmpty || !ctx.options.findOptionOrDefault(optCompareFuns).isEmpty)
+        
+  def printEverything(implicit ctx: inox.Context) = {
+    import ctx.{ reporter, timers }
+    if(!clusters.isEmpty || !errors.isEmpty || !unknowns.isEmpty || !wrong.isEmpty) {
+      reporter.info(s"Printing equivalence checking results:")  
+      allModels.foreach(model => {
+        val l = clusters(model).map(CheckFilter.fixedFullName).mkString(", ")
+        val m = CheckFilter.fixedFullName(model)
+        reporter.info(s"List of functions that are equivalent to model $m: $l")
+      })
+
+      val errorneous = errors.map(CheckFilter.fixedFullName).mkString(", ")
+      reporter.info(s"List of erroneous functions: $errorneous")
+      val timeouts = unknowns.map(CheckFilter.fixedFullName).mkString(", ")
+      reporter.info(s"List of timed-out functions: $timeouts")
+      val wrongs = wrong.map(CheckFilter.fixedFullName).mkString(", ")
+      reporter.info(s"List of wrong functions: $wrongs")
+    }
+  }
+
+  var allModels: List[Identifier] = List()
+  var tmpModels: List[Identifier] = List()
+
+  var allFunctions: List[Identifier] = List()
+  var tmpFunctions: List[Identifier] = List()
+
+  var model: Option[Identifier] = None
+  var function: Option[Identifier] = None
+  var trace: Option[Identifier] = None
+  var proof: Option[Identifier] = None
+
   def apply(ts: Trees, tt: termination.Trees)(implicit ctx: inox.Context): ExtractionPipeline {
     val s: ts.type
     val t: tt.type
@@ -136,4 +299,104 @@ object Trace {
     override val t: tt.type = tt
     override val context = ctx
   }
+
+  def setModels(m: List[Identifier]) = {
+    allModels = m
+    tmpModels = m
+    clusters = (m zip m.map(_ => Nil)).toMap
+  }
+
+  def setFunctions(f: List[Identifier]) = {
+    allFunctions = f
+    tmpFunctions = f
+  }
+
+  def getModels = allModels
+
+  def getFunctions = allFunctions
+
+  //model for the current iteration
+  def getModel = model
+
+  //function to check in the current iteration
+  def getFunction = function
+
+  def setTrace(t: Identifier) = trace = Some(t)
+  def setProof(p: Identifier) = proof = Some(p)
+
+
+  def resetTrace = {
+    trace = None
+    proof = None
+  }
+
+  //iterate model for the current function
+  def nextModel = tmpModels match {
+    case x::xs => { 
+      tmpModels = xs
+      model = Some(x)
+    }
+    case Nil => model = None
+  }
+
+  //iterate function to check; reset model
+  def nextFunction = {
+    trace = None
+    proof = None
+      tmpFunctions match {
+      case x::xs => {
+        tmpModels = allModels
+        nextModel
+        tmpFunctions = xs
+        function = Some(x)
+      }
+      case Nil => {
+        function = None
+      }
+    }
+  }
+
+  def nextIteration[T <: AbstractReport[T]](report: AbstractReport[T])(implicit context: inox.Context): Boolean = {
+    (function, proof, trace) match {
+      case (Some(f), Some(p), Some(t)) => {
+        if (report.hasError(f) || report.hasError(p) || report.hasError(t)) reportError
+        else if (report.hasUnknown(f) || report.hasUnknown(p) || report.hasError(t)) reportUnknown
+        else reportValid
+      }
+      case (Some(f), _, Some(t)) => {
+        if (report.hasError(f) || report.hasError(t)) reportError
+        else if (report.hasUnknown(f) || report.hasError(t)) reportUnknown
+        else reportValid
+      }
+      case _ => reportWrong
+    }
+    !isDone
+  }
+
+  private def isDone = function == None
+
+  private def reportError = {
+    errors = function.get::errors
+    nextFunction
+  }
+
+  private def reportUnknown = {
+    nextModel
+    if (model == None) {
+      unknowns = function.get::unknowns
+      nextFunction
+    }
+  }
+
+  private def reportValid = {
+    clusters = clusters + (model.get -> (function.get::clusters(model.get)))
+    nextFunction
+  }
+
+  private def reportWrong = {
+    if (function != None) wrong = function.get::wrong
+    resetTrace
+    nextFunction
+  }
+
 }
\ No newline at end of file
diff --git a/core/src/main/scala/stainless/frontend/BatchedCallBack.scala b/core/src/main/scala/stainless/frontend/BatchedCallBack.scala
index 9714de804a..a767c39309 100644
--- a/core/src/main/scala/stainless/frontend/BatchedCallBack.scala
+++ b/core/src/main/scala/stainless/frontend/BatchedCallBack.scala
@@ -6,6 +6,7 @@ package frontend
 import stainless.extraction.xlang.{trees => xt, TreeSanitizer}
 import stainless.extraction.utils.DebugSymbols
 import stainless.utils.LibraryFilter
+import stainless.extraction.trace.Trace
 
 import scala.util.{Try, Success, Failure}
 import scala.concurrent.Await
@@ -99,13 +100,17 @@ class BatchedCallBack(components: Seq[Component])(implicit val context: inox.Con
         reportError(defn.getPos, e.getMessage, symbols)
     }
 
-    val reports = runs map { run =>
-      val ids = symbols.functions.keys.toSeq
-      val analysis = Await.result(run(ids, symbols, filterSymbols = true), Duration.Inf)
-      RunReport(run)(analysis.toReport)
+    var rerunPipeline = true
+    while (rerunPipeline) {
+      val reports = runs map { run =>
+        val ids = symbols.functions.keys.toSeq
+        val analysis = Await.result(run(ids, symbols, filterSymbols = true), Duration.Inf)
+        RunReport(run)(analysis.toReport)
+      }
+      report = Report(reports)
+      rerunPipeline = Trace.nextIteration(report)
+      if (!rerunPipeline) Trace.printEverything
     }
-
-    report = Report(reports)
   }
 
   def stop(): Unit = {
diff --git a/core/src/main/scala/stainless/utils/CheckFilter.scala b/core/src/main/scala/stainless/utils/CheckFilter.scala
index 79df04a800..396287fdfa 100644
--- a/core/src/main/scala/stainless/utils/CheckFilter.scala
+++ b/core/src/main/scala/stainless/utils/CheckFilter.scala
@@ -10,25 +10,9 @@ trait CheckFilter {
   import trees._
 
   type Path = Seq[String]
-  private def fullNameToPath(fullName: String): Path = (fullName split '.').toSeq
-
-  // TODO this is probably done somewhere else in a cleaner fasion...
-  private def fixedFullName(id: Identifier): String = id.fullName
-    .replaceAllLiterally("$bar", "|")
-    .replaceAllLiterally("$up", "^")
-    .replaceAllLiterally("$eq", "=")
-    .replaceAllLiterally("$plus", "+")
-    .replaceAllLiterally("$minus", "-")
-    .replaceAllLiterally("$times", "*")
-    .replaceAllLiterally("$div", "/")
-    .replaceAllLiterally("$less", "<")
-    .replaceAllLiterally("$geater", ">")
-    .replaceAllLiterally("$colon", ":")
-    .replaceAllLiterally("$amp", "&")
-    .replaceAllLiterally("$tilde", "~")
 
   private lazy val pathsOpt: Option[Seq[Path]] = context.options.findOption(optFunctions) map { functions =>
-    functions map fullNameToPath
+    functions map CheckFilter.fullNameToPath
   }
 
   private def shouldBeChecked(fid: Identifier, flags: Seq[trees.Flag]): Boolean = pathsOpt match {
@@ -40,7 +24,7 @@ trait CheckFilter {
     case Some(paths) =>
       // Support wildcard `_` as specified in the documentation.
       // A leading wildcard is always assumes.
-      val path: Path = fullNameToPath(fixedFullName(fid))
+      val path: Path = CheckFilter.fullNameToPath(CheckFilter.fixedFullName(fid))
       paths exists { p =>
         if (p endsWith Seq("_")) path containsSlice p.init
         else path endsWith p
@@ -86,5 +70,23 @@ object CheckFilter {
     override val context = ctx
     override val trees: t.type = t
   }
-}
 
+  type Path = Seq[String]
+
+  def fullNameToPath(fullName: String): Path = (fullName split '.').toSeq
+
+  // TODO this is probably done somewhere else in a cleaner fasion...
+  def fixedFullName(id: Identifier): String = id.fullName
+    .replaceAllLiterally("$bar", "|")
+    .replaceAllLiterally("$up", "^")
+    .replaceAllLiterally("$eq", "=")
+    .replaceAllLiterally("$plus", "+")
+    .replaceAllLiterally("$minus", "-")
+    .replaceAllLiterally("$times", "*")
+    .replaceAllLiterally("$div", "/")
+    .replaceAllLiterally("$less", "<")
+    .replaceAllLiterally("$geater", ">")
+    .replaceAllLiterally("$colon", ":")
+    .replaceAllLiterally("$amp", "&")
+    .replaceAllLiterally("$tilde", "~")
+}
diff --git a/frontends/benchmarks/verification/valid/Count.scala b/frontends/benchmarks/verification/valid/Count.scala
index 14a27ac9b5..d574a71cb3 100644
--- a/frontends/benchmarks/verification/valid/Count.scala
+++ b/frontends/benchmarks/verification/valid/Count.scala
@@ -17,7 +17,7 @@ object Count {
   }//ensuring(res => res == count1(p, l))
 
   @traceInduct("")
-  def count_check(p: BigInt => Boolean, l: List[BigInt]): Boolean = {
-    count1(p, l) == count2(p, l)
-  }.holds
-}
+  def count_check(p: BigInt => Boolean, l: List[BigInt]): Unit = {
+    ()
+  } ensuring (res => count1(p, l) == count2(p, l))
+}
\ No newline at end of file
diff --git a/frontends/benchmarks/verification/valid/Filter.scala b/frontends/benchmarks/verification/valid/Filter.scala
index 39d714259a..6fedbaa04e 100644
--- a/frontends/benchmarks/verification/valid/Filter.scala
+++ b/frontends/benchmarks/verification/valid/Filter.scala
@@ -7,7 +7,7 @@ object Filter {
 
   def filter1(p: BigInt => Boolean, l: List[BigInt], n: BigInt): List[BigInt] = { 
     require(l.size <= n)
-    if(l.isEmpty) Nil()
+    if (l.isEmpty) List()
     else if(p(l.head)) l.head::filter1(p, l.tail, n)
     else filter1(p, l.tail, n)
   }
@@ -18,8 +18,9 @@ object Filter {
   }
   
   @traceInduct("")
-  def filter_check(p: BigInt => Boolean, l: List[BigInt], n: BigInt): Boolean = {
+  def filter_check(p: BigInt => Boolean, l: List[BigInt], n: BigInt): Unit = {
     require(l.size <= n)
-    filter1(p, l, n) == filter2(p, l, n)
-  }.holds
-}
+    ()
+  } ensuring(filter1(p, l, n) == filter2(p, l, n))
+  
+}
\ No newline at end of file
diff --git a/frontends/benchmarks/verification/valid/Insert.scala b/frontends/benchmarks/verification/valid/Insert.scala
deleted file mode 100644
index 186a964235..0000000000
--- a/frontends/benchmarks/verification/valid/Insert.scala
+++ /dev/null
@@ -1,29 +0,0 @@
-import stainless.lang._
-import stainless.annotation._
-import stainless.collection._
-import stainless.proof._
-
-object Insert {
-    
-  def insertAtIndex[T](l: List[T], i: BigInt, y: T): List[T] = {
-    require(0 <= i && i <= l.size)
-    l match {
-      case Nil() =>
-        Cons[T](y, Nil())
-      case _ if i == 0 =>
-        Cons[T](y, l)
-      case Cons(x, tail) =>
-        Cons[T](x, insertAtIndex(tail, i - 1, y))
-    }
-  }
-
-  @traceInduct("insertAtIndex")
-  def appendInsertIndex[T](l1: List[T], l2: List[T], i: BigInt, y: T): Boolean = {
-    require(0 <= i && i <= l1.size + l2.size)
-      (insertAtIndex((l1 ++ l2), i, y) == (
-        if (i < l1.size) insertAtIndex(l1, i, y) ++ l2
-        else l1 ++ insertAtIndex(l2, (i - l1.size), y))
-      )
-  }.holds
-}
-
diff --git a/frontends/benchmarks/verification/valid/Monotonicity.scala b/frontends/benchmarks/verification/valid/Monotonicity.scala
index 1459ed5430..5b00119007 100644
--- a/frontends/benchmarks/verification/valid/Monotonicity.scala
+++ b/frontends/benchmarks/verification/valid/Monotonicity.scala
@@ -13,8 +13,8 @@ object Monotonicity {
   }
   
   @traceInduct("")
-  def monotonicity(l: List[BigInt], set1: Set[BigInt], set2: Set[BigInt]): Boolean = {
-    (contains(l, set1, set2) && set1.subsetOf(set2)) ==> contains(l, set2, set1)
-  }.holds
+  def monotonicity(l: List[BigInt], set1: Set[BigInt], set2: Set[BigInt]): Unit = {
+    ()
+  } ensuring((contains(l, set1, set2) && set1.subsetOf(set2)) ==> contains(l, set2, set1))
 }
 
diff --git a/frontends/benchmarks/verification/valid/Reverse.scala b/frontends/benchmarks/verification/valid/Reverse.scala
index 17facc7069..45b1e438a5 100644
--- a/frontends/benchmarks/verification/valid/Reverse.scala
+++ b/frontends/benchmarks/verification/valid/Reverse.scala
@@ -20,8 +20,8 @@ object Reverse {
   }
   
   @traceInduct("reverse0")
-  def revPreservesContent(l1: IList, l2: IList): Boolean = {
-    content(l1) ++ content(l2) == content(reverse0(l1, l2))
-  }.holds
+  def revPreservesContent(l1: IList, l2: IList): Unit = {
+    ()
+  } ensuring (content(l1) ++ content(l2) == content(reverse0(l1, l2)))
 }
 
diff --git a/frontends/benchmarks/verification/valid/Size.scala b/frontends/benchmarks/verification/valid/Size.scala
index 517ea7d73b..daab04f0d5 100644
--- a/frontends/benchmarks/verification/valid/Size.scala
+++ b/frontends/benchmarks/verification/valid/Size.scala
@@ -13,8 +13,8 @@ object Size {
   }) //ensuring(res => res >= 0)
 
   @traceInduct("")
-  def nonNegSize(l: IList): Boolean = {
-    size(l) >= 0
-  }.holds
+  def nonNegSize(l: IList): Unit = {
+    ()
+  } ensuring (size(l) >= 0)
 }
 
diff --git a/frontends/benchmarks/verification/valid/Sorted.scala b/frontends/benchmarks/verification/valid/Sorted.scala
index f3c0ca8b96..49bd0669a9 100644
--- a/frontends/benchmarks/verification/valid/Sorted.scala
+++ b/frontends/benchmarks/verification/valid/Sorted.scala
@@ -22,8 +22,8 @@ object Sorted {
   }//ensuring(res => res == sorted1(l))
 
   @traceInduct("")
-  def sorted_check(l: List[BigInt]): Boolean = {
-    sorted1(l) == sorted2(l)
-  }.holds
+  def sorted_check(l: List[BigInt]): Unit = {
+    ()
+  } ensuring (sorted1(l) == sorted2(l))
 
 }
diff --git a/frontends/benchmarks/verification/valid/Zero.scala b/frontends/benchmarks/verification/valid/Zero.scala
index d8ae55bc68..b58aee374f 100644
--- a/frontends/benchmarks/verification/valid/Zero.scala
+++ b/frontends/benchmarks/verification/valid/Zero.scala
@@ -14,8 +14,8 @@ object Zero {
   }//ensuring(res => res == zero1(arg))
   
   @traceInduct("")
-  def zero_check(arg: BigInt): Boolean = {
-    zero1(arg) == zero2(arg)
-  }.holds
+  def zero_check(arg: BigInt): Unit = {
+    ()
+  } ensuring (zero1(arg) == zero2(arg))
 
 }