Dafny unable to produce arbitrary witness element from set of nats in custom datatype

[efl9013]

Dafny version

4.1.0.0

Code to produce this issue

newtype Int = nat
datatype IntWrapper = Wrap(s: set<Int>)

method m(x: IntWrapper) {
  var iter := x.s;
  while iter != {}
    decreases |iter|
  {
    var i: Int :| i in iter;
    iter := iter - {i};
  }
}

Command to run and resulting output

VSCode verifier shows the following error message: 
cannot establish the existence of LHS values that satisfy the such-that predicate

What happened?

The current code fails at the line var i: Int :| i in iter; -- Dafny cannot find an arbitrary witness from the set iter of type set<nat>. However, if I change the newtype definition from newtype Int = nat to newtype Int = int, verification succeeds.

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

Mac

[fabiomadge]

The bug is in the generation of the axioms for newtypes. Until we can fix it, consider using newtype Int = n: nat | true
, or type Int = nat.