Extracting arguments from a function call reduces resource count

[keyboardDrummer]

The following two proofs surprisingly differ in their resource count usage:

predicate P(x: int)

method Foo() { // resource count 4102
  assert P(3 + 1 * 4 - 6 + 7); 
}

method Bar() { // resource count 4051
  var arg := 3 + 1 * 4 - 6 + 7;
  assert P(arg); 
}

You can see why by looking at the passified Boogie:

Foo (note the quadruplication of the argument to P):

    assume $_ModifiesFrame#AT#0 == lambda#0(null, $Heap, alloc, false);
    assume ##x#0#AT#0 == LitInt(3 + Mul(LitInt(1), LitInt(4)) - 6 + 7);
    assume $IsAlloc(##x#0#AT#0, TInt, $Heap);
    assume _module.__default.P#canCall(LitInt(3 + Mul(LitInt(1), LitInt(4)) - 6 + 7));
    assume _module.__default.P#canCall(LitInt(3 + Mul(LitInt(1), LitInt(4)) - 6 + 7));
    assert {:id "id0"} _module.__default.P(LitInt(3 + Mul(LitInt(1), LitInt(4)) - 6 + 7));
    return;

Bar:

    assume $_ModifiesFrame#AT#0 == lambda#0(null, $Heap, alloc, false);
    assume {:id "id1"} arg#0#AT#0 == LitInt(3 + Mul(LitInt(1), LitInt(4)) - 6 + 7);
    assume {:captureState "Scratchpad/Temp/temp.dfy(8,30)"} true;
    assume $IsAlloc(arg#0#AT#0, TInt, $Heap);
    assume _module.__default.P#canCall(arg#0#AT#0);
    assume _module.__default.P#canCall(arg#0#AT#0);
    assert {:id "id2"} _module.__default.P(arg#0#AT#0);
    return;

What's extra silly about the Foo translation is that it already creates a temporary variable to store the argument, ##x#0#AT#0, but then does not use that to prevent duplication.