fix session for gcd

examples/gcd/why3session.xml

@@ -6,15 +6,27 @@
 <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"/>
 <file name="../gcd.mlw" expanded="true">
-<theory name="EuclideanAlgorithm" sum="b19fdaf810947d1effcb1fb33e3d7e49">
+<theory name="EuclideanAlgorithm" sum="93083dc87e1612939f080d411978440f" expanded="true">
  <goal name="VC euclid" expl="VC for euclid">
- <proof prover="8"><result status="valid" time="8.35"/></proof>
+ <transf name="split_goal_wp">
+  <goal name="VC euclid.1" expl="1. check modulo by zero">
+  <proof prover="9"><result status="valid" time="0.01" steps="4"/></proof>
+  </goal>
+  <goal name="VC euclid.2" expl="2. variant decrease">
+  <proof prover="9"><result status="valid" time="0.02" steps="21"/></proof>
+  </goal>
+  <goal name="VC euclid.3" expl="3. precondition">
+  <proof prover="9"><result status="valid" time="0.00" steps="8"/></proof>
+  </goal>
+  <goal name="VC euclid.4" expl="4. postcondition">
+  <proof prover="9"><result status="valid" time="0.03" steps="47"/></proof>
+  </goal>
+ </transf>
  </goal>
 </theory>
-<theory name="EuclideanAlgorithmIterative" sum="4841a879f96158e78cf1e196ec0e2c3b">
+<theory name="EuclideanAlgorithmIterative" sum="4841a879f96158e78cf1e196ec0e2c3b" expanded="true">
  <goal name="VC euclid" expl="VC for euclid">
  <proof prover="4"><result status="valid" time="0.02"/></proof>
  </goal>
@@ -33,7 +45,7 @@
  <proof prover="9"><result status="valid" time="0.01" steps="29"/></proof>
  </goal>
  <goal name="gcd_even_odd">
- <proof prover="0" edited="gcd_BinaryGcd_gcd_even_odd_2.v"><result status="valid" time="0.28"/></proof>
+ <proof prover="0" edited="gcd_BinaryGcd_gcd_even_odd_2.v"><result status="valid" time="0.45"/></proof>
  </goal>
  <goal name="gcd_even_odd2">
  <proof prover="9"><result status="valid" time="0.05" steps="29"/></proof>
@@ -129,7 +141,7 @@
  </goal>
 </theory>
 <theory name="EuclideanAlgorithm63" sum="40b32678ce74c347e73fb0ee700b3141" expanded="true">
- <goal name="VC euclid" expl="VC for euclid" expanded="true">
+ <goal name="VC euclid" expl="VC for euclid">
  <proof prover="1"><result status="valid" time="0.24"/></proof>
  </goal>
 </theory>