Add the SMT lib file ID in the report table if the option debug=smt is enabled

bin/package-standalone.sh

@@ -37,7 +37,7 @@ Z3_WIN_NAME="z3-$Z3_VERSION-x64-win.zip"
 
 CVC5_GITHUB_URL="https://github.com/cvc5/cvc5/releases/download/cvc5-$CVC5_VERSION"
 CVC5_LICENSES_URL="https://raw.githubusercontent.com/cvc5/cvc5/main/licenses/"
-CVC5_LICENSES=("antlr3-LICENSE" "gpl-3.0.txt" "lgpl-3.0.txt")
+CVC5_LICENSES=("minisat-LICENSE" "gpl-3.0.txt" "lgpl-3.0.txt")
 CVC5_LINUX_NAME="cvc5-Linux"
 CVC5_MAC_ARM64_NAME="cvc5-macOS-arm64"
 CVC5_MAC_X64_NAME="cvc5-macOS"

build.sbt

@@ -278,7 +278,7 @@ val scriptSettings: Seq[Setting[_]] = Seq(
 def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
 
 // lazy val inox = RootProject(file("../inox"))
-lazy val inox = ghProject("https://github.com/epfl-lara/inox.git", "ae3eb97aaf50696bf416104ceae5b5d85be334db")
+lazy val inox = ghProject("https://github.com/epfl-lara/inox.git", "3b02dcf4308f9e8d74ea82304bd651be8e93517f")
 lazy val cafebabe = ghProject("https://github.com/epfl-lara/cafebabe.git", "616e639b34379e12b8ac202849de3ebbbd0848bc")
 
 // Allow integration test to use facilities from regular tests

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]
 )
 
 /**
@@ -77,12 +78,24 @@ trait AbstractReport[SelfType <: AbstractReport[SelfType]] { self: SelfType =>
  /** Filter, sort & process rows. */
  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)
+ val rows = for {
+ 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) => f"smt-lib-$v"
+ case None => ""
+ }
+ contents = Position.smartPos(pos) +: (name +: ((extra :+ f"${time / 1000d}%3.1f" ) :+ t))
  } yield Row(contents map { str => Cell(withColor(str, level)) })
+
+ // Delete the last cell if all are empty (i.e., the debug smt flag is false, and so smt-lib-id is empty)
+ val colorRegex = "\u001B\\[[;\\d]*m".r
+ if rows.forall(r => colorRegex.replaceAllIn(r.cells.last.vString, "").isBlank()) then {
+ rows.map(r => Row(r.cells.dropRight(1)))
+ } else {
+ rows
+ }
  }
 
  private def withColor(str: String, level: Level)(using inox.Context): String =
@@ -105,7 +118,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 +127,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)
  }