Flush SMT profiling info before (check-sat)

apalache-mc · Aug 23, 2024 · 3c5f240 · 3c5f240
1 parent db471f8
commit 3c5f240
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 0 deletions.
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImpl.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImpl.scala
@@ -563,6 +563,7 @@ class SymbStateRewriterImpl(
   }
 
   override def flushStatistics(): Unit = {
+    profilerListener.foreach { _.dumpToFile() }
     statListener.locator.writeStats()
   }
 

diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/TransitionExecutorImpl.scala b/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)
   }