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

Make obligation checking more configurable #1216

Merged
merged 16 commits into from
Jul 16, 2024
Merged

Make obligation checking more configurable #1216

merged 16 commits into from
Jul 16, 2024

Conversation

langston-barrett
Copy link
Contributor

@langston-barrett langston-barrett commented Jun 20, 2024 •
edited
Loading

  • Enable the use of online solvers
  • Enable clients to select between "failing fast" vs. "keeping going"
  • Timeouts for offline solvers
  • Parallel proving

@langston-barrett langston-barrett self-assigned this Jun 20, 2024
@langston-barrett langston-barrett marked this pull request as ready for review June 26, 2024 21:13
RyanGlScott
RyanGlScott approved these changes Jul 1, 2024
View reviewed changes
crucible/src/Lang/Crucible/Backend/Prove.hs Outdated Show resolved Hide resolved
crucible/src/Lang/Crucible/Backend/Prove.hs Outdated Show resolved Hide resolved
crucible/src/Lang/Crucible/Backend/Prove.hs Outdated Show resolved Hide resolved
crucible/src/Lang/Crucible/Backend/Prove.hs Show resolved Hide resolved
@langston-barrett langston-barrett mentioned this pull request Jul 3, 2024
Closed
@langston-barrett
Copy link
Contributor Author

(This is just waiting for me to test this in my downstream codebase to confirm it all works as expected there)

@langston-barrett langston-barrett merged commit c310fcb into GaloisInc:master Jul 16, 2024
32 checks passed
@langston-barrett langston-barrett deleted the lb/prove-goals-faster branch July 16, 2024 16:04
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@sauclovian-g sauclovian-g sauclovian-g left review comments

@RyanGlScott RyanGlScott RyanGlScott approved these changes

Assignees

@langston-barrett langston-barrett

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@langston-barrett @RyanGlScott @sauclovian-g