Refactor booster smt #4017
Merged
Refactor booster smt #4017
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
geo2a
reviewed
Aug 7, 2024
geo2a
reviewed
Aug 7, 2024
geo2a
approved these changes
Aug 7, 2024
jberthold
approved these changes
Aug 7, 2024
Comment on lines
+160
to
+161
| -- set large default timeout value for checking the prelude | ||
| setTimeout defaultSMTOptions.timeout |
There was a problem hiding this comment.
Is the default "large"?
I vaguely remember us discussing whether or not to use the user-provided modified timeout value for the prelude... not sure.
There was a problem hiding this comment.
The default is 125. Maybe it isn't that large actually. Either way, I was puzzled by this behaviour because the current code always overrides the user supplied value with 125, which is what I have done here as well. Perhaps we should just use the user defined value? @geo2a what do you think?
There was a problem hiding this comment.
Yes, let's use the user defined value here.
|
I will merge this and we can address the prelude timeout in a separate PR if need be. |
rv-jenkins
pushed a commit
that referenced
this pull request
Aug 12, 2024
Followup to #4017 addressing a potential issue I noticed whilst refactoring the SMT interface in booster. Namely, we set the hard-coded timeout value when checking the consistency of the prelude, before setting the user supplied value for general queries. This PR instead just sets the user supplied timeout value before checking the prelude.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The following changes were made:
Textreason in theUnknownconstructorisSat,checkPredicatesandgetModelForthrow errors as Exceptions and return anIsSatResult, as the only error we are catching is the one thrown when the SMT result is unknown