diff --git a/.unreleased/bug-fixes/2758-sim-timeout.md b/.unreleased/bug-fixes/2758-sim-timeout.md
new file mode 100644
index 0000000000..6710887e62
--- /dev/null
+++ 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
index e725879794..e7360504ff 100644
--- 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)