[Why3-club] special "ignoring" construct for VC creation

David MENTRE dmentre at linux-france.org
Wed Nov 16 18:07:41 CET 2011


Hello Yannick,

2011/11/16 Yannick Moy <moy at adacore.com>:
> Thinking more about that, this is only a half-baked solution, as we will still
> get all the useless hypotheses in the context of VCs for run-time errors. So
> having something at the VC creation (splitting) level would be much better.

Have you tried an "inline" transformation on the VCs that do not work
with Alt-Ergo? In some of my cases, it helps the proof by removing
unneeded context. YMMV. ;-)

Best regards,
david



More information about the Why3-club mailing list