Continue simulation on SMT timeout in enabledness check

[thpani]

Prevent Apalache from halting the (global) search if an enabledness query times out in simulate.

This is a simple fix that considers a transition disabled if the corresponding SMT query times out in simulate mode.

A more comprehensive treatment of timeouts in simulate would be more invasive: It would require us to differentiate timeouts from other UNKNOWN Z3 results, and to define (or parameterize) the expected search behavior if invariant or deadlock checks time out during simulation.

Partially addresses #2316 and unblocks informalsystems/quint#1196.

• Tests added for any new code
• Ran make fmt-fix (or had formatting run automatically on all files edited)
• Documentation added for any new functionality
• Entries added to ./unreleased/ for any new functionality

[codecov-commenter]

Codecov Report

Merging #2758 (42d25ca) into main (5316435) will increase coverage by 0.00%.
The diff coverage is 0.00%.

@@           Coverage Diff           @@
##             main    #2758   +/-   ##
=======================================
  Coverage   78.86%   78.87%           
=======================================
  Files         464      464           
  Lines       15876    15878    +2     
  Branches     2557     2545   -12     
=======================================
+ Hits        12520    12523    +3     
+ Misses       3356     3355    -1     

Files	Coverage Δ
...t/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala	82.38% <0.00%> (-0.87%)	⬇️

... and 2 files with indirect coverage changes

📣 We’re building smart automated test selection to slash your CI/CD build times. Learn more

[konnov]

That's a nice and simple workaround! I guess, we cannot distinguish between UNKNOWN and TIMEOUT in this case, right?

[thpani]

I guess, we cannot distinguish between UNKNOWN and TIMEOUT in this case, right?

We could, but it would be a much bigger change, starting in Z3SolverContext.
I started working on it, but then gave up and decided this is probably the easier fix for now.
We can still pursue it if you think it's relevant.

[konnov]

I think it's fine, especially, in combination with the log message. It does solve the issue!