From 3c5f240d53e88ba04ff8b0647b058f4d4986f4ae Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Fri, 23 Aug 2024 16:12:09 +0200 Subject: [PATCH] Flush SMT profiling info before (check-sat) --- .../at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImpl.scala | 1 + .../forsyte/apalache/tla/bmcmt/trex/TransitionExecutorImpl.scala | 1 + 2 files changed, 2 insertions(+) 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 index 11539bc03b..3de414aaf6 100644 --- 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 index 17f23c3a44..3fd7755c52 100644 --- 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) }