From db471f821721028328b323eab0329e6f006a1fd6 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Fri, 23 Aug 2024 16:11:20 +0200 Subject: [PATCH 1/3] Flush SMT log before (check-sat) --- .../at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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 883ec6bc89..5019b7cac4 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) From 3c5f240d53e88ba04ff8b0647b058f4d4986f4ae Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Fri, 23 Aug 2024 16:12:09 +0200 Subject: [PATCH 2/3] 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) } From ecec7259b02e81657c9ca8e686bf071c6fc71f3a Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Fri, 23 Aug 2024 16:14:42 +0200 Subject: [PATCH 3/3] Update changelog --- .unreleased/bug-fixes/2962-fix-trunc-smt-log | 1 + 1 file changed, 1 insertion(+) create mode 100644 .unreleased/bug-fixes/2962-fix-trunc-smt-log 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