[Why3-club] Problem with the hypothesis_selection plugin
piotr.trojanek at gmail.com
Tue Nov 12 13:22:33 CET 2013
I have forgot to attach the patch :(
PS With hypothesis_selection enabled my goals are indeed proved.
On Tue, Nov 12, 2013 at 12:15:20PM +0000, Piotr Trojanek wrote:
> Hi, fortunately I did not gave up. The "solution" is to add description
> when registering the transformation (see the attached patch).
> Now, my question is whether the lack of description when registering
> hypothesis_selection is intentional or is it a bug?
> Piotr Trojanek
> On Tue, Nov 12, 2013 at 10:58:01AM +0000, Piotr Trojanek wrote:
> > Dear Why3-club,
> > I believe that the "hypothesis_selection" should help in proving my
> > goals, but I am unable to apply this transformation.
> > I have checked that:
> > - the configure script outputs "Hypothesis selection : yes"
> > - the plugin file is compiled, installed and detected properly
> > - the plugin is executed, because I see a debug print message that
> > I have put just before the "Trans.register_transform" call
> > However, the "hypothesis_selection" is missing from the output of
> > 'why3 --list-transforms' and is not available in the why3ide.
> > Any advice?
> > --
> > Piotr Trojanek
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 505 bytes
Desc: not available
More information about the Why3-club