[Verifpal] precondition, 3.2.6

Nadim Kobeissi nadim at symbolic.software
Fri Dec 18 06:52:11 CET 2020


Dear Mike,

Thank you, this has been fixed.

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

> On Dec 15, 2020, at 8:33 AM, Mike via Verifpal <verifpal at lists.symbolic.software> wrote:
> 
> hi all,
> 
> Model from Chapter 3.2.6 from manual runs with error because "Carol" dont use received m2.
> You should add this line for consistency if you want
> 
> _ = HASH(m2)
> 
> (mike)
> 
> _______________________________________________
> Verifpal mailing list
> Verifpal at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal



More information about the Verifpal mailing list