[Why3-club] Problem with the hypothesis_selection plugin

Piotr Trojanek piotr.trojanek at gmail.com
Tue Nov 12 11:58:01 CET 2013

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