Test generation cannot find witness for type nat

[stefan-aws]

Dafny version

4.7.0

Code to produce this issue

module M {
method {:testEntry} plus_one(n: nat)
{
}
}

Command to run and resulting output

dafny generate-tests InlinedBlock nat.dfy

What happened?

Test generation yields the warning Warning: Cannot find witness for type nat. Please consider adding a witness to the declaration. Replacing nat with type mynat = n: int | 0 <= n witness 0 suppresses the warning.

These two issues related to subset types may be relevant: #4188 #2339

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

Mac