Stefan Zetzsche

### Dafny version 4.7.0 ### Code to produce this issue ```dafny module M { function {:testEntry} F(xs: seq): seq requires |xs| > 0 requires forall i :: 0 xs[i] >...

Test generation cannot find witness for type nat

1

### Dafny version 4.7.0 ### Code to produce this issue ```dafny module M { method {:testEntry} plus_one(n: nat) { } } ``` ### Command to run and resulting output ```code...

### Description Addresses https://github.com/dafny-lang/dafny/issues/5372. ### How has this been tested? By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).

Fixes https://github.com/dafny-lang/dafny/issues/4364. ### Description The author of the issue argues that the types of `x` on line 12 and 21 should both be of type `int` (currently one is of...