[Verifpal] assert assert

Nadim Kobeissi nadim at symbolic.software
Wed Sep 11 13:17:01 CEST 2019


Dear Mike,

The latest pushes to master (0c7a90df6c and 75ed71ba38) should address the issues you’ve found with `should_ok` and `should_fail` respectively.

Your testing and feedback is really valuable, thank you so much for continuing to contribute! :-)

Hope to hear from you soon,

Nadim Kobeissi
Symbolic Software • https://symbolic.software

> On Sep 11, 2019, at 12:29 PM, Nadim Kobeissi <nadim at symbolic.software> wrote:
> 
> (Mixed them up — I was referring to `should_ok` when I said `should_fail`, and vice-versa.)
> 
> Nadim Kobeissi
> Symbolic Software • https://symbolic.software
> 
>> On Sep 11, 2019, at 12:28 PM, Nadim Kobeissi <nadim at symbolic.software> wrote:
>> 
>> Dear Mike,
>> 
>> Thanks for this.
>> 
>> `should_fail` is an easy fix (a change in 0.6.x led to ASSERT being blocked by another call) and is fixed now in master.
>> 
>> `should_ok` is related to a deeper issue that I thought I had taken care of a few weeks ago. Working on it.
>> 
>> Nadim Kobeissi
>> Symbolic Software • https://symbolic.software
>> 
>>> On Sep 11, 2019, at 10:24 AM, Mike via Verifpal <verifpal at lists.symbolic.software> wrote:
>>> 
>>> hi all,
>>> 
>>> While testing verifpal I found ASSERT() doesn't understand something simple.
>>> Cut versions attached.
>>> 
>>> (mike)
>>> <should_fail.vp><should_ok.vp>
>>> _______________________________________________
>>> Verifpal mailing list
>>> Verifpal at lists.symbolic.software
>>> https://lists.symbolic.software/mailman/listinfo/verifpal
>> 
> 




More information about the Verifpal mailing list