[Why3-club] Problem with the hypothesis_selection plugin

Piotr Trojanek piotr.trojanek at gmail.com
Tue Nov 12 13:15:20 CET 2013

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

More information about the Why3-club mailing list