Quantifiers break lockstep unfolding of recursive functions and predicates

[mschwerhoff]

Viper ensures that Z3 may unroll a recursive function as deep as the predicates it depends on where manually (un)folded. Canonical example is a linked list and its recursively defined length function. E.g.

...
fold(list(x1)) // x1.next is null
...
fold(list(x4)) // x4.next is x3, x3.next is x2, x2.next is x1
assert length(x4) == 4

However, neither Silicon nor Carbon appear to support this lock-step approach when quantifiers are involved: either in the form of QPs, but also when the recursion is under a quantifier.

See also:

• Test case for this issue: 0455.vpr
• Corresponding Silicon issue: #494
• Corresponding Carbon issue: #356