Hello Nicolas,

Le 19/09/2016 à 15:39, Niols a écrit :
> The compilation goes well, and the transformation is available in the
> IDE. But when I try to use it, nothing happens. I tried to use debug
> messages, and the transformation seems to be applied on the right task,
> but nothing changes in the IDE, except that, when I try to apply other
> transformations, they are only scheduled but never applied: the IDE
> seems to be blocked in an inconsistent state.

Not really blocked, but nothing happens because the transformation
fails. This can be seen by looking at the standard error, where you
should see :

Failure in transformation eliminate_exists
The task already ends with a goal

Instead of using the IDE, is is better for debugging transformations to
use the "why3 prove" command, e.g.

why3 prove -a eliminate_exists -D why3 <your test file>

-a applies the given transformation, and -D why3 instructs to print the
result in why3 syntax (why3.drv is just a driver like drivers for provers)

The reason for your error is here

>       | _ ->
>          [create_prop_decl Pgoal pr t]

you should put back a "Paxiom" in the task instead.

- Claude

Claude Marché                          | tel: +33 1 69 15 66 08
INRIA Saclay - Île-de-France           |
Université Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |
Why3-club mailing list

Reply via email to