Inconsistent treatment of recursive function postconditions

[mschwerhoff]

It seems that for self-recursive functions, the callee's postcondition is available, see v1 below. For mutual recursive functions, however, the callee's postcondition does not seem to be available, see v2 below. This difference is probably not by design.

For what it is worth, blocks v3 and v4 show undesirable workarounds.

domain _ {
  function P(i: Int): Bool
  axiom { forall i: Int :: {P(i)} i < 0 ==> P(i) }
}

// ----------- v1 --------------

function f1(j: Int): Int
  ensures P(result) // Holds
{ j < 0 ? j : f1(j - 1) }

// ----------- v2 --------------

function f2(j: Int): Int
  ensures P(result) // Fails
{ j < 0 ? j : g2(j - 1) }

function g2(k: Int): Int
  ensures P(result) // Likewise
{ k < 0 ? k : f2(k - 1) }

// ----------- v3 --------------

function f3(j: Int): Int
  ensures P(f3(j)) // Holds
  decreases * // "j" ---> call in preceding line might not terminate; makes sense, and shows that "result" is not just syntactic sugar for "f3(j)"
{ j < 0 ? j : g3(j - 1) }

function g3(k: Int): Int
  ensures P(g3(k)) // Holds
  decreases * // "k" ---> analogous
{ k < 0 ? k : f3(k - 1) }

// ----------- v4 --------------

function f4(j: Int): Int
  ensures [P(result), true] // Holds trivially
{ j < 0 ? j : g4(j - 1) }

function g4(k: Int): Int
  ensures [P(result), true] // Likewise
{ k < 0 ? k : f4(k - 1) }

This problem was originally reported by Paul Winkler (thank you!).