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

[Sorawee Porncharoenwase]

One more bug:

https://github.com/dafny-lang/dafny/issues/1397

On Fri, Aug 27, 2021 at 2:36 AM Sorawee Porncharoenwase <
sorawee.pwase at gmail.com> wrote:

> 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/b48cbb57/attachment.html>