assertion of map values fails when same postcondition succeeds (or if preceded by Keys assertion)

[kjx]

Dafny version

4.6.0.0 nightly

Code to produce this issue

class Object {}

method ISSUE( rm : map<Object,Object>, a : Object, b : Object, context : set<Object>) returns (m : map<Object,Object>)
   requires a !in rm.Keys
   ensures  a in m.Keys
   ensures  m.Keys == rm.Keys + {a}
   ensures  m.Values == rm.Values + {b}
{  
        m := rm[a:=b];
        //assert m.Keys == rm.Keys + {a};
        assert m.Values == rm.Values + {b};
}

Steps to reproduce the issue

• Dafny version: 4.6.0.0
• Dafny VSCode extension version: 3.3.0

Expected behavior

• vain hope that this verifies

Actual behavior

• it DOES verify, just "not like this" (to quote Switch from the Matrix)
• remove the Values assertion and the rest verifies - including the same assertion in the method spec
• uncomment the Keys assertion and the rest verifies

Command to run and resulting output

Just run Dafny

What happened?

I'd kind of hope it verifies...

Note I lodged this by pressing the IDE button, not realising that would put it in the wrong place: dafny-lang/ide-vscode#478

What type of operating system are you experiencing the problem on?

Mac

[kjx]

which is listed in the manual as desired behaviour - butI still think it's a BUG!

[fabiomadge]

I'd be interested to see the impact of always giving the necessary information. For now, I fixed the typos.