Skip to content

proverTimeout is broken for What4-based solvers #1807

@RyanGlScott

Description

@RyanGlScott

Attempting to use a non-zero proverTimeout with any What4-based SMT solver will cause Cryptol to throw an exception. Example:

$ ~/Software/cryptol-3.2.0/bin/cryptol
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 3.2.0 (1bcb75c)
https://cryptol.net  :? for help

Loading module Cryptol
Cryptol> :set prover=w4-z3
Cryptol> :set proverTimeout=5
Cryptol> :prove \(x : [8]) -> x == x

What4 exception:
Failed to get solver.cvc4.timeout: not found

I suspect that the culprit is the following code:

setTimeout :: W4.IsExprBuilder sym => Integer -> sym -> IO ()
setTimeout s sym =
do symCfg sym W4.z3Timeout (1000 * s)
symCfg sym W4.cvc4Timeout (1000 * s)
symCfg sym W4.cvc5Timeout (1000 * s)
symCfg sym W4.boolectorTimeout (1000 * s)
symCfg sym W4.yicesGoalTimeout s -- N.B. yices takes seconds
pure ()

As seen above, we don't want to unconditionally set the timeout configuration settings for all SMT solvers, as each solver has its own settings. Instead, I think we need to do something solver-specific here.

Metadata

Metadata

Assignees

Labels

bugSomething not working correctlyproverIssues related to :sat and :prove

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions