Silver sometimes auto-generates triggers that cannot be used by Silicon because of missing old-wrappers

[marcoeilers]

For the following program

function foo(i: Int): Int
  requires i > 0
{
  i + 5
}

predicate P()
predicate Q() { true }

function bar(i: Int): Int
  requires i > 0
  requires P()

method m() 
  requires P()
  requires Q()
{
  assume forall i: Int ::  i > 0 ==> foo(i * 6 + 1 ) == old( unfolding Q() in bar(i))

  assert bar(8) == 48+1+5
}

Silver generates the trigger { bar(i) } for the assumed quantifier. However, Silicon cannot use this trigger (the warning Might not be able to use trigger bar(i), since it is not evaluated while evaluating the body of the quantifier is emitted). Silver should generate { old(bar(i)) } instead, since that is (ignoring the unfolding) the expression that actually occurs inside the quantifier, and that Silicon can use.