Loop invariant inference?

[mschwerhoff]

Does Dafny (or Boogie) automatically apply loop invariant inference? Consider the following program:

method compute(a: int, b: int) returns (res: int)
  requires a >= 0
  ensures res == b + a
  decreases *  
{
  var x := a;
  res := b;

  while (x > 0) 
    invariant res == b + a - x
    // invariant x >= 0 // Dafny appears to infer this
    decreases *
  {
    x := x - 1;
    res := res + 1;
  }

  assert x == 0; // Verifies with and without invariant x >= 0
}

I remember that Dafny supported CLI option /noinfer to disable such inference, but this option doesn't seem to be supported anymore.

Is it still possible to disable inference?