Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

check if what4 adapter is present before setting timeout #1809

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

danmatichuk
Copy link

fixes #1807

Comment on lines +788 to +792
do symCfg cfg sym "Z3" W4.z3Timeout (1000 * s)
symCfg cfg sym "CVC4" W4.cvc4Timeout (1000 * s)
symCfg cfg sym "CVC5" W4.cvc5Timeout (1000 * s)
symCfg cfg sym "Boolector" W4.boolectorTimeout (1000 * s)
symCfg cfg sym "Yices" W4.yicesGoalTimeout s -- N.B. yices takes seconds
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Instead of having to enumerate all of the solvers and their timeout options, I wonder if we should do the following:

  1. Add a new field to AnOnlineAdapter (of type ConfigOption BaseIntegerType) to represent the timeout option for a particular solver.
  2. In setTimeout, match on cfg and apply the timeout option for each solver that is contained in the W4ProverConfig.

This approach has the advantage that we wouldn't need to remember to keep the implementation of this function in sync whenever Cryptol adds support for a new SMT solver. (In fact, I suspect that this function is already out of sync, since this function doesn't mention the recently-added Bitwuzla solver anywhere.)

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This makes sense to me, although I think we'll need an auxiliary config option for yices to account for the second/millisecond discrepancy vs. the rest of the solvers.

@RyanGlScott
Copy link
Contributor

Are you able to reproduce this test failure from CI locally? If so, do you know what might be causing it?

      issue_1807.icry: [Failed]
6c6,8
< Solver returned UNKNOWN
---
> 
> What4 exception:
> fd:18: hFlush: resource vanished (Broken pipe)

(I do not use macOS, so I am unable to reproduce it myself.)

@danmatichuk
Copy link
Author

I've seen this before and it's definitely an issue with What4 itself. It's highly nondeterministic from what I can tell.

I'll see if I can reproduce it on an up to date What4 build and raise a corresponding issue there. I believe it's limited to the cvc solvers, so we can remove those from the test for now.

# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

proverTimeout is broken for What4-based solvers
2 participants