timeout is not set when using yices

[danmatichuk]

Yices does not support (set-option :timeout <n>), and (set-timeout <n>) is not supported by yices-smt2.

The only available timeout option is passing --timeout <n> as a launch argument. However this does not work as expected due to a known issue with yices: SRI-CSL/yices2#547. Specifically calling (get-info :reason-unknown) after check-sat times out results in the error "can't tell until you call (check-sat)". This causes SBV to throw an exception due to the unexpected response.

Ideally this could be handled by SBV as a special case. When invoked manually at verbosity level 2, yices reports (check-sat: interrupted) when it times out.

As a side note, Yices interprets the argument to "--timeout" in seconds, in contrast to ":timeout" and ":tlimit" being interpreted as milliseconds.

[LeventErkok]

I'm not sure what sort of a solution would work the best here. You can tweak SBV to pass extra arguments as you wish, that's definitely the way to go for handling this one. (i.e., if you're using Yices, don't call setTimeOut, but tweak the arguments instead via:

proveWith yices{extraArgs = ["--timeout", "10"]} 

Regarding the handing of unknown response: Increasing verbosity would confuse a lot more in SBV as it tries to understand the output produced. That seems to be a non-starter.

If you've an alternative idea, feel free to send a PR and I'd be happy to merge. Otherwise, I don't see what course of action SBV can take here.

[LeventErkok]

@danmatichuk Is there more you need from SBV regarding this? I'm planning a release sometime this weekend and would be good to include whatever else might be needed.

[LeventErkok]

I'm assuming this is in good-shape, nothing more for SBV to do. I also noticed that the documentation for timeOut explicitly states that this call is "solver-dependent." See: https://hackage.haskell.org/package/sbv-11.0/docs/Data-SBV.html#v:setTimeOut:

Set a solver time-out value, in milli-seconds. This function essentially translates to the SMTLib call (set-info :timeout val), and your backend solver may or may not support it! The amount given is in milliseconds. Also see the function timeOut for finer level control of time-outs, directly from SBV.

I don't think Cryptol uses the query mode, so the finer timeout control is not directly usable to you. (In this case SBV itself controls the time-out, i.e., kills the solver if it doesn't respond in a given amount of time.)

In any case, I'm closing this ticket as I ready for a new release. But feel free to re-open/file a new issue if there's more SBV can do here.