Introduce --timeout in quint verify

[konnov]

As a follow-up to #1185, it would be great to have a timeout option for every individual symbolic run when quint verify is executed with --random-transitions. In my experiments, it happens that Apalache gets stuck on one of the randomly sequences. It would be great, if it could simply timeout after e.g. 10 min and try another choice of transitions. This should be doable by setting a z3 timeout in Apalache.

This would require changes both in Quint and Apalache.

[shonfeder]

On the apalache side, would it suffice to set search.smt.timeout or do we need to set something else?

As an aside: We have the option of making it easier to pass in any apalache configurations without having to add flags for them. So IMO we should be careful how many flags we add that just require mapping into the existing apalache config system, since it amounts to added complexity in our interface and CLI that doesn't translate into any increase in expressiveness or capability in the underlying system. This is mostly accidental complexity and makes the coupling between quint and apalache tighter, increasing the risk of breakage from integration mismatches.

[thpani]

Note to self: the right syntax for --apalache-config is:

{
  "checker": {
    "tuning": {
      "search.smt.timeout": 2
    }
  }
}

[thpani]

Blocked by apalache-mc/apalache#2316

Apalache currently quits the search (globally) if it runs into an SMT timeout

[thpani]

Addressed through apalache-mc/apalache#2758