`proverTimeout` is broken for various SBV-based solvers

[RyanGlScott]

Cryptol correctly propagates the proverTimeout setting to some SBV-based solvers, but not all of them. The sbv-bitwuzla, sbv-abc, and sbv-z3 solvers appear to do this correctly:

Cryptol> :set proverTimeout=1
Cryptol> :set prover=sbv-bitwuzla
Cryptol> :prove \(x : [8]) -> x == x
Q.E.D.
(Total Elapsed Time: 0.004s, using "Bitwuzla")
Cryptol> :set prover=sbv-abc
Cryptol> :prove \(x : [8]) -> x == x
Q.E.D.
(Total Elapsed Time: 0.032s, using "ABC")
Cryptol> :set prover=sbv-z3
Cryptol> :prove \(x : [8]) -> x == x
Q.E.D.
(Total Elapsed Time: 0.022s, using "Z3")

On the other hand, the sbv-cvc4, sbv-cvc5, sbv-boolector, and sbv-yices solvers all throw an exception when attempting to use the timeout:

Cryptol> :set proverTimeout=1
Cryptol> :set prover=sbv-cvc4
Cryptol> :prove \(x : [8]) -> x == x

SBV exception:

*** Data.SBV: Unexpected non-success response from CVC4:
***
***    Sent      : (set-option :timeout 1000)
***    Expected  : success
***    Received  : unsupported
***
***    Stderr    : CVC4 interrupted by SIGTERM.
***    Exit code : ExitFailure (-6)
***    Executable: /home/ryanscott/Software/what4-solvers/cvc4
***    Options   : --lang smt --incremental --interactive --no-interactive-prompt --model-witness-value
***
***    Reason    : Backend solver reports it does not support this option.
***                Check the spelling, and if correct please report this as a
***                bug/feature request with the solver!

Cryptol> :set prover=sbv-cvc5
Cryptol> :prove \(x : [8]) -> x == x

SBV exception:

*** Data.SBV: Unexpected non-success response from CVC5:
***
***    Sent      : (set-option :timeout 1000)
***    Expected  : success
***    Received  : unsupported
***
***    Stderr    : cvc5 interrupted by SIGTERM.
***    Exit code : ExitFailure (-15)
***    Executable: /home/ryanscott/Software/what4-solvers/cvc5
***    Options   : --lang smt --incremental --nl-cov
***
***    Reason    : Backend solver reports it does not support this option.
***                Check the spelling, and if correct please report this as a
***                bug/feature request with the solver!

Cryptol> :set prover=sbv-boolector
Cryptol> :prove \(x : [8]) -> x == x

SBV exception:

*** Data.SBV: fd:19: hGetLine: end of file:
***
***    Sent      : (set-option :timeout 1000)
***
***    Executable: /home/ryanscott/Software/what4-solvers/boolector
***    Options   : --smt2 -m --output-format=smt2 --no-exit-codes --incremental
***
***    Hint      : Solver process prematurely ended communication.
***                It is likely it was terminated because of a seg-fault.
***                Run with 'transcript=Just "bad.smt2"' option, and feed
***                the generated "bad.smt2" file directly to the solver
***                outside of SBV for further information.

Cryptol> :set prover=sbv-yices
Cryptol> :prove \(x : [8]) -> x == x

SBV exception:

*** Data.SBV: Unexpected non-success response from Yices:
***
***    Sent      : (set-option :timeout 1000)
***    Expected  : success
***    Received  : unsupported
***
***    Exit code : ExitFailure (-15)
***    Executable: /home/ryanscott/Software/what4-solvers/yices-smt2
***    Options   : --incremental
***
***    Reason    : Backend solver reports it does not support this option.
***                Check the spelling, and if correct please report this as a
***                bug/feature request with the solver!

The problem is that the code in Cryptol attempts to propagate proverTimeout information to all SBV-based solvers by sending the (set-option :timeout <NUM>) command:

cryptol/src/Cryptol/Symbolic/SBV.hs

Lines 110 to 119 in ba0f8d9

	setTimeoutSecs ::
	Int {- ^ seconds -} ->
	SBV.SMTConfig -> SBV.SMTConfig
	setTimeoutSecs s cfg = cfg
	{ SBV.solverSetOptions =
	SBV.OptionKeyword ":timeout" [show (toInteger s * 1000)] :
	filter (not . isTimeout) (SBV.solverSetOptions cfg) }
	where
	isTimeout (SBV.OptionKeyword k _) = k == ":timeout"
	isTimeout _ = False

But as seen above, not all solvers understand (set-option :timeout <NUM>). For instance, cvc5 configures a timeout by way of its --tlimit=<MILLISECONDS> command-line option.

We should figure out if SBV has a better way to configure timeout information that does the right thing for all solvers and do that instead.

[danmatichuk]

SBV does have a solver-independent mechanism for setting a timeout, but apparently that actually suffers from the same bug. I raised an issue, but I believe we can work around it for some of the solvers. In particular cvc4/5 can use "set-option :tlimit" instead of ":timeout".

[danmatichuk]

The yices manual indicates that set-timeout can be used to set a timeout, however yices-smt2 reports that this isn't a valid command.

It can be passed in at startup using --timeout, however this breaks the interaction with SBV due to this issue: SRI-CSL/yices2#547