[Why3-club] Why3 simplifying too much

Johannes Kanig kanig at adacore.com
Mon Mar 3 10:04:14 CET 2014

On Mon, 03 Mar 2014 10:02:19 +0100, Johannes Kanig <kanig at adacore.com> wrote:
> I was confused - we would indeed want to make the distinction you describe:

And attached is a file which describes the issue: currently Why issues a VC on the call, although it doesn't have a precondition.



Johannes Kanig <kanig at adacore.com>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test_vdll.mlw
Type: application/octet-stream
Size: 447 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20140303/dffc9d5d/attachment.obj>

More information about the Why3-club mailing list