[xsmith-dev] Early Dafny Results (Re: XSmith questions)

[William G Hatch]

Thanks for the update, and I'm really glad you're having such success!

Are these 4 bugs or 6?  Or is it uncertain whether the two comment
links are separate bugs?

As an aside, I recently wrote a built-in minimizer.  I haven't really
documented it aside from adding it to the `--help` text.  I've found
it helpful for minimizing some things I've been looking at, but I'm
interested in any feedback you have.  You give it a path to a script
that uses a file called `reduction-candidate` in its current
directory, and returns 0 for successful reductions (IE the bug is
still there) and non-zero for failed reductions.  Basically the idea
is that you give it the seed (and other configuration) of the
interesting test case, then it re-generates it, then adds a
minimization step before printing.  I hope it will save you time while
you find more Dafny bugs. :)

Also, I'm curious to hear about your testing setup.  Are you using any
of our harness repository tools, or did you set up your own
infrastructure?  How have you been minimizing test cases so far?  How
much have you been running your fuzzer (ballpark approximation)?  Have
you spent much time doing things like adjusting weights?  How big is
your fuzzer (eg. LOC)?

On Fri, Aug 20, 2021 at 11:38:14AM -0700, Sorawee Porncharoenwase wrote:
>A lot more bugs:
>
>- https://github.com/dafny-lang/dafny/issues/1359 and
>https://github.com/dafny-lang/dafny/issues/1359#issuecomment-902594485
>- https://github.com/dafny-lang/dafny/issues/1360
>- https://github.com/dafny-lang/dafny/issues/1361 and
>https://github.com/dafny-lang/dafny/issues/1361#issuecomment-902842190
>- https://github.com/dafny-lang/dafny/issues/1362
>
>On Thu, Aug 19, 2021 at 6:35 PM Sorawee Porncharoenwase <
>sorawee.pwase at gmail.com> wrote:
>
>> One more bug :)
>>
>> https://github.com/dafny-lang/dafny/issues/1358
>>
>> On Thu, Aug 19, 2021 at 6:33 PM Eric Eide <eeide at cs.utah.edu> wrote:
>>
>>> Sorawee Porncharoenwase <sorawee.pwase at gmail.com> writes:
>>>
>>> > Two more bugs:
>>>
>>> Thank you for keeping us up to date!  We are very excited that you are
>>> having
>>> such success fuzzing Dafny!
>>>
>>> --
>>>
>>> -------------------------------------------------------------------------------
>>> Eric Eide <eeide at cs.utah.edu>   .        University of Utah School of
>>> Computing
>>> https://www.cs.utah.edu/~eeide/ . +1 801-585-5512 .   Salt Lake City,
>>> Utah, USA
>>>
>>