[Why3-club] strategy definitions in the config file

Claude Marche Claude.Marche at inria.fr
Mon Mar 18 13:35:24 CET 2019


Sorry for the late answer.

Please look at the manual http://why3.lri.fr/doc/technical.html#sec137 
for a description of the language of proof strategies.

As shown by Mario's answer, the "t" instruction requires both a 
transformation name and a label. You did not give any label. The 
newlines are not significant so in your case the "c" on the next line is 
taken as the label, and then the next token "Alt-Ergo,2.0" is not 
understood as a command, which can be only c, p, t or a label.

- Claude

Le 16/03/2019 à 09:17, Julia Lawall a écrit :
> Often I do split_vc and the alt-ergo.  How would I define such a strategy
> in the configuration file?
> 
> I tried:
> 
> [strategy]
> code = "start:
> t split_all_full
> c Alt-Ergo,2.0 40 10000
> 
> But it says "Fatal: loading strategy 'Auto_level_1' failed: syntax error
> on character 'A' at position 26"
> 
> I see examples with Eprover where the value in the name keyval pair is
> used to name the prover.  Alt-Ergo has Alt-Ergo in this line, but it
> doesn't work.
> 
> thanks,
> julia
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> 


More information about the Why3-club mailing list