diff --git a/.unreleased/bug-fixes/2962-fix-trunc-smt-log b/.unreleased/bug-fixes/2962-fix-trunc-smt-log
new file mode 100644
index 0000000000..7f0cf369a9
--- /dev/null
+++ b/.unreleased/bug-fixes/2962-fix-trunc-smt-log
@@ -0,0 +1 @@
+Fix truncation of SMT logs, see #2962
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 be9b21862c..9c399c68e4 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
@@ -565,6 +565,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/smt/Z3SolverContext.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala
index 0303ab7091..76cac9981d 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala
+++ b/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)
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)
   }