-
Notifications
You must be signed in to change notification settings - Fork 62
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.
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
Simple loop fixpoint2 #1553
Simple loop fixpoint2 #1553
Conversation
a156d15
to
fef99b7
Compare
@andreistefanescu, any ideas on how to make the new test faster? As I watch the CI, I'm seeing the awslc task is taking about 70 minutes building before it gets to the phase where it actually starts running the SAW proofs. |
src/SAWScript/Crucible/LLVM/X86.hs
Outdated
let uninterpreted_constants = foldMap | ||
(viewSome $ Set.map (mapSome $ W4.varExpr sym) . W4.exprUninterpConstants sym) | ||
(Some condition : body_exprs) | ||
let filtered_uninterpreted_constants = Set.toList $ Set.filter |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@andreistefanescu, can you say a little bit about what's going on here with this filtering function?
61f7fba
to
d546702
Compare
On a second look, I think the proofs are getting interleaved with compiling, so it isn't spending a full hour on compiles the way I thought initially. We should still maybe consider ways to speed up the CI, but it isn't as dire as I thought. |
@kquick, mostly interested in your thoughts about the CI impact |
d546702
to
321e1ed
Compare
No description provided.