diff --git a/.unreleased/features/z3-stats.md b/.unreleased/features/z3-stats.md new file mode 100644 index 0000000000..a3011f003a --- /dev/null +++ b/.unreleased/features/z3-stats.md @@ -0,0 +1 @@ +Periodically print Z3 statistics when `--debug` is on (#2992) diff --git a/CHANGES.md b/CHANGES.md index bb75d1bb16..e0025d5475 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,12 @@ +## 0.45.6 - 2024-09-19 + +### Features + +- Added an `apalache-mc.bat` file to easily start Apalache on Windows, see #2980 + ## 0.45.4 - 2024-09-02 ### Features diff --git a/VERSION b/VERSION index 35fef456c5..c17c8e0466 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -0.45.5-SNAPSHOT +0.45.7-SNAPSHOT diff --git a/project/Dependencies.scala b/project/Dependencies.scala index c984a6feb0..574ff2cc52 100644 --- a/project/Dependencies.scala +++ b/project/Dependencies.scala @@ -21,7 +21,7 @@ object Dependencies { val commonsBeanutils = "commons-beanutils" % "commons-beanutils" % "1.9.4" // Apparently an untracked dependency of commonsConfiguration2 val commonsConfiguration2 = "org.apache.commons" % "commons-configuration2" % "2.11.0" - val commonsIo = "commons-io" % "commons-io" % "2.16.1" + val commonsIo = "commons-io" % "commons-io" % "2.17.0" val guice = "com.google.inject" % "guice" % "7.0.0" val kiama = "org.bitbucket.inkytonik.kiama" %% "kiama" % "2.5.1" val logbackClassic = "ch.qos.logback" % "logback-classic" % logbackVersion @@ -40,7 +40,7 @@ object Dependencies { val zio = "dev.zio" %% "zio" % zioVersion // Keep up to sync with version in plugins.sbt val zioGrpcCodgen = "com.thesamet.scalapb.zio-grpc" %% "zio-grpc-codegen" % "0.6.0-test3" % "provided" - val grpcNetty = "io.grpc" % "grpc-netty" % "1.66.0" + val grpcNetty = "io.grpc" % "grpc-netty" % "1.68.0" val scalapbRuntimGrpc = "com.thesamet.scalapb" %% "scalapb-runtime-grpc" % scalapb.compiler.Version.scalapbVersion // Ensures we have access to commonly used protocol buffers (e.g., google.protobuf.Struct) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala index d9f50d9dc7..71c00aa3c2 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala @@ -76,6 +76,8 @@ class BoundedCheckerPassImpl @Inject() ( val smtProfile = options.common.smtprof val smtRandomSeed = tuning.getOrElse("smt.randomSeed", "0").toInt + val smtStatsSec = + tuning.getOrElse("smt.statsSec", SolverConfig.default.z3StatsSec.toString).toInt // Parse the tuning parameters that are relevant to Z3. // Currently, `tuning` may contain more configuration options (added by some passes) than we parse in // `FineTuningParser`. @@ -83,7 +85,7 @@ class BoundedCheckerPassImpl @Inject() ( case Right(params) => params.map { case (k, v) => (k.substring("z3.".length), v) } case Left(error) => throw new PassOptionException(s"Error in tuning parameters: $error") } - val solverConfig = SolverConfig(debug, smtProfile, smtRandomSeed, smtEncoding, z3Parameters) + val solverConfig = SolverConfig(debug, smtProfile, smtRandomSeed, smtEncoding, smtStatsSec, z3Parameters) val result = options.checker.algo match { case Algorithm.Incremental => runIncrementalChecker(params, input, tuning, solverConfig) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/SolverConfig.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/SolverConfig.scala index 23482010a9..fcd282e5c9 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/SolverConfig.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/SolverConfig.scala @@ -25,6 +25,7 @@ sealed case class SolverConfig( profile: Boolean, randomSeed: Int, smtEncoding: SMTEncoding, + z3StatsSec: Int, z3Params: Map[String, Object] = Map()) {} object SolverConfig { @@ -34,5 +35,5 @@ object SolverConfig { */ val default: SolverConfig = new SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.OOPSLA19, - z3Params = Map()) + z3StatsSec = 60, z3Params = Map()) } 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 c17b7ed158..a978d637bb 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 @@ -18,6 +18,7 @@ import com.typesafe.scalalogging.LazyLogging import java.io.PrintWriter import java.util.concurrent.atomic.AtomicLong +import java.util.concurrent.locks.ReentrantLock import scala.collection.mutable import scala.collection.mutable.ListBuffer @@ -132,17 +133,61 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL */ private var maxCellIdPerContext = List(-1) + private trait ContextState + private case class Running() extends ContextState + private case class Disposed() extends ContextState + + // the state of the context: Running or Disposed + private var state: ContextState = Running() + + // the lock shared between the context and the statistics thread + private val statisticsLock: ReentrantLock = new ReentrantLock() + // start a new thread to collect statistics + private val statisticsThread = new Thread(() => { + while (state == Running()) { + // Sleep for a while. + // If we call printStatistics right away, we can easily run into a race condition with Z3 initializing. + // This produces a core dump. + Thread.sleep(config.z3StatsSec * 1000) + // make sure that the context is not being disposed right now. Otherwise, we can get a nice core dump. + statisticsLock.lock() + try { + if (state == Running()) { + printStatistics() + } + } finally { + statisticsLock.unlock() + } + } + }) + + if (config.debug && config.z3StatsSec > 0) { + statisticsThread.start() + } + /** * Dispose whatever has to be disposed in the end. */ override def dispose(): Unit = { logger.debug(s"Disposing Z3 solver context ${id}") - z3context.close() - closeLogs() - cellCache.clear() - inCache.clear() - funDecls.clear() - cellSorts.clear() + state = Disposed() + // Try to obtain the lock, to let the statistics thread finish its work. + // If it is stuck for some reason, continue after the timeout in any case. + statisticsLock.tryLock(2 * config.z3StatsSec, java.util.concurrent.TimeUnit.SECONDS) + try { + if (config.debug) { + printStatistics() + } + z3context.close() + closeLogs() + cellCache.clear() + inCache.clear() + funDecls.clear() + cellSorts.clear() + } finally { + // it's not that important at this point, but let's unlock it for the piece of mind + statisticsLock.unlock() + } } /** @@ -1026,6 +1071,14 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL flushLogs() throw e } + + private def printStatistics(): Unit = { + logger.info(s"Z3 statistics for context $id...") + val entries = z3solver.getStatistics.getEntries.map(stat => { + s"${stat.Key}=${stat.getValueString}" + }) + logger.info(entries.mkString(",") + "\n") + } } object Z3SolverContext { diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala index f55afdc52b..44b94ec10e 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala @@ -183,7 +183,8 @@ trait CrossTestEncodings extends AnyFunSuite with Checkers { val checkerParams = new ModelCheckerParams(checkerInput, 0) val solverContext = - new Z3SolverContext(new SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = smtEncoding)) + new Z3SolverContext(new SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = smtEncoding, + z3StatsSec = 0)) val rewriter: SymbStateRewriterImpl = smtEncoding match { case SMTEncoding.OOPSLA19 => new SymbStateRewriterImpl(solverContext, renaming) case SMTEncoding.Arrays => new SymbStateRewriterImplWithArrays(solverContext, renaming) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithArrays.scala index e6e69cfe9d..7a385d4646 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithArrays.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithArrays.scala @@ -13,7 +13,7 @@ import org.scalatestplus.junit.JUnitRunner class TestSeqModelCheckerWithArrays extends TestSeqModelCheckerTrait { override protected def withFixture(test: OneArgTest): Outcome = { val solver = RecordingSolverContext - .createZ3(None, SolverConfig(debug = false, profile = false, 0, smtEncoding = SMTEncoding.Arrays)) + .createZ3(None, SolverConfig(debug = false, profile = false, 0, z3StatsSec = 0, smtEncoding = SMTEncoding.Arrays)) val rewriter = new SymbStateRewriterImpl(solver, new IncrementalRenaming(new IdleTracker), new ExprGradeStoreImpl) test(rewriter) } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithFunArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithFunArrays.scala index 768510f257..ced0b710ed 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithFunArrays.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithFunArrays.scala @@ -13,7 +13,8 @@ import org.scalatestplus.junit.JUnitRunner class TestSeqModelCheckerWithFunArrays extends TestSeqModelCheckerTrait { override protected def withFixture(test: OneArgTest): Outcome = { val solver = RecordingSolverContext - .createZ3(None, SolverConfig(debug = false, profile = false, 0, smtEncoding = SMTEncoding.FunArrays)) + .createZ3(None, + SolverConfig(debug = false, profile = false, 0, z3StatsSec = 0, smtEncoding = SMTEncoding.FunArrays)) val rewriter = new SymbStateRewriterImpl(solver, new IncrementalRenaming(new IdleTracker), new ExprGradeStoreImpl) test(rewriter) } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithOOPSLA19.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithOOPSLA19.scala index c0140039bc..44d0df1e92 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithOOPSLA19.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithOOPSLA19.scala @@ -13,7 +13,8 @@ import org.scalatestplus.junit.JUnitRunner class TestSeqModelCheckerWithOOPSLA19 extends TestSeqModelCheckerTrait { override protected def withFixture(test: OneArgTest): Outcome = { val solver = RecordingSolverContext - .createZ3(None, SolverConfig(debug = false, profile = false, 0, smtEncoding = SMTEncoding.OOPSLA19)) + .createZ3(None, + SolverConfig(debug = false, profile = false, 0, z3StatsSec = 0, smtEncoding = SMTEncoding.OOPSLA19)) val rewriter = new SymbStateRewriterImpl(solver, new IncrementalRenaming(new IdleTracker), new ExprGradeStoreImpl) test(rewriter) } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithArrays.scala index 06bdac0974..ba43176647 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithArrays.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithArrays.scala @@ -8,7 +8,8 @@ import org.scalatestplus.junit.JUnitRunner @RunWith(classOf[JUnitRunner]) class TestRecordingSolverContextWithArrays extends TestRecordingSolverContext { override protected def withFixture(test: NoArgTest): Outcome = { - solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.Arrays) + solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, + smtEncoding = SMTEncoding.Arrays) test() } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithFunArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithFunArrays.scala index d6aa779b3d..9463feb097 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithFunArrays.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithFunArrays.scala @@ -8,7 +8,8 @@ import org.scalatestplus.junit.JUnitRunner @RunWith(classOf[JUnitRunner]) class TestRecordingSolverContextWithFunArrays extends TestRecordingSolverContext { override protected def withFixture(test: NoArgTest): Outcome = { - solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.FunArrays) + solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, + smtEncoding = SMTEncoding.FunArrays) test() } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithOOPSLA19.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithOOPSLA19.scala index 41e8153c4b..b5dd9265b3 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithOOPSLA19.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithOOPSLA19.scala @@ -8,7 +8,8 @@ import org.scalatestplus.junit.JUnitRunner @RunWith(classOf[JUnitRunner]) class TestRecordingSolverContextWithOOPSLA19 extends TestRecordingSolverContext { override protected def withFixture(test: NoArgTest): Outcome = { - solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.OOPSLA19) + solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, + smtEncoding = SMTEncoding.OOPSLA19) test() } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndArrays.scala index 3b0f552d11..4a0401caac 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndArrays.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndArrays.scala @@ -12,7 +12,7 @@ class TestTransitionExecutorWithIncrementalAndArrays with TestFilteredTransitionExecutor[IncrementalExecutionContextSnapshot] { override protected def withFixture(test: OneArgTest): Outcome = { val solver = - new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0, + new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, smtEncoding = SMTEncoding.Arrays)) withFixtureInContext(solver, new IncrementalExecutionContext(_), test) } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndFunArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndFunArrays.scala index ef0afec8ce..dca20cf4fe 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndFunArrays.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndFunArrays.scala @@ -11,7 +11,7 @@ class TestTransitionExecutorWithIncrementalAndFunArrays extends TestTransitionExecutorImpl[IncrementalExecutionContextSnapshot] with TestFilteredTransitionExecutor[IncrementalExecutionContextSnapshot] { override protected def withFixture(test: OneArgTest): Outcome = { - val solver = new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0, + val solver = new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, smtEncoding = SMTEncoding.FunArrays)) withFixtureInContext(solver, new IncrementalExecutionContext(_), test) } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndOOPSLA19.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndOOPSLA19.scala index b697502d79..3cb658ab3d 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndOOPSLA19.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndOOPSLA19.scala @@ -18,7 +18,7 @@ class TestTransitionExecutorWithIncrementalAndOOPSLA19 with TestFilteredTransitionExecutor[IncrementalExecutionContextSnapshot] { override protected def withFixture(test: OneArgTest): Outcome = { val solver = - new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0, + new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, smtEncoding = SMTEncoding.OOPSLA19)) withFixtureInContext(solver, new IncrementalExecutionContext(_), test) } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndArrays.scala index f96b0133cf..b4df42ad9d 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndArrays.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndArrays.scala @@ -12,7 +12,9 @@ import org.scalatestplus.junit.JUnitRunner class TestTransitionExecutorWithOfflineAndArrays extends TestTransitionExecutorImpl[OfflineExecutionContextSnapshot] { override protected def withFixture(test: OneArgTest): Outcome = { val solver = RecordingSolverContext - .createZ3(None, SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.Arrays)) + .createZ3(None, + SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, + smtEncoding = SMTEncoding.Arrays)) withFixtureInContext(solver, new OfflineExecutionContext(_, new IncrementalRenaming(new IdleTracker)), test) } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndFunArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndFunArrays.scala index 701d8fcbe0..e4dec6e82c 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndFunArrays.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndFunArrays.scala @@ -13,7 +13,9 @@ class TestTransitionExecutorWithOfflineAndFunArrays extends TestTransitionExecutorImpl[OfflineExecutionContextSnapshot] { override protected def withFixture(test: OneArgTest): Outcome = { val solver = RecordingSolverContext - .createZ3(None, SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.FunArrays)) + .createZ3(None, + SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, + smtEncoding = SMTEncoding.FunArrays)) withFixtureInContext(solver, new OfflineExecutionContext(_, new IncrementalRenaming(new IdleTracker)), test) } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndOOPSLA19.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndOOPSLA19.scala index 85ca1e0edb..1ff9ad4d81 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndOOPSLA19.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndOOPSLA19.scala @@ -18,7 +18,9 @@ import org.scalatestplus.junit.JUnitRunner class TestTransitionExecutorWithOfflineAndOOPSLA19 extends TestTransitionExecutorImpl[OfflineExecutionContextSnapshot] { override def withFixture(test: OneArgTest): Outcome = { val solver = RecordingSolverContext - .createZ3(None, SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.OOPSLA19)) + .createZ3(None, + SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, + smtEncoding = SMTEncoding.OOPSLA19)) withFixtureInContext(solver, new OfflineExecutionContext(_, new IncrementalRenaming(new IdleTracker)), test) } }