The opaque keyword does not always hide the body of functions

[keyboardDrummer]

Example:

function FibDef(n: nat): nat {
  if n < 2 then n else FibDef(n-1) + FibDef(n-2)
}

opaque function Hidden(): nat {
  3
}

opaque function Hidden2(): nat {
  FibDef(10)
}

function Visible(): nat {
  FibDef(10)
}

method User() { // Resource usage 3.74K RU
  var x := Hidden();
  assert 3 == 3;
}

method User2() { // Resource usage 5.86K RU
  var x := Hidden2();
  assert 3 == 3;
}

method User3() { // Resource usage 5.68K RU
  var x := Visible();
  assert 3 == 3;
}

You would expect User and User2 to have the same resource usage, and User3 to have a higher usage.