Continue simulation on SMT timeout in enabledness check (#2758)

* Continue simulation on SMT timeout * Update changelog
apalache-mc · Oct 16, 2023 · c877256 · c877256
1 parent 5316435
commit c877256
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 2 deletions.
diff --git a/.unreleased/bug-fixes/2758-sim-timeout.md b/.unreleased/bug-fixes/2758-sim-timeout.md
@@ -0,0 +1 @@
+Continue simulation on SMT timeout in enabledness check, see #2758
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala
@@ -262,8 +262,12 @@ class SeqModelChecker[ExecutorContextT](
               logger.info(s"Step ${trex.stepNo}: Transition #$no is disabled")
 
             case None =>
-              searchState.onResult(RuntimeError())
-              return (Set.empty, Set.empty) // UNKNOWN or timeout
+              if (params.isRandomSimulation) {
+                logger.info(s"Step ${trex.stepNo}: Transition #$no enabledness is UNKNOWN; assuming it is disabled")
+              } else {
+                searchState.onResult(RuntimeError())
+                return (Set.empty, Set.empty) // UNKNOWN or timeout
+              }
           }
           // recover from the snapshot
           trex.recover(snapshot.get)