Fix profiling: use --verbosity 8 instead of 10#8977
Fix profiling: use --verbosity 8 instead of 10#8977tautschnig wants to merge 1 commit intodiffblue:developfrom
Conversation
Verbosity 10 triggers per-step SSA output via SSA_stept::output, which calls format_rec and accounts for ~16% of the profile. This distorts the results. Verbosity 8 still captures Runtime statistics without the per-step output. Co-authored-by: Kiro <[email protected]>
There was a problem hiding this comment.
Pull request overview
Note
Copilot was unable to run its full agentic suite in this review.
This PR adjusts the profiling runner to avoid distorting profiling results by preventing CBMC from emitting expensive per-step SSA output.
Changes:
- Lower CBMC verbosity from 10 to 8 in the profiling runner to keep runtime statistics without per-step SSA output.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| if not any(a in cmd for a in ("--dimacs", "--smt2", "--show-vcc")): | ||
| cmd += ["--dimacs", "--outfile", "/dev/null"] | ||
| cmd += ["--verbosity", "10"] | ||
| cmd += ["--verbosity", "8"] |
There was a problem hiding this comment.
This introduces a new implicit tuning parameter (verbosity level) as a magic number. Consider defining a named constant (e.g., CBMC_PROFILE_VERBOSITY = 8) or making it configurable via a CLI flag/env var for the runner, so future profiling runs can adjust verbosity without editing code.
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #8977 +/- ##
========================================
Coverage 80.50% 80.50%
========================================
Files 1704 1704
Lines 188778 188778
Branches 73 73
========================================
+ Hits 151975 151978 +3
+ Misses 36803 36800 -3 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
Verbosity 10 triggers per-step SSA output via SSA_stept::output, which calls format_rec and accounts for ~16% of the profile. This distorts the results. Verbosity 8 still captures Runtime statistics without the per-step output.