Two more bugs:The latter, again, is not discovered by the fuzzer, but by trying to formalizing it (well, I still couldn't implement it either -- see the original thread for the problem and question).On Thu, Aug 26, 2021 at 4:49 AM Sorawee Porncharoenwase <firstname.lastname@example.org> wrote:Here's another bug: https://github.com/dafny-lang/dafny/issues/1387On Tue, Aug 24, 2021 at 2:40 PM Sorawee Porncharoenwase <email@example.com> wrote:One more bug:On Sun, Aug 22, 2021 at 5:34 PM Sorawee Porncharoenwase <firstname.lastname@example.org> wrote:More bugs!On Sun, Aug 22, 2021 at 12:56 PM John Regehr <email@example.com> wrote:I'm just sort of lurking here, but I've really been enjoying this
thread. Great work everyone!!!
> The latter one is not discovered by fuzzing itself. I was writing a type
> constraint to be put in the fuzzer, and thinking what will happen if we
> violate the constraint, so I tried it out manually and discovered the issue.
In my experience this happens a lot :)