Record the SMT input size for each split#938
Record the SMT input size for each split#938keyboardDrummer wants to merge 9 commits intoboogie-org:masterfrom
Conversation
… regressions in encoding performance
atomb
left a comment
atomb
left a comment
There was a problem hiding this comment.
This seems like a useful thing to have. I'd prefer to have the size increment and Send calls paired in a separate method, though I don't feel strongly about that.
|
|
||
| if (Process != null) | ||
| { | ||
| SentSize += s.Length; |
There was a problem hiding this comment.
It would be lovely if this could only be done from a wrapper around Send, to ensure that it's always incremented. It would be even nicer if the reset to size 0 could be encapsulated somewhere, too, though I remember from working on this code that there isn't a clear place to put it at the moment.
atomb
left a comment
atomb
left a comment
There was a problem hiding this comment.
This looks good overall, but it looks like there are some minor test fixes needed.
| // CHECK: \<assertionBatch number="1" iteration="0" startTime=".*"\> | ||
| // CHECK: \<assertion file="xml.bpl" line="25" column="3" /\> | ||
| // CHECK: \<conclusion duration=".*" outcome="valid" resourceCount=".*" /\> | ||
| // CHECK: \<conclusion duration=".*" outcome="valid" resourceCount=".*" smtInputSize="601" /\> |
There was a problem hiding this comment.
It looks like these values need updating again.
|
Currently sometimes |
2 participants
Changes
Record the SMT input string size for each split, which can be used to detect regressions in encoding performance
Testing
Updated existing test xml.bpl