Verification issue

[kjx]

Failing code

type Mode = nat

class Object {

    var fields : map<string,Object>
    var fieldModes : map<string,Mode>

    predicate Ready()
       reads this`fields, this`fieldModes
       { fields.Keys <= fieldModes.Keys }
}

predicate regression(os : set<Object>)
    requires forall o <- os :: o.Ready()
    reads os`fields, os`fieldModes
{
  (forall o <- os, n <- o.fields :: o.fieldModes[n] > 1)
}

Steps to reproduce the issue

• Dafny version: 4.9.2.0
• Dafny VSCode extension version: 3.4.3
• actually running dafny .nightly --version
  4.9.2+b79708edc871d0cd8149a03739641af63d06f8b5

Expected behavior

verifies - which it does on stock 4.9.0

Actual behavior

element might not be in domainVerifier on last line

ackage.dfy.txt

this is wrong because fields.Keys <= fieldModes.Keys;
so forall x <- fields.Keys :: x in fieldModes.Keys

inserting "assert forall o <- os :: o.Ready();"
before the last line gets it to verify on 4.9.2+b79708edc871d0cd8149a03739641af63d06f8b5