Uh oh!
There was an error while loading. Please reload this page.
Maintain ID_C_expr_simplified - #37
Conversation
47ada4a to
60d4be2Compare60d4be2 to
1a10146Compare1a10146 to
c3b8410Comparec3b8410 to
1dbac32Compare1dbac32 to
09ee69dCompareThere was a problem hiding this comment.
@tautschnig, can you explain why this code is commented out?
Otherwise, this looks mergeable.
09ee69d to
ff77afcComparetautschnig
commented
Jan 11, 2017
I have cleaned up the code that really was for debugging purposes only. |
ff77afc to
b13b788Compareforejtv
commented
Feb 21, 2017
@tautschnig can you please rebase to fix the conflict and also see if all tests pass? |
b13b788 to
4a018c6Comparetautschnig
commented
Feb 22, 2017
Rebased, all checks passing. As with #35, there is another question about performance, however. |
forejtv
commented
Feb 22, 2017
@kroening can you let me know if this is good to go or whom I should ask to evaluate the performance? |
tautschnig
commented
Feb 22, 2017
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
88e52cfCompare…_make Only build CBMC directories we need
hannes-steffenhagen-diffblue
commented
Feb 24, 2021
@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.