search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.92k stars 262 forks source link

Test generation cannot find witness for type nat #5607

Open stefan-aws opened 4 months ago

stefan-aws commented 4 months ago

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

stefan-aws commented 4 months ago

Temporary workaround was merged in https://github.com/dafny-lang/dafny/pull/5609. Does not fix the underlying issue.