-
Notifications
You must be signed in to change notification settings - Fork 273
Maintain ID_C_expr_simplified #37
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
Conversation
47ada4a
to
60d4be2
Compare
60d4be2
to
1a10146
Compare
1a10146
to
c3b8410
Compare
c3b8410
to
1dbac32
Compare
1dbac32
to
09ee69d
Compare
#else | ||
if(!local_replace_map.empty() && | ||
} | ||
#if 0 |
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.
@tautschnig, can you explain why this code is commented out?
Otherwise, this looks mergeable.
09ee69d
to
ff77afc
Compare
I have cleaned up the code that really was for debugging purposes only. |
ff77afc
to
b13b788
Compare
@tautschnig can you please rebase to fix the conflict and also see if all tests pass? |
b13b788
to
4a018c6
Compare
Rebased, all checks passing. As with #35, there is another question about performance, however. |
@kroening can you let me know if this is good to go or whom I should ask to evaluate the performance? |
It would be nice to have some continuous performance evaluations set up. As a first step, the scripting outlined in https://github.com/diffblue/cprover-sv-comp/blob/master/README.md could be picked up. That is, one would likely want a two-fold evaluation: monitor SV-COMP overall results, but also build and run with profiling data as 1) not every change results in immediate overall verification improvements and 2) overall improvement on any specific set of benchmarks (such as SV-COMP) is not necessarily representative. |
…vity-const-domain Variable Sensitivity Domain
4a018c6
to
88e52cf
Compare
…_make Only build CBMC directories we need
@tautschnig This has been stale for a while. I'm not sure if this still makes sense to do now 5 years later, if you want to revive this feel free to rebase and reopen, but closing for now. |
The aim is to avoid redundant invocations of the simplifier by storing is_simplified with each expression. This patch is the first part of this, then second half will be added once #25 is merged as there would be conflicting code changes.