Supporting timeouts

[bruderj15]

Hello there.

Z3 supports setting timeout as an option.

; time in millis
(set-option :timeout 10000)

Would be cool if the winning solver for QF_LRA and QF_LIA supported this as well.

NB: Congrats on the great result in SMT-COMP 2024!

[blishko]

Thank you!

Do you strictly need SMT-LIB options, or would a command-line option work as well?
Anyway, this would still require some work, we'll see what we can do. @Tomaqa

[bruderj15]

SMTLib-option would be preferred for unity across solvers.
This screams like someone should propose it for a future SMTLib version.

As this is may take too much effort for you guys, I will let the host-language handle this in my case (Haskell).

Thanks for the fast reply!

[Tomaqa]

Although it is not a standard option, it sounds reasonable. It is questionable though whether ms is the right unit here.