Optimizing generated termination checks to omit unfolds and condition…

[marcoeilers]

For unfolding-expressions of the form unfolding acc(P(args), p) in e, the termination plugin currently generates the following (simplified) termination check:

<check for args>
<check for p>
if (*) {
  unfold acc(P(args), p)
  <check for e>
  assume false
}

If there are no conditions to check for e, this code is currently still generated; in particular, the predicate is still unfolded inside a branch, and subsequently, we assume false. The unfold is completely unnecessary in this scenario though and could just be omitted.
Even though the code generated by the plugin is subsequently run through the Simplifier, this block is not removed, because it's not empty (it unfolds a predicate and assumes false, after all).
While this is not a problem for individual unfolds, the effect can cascade into situations where we perform multiple unfolds inside branches after other unfolds only to not actually check anything in the end, as shown in viperproject/silicon#934.

So this PR modifies the termination plugin to generate some code blocks that exist to check termination conditions for some expressions only if there are actually termination conditions to check for those expressions, and omits them otherwise. In particular, we do this for unfoldings (omit the unfold, as explained above), implications, disjunctions, and some conjunctions (remove the need to evaluate the condition), let-expressions (remove the need to evaluate the bound expression).

[jcp19]

LGTM