only do bitvector analysis when used

[kroening]

The bitvector analysis can be expensive in terms of time and memory.
This avoids doing it unless the result is actually used.

[tautschnig]

It would still be nice if such changes came with data, e.g., "before, doing X took N seconds; now this returns in M<N seconds."

[allredj]

This PR failed Diffblue compatibility checks (cbmc commit: cae4f30).
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

• the cbmc commit has disappeared in the mean time (e.g. in a force-push)
• the author is not in the list of contributors (e.g. first-time contributors).

[kroening]

Say goto-instrument --count-eloc on a larger goto-binary (with 10k ELOCs) is now 0.4s vs. 5.1s before.

[tautschnig]

Say goto-instrument --count-eloc on a larger goto-binary (with 10k ELOCs) is now 0.4s vs. 5.1s before.

Thanks - that's the sort of information I would expect to be included in commit messages by default. It's data that is trivial to gather while working on it, but a lot more effort to collect later on.

[kroening]

ok, done

[allredj]

This PR failed Diffblue compatibility checks (cbmc commit: 6a94dfb).
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

• the cbmc commit has disappeared in the mean time (e.g. in a force-push)
• the author is not in the list of contributors (e.g. first-time contributors).

[allredj]

This PR failed Diffblue compatibility checks (cbmc commit: a224e94).
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

• the cbmc commit has disappeared in the mean time (e.g. in a force-push)
• the author is not in the list of contributors (e.g. first-time contributors).