Internal function preconditions not assumed in wand-related scenario

[marcoeilers]

The following program does not verify in Silicon: The apply fails because the wand is not found.

field val : Int;

function atMostb(x: Int, y: Int): Bool
{
 x <= y
}

method test08b() {
  var x: Int
  var y: Int

  package x <= y --* atMostb(x, y)
  assume x < y
  x := x + 1
  apply x <= y --* atMostb(x, y)  // fails: wand not found
}

If we use an equivalent domain function, everything is fine:

domain Foo {
  function atMosta(x: Int, y: Int): Bool

  axiom atMost_def {
    forall x: Int, y: Int :: atMosta(x, y) <==> x <= y
  }
}

method test08a() {
  var x: Int
  var y: Int

  package x <= y --* atMosta(x, y)
  assume x < y
  x := x + 1
  apply x <= y --* atMosta(x, y)  // verifies
}

The problem is not the structure of the wand, as I initially thought, but somehow atMostb%precondition is not assumed for the relevant arguments, so the definition of atMostb is not known and cannot be used to establish that atMostb(x, y) is still the same.