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

Yannick Moy moy at adacore.com
Fri Nov 18 17:32:39 CET 2011


On 11/16/2011 06:07 PM, David MENTRE wrote:

> 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. ;-)

Thanks David for the suggestion, but it does not improve things in the case I'm
reporting.
-- 
Yannick



More information about the Why3-club mailing list