You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
For ctrace enhanced with 2036 location invariants (generation of YAML file takes much less than a minute), validation takes undue amounts of time (5s of solving vs over 6min of validation).
Whether the validation time is excessive depends mostly on how long the analysis takes when all the same invariants are integrated as assertions and done during the analysis. Assert-instrumentation probably produces differently placed invariants than witness generation, so this might be difficult to compare.
I suspect it's just the overhead of actually abstractly evaluating thousands of expressions that simply adds up. It's the reason the benchmark scripts did two runs I think: one for performance and another for precision checking (or something like that).
On the faster server, 60 minutes seems to be enough to get verdicts everywhere, but it still seems odd that this takes orders of magnitude longer than analysis.
For
ctrace
enhanced with 2036 location invariants (generation of YAML file takes much less than a minute), validation takes undue amounts of time (5s of solving vs over 6min of validation).For the Octagon configuration, we even have a timeout after 30mins, even though analysis only takes 12.2s.
The text was updated successfully, but these errors were encountered: