search

usi-verification-and-security / opensmt

The opensmt solver
Other
77 stars 18 forks source link

Supporting timeouts #766

Open bruderj15 opened 1 month ago

bruderj15 commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

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