Hi, On 3/23/20 4:39 PM, Julia Lawall wrote: > I see the option --apply-transform to apply a specific transform, but is > it possible to apply a strategy, as defined in the .why3.conf file? >
We also faced this limitation of Why3 in AstraVer project. We implemented separate tool called "sprove" in why3. It's similar to prove but supports sessions and strategies. You can find it here: https://forge.ispras.ru/projects/astraver/repository/why3/revisions/bv_and_lemma_functions_stable-4.07/entry/src/tools/why3sprove.ml Thanks, Denis _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
