[Why3-club] strategy definitions in the config file

Julia Lawall julia.lawall at lip6.fr
Sat Mar 16 09:17:06 CET 2019

Often I do split_vc and the alt-ergo.  How would I define such a strategy
in the configuration file?

I tried:

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.


More information about the Why3-club mailing list