Update traceInduct and clustering

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

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.")
       }

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)