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

[Sorawee Porncharoenwase]

Two more bugs:
- https://github.com/dafny-lang/dafny/issues/1396
- https://github.com/dafny-lang/dafny/issues/1395

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 <
sorawee.pwase at gmail.com> wrote:

> Here's another bug: https://github.com/dafny-lang/dafny/issues/1387
>
> On Tue, Aug 24, 2021 at 2:40 PM Sorawee Porncharoenwase <
> sorawee.pwase at gmail.com> wrote:
>
>> One more bug:
>>
>> https://github.com/dafny-lang/dafny/issues/1384
>>
>> On Sun, Aug 22, 2021 at 5:34 PM Sorawee Porncharoenwase <
>> sorawee.pwase at gmail.com> wrote:
>>
>>> More bugs!
>>>
>>> - https://github.com/dafny-lang/dafny/issues/1372#issuecomment-903359423
>>> - https://github.com/dafny-lang/dafny/issues/1374
>>>
>>> On Sun, Aug 22, 2021 at 12:56 PM John Regehr <regehr at cs.utah.edu> 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 :)
>>>>
>>>> John
>>>>
>>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </listarchives/xsmith-dev/attachments/20210827/7027fe99/attachment.html>