[Verifpal] assert assert

Nadim Kobeissi nadim at symbolic.software
Wed Sep 11 12:29:53 CEST 2019


(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