Enable CBMC's equation-level slicer

[zhassan-aws]

Description of changes:

Use CBMC's equation-level slicer (--slice-formula). This results in a nice performance boost in some cases (e.g. s2n-quic's vectored_copy_u8) as well as some memory reduction.

	Default		With --slice-formula
Benchmark	Time (s)	Memory (MB)	Time (s)	Memory (MB)
s2n-quic vectored_copy_u8	125.8	2658	23.13	1768
Firecracker block example	4.75	213	3.2	127
Rectangle example	6.28	106	7.53	127
VecDeque CVE	0.57	191	0.26	190

Resolved issues:

Resolves #ISSUE-NUMBER

Call-outs:

The known side effect of using --slice-formula is that the trace generated by CBMC might exclude assignments to variables that are irrelevant to the check. This might actually be useful in since it could result in a smaller trace.

Testing:

• How is this change tested? Existing regressions

• Is this a refactor change? No

Checklist

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[adpaco-aws]

The resource usage increase in the rectangle example is surprising but the improvement in other ones means this is likely to boost performance in more complex proofs.

We should consider in the future adding all "CBMC optimization" flags into another set and allow users to opt out of it. But there's no need to do that now because, if I'm not mistaken, we'll be adding this but not #1221.