Skip to content
New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Jump to bottom

per-goal timeout option doesn't seem to be working for yices #439

Closed
robdockins opened this issue Feb 12, 2020 · 1 comment · May be fixed by #617
Closed

per-goal timeout option doesn't seem to be working for yices #439

robdockins opened this issue Feb 12, 2020 · 1 comment · May be fixed by #617
Assignees
@atomb
Labels
crux what4
Milestone
Crux 0.5

Comments

@robdockins
Copy link
Contributor

crux verification goals do not seem to be honoring the goal timeout setting.
@atomb atomb added this to the Crux 0.5 milestone Dec 11, 2020
@atomb atomb self-assigned this Jan 15, 2021
kquick added a commit that referenced this issue Jan 17, 2021
@kquick
[crucible] Add deadman timeout for online solver actions
2ff4d64 
Fixes #439 by implementing
a parallel timeout operation (at 1 second longer than the timeout
requested of the solver itself) whose expiration causes the solver
process to be killed.

This helps with issue 439 because Yices encounters some internal
divergence issue that is not stopped by the specified timeout
value (demonstrable by running the crux-llvm
test-data/golden/strlen_test2 with the Yices solver option).

This also helps provide timeout management for solvers that do not
provide a built-in timeout capability (like Boolector).
@kquick kquick mentioned this issue Jan 17, 2021
Draft
@atomb
Copy link
Contributor

atomb commented Sep 22, 2021

This seems to be working now.

@atomb atomb closed this as completed Sep 22, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@atomb atomb

Labels
crux what4
Projects
None yet
Milestone
Crux 0.5
Development

Successfully merging a pull request may close this issue.

[crucible] Add deadman timeout for online solver actions GaloisInc/crucible
2 participants
@atomb @robdockins