port example gcd. previous code was WRONG !!!

d1212070 · MARCHE Claude · 7e5c6a29 · d1212070 · d1212070 · d1212070
Commit d1212070 authored Jun 09, 2017 by MARCHE Claude
--- a/bench/bench
+++ b/bench/bench
@@ -251,8 +251,7 @@ echo ""

 echo "=== Checking extraction to OCaml ==="
 extract_and_run examples/euler001 euler001.ml 1000000
-# needs to port
-# extract_and_run examples/gcd gcd.ml 6 15
+extract_and_run examples/gcd gcd.ml 6 15
 extract_and_run examples/vstte10_max_sum vstte10_max_sum.ml
 # needs to port
 # extract_and_run examples/vstte12_combinators vstte12_combinators.ml "((((K K) K) K) K)"

--- a/examples/to_port/gcd.mlw
+++ b/examples/to_port/gcd.mlw
@@ -81,10 +81,10 @@ module BinaryGcd
    if v > u then binary_gcd v u else
    if v = 0 then u else
    if mod u 2 = 0 then
-      if mod u 2 = 0 then 2 * binary_gcd (u / 2) (v / 2)
+      if mod v 2 = 0 then 2 * binary_gcd (u / 2) (v / 2)
                     else binary_gcd (u / 2) v
      else
-      if mod u 2 = 0 then binary_gcd u (v / 2)
+      if mod v 2 = 0 then binary_gcd u (v / 2)
                     else binary_gcd ((u - v) / 2) v

 end

--- a/examples/to_port/gcd/Makefile
+++ b/examples/to_port/gcd/Makefile
--- a/examples/to_port/gcd/gcd_BinaryGcd_gcd_even_odd_2.v
+++ b/examples/to_port/gcd/gcd_BinaryGcd_gcd_even_odd_2.v
--- a/examples/to_port/gcd/gcd_WP_EuclideanAlgorithm_WP_parameter_gcd_1.v
+++ b/examples/to_port/gcd/gcd_WP_EuclideanAlgorithm_WP_parameter_gcd_1.v
--- a/examples/to_port/gcd/index.html
+++ b/examples/to_port/gcd/index.html
--- a/examples/to_port/gcd/jsmain.ml
+++ b/examples/to_port/gcd/jsmain.ml
--- a/examples/to_port/gcd/main.ml
+++ b/examples/to_port/gcd/main.ml
--- a/examples/to_port/gcd/why3session.xml
+++ b/examples/to_port/gcd/why3session.xml
@@ -3,6 +3,8 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
 <prover id="0" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="1" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="2" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="4" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="8" name="Spass" version="3.7" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="9" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
@@ -17,7 +19,7 @@
 <proof prover="4"><result status="valid" time="0.02"/></proof>
 </goal>
 </theory>
-<theory name="BinaryGcd" sum="bd104d3dd00bc2d7a3faa1d20c49e676" expanded="true">
+<theory name="BinaryGcd" sum="993b8cec44b47d264ddb4f75ecd183d3" expanded="true">
 <goal name="even1">
 <proof prover="9"><result status="valid" time="0.01" steps="19"/></proof>
 </goal>
@@ -45,8 +47,8 @@
 <goal name="gcd_odd_odd2">
 <proof prover="9"><result status="valid" time="0.07" steps="30"/></proof>
 </goal>
- <goal name="VC binary_gcd" expl="VC for binary_gcd" expanded="true">
- <transf name="split_goal_wp" expanded="true">
+ <goal name="VC binary_gcd" expl="VC for binary_gcd">
+ <transf name="split_goal_wp">
  <goal name="VC binary_gcd.1" expl="1. variant decrease">
  <proof prover="9"><result status="valid" time="0.01" steps="11"/></proof>
  </goal>
@@ -60,54 +62,75 @@
  <proof prover="9"><result status="valid" time="0.01" steps="9"/></proof>
  </goal>
  <goal name="VC binary_gcd.5" expl="5. check division by zero">
-  <proof prover="9"><result status="valid" time="0.00" steps="9"/></proof>
+  <proof prover="9"><result status="valid" time="0.01" steps="10"/></proof>
  </goal>
  <goal name="VC binary_gcd.6" expl="6. check division by zero">
-  <proof prover="9"><result status="valid" time="0.01" steps="9"/></proof>
+  <proof prover="9"><result status="valid" time="0.01" steps="10"/></proof>
  </goal>
  <goal name="VC binary_gcd.7" expl="7. variant decrease">
-  <proof prover="9"><result status="valid" time="0.02" steps="33"/></proof>
+  <proof prover="9"><result status="valid" time="0.02" steps="24"/></proof>
  </goal>
  <goal name="VC binary_gcd.8" expl="8. precondition">
-  <proof prover="9"><result status="valid" time="0.01" steps="17"/></proof>
+  <proof prover="9"><result status="valid" time="0.01" steps="18"/></proof>
  </goal>
  <goal name="VC binary_gcd.9" expl="9. check division by zero">
-  <proof prover="9"><result status="valid" time="0.01" steps="9"/></proof>
+  <proof prover="9"><result status="valid" time="0.01" steps="10"/></proof>
  </goal>
  <goal name="VC binary_gcd.10" expl="10. variant decrease">
-  <proof prover="9"><result status="valid" time="0.01" steps="9"/></proof>
+  <proof prover="9"><result status="valid" time="0.01" steps="20"/></proof>
  </goal>
  <goal name="VC binary_gcd.11" expl="11. precondition">
-  <proof prover="9"><result status="valid" time="0.01" steps="9"/></proof>
+  <proof prover="9"><result status="valid" time="0.01" steps="13"/></proof>
  </goal>
  <goal name="VC binary_gcd.12" expl="12. precondition">
  <proof prover="9"><result status="valid" time="0.00" steps="9"/></proof>
  </goal>
  <goal name="VC binary_gcd.13" expl="13. check division by zero">
-  <proof prover="9"><result status="valid" time="0.01" steps="9"/></proof>
+  <proof prover="9"><result status="valid" time="0.00" steps="10"/></proof>
  </goal>
  <goal name="VC binary_gcd.14" expl="14. variant decrease">
-  <proof prover="9"><result status="valid" time="0.01" steps="9"/></proof>
+  <proof prover="9"><result status="valid" time="0.01" steps="19"/></proof>
  </goal>
  <goal name="VC binary_gcd.15" expl="15. precondition">
-  <proof prover="9"><result status="valid" time="0.01" steps="9"/></proof>
+  <proof prover="9"><result status="valid" time="0.01" steps="13"/></proof>
  </goal>
  <goal name="VC binary_gcd.16" expl="16. check division by zero">
-  <proof prover="9"><result status="valid" time="0.01" steps="9"/></proof>
+  <proof prover="9"><result status="valid" time="0.01" steps="10"/></proof>
  </goal>
  <goal name="VC binary_gcd.17" expl="17. variant decrease">
-  <proof prover="9"><result status="valid" time="0.02" steps="23"/></proof>
+  <proof prover="9"><result status="valid" time="0.02" steps="24"/></proof>
  </goal>
  <goal name="VC binary_gcd.18" expl="18. precondition">
-  <proof prover="9"><result status="valid" time="0.01" steps="12"/></proof>
-  </goal>
-  <goal name="VC binary_gcd.19" expl="19. postcondition" expanded="true">
+  <proof prover="9"><result status="valid" time="0.01" steps="13"/></proof>
+  </goal>
+  <goal name="VC binary_gcd.19" expl="19. postcondition">
+  <transf name="split_goal_wp">
+   <goal name="VC binary_gcd.19.1" expl="1. postcondition">
+   <proof prover="9"><result status="valid" time="0.01" steps="8"/></proof>
+   </goal>
+   <goal name="VC binary_gcd.19.2" expl="2. postcondition">
+   <proof prover="9"><result status="valid" time="0.01" steps="16"/></proof>
+   </goal>
+   <goal name="VC binary_gcd.19.3" expl="3. postcondition">
+   <proof prover="9"><result status="valid" time="0.12" steps="89"/></proof>
+   </goal>
+   <goal name="VC binary_gcd.19.4" expl="4. postcondition">
+   <proof prover="2"><result status="valid" time="0.03"/></proof>
+   </goal>
+   <goal name="VC binary_gcd.19.5" expl="5. postcondition">
+   <proof prover="2"><result status="valid" time="0.02"/></proof>
+   </goal>
+   <goal name="VC binary_gcd.19.6" expl="6. postcondition">
+   <proof prover="2"><result status="valid" time="0.03"/></proof>
+   </goal>
+  </transf>
  </goal>
 </transf>
 </goal>
 </theory>
 <theory name="EuclideanAlgorithm63" sum="40b32678ce74c347e73fb0ee700b3141" expanded="true">
 <goal name="VC euclid" expl="VC for euclid" expanded="true">
+ <proof prover="1"><result status="valid" time="0.24"/></proof>
 </goal>
 </theory>
 </file>

--- a/examples/gcd/why3shapes.gz
+++ b/examples/gcd/why3shapes.gz
--- a/examples/gcd_vc_sp/gcd_BinaryGcd_gcd_even_odd_1.v
+++ b/examples/gcd_vc_sp/gcd_BinaryGcd_gcd_even_odd_1.v
+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import BuiltIn.
+Require BuiltIn.
+Require int.Int.
+Require int.Abs.
+Require int.EuclideanDivision.
+Require int.ComputerDivision.
+Require number.Parity.
+Require number.Divisibility.
+Require number.Gcd.
+Require number.Prime.
+Require number.Coprime.
+
+(* Why3 assumption *)
+Definition lt_nat (x:Z) (y:Z): Prop := (0%Z <= y)%Z /\ (x < y)%Z.
+
+(* Why3 assumption *)
+Inductive lex: (Z* Z)%type -> (Z* Z)%type -> Prop :=
+  | Lex_1 : forall (x1:Z) (x2:Z) (y1:Z) (y2:Z), (lt_nat x1 x2) -> (lex (x1,
+      y1) (x2, y2))
+  | Lex_2 : forall (x:Z) (y1:Z) (y2:Z), (lt_nat y1 y2) -> (lex (x, y1) (x,
+      y2)).
+
+Axiom even1 : forall (n:Z), (0%Z <= n)%Z -> ((number.Parity.even n) <->
+  (n = (2%Z * (ZArith.BinInt.Z.quot n 2%Z))%Z)).
+
+Axiom odd1 : forall (n:Z), (0%Z <= n)%Z -> ((~ (number.Parity.even n)) <->
+  (n = ((2%Z * (ZArith.BinInt.Z.quot n 2%Z))%Z + 1%Z)%Z)).
+
+Axiom div_nonneg : forall (n:Z), (0%Z <= n)%Z ->
+  (0%Z <= (ZArith.BinInt.Z.quot n 2%Z))%Z.
+
+Axiom gcd_even_even : forall (u:Z) (v:Z), (0%Z <= v)%Z -> ((0%Z <= u)%Z ->
+  ((number.Gcd.gcd (2%Z * u)%Z (2%Z * v)%Z) = (2%Z * (number.Gcd.gcd u
+  v))%Z)).
+
+(* Why3 goal *)
+Theorem gcd_even_odd : forall (u:Z) (v:Z), (0%Z <= v)%Z -> ((0%Z <= u)%Z ->
+  ((number.Gcd.gcd (2%Z * u)%Z ((2%Z * v)%Z + 1%Z)%Z) = (number.Gcd.gcd u
+  ((2%Z * v)%Z + 1%Z)%Z))).
+intros u v h1 h2.
+rewrite Gcd.Comm.
+rewrite number.Coprime.gcd_coprime.
+now rewrite Gcd.Comm.
+unfold Coprime.coprime.
+rewrite <- Gcd.Gcd_computer_mod; auto with zarith.
+rewrite ComputerDivision.Mod_mult; auto with zarith.
+Qed.
+
--- a/examples/to_port/gcd_vc_sp/why3session.xml
+++ b/examples/to_port/gcd_vc_sp/why3session.xml
@@ -2,177 +2,168 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
-<prover id="1" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
-<prover id="2" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
+<prover id="1" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="3" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="4" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="6" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../gcd.mlw" expanded="true">
-<theory name="EuclideanAlgorithm" sum="644b8d8ecd1a9e6f8fe429dc2c6ceeda">
+<theory name="EuclideanAlgorithm" sum="93083dc87e1612939f080d411978440f">
 <goal name="VC euclid" expl="VC for euclid">
 <transf name="split_goal_wp">
-  <goal name="VC euclid.1" expl="1. division by zero">
-  <proof prover="0"><result status="valid" time="0.02" steps="3"/></proof>
+  <goal name="VC euclid.1" expl="1. check modulo by zero">
+  <proof prover="3"><result status="valid" time="0.01" steps="4"/></proof>
  </goal>
  <goal name="VC euclid.2" expl="2. variant decrease">
-  <proof prover="0"><result status="valid" time="0.05" steps="47"/></proof>
+  <proof prover="3"><result status="valid" time="0.02" steps="21"/></proof>
  </goal>
  <goal name="VC euclid.3" expl="3. precondition">
-  <proof prover="0"><result status="valid" time="0.02" steps="7"/></proof>
+  <proof prover="3"><result status="valid" time="0.00" steps="8"/></proof>
  </goal>
  <goal name="VC euclid.4" expl="4. postcondition">
-  <proof prover="0"><result status="valid" time="1.15" steps="192"/></proof>
+  <proof prover="3"><result status="valid" time="0.03" steps="47"/></proof>
  </goal>
 </transf>
 </goal>
 </theory>
-<theory name="EuclideanAlgorithmIterative" sum="0b539327de02ae3286b21bfab58f2abf">
+<theory name="EuclideanAlgorithmIterative" sum="d113c1d8f52120eee1470fface43fc4b">
 <goal name="VC euclid" expl="VC for euclid">
 <transf name="split_goal_wp">
  <goal name="VC euclid.1" expl="1. loop invariant init">
-  <proof prover="0"><result status="valid" time="0.01" steps="2"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="3"/></proof>
  </goal>
  <goal name="VC euclid.2" expl="2. loop invariant init">
-  <proof prover="0"><result status="valid" time="0.02" steps="0"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="1"/></proof>
  </goal>
-  <goal name="VC euclid.3" expl="3. division by zero">
-  <proof prover="0"><result status="valid" time="0.02" steps="6"/></proof>
+  <goal name="VC euclid.3" expl="3. check modulo by zero">
+  <proof prover="3"><result status="valid" time="0.00" steps="7"/></proof>
  </goal>
-  <goal name="VC euclid.4" expl="4. loop invariant preservation">
-  <proof prover="0"><result status="valid" time="0.03" steps="20"/></proof>
+  <goal name="VC euclid.4" expl="4. loop variant decrease">
+  <proof prover="3"><result status="valid" time="0.25" steps="65"/></proof>
  </goal>
  <goal name="VC euclid.5" expl="5. loop invariant preservation">
-  <proof prover="0"><result status="valid" time="0.02" steps="13"/></proof>
+  <proof prover="3"><result status="valid" time="0.02" steps="21"/></proof>
  </goal>
-  <goal name="VC euclid.6" expl="6. loop variant decrease">
-  <proof prover="1"><result status="valid" time="0.03"/></proof>
+  <goal name="VC euclid.6" expl="6. loop invariant preservation">
+  <proof prover="3"><result status="valid" time="2.53" steps="230"/></proof>
  </goal>
  <goal name="VC euclid.7" expl="7. postcondition">
-  <proof prover="0"><result status="valid" time="0.03" steps="16"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="16"/></proof>
  </goal>
 </transf>
 </goal>
 </theory>
-<theory name="BinaryGcd" sum="95664ddbe38ef16f39ae9ef12ab1c735">
+<theory name="BinaryGcd" sum="993b8cec44b47d264ddb4f75ecd183d3" expanded="true">
 <goal name="even1">
- <proof prover="0"><result status="valid" time="0.03" steps="16"/></proof>
+ <proof prover="3"><result status="valid" time="0.02" steps="19"/></proof>
 </goal>
 <goal name="odd1">
- <proof prover="0"><result status="valid" time="0.03" steps="14"/></proof>
+ <proof prover="3"><result status="valid" time="0.02" steps="21"/></proof>
 </goal>
 <goal name="div_nonneg">
- <proof prover="0"><result status="valid" time="0.03" steps="4"/></proof>
+ <proof prover="3"><result status="valid" time="0.01" steps="5"/></proof>
 </goal>
 <goal name="gcd_even_even">
- <proof prover="0"><result status="valid" time="0.04" steps="28"/></proof>
+ <proof prover="3"><result status="valid" time="0.01" steps="29"/></proof>
 </goal>
 <goal name="gcd_even_odd">
- <proof prover="2"><result status="valid" time="0.03"/></proof>
+ <proof prover="6" edited="gcd_BinaryGcd_gcd_even_odd_1.v"><result status="valid" time="0.46"/></proof>
 </goal>
 <goal name="gcd_even_odd2">
- <proof prover="0"><result status="valid" time="0.07" steps="24"/></proof>
+ <proof prover="3"><result status="valid" time="0.06" steps="29"/></proof>
 </goal>
 <goal name="odd_odd_div2">
- <proof prover="0"><result status="valid" time="0.21" steps="178"/></proof>
+ <proof prover="3"><result status="valid" time="0.74" steps="389"/></proof>
 </goal>
 <goal name="VC gcd_odd_odd" expl="VC for gcd_odd_odd">
- <proof prover="0"><result status="valid" time="0.06" steps="32"/></proof>
+ <proof prover="3"><result status="valid" time="0.02" steps="32"/></proof>
 </goal>
 <goal name="gcd_odd_odd2">
- <proof prover="0"><result status="valid" time="0.53" steps="30"/></proof>
+ <proof prover="3"><result status="valid" time="0.08" steps="30"/></proof>
 </goal>
 <goal name="VC binary_gcd" expl="VC for binary_gcd">
 <transf name="split_goal_wp">
  <goal name="VC binary_gcd.1" expl="1. variant decrease">
-  <proof prover="2"><result status="valid" time="0.01"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="11"/></proof>
  </goal>
  <goal name="VC binary_gcd.2" expl="2. precondition">
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="7"/></proof>
  </goal>
  <goal name="VC binary_gcd.3" expl="3. precondition">
-  <proof prover="0"><result status="valid" time="0.02" steps="7"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="8"/></proof>
  </goal>
  <goal name="VC binary_gcd.4" expl="4. precondition">
-  <proof prover="0"><result status="valid" time="0.02" steps="8"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="9"/></proof>
  </goal>
-  <goal name="VC binary_gcd.5" expl="5. division by zero">
-  <proof prover="2"><result status="valid" time="0.00"/></proof>
+  <goal name="VC binary_gcd.5" expl="5. check division by zero">
+  <proof prover="3"><result status="valid" time="0.01" steps="10"/></proof>
  </goal>
-  <goal name="VC binary_gcd.6" expl="6. division by zero">
-  <proof prover="2"><result status="valid" time="0.00"/></proof>
+  <goal name="VC binary_gcd.6" expl="6. check division by zero">
+  <proof prover="3"><result status="valid" time="0.01" steps="10"/></proof>
  </goal>
  <goal name="VC binary_gcd.7" expl="7. variant decrease">
-  <proof prover="2"><result status="valid" time="0.01"/></proof>
+  <proof prover="3"><result status="valid" time="0.02" steps="24"/></proof>
  </goal>
  <goal name="VC binary_gcd.8" expl="8. precondition">
-  <proof prover="0"><result status="valid" time="0.02" steps="16"/></proof>
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <proof prover="3"><result status="valid" time="0.02" steps="18"/></proof>
  </goal>
-  <goal name="VC binary_gcd.9" expl="9. division by zero">
-  <proof prover="0"><result status="valid" time="0.02" steps="8"/></proof>
-  <proof prover="2"><result status="valid" time="0.00"/></proof>
+  <goal name="VC binary_gcd.9" expl="9. check division by zero">
+  <proof prover="3"><result status="valid" time="0.01" steps="10"/></proof>
  </goal>
  <goal name="VC binary_gcd.10" expl="10. variant decrease">
-  <proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
-  <proof prover="2"><result status="valid" time="0.00"/></proof>
+  <proof prover="3"><result status="valid" time="0.02" steps="20"/></proof>
  </goal>
  <goal name="VC binary_gcd.11" expl="11. precondition">
-  <proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
-  <proof prover="2"><result status="valid" time="0.00"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="13"/></proof>
  </goal>
  <goal name="VC binary_gcd.12" expl="12. precondition">
-  <proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="9"/></proof>
  </goal>
-  <goal name="VC binary_gcd.13" expl="13. division by zero">
-  <proof prover="0"><result status="valid" time="0.03" steps="8"/></proof>
-  <proof prover="2"><result status="valid" time="0.01"/></proof>
+  <goal name="VC binary_gcd.13" expl="13. check division by zero">
+  <proof prover="3"><result status="valid" time="0.01" steps="10"/></proof>
  </goal>
  <goal name="VC binary_gcd.14" expl="14. variant decrease">
-  <proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
-  <proof prover="2"><result status="valid" time="0.00"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="19"/></proof>
  </goal>
  <goal name="VC binary_gcd.15" expl="15. precondition">
-  <proof prover="0"><result status="valid" time="0.02" steps="8"/></proof>
-  <proof prover="2"><result status="valid" time="0.01"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="13"/></proof>
  </goal>
-  <goal name="VC binary_gcd.16" expl="16. division by zero">
-  <proof prover="0"><result status="valid" time="0.02" steps="8"/></proof>
-  <proof prover="2"><result status="valid" time="0.00"/></proof>
+  <goal name="VC binary_gcd.16" expl="16. check division by zero">
+  <proof prover="3"><result status="valid" time="0.01" steps="10"/></proof>
  </goal>
  <goal name="VC binary_gcd.17" expl="17. variant decrease">
-  <proof prover="0"><result status="valid" time="0.04" steps="24"/></proof>
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <proof prover="3"><result status="valid" time="0.02" steps="24"/></proof>
  </goal>
  <goal name="VC binary_gcd.18" expl="18. precondition">
-  <proof prover="0"><result status="valid" time="0.02" steps="11"/></proof>
-  <proof prover="2"><result status="valid" time="0.01"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="13"/></proof>
  </goal>
  <goal name="VC binary_gcd.19" expl="19. postcondition">
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <transf name="split_goal_wp">
+   <goal name="VC binary_gcd.19.1" expl="1. postcondition">
+   <proof prover="4"><result status="valid" time="0.02"/></proof>
+   </goal>
+   <goal name="VC binary_gcd.19.2" expl="2. postcondition">
+   <proof prover="4"><result status="valid" time="0.02"/></proof>
+   </goal>
+   <goal name="VC binary_gcd.19.3" expl="3. postcondition">
+   <proof prover="3" timelimit="1"><result status="valid" time="0.11" steps="89"/></proof>
+   </goal>
+   <goal name="VC binary_gcd.19.4" expl="4. postcondition">
+   <proof prover="4"><result status="valid" time="0.02"/></proof>
+   </goal>
+   <goal name="VC binary_gcd.19.5" expl="5. postcondition">
+   <proof prover="4"><result status="valid" time="0.02"/></proof>
+   </goal>
+   <goal name="VC binary_gcd.19.6" expl="6. postcondition">
+   <proof prover="4"><result status="valid" time="0.02"/></proof>
+   </goal>
+  </transf>
  </goal>
 </transf>
 </goal>
 </theory>
-<theory name="EuclideanAlgorithm31" sum="96988f323e3bdbdcd87c5915f5871171">
- <goal name="VC euclid" expl="VC for euclid">
- <transf name="split_goal_wp">
-  <goal name="VC euclid.1" expl="1. integer overflow">
-  <proof prover="0"><result status="valid" time="0.02" steps="3"/></proof>
-  </goal>
-  <goal name="VC euclid.2" expl="2. division by zero">
-  <proof prover="0"><result status="valid" time="0.02" steps="5"/></proof>
-  </goal>
-  <goal name="VC euclid.3" expl="3. integer overflow">
-  <proof prover="0"><result status="valid" time="0.09" steps="52"/></proof>
-  </goal>
-  <goal name="VC euclid.4" expl="4. variant decrease">
-  <proof prover="0"><result status="valid" time="0.95" steps="177"/></proof>
-  </goal>
-  <goal name="VC euclid.5" expl="5. precondition">
-  <proof prover="0"><result status="valid" time="0.02" steps="15"/></proof>
-  </goal>
-  <goal name="VC euclid.6" expl="6. postcondition">
-  <proof prover="0"><result status="valid" time="0.25" steps="90"/></proof>
-  </goal>
- </transf>
+<theory name="EuclideanAlgorithm63" sum="40b32678ce74c347e73fb0ee700b3141" expanded="true">
+ <goal name="VC euclid" expl="VC for euclid" expanded="true">
+ <proof prover="1"><result status="valid" time="0.23"/></proof>
 </goal>
 </theory>
 </file>

--- a/examples/gcd_vc_sp/why3shapes.gz
+++ b/examples/gcd_vc_sp/why3shapes.gz
--- a/examples/to_port/gcd/why3shapes.gz
+++ b/examples/to_port/gcd/why3shapes.gz
--- a/examples/to_port/gcd_vc_sp/why3shapes.gz
+++ b/examples/to_port/gcd_vc_sp/why3shapes.gz
--- a/examples/vstte12_tree_reconstruction/why3session.xml
+++ b/examples/vstte12_tree_reconstruction/why3session.xml
@@ -7,7 +7,11 @@
 <prover id="5" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="6" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../vstte12_tree_reconstruction.mlw" expanded="true">
-<theory name="Tree" sum="29ec6bca61c2eb01c53689a1c783adf7">
+<theory name="Tree" sum="d4afd8fd1322d8d78d7de8637f4e5856">
+ <goal name="VC depths" expl="VC for depths">
+ <transf name="split_goal_wp">
+ </transf>
+ </goal>
 <goal name="depths_head">
 <transf name="induction_ty_lex">
  <goal name="depths_head.1" expl="1.">
@@ -88,20 +92,19 @@
 <proof prover="2"><result status="valid" time="0.05" steps="249"/></proof>
 </goal>
 </theory>
-<theory name="ZipperBased" sum="52a1d639be2b96a70893bf3e1937c0fd" expanded="true">
- <goal name="forest_depths_append" expanded="true">
+<theory name="ZipperBased" sum="52a1d639be2b96a70893bf3e1937c0fd">
+ <goal name="forest_depths_append">
 <proof prover="5" timelimit="10" memlimit="0" edited="vstte12_tree_reconstruction_WP_ZipperBased_forest_depths_append_1.v"><result status="valid" time="0.48"/></proof>
 </goal>
- <goal name="g_append" expanded="true">
+ <goal name="g_append">
 <proof prover="5" timelimit="20" memlimit="0" edited="vstte12_tree_reconstruction_WP_ZipperBased_g_append_1.v"><result status="valid" time="0.97"/></proof>
 </goal>
- <goal name="right_nil" expanded="true">
+ <goal name="right_nil">
 <proof prover="5" timelimit="29" memlimit="0" edited="vstte12_tree_reconstruction_WP_ZipperBased_right_nil_1.v"><result status="valid" time="2.67"/></proof>
 </goal>
- <goal name="main_lemma" expanded="true">
+ <goal name="main_lemma">
 <proof prover="2"><result status="valid" time="0.02" steps="107"/></proof>
- <metas
-  expanded="true">
+ <metas>
  <ts_pos name="real" arity="0" id="real" ip_theory="BuiltIn">
   <ip_library name="why3"/>
   <ip_library name="BuiltIn"/>
@@ -549,9 +552,9 @@
  <meta name="remove_type">
   <meta_arg_ts id="unit"/>
  </meta>
-  <goal name="main_lemma" expanded="true">
-  <transf name="eliminate_builtin" expanded="true">
-   <goal name="main_lemma.1" expl="1." expanded="true">
+  <goal name="main_lemma">
+  <transf name="eliminate_builtin">
+   <goal name="main_lemma.1" expl="1.">
   <proof prover="2"><result status="valid" time="0.02" steps="37"/></proof>
   <proof prover="3"><result status="valid" time="0.02"/></proof>
   </goal>
@@ -559,8 +562,8 @@
  </goal>
 </metas>
 </goal>
- <goal name="VC tc" expl="VC for tc" expanded="true">
- <transf name="split_goal_wp" expanded="true">
+ <goal name="VC tc" expl="VC for tc">
+ <transf name="split_goal_wp">
  <goal name="VC tc.1" expl="1. exceptional postcondition">
  <proof prover="3"><result status="valid" time="0.07"/></proof>
  </goal>

--- a/examples/vstte12_tree_reconstruction/why3shapes.gz
+++ b/examples/vstte12_tree_reconstruction/why3shapes.gz