add a function to get the SMT lib ID from the solver if needed (#206)

src/main/scala/inox/solvers/Solver.scala

@@ -28,6 +28,10 @@ trait AbstractSolver extends Interruptible {
   // This is ugly, but helpful for smtlib solvers
   def dbg(msg: => Any): Unit = {}
 
+  // Used to report SMT Lib files <-> VCs correspondence
+  // Therefore it should be overriden in solvers that extends SMTLibDebugger traits
+  def getSmtLibFileId: Option[Int] = None
+
   object SolverUnsupportedError {
     def msg(t: Tree, reason: Option[String]) = {
       s"(of ${t.getClass}) is unsupported by solver $name" + reason.map(":\n  " + _ ).getOrElse("")

src/main/scala/inox/solvers/SolverFactory.scala

@@ -280,6 +280,9 @@ object SolverFactory {
 
           // encoder is from TipDebugger and enc from AbstractUnrollingSolver
           override protected val encoder = enc
+
+          // Used to report SMT Lib files <-> VCs correspondence
+          override def getSmtLibFileId: Option[Int] = underlying.getSmtLibFileId
         }
 
         () => new SMTZ3Impl(p)(enc)(ChooseEncoder(p)(enc))
@@ -307,6 +310,9 @@ object SolverFactory {
 
           protected val underlying = nonIncrementalWrap(targetProgram)(finalName, targetSemantics, () => new Underlying(targetProgram))
 
+          // Used to report SMT Lib files <-> VCs correspondence
+          override def getSmtLibFileId: Option[Int] = underlying.getSmtLibFileId
+
           // encoder is from TipDebugger and enc from AbstractUnrollingSolver
           override protected val encoder = enc
         }
@@ -336,6 +342,9 @@ object SolverFactory {
 
           protected val underlying = nonIncrementalWrap(targetProgram)(finalName, targetSemantics, () => new Underlying(targetProgram))
 
+          // Used to report SMT Lib files <-> VCs correspondence
+          override def getSmtLibFileId: Option[Int] = underlying.getSmtLibFileId
+
           // encoder is from TipDebugger and enc from AbstractUnrollingSolver
           override protected val encoder = enc
         }

src/main/scala/inox/solvers/combinators/NonIncrementalSolver.scala

@@ -18,6 +18,11 @@ trait NonIncrementalSolver extends AbstractSolver { self =>
     type Model = self.Model
   }
 
+  // Used to report SMT Lib files <-> VCs correspondence
+  override def getSmtLibFileId: Option[Int] = currentSolver match
+    case Some(solver) => solver.getSmtLibFileId
+    case None => None
+
   val assertions: IncrementalSeq[Trees] = new IncrementalSeq[Trees]
 
   var currentSolver: Option[AbstractSolver] = None

src/main/scala/inox/solvers/combinators/PortfolioSolver.scala

@@ -20,6 +20,9 @@ trait PortfolioSolver extends Solver { self =>
   val solvers: Seq[SubSolver]
   val name = "Pfolio"
 
+  // Used to report SMT Lib files <-> VCs correspondence
+  override def getSmtLibFileId: Option[Int] = if solvers.isEmpty then None else solvers.head.getSmtLibFileId
+
   protected var resultSolver: Option[Solver] = None
 
   private[this] var tasks: Future[Unit] = Future(())

src/main/scala/inox/solvers/smtlib/SMTLIBDebugger.scala

@@ -22,14 +22,26 @@ trait SMTLIBDebugger extends SMTLIBTarget {
     super.free()
     debugOut.foreach(_.close())
   }
+  lazy private val file = options.findOptionOrDefault(Main.optFiles).headOption.map(_.getName).getOrElse("NA")
+  lazy private val smtLibFileId: Int = DebugFileNumbers.next(targetName + file)
 
+  /**
+   * Returns the SMT-lib file query ID if the debug=smt option is activated, otherwise None
+   * @return
+   */
+  def getSmtLibFileIdIfDebug: Option[Int] = {
+    given DebugSectionSMT.type = DebugSectionSMT
+    if (reporter.isDebugEnabled) {
+      Some(smtLibFileId)
+    } else {
+      None
+    }
+  }
   /* Printing VCs */
   protected lazy val debugOut: Option[java.io.FileWriter] = {
     given DebugSectionSMT.type = DebugSectionSMT
     if (reporter.isDebugEnabled) {
-      val file = options.findOptionOrDefault(Main.optFiles).headOption.map(_.getName).getOrElse("NA")
-      val n = DebugFileNumbers.next(targetName + file)
-      val fileName = s"smt-sessions/$targetName-$file-$n.smt2"
+      val fileName = s"smt-sessions/$targetName-$file-$smtLibFileId.smt2"
 
       val javaFile = new java.io.File(fileName)
       javaFile.getParentFile.mkdirs()

src/main/scala/inox/solvers/smtlib/SMTLIBSolver.scala

@@ -40,6 +40,8 @@ abstract class SMTLIBSolver private(override val program: Program,
     }
   }
 
+  override def getSmtLibFileId: Option[Int] = this.getSmtLibFileIdIfDebug
+
   /* Public solver interface */
   def assertCnstr(expr: Expr): Unit = {
     variablesOf(expr).foreach(declareVariable)

src/main/scala/inox/solvers/z3/NativeZ3Solver.scala

@@ -23,6 +23,8 @@ class NativeZ3Solver(override val program: Program)
 
   protected val underlying =
     NativeZ3Solver.synchronized(new Underlying(targetProgram, self.context)(using targetSemantics))
+
+
 
   override def free(): Unit = NativeZ3Solver.synchronized(super.free())