[Verifpal] precondition, 3.2.6

Mike tankf33der at disroot.org
Tue Dec 15 08:33:52 CET 2020


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)


More information about the Verifpal mailing list