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

[Sorawee Porncharoenwase]

Two more issues (though I filed them together in one bug report, to not
clutter GitHub issues)

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

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

> 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/20210828/3440dbb8/attachment.html>