add SMT lib file id to the report for each VC when debug=smt is enabled

core/src/main/scala/stainless/Report.scala

@@ -33,7 +33,8 @@ case class RecordRow(
   pos: Position,
   level: Level.Type,
   extra: Seq[String],
-  time: Long
+  time: Long,
+  smtLibId: Option[Int]
 )
 
 /**
@@ -78,10 +79,14 @@ trait AbstractReport[SelfType <: AbstractReport[SelfType]] { self: SelfType =>
   private def processRows(full: Boolean)(using ctx: inox.Context): Seq[Row] = {
     val printUniqueName = ctx.options.findOptionOrDefault(inox.ast.optPrintUniqueIds)
     for {
-      RecordRow(id, pos, level, extra, time) <- annotatedRows.sortBy(r => r.id -> r.pos)
+      RecordRow(id, pos, level, extra, time, smtLibId) <- annotatedRows.sortBy(r => r.id -> r.pos)
       if full || level != Level.Normal
       name = if (printUniqueName) id.uniqueName else id.name
-      contents = Position.smartPos(pos) +: (name +: (extra :+ f"${time / 1000d}%3.1f"))
+      t = smtLibId match {
+        case Some(v) => (extra :+ f"${time / 1000d}%3.1f" ) :+  f"smt-lib-$v"
+        case None => extra :+ f"${time / 1000d}%3.1f"
+      }
+      contents = Position.smartPos(pos) +: (name +: t)
     } yield Row(contents map { str => Cell(withColor(str, level)) })
   }
 
@@ -105,7 +110,7 @@ trait AbstractReport[SelfType <: AbstractReport[SelfType]] { self: SelfType =>
   def hasError(identifier: Option[Identifier])(using inox.Context): Boolean = identifier match {
     case None => false
     case Some(i) => annotatedRows.exists(elem => elem match {
-      case RecordRow(id, pos, level, extra, time) => {
+      case RecordRow(id, pos, level, extra, time, smtLibId) => {
         (level == Level.Error && id == i)
       }
     })
@@ -114,7 +119,7 @@ trait AbstractReport[SelfType <: AbstractReport[SelfType]] { self: SelfType =>
   def hasUnknown(identifier: Option[Identifier])(using inox.Context): Boolean = identifier match {
     case None => false
     case Some(i) => annotatedRows.exists(elem => elem match {
-      case RecordRow(id, pos, level, extra, time) => level == Level.Warning && id == i
+      case RecordRow(id, pos, level, extra, time, smtLibId) => level == Level.Warning && id == i
     })
   }
 

core/src/main/scala/stainless/equivchk/EquivalenceChecker.scala

@@ -467,7 +467,7 @@ class EquivalenceChecker(override val trees: Trees,
 
       val report = analysis.toReport
       val allCtexs = analysis.vrs.collect {
-        case (vc, VCResult(VCStatus.Invalid(VCStatus.CounterExample(model)), _, _)) =>
+        case (vc, VCResult(VCStatus.Invalid(VCStatus.CounterExample(model)), _, _, _)) =>
           ctexOrderedArguments(vc.fid, model.program)(model.vars).map(vc.fid -> _)
       }.flatten.groupMap(_._1)(_._2)
 

core/src/main/scala/stainless/equivchk/EquivalenceCheckingComponent.scala

@@ -235,7 +235,7 @@ class EquivalenceCheckingRun private(override val component: EquivalenceChecking
 
   private def counterExamples(analysis: VerificationAnalysis) = {
     analysis.vrs.collect {
-      case (vc, VCResult(VCStatus.Invalid(VCStatus.CounterExample(model)), _, _)) =>
+      case (vc, VCResult(VCStatus.Invalid(VCStatus.CounterExample(model)), _, _, _)) =>
         vc -> model
     }.toMap
   }

core/src/main/scala/stainless/equivchk/EquivalenceCheckingReport.scala

@@ -97,7 +97,7 @@ class EquivalenceCheckingReport(override val results: Seq[EquivalenceCheckingRep
       val level = levelOf(status)
       val solver = solverName getOrElse ""
       val extra = Seq(kind, statusName, solver)
-      RecordRow(id, pos, level, extra, time)
+      RecordRow(id, pos, level, extra, time, None)
   }
   lazy val totalConditions: Int = results.size
   lazy val totalTime: Long = results.map(_.time).sum

core/src/main/scala/stainless/evaluators/EvaluatorReport.scala

@@ -57,7 +57,7 @@ class EvaluatorReport(val results: Seq[EvaluatorReport.Record], val sources: Set
 
   override lazy val annotatedRows = results map {
     case Record(id, pos, status, time) =>
-      RecordRow(id, pos, levelOf(status), Seq(descriptionOf(status)), time)
+      RecordRow(id, pos, levelOf(status), Seq(descriptionOf(status)), time, None)
   }
 
   private lazy val totalTime = (results map { _.time }).sum

core/src/main/scala/stainless/genc/GenCComponent.scala

@@ -131,7 +131,7 @@ case class GenCReport(results: Seq[Record], sources: Set[Identifier], override v
   override val name = GenCComponent.name
 
   override def annotatedRows: Seq[RecordRow] = results.map {
-    case Record(id, pos, status, time) => RecordRow(id, pos, levelOf(status), Seq(descriptionOf(status)), time)
+    case Record(id, pos, status, time) => RecordRow(id, pos, levelOf(status), Seq(descriptionOf(status)), time, None)
   }
 
   protected def build(results: Seq[Record], sources: Set[Identifier]): GenCReport =

core/src/main/scala/stainless/termination/TerminationReport.scala

@@ -68,7 +68,7 @@ class TerminationReport(val results: Seq[TerminationReport.Record], val sources:
       val symbol = if (status.isTerminating) "\u2713" else "\u2717"
       val extra  = Seq(s"$symbol")
 
-      RecordRow(id, pos, level, extra, 0L)
+      RecordRow(id, pos, level, extra, 0L, None)
   }
 
   private def levelOf(status: Status) = status match {

core/src/main/scala/stainless/testgen/GenCTestGen.scala

@@ -19,7 +19,7 @@ object GenCTestGen {
                        (res: Map[VC[p.trees.type], VCResult[p.Model]])
                        (using ctx: inox.Context): Unit = {
     val counterExs = res.toSeq.collect {
-      case (vc, VCResult(VCStatus.Invalid(VCStatus.CounterExample(model)), _, _)) => (vc, model)
+      case (vc, VCResult(VCStatus.Invalid(VCStatus.CounterExample(model)), _, _, _)) => (vc, model)
     }
     if (counterExs.isEmpty) {
       return

core/src/main/scala/stainless/testgen/ScalaTestGen.scala

@@ -25,7 +25,7 @@ object ScalaTestGen {
                        (res: Map[VC[p.trees.type], VCResult[p.Model]])
                        (using ctx: inox.Context): Unit = {
     val counterExs = res.toSeq.collect {
-      case (vc, VCResult(VCStatus.Invalid(VCStatus.CounterExample(model)), _, _)) => (vc, model)
+      case (vc, VCResult(VCStatus.Invalid(VCStatus.CounterExample(model)), _, _, _)) => (vc, model)
     }
     if (counterExs.isEmpty) {
       return

core/src/main/scala/stainless/verification/CoqVerificationChecher.scala

@@ -38,7 +38,7 @@ trait CoqVerificationChecker { self =>
     val pCoq = CoqEncoder.transformProgram(program, context)
     CoqIO.makeOutputDirectory()
     val files = CoqIO.writeToCoqFile(pCoq.map { case (id, name, com) => (name, com) } )
-    val unknownResult: VCResult = VCResult(VCStatus.Unknown, None, None)
+    val unknownResult: VCResult = VCResult(VCStatus.Unknown, None, None, None)
     val vcs: Seq[VC] = pCoq map { case(fun, _, _) =>
       VC(getFunction(fun).fullBody, fun, VCKind.CoqMethod, true).setPos(symbols.getFunction(fun))
     }
@@ -76,7 +76,7 @@ trait CoqVerificationChecker { self =>
         case Failure(e) => reporter.internalError(e)
       }
 
-      vc -> VCResult(vcres, None, Some(time))
+      vc -> VCResult(vcres, None, Some(time), None)
     }}.toMap
     initMap ++ res
   }

core/src/main/scala/stainless/verification/VerificationAnalysis.scala

@@ -22,7 +22,8 @@ trait VerificationAnalysis extends AbstractAnalysis {
     val time = vr.time.getOrElse(0L) // TODO make time mandatory (?)
     val status = VerificationReport.Status(program)(vr.status)
     val source = symbols.getFunction(vc.fid).source
-    VerificationReport.Record(vc.fid, vc.getPos, time, status, vr.solverName, vc.kind.name, derivedFrom = source)
+    val smtFileId = vr.smtLibFileId
+    VerificationReport.Record(vc.fid, vc.getPos, time, status, vr.solverName, vc.kind.name, derivedFrom = source, smtId = smtFileId)
   }
 
   override val name = VerificationComponent.name

core/src/main/scala/stainless/verification/VerificationCache.scala

@@ -61,7 +61,7 @@ trait VerificationCache extends VerificationChecker { self =>
           debugVC(vc, origVC)
           reporter.debug("--------------")
         }
-        VCResult(VCStatus.ValidFromCache, None, None)
+        VCResult(VCStatus.ValidFromCache, None, None, None)
       } else {
         reporter.synchronized {
           reporter.debug(s"Cache miss: '${vc.kind}' VC for ${vc.fid.asString} @${vc.getPos}...")
@@ -94,7 +94,7 @@ trait VerificationCache extends VerificationChecker { self =>
     // Update the result with the correct processing time
     tryResult match {
       case Failure(e) => reporter.internalError(e)
-      case Success(VCResult(status, solver, _)) => VCResult(status, solver, Some(time))
+      case Success(VCResult(status, solver, _, smtLibFileId)) => VCResult(status, solver, Some(time), smtLibFileId)
     }
   }
 }

core/src/main/scala/stainless/verification/VerificationChecker.scala

@@ -117,7 +117,7 @@ trait VerificationChecker { self =>
     }
   }
 
-  private lazy val unknownResult: VCResult = VCResult(VCStatus.Unknown, None, None)
+  private lazy val unknownResult: VCResult = VCResult(VCStatus.Unknown, None, None, None)
 
   def checkVCs(vcs: Seq[VC], stopWhen: VCResult => Boolean = defaultStop): Future[Map[VC, VCResult]] = {
     if (!VerificationChecker.startedVerification.getAndSet(true)) reporter.info("Starting verification...")
@@ -280,7 +280,7 @@ trait VerificationChecker { self =>
     import SolverResponses._
     val cond = vc.condition
     if (cond == BooleanLiteral(true)) {
-      return VCResult(VCStatus.Trivial, None, None)
+      return VCResult(VCStatus.Trivial, None, None, None)
     }
 
     val s = sf.getNewSolver()
@@ -300,10 +300,10 @@ trait VerificationChecker { self =>
           s.check(Model)
         }
       }
-
+      
       val vcres = tryRes match {
         case _ if interruptManager.isInterrupted =>
-          VCResult(VCStatus.Cancelled, Some(s.name), Some(time))
+          VCResult(VCStatus.Cancelled, Some(s.name), Some(time), s.getSmtLibFileId)
 
         case Success(res) => res match {
           case Unknown =>
@@ -313,35 +313,35 @@ trait VerificationChecker { self =>
                 case _ => VCStatus.Unknown
               }
               case _ => VCStatus.Unknown
-            }, Some(s.name), Some(time))
+            }, Some(s.name), Some(time), s.getSmtLibFileId)
 
           case Unsat if !vc.satisfiability =>
-            VCResult(VCStatus.Valid, s.getResultSolver.map(_.name), Some(time))
+            VCResult(VCStatus.Valid, s.getResultSolver.map(_.name), Some(time), s.getSmtLibFileId)
 
           case SatWithModel(model) if checkModels && vc.kind.isInstanceOf[VCKind.AdtInvariant] =>
             val VCKind.AdtInvariant(invId) = vc.kind: @unchecked
             val status = checkAdtInvariantModel(vc, invId, model)
-            VCResult(status, s.getResultSolver.map(_.name), Some(time))
+            VCResult(status, s.getResultSolver.map(_.name), Some(time), s.getSmtLibFileId)
 
           case SatWithModel(model) if !vc.satisfiability =>
-            VCResult(VCStatus.Invalid(VCStatus.CounterExample(model)), s.getResultSolver.map(_.name), Some(time))
+            VCResult(VCStatus.Invalid(VCStatus.CounterExample(model)), s.getResultSolver.map(_.name), Some(time), s.getSmtLibFileId)
 
           case Sat if vc.satisfiability =>
-            VCResult(VCStatus.Valid, s.getResultSolver.map(_.name), Some(time))
+            VCResult(VCStatus.Valid, s.getResultSolver.map(_.name), Some(time), s.getSmtLibFileId)
 
           case Unsat if vc.satisfiability =>
-            VCResult(VCStatus.Invalid(VCStatus.Unsatisfiable), s.getResultSolver.map(_.name), Some(time))
+            VCResult(VCStatus.Invalid(VCStatus.Unsatisfiable), s.getResultSolver.map(_.name), Some(time), s.getSmtLibFileId)
 
           case _ => sys.error(s"Unreachable: $res")
         }
 
         case Failure(u: inox.Unsupported) =>
           reporter.warning(u.getMessage)
-          VCResult(VCStatus.Unsupported, Some(s.name), Some(time))
+          VCResult(VCStatus.Unsupported, Some(s.name), Some(time), s.getSmtLibFileId)
 
         case Failure(e @ NotWellFormedException(d, info)) =>
           reporter.error(d.getPos, e.getMessage)
-          VCResult(VCStatus.Crashed, Some(s.name), Some(time))
+          VCResult(VCStatus.Crashed, Some(s.name), Some(time), s.getSmtLibFileId)
 
         case Failure(e) => reporter.internalError(e)
       }

core/src/main/scala/stainless/verification/VerificationComponent.scala

@@ -116,11 +116,11 @@ class VerificationRun private(override val component: VerificationComponent.type
       val opaqueEncoder = inox.transformers.ProgramEncoder(vcGenEncoder.targetProgram)(OpaqueChooseInjector(vcGenEncoder.targetProgram))
       val res: Future[Map[VC[p.trees.type], VCResult[p.Model]]] =
         if (context.options.findOptionOrDefault(optAdmitVCs)) {
-          Future(vcs.map(vc => vc -> VCResult(VCStatus.Admitted, None, None)).toMap)
+          Future(vcs.map(vc => vc -> VCResult(VCStatus.Admitted, None, None, None)).toMap)
         } else {
           VerificationChecker.verify(opaqueEncoder.targetProgram, context)(vcs).map(_.view.mapValues {
-            case VCResult(VCStatus.Invalid(VCStatus.CounterExample(model)), s, t) =>
-              VCResult(VCStatus.Invalid(VCStatus.CounterExample(model.encode(opaqueEncoder.reverse.andThen(vcGenEncoder.reverse)))), s, t)
+            case VCResult(VCStatus.Invalid(VCStatus.CounterExample(model)), s, t, smtid) =>
+              VCResult(VCStatus.Invalid(VCStatus.CounterExample(model.encode(opaqueEncoder.reverse.andThen(vcGenEncoder.reverse)))), s, t, smtid)
             case res => res.asInstanceOf[VCResult[p.Model]]
           }.toMap)
         }

core/src/main/scala/stainless/verification/VerificationConditions.scala

@@ -112,7 +112,8 @@ object VCStatus {
 case class VCResult[+Model](
   status: VCStatus[Model],
   solverName: Option[String],
-  time: Option[Long]
+  time: Option[Long],
+  smtLibFileId: Option[Int]
 ) {
   def isValid           = status == VCStatus.Valid || isValidFromCache || isTrivial
   def isValidFromCache  = status == VCStatus.ValidFromCache

core/src/main/scala/stainless/verification/VerificationReport.scala

@@ -51,7 +51,7 @@ object VerificationReport {
   case class Record(
     id: Identifier, pos: inox.utils.Position, time: Long,
     status: Status, solverName: Option[String], kind: String,
-    derivedFrom: Identifier
+    derivedFrom: Identifier, smtId: Option[Int]
   ) extends AbstractReportHelper.Record
 
   given recordDecoder: Decoder[Record] = deriveDecoder
@@ -84,12 +84,12 @@ class VerificationReport(val results: Seq[VerificationReport.Record], val source
   override val name = VerificationComponent.name
 
   override lazy val annotatedRows = results map {
-    case Record(id, pos, time, status, solverName, kind, _) =>
+    case Record(id, pos, time, status, solverName, kind, _, smtId) =>
       val level = levelOf(status)
       val solver = solverName getOrElse ""
       val extra = Seq(kind, status.name, solver)
 
-      RecordRow(id, pos, level, extra, time)
+      RecordRow(id, pos, level, extra, time, smtId)
   }