BranchSet: Possibilities for Optimization

[michael-schwarz]

Looking at the BranchSet analysis (#1792), I noticed an obvious deficiency in the way we use it for SV-COMP.

If we are fully context-sensitive, having the set of taken branches in the context and in the local state only causes a needless blowup of the number of contexts and of the size of the sets. This should be remedied by configuring the analysis the context-insensitive in SV-COMP and by starting with {} as the set of taken branches in enter.

---

Independent of this, we should look into ways to limit the size of the set, by, e.g., using some heuristic to identify "important" branches (easy) or collapsing the path-splitting where abstract values are identical (hard in our framework).

[sim642]

Independent of this, we should look into ways to limit the size of the set, by, e.g., using some heuristic to identify "important" branches (easy) or collapsing the path-splitting where abstract values are identical (hard in our framework).

I think we realized something similar with @karoliineh when looking at some SV-COMP prerun or experiment results recently. There are many crafted benchmarks (product-lines? ECA?) which contain functions that contain huge numbers of branchings (together with lots of logical operators). This admits an exponential number of subsets which would each be separate paths. And this is made worse by the quadratic complexity of our path-sensitivity.

This is also apparent in the SV-COMP "final" results, where 60% of timeouts/out of memorys come from level 3, which enables branchSet.