Verification issue

[kjx]

Failing code

type Owner = set<Object>

class Object {

  const bound : Owner
  const AMFB  : Owner

  const xtrnl : Owner
  const AMFX :  Owner

  const ntrnl : Owner
  const AMFO  : Owner

  constructor  bake(oo : Owner, mb : Owner)
    requires oo >= mb
    {
      bound := mb;
      xtrnl := oo;
      ntrnl := oo + {this};
      AMFB  := flatten1(mb);
      AMFX  := flatten1(oo);
      AMFO  := flatten1(oo) + {this};
      new;

      assert forall o <- xtrnl :: AMFO > o.AMFO;

      assert
      && (AMFB == (set o <- bound, oo <- o.AMFO :: oo))
      && (AMFX == (set o <- xtrnl, oo <- o.AMFO :: oo))
      && (AMFO == (set o <- ntrnl, oo <- o.AMFO :: oo) +  {this})

      && (forall o <- bound :: o.Valid())
      && (forall o <- xtrnl :: o.Valid())
      ;
    }

  predicate Valid()
    {
      && (this  in AMFO)
      && (this !in AMFX)
      && (AMFO > AMFX >= AMFB)
    }
}

function flatten1(os : Owner) : (rv : Owner)  {set o <- os, oo <- o.AMFO :: oo}

Steps to reproduce the issue

• Dafny version: 4.9.2.0
• Dafny VSCode extension version: 3.4.3

Expected behavior

Code should verify or time out

Actual behavior

without a time limit, or a time limit >= 60s or thereabouts - dafny loops for ever.

this version fails reliably - longer versions would e.g. fail on recent versions of dafny, but work on dafny4.4, say, or work with --isolate-assertions but not without. "objectage-spike.dfy" (attached) does this against 4.9.2+a88767fb453b51d475667aab6f230711d7eeeb79, but verifies in 2.0s fine with 4.4.0+707b18acee078b3aa4d84c0590a980966bf22428,.

spike-bug4.dfy.txt
objectage-spike.dfy.txt

[keyboardDrummer]

I agree Dafny should have a default timeout. Created an explicit issue for that here: dafny-lang/dafny#6027