bruderj15 / Hasmtlib

A monad for interfacing with external SMT solvers
GNU General Public License v3.0
12 stars 1 forks source link

Setting solver timeouts #104

Closed bruderj15 closed 2 months ago

bruderj15 commented 2 months ago

Unfortunately the SMTLib Standard version 2.6 does not specify an option timeout. Some solvers like Z3 do:

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

However, most unfortunately do not (yet): https://github.com/usi-verification-and-security/opensmt/issues/766

We may just have Haskell handle this. At best something like:

setTimeout :: MonadSMT s m => Int -> m ()