Merge pull request #2962 from apalache-mc/th/flush-logs

Flush SMT logs and SMT profiling logs before (check-sat)

.unreleased/bug-fixes/2962-fix-trunc-smt-log

@@ -0,0 +1 @@
+Fix truncation of SMT logs, see #2962

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImpl.scala

@@ -565,6 +565,7 @@ class SymbStateRewriterImpl(
   }
 
   override def flushStatistics(): Unit = {
+    profilerListener.foreach { _.dumpToFile() }
     statListener.locator.writeStats()
   }
 

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala

@@ -486,6 +486,7 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL
 
   override def sat(): Boolean = {
     log("(check-sat)")
+    flushLogs() // good time to flush
     val status = z3solver.check()
     log(s";; sat = ${status.name()}")
     flushLogs() // good time to flush
@@ -513,11 +514,12 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL
       // temporarily, change the timeout
       setTimeout(timeoutSec * 1000)
       log("(check-sat)")
+      flushLogs() // good time to flush
       val status = z3solver.check()
       log(s";; sat = ${status.name()}")
+      flushLogs() // good time to flush
       // return timeout to maximum
       setTimeout(Int.MaxValue)
-      flushLogs() // good time to flush
       status match {
         case Status.SATISFIABLE   => Some(true)
         case Status.UNSATISFIABLE => Some(false)

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/TransitionExecutorImpl.scala

@@ -318,6 +318,7 @@ class TransitionExecutorImpl[ExecCtxT](consts: Set[String], vars: Set[String], c
    *   timed out or reported *unknown*.
    */
   override def sat(timeoutSec: Int): Option[Boolean] = {
+    ctx.rewriter.flushStatistics()
     ctx.rewriter.solverContext.satOrTimeout(timeoutSec)
   }