From 4c32479b86c942b6eb315e756aebb4d3179b9892 Mon Sep 17 00:00:00 2001
From: Dragana Milovancevic <milovanc@thinkpadx1e.epfl.ch>
Date: Tue, 9 Mar 2021 18:32:55 +0100
Subject: [PATCH 1/7] @traceInduct clustering implementation

---
 core/src/main/scala/stainless/Component.scala |  14 +
 .../main/scala/stainless/MainHelpers.scala    |   2 +
 core/src/main/scala/stainless/Report.scala    |  16 ++
 .../stainless/extraction/trace/Trace.scala    | 259 +++++++++++++++++-
 .../stainless/frontend/BatchedCallBack.scala  |  25 +-
 5 files changed, 307 insertions(+), 9 deletions(-)

diff --git a/core/src/main/scala/stainless/Component.scala b/core/src/main/scala/stainless/Component.scala
index 3c3b445fbb..74c5db27f0 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 b4b559c3e3..227ba7f376 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,..."),
+    optModels -> Description(General, "Consider functions f1, f2, ... as model functions for @traceInduct"),
+    optCompareFuns -> Description(General, "Only consider @traceInduct functions f1,f2,..."),
     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: " +
diff --git a/core/src/main/scala/stainless/Report.scala b/core/src/main/scala/stainless/Report.scala
index 1f3747619d..cf5f36beca 100644
--- a/core/src/main/scala/stainless/Report.scala
+++ b/core/src/main/scala/stainless/Report.scala
@@ -100,6 +100,22 @@ trait AbstractReport[SelfType <: AbstractReport[SelfType]] { self: SelfType =>
     case Level.Error   => Console.RED
   }
 
+  def isError(identifier: Identifier)(implicit ctx: inox.Context): Boolean = {
+    val res = for {
+      RecordRow(id, pos, level, extra, time) <- annotatedRows
+      if(level == Level.Error && id == identifier)
+    }yield (id, level)
+    !res.isEmpty
+  }
+
+  def isUnknown(identifier: Identifier)(implicit ctx: inox.Context): Boolean = {
+    val res = for {
+      RecordRow(id, pos, level, extra, time) <- annotatedRows
+      if(level == Level.Warning && id == identifier)
+    }yield (id, level)
+    !res.isEmpty
+  }
+
   // 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..6ad07fb27b 100644
--- a/core/src/main/scala/stainless/extraction/trace/Trace.scala
+++ b/core/src/main/scala/stainless/extraction/trace/Trace.scala
@@ -24,6 +24,87 @@ trait Trace extends CachingPhase with SimpleFunctions with IdentitySorts { self
     override val t: self.t.type = self.t
   }
 
+  override protected def extractSymbols(context: TransformerContext, symbols: s.Symbols): t.Symbols = {
+    import symbols._
+    import trees._
+
+    val models = symbols.functions.values.toList.filter(elem => isModel(elem.id)).map(elem => elem.id)
+    val functions = symbols.functions.values.toList.filter(elem => shouldBeChecked(elem.id)).map(elem => elem.id)
+   
+    if (Trace.getModels.isEmpty) {
+      Trace.setModels(models)
+      Trace.nextModel
+    }
+    if (Trace.getFunctions.isEmpty) {
+      Trace.setFunctions(functions)
+      Trace.nextFunction
+    }
+
+    var localCounter = 0
+
+    def freshId(a: Identifier, b: Identifier): Identifier = {
+      localCounter = localCounter + 1
+      new Identifier(fixedFullName(a)+"$"+fixedFullName(b),localCounter,localCounter)
+    }
+
+    //if (fd1 != fd2) && (fd1.params.size == fd2.params.size)
+    def checkPair(fd1: s.FunDef, fd2: s.FunDef): s.FunDef = {
+
+      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 vd = s.ValDef.fresh("holds", s.BooleanType())
+      val post = s.Lambda(Seq(vd), vd.toVariable)
+
+      val body = s.Ensuring(s.Equals(s.FunctionInvocation(fd1.id, newParamTps, newParamVars), s.FunctionInvocation(fd2.id, newParamTps, newParamVars)), post)
+      val flags: Seq[s.Flag] = Seq(s.Derived(fd1.id), s.Annotation("traceInduct",List(StringLiteral(fd1.id.name))))
+
+      new s.FunDef(freshId(fd1.id, fd2.id), newParamTypes, newParams, s.BooleanType(), body, flags)
+    }
+
+    def newFuns: List[s.FunDef] = (Trace.getModel, Trace.getFunction) match {
+      case (Some(model), Some(function)) => {
+        val m = symbols.functions.filter(elem => elem._2.id == model).head._2
+        val f = symbols.functions.filter(elem => elem._2.id == function).head._2
+        val newFun = checkPair(m, f)
+        Trace.setTrace(newFun.id)
+        List(newFun)
+      }
+      case _ => Nil
+    }
+
+/*
+    def newFuns: List[s.FunDef] = Trace.nextModel match {
+      case Some(model) => toCheck.map(f => checkPair(
+
+        symbols.functions.filter(elem => elem._2.id == model).head._2
+
+    , f))
+      case None => check(toCheck, toCheck, Nil)
+    }
+
+    def check(funs1: List[s.FunDef], funs2: List[s.FunDef], acc: List[s.FunDef]): List[s.FunDef] = {
+      funs1 match {
+        case Nil => acc
+        case fd1::xs1 => {
+          funs2 match {
+            case Nil => check(xs1, toCheck, acc)
+              //todo: check if both funs have same arg list
+            case fd2::xs2 if (fd1 != fd2) && (fd1.params.size == fd2.params.size) =>
+              check(funs1, xs2, checkPair(fd1, fd2)::acc)
+            case _ => check(funs1, funs2.tail, acc)
+          }
+        }
+      }
+    }
+*/
+    val extracted = super.extractSymbols(context, symbols)
+    //newFuns(toCheck, toCheck, Nil).map(f => extractFunction(symbols, f))
+    registerFunctions(extracted, newFuns.map(f => extractFunction(symbols, f)))
+  }
+
   override protected def extractFunction(symbols: Symbols, fd: FunDef): t.FunDef = {
     import symbols._
     var funInv: Option[FunctionInvocation] = None
@@ -33,13 +114,12 @@ trait Trace extends CachingPhase with SimpleFunctions with IdentitySorts { self
         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("")))
-            => {
+            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 _ => 
           }(fd.fullBody)
         }
@@ -51,6 +131,7 @@ trait Trace extends CachingPhase with SimpleFunctions with IdentitySorts { self
       case Some(finv) => createTactFun(symbols, fd, finv)
     })
 
+
     identity.transform(result.copy(flags = result.flags filterNot (f => f == TraceInduct)))    
   }
   
@@ -105,8 +186,8 @@ trait Trace extends CachingPhase with SimpleFunctions with IdentitySorts { self
     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 inductScheme = inductPattern(inlinedBody)
     val prevBody = function.fullBody match {
       case Ensuring(body, pred) => body
       case _ => function.fullBody
@@ -115,19 +196,95 @@ trait Trace extends CachingPhase with SimpleFunctions with IdentitySorts { self
     // body, pre and post for the tactFun
 
     val body = andJoin(Seq(inductScheme, prevBody))
-    val precondition = function.precondition
-    val postcondition = function.postcondition
- 
+    val precondition = exprOps.preconditionOf(function.fullBody)  //function.precondition
+    val postcondition = exprOps.postconditionOf(function.fullBody) //function.postcondition
     val bodyPre = exprOps.withPrecondition(body, precondition)
     val bodyPost = exprOps.withPostcondition(bodyPre,postcondition)
+    function.copy(function.id, function.tparams, function.params, function.returnType, bodyPost, function.flags)  
+
+  }
+
+//from CheckFilter.scala
+  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(optCompareFuns) map { functions =>
+    functions map fullNameToPath
+  }
+
+  private def shouldBeChecked(fid: Identifier): Boolean = pathsOpt match {
+    case None => false
+
+    case Some(paths) =>
+      // Support wildcard `_` as specified in the documentation.
+      // A leading wildcard is always assumes.
+      val path: Path = fullNameToPath(fixedFullName(fid))
+      paths exists { p =>
+        if (p endsWith Seq("_")) path containsSlice p.init
+        else path endsWith p
+      }
+  }
 
-    function.copy(function.id, function.tparams, function.params, function.returnType, bodyPost, function.flags)
+  private lazy val pathsOptModels: Option[Seq[Path]] = context.options.findOption(optModels) map { functions =>
+    functions map fullNameToPath
+  }
+
+  private def isModel(fid: Identifier): Boolean = pathsOptModels match {
+    case None => false
+
+    case Some(paths) =>
+      // Support wildcard `_` as specified in the documentation.
+      // A leading wildcard is always assumes.
+      val path: Path = fullNameToPath(fixedFullName(fid))
+      paths exists { p =>
+        if (p endsWith Seq("_")) path containsSlice p.init
+        else path endsWith p
+      }
   }
 
 }
 
 
 object Trace {
+  var boxes: Map[Identifier, List[Identifier]] = Map()
+  var errors: List[Identifier] = List()
+  var unknowns: List[Identifier] = List()
+
+  def printEverything() = {
+    System.out.println("boxes")   
+    System.out.println(boxes)
+    System.out.println("errors")
+    System.out.println(errors)
+    System.out.println("unknowns")
+    System.out.println(unknowns)
+  }
+
+  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
+
   def apply(ts: Trees, tt: termination.Trees)(implicit ctx: inox.Context): ExtractionPipeline {
     val s: ts.type
     val t: tt.type
@@ -136,4 +293,90 @@ object Trace {
     override val t: tt.type = tt
     override val context = ctx
   }
+
+  def setModels(m: List[Identifier]) = {
+    allModels = m
+    tmpModels = m
+    boxes = (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 getTrace = trace
+
+  //iterate model for the current function
+  def nextModel = (tmpModels, allModels) match {
+    case (x::xs, _) => { // check the next model for the current function
+      tmpModels = xs
+      model = Some(x)
+    }
+    case (Nil, x::xs) => {
+      tmpModels = allModels
+      model = Some(x)
+      tmpModels = xs
+      function = tmpFunctions match {
+        case x::xs => {
+          tmpFunctions = xs
+          Some(x)
+        }
+        case Nil => None
+      }
+    }
+    case _ => model = None
+  }
+
+  //iterate function to check; reset model
+  def nextFunction = tmpFunctions match {
+    case x::xs => {
+      tmpFunctions = xs
+      function = Some(x)
+      tmpModels = allModels
+      tmpModels match {
+        case Nil => model = None
+        case x::xs => {
+          model = Some(x)
+          tmpModels = xs
+        }
+      }
+      function
+    }
+    case Nil => {
+      function = None
+    }
+  }
+
+  def isDone = function == None
+
+  def reportError = {
+    errors = function.get::errors
+    nextFunction
+  }
+
+  def reportUnknown = {
+    nextModel
+    if(model == None){
+      unknowns = function.get::unknowns
+      nextFunction
+    }
+  }
+
+  def reportValid = {
+    boxes = boxes + (model.get -> (function.get::boxes(model.get)))
+    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 9b4110f14b..e218b55e02 100644
--- a/core/src/main/scala/stainless/frontend/BatchedCallBack.scala
+++ b/core/src/main/scala/stainless/frontend/BatchedCallBack.scala
@@ -5,6 +5,7 @@ package frontend
 
 import stainless.extraction.xlang.{trees => xt, TreeSanitizer}
 import stainless.utils.LibraryFilter
+import stainless.extraction.trace.Trace
 
 import scala.util.{Try, Success, Failure}
 import scala.concurrent.Await
@@ -102,13 +103,35 @@ class BatchedCallBack(components: Seq[Component])(implicit val context: inox.Con
         reportError(defn.getPos, e.getMessage, symbols)
     }
 
-    val reports = runs map { run =>
+    var 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)
+
+    if (report.isError(Trace.getTrace.get)) Trace.reportError
+    else if (report.isUnknown(Trace.getTrace.get)) Trace.reportUnknown
+    else Trace.reportValid
+
+    while (!Trace.isDone) {
+      report.emit(context)
+
+      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)
+
+      if (report.isError(Trace.getTrace.get)) Trace.reportError
+      else if (report.isUnknown(Trace.getTrace.get)) Trace.reportUnknown
+      else Trace.reportValid
+    }
+
+    extraction.trace.Trace.printEverything
   }
 
   def stop(): Unit = {

From 1952ed9713845e42d05b8f6376fff10b006d02e8 Mon Sep 17 00:00:00 2001
From: Dragana Milovancevic <milovanc@thinkpadx1e.epfl.ch>
Date: Thu, 11 Mar 2021 18:21:43 +0100
Subject: [PATCH 2/7] Refactor @traceInduct clustering implementation

---
 core/src/main/scala/stainless/Report.scala    |  4 +-
 .../stainless/extraction/trace/Trace.scala    | 80 +++++++++----------
 .../stainless/frontend/BatchedCallBack.scala  | 27 ++-----
 .../scala/stainless/utils/CheckFilter.scala   | 39 ++++-----
 4 files changed, 67 insertions(+), 83 deletions(-)

diff --git a/core/src/main/scala/stainless/Report.scala b/core/src/main/scala/stainless/Report.scala
index cf5f36beca..5b4c015b99 100644
--- a/core/src/main/scala/stainless/Report.scala
+++ b/core/src/main/scala/stainless/Report.scala
@@ -104,7 +104,7 @@ trait AbstractReport[SelfType <: AbstractReport[SelfType]] { self: SelfType =>
     val res = for {
       RecordRow(id, pos, level, extra, time) <- annotatedRows
       if(level == Level.Error && id == identifier)
-    }yield (id, level)
+    } yield (id, level)
     !res.isEmpty
   }
 
@@ -112,7 +112,7 @@ trait AbstractReport[SelfType <: AbstractReport[SelfType]] { self: SelfType =>
     val res = for {
       RecordRow(id, pos, level, extra, time) <- annotatedRows
       if(level == Level.Warning && id == identifier)
-    }yield (id, level)
+    } yield (id, level)
     !res.isEmpty
   }
 
diff --git a/core/src/main/scala/stainless/extraction/trace/Trace.scala b/core/src/main/scala/stainless/extraction/trace/Trace.scala
index 6ad07fb27b..cadd7da592 100644
--- a/core/src/main/scala/stainless/extraction/trace/Trace.scala
+++ b/core/src/main/scala/stainless/extraction/trace/Trace.scala
@@ -4,6 +4,8 @@ package stainless
 package extraction
 package trace
 
+import stainless.utils.CheckFilter
+
 trait Trace extends CachingPhase with SimpleFunctions with IdentitySorts { self =>
   val s: Trees
   val t: termination.Trees
@@ -28,14 +30,14 @@ trait Trace extends CachingPhase with SimpleFunctions with IdentitySorts { self
     import symbols._
     import trees._
 
-    val models = symbols.functions.values.toList.filter(elem => isModel(elem.id)).map(elem => elem.id)
-    val functions = symbols.functions.values.toList.filter(elem => shouldBeChecked(elem.id)).map(elem => elem.id)
-   
     if (Trace.getModels.isEmpty) {
+      val models = symbols.functions.values.toList.filter(elem => isModel(elem.id)).map(elem => elem.id)
       Trace.setModels(models)
       Trace.nextModel
     }
+
     if (Trace.getFunctions.isEmpty) {
+      val functions = symbols.functions.values.toList.filter(elem => shouldBeChecked(elem.id)).map(elem => elem.id)
       Trace.setFunctions(functions)
       Trace.nextFunction
     }
@@ -44,10 +46,9 @@ trait Trace extends CachingPhase with SimpleFunctions with IdentitySorts { self
 
     def freshId(a: Identifier, b: Identifier): Identifier = {
       localCounter = localCounter + 1
-      new Identifier(fixedFullName(a)+"$"+fixedFullName(b),localCounter,localCounter)
+      new Identifier(CheckFilter.fixedFullName(a)+"$"+CheckFilter.fixedFullName(b),localCounter,localCounter)
     }
 
-    //if (fd1 != fd2) && (fd1.params.size == fd2.params.size)
     def checkPair(fd1: s.FunDef, fd2: s.FunDef): s.FunDef = {
 
       val newParams = fd1.params.map{param => param.freshen}
@@ -68,6 +69,7 @@ trait Trace extends CachingPhase with SimpleFunctions with IdentitySorts { self
       case (Some(model), Some(function)) => {
         val m = symbols.functions.filter(elem => elem._2.id == model).head._2
         val f = symbols.functions.filter(elem => elem._2.id == function).head._2
+        //if (fd1 != fd2) && (fd1.params.size == fd2.params.size)
         val newFun = checkPair(m, f)
         Trace.setTrace(newFun.id)
         List(newFun)
@@ -204,28 +206,10 @@ trait Trace extends CachingPhase with SimpleFunctions with IdentitySorts { self
 
   }
 
-//from CheckFilter.scala
   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(optCompareFuns) map { functions =>
-    functions map fullNameToPath
+    functions map CheckFilter.fullNameToPath
   }
 
   private def shouldBeChecked(fid: Identifier): Boolean = pathsOpt match {
@@ -234,7 +218,7 @@ trait Trace extends CachingPhase with SimpleFunctions with IdentitySorts { self
     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
@@ -242,7 +226,7 @@ trait Trace extends CachingPhase with SimpleFunctions with IdentitySorts { self
   }
 
   private lazy val pathsOptModels: Option[Seq[Path]] = context.options.findOption(optModels) map { functions =>
-    functions map fullNameToPath
+    functions map CheckFilter.fullNameToPath
   }
 
   private def isModel(fid: Identifier): Boolean = pathsOptModels match {
@@ -251,7 +235,7 @@ trait Trace extends CachingPhase with SimpleFunctions with IdentitySorts { self
     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
@@ -260,19 +244,20 @@ trait Trace extends CachingPhase with SimpleFunctions with IdentitySorts { self
 
 }
 
-
 object Trace {
-  var boxes: Map[Identifier, List[Identifier]] = Map()
+  var clusters: Map[Identifier, List[Identifier]] = Map()
   var errors: List[Identifier] = List()
   var unknowns: List[Identifier] = List()
 
   def printEverything() = {
-    System.out.println("boxes")   
-    System.out.println(boxes)
-    System.out.println("errors")
-    System.out.println(errors)
-    System.out.println("unknowns")
-    System.out.println(unknowns)
+    if(!clusters.isEmpty || !errors.isEmpty || !unknowns.isEmpty) {
+      System.out.println("clusters")   
+      System.out.println(clusters)
+      System.out.println("errors")
+      System.out.println(errors)
+      System.out.println("unknowns")
+      System.out.println(unknowns)
+    }
   }
 
   var allModels: List[Identifier] = List()
@@ -297,7 +282,7 @@ object Trace {
   def setModels(m: List[Identifier]) = {
     allModels = m
     tmpModels = m
-    boxes = (m zip m.map(_ => Nil)).toMap
+    clusters = (m zip m.map(_ => Nil)).toMap
   }
 
   def setFunctions(f: List[Identifier]) = {
@@ -309,7 +294,6 @@ object Trace {
 
   def getFunctions = allFunctions
 
-
   //model for the current iteration
   def getModel = model
 
@@ -360,23 +344,33 @@ object Trace {
     }
   }
 
-  def isDone = function == None
+  def nextIteration[T <: AbstractReport[T]](report: AbstractReport[T])(implicit context: inox.Context): Boolean = trace match {
+    case Some(t) => {
+      if (report.isError(t)) reportError
+      else if (report.isUnknown(t)) reportUnknown
+      else reportValid
+      !isDone
+    }
+    case None => false
+  }
+
+  private def isDone = function == None
 
-  def reportError = {
+  private def reportError = {
     errors = function.get::errors
     nextFunction
   }
 
-  def reportUnknown = {
+  private def reportUnknown = {
     nextModel
-    if(model == None){
+    if (model == None) {
       unknowns = function.get::unknowns
       nextFunction
     }
   }
 
-  def reportValid = {
-    boxes = boxes + (model.get -> (function.get::boxes(model.get)))
+  private def reportValid = {
+    clusters = clusters + (model.get -> (function.get::clusters(model.get)))
     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 e218b55e02..9f1543ae28 100644
--- a/core/src/main/scala/stainless/frontend/BatchedCallBack.scala
+++ b/core/src/main/scala/stainless/frontend/BatchedCallBack.scala
@@ -103,35 +103,22 @@ class BatchedCallBack(components: Seq[Component])(implicit val context: inox.Con
         reportError(defn.getPos, e.getMessage, symbols)
     }
 
-    var 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)
-
-    if (report.isError(Trace.getTrace.get)) Trace.reportError
-    else if (report.isUnknown(Trace.getTrace.get)) Trace.reportUnknown
-    else Trace.reportValid
+    var rerunPipeline = true
 
-    while (!Trace.isDone) {
-      report.emit(context)
-
-      reports = runs map { run =>
+    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 (report.isError(Trace.getTrace.get)) Trace.reportError
-      else if (report.isUnknown(Trace.getTrace.get)) Trace.reportUnknown
-      else Trace.reportValid
+      if (rerunPipeline) report.emit(context)
+      else Trace.printEverything
     }
-
-    extraction.trace.Trace.printEverything
+    
   }
 
   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..5692d95619 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,24 @@ 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", "~")
 }
 

From 11a007124fa6127f5ce5a07c78e14768136b38ac Mon Sep 17 00:00:00 2001
From: Jad Hamza <jad.hamza@epfl.ch>
Date: Thu, 11 Mar 2021 18:44:58 +0100
Subject: [PATCH 3/7] Fix extraction of Array.updated

---
 .../benchmarks/extraction/valid/Arrays.scala  | 29 +++++--------------
 .../library/stainless/lang/package.scala      | 10 +++++++
 .../frontends/scalac/ASTExtractors.scala      | 12 ++++++++
 3 files changed, 30 insertions(+), 21 deletions(-)

diff --git a/frontends/benchmarks/extraction/valid/Arrays.scala b/frontends/benchmarks/extraction/valid/Arrays.scala
index e2e94b2e4b..a10538cf82 100644
--- a/frontends/benchmarks/extraction/valid/Arrays.scala
+++ b/frontends/benchmarks/extraction/valid/Arrays.scala
@@ -1,12 +1,12 @@
 /* Copyright 2009-2021 EPFL, Lausanne */
 
+// use `.updated` from Stainless library
 import stainless.lang._
 
-object Arrays {
+// unimport implicit conversions for `.updated`
+import scala.Predef.{ genericArrayOps => _, genericWrapArray => _, _ }
 
-  def len[T](a: Array[T]): Boolean = {
-    a.length == a.size
-  }.holds
+object Arrays {
 
   def update[T](a: Array[T], i: Int, t: T) = {
     require(i >= 0 && i < a.length)
@@ -17,24 +17,11 @@ object Arrays {
     a.update(i, t)
   }
 
+  def updated[T](a: Array[T], i: Int, t: T): Array[T] = {
+    require(i >= 0 && i < a.length)
 
-  // ArraySeq not supported.
-  /*
-   * import scala.collection.mutable.ArraySeq
-   * def updated[T](a: Array[T], i: Int, t: T): ArraySeq[T] = {
-   *   require(i >= 0 && i < a.length)
-   *   a.updated(i, t)
-   * }
-   */
-
-  // ClassTag not supported.
-  /*
-   * import scala.reflect.ClassTag
-   * def updated[T](a: Array[T], i: Int, u: T)(implicit m: ClassTag[T]): Array[T] = {
-   *   require(i >= 0 && i < a.length)
-   *   a.updated(i, u)
-   * }
-   */
+    a.updated(i, t)
+  }
 
   def updated(a: Array[Int], i: Int, v: Int): Array[Int] = {
     require(i >= 0 && i < a.length)
diff --git a/frontends/library/stainless/lang/package.scala b/frontends/library/stainless/lang/package.scala
index 75f749b3e7..5d7e8fff89 100644
--- a/frontends/library/stainless/lang/package.scala
+++ b/frontends/library/stainless/lang/package.scala
@@ -145,4 +145,14 @@ package object lang {
 
   @library
   def specialize[T](call: T): T = call
+
+  @ignore @library
+  implicit class ArrayUpdating[T](a: Array[T]) {
+    def updated(index: Int, value: T): Array[T] = {
+      val res = a.clone
+      res(index) = value
+      res
+    }
+  }
+
 }
diff --git a/frontends/scalac/src/main/scala/stainless/frontends/scalac/ASTExtractors.scala b/frontends/scalac/src/main/scala/stainless/frontends/scalac/ASTExtractors.scala
index e86b0f9308..6b310c785d 100644
--- a/frontends/scalac/src/main/scala/stainless/frontends/scalac/ASTExtractors.scala
+++ b/frontends/scalac/src/main/scala/stainless/frontends/scalac/ASTExtractors.scala
@@ -844,6 +844,18 @@ trait ASTExtractors {
              if (arrayOps.toString endsWith "ArrayOps") && (update.toString == "updated")
              => Some((array, index, value))
 
+        case Apply(
+          Select(
+            Apply(
+              TypeApply(ExSelected("stainless", "lang", "package", "ArrayUpdating"), tpe :: Nil),
+              array :: Nil
+            ),
+            ExNamed("updated")
+          ),
+          index :: value :: Nil) =>
+
+          Some((array, index, value))
+
         // There's no `updated` method in the Array class itself, only though implicit conversion.
         case _ => None
       }

From 1fdf28fb5e9946c744b0af0194d6cffcd5672b02 Mon Sep 17 00:00:00 2001
From: Dragana Milovancevic <milovanc@thinkpadx1e.epfl.ch>
Date: Fri, 12 Mar 2021 10:17:04 +0100
Subject: [PATCH 4/7] Revert

---
 .../benchmarks/extraction/valid/Arrays.scala  | 29 ++++++++++++++-----
 .../library/stainless/lang/package.scala      | 10 -------
 .../frontends/scalac/ASTExtractors.scala      | 12 --------
 3 files changed, 21 insertions(+), 30 deletions(-)

diff --git a/frontends/benchmarks/extraction/valid/Arrays.scala b/frontends/benchmarks/extraction/valid/Arrays.scala
index a10538cf82..e2e94b2e4b 100644
--- a/frontends/benchmarks/extraction/valid/Arrays.scala
+++ b/frontends/benchmarks/extraction/valid/Arrays.scala
@@ -1,13 +1,13 @@
 /* Copyright 2009-2021 EPFL, Lausanne */
 
-// use `.updated` from Stainless library
 import stainless.lang._
 
-// unimport implicit conversions for `.updated`
-import scala.Predef.{ genericArrayOps => _, genericWrapArray => _, _ }
-
 object Arrays {
 
+  def len[T](a: Array[T]): Boolean = {
+    a.length == a.size
+  }.holds
+
   def update[T](a: Array[T], i: Int, t: T) = {
     require(i >= 0 && i < a.length)
     val array: Array[Int] = Array(0, 1)
@@ -17,11 +17,24 @@ object Arrays {
     a.update(i, t)
   }
 
-  def updated[T](a: Array[T], i: Int, t: T): Array[T] = {
-    require(i >= 0 && i < a.length)
 
-    a.updated(i, t)
-  }
+  // ArraySeq not supported.
+  /*
+   * import scala.collection.mutable.ArraySeq
+   * def updated[T](a: Array[T], i: Int, t: T): ArraySeq[T] = {
+   *   require(i >= 0 && i < a.length)
+   *   a.updated(i, t)
+   * }
+   */
+
+  // ClassTag not supported.
+  /*
+   * import scala.reflect.ClassTag
+   * def updated[T](a: Array[T], i: Int, u: T)(implicit m: ClassTag[T]): Array[T] = {
+   *   require(i >= 0 && i < a.length)
+   *   a.updated(i, u)
+   * }
+   */
 
   def updated(a: Array[Int], i: Int, v: Int): Array[Int] = {
     require(i >= 0 && i < a.length)
diff --git a/frontends/library/stainless/lang/package.scala b/frontends/library/stainless/lang/package.scala
index 5d7e8fff89..75f749b3e7 100644
--- a/frontends/library/stainless/lang/package.scala
+++ b/frontends/library/stainless/lang/package.scala
@@ -145,14 +145,4 @@ package object lang {
 
   @library
   def specialize[T](call: T): T = call
-
-  @ignore @library
-  implicit class ArrayUpdating[T](a: Array[T]) {
-    def updated(index: Int, value: T): Array[T] = {
-      val res = a.clone
-      res(index) = value
-      res
-    }
-  }
-
 }
diff --git a/frontends/scalac/src/main/scala/stainless/frontends/scalac/ASTExtractors.scala b/frontends/scalac/src/main/scala/stainless/frontends/scalac/ASTExtractors.scala
index 6b310c785d..e86b0f9308 100644
--- a/frontends/scalac/src/main/scala/stainless/frontends/scalac/ASTExtractors.scala
+++ b/frontends/scalac/src/main/scala/stainless/frontends/scalac/ASTExtractors.scala
@@ -844,18 +844,6 @@ trait ASTExtractors {
              if (arrayOps.toString endsWith "ArrayOps") && (update.toString == "updated")
              => Some((array, index, value))
 
-        case Apply(
-          Select(
-            Apply(
-              TypeApply(ExSelected("stainless", "lang", "package", "ArrayUpdating"), tpe :: Nil),
-              array :: Nil
-            ),
-            ExNamed("updated")
-          ),
-          index :: value :: Nil) =>
-
-          Some((array, index, value))
-
         // There's no `updated` method in the Array class itself, only though implicit conversion.
         case _ => None
       }

From a56bb515c24af9bea1326586136913693c592f03 Mon Sep 17 00:00:00 2001
From: Dragana Milovancevic <milovanc@thinkpadx1e.epfl.ch>
Date: Wed, 17 Mar 2021 10:44:54 +0100
Subject: [PATCH 5/7] Refactoring

---
 .../main/scala/stainless/MainHelpers.scala    |  9 ++-
 core/src/main/scala/stainless/Report.scala    | 20 +++----
 .../stainless/extraction/trace/Trace.scala    | 55 ++++---------------
 .../stainless/frontend/BatchedCallBack.scala  |  5 +-
 4 files changed, 28 insertions(+), 61 deletions(-)

diff --git a/core/src/main/scala/stainless/MainHelpers.scala b/core/src/main/scala/stainless/MainHelpers.scala
index 227ba7f376..4b9956cc5a 100644
--- a/core/src/main/scala/stainless/MainHelpers.scala
+++ b/core/src/main/scala/stainless/MainHelpers.scala
@@ -25,8 +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,..."),
-    optModels -> Description(General, "Consider functions f1, f2, ... as model functions for @traceInduct"),
-    optCompareFuns -> Description(General, "Only consider @traceInduct 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: " +
@@ -168,6 +168,11 @@ trait MainHelpers extends inox.MainHelpers { self =>
 
       import ctx.{ reporter, timers }
 
+      if(!ctx.options.findOptionOrDefault(frontend.optBatchedProgram) && (!ctx.options.findOptionOrDefault(optModels).isEmpty || !ctx.options.findOptionOrDefault(optCompareFuns).isEmpty)) {
+        reporter.error(s"Equivalence checking for --comparefuns and --models only works in batched mode.")
+        System.exit(1)
+      }
+
       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 5b4c015b99..99cdea9549 100644
--- a/core/src/main/scala/stainless/Report.scala
+++ b/core/src/main/scala/stainless/Report.scala
@@ -100,20 +100,16 @@ trait AbstractReport[SelfType <: AbstractReport[SelfType]] { self: SelfType =>
     case Level.Error   => Console.RED
   }
 
-  def isError(identifier: Identifier)(implicit ctx: inox.Context): Boolean = {
-    val res = for {
-      RecordRow(id, pos, level, extra, time) <- annotatedRows
-      if(level == Level.Error && id == identifier)
-    } yield (id, level)
-    !res.isEmpty
+  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 isUnknown(identifier: Identifier)(implicit ctx: inox.Context): Boolean = {
-    val res = for {
-      RecordRow(id, pos, level, extra, time) <- annotatedRows
-      if(level == Level.Warning && id == identifier)
-    } yield (id, level)
-    !res.isEmpty
+  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.
diff --git a/core/src/main/scala/stainless/extraction/trace/Trace.scala b/core/src/main/scala/stainless/extraction/trace/Trace.scala
index cadd7da592..ae81e7ec9a 100644
--- a/core/src/main/scala/stainless/extraction/trace/Trace.scala
+++ b/core/src/main/scala/stainless/extraction/trace/Trace.scala
@@ -42,14 +42,8 @@ trait Trace extends CachingPhase with SimpleFunctions with IdentitySorts { self
       Trace.nextFunction
     }
 
-    var localCounter = 0
-
-    def freshId(a: Identifier, b: Identifier): Identifier = {
-      localCounter = localCounter + 1
-      new Identifier(CheckFilter.fixedFullName(a)+"$"+CheckFilter.fixedFullName(b),localCounter,localCounter)
-    }
-
     def checkPair(fd1: s.FunDef, fd2: s.FunDef): s.FunDef = {
+      val name = CheckFilter.fixedFullName(fd1.id)+"$"+CheckFilter.fixedFullName(fd2.id)
 
       val newParams = fd1.params.map{param => param.freshen}
       val newParamVars = newParams.map{param => param.toVariable}
@@ -62,48 +56,24 @@ trait Trace extends CachingPhase with SimpleFunctions with IdentitySorts { self
       val body = s.Ensuring(s.Equals(s.FunctionInvocation(fd1.id, newParamTps, newParamVars), s.FunctionInvocation(fd2.id, newParamTps, newParamVars)), post)
       val flags: Seq[s.Flag] = Seq(s.Derived(fd1.id), s.Annotation("traceInduct",List(StringLiteral(fd1.id.name))))
 
-      new s.FunDef(freshId(fd1.id, fd2.id), newParamTypes, newParams, s.BooleanType(), body, flags)
+      new s.FunDef(FreshIdentifier(name), newParamTypes, newParams, s.BooleanType(), body, flags)
     }
 
     def newFuns: List[s.FunDef] = (Trace.getModel, Trace.getFunction) match {
       case (Some(model), Some(function)) => {
-        val m = symbols.functions.filter(elem => elem._2.id == model).head._2
-        val f = symbols.functions.filter(elem => elem._2.id == function).head._2
-        //if (fd1 != fd2) && (fd1.params.size == fd2.params.size)
-        val newFun = checkPair(m, f)
-        Trace.setTrace(newFun.id)
-        List(newFun)
+        val m = symbols.functions(model)
+        val f = symbols.functions(function)
+        if (m != f && m.params.size == f.params.size) {
+          val newFun = checkPair(m, f)
+          Trace.setTrace(newFun.id)
+          List(newFun)
+        }
+        else Nil
       }
       case _ => Nil
     }
 
-/*
-    def newFuns: List[s.FunDef] = Trace.nextModel match {
-      case Some(model) => toCheck.map(f => checkPair(
-
-        symbols.functions.filter(elem => elem._2.id == model).head._2
-
-    , f))
-      case None => check(toCheck, toCheck, Nil)
-    }
-
-    def check(funs1: List[s.FunDef], funs2: List[s.FunDef], acc: List[s.FunDef]): List[s.FunDef] = {
-      funs1 match {
-        case Nil => acc
-        case fd1::xs1 => {
-          funs2 match {
-            case Nil => check(xs1, toCheck, acc)
-              //todo: check if both funs have same arg list
-            case fd2::xs2 if (fd1 != fd2) && (fd1.params.size == fd2.params.size) =>
-              check(funs1, xs2, checkPair(fd1, fd2)::acc)
-            case _ => check(funs1, funs2.tail, acc)
-          }
-        }
-      }
-    }
-*/
     val extracted = super.extractSymbols(context, symbols)
-    //newFuns(toCheck, toCheck, Nil).map(f => extractFunction(symbols, f))
     registerFunctions(extracted, newFuns.map(f => extractFunction(symbols, f)))
   }
 
@@ -133,7 +103,6 @@ trait Trace extends CachingPhase with SimpleFunctions with IdentitySorts { self
       case Some(finv) => createTactFun(symbols, fd, finv)
     })
 
-
     identity.transform(result.copy(flags = result.flags filterNot (f => f == TraceInduct)))    
   }
   
@@ -346,8 +315,8 @@ object Trace {
 
   def nextIteration[T <: AbstractReport[T]](report: AbstractReport[T])(implicit context: inox.Context): Boolean = trace match {
     case Some(t) => {
-      if (report.isError(t)) reportError
-      else if (report.isUnknown(t)) reportUnknown
+      if (report.hasError(t)) reportError
+      else if (report.hasUnknown(t)) reportUnknown
       else reportValid
       !isDone
     }
diff --git a/core/src/main/scala/stainless/frontend/BatchedCallBack.scala b/core/src/main/scala/stainless/frontend/BatchedCallBack.scala
index 9f1543ae28..d9ba2068dc 100644
--- a/core/src/main/scala/stainless/frontend/BatchedCallBack.scala
+++ b/core/src/main/scala/stainless/frontend/BatchedCallBack.scala
@@ -104,23 +104,20 @@ class BatchedCallBack(components: Seq[Component])(implicit val context: inox.Con
     }
 
     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) report.emit(context)
       else Trace.printEverything
     }
     
   }
-
+  
   def stop(): Unit = {
     currentClasses = Seq()
     currentFunctions = Seq()

From 6dc51213bbd9733a5638f0705fec177c494dd3fc Mon Sep 17 00:00:00 2001
From: Dragana Milovancevic <milovanc@thinkpadx1e.epfl.ch>
Date: Wed, 31 Mar 2021 10:46:11 +0200
Subject: [PATCH 6/7] Add documentation

---
 core/src/sphinx/index.rst |  1 +
 core/src/sphinx/trace.rst | 84 +++++++++++++++++++++++++++++++++++++++
 2 files changed, 85 insertions(+)
 create mode 100644 core/src/sphinx/trace.rst

diff --git a/core/src/sphinx/index.rst b/core/src/sphinx/index.rst
index e322207388..8d0aa2f116 100644
--- a/core/src/sphinx/index.rst
+++ b/core/src/sphinx/index.rst
@@ -18,6 +18,7 @@ Contents:
    options
    verification
    laws
+   trace
    imperative
    ghost
    wrap
diff --git a/core/src/sphinx/trace.rst b/core/src/sphinx/trace.rst
new file mode 100644
index 0000000000..06e010749e
--- /dev/null
+++ b/core/src/sphinx/trace.rst
@@ -0,0 +1,84 @@
+.. _trace:
+
+Induction and equivalence checking
+==================================
+
+Induction and @traceInduct annotation
+-------------------------------------
+
+We introduce the @traceInduct annotation for automating proofs using induction. Stainless will transform the annotated lemma by generating the inductive proof, based on the structure of one of the functions that appear in the lemma. This approach is useful for functions that have simple inductive form and are easily mapped into inductive proofs.
+
+Here is one simple example of an equivalence lemma:
+
+.. code-block:: scala
+
+   def zero1(arg: BigInt): BigInt = { 
+    if (arg > 0) zero1(arg - 1)
+    else BigInt(0)
+  }
+
+  def zero2(arg: BigInt): BigInt = {
+    BigInt(0)
+  }
+  
+  @traceInduct("")
+  def zero_check(arg: BigInt): Boolean = {
+    zero1(arg) == zero2(arg)
+  }.holds
+
+Without the annotation, Stainless times out when trying to prove equivalence. To help with the proof, the user would have to write more details:
+
+.. code-block:: scala
+
+  def zero_check(arg: BigInt): Boolean = {
+    zero1(arg) == zero2(arg)
+  }.holds because {
+    if (arg > 0) zero_check(arg - 1)
+    else true
+  }
+
+With @traceInduct annotation, Stainless automatically comes up with a similar proof.
+
+
+It is possible to specify which function should serve as reference implementation for the inductive proof. This can be done by specifying the reference function name as @traceInduct parameter:
+
+.. code-block:: scala
+
+  def content(l: List[BigInt]): Set[BigInt] = l match {
+    case Nil() => Set.empty[BigInt]
+    case x::xs => Set(x) ++ content(xs)
+  }
+
+  def reverse(l1: List[BigInt], l2: List[BigInt]): List[BigInt] = l1 match {
+    case Nil() => l2
+    case x::xs => reverse(xs, x::l2)
+  }
+
+  @traceInduct("reverse")
+  def revPreservesContent(l1: List[BigInt], l2: List[BigInt]): Boolean = {
+    content(l1) ++ content(l2) == content(reverse(l1, l2))
+  }.holds
+
+Stainless constructs the proof based on the definition of the function reverse, by writing its name as annotation parameter. By induction on l1 and following the structure of the reverse function, Stainless manages to prove this lemma.
+
+Equivalence checking
+--------------------
+
+The first example of the previous section shows how @traceInduct annotation can be used to automate equivalence checking for pairs of functions. This way it is possible to verify given implementation by proving equivalence to some reference implementation.
+
+In batched mode, Stainless also supports checking equivalence of larger sets of functions. To avoid writing @traceInduct annotated lemmas for each pair, it is possible to specify the list of functions that we want to check for equivalence. Command line option --comparefuns is used for specifying the list of functions. Command line option --models is used for specifying the list of reference model functions. Those model functions are considered correct and serve as reference implementation for the inductive proof. 
+
+Stainless can automatically generate all the equivalence lemmas and report resulting equivalence classes. This is done by checking for eqivalence of each function from the --comparefuns list and each model function from the --models list, until the proof of equvalence or a counter example is found for one of the models.
+
+For example, when running Stainless with the following options (assuming that the file zero.scala contains functions f1, f2, f3, m1 and m2):
+
+.. code-block:: bash
+
+  $ stainless file.scala --batched=true --comparefuns=f1,f2,f3 --models=m1,m2 --timeout=5
+
+Stainless will try to prove equivalence for the following pairs of functions, assuming that f1 and f3 are equivalent to m1, and f2 is equivalent to m2 (but not m1):
+
+- f1 == m1 (verifies, no need to check for f1 == m2)
+- f2 == m1
+- f2 == m2
+- f3 == m1 (verifies, no need to check for f3 == m2)

From 7ed129f446224b09f3682842e0063e77bd0946a6 Mon Sep 17 00:00:00 2001
From: Dragana Milovancevic <milovanc@thinkpadx1e.epfl.ch>
Date: Wed, 31 Mar 2021 10:48:39 +0200
Subject: [PATCH 7/7] Update trace report printing

---
 .../main/scala/stainless/MainHelpers.scala    |  2 +-
 .../stainless/extraction/trace/Trace.scala    | 41 ++++++++++++++-----
 2 files changed, 31 insertions(+), 12 deletions(-)

diff --git a/core/src/main/scala/stainless/MainHelpers.scala b/core/src/main/scala/stainless/MainHelpers.scala
index 4b9956cc5a..88bb4c1688 100644
--- a/core/src/main/scala/stainless/MainHelpers.scala
+++ b/core/src/main/scala/stainless/MainHelpers.scala
@@ -168,7 +168,7 @@ trait MainHelpers extends inox.MainHelpers { self =>
 
       import ctx.{ reporter, timers }
 
-      if(!ctx.options.findOptionOrDefault(frontend.optBatchedProgram) && (!ctx.options.findOptionOrDefault(optModels).isEmpty || !ctx.options.findOptionOrDefault(optCompareFuns).isEmpty)) {
+      if (extraction.trace.Trace.optionsError) {
         reporter.error(s"Equivalence checking for --comparefuns and --models only works in batched mode.")
         System.exit(1)
       }
diff --git a/core/src/main/scala/stainless/extraction/trace/Trace.scala b/core/src/main/scala/stainless/extraction/trace/Trace.scala
index ae81e7ec9a..dadf988a17 100644
--- a/core/src/main/scala/stainless/extraction/trace/Trace.scala
+++ b/core/src/main/scala/stainless/extraction/trace/Trace.scala
@@ -68,7 +68,10 @@ trait Trace extends CachingPhase with SimpleFunctions with IdentitySorts { self
           Trace.setTrace(newFun.id)
           List(newFun)
         }
-        else Nil
+        else {
+          Trace.reportWrong
+          Nil
+        }
       }
       case _ => Nil
     }
@@ -172,7 +175,6 @@ trait Trace extends CachingPhase with SimpleFunctions with IdentitySorts { self
     val bodyPre = exprOps.withPrecondition(body, precondition)
     val bodyPost = exprOps.withPostcondition(bodyPre,postcondition)
     function.copy(function.id, function.tparams, function.params, function.returnType, bodyPost, function.flags)  
-
   }
 
   type Path = Seq[String]
@@ -217,15 +219,24 @@ object Trace {
   var clusters: Map[Identifier, List[Identifier]] = Map()
   var errors: List[Identifier] = List()
   var unknowns: List[Identifier] = List()
-
-  def printEverything() = {
+  var wrong: List[Identifier] = List()
+
+  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) {
-      System.out.println("clusters")   
-      System.out.println(clusters)
-      System.out.println("errors")
-      System.out.println(errors)
-      System.out.println("unknowns")
-      System.out.println(unknowns)
+      reporter.info(s"Printing equivalence checking results:")  
+      allModels.foreach(model => {
+        val l = clusters(model).mkString(", ")
+        reporter.info(s"List of functions that are equivalent to model $model: $l")
+      })
+      val errorneous = errors.mkString(", ")
+      reporter.info(s"List of erroneous functions: $errorneous")
+      val timeouts = unknowns.mkString(", ")
+      reporter.info(s"List of timed-out functions: $timeouts")
     }
   }
 
@@ -320,7 +331,10 @@ object Trace {
       else reportValid
       !isDone
     }
-    case None => false
+    case None => {
+      nextFunction
+      !isDone
+    }
   }
 
   private def isDone = function == None
@@ -342,4 +356,9 @@ object Trace {
     clusters = clusters + (model.get -> (function.get::clusters(model.get)))
     nextFunction
   }
+
+  private def reportWrong = {
+    trace = None
+    wrong = function.get::wrong
+  }
 }
\ No newline at end of file