IDE shows "Verified", but input contains a resolution error

[cpitclaudel]

The following example confuses the IDE:

function f(x: nat) : nat

method test() {
  assert forall x: nat {:trigger false} :: f(x) == f(x);
}

It says verification succeeded, but the CLI says this instead:

"c:/Apps/dafny-3.3/Dafny.exe" "/compile:0" "c:/Users/cpitcla/wip/difftests/inconsistent.dfy"
c:/Users/cpitcla/wip/difftests/inconsistent.dfy(4,9): Error: trigger must mention all quantified variables, but does not mention: x#1
c:/Users/cpitcla/wip/difftests/inconsistent.dfy(4,9): Error: trigger must mention all quantified variables, but does not mention: x#1
2 name resolution errors detected in C:\Users\cpitcla\AppData\Local\Temp\inconsistent__module.bpl

*** Encountered internal translation error - re-running Boogie to get better debug information

C:\Users\cpitcla\AppData\Local\Temp\inconsistent__module.bpl(2871,6): Error: trigger must mention all quantified variables, but does not mention: x#1
C:\Users\cpitcla\AppData\Local\Temp\inconsistent__module.bpl(2875,6): Error: trigger must mention all quantified variables, but does not mention: x#1
2 name resolution errors detected in C:\Users\cpitcla\AppData\Local\Temp\inconsistent__module.bpl