Definitions of function applications in postconditions of recursively called functions available too late

[marcoeilers]

The following verifies in Carbon but not in Silicon:

function fac(i: Int): Int
  ensures ge(result, 1)
{
  i <= 1 ? 1 : i * fac(i - 1)
}

function ge(i1: Int, i2: Int): Bool
{
  i1 >= i2
}

The issue is that the precondition propagation axiom for fac (which states that if the precondition of fac is satisfied, then the precondition of ge in its postcondition is also satisfied) is not available while verifying the body of fac, and thus the definition of ge cannot be used when learning the postcondition of the recursive call.

[marcoeilers]

Fixed in PR #745