diff --git a/examples/add_list/why3session.xml b/examples/add_list/why3session.xml
index fe83c110de8a8995bb44e509c392b7fef935f942..b42fc4a604ce56eabb1130849d60294d75ef79a3 100644
--- a/examples/add_list/why3session.xml
+++ b/examples/add_list/why3session.xml
@@ -1,10 +1,12 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../add_list.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="add_list.mlw"/>
 <theory name="AddListRec" proved="true">
  <goal name="VC sum" expl="VC for sum" proved="true">
  <proof prover="2"><result status="valid" time="0.02" steps="92"/></proof>
diff --git a/examples/add_list/why3shapes.gz b/examples/add_list/why3shapes.gz
index bc38d22906745ebbaf25dd4d649382e60e66ef61..f3fb3aebe4edd8b7383fced6a01d684e96f46dda 100644
Binary files a/examples/add_list/why3shapes.gz and b/examples/add_list/why3shapes.gz differ
diff --git a/examples/add_list_vc_sp/why3session.xml b/examples/add_list_vc_sp/why3session.xml
index be42d7c4a61a45a6ab250a5a29724d21780848cf..2d7c113e4127c31493b48371359f8e66866264b4 100644
--- a/examples/add_list_vc_sp/why3session.xml
+++ b/examples/add_list_vc_sp/why3session.xml
@@ -1,9 +1,11 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
-<file name="../add_list_vc_sp.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="add_list_vc_sp.mlw"/>
 <theory name="AddListRec" proved="true">
  <goal name="VC sum" expl="VC for sum" proved="true">
  <proof prover="0"><result status="valid" time="0.04"/></proof>
diff --git a/examples/add_list_vc_sp/why3shapes.gz b/examples/add_list_vc_sp/why3shapes.gz
index 2e28c772966537dd0d526aba2a7e2e4d488f16ec..439adc4317b37a8dc7d1ef2e03c1d9b11026a3ec 100644
Binary files a/examples/add_list_vc_sp/why3shapes.gz and b/examples/add_list_vc_sp/why3shapes.gz differ
diff --git a/examples/binary_multiplication/why3session.xml b/examples/binary_multiplication/why3session.xml
index 99fdfff5b6bef14e42820e3b007c357199ce47d3..00513779f384db5092ac5996360179cb94d9188a 100644
--- a/examples/binary_multiplication/why3session.xml
+++ b/examples/binary_multiplication/why3session.xml
@@ -1,10 +1,12 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
 <prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
-<file name="../binary_multiplication.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="binary_multiplication.mlw"/>
 <theory name="BinaryMultiplication" proved="true">
  <goal name="VC binary_mult" expl="VC for binary_mult" proved="true">
  <proof prover="0"><result status="valid" time="0.05" steps="63"/></proof>
diff --git a/examples/binary_multiplication/why3shapes.gz b/examples/binary_multiplication/why3shapes.gz
index f222949d9816b315d8426c01ebf6cf432f119327..46a4b5df70b889e3f69fd5b4bceb496d016784c0 100644
Binary files a/examples/binary_multiplication/why3shapes.gz and b/examples/binary_multiplication/why3shapes.gz differ
diff --git a/examples/binary_search/why3session.xml b/examples/binary_search/why3session.xml
index b9728c1bbac33b4881396aa73b3c1d9fad32ba49..70071e46cd6c5b876d613d16498690664341196f 100644
--- a/examples/binary_search/why3session.xml
+++ b/examples/binary_search/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
 <file proved="true">
 <path name=".."/>
diff --git a/examples/binary_search/why3shapes.gz b/examples/binary_search/why3shapes.gz
index 416cbb71a2b43042c528d918141168bac0a046e6..ad2d0d805c9097d6e3eb11c54f24092ec31cec14 100644
Binary files a/examples/binary_search/why3shapes.gz and b/examples/binary_search/why3shapes.gz differ
diff --git a/examples/binary_search_vc_sp/why3session.xml b/examples/binary_search_vc_sp/why3session.xml
index 2b058a5353ea696d55f3c8e557e9b0023e36c5b0..a50078d49da3a27ac15a1647999af2806a47ea91 100644
--- a/examples/binary_search_vc_sp/why3session.xml
+++ b/examples/binary_search_vc_sp/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
 <file proved="true">
 <path name=".."/>
diff --git a/examples/binary_search_vc_sp/why3shapes.gz b/examples/binary_search_vc_sp/why3shapes.gz
index f1fbcca8ffc4181b4843eeb293335c4222161664..238a1ba253652f7137d490a30a5a240250334b50 100644
Binary files a/examples/binary_search_vc_sp/why3shapes.gz and b/examples/binary_search_vc_sp/why3shapes.gz differ
diff --git a/examples/binary_sqrt/why3session.xml b/examples/binary_sqrt/why3session.xml
index 09ddc49d635248f18a15da8228a85c70e78b762f..a7864d066169c3793ed405dd550eef37cd2059c7 100644
--- a/examples/binary_sqrt/why3session.xml
+++ b/examples/binary_sqrt/why3session.xml
@@ -1,10 +1,12 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="2" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="3" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
-<file name="../binary_sqrt.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="binary_sqrt.mlw"/>
 <theory name="BinarySqrt" proved="true">
  <goal name="VC sqrt" expl="VC for sqrt" proved="true">
  <transf name="split_goal_right" proved="true" >
diff --git a/examples/binary_sqrt/why3shapes.gz b/examples/binary_sqrt/why3shapes.gz
index 946eb3593e06d107866e9b6e4d6e538c48f835f4..600ca3855b5a79355650a22ae3a5986ae0c6a99d 100644
Binary files a/examples/binary_sqrt/why3shapes.gz and b/examples/binary_sqrt/why3shapes.gz differ
diff --git a/examples/bitcount/why3session.xml b/examples/bitcount/why3session.xml
index 5e1182863947b3e9b578c1980786f32ba79b8db0..44a5adb0fec6b760cf84d40f09b79537424a1463 100644
--- a/examples/bitcount/why3session.xml
+++ b/examples/bitcount/why3session.xml
@@ -1,14 +1,16 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="4000"/>
 <prover id="1" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Z3" version="4.4.1" alternative="noBV" timelimit="5" steplimit="0" memlimit="4000"/>
 <prover id="4" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="0" memlimit="4000"/>
 <prover id="5" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="4000"/>
 <prover id="6" name="Alt-Ergo" version="2.0.0" timelimit="6" steplimit="0" memlimit="4000"/>
-<file name="../bitcount.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="bitcount.mlw"/>
 <theory name="BitCount8bit_fact" proved="true">
  <goal name="nth_as_bv_is_int" proved="true">
  <proof prover="0"><result status="valid" time="0.05"/></proof>
@@ -45,15 +47,11 @@
   <proof prover="6"><result status="valid" time="0.04" steps="78"/></proof>
   </goal>
   <goal name="VC step2.1" expl="precondition" proved="true">
-  <transf name="split_goal_right" proved="true" >
-   <goal name="VC step2.1.0" expl="precondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.04"/></proof>
-   <proof prover="2"><result status="valid" time="0.01"/></proof>
-   <proof prover="4"><result status="valid" time="0.07"/></proof>
-   <proof prover="5"><result status="valid" time="0.02"/></proof>
-   <proof prover="6"><result status="valid" time="0.02" steps="80"/></proof>
-   </goal>
-  </transf>
+  <proof prover="0"><result status="valid" time="0.04"/></proof>
+  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <proof prover="4"><result status="valid" time="0.07"/></proof>
+  <proof prover="5"><result status="valid" time="0.02"/></proof>
+  <proof prover="6"><result status="valid" time="0.02" steps="80"/></proof>
   </goal>
   <goal name="VC step2.2" expl="precondition" proved="true">
   <transf name="split_goal_right" proved="true" >
@@ -74,17 +72,21 @@
   </transf>
   </goal>
   <goal name="VC step2.3" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.04"/></proof>
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
-  <proof prover="4"><result status="valid" time="0.07"/></proof>
-  <proof prover="5"><result status="valid" time="0.02"/></proof>
-  <proof prover="6"><result status="valid" time="0.02" steps="83"/></proof>
+  <transf name="split_goal_right" proved="true" >
+   <goal name="VC step2.3.0" expl="precondition" proved="true">
+   <proof prover="0"><result status="valid" time="0.04"/></proof>
+   <proof prover="2"><result status="valid" time="0.01"/></proof>
+   <proof prover="4"><result status="valid" time="0.07"/></proof>
+   <proof prover="5"><result status="valid" time="0.02"/></proof>
+   <proof prover="6"><result status="valid" time="0.02" steps="83"/></proof>
+   </goal>
+  </transf>
   </goal>
   <goal name="VC step2.4" expl="assertion" proved="true">
   <transf name="split_goal_right" proved="true" >
    <goal name="VC step2.4.0" expl="assertion" proved="true">
    <proof prover="0"><result status="valid" time="0.11"/></proof>
-   <proof prover="2"><result status="valid" time="0.48"/></proof>
+   <proof prover="2"><result status="valid" time="0.69"/></proof>
    <proof prover="4"><result status="valid" time="0.10"/></proof>
    <proof prover="6"><result status="valid" time="0.10" steps="104"/></proof>
    </goal>
@@ -101,7 +103,7 @@
    <proof prover="0"><result status="valid" time="0.04"/></proof>
    </goal>
    <goal name="VC step2.4.4" expl="assertion" proved="true">
-   <proof prover="0"><result status="valid" time="2.87"/></proof>
+   <proof prover="0"><result status="valid" time="3.60"/></proof>
    </goal>
   </transf>
   </goal>
@@ -109,7 +111,7 @@
   <proof prover="0"><result status="valid" time="0.05"/></proof>
   <proof prover="4"><result status="valid" time="0.12"/></proof>
   <proof prover="5"><result status="valid" time="0.04"/></proof>
-  <proof prover="6" timelimit="5" memlimit="1000"><result status="valid" time="2.64" steps="1399"/></proof>
+  <proof prover="6" timelimit="5" memlimit="1000"><result status="valid" time="3.17" steps="1399"/></proof>
   </goal>
   <goal name="VC step2.6" expl="postcondition" proved="true">
   <proof prover="0"><result status="valid" time="0.10"/></proof>
@@ -129,8 +131,8 @@
   <proof prover="6"><result status="valid" time="0.04" steps="79"/></proof>
   </goal>
   <goal name="VC prove.1" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.03"/></proof>
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <proof prover="0"><result status="valid" time="0.04"/></proof>
+  <proof prover="2"><result status="valid" time="0.01"/></proof>
   <proof prover="4"><result status="valid" time="0.06"/></proof>
   <proof prover="5"><result status="valid" time="0.02"/></proof>
   <proof prover="6"><result status="valid" time="0.04" steps="81"/></proof>
@@ -139,7 +141,7 @@
   <proof prover="0"><result status="valid" time="0.04"/></proof>
   <proof prover="2"><result status="valid" time="0.02"/></proof>
   <proof prover="4"><result status="valid" time="0.06"/></proof>
-  <proof prover="5"><result status="valid" time="0.01"/></proof>
+  <proof prover="5"><result status="valid" time="0.02"/></proof>
   <proof prover="6"><result status="valid" time="0.04" steps="81"/></proof>
   </goal>
   <goal name="VC prove.3" expl="precondition" proved="true">
@@ -150,8 +152,8 @@
   <proof prover="6"><result status="valid" time="0.04" steps="81"/></proof>
   </goal>
   <goal name="VC prove.4" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.04"/></proof>
-  <proof prover="2"><result status="valid" time="0.01"/></proof>
+  <proof prover="0"><result status="valid" time="0.03"/></proof>
+  <proof prover="2"><result status="valid" time="0.02"/></proof>
   <proof prover="4"><result status="valid" time="0.06"/></proof>
   <proof prover="5"><result status="valid" time="0.02"/></proof>
   <proof prover="6"><result status="valid" time="0.04" steps="83"/></proof>
@@ -160,7 +162,7 @@
   <proof prover="0"><result status="valid" time="0.04"/></proof>
   <proof prover="2"><result status="valid" time="0.02"/></proof>
   <proof prover="4"><result status="valid" time="0.06"/></proof>
-  <proof prover="5"><result status="valid" time="0.02"/></proof>
+  <proof prover="5"><result status="valid" time="0.01"/></proof>
   <proof prover="6"><result status="valid" time="0.04" steps="83"/></proof>
   </goal>
   <goal name="VC prove.6" expl="assertion" proved="true">
@@ -300,7 +302,7 @@
    <proof prover="5"><result status="valid" time="0.12"/></proof>
    </goal>
    <goal name="VC proof1.6.2" expl="VC for proof1" proved="true">
-   <proof prover="4"><result status="valid" time="1.00"/></proof>
+   <proof prover="4"><result status="valid" time="1.41"/></proof>
    <proof prover="6"><result status="valid" time="0.04" steps="96"/></proof>
    </goal>
   </transf>
@@ -451,7 +453,7 @@
   <proof prover="6"><result status="valid" time="0.04" steps="87"/></proof>
   </goal>
   <goal name="VC proof3.8" expl="assertion" proved="true">
-  <proof prover="2"><result status="valid" time="0.51"/></proof>
+  <proof prover="2"><result status="valid" time="0.67"/></proof>
   <proof prover="4"><result status="valid" time="0.10"/></proof>
   <proof prover="6"><result status="valid" time="0.05" steps="114"/></proof>
   </goal>
@@ -476,7 +478,7 @@
    </goal>
    <goal name="VC proof3.11.2" expl="VC for proof3" proved="true">
    <proof prover="4"><result status="valid" time="0.08"/></proof>
-   <proof prover="5"><result status="valid" time="3.61"/></proof>
+   <proof prover="5"><result status="valid" time="4.08"/></proof>
    <proof prover="6"><result status="valid" time="0.03" steps="101"/></proof>
    </goal>
   </transf>
@@ -596,7 +598,7 @@
   </goal>
   <goal name="VC count.2" expl="precondition" proved="true">
   <proof prover="0"><result status="valid" time="0.02"/></proof>
-  <proof prover="2"><result status="valid" time="0.46"/></proof>
+  <proof prover="2"><result status="valid" time="0.61"/></proof>
   <proof prover="4"><result status="valid" time="0.08"/></proof>
   <proof prover="5"><result status="valid" time="0.12"/></proof>
   <proof prover="6"><result status="valid" time="0.05" steps="86"/></proof>
@@ -620,7 +622,7 @@
   <proof prover="2"><result status="valid" time="0.22"/></proof>
   <proof prover="4"><result status="valid" time="0.09"/></proof>
   <proof prover="5"><result status="valid" time="0.04"/></proof>
-  <proof prover="6"><result status="valid" time="0.05" steps="159"/></proof>
+  <proof prover="6"><result status="valid" time="0.05" steps="86"/></proof>
   </goal>
  </transf>
  </goal>
@@ -643,8 +645,8 @@
  <proof prover="6"><result status="valid" time="0.23" steps="450"/></proof>
  </goal>
  <goal name="numof_ytpmE" proved="true">
- <proof prover="0"><result status="valid" time="0.94"/></proof>
- <proof prover="4"><result status="valid" time="1.22"/></proof>
+ <proof prover="0"><result status="valid" time="1.42"/></proof>
+ <proof prover="4"><result status="valid" time="1.52"/></proof>
  </goal>
  <goal name="VC separation" expl="VC for separation" proved="true">
  <transf name="split_goal_right" proved="true" >
@@ -684,7 +686,7 @@
    <proof prover="6"><result status="valid" time="0.03" steps="79"/></proof>
    </goal>
    <goal name="VC triangleInequalityInt.0.1" expl="VC for triangleInequalityInt" proved="true">
-   <proof prover="0" timelimit="10"><result status="valid" time="5.72"/></proof>
+   <proof prover="0" timelimit="10"><result status="valid" time="7.41"/></proof>
    </goal>
   </transf>
   </goal>
@@ -742,7 +744,7 @@
  </goal>
  <goal name="VC numof_or" expl="VC for numof_or" proved="true">
  <proof prover="0"><result status="valid" time="0.31"/></proof>
- <proof prover="4"><result status="valid" time="0.45"/></proof>
+ <proof prover="4"><result status="valid" time="0.60"/></proof>
  <proof prover="5"><result status="valid" time="0.06"/></proof>
  </goal>
  <goal name="VC count_or" expl="VC for count_or" proved="true">
@@ -760,7 +762,7 @@
   <proof prover="5"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC count_or.3" expl="assertion" proved="true">
-  <proof prover="4"><result status="valid" time="2.02"/></proof>
+  <proof prover="4"><result status="valid" time="2.59"/></proof>
   </goal>
   <goal name="VC count_or.4" expl="postcondition" proved="true">
   <proof prover="0"><result status="valid" time="0.08"/></proof>
@@ -810,10 +812,10 @@
   </goal>
   <goal name="VC ascii.5" expl="postcondition" proved="true">
   <proof prover="0"><result status="valid" time="0.11"/></proof>
-  <proof prover="4"><result status="valid" time="1.58"/></proof>
+  <proof prover="4"><result status="valid" time="1.91"/></proof>
   </goal>
   <goal name="VC ascii.6" expl="postcondition" proved="true">
-  <proof prover="4"><result status="valid" time="0.52"/></proof>
+  <proof prover="4"><result status="valid" time="0.71"/></proof>
   <proof prover="5"><result status="valid" time="0.06"/></proof>
   <proof prover="6"><result status="valid" time="0.21" steps="374"/></proof>
   </goal>
@@ -836,7 +838,7 @@
   <proof prover="6"><result status="valid" time="0.02" steps="80"/></proof>
   </goal>
   <goal name="VC tmp.2" expl="postcondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.66"/></proof>
+  <proof prover="5"><result status="valid" time="0.87"/></proof>
   </goal>
  </transf>
  </goal>
diff --git a/examples/bitcount/why3shapes.gz b/examples/bitcount/why3shapes.gz
index bad78c0fbbda6a3038ea15a6b7b7350cbacb2a6f..008ba90f7c034ed2ea639660e59364eb3b8c39b1 100644
Binary files a/examples/bitcount/why3shapes.gz and b/examples/bitcount/why3shapes.gz differ
diff --git a/examples/bitvector_examples/why3session.xml b/examples/bitvector_examples/why3session.xml
index 6d509005f1bc7b6d2d29db412ccd8aab180c198a..6e05413e148b6cd21f23e6d4fd23a9652c9cb1d6 100644
--- a/examples/bitvector_examples/why3session.xml
+++ b/examples/bitvector_examples/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="4" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
 <file proved="true">
diff --git a/examples/bitvector_examples/why3shapes.gz b/examples/bitvector_examples/why3shapes.gz
index ccd714caf824012c2d14a92a3d34214a2eef1f92..67d2cacb2355613338e79e333b99df5ff0a48c13 100644
Binary files a/examples/bitvector_examples/why3shapes.gz and b/examples/bitvector_examples/why3shapes.gz differ
diff --git a/examples/bitvectors/double/why3session.xml b/examples/bitvectors/double/why3session.xml
index 486a719490403ecc0009cf2556c3614b43f72a0e..7814590ef9f04a8c40cb4ee2a84bdd214b5653ee 100644
--- a/examples/bitvectors/double/why3session.xml
+++ b/examples/bitvectors/double/why3session.xml
@@ -1,13 +1,15 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="4" name="Coq" version="8.7.1" timelimit="30" steplimit="0" memlimit="1000"/>
 <prover id="5" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../double.why" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="double.why"/>
 <theory name="TestDouble" proved="true">
  <goal name="nth_one1" proved="true">
  <proof prover="2" timelimit="3"><result status="valid" time="0.05" steps="79"/></proof>
@@ -26,7 +28,7 @@
  </goal>
  <goal name="exp_one" proved="true">
  <proof prover="2" timelimit="30"><result status="valid" time="0.16" steps="210"/></proof>
- <proof prover="4" edited="double_TestDouble_exp_one_1.v"><result status="valid" time="0.52"/></proof>
+ <proof prover="4" edited="double_TestDouble_exp_one_1.v"><result status="valid" time="1.23"/></proof>
  </goal>
  <goal name="mantissa_one" proved="true">
  <proof prover="2"><result status="valid" time="0.09" steps="88"/></proof>
diff --git a/examples/bitvectors/double/why3shapes.gz b/examples/bitvectors/double/why3shapes.gz
index e7f33afc95e1cb742492b8867b92c786478b3acb..26fae3d7086e27c440e2e8a11b6b92c0a03c1d22 100644
Binary files a/examples/bitvectors/double/why3shapes.gz and b/examples/bitvectors/double/why3shapes.gz differ
diff --git a/examples/bitvectors/double_of_int/why3session.xml b/examples/bitvectors/double_of_int/why3session.xml
index ed042e656f3e1c350a2035fa5b74b8f114bda7b2..4bd77e7d3ffa05081eadb103383a4bb6c02ba4e1 100644
--- a/examples/bitvectors/double_of_int/why3session.xml
+++ b/examples/bitvectors/double_of_int/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="3" name="Eprover" version="2.0" timelimit="1" steplimit="0" memlimit="1000"/>
@@ -11,7 +11,9 @@
 <prover id="8" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="10" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="11" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
-<file name="../double_of_int.why" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="double_of_int.why"/>
 <theory name="DoubleOfInt" proved="true">
  <goal name="nth_j1" proved="true">
  <proof prover="10"><result status="valid" time="0.04" steps="80"/></proof>
@@ -60,7 +62,7 @@
  <proof prover="10"><result status="valid" time="0.11" steps="101"/></proof>
  </goal>
  <goal name="nth_const6" proved="true">
- <proof prover="4"><result status="valid" time="1.36"/></proof>
+ <proof prover="4"><result status="valid" time="1.72"/></proof>
  <proof prover="8"><result status="valid" time="0.79"/></proof>
  <proof prover="10"><result status="valid" time="0.09" steps="101"/></proof>
  </goal>
@@ -88,7 +90,7 @@
  <proof prover="10"><result status="valid" time="0.03" steps="80"/></proof>
  </goal>
  <goal name="exp_const" proved="true">
- <proof prover="5" timelimit="30" edited="double_of_int_DoubleOfInt_exp_const_1.v"><result status="valid" time="0.80"/></proof>
+ <proof prover="5" timelimit="30" edited="double_of_int_DoubleOfInt_exp_const_1.v"><result status="valid" time="1.50"/></proof>
  </goal>
  <goal name="to_nat_mantissa_1" proved="true">
  <proof prover="4"><result status="valid" time="1.11"/></proof>
@@ -140,7 +142,7 @@
  </goal>
  <goal name="nth_0_30" proved="true">
  <proof prover="2"><result status="valid" time="0.46"/></proof>
- <proof prover="4"><result status="valid" time="3.12"/></proof>
+ <proof prover="4"><result status="valid" time="3.60"/></proof>
  </goal>
  <goal name="nth_jpxor_0_30" proved="true">
  <proof prover="2"><result status="valid" time="0.06"/></proof>
@@ -148,7 +150,7 @@
  <proof prover="10"><result status="valid" time="0.08" steps="106"/></proof>
  </goal>
  <goal name="nth_var31" proved="true">
- <proof prover="4"><result status="valid" time="2.76"/></proof>
+ <proof prover="4"><result status="valid" time="3.16"/></proof>
  <proof prover="10" timelimit="125"><result status="valid" time="0.96" steps="476"/></proof>
  </goal>
  <goal name="to_nat_sub_0_30" proved="true">
@@ -164,7 +166,7 @@
  <proof prover="10"><result status="valid" time="0.13" steps="148"/></proof>
  </goal>
  <goal name="from_int2c_to_nat_sub_pos" proved="true">
- <proof prover="5" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_pos_1.v"><result status="valid" time="0.56"/></proof>
+ <proof prover="5" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_pos_1.v"><result status="valid" time="1.58"/></proof>
  </goal>
  <goal name="lemma1_pos" proved="true">
  <transf name="split_all_full" proved="true" >
@@ -180,7 +182,7 @@
  <proof prover="8"><result status="valid" time="0.19"/></proof>
  </goal>
  <goal name="from_int2c_to_nat_sub_neg" proved="true">
- <proof prover="5" timelimit="5" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_neg_1.v"><result status="valid" time="0.66"/></proof>
+ <proof prover="5" timelimit="5" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_neg_1.v"><result status="valid" time="1.49"/></proof>
  </goal>
  <goal name="lemma1_neg" proved="true">
  <transf name="split_all_full" proved="true" >
@@ -249,7 +251,7 @@
  </transf>
  </goal>
  <goal name="nth_var4" proved="true">
- <proof prover="4"><result status="valid" time="1.50"/></proof>
+ <proof prover="4"><result status="valid" time="1.84"/></proof>
  <proof prover="8"><result status="valid" time="0.85"/></proof>
  <proof prover="10"><result status="valid" time="0.14" steps="149"/></proof>
  </goal>
@@ -308,7 +310,7 @@
     <goal name="var_value0.0.0.0" proved="true">
     <transf name="rewrite" proved="true" arg1="sign_var">
      <goal name="var_value0.0.0.0.0" proved="true">
-     <proof prover="3"><result status="valid" time="0.64"/></proof>
+     <proof prover="3"><result status="valid" time="0.04"/></proof>
      <transf name="split_all_full" proved="true" >
       <goal name="var_value0.0.0.0.0.0" proved="true">
       <proof prover="10" timelimit="10" memlimit="4000"><result status="valid" time="1.05" steps="271"/></proof>
diff --git a/examples/bitvectors/double_of_int/why3shapes.gz b/examples/bitvectors/double_of_int/why3shapes.gz
index a6d44f7d1e818f3e7c6aa9d3989259c88e92937b..1f9b62755cc6c96ffca7f7d6ecb00c420f0f6eb8 100644
Binary files a/examples/bitvectors/double_of_int/why3shapes.gz and b/examples/bitvectors/double_of_int/why3shapes.gz differ
diff --git a/examples/bitvectors/neg_as_xor/why3session.xml b/examples/bitvectors/neg_as_xor/why3session.xml
index 0ba4121ad56be971fb6f18f68bc2096c57c15ff9..a9e3b46d5428b1704ec35992cbf5456827bbcbf1 100644
--- a/examples/bitvectors/neg_as_xor/why3session.xml
+++ b/examples/bitvectors/neg_as_xor/why3session.xml
@@ -1,19 +1,21 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="5" name="Z3" version="3.2" timelimit="10" steplimit="0" memlimit="1000"/>
 <prover id="9" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../neg_as_xor.why" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="neg_as_xor.why"/>
 <theory name="TestNegAsXOR" proved="true">
  <goal name="Nth_j" proved="true">
  <proof prover="0"><result status="valid" time="0.05" steps="79"/></proof>
  </goal>
  <goal name="sign_of_j" proved="true">
  <proof prover="0"><result status="valid" time="0.02" steps="75"/></proof>
- <proof prover="3"><result status="valid" time="4.23"/></proof>
+ <proof prover="3"><result status="valid" time="4.98"/></proof>
  </goal>
  <goal name="mantissa_of_j" proved="true">
  <proof prover="0"><result status="valid" time="0.16" steps="121"/></proof>
@@ -54,7 +56,7 @@
  <proof prover="9"><result status="valid" time="0.69"/></proof>
  </goal>
  <goal name="Mantissa_of_xor_j" proved="true">
- <proof prover="3"><result status="valid" time="1.43"/></proof>
+ <proof prover="3"><result status="valid" time="1.75"/></proof>
  <proof prover="5"><result status="valid" time="3.22"/></proof>
  <proof prover="9"><result status="valid" time="0.75"/></proof>
  </goal>
diff --git a/examples/bitvectors/neg_as_xor/why3shapes.gz b/examples/bitvectors/neg_as_xor/why3shapes.gz
index 94a3b03ead537935ce2774615db2207da8f48fe8..cb3c9f980dca194c94b6692dc168cbfc36715d29 100644
Binary files a/examples/bitvectors/neg_as_xor/why3shapes.gz and b/examples/bitvectors/neg_as_xor/why3shapes.gz differ
diff --git a/examples/bitvectors/power2/why3session.xml b/examples/bitvectors/power2/why3session.xml
index 2d1ffe0088abb878faac27c75c90768543ac4afc..e371b42f971bdeddff13e2b6bebf6dd24ca33e95 100644
--- a/examples/bitvectors/power2/why3session.xml
+++ b/examples/bitvectors/power2/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Eprover" version="2.0" timelimit="5" steplimit="0" memlimit="2000"/>
 <prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
@@ -10,7 +10,9 @@
 <prover id="6" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="7" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="9" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../power2.why" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="power2.why"/>
 <theory name="Pow2int" proved="true">
  <goal name="Power_1" proved="true">
  <proof prover="2"><result status="valid" time="0.00"/></proof>
@@ -310,7 +312,7 @@
  <proof prover="2"><result status="valid" time="0.03"/></proof>
  <proof prover="6"><result status="valid" time="0.85"/></proof>
  <proof prover="7"><result status="valid" time="0.02" steps="44"/></proof>
- <proof prover="9"><result status="valid" time="0.76"/></proof>
+ <proof prover="9"><result status="valid" time="0.97"/></proof>
  </goal>
  <goal name="pow2_41" proved="true">
  <proof prover="2"><result status="valid" time="0.00"/></proof>
@@ -322,7 +324,7 @@
  <proof prover="2"><result status="valid" time="0.03"/></proof>
  <proof prover="6"><result status="valid" time="0.92"/></proof>
  <proof prover="7"><result status="valid" time="0.02" steps="46"/></proof>
- <proof prover="9"><result status="valid" time="0.87"/></proof>
+ <proof prover="9"><result status="valid" time="1.08"/></proof>
  </goal>
  <goal name="pow2_43" proved="true">
  <proof prover="2"><result status="valid" time="0.00"/></proof>
@@ -352,7 +354,7 @@
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="6" timelimit="6"><result status="valid" time="1.24"/></proof>
  <proof prover="7"><result status="valid" time="0.02" steps="51"/></proof>
- <proof prover="9"><result status="valid" time="1.23"/></proof>
+ <proof prover="9"><result status="valid" time="1.46"/></proof>
  </goal>
  <goal name="pow2_48" proved="true">
  <proof prover="2"><result status="valid" time="0.04"/></proof>
@@ -434,7 +436,7 @@
  </goal>
  <goal name="pow2_61" proved="true">
  <proof prover="2"><result status="valid" time="0.00"/></proof>
- <proof prover="6" timelimit="8"><result status="valid" time="5.62"/></proof>
+ <proof prover="6" timelimit="8"><result status="valid" time="6.32"/></proof>
  <proof prover="7"><result status="valid" time="0.03" steps="65"/></proof>
  <proof prover="9"><result status="valid" time="2.51"/></proof>
  </goal>
@@ -581,7 +583,7 @@
  </transf>
  </goal>
  <goal name="Power_sum" proved="true">
- <proof prover="1"><result status="valid" time="3.92"/></proof>
+ <proof prover="1"><result status="valid" time="1.87"/></proof>
  </goal>
  <goal name="Pow2_int_real" proved="true">
  <transf name="introduce_premises" proved="true" >
diff --git a/examples/bitvectors/power2/why3shapes.gz b/examples/bitvectors/power2/why3shapes.gz
index 0c353e60f6a549d17c2322a81ea5df1c0d0cbd71..487e683871678ad4086a5f8f7959206d5e57ead7 100644
Binary files a/examples/bitvectors/power2/why3shapes.gz and b/examples/bitvectors/power2/why3shapes.gz differ
diff --git a/examples/bitwalker/why3session.xml b/examples/bitwalker/why3session.xml
index cfbe5fd58ed3a4e521e0b96486a25474c7762c1e..bbb35462119cffe996a92972663a7214b3640c34 100644
--- a/examples/bitwalker/why3session.xml
+++ b/examples/bitwalker/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Z3" version="4.7.1" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
diff --git a/examples/bitwalker/why3shapes.gz b/examples/bitwalker/why3shapes.gz
index a42964e5846e39b13828bc064f10c149f2852044..5427437762e1e1581dc9949027509c479329d59f 100644
Binary files a/examples/bitwalker/why3shapes.gz and b/examples/bitwalker/why3shapes.gz differ
diff --git a/examples/bts/116_array_access/why3session.xml b/examples/bts/116_array_access/why3session.xml
index 07a03a924d2dd380b5ccae04f8bf96a3a5cbe899..d0c9cd05dd9fdadd9fe90d30f5b8274cc9c783ca 100644
--- a/examples/bts/116_array_access/why3session.xml
+++ b/examples/bts/116_array_access/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <file>
 <path name=".."/>
 <path name="116_array_access.mlw"/>
diff --git a/examples/bts/116_array_access/why3shapes.gz b/examples/bts/116_array_access/why3shapes.gz
index 23e30289d572d0dc6e8c1d6b4f9855dcca132a68..744a01c1512c7812f6152d4b10c993f59af90a8c 100644
Binary files a/examples/bts/116_array_access/why3shapes.gz and b/examples/bts/116_array_access/why3shapes.gz differ
diff --git a/examples/bts/12475/why3session.xml b/examples/bts/12475/why3session.xml
index dbcf583033a9935fc7c049b3f5a52e0a0a8e30df..f921a6ed9b18dd7d6d8fdaf54fcafbb763da93b7 100644
--- a/examples/bts/12475/why3session.xml
+++ b/examples/bts/12475/why3session.xml
@@ -1,12 +1,14 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="1" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="CVC3" version="2.4.1" timelimit="2" steplimit="0" memlimit="0"/>
 <prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="4" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../12475.why" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="12475.why"/>
 <theory name="Stmt" proved="true">
  <goal name="toto" proved="true">
  <proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
diff --git a/examples/bts/12475/why3shapes.gz b/examples/bts/12475/why3shapes.gz
index c0d4de6244ecdc0a1f9869d3deac7508e92745f3..f53a869a8b36c093476a7c0cda50d2254ca2912a 100644
Binary files a/examples/bts/12475/why3shapes.gz and b/examples/bts/12475/why3shapes.gz differ
diff --git a/examples/bts/71_disambiguation/why3session.xml b/examples/bts/71_disambiguation/why3session.xml
index 53a332ed184cefb3d14f6b38096505a2231e5359..54375a5e85c449067535d68f8d48e61513c4ed47 100644
--- a/examples/bts/71_disambiguation/why3session.xml
+++ b/examples/bts/71_disambiguation/why3session.xml
@@ -1,9 +1,11 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../71_disambiguation.mlw">
+<file>
+<path name=".."/>
+<path name="71_disambiguation.mlw"/>
 <theory name="M" proved="true">
  <goal name="g" proved="true">
  <proof prover="0"><result status="valid" time="0.00"/></proof>
@@ -19,11 +21,11 @@
   <transf name="cut" arg1="(1.0 +&#39; 1.3 = 2.2)">
    <goal name="g.0.0">
    </goal>
-   <goal name="g.0.1">
+   <goal name="g.0.1" expl="asserted formula">
    </goal>
   </transf>
   </goal>
-  <goal name="g.1">
+  <goal name="g.1" expl="asserted formula">
   </goal>
  </transf>
  </goal>
diff --git a/examples/bts/71_disambiguation/why3shapes.gz b/examples/bts/71_disambiguation/why3shapes.gz
index c78bcb71c0f0cfd6e9fe6aa496bed0133ce53a81..981c6dc90c0c2b7203c3488d1a52e8ae0d990ed2 100644
Binary files a/examples/bts/71_disambiguation/why3shapes.gz and b/examples/bts/71_disambiguation/why3shapes.gz differ
diff --git a/examples/check-builtin/floats/why3session.xml b/examples/check-builtin/floats/why3session.xml
index 4acf44f27684f97af694aa70f01ef3289f82fb22..a21e89965198fb717c5c60c1d350dc176d61d6f0 100644
--- a/examples/check-builtin/floats/why3session.xml
+++ b/examples/check-builtin/floats/why3session.xml
@@ -1,12 +1,14 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/>
 <prover id="1" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="0"/>
 <prover id="2" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="0"/>
 <prover id="5" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="0"/>
-<file name="../floats.why" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="floats.why"/>
 <theory name="TestGappa" proved="true">
  <goal name="Round_single_01" proved="true">
  <proof prover="1"><result status="valid" time="0.00"/></proof>
diff --git a/examples/check-builtin/floats/why3shapes.gz b/examples/check-builtin/floats/why3shapes.gz
index a1da9902242640e27daceba7e1380efd1c74eaed..12784a74d14592739bc1bb29f2bb2bb2b50ccd33 100644
Binary files a/examples/check-builtin/floats/why3shapes.gz and b/examples/check-builtin/floats/why3shapes.gz differ
diff --git a/examples/check-builtin/intreal/why3session.xml b/examples/check-builtin/intreal/why3session.xml
index 0b55954969b30b14658f76ce6b61324c0e743322..3cc071aa5938f1804ef743388b33516dc4fdf601 100644
--- a/examples/check-builtin/intreal/why3session.xml
+++ b/examples/check-builtin/intreal/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="CVC3" version="2.4.1" timelimit="10" steplimit="0" memlimit="0"/>
 <prover id="1" name="Gappa" version="1.3.0" timelimit="2" steplimit="0" memlimit="0"/>
 <prover id="2" name="Alt-Ergo" version="2.1.0" timelimit="5" steplimit="0" memlimit="1000"/>
@@ -10,7 +10,9 @@
 <prover id="5" name="Alt-Ergo" version="2.2.0" timelimit="10" steplimit="0" memlimit="0"/>
 <prover id="6" name="Z3" version="3.2" timelimit="10" steplimit="0" memlimit="0"/>
 <prover id="9" name="Z3" version="4.3.2" timelimit="10" steplimit="0" memlimit="0"/>
-<file name="../intreal.why" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="intreal.why"/>
 <theory name="IntReal" proved="true">
  <goal name="G1" proved="true">
  <proof prover="0"><result status="valid" time="0.00"/></proof>
diff --git a/examples/check-builtin/intreal/why3shapes.gz b/examples/check-builtin/intreal/why3shapes.gz
index cacf820c2eda2939ded0d5c05f8c4ef4808bb922..ed2d743df62c08abb0aee292b2289d882b00329a 100644
Binary files a/examples/check-builtin/intreal/why3shapes.gz and b/examples/check-builtin/intreal/why3shapes.gz differ
diff --git a/examples/check-builtin/real/why3session.xml b/examples/check-builtin/real/why3session.xml
index ca838ccf4864fe4423f96180f6d7337c3f0826e2..c54e006ecb23c9f5436e3944c406a8f121062b0d 100644
--- a/examples/check-builtin/real/why3session.xml
+++ b/examples/check-builtin/real/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Alt-Ergo" version="2.2.0" timelimit="3" steplimit="0" memlimit="0"/>
 <prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/>
@@ -9,7 +9,9 @@
 <prover id="8" name="Z3" version="3.2" timelimit="3" steplimit="0" memlimit="0"/>
 <prover id="9" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="0"/>
 <prover id="14" name="Z3" version="4.3.2" timelimit="3" steplimit="0" memlimit="0"/>
-<file name="../real.why" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="real.why"/>
 <theory name="Test" proved="true">
  <goal name="G1" proved="true">
  <proof prover="1"><result status="valid" time="0.01" steps="0"/></proof>
@@ -135,13 +137,13 @@
  <proof prover="14"><result status="valid" time="0.17"/></proof>
  </goal>
  <goal name="Tan_pi_4" proved="true">
- <proof prover="0" edited="real_TrigonometryTest_Tan_pi_4_1.v"><result status="valid" time="0.39"/></proof>
+ <proof prover="0" edited="real_TrigonometryTest_Tan_pi_4_1.v"><result status="valid" time="1.32"/></proof>
  </goal>
  <goal name="Tan_pi_3" proved="true">
- <proof prover="0" edited="real_TrigonometryTest_Tan_pi_3_1.v"><result status="valid" time="0.43"/></proof>
+ <proof prover="0" edited="real_TrigonometryTest_Tan_pi_3_1.v"><result status="valid" time="1.28"/></proof>
  </goal>
  <goal name="Atan_1" proved="true">
- <proof prover="0" edited="real_TrigonometryTest_Atan_1_1.v"><result status="valid" time="0.41"/></proof>
+ <proof prover="0" edited="real_TrigonometryTest_Atan_1_1.v"><result status="valid" time="1.27"/></proof>
  </goal>
 </theory>
 </file>
diff --git a/examples/check-builtin/real/why3shapes.gz b/examples/check-builtin/real/why3shapes.gz
index a3151f21a7b4405d0b7ea3d57152c651afcc4435..1d89785fe8b984b363085983e8b73a9f5f6bb5e7 100644
Binary files a/examples/check-builtin/real/why3shapes.gz and b/examples/check-builtin/real/why3shapes.gz differ
diff --git a/examples/esterel/why3session.xml b/examples/esterel/why3session.xml
index f7046e89cb251dd99bec1554eaad3a7a46bec993..d6df6e957f75c0059c7ee5aa27692a0645c4ac5b 100644
--- a/examples/esterel/why3session.xml
+++ b/examples/esterel/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="4" name="Z3" version="4.6.0" timelimit="5" steplimit="0" memlimit="4000"/>
 <prover id="5" name="Eprover" version="2.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="6" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="4000"/>
diff --git a/examples/esterel/why3shapes.gz b/examples/esterel/why3shapes.gz
index be9ab491995fce6d7558c0ad90d3d6f2c7ac5332..0d67f4410767c550f185823966113d44a3b9d5c0 100644
Binary files a/examples/esterel/why3shapes.gz and b/examples/esterel/why3shapes.gz differ
diff --git a/examples/gcd/why3session.xml b/examples/gcd/why3session.xml
index c82e78c0f492ac5fe0e8dc9c27e818b63f509975..ba4def3230ea6215fc90c1c3a5f10eecb87dec66 100644
--- a/examples/gcd/why3session.xml
+++ b/examples/gcd/why3session.xml
@@ -1,13 +1,15 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="3" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="5" name="Eprover" version="2.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="6" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="7" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
-<file name="../gcd.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="gcd.mlw"/>
 <theory name="EuclideanAlgorithm" proved="true">
  <goal name="VC euclid" expl="VC for euclid" proved="true">
  <transf name="split_goal_right" proved="true" >
@@ -45,7 +47,7 @@
  <proof prover="6"><result status="valid" time="0.01" steps="31"/></proof>
  </goal>
  <goal name="gcd_even_odd" proved="true">
- <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="1.00"/></proof>
  </goal>
  <goal name="gcd_even_odd2" proved="true">
  <proof prover="6"><result status="valid" time="0.05" steps="29"/></proof>
diff --git a/examples/gcd/why3shapes.gz b/examples/gcd/why3shapes.gz
index 4c247541d829f1efd370b82725e2c1c7ab7605a4..6fc22356bdbfa132eda16e7a137c3e41d0b8bcfd 100644
Binary files a/examples/gcd/why3shapes.gz and b/examples/gcd/why3shapes.gz differ
diff --git a/examples/gcd_vc_sp/why3session.xml b/examples/gcd_vc_sp/why3session.xml
index 32695d99febea4bc1d770574a6144684352c2264..b3dac49e5e20a10a190331b856237914956178a0 100644
--- a/examples/gcd_vc_sp/why3session.xml
+++ b/examples/gcd_vc_sp/why3session.xml
@@ -1,12 +1,14 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="2" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="3" name="Coq" version="8.7.1" timelimit="0" steplimit="0" memlimit="0"/>
 <prover id="4" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
-<file name="../gcd_vc_sp.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="gcd_vc_sp.mlw"/>
 <theory name="EuclideanAlgorithm" proved="true">
  <goal name="VC euclid" expl="VC for euclid" proved="true">
  <proof prover="2"><result status="valid" time="0.06"/></proof>
@@ -31,7 +33,7 @@
  <proof prover="4"><result status="valid" time="0.01" steps="31"/></proof>
  </goal>
  <goal name="gcd_even_odd" proved="true">
- <proof prover="3" edited="gcd_vc_sp_BinaryGcd_gcd_even_odd_1.v"><result status="valid" time="0.33"/></proof>
+ <proof prover="3" edited="gcd_vc_sp_BinaryGcd_gcd_even_odd_1.v"><result status="valid" time="1.06"/></proof>
  </goal>
  <goal name="gcd_even_odd2" proved="true">
  <proof prover="4"><result status="valid" time="0.05" steps="29"/></proof>
diff --git a/examples/gcd_vc_sp/why3shapes.gz b/examples/gcd_vc_sp/why3shapes.gz
index b15ff82fa221f8244d1d7971473e890660b92652..62c1750af3c08c9f23f2e1cfd808d08b04b6d34c 100644
Binary files a/examples/gcd_vc_sp/why3shapes.gz and b/examples/gcd_vc_sp/why3shapes.gz differ
diff --git a/examples/hackers-delight/why3session.xml b/examples/hackers-delight/why3session.xml
index 62abdfb41c8fc3a9635a2fbb87d57abbd699432d..9f8799dce53548b1665e1a65101bc92a5a10d911 100644
--- a/examples/hackers-delight/why3session.xml
+++ b/examples/hackers-delight/why3session.xml
@@ -1,12 +1,14 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="5" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="8" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="9" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
-<file name="../hackers-delight.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="hackers-delight.mlw"/>
 <theory name="Utils_Spec" proved="true">
  <goal name="countZero" proved="true">
  <proof prover="9"><result status="valid" time="0.01"/></proof>
diff --git a/examples/hackers-delight/why3shapes.gz b/examples/hackers-delight/why3shapes.gz
index ca63163fe7ebec271b76a2904919c80c11cdd984..6ad6cf703f37f1aa7c7ec1cceb7a4599505a3d23 100644
Binary files a/examples/hackers-delight/why3shapes.gz and b/examples/hackers-delight/why3shapes.gz differ
diff --git a/examples/hillel_challenge/why3session.xml b/examples/hillel_challenge/why3session.xml
index 2b7588703db5b1b9193f23b754d20d3442987190..ff80a26cbfc50a9a05ef22ed6a851efe06ff37d5 100644
--- a/examples/hillel_challenge/why3session.xml
+++ b/examples/hillel_challenge/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
diff --git a/examples/hillel_challenge/why3shapes.gz b/examples/hillel_challenge/why3shapes.gz
index be517b8385fbdadb794318232621e3498d9527b2..bb53b81f82522c0670edfd105eccfe7969a4044f 100644
Binary files a/examples/hillel_challenge/why3shapes.gz and b/examples/hillel_challenge/why3shapes.gz differ
diff --git a/examples/isqrt_von_neumann/why3session.xml b/examples/isqrt_von_neumann/why3session.xml
index 6808189a2478c4431b5dc774b483d244e01896b8..f8a84da22bdb7aefdbbc282b60d22f8a7e84313d 100644
--- a/examples/isqrt_von_neumann/why3session.xml
+++ b/examples/isqrt_von_neumann/why3session.xml
@@ -1,13 +1,15 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="4" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="5" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../isqrt_von_neumann.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="isqrt_von_neumann.mlw"/>
 <theory name="VonNeumann16" proved="true">
  <goal name="sqr_add2" proved="true">
  <proof prover="2" timelimit="1"><result status="valid" time="0.16"/></proof>
@@ -160,10 +162,10 @@
   <proof prover="3"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC isqrt32.1" expl="loop invariant init" proved="true">
-  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="VC isqrt32.2" expl="loop invariant init" proved="true">
-  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC isqrt32.3" expl="loop invariant init" proved="true">
   <proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -368,10 +370,10 @@
   <proof prover="3" timelimit="5"><result status="valid" time="0.91"/></proof>
   </goal>
   <goal name="VC isqrt64.18" expl="assertion" proved="true">
-  <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.58"/></proof>
+  <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.89"/></proof>
   </goal>
   <goal name="VC isqrt64.19" expl="loop variant decrease" proved="true">
-  <proof prover="3" timelimit="5"><result status="valid" time="1.01"/></proof>
+  <proof prover="3" timelimit="5"><result status="valid" time="1.63"/></proof>
   </goal>
   <goal name="VC isqrt64.20" expl="loop invariant preservation" proved="true">
   <proof prover="3"><result status="valid" time="0.36"/></proof>
@@ -380,13 +382,13 @@
   <proof prover="3"><result status="valid" time="0.50"/></proof>
   </goal>
   <goal name="VC isqrt64.22" expl="loop invariant preservation" proved="true">
-  <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="2.42"/></proof>
+  <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="2.98"/></proof>
   </goal>
   <goal name="VC isqrt64.23" expl="loop invariant preservation" proved="true">
-  <proof prover="3" timelimit="60"><result status="valid" time="1.70"/></proof>
+  <proof prover="3" timelimit="60"><result status="valid" time="1.99"/></proof>
   </goal>
   <goal name="VC isqrt64.24" expl="loop invariant preservation" proved="true">
-  <proof prover="3"><result status="valid" time="0.34"/></proof>
+  <proof prover="3"><result status="valid" time="0.49"/></proof>
   </goal>
   <goal name="VC isqrt64.25" expl="loop invariant preservation" proved="true">
   <proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -419,7 +421,7 @@
   <proof prover="3"><result status="valid" time="0.54"/></proof>
   </goal>
   <goal name="VC isqrt64.30" expl="loop variant decrease" proved="true">
-  <proof prover="3" timelimit="5"><result status="valid" time="1.00"/></proof>
+  <proof prover="3" timelimit="5"><result status="valid" time="1.25"/></proof>
   </goal>
   <goal name="VC isqrt64.31" expl="loop invariant preservation" proved="true">
   <proof prover="3"><result status="valid" time="0.30"/></proof>
@@ -508,7 +510,7 @@
                 <goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.0" expl="true case" proved="true">
                 <transf name="unfold" proved="true" arg1="sqr" arg2="in" arg3="h">
                  <goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.0.0" expl="true case" proved="true">
-                 <proof prover="3" timelimit="5"><result status="valid" time="2.30"/></proof>
+                 <proof prover="3" timelimit="5"><result status="valid" time="3.24"/></proof>
                  </goal>
                 </transf>
                 </goal>
@@ -587,7 +589,7 @@
                              <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="2.80" steps="571"/></proof>
                              </goal>
                              <goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.0.0.0.1.0.0.0.1" expl="rewrite premises" proved="true">
-                             <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="2.16"/></proof>
+                             <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="3.04"/></proof>
                              </goal>
                             </transf>
                             </goal>
@@ -611,7 +613,7 @@
                        </transf>
                        </goal>
                        <goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.0.1" expl="rewrite premises" proved="true">
-                       <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.91"/></proof>
+                       <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="2.59"/></proof>
                        </goal>
                       </transf>
                       </goal>
@@ -650,7 +652,7 @@
                               </transf>
                               </goal>
                               <goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.1.0.0.1.0.0.0.0.1" expl="rewrite premises" proved="true">
-                              <proof prover="3" timelimit="5"><result status="valid" time="1.99"/></proof>
+                              <proof prover="3" timelimit="5"><result status="valid" time="2.73"/></proof>
                               </goal>
                              </transf>
                              </goal>
@@ -679,7 +681,7 @@
                        </transf>
                        </goal>
                        <goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.1.1" expl="rewrite premises" proved="true">
-                       <proof prover="3" timelimit="5"><result status="valid" time="2.16"/></proof>
+                       <proof prover="3" timelimit="5"><result status="valid" time="2.62"/></proof>
                        </goal>
                       </transf>
                       </goal>
diff --git a/examples/isqrt_von_neumann/why3shapes.gz b/examples/isqrt_von_neumann/why3shapes.gz
index 79de5d9934ff6cef23f57ec122e73826f43dca8b..735624d21e19f661b7a3d7ffa39235f273e33486 100644
Binary files a/examples/isqrt_von_neumann/why3shapes.gz and b/examples/isqrt_von_neumann/why3shapes.gz differ
diff --git a/examples/logic/bitvectors/why3session.xml b/examples/logic/bitvectors/why3session.xml
index 023cd1024b0ae5c4d43073f28e1fdc83e298dc7f..8454ca7caaa0831ee85e18c7ee7a4524021e73ea 100644
--- a/examples/logic/bitvectors/why3session.xml
+++ b/examples/logic/bitvectors/why3session.xml
@@ -1,14 +1,16 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Z3" version="4.7.1" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="3" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="4" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="5" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
-<file name="../bitvectors.why">
+<file>
+<path name=".."/>
+<path name="bitvectors.why"/>
 <theory name="TestBV">
  <goal name="g1" proved="true">
  <proof prover="2"><result status="valid" time="0.01"/></proof>
diff --git a/examples/logic/bitvectors/why3shapes.gz b/examples/logic/bitvectors/why3shapes.gz
index 8eae555d000be21795386dcd2e91a9d41fc6be33..9bd7fa7bfb0f10ffdbcfaaf59f9bb3905fb4da1f 100644
Binary files a/examples/logic/bitvectors/why3shapes.gz and b/examples/logic/bitvectors/why3shapes.gz differ
diff --git a/examples/logic/lagrange_inequality/why3session.xml b/examples/logic/lagrange_inequality/why3session.xml
index 84b4807f5fa7165c6cb9ebb3950bdf3a846ad907..7d94b7eb373f7a9c1423514ea208ef34102931e8 100644
--- a/examples/logic/lagrange_inequality/why3session.xml
+++ b/examples/logic/lagrange_inequality/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="CVC3" version="2.4.1" timelimit="3" steplimit="0" memlimit="1000"/>
 <prover id="3" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
@@ -9,7 +9,9 @@
 <prover id="5" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="6" name="MetiTarski" version="2.4" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="11" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../lagrange_inequality.why" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="lagrange_inequality.why"/>
 <theory name="LagrangeInequality" proved="true">
  <goal name="norm2_pos" proved="true">
  <proof prover="6"><result status="valid" time="0.02"/></proof>
@@ -48,7 +50,7 @@
  <proof prover="6"><result status="valid" time="0.06"/></proof>
  </goal>
  <goal name="triangle" proved="true">
- <proof prover="0" edited="lagrange_inequality_TriangleInequality_triangle_1.v"><result status="valid" time="0.33"/></proof>
+ <proof prover="0" edited="lagrange_inequality_TriangleInequality_triangle_1.v"><result status="valid" time="1.06"/></proof>
  </goal>
 </theory>
 </file>
diff --git a/examples/logic/lagrange_inequality/why3shapes.gz b/examples/logic/lagrange_inequality/why3shapes.gz
index 9714ed1ed663f462732825c90a5293bbd30df4de..e9f733b34e8534087e002434a0ae9f396532de13 100644
Binary files a/examples/logic/lagrange_inequality/why3shapes.gz and b/examples/logic/lagrange_inequality/why3shapes.gz differ
diff --git a/examples/logic/my_cosine/why3session.xml b/examples/logic/my_cosine/why3session.xml
index 545b278b716abeeb0d1de55e611c80b837899498..a59b121953d6bd7c537105029a115717e0f65cd5 100644
--- a/examples/logic/my_cosine/why3session.xml
+++ b/examples/logic/my_cosine/why3session.xml
@@ -1,15 +1,17 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Gappa" version="1.3.0" timelimit="2" steplimit="0" memlimit="0"/>
 <prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="3" steplimit="0" memlimit="0"/>
 <prover id="2" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="3" name="MetiTarski" version="2.4" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../my_cosine.why" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="my_cosine.why"/>
 <theory name="CosineSingle" proved="true">
  <goal name="MethodError" proved="true">
- <proof prover="2" edited="my_cosine_CosineSingle_MethodError_1.v"><result status="valid" time="1.77"/></proof>
+ <proof prover="2" edited="my_cosine_CosineSingle_MethodError_1.v"><result status="valid" time="2.30"/></proof>
  <proof prover="3"><result status="valid" time="0.24"/></proof>
  </goal>
  <goal name="TotalErrorFullyExpanded" proved="true">
diff --git a/examples/logic/my_cosine/why3shapes.gz b/examples/logic/my_cosine/why3shapes.gz
index 5605f1c7f9f989692f8f831c8abcad6cf56f1286..5a5ee536f669fbb639d7a53aba2700328e8e057f 100644
Binary files a/examples/logic/my_cosine/why3shapes.gz and b/examples/logic/my_cosine/why3shapes.gz differ
diff --git a/examples/logic/real/why3session.xml b/examples/logic/real/why3session.xml
index b3ed694fe6a4db368511a1c045e1b9b4e98c07ab..18da5a1851e27e88583c0e5c3471001afd0774de 100644
--- a/examples/logic/real/why3session.xml
+++ b/examples/logic/real/why3session.xml
@@ -1,13 +1,15 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="MetiTarski" version="2.4" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../real.why" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="real.why"/>
 <theory name="CosineSingle" proved="true">
  <goal name="MethodError" proved="true">
- <proof prover="0" edited="real_CosineSingle_MethodError_1.v"><result status="valid" time="1.56"/></proof>
+ <proof prover="0" edited="real_CosineSingle_MethodError_1.v"><result status="valid" time="2.25"/></proof>
  <proof prover="2"><result status="valid" time="0.11"/></proof>
  </goal>
 </theory>
diff --git a/examples/logic/real/why3shapes.gz b/examples/logic/real/why3shapes.gz
index b6fd691761e2b57463455d47655bdf1cf88787ff..f47bd4d41c430207555548e4a33ce36d58b876a4 100644
Binary files a/examples/logic/real/why3shapes.gz and b/examples/logic/real/why3shapes.gz differ
diff --git a/examples/logic/simple/why3session.xml b/examples/logic/simple/why3session.xml
index 41058459313e5b966863e37b6e8306664f40dce6..f8a32e5ed0ce67dfc36683730c1ab60046c6e2ea 100644
--- a/examples/logic/simple/why3session.xml
+++ b/examples/logic/simple/why3session.xml
@@ -1,13 +1,15 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Z3" version="4.6.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="3" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="4" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="4000"/>
 <prover id="5" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../simple.why" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="simple.why"/>
 <theory name="T" proved="true">
  <goal name="g" proved="true">
  <proof prover="1"><result status="valid" time="0.01"/></proof>
diff --git a/examples/logic/simple/why3shapes.gz b/examples/logic/simple/why3shapes.gz
index 2324179042bde9b9a0024f894f4a4f6ccbb0b562..69d708b55598b39831767e8d6f7dc5d560f72d0f 100644
Binary files a/examples/logic/simple/why3shapes.gz and b/examples/logic/simple/why3shapes.gz differ
diff --git a/examples/logic/triangle_inequality/why3session.xml b/examples/logic/triangle_inequality/why3session.xml
index c67ac9a0542cf9c6b5ff0b9fc500e0e5a5fc6aa1..16e7f9f3997c1e44db4e5265ec23e4fa7e75e5c2 100644
--- a/examples/logic/triangle_inequality/why3session.xml
+++ b/examples/logic/triangle_inequality/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
@@ -9,7 +9,9 @@
 <prover id="6" name="Z3" version="3.2" timelimit="3" steplimit="0" memlimit="1000"/>
 <prover id="7" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="8" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../triangle_inequality.why" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="triangle_inequality.why"/>
 <theory name="CauchySchwarzInequality" proved="true">
  <goal name="norm2_pos" proved="true">
  <proof prover="4"><result status="valid" time="0.04"/></proof>
@@ -62,7 +64,7 @@
  </goal>
  <goal name="CauchySchwarz_aux_non_null" proved="true">
  <proof prover="4"><result status="valid" time="0.03"/></proof>
- <proof prover="8" edited="triangle_inequality_CauchySchwarzInequality_CauchySchwarz_aux_non_null_1.v"><result status="valid" time="0.23"/></proof>
+ <proof prover="8" edited="triangle_inequality_CauchySchwarzInequality_CauchySchwarz_aux_non_null_1.v"><result status="valid" time="1.12"/></proof>
  </goal>
  <goal name="norm_null" proved="true">
  <proof prover="4"><result status="valid" time="0.06"/></proof>
@@ -92,7 +94,7 @@
  <proof prover="4"><result status="valid" time="0.07"/></proof>
  </goal>
  <goal name="CauchySchwarz" proved="true">
- <proof prover="8" edited="triangle_inequality_CauchySchwarzInequality_CauchySchwarz_1.v"><result status="valid" time="0.48"/></proof>
+ <proof prover="8" edited="triangle_inequality_CauchySchwarzInequality_CauchySchwarz_1.v"><result status="valid" time="1.21"/></proof>
  </goal>
 </theory>
 <theory name="TriangleInequality" proved="true">
@@ -105,7 +107,7 @@
  <proof prover="4"><result status="valid" time="0.04"/></proof>
  </goal>
  <goal name="triangle" proved="true">
- <proof prover="8" edited="triangle_inequality_TriangleInequality_triangle_1.v"><result status="valid" time="0.40"/></proof>
+ <proof prover="8" edited="triangle_inequality_TriangleInequality_triangle_1.v"><result status="valid" time="1.16"/></proof>
  </goal>
 </theory>
 </file>
diff --git a/examples/logic/triangle_inequality/why3shapes.gz b/examples/logic/triangle_inequality/why3shapes.gz
index 3a7c51401cf5bb60e2a6bc1e7223093b787d8620..e6c668bc77ff18df1434b5edacc6d3b95f6fab4e 100644
Binary files a/examples/logic/triangle_inequality/why3shapes.gz and b/examples/logic/triangle_inequality/why3shapes.gz differ
diff --git a/examples/maximum_subarray/why3session.xml b/examples/maximum_subarray/why3session.xml
index f670c1db770fa817c23a7f658e47ea720d36f499..bedf218099cda9a3c31d4c6645477533bb82b83b 100644
--- a/examples/maximum_subarray/why3session.xml
+++ b/examples/maximum_subarray/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="2" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="4" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="5" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
@@ -220,7 +220,7 @@
   <proof prover="5"><result status="valid" time="0.01" steps="21"/></proof>
   </goal>
   <goal name="VC maximum_subarray.14" expl="loop invariant preservation" proved="true">
-  <proof prover="5" timelimit="120"><result status="valid" time="34.65" steps="23080"/></proof>
+  <proof prover="5" timelimit="120"><result status="valid" time="39.74" steps="23080"/></proof>
   </goal>
   <goal name="VC maximum_subarray.15" expl="loop invariant preservation" proved="true">
   <proof prover="5"><result status="valid" time="0.05" steps="127"/></proof>
diff --git a/examples/maximum_subarray/why3shapes.gz b/examples/maximum_subarray/why3shapes.gz
index 7173d2cd9635e90789ffbc1c91eaa17e7f4c4af5..a8e064bc5c0d06a7f842b34a6df771b529878d6a 100644
Binary files a/examples/maximum_subarray/why3shapes.gz and b/examples/maximum_subarray/why3shapes.gz differ
diff --git a/examples/mccarthy/why3session.xml b/examples/mccarthy/why3session.xml
index b9cbfbcc4e0f757bc337e5790bbf0455cdb04a9e..2bd15a0a864f92720c5371f4ce37bd37af6af0a5 100644
--- a/examples/mccarthy/why3session.xml
+++ b/examples/mccarthy/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="1" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="3" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
 <file proved="true">
diff --git a/examples/mccarthy/why3shapes.gz b/examples/mccarthy/why3shapes.gz
index 112473141f771df03104667826ee15d473dcc26b..9d63490c89634ecafe992a65129090f4db17721a 100644
Binary files a/examples/mccarthy/why3shapes.gz and b/examples/mccarthy/why3shapes.gz differ
diff --git a/examples/mccarthy_vc_sp/why3session.xml b/examples/mccarthy_vc_sp/why3session.xml
index e2980c4051698f43f84263aea99f4c7e61996156..bc545a0359660312136cc67461ebd57ab7ab167f 100644
--- a/examples/mccarthy_vc_sp/why3session.xml
+++ b/examples/mccarthy_vc_sp/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="1" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="3" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="4" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
diff --git a/examples/mccarthy_vc_sp/why3shapes.gz b/examples/mccarthy_vc_sp/why3shapes.gz
index ec4ba20f01eb43239840ab16a18c9bbdc17a6ccb..761b9f5ee0f1606f47e94a61da6de04e6eb1eb4c 100644
Binary files a/examples/mccarthy_vc_sp/why3shapes.gz and b/examples/mccarthy_vc_sp/why3shapes.gz differ
diff --git a/examples/multiprecision/add/why3session.xml b/examples/multiprecision/add/why3session.xml
index e3f6e973a9f53c0d1020f280be71a6815962f0fa..2e46a0192f920b4c4ae16de7bedc4ffb5c2ea103 100644
--- a/examples/multiprecision/add/why3session.xml
+++ b/examples/multiprecision/add/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Eprover" version="1.9.1-001" timelimit="5" steplimit="0" memlimit="2000"/>
 <prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
@@ -1266,7 +1266,7 @@
   <proof prover="5"><result status="valid" time="0.04" steps="56"/></proof>
   </goal>
   <goal name="VC wmpn_incr_1.18" expl="integer overflow" proved="true">
-  <proof prover="3"><result status="valid" time="0.26"/></proof>
+  <proof prover="3"><result status="valid" time="0.32"/></proof>
   </goal>
   <goal name="VC wmpn_incr_1.19" expl="assertion" proved="true">
   <transf name="split_vc" proved="true" >
@@ -1283,7 +1283,7 @@
    <proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="48"/></proof>
    </goal>
    <goal name="VC wmpn_incr_1.19.4" expl="VC for wmpn_incr_1" proved="true">
-   <proof prover="5" timelimit="5"><result status="valid" time="0.18" steps="176"/></proof>
+   <proof prover="5" timelimit="5"><result status="valid" time="0.20" steps="176"/></proof>
    </goal>
   </transf>
   </goal>
@@ -1291,7 +1291,7 @@
   <proof prover="3"><result status="valid" time="0.03"/></proof>
   </goal>
   <goal name="VC wmpn_incr_1.21" expl="loop invariant preservation" proved="true">
-  <proof prover="5"><result status="valid" time="0.06" steps="122"/></proof>
+  <proof prover="5"><result status="valid" time="0.07" steps="122"/></proof>
   </goal>
   <goal name="VC wmpn_incr_1.22" expl="loop invariant preservation" proved="true">
   <proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -1306,10 +1306,10 @@
   <proof prover="5"><result status="valid" time="0.02" steps="51"/></proof>
   </goal>
   <goal name="VC wmpn_incr_1.26" expl="loop invariant preservation" proved="true">
-  <proof prover="5"><result status="valid" time="0.04" steps="67"/></proof>
+  <proof prover="5"><result status="valid" time="0.02" steps="67"/></proof>
   </goal>
   <goal name="VC wmpn_incr_1.27" expl="loop invariant preservation" proved="true">
-  <proof prover="5"><result status="valid" time="0.03" steps="70"/></proof>
+  <proof prover="5"><result status="valid" time="0.07" steps="70"/></proof>
   </goal>
   <goal name="VC wmpn_incr_1.28" expl="assertion" proved="true">
   <proof prover="5"><result status="valid" time="0.02" steps="54"/></proof>
@@ -1339,7 +1339,7 @@
   <proof prover="5"><result status="valid" time="0.03" steps="44"/></proof>
   </goal>
   <goal name="VC wmpn_incr_1.37" expl="integer overflow" proved="true">
-  <proof prover="3"><result status="valid" time="0.32"/></proof>
+  <proof prover="3"><result status="valid" time="0.26"/></proof>
   </goal>
   <goal name="VC wmpn_incr_1.38" expl="assertion" proved="true">
   <transf name="split_vc" proved="true" >
@@ -1364,7 +1364,7 @@
   <proof prover="3"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC wmpn_incr_1.40" expl="loop invariant preservation" proved="true">
-  <proof prover="5"><result status="valid" time="0.07" steps="122"/></proof>
+  <proof prover="5"><result status="valid" time="0.06" steps="122"/></proof>
   </goal>
   <goal name="VC wmpn_incr_1.41" expl="loop invariant preservation" proved="true">
   <proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -1379,10 +1379,10 @@
   <proof prover="5"><result status="valid" time="0.05" steps="51"/></proof>
   </goal>
   <goal name="VC wmpn_incr_1.45" expl="loop invariant preservation" proved="true">
-  <proof prover="5"><result status="valid" time="0.02" steps="67"/></proof>
+  <proof prover="5"><result status="valid" time="0.04" steps="67"/></proof>
   </goal>
   <goal name="VC wmpn_incr_1.46" expl="loop invariant preservation" proved="true">
-  <proof prover="5"><result status="valid" time="0.07" steps="70"/></proof>
+  <proof prover="5"><result status="valid" time="0.03" steps="70"/></proof>
   </goal>
   <goal name="VC wmpn_incr_1.47" expl="precondition" proved="true">
   <proof prover="3"><result status="valid" time="0.02"/></proof>
diff --git a/examples/multiprecision/add/why3shapes.gz b/examples/multiprecision/add/why3shapes.gz
index 1eaf1b60ca0ebccd3d37418165e0b31b2df4567b..9b9a5259d01f7d589bca3a3d78f1bf92c0399fc1 100644
Binary files a/examples/multiprecision/add/why3shapes.gz and b/examples/multiprecision/add/why3shapes.gz differ
diff --git a/examples/multiprecision/compare/why3session.xml b/examples/multiprecision/compare/why3session.xml
index 501a5edbc1fc70244a79cfeff8871867e4180edc..181803b220e5ff6e1f93752fa5b4e9107f338608 100644
--- a/examples/multiprecision/compare/why3session.xml
+++ b/examples/multiprecision/compare/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="3" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
diff --git a/examples/multiprecision/compare/why3shapes.gz b/examples/multiprecision/compare/why3shapes.gz
index 8c4906a0fae065e807db83f3bfd3e65a33cd7b8f..43e8a619cba04d5d75e0b3b657091bc6ec0b9a99 100644
Binary files a/examples/multiprecision/compare/why3shapes.gz and b/examples/multiprecision/compare/why3shapes.gz differ
diff --git a/examples/multiprecision/div/why3session.xml b/examples/multiprecision/div/why3session.xml
index b22dd2d4e4eb1101dc6e6f7fad7c4bc670255ff4..7a6fb60e5e3c0fe0c50432639ce07ceb8f2b7202 100644
--- a/examples/multiprecision/div/why3session.xml
+++ b/examples/multiprecision/div/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Eprover" version="1.9.1-001" timelimit="5" steplimit="0" memlimit="2000"/>
 <prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="2000"/>
 <prover id="2" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
@@ -442,7 +442,7 @@
   <proof prover="3"><result status="valid" time="0.03"/></proof>
   </goal>
   <goal name="VC div2by1_inv.21" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="3.22"/></proof>
+  <proof prover="0"><result status="valid" time="2.43"/></proof>
   </goal>
   <goal name="VC div2by1_inv.22" expl="assertion" proved="true">
   <transf name="split_goal_right" proved="true" >
@@ -1016,7 +1016,7 @@
    <proof prover="0" timelimit="10"><result status="valid" time="0.02"/></proof>
    </goal>
    <goal name="VC wmpn_divrem_1.38.2" expl="VC for wmpn_divrem_1" proved="true">
-   <proof prover="0" timelimit="10"><result status="valid" time="5.09"/></proof>
+   <proof prover="0" timelimit="10"><result status="valid" time="4.04"/></proof>
    </goal>
   </transf>
   </goal>
@@ -1041,7 +1041,7 @@
   <proof prover="3"><result status="valid" time="0.08"/></proof>
   </goal>
   <goal name="VC wmpn_divrem_1.44" expl="loop invariant preservation" proved="true">
-  <proof prover="0" timelimit="10"><result status="valid" time="4.23"/></proof>
+  <proof prover="0" timelimit="10"><result status="valid" time="3.34"/></proof>
   </goal>
   <goal name="VC wmpn_divrem_1.45" expl="loop invariant preservation" proved="true">
   <proof prover="3"><result status="valid" time="0.03"/></proof>
@@ -1130,7 +1130,7 @@
    <proof prover="0"><result status="valid" time="0.03"/></proof>
    </goal>
    <goal name="VC wmpn_divrem_1.71.2" expl="VC for wmpn_divrem_1" proved="true">
-   <proof prover="0"><result status="valid" time="3.34"/></proof>
+   <proof prover="0"><result status="valid" time="2.60"/></proof>
    </goal>
    <goal name="VC wmpn_divrem_1.71.3" expl="VC for wmpn_divrem_1" proved="true">
    <proof prover="2"><result status="valid" time="0.07"/></proof>
@@ -1148,7 +1148,7 @@
    <proof prover="3"><result status="valid" time="0.02"/></proof>
    </goal>
    <goal name="VC wmpn_divrem_1.71.8" expl="VC for wmpn_divrem_1" proved="true">
-   <proof prover="0"><result status="valid" time="3.20"/></proof>
+   <proof prover="0"><result status="valid" time="2.45"/></proof>
    </goal>
    <goal name="VC wmpn_divrem_1.71.9" expl="VC for wmpn_divrem_1" proved="true">
    <proof prover="0"><result status="valid" time="0.02"/></proof>
@@ -1309,7 +1309,7 @@
    <proof prover="2"><result status="valid" time="0.10"/></proof>
    </goal>
    <goal name="VC div3by2_inv.14.2" expl="VC for div3by2_inv" proved="true">
-   <proof prover="0"><result status="valid" time="4.07"/></proof>
+   <proof prover="0"><result status="valid" time="3.32"/></proof>
    </goal>
    <goal name="VC div3by2_inv.14.3" expl="VC for div3by2_inv" proved="true">
    <proof prover="2"><result status="valid" time="0.06"/></proof>
@@ -1318,7 +1318,7 @@
    <proof prover="2"><result status="valid" time="0.08"/></proof>
    </goal>
    <goal name="VC div3by2_inv.14.5" expl="VC for div3by2_inv" proved="true">
-   <proof prover="0" timelimit="20"><result status="valid" time="22.29"/></proof>
+   <proof prover="0" timelimit="20"><result status="valid" time="17.83"/></proof>
    <proof prover="1" timelimit="20"><result status="valid" time="15.29"/></proof>
    </goal>
    <goal name="VC div3by2_inv.14.6" expl="VC for div3by2_inv" proved="true">
@@ -1476,7 +1476,7 @@
    <proof prover="2"><result status="valid" time="0.13"/></proof>
    </goal>
    <goal name="VC div3by2_inv.15.38" expl="VC for div3by2_inv" proved="true">
-   <proof prover="0"><result status="valid" time="4.57"/></proof>
+   <proof prover="0"><result status="valid" time="3.73"/></proof>
    </goal>
    <goal name="VC div3by2_inv.15.39" expl="VC for div3by2_inv" proved="true">
    <proof prover="2"><result status="valid" time="0.03"/></proof>
@@ -1544,7 +1544,7 @@
    <proof prover="2"><result status="valid" time="0.27"/></proof>
    </goal>
    <goal name="VC div3by2_inv.15.57" expl="VC for div3by2_inv" proved="true">
-   <proof prover="0"><result status="valid" time="1.39"/></proof>
+   <proof prover="0"><result status="valid" time="1.04"/></proof>
    </goal>
    <goal name="VC div3by2_inv.15.58" expl="VC for div3by2_inv" proved="true">
    <proof prover="2"><result status="valid" time="0.04"/></proof>
@@ -1565,7 +1565,7 @@
    <proof prover="2"><result status="valid" time="0.11"/></proof>
    </goal>
    <goal name="VC div3by2_inv.15.64" expl="VC for div3by2_inv" proved="true">
-   <proof prover="0"><result status="valid" time="2.01"/></proof>
+   <proof prover="0"><result status="valid" time="1.68"/></proof>
    </goal>
    <goal name="VC div3by2_inv.15.65" expl="VC for div3by2_inv" proved="true">
    <proof prover="2"><result status="valid" time="0.03"/></proof>
@@ -2991,7 +2991,7 @@
   <goal name="VC submul_limb.19" expl="assertion" proved="true">
   <transf name="split_goal_right" proved="true" >
    <goal name="VC submul_limb.19.0" expl="VC for submul_limb" proved="true">
-   <proof prover="0" timelimit="10"><result status="valid" time="2.03"/></proof>
+   <proof prover="0" timelimit="10"><result status="valid" time="1.56"/></proof>
    </goal>
    <goal name="VC submul_limb.19.1" expl="VC for submul_limb" proved="true">
    <proof prover="0"><result status="valid" time="0.06"/></proof>
@@ -3046,7 +3046,7 @@
    <proof prover="3"><result status="valid" time="0.02"/></proof>
    </goal>
    <goal name="VC submul_limb.19.14" expl="VC for submul_limb" proved="true">
-   <proof prover="0"><result status="valid" time="0.60"/></proof>
+   <proof prover="0"><result status="valid" time="0.42"/></proof>
    </goal>
    <goal name="VC submul_limb.19.15" expl="VC for submul_limb" proved="true">
    <proof prover="0"><result status="valid" time="0.08"/></proof>
@@ -3326,7 +3326,7 @@
    <proof prover="2" timelimit="5"><result status="valid" time="0.14"/></proof>
    </goal>
    <goal name="VC div_sb_qr.39.8" expl="VC for div_sb_qr" proved="true">
-   <proof prover="1"><result status="valid" time="3.70"/></proof>
+   <proof prover="1"><result status="valid" time="3.13"/></proof>
    </goal>
    <goal name="VC div_sb_qr.39.9" expl="VC for div_sb_qr" proved="true">
    <proof prover="1"><result status="valid" time="2.58"/></proof>
@@ -3598,10 +3598,10 @@
   <goal name="VC div_sb_qr.74" expl="assertion" proved="true">
   <transf name="split_goal_right" proved="true" >
    <goal name="VC div_sb_qr.74.0" expl="assertion" proved="true">
-   <proof prover="1" memlimit="1000"><result status="valid" time="0.17"/></proof>
+   <proof prover="1" memlimit="1000"><result status="valid" time="0.09"/></proof>
    </goal>
    <goal name="VC div_sb_qr.74.1" expl="assertion" proved="true">
-   <proof prover="1" memlimit="1000"><result status="valid" time="0.09"/></proof>
+   <proof prover="1" memlimit="1000"><result status="valid" time="0.17"/></proof>
    </goal>
   </transf>
   </goal>
@@ -3609,7 +3609,7 @@
   <proof prover="2" timelimit="5"><result status="valid" time="0.24"/></proof>
   </goal>
   <goal name="VC div_sb_qr.76" expl="precondition" proved="true">
-  <proof prover="2" timelimit="5" memlimit="2000"><result status="valid" time="2.80"/></proof>
+  <proof prover="2" timelimit="5" memlimit="2000"><result status="valid" time="2.17"/></proof>
   </goal>
   <goal name="VC div_sb_qr.77" expl="precondition" proved="true">
   <proof prover="0" memlimit="1000"><result status="valid" time="0.02"/></proof>
@@ -3940,7 +3940,7 @@
    <proof prover="0"><result status="valid" time="0.04"/></proof>
    </goal>
    <goal name="VC div_sb_qr.96.7" expl="VC for div_sb_qr" proved="true">
-   <proof prover="0"><result status="valid" time="1.69"/></proof>
+   <proof prover="0"><result status="valid" time="1.26"/></proof>
    </goal>
    <goal name="VC div_sb_qr.96.8" expl="VC for div_sb_qr" proved="true">
    <proof prover="1"><result status="valid" time="0.12"/></proof>
@@ -3985,7 +3985,7 @@
    <proof prover="2"><result status="valid" time="0.20"/></proof>
    </goal>
    <goal name="VC div_sb_qr.96.22" expl="VC for div_sb_qr" proved="true">
-   <proof prover="0"><result status="valid" time="5.24"/></proof>
+   <proof prover="0"><result status="valid" time="3.93"/></proof>
    </goal>
    <goal name="VC div_sb_qr.96.23" expl="VC for div_sb_qr" proved="true">
    <proof prover="0" memlimit="1000"><result status="valid" time="0.02"/></proof>
@@ -4021,7 +4021,7 @@
    <proof prover="0"><result status="valid" time="0.05"/></proof>
    </goal>
    <goal name="VC div_sb_qr.96.34" expl="VC for div_sb_qr" proved="true">
-   <proof prover="0" memlimit="1000"><result status="valid" time="1.04"/></proof>
+   <proof prover="0" memlimit="1000"><result status="valid" time="0.79"/></proof>
    </goal>
    <goal name="VC div_sb_qr.96.35" expl="VC for div_sb_qr" proved="true">
    <proof prover="0"><result status="valid" time="0.26"/></proof>
@@ -4271,7 +4271,7 @@
   </transf>
   </goal>
   <goal name="VC div_sb_qr.117" expl="precondition" proved="true">
-  <proof prover="3"><result status="valid" time="2.46"/></proof>
+  <proof prover="3"><result status="valid" time="2.05"/></proof>
   </goal>
   <goal name="VC div_sb_qr.118" expl="precondition" proved="true">
   <proof prover="2" timelimit="5"><result status="valid" time="0.24"/></proof>
@@ -4335,7 +4335,7 @@
   <proof prover="2" timelimit="5" memlimit="2000"><result status="valid" time="0.23"/></proof>
   </goal>
   <goal name="VC div_sb_qr.128" expl="precondition" proved="true">
-  <proof prover="2" timelimit="5" memlimit="2000"><result status="valid" time="2.68"/></proof>
+  <proof prover="2" timelimit="5" memlimit="2000"><result status="valid" time="2.20"/></proof>
   </goal>
   <goal name="VC div_sb_qr.129" expl="integer overflow" proved="true">
   <proof prover="3"><result status="valid" time="0.05"/></proof>
@@ -4417,7 +4417,7 @@
    <proof prover="0"><result status="valid" time="0.04"/></proof>
    </goal>
    <goal name="VC div_sb_qr.147.2" expl="VC for div_sb_qr" proved="true">
-   <proof prover="0"><result status="valid" time="3.27"/></proof>
+   <proof prover="0"><result status="valid" time="2.54"/></proof>
    </goal>
    <goal name="VC div_sb_qr.147.3" expl="VC for div_sb_qr" proved="true">
    <proof prover="1"><result status="valid" time="1.81"/></proof>
@@ -4462,7 +4462,7 @@
     <goal name="VC div_sb_qr.153.0.0" expl="postcondition" proved="true">
     <transf name="reflection_f" proved="true" arg1="mp_decision">
      <goal name="VC div_sb_qr.153.0.0.0" expl="postcondition" proved="true">
-     <proof prover="0"><result status="valid" time="3.34"/></proof>
+     <proof prover="0"><result status="valid" time="2.33"/></proof>
      </goal>
      <goal name="VC div_sb_qr.153.0.0.1" proved="true">
      <proof prover="2"><result status="valid" time="0.28"/></proof>
@@ -4547,46 +4547,46 @@
      <proof prover="9"><result status="valid" time="0.58"/></proof>
      </goal>
      <goal name="VC div_sb_qr.156.13.0.1" expl="VC for div_sb_qr" proved="true">
-     <proof prover="9"><result status="valid" time="0.59"/></proof>
+     <proof prover="9"><result status="valid" time="0.57"/></proof>
      </goal>
      <goal name="VC div_sb_qr.156.13.0.2" expl="VC for div_sb_qr" proved="true">
-     <proof prover="9"><result status="valid" time="0.57"/></proof>
+     <proof prover="9"><result status="valid" time="0.60"/></proof>
      </goal>
      <goal name="VC div_sb_qr.156.13.0.3" expl="VC for div_sb_qr" proved="true">
-     <proof prover="9"><result status="valid" time="0.57"/></proof>
+     <proof prover="9"><result status="valid" time="0.54"/></proof>
      </goal>
      <goal name="VC div_sb_qr.156.13.0.4" expl="VC for div_sb_qr" proved="true">
      <proof prover="9"><result status="valid" time="0.59"/></proof>
      </goal>
      <goal name="VC div_sb_qr.156.13.0.5" expl="VC for div_sb_qr" proved="true">
-     <proof prover="9"><result status="valid" time="0.59"/></proof>
+     <proof prover="9"><result status="valid" time="0.58"/></proof>
      </goal>
      <goal name="VC div_sb_qr.156.13.0.6" expl="VC for div_sb_qr" proved="true">
-     <proof prover="9"><result status="valid" time="0.58"/></proof>
+     <proof prover="9"><result status="valid" time="0.59"/></proof>
      </goal>
      <goal name="VC div_sb_qr.156.13.0.7" expl="VC for div_sb_qr" proved="true">
-     <proof prover="9"><result status="valid" time="0.61"/></proof>
+     <proof prover="9"><result status="valid" time="0.59"/></proof>
      </goal>
      <goal name="VC div_sb_qr.156.13.0.8" expl="VC for div_sb_qr" proved="true">
-     <proof prover="9"><result status="valid" time="0.58"/></proof>
+     <proof prover="9"><result status="valid" time="0.61"/></proof>
      </goal>
      <goal name="VC div_sb_qr.156.13.0.9" expl="VC for div_sb_qr" proved="true">
-     <proof prover="9"><result status="valid" time="0.56"/></proof>
+     <proof prover="9"><result status="valid" time="0.57"/></proof>
      </goal>
      <goal name="VC div_sb_qr.156.13.0.10" expl="VC for div_sb_qr" proved="true">
-     <proof prover="9"><result status="valid" time="0.61"/></proof>
+     <proof prover="9"><result status="valid" time="0.56"/></proof>
      </goal>
      <goal name="VC div_sb_qr.156.13.0.11" expl="VC for div_sb_qr" proved="true">
      <proof prover="9"><result status="valid" time="0.57"/></proof>
      </goal>
      <goal name="VC div_sb_qr.156.13.0.12" expl="VC for div_sb_qr" proved="true">
-     <proof prover="9"><result status="valid" time="0.60"/></proof>
+     <proof prover="9"><result status="valid" time="0.57"/></proof>
      </goal>
      <goal name="VC div_sb_qr.156.13.0.13" expl="VC for div_sb_qr" proved="true">
-     <proof prover="9"><result status="valid" time="0.57"/></proof>
+     <proof prover="9"><result status="valid" time="0.61"/></proof>
      </goal>
      <goal name="VC div_sb_qr.156.13.0.14" expl="VC for div_sb_qr" proved="true">
-     <proof prover="9"><result status="valid" time="0.54"/></proof>
+     <proof prover="9"><result status="valid" time="0.58"/></proof>
      </goal>
      <goal name="VC div_sb_qr.156.13.0.15" expl="VC for div_sb_qr" proved="true">
      <proof prover="9"><result status="valid" time="0.57"/></proof>
@@ -4777,7 +4777,7 @@
       <proof prover="3"><result status="valid" time="0.02"/></proof>
       </goal>
       <goal name="VC div_sb_qr.157.0.0.0.56" expl="apply premises" proved="true">
-      <proof prover="3"><result status="valid" time="0.02"/></proof>
+      <proof prover="2"><result status="valid" time="0.21"/></proof>
       </goal>
       <goal name="VC div_sb_qr.157.0.0.0.57" expl="apply premises" proved="true">
       <proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -4789,7 +4789,7 @@
       <proof prover="3"><result status="valid" time="0.04"/></proof>
       </goal>
       <goal name="VC div_sb_qr.157.0.0.0.60" expl="apply premises" proved="true">
-      <proof prover="3"><result status="valid" time="0.02"/></proof>
+      <proof prover="3"><result status="valid" time="0.04"/></proof>
       </goal>
       <goal name="VC div_sb_qr.157.0.0.0.61" expl="apply premises" proved="true">
       <proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -4906,7 +4906,7 @@
       <proof prover="3"><result status="valid" time="0.02"/></proof>
       </goal>
       <goal name="VC div_sb_qr.157.0.0.0.99" expl="apply premises" proved="true">
-      <proof prover="3"><result status="valid" time="0.02"/></proof>
+      <proof prover="3"><result status="valid" time="0.04"/></proof>
       </goal>
       <goal name="VC div_sb_qr.157.0.0.0.100" expl="apply premises" proved="true">
       <proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -4951,13 +4951,13 @@
       <proof prover="3"><result status="valid" time="0.02"/></proof>
       </goal>
       <goal name="VC div_sb_qr.157.0.0.0.114" expl="apply premises" proved="true">
-      <proof prover="3"><result status="valid" time="0.02"/></proof>
+      <proof prover="3"><result status="valid" time="0.03"/></proof>
       </goal>
       <goal name="VC div_sb_qr.157.0.0.0.115" expl="apply premises" proved="true">
-      <proof prover="3"><result status="valid" time="0.04"/></proof>
+      <proof prover="3"><result status="valid" time="0.02"/></proof>
       </goal>
       <goal name="VC div_sb_qr.157.0.0.0.116" expl="apply premises" proved="true">
-      <proof prover="2"><result status="valid" time="0.21"/></proof>
+      <proof prover="3"><result status="valid" time="0.02"/></proof>
       </goal>
       <goal name="VC div_sb_qr.157.0.0.0.117" expl="apply premises" proved="true">
       <proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -4984,7 +4984,7 @@
       <proof prover="3"><result status="valid" time="0.18"/></proof>
       </goal>
       <goal name="VC div_sb_qr.157.0.0.0.125" expl="apply premises" proved="true">
-      <proof prover="3"><result status="valid" time="0.02"/></proof>
+      <proof prover="3"><result status="valid" time="0.04"/></proof>
       </goal>
       <goal name="VC div_sb_qr.157.0.0.0.126" expl="apply premises" proved="true">
       <proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -5011,7 +5011,7 @@
       <proof prover="3"><result status="valid" time="0.02"/></proof>
       </goal>
       <goal name="VC div_sb_qr.157.0.0.0.134" expl="apply premises" proved="true">
-      <proof prover="3"><result status="valid" time="0.03"/></proof>
+      <proof prover="3"><result status="valid" time="0.02"/></proof>
       </goal>
       <goal name="VC div_sb_qr.157.0.0.0.135" expl="apply premises" proved="true">
       <proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -5029,7 +5029,7 @@
       <proof prover="3"><result status="valid" time="0.02"/></proof>
       </goal>
       <goal name="VC div_sb_qr.157.0.0.0.140" expl="apply premises" proved="true">
-      <proof prover="3"><result status="valid" time="0.03"/></proof>
+      <proof prover="3"><result status="valid" time="0.02"/></proof>
       </goal>
       <goal name="VC div_sb_qr.157.0.0.0.141" expl="apply premises" proved="true">
       <proof prover="3"><result status="valid" time="0.04"/></proof>
@@ -5071,10 +5071,10 @@
       <proof prover="3"><result status="valid" time="0.02"/></proof>
       </goal>
       <goal name="VC div_sb_qr.157.0.0.0.154" expl="apply premises" proved="true">
-      <proof prover="3"><result status="valid" time="0.04"/></proof>
+      <proof prover="3"><result status="valid" time="0.02"/></proof>
       </goal>
       <goal name="VC div_sb_qr.157.0.0.0.155" expl="apply premises" proved="true">
-      <proof prover="3"><result status="valid" time="0.04"/></proof>
+      <proof prover="3"><result status="valid" time="0.03"/></proof>
       </goal>
       <goal name="VC div_sb_qr.157.0.0.0.156" expl="apply premises" proved="true">
       <proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -5279,7 +5279,7 @@
    <proof prover="3"><result status="valid" time="0.04"/></proof>
    </goal>
    <goal name="VC div_sb_qr.162.15" expl="VC for div_sb_qr" proved="true">
-   <proof prover="0"><result status="valid" time="8.24"/></proof>
+   <proof prover="0"><result status="valid" time="6.33"/></proof>
    </goal>
    <goal name="VC div_sb_qr.162.16" expl="VC for div_sb_qr" proved="true">
    <proof prover="3"><result status="valid" time="0.04"/></proof>
@@ -5368,7 +5368,7 @@
    <proof prover="3"><result status="valid" time="0.11"/></proof>
    </goal>
    <goal name="VC div_sb_qr.168.14" expl="VC for div_sb_qr" proved="true">
-   <proof prover="0"><result status="valid" time="6.95"/></proof>
+   <proof prover="0"><result status="valid" time="5.23"/></proof>
    </goal>
    <goal name="VC div_sb_qr.168.15" expl="VC for div_sb_qr" proved="true">
    <proof prover="1"><result status="valid" time="0.22"/></proof>
@@ -5469,7 +5469,7 @@
   <proof prover="2" timelimit="5"><result status="valid" time="1.38"/></proof>
   </goal>
   <goal name="VC div_sb_qr.177" expl="assertion" proved="true">
-  <proof prover="2" timelimit="5"><result status="valid" time="2.76"/></proof>
+  <proof prover="2" timelimit="5"><result status="valid" time="2.29"/></proof>
   </goal>
   <goal name="VC div_sb_qr.178" expl="precondition" proved="true">
   <proof prover="2" timelimit="5" memlimit="2000"><result status="valid" time="0.52"/></proof>
@@ -5667,7 +5667,7 @@
    </transf>
    </goal>
    <goal name="VC div_sb_qr.196.10" expl="VC for div_sb_qr" proved="true">
-   <proof prover="0" timelimit="20" memlimit="1000"><result status="valid" time="10.04"/></proof>
+   <proof prover="0" timelimit="20" memlimit="1000"><result status="valid" time="7.91"/></proof>
    </goal>
    <goal name="VC div_sb_qr.196.11" expl="VC for div_sb_qr" proved="true">
    <proof prover="0"><result status="valid" time="0.03"/></proof>
@@ -5780,7 +5780,7 @@
    <proof prover="2"><result status="valid" time="0.44"/></proof>
    </goal>
    <goal name="VC div_sb_qr.196.45" expl="VC for div_sb_qr" proved="true">
-   <proof prover="0"><result status="valid" time="1.09"/></proof>
+   <proof prover="0"><result status="valid" time="0.82"/></proof>
    </goal>
    <goal name="VC div_sb_qr.196.46" expl="VC for div_sb_qr" proved="true">
    <proof prover="0"><result status="valid" time="0.40"/></proof>
@@ -5980,29 +5980,29 @@
   <goal name="VC div_sb_qr.219" expl="assertion" proved="true">
   <transf name="split_goal_right" proved="true" >
    <goal name="VC div_sb_qr.219.0" expl="assertion" proved="true">
-   <transf name="split_vc" proved="true" >
-    <goal name="VC div_sb_qr.219.0.0" expl="assertion" proved="true">
-    <proof prover="0"><result status="valid" time="0.02"/></proof>
-    </goal>
-    <goal name="VC div_sb_qr.219.0.1" expl="assertion" proved="true">
-    <proof prover="0"><result status="valid" time="0.02"/></proof>
-    </goal>
-   </transf>
-   </goal>
-   <goal name="VC div_sb_qr.219.1" expl="assertion" proved="true">
    <transf name="introduce_premises" proved="true" >
-    <goal name="VC div_sb_qr.219.1.0" expl="assertion" proved="true">
+    <goal name="VC div_sb_qr.219.0.0" expl="assertion" proved="true">
     <transf name="replace" proved="true" arg1="(value qp ((int32&#39;int sx - int32&#39;int sy) - int32&#39;int i))" arg2="(uint64&#39;int ql+ radix2 *value_sub (pelts q) (offset qp + 1) (((offset qp + int32&#39;int sx) - int32&#39;int sy) - int32&#39;int i))">
-     <goal name="VC div_sb_qr.219.1.0.0" expl="assertion" proved="true">
+     <goal name="VC div_sb_qr.219.0.0.0" expl="assertion" proved="true">
      <proof prover="3" memlimit="2000"><result status="valid" time="0.01"/></proof>
      </goal>
-     <goal name="VC div_sb_qr.219.1.0.1" expl="equality hypothesis" proved="true">
-     <proof prover="0"><result status="valid" time="0.78"/></proof>
+     <goal name="VC div_sb_qr.219.0.0.1" expl="equality hypothesis" proved="true">
+     <proof prover="0"><result status="valid" time="0.01"/></proof>
      </goal>
     </transf>
     </goal>
    </transf>
    </goal>
+   <goal name="VC div_sb_qr.219.1" expl="assertion" proved="true">
+   <transf name="split_vc" proved="true" >
+    <goal name="VC div_sb_qr.219.1.0" expl="assertion" proved="true">
+    <proof prover="0"><result status="valid" time="1.78"/></proof>
+    </goal>
+    <goal name="VC div_sb_qr.219.1.1" expl="assertion" proved="true">
+    <proof prover="0"><result status="valid" time="1.92"/></proof>
+    </goal>
+   </transf>
+   </goal>
   </transf>
   </goal>
   <goal name="VC div_sb_qr.220" expl="assertion" proved="true">
@@ -6075,10 +6075,10 @@
   <goal name="VC div_sb_qr.230" expl="assertion" proved="true">
   <transf name="split_goal_right" proved="true" >
    <goal name="VC div_sb_qr.230.0" expl="assertion" proved="true">
-   <proof prover="0"><result status="valid" time="0.03"/></proof>
+   <proof prover="0"><result status="valid" time="0.04"/></proof>
    </goal>
    <goal name="VC div_sb_qr.230.1" expl="assertion" proved="true">
-   <proof prover="0"><result status="valid" time="0.04"/></proof>
+   <proof prover="0"><result status="valid" time="0.03"/></proof>
    </goal>
   </transf>
   </goal>
@@ -6093,7 +6093,7 @@
   </transf>
   </goal>
   <goal name="VC div_sb_qr.232" expl="assertion" proved="true">
-  <proof prover="1" timelimit="20"><result status="valid" time="8.59"/></proof>
+  <proof prover="1" timelimit="20"><result status="valid" time="7.02"/></proof>
   </goal>
   <goal name="VC div_sb_qr.233" expl="assertion" proved="true">
   <transf name="introduce_premises" proved="true" >
@@ -6154,7 +6154,7 @@
        <proof prover="2"><result status="valid" time="0.21"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.15" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.24"/></proof>
+       <proof prover="2"><result status="valid" time="0.23"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.16" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.31"/></proof>
@@ -6163,7 +6163,7 @@
        <proof prover="2"><result status="valid" time="0.18"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.18" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.21"/></proof>
+       <proof prover="2"><result status="valid" time="0.24"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.19" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.18"/></proof>
@@ -6277,13 +6277,13 @@
        <proof prover="2"><result status="valid" time="0.23"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.56" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.23"/></proof>
+       <proof prover="2"><result status="valid" time="0.24"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.57" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.28"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.58" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.22"/></proof>
+       <proof prover="2"><result status="valid" time="0.24"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.59" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.21"/></proof>
@@ -6292,25 +6292,25 @@
        <proof prover="2"><result status="valid" time="0.19"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.61" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.24"/></proof>
+       <proof prover="2"><result status="valid" time="0.20"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.62" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.18"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.63" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.26"/></proof>
+       <proof prover="2"><result status="valid" time="0.21"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.64" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.18"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.65" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.24"/></proof>
+       <proof prover="2"><result status="valid" time="0.19"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.66" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.19"/></proof>
+       <proof prover="2"><result status="valid" time="0.18"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.67" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.23"/></proof>
+       <proof prover="2"><result status="valid" time="0.24"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.68" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.18"/></proof>
@@ -6406,10 +6406,10 @@
        <proof prover="2"><result status="valid" time="0.18"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.99" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.18"/></proof>
+       <proof prover="2"><result status="valid" time="0.19"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.100" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.18"/></proof>
+       <proof prover="2"><result status="valid" time="0.19"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.101" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.23"/></proof>
@@ -6421,7 +6421,7 @@
        <proof prover="2"><result status="valid" time="0.24"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.104" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.19"/></proof>
+       <proof prover="2"><result status="valid" time="0.18"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.105" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.24"/></proof>
@@ -6430,7 +6430,7 @@
        <proof prover="2"><result status="valid" time="0.18"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.107" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.19"/></proof>
+       <proof prover="2"><result status="valid" time="0.18"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.108" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.20"/></proof>
@@ -6439,31 +6439,31 @@
        <proof prover="2"><result status="valid" time="0.23"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.110" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.24"/></proof>
+       <proof prover="2"><result status="valid" time="0.25"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.111" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.18"/></proof>
+       <proof prover="2"><result status="valid" time="0.23"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.112" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.18"/></proof>
+       <proof prover="2"><result status="valid" time="0.20"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.113" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.17"/></proof>
+       <proof prover="2"><result status="valid" time="0.20"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.114" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.22"/></proof>
+       <proof prover="2"><result status="valid" time="0.18"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.115" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.23"/></proof>
+       <proof prover="2"><result status="valid" time="0.19"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.116" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.20"/></proof>
+       <proof prover="2"><result status="valid" time="0.24"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.117" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.23"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.118" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.24"/></proof>
+       <proof prover="2"><result status="valid" time="0.22"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.119" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.20"/></proof>
@@ -6484,13 +6484,13 @@
        <proof prover="2"><result status="valid" time="0.26"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.125" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.19"/></proof>
+       <proof prover="2"><result status="valid" time="0.20"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.126" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.22"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.127" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.19"/></proof>
+       <proof prover="2"><result status="valid" time="0.17"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.128" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.24"/></proof>
@@ -6499,10 +6499,10 @@
        <proof prover="2"><result status="valid" time="0.23"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.130" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.24"/></proof>
+       <proof prover="2"><result status="valid" time="0.22"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.131" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.23"/></proof>
+       <proof prover="2"><result status="valid" time="0.19"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.132" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.17"/></proof>
@@ -6511,28 +6511,28 @@
        <proof prover="2"><result status="valid" time="0.23"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.134" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.24"/></proof>
+       <proof prover="2"><result status="valid" time="0.22"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.135" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.17"/></proof>
+       <proof prover="2"><result status="valid" time="0.23"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.136" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.17"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.137" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.23"/></proof>
+       <proof prover="2"><result status="valid" time="0.24"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.138" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.20"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.139" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.20"/></proof>
+       <proof prover="2"><result status="valid" time="0.18"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.140" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.18"/></proof>
+       <proof prover="2"><result status="valid" time="0.23"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.141" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.18"/></proof>
+       <proof prover="2"><result status="valid" time="0.19"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.142" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.23"/></proof>
@@ -6541,40 +6541,40 @@
        <proof prover="2"><result status="valid" time="0.17"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.144" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.25"/></proof>
+       <proof prover="2"><result status="valid" time="0.24"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.145" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.24"/></proof>
+       <proof prover="2"><result status="valid" time="0.18"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.146" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.20"/></proof>
+       <proof prover="2"><result status="valid" time="0.18"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.147" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.18"/></proof>
+       <proof prover="2"><result status="valid" time="0.17"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.148" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.23"/></proof>
+       <proof prover="2"><result status="valid" time="0.22"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.149" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.19"/></proof>
+       <proof prover="2"><result status="valid" time="0.23"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.150" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.24"/></proof>
+       <proof prover="2"><result status="valid" time="0.23"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.151" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.18"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.152" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.21"/></proof>
+       <proof prover="2"><result status="valid" time="0.26"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.153" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.24"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.154" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.20"/></proof>
+       <proof prover="2"><result status="valid" time="0.19"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.155" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.22"/></proof>
+       <proof prover="2"><result status="valid" time="0.18"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.156" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.18"/></proof>
@@ -6595,13 +6595,13 @@
        <proof prover="2"><result status="valid" time="0.19"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.162" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.28"/></proof>
+       <proof prover="2"><result status="valid" time="0.16"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.163" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.20"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.164" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.18"/></proof>
+       <proof prover="2"><result status="valid" time="0.27"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.165" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.17"/></proof>
@@ -6634,19 +6634,19 @@
        <proof prover="2"><result status="valid" time="0.19"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.175" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.19"/></proof>
+       <proof prover="2"><result status="valid" time="0.24"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.176" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.18"/></proof>
+       <proof prover="2"><result status="valid" time="0.19"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.177" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.24"/></proof>
+       <proof prover="2"><result status="valid" time="0.23"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.178" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.30"/></proof>
+       <proof prover="2"><result status="valid" time="0.28"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.179" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.27"/></proof>
+       <proof prover="2"><result status="valid" time="0.18"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.180" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.22"/></proof>
@@ -6670,10 +6670,10 @@
        <proof prover="2"><result status="valid" time="0.22"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.187" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.19"/></proof>
+       <proof prover="2"><result status="valid" time="0.24"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.188" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.22"/></proof>
+       <proof prover="2"><result status="valid" time="0.24"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.189" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.18"/></proof>
@@ -6688,10 +6688,10 @@
        <proof prover="2"><result status="valid" time="0.20"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.193" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.18"/></proof>
+       <proof prover="2"><result status="valid" time="0.24"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.194" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.24"/></proof>
+       <proof prover="2"><result status="valid" time="0.18"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.195" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.20"/></proof>
@@ -6703,7 +6703,7 @@
        <proof prover="2"><result status="valid" time="0.19"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.198" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.23"/></proof>
+       <proof prover="2"><result status="valid" time="0.21"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.199" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.18"/></proof>
@@ -6730,7 +6730,7 @@
        <proof prover="2"><result status="valid" time="0.24"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.207" expl="apply premises" proved="true">
-       <proof prover="2"><result status="valid" time="0.31"/></proof>
+       <proof prover="2"><result status="valid" time="0.17"/></proof>
        </goal>
        <goal name="VC div_sb_qr.233.0.0.1.0.208" expl="apply premises" proved="true">
        <proof prover="2"><result status="valid" time="0.20"/></proof>
@@ -7094,7 +7094,7 @@
    </transf>
    </goal>
    <goal name="VC div_sb_qr.261.1" expl="VC for div_sb_qr" proved="true">
-   <proof prover="0" timelimit="20"><result status="valid" time="4.67"/></proof>
+   <proof prover="0" timelimit="20"><result status="valid" time="3.51"/></proof>
    </goal>
   </transf>
   </goal>
@@ -7117,7 +7117,7 @@
    <proof prover="0"><result status="valid" time="0.06"/></proof>
    </goal>
    <goal name="VC div_sb_qr.263.4" expl="VC for div_sb_qr" proved="true">
-   <proof prover="0"><result status="valid" time="1.22"/></proof>
+   <proof prover="0"><result status="valid" time="0.95"/></proof>
    </goal>
    <goal name="VC div_sb_qr.263.5" expl="VC for div_sb_qr" proved="true">
    <proof prover="0"><result status="valid" time="0.02"/></proof>
@@ -7350,15 +7350,15 @@
   <goal name="VC wmpn_divrem_2.43" expl="loop variant decrease" proved="true">
   <transf name="split_goal_right" proved="true" >
    <goal name="VC wmpn_divrem_2.43.0" expl="loop variant decrease" proved="true">
+   <proof prover="2"><result status="valid" time="0.06"/></proof>
+   </goal>
+   <goal name="VC wmpn_divrem_2.43.1" expl="loop variant decrease" proved="true">
    <transf name="introduce_premises" proved="true" >
-    <goal name="VC wmpn_divrem_2.43.0.0" expl="loop variant decrease" proved="true">
+    <goal name="VC wmpn_divrem_2.43.1.0" expl="loop variant decrease" proved="true">
     <proof prover="2"><result status="valid" time="0.12"/></proof>
     </goal>
    </transf>
    </goal>
-   <goal name="VC wmpn_divrem_2.43.1" expl="loop variant decrease" proved="true">
-   <proof prover="2"><result status="valid" time="0.06"/></proof>
-   </goal>
   </transf>
   </goal>
   <goal name="VC wmpn_divrem_2.44" expl="loop invariant preservation" proved="true">
@@ -7607,7 +7607,7 @@
   <proof prover="5"><result status="valid" time="0.02" steps="39"/></proof>
   </goal>
   <goal name="VC div_qr.35" expl="assertion" proved="true">
-  <proof prover="0" memlimit="1000"><result status="valid" time="3.30"/></proof>
+  <proof prover="0" memlimit="1000"><result status="valid" time="2.54"/></proof>
   <proof prover="2"><result status="valid" time="0.14"/></proof>
   </goal>
   <goal name="VC div_qr.36" expl="precondition" proved="true">
@@ -8197,13 +8197,13 @@
   <goal name="VC div_qr.82" expl="integer overflow" proved="true">
   <transf name="split_goal_right" proved="true" >
    <goal name="VC div_qr.82.0" expl="integer overflow" proved="true">
-   <proof prover="2"><result status="valid" time="0.14"/></proof>
-   <proof prover="3"><result status="valid" time="0.04"/></proof>
-   </goal>
-   <goal name="VC div_qr.82.1" expl="integer overflow" proved="true">
    <proof prover="2"><result status="valid" time="0.08"/></proof>
    <proof prover="3"><result status="valid" time="0.08"/></proof>
    </goal>
+   <goal name="VC div_qr.82.1" expl="integer overflow" proved="true">
+   <proof prover="2"><result status="valid" time="0.14"/></proof>
+   <proof prover="3"><result status="valid" time="0.04"/></proof>
+   </goal>
   </transf>
   </goal>
   <goal name="VC div_qr.83" expl="precondition" proved="true">
@@ -8245,7 +8245,7 @@
    <proof prover="2"><result status="valid" time="0.09"/></proof>
    </goal>
    <goal name="VC div_qr.90.1" expl="VC for div_qr" proved="true">
-   <proof prover="0"><result status="valid" time="1.60"/></proof>
+   <proof prover="0"><result status="valid" time="1.21"/></proof>
    </goal>
    <goal name="VC div_qr.90.2" expl="VC for div_qr" proved="true">
    <proof prover="0"><result status="valid" time="0.09"/></proof>
@@ -8321,7 +8321,7 @@
   <proof prover="3"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC div_qr.96" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="4.50"/></proof>
+  <proof prover="0"><result status="valid" time="3.75"/></proof>
   </goal>
   <goal name="VC div_qr.97" expl="postcondition" proved="true">
   <proof prover="0"><result status="valid" time="0.02"/></proof>
@@ -8483,13 +8483,13 @@
   <goal name="VC div_qr.120" expl="assertion" proved="true">
   <transf name="split_goal_right" proved="true" >
    <goal name="VC div_qr.120.0" expl="assertion" proved="true">
-   <proof prover="2"><result status="valid" time="0.05"/></proof>
-   <proof prover="3"><result status="valid" time="0.04"/></proof>
-   </goal>
-   <goal name="VC div_qr.120.1" expl="assertion" proved="true">
    <proof prover="2"><result status="valid" time="0.07"/></proof>
    <proof prover="5"><result status="valid" time="0.11" steps="64"/></proof>
    </goal>
+   <goal name="VC div_qr.120.1" expl="assertion" proved="true">
+   <proof prover="2"><result status="valid" time="0.05"/></proof>
+   <proof prover="3"><result status="valid" time="0.04"/></proof>
+   </goal>
   </transf>
   </goal>
   <goal name="VC div_qr.121" expl="assertion" proved="true">
@@ -8571,7 +8571,7 @@
   <goal name="VC div_qr.122" expl="postcondition" proved="true">
   <transf name="introduce_premises" proved="true" >
    <goal name="VC div_qr.122.0" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="4.00"/></proof>
+   <proof prover="0"><result status="valid" time="3.05"/></proof>
    </goal>
   </transf>
   </goal>
@@ -8594,7 +8594,7 @@
    <proof prover="2"><result status="valid" time="0.30"/></proof>
    </goal>
    <goal name="VC div_qr.123.5" expl="VC for div_qr" proved="true">
-   <proof prover="0"><result status="valid" time="3.66"/></proof>
+   <proof prover="0"><result status="valid" time="2.97"/></proof>
    <proof prover="1"><result status="valid" time="0.66"/></proof>
    </goal>
    <goal name="VC div_qr.123.6" expl="VC for div_qr" proved="true">
diff --git a/examples/multiprecision/div/why3shapes.gz b/examples/multiprecision/div/why3shapes.gz
index 31b997938e76cff88dbb17baf9ccab93dd60e62e..9e91d52964d47004957d68e9b5a41b818111f24f 100644
Binary files a/examples/multiprecision/div/why3shapes.gz and b/examples/multiprecision/div/why3shapes.gz differ
diff --git a/examples/multiprecision/lemmas/why3session.xml b/examples/multiprecision/lemmas/why3session.xml
index 8c8eb6491242549cead99c6452fb1bfa9104b573..bf7f0a40ca88a4cbbbb378883387e5d45a1dd8be 100644
--- a/examples/multiprecision/lemmas/why3session.xml
+++ b/examples/multiprecision/lemmas/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Eprover" version="1.9.1-001" timelimit="5" steplimit="0" memlimit="2000"/>
 <prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
diff --git a/examples/multiprecision/lemmas/why3shapes.gz b/examples/multiprecision/lemmas/why3shapes.gz
index b3de7cce952d87cbe445c03ac4dd8352eaf67455..3b2be5e2a4e1b6e292104f6ab54292c610fa105c 100644
Binary files a/examples/multiprecision/lemmas/why3shapes.gz and b/examples/multiprecision/lemmas/why3shapes.gz differ
diff --git a/examples/multiprecision/lineardecision/why3session.xml b/examples/multiprecision/lineardecision/why3session.xml
index f6fee30829bb20126d8c9234482a8904111df3e7..a1f0f49335428faba05ea3763c68fa3b62fe96fe 100644
--- a/examples/multiprecision/lineardecision/why3session.xml
+++ b/examples/multiprecision/lineardecision/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="1" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
@@ -1903,7 +1903,7 @@
    <goal name="VC radd.1.3" expl="VC for radd" proved="true">
    <transf name="compute_in_goal" proved="true" >
     <goal name="VC radd.1.3.0" expl="VC for radd" proved="true">
-    <proof prover="3" timelimit="10"><result status="valid" time="0.05"/></proof>
+    <proof prover="3" timelimit="10"><result status="valid" time="0.52"/></proof>
     </goal>
    </transf>
    </goal>
@@ -1992,7 +1992,7 @@
   <goal name="VC rinv.2" expl="postcondition" proved="true">
   <transf name="compute_in_goal" proved="true" >
    <goal name="VC rinv.2.0" expl="postcondition" proved="true">
-   <proof prover="3" timelimit="10"><result status="valid" time="0.08"/></proof>
+   <proof prover="3" timelimit="10"><result status="valid" time="0.20"/></proof>
    </goal>
   </transf>
   </goal>
@@ -3461,7 +3461,7 @@
  <goal name="VC impl_self" expl="VC for impl_self" proved="true">
  <transf name="split_goal_right" proved="true" >
   <goal name="VC impl_self.0" expl="variant decrease" proved="true">
-  <proof prover="2"><result status="valid" time="0.28"/></proof>
+  <proof prover="2"><result status="valid" time="0.15"/></proof>
   </goal>
   <goal name="VC impl_self.1" expl="precondition" proved="true">
   <proof prover="2"><result status="valid" time="0.15"/></proof>
diff --git a/examples/multiprecision/lineardecision/why3shapes.gz b/examples/multiprecision/lineardecision/why3shapes.gz
index 77ef68ba1b09dbb95fc43ded2f106ab306b072c7..c3a44af875d9f2050cad476d29b7006934269869 100644
Binary files a/examples/multiprecision/lineardecision/why3shapes.gz and b/examples/multiprecision/lineardecision/why3shapes.gz differ
diff --git a/examples/multiprecision/logical/why3session.xml b/examples/multiprecision/logical/why3session.xml
index e71f1512f603d5363026a332958d7c550aae8328..7c4c19cd896bb85929882848124a51122ab07b58 100644
--- a/examples/multiprecision/logical/why3session.xml
+++ b/examples/multiprecision/logical/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Eprover" version="1.9.1-001" timelimit="5" steplimit="0" memlimit="2000"/>
 <prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="2000"/>
 <prover id="2" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
@@ -735,7 +735,7 @@
   <goal name="VC wmpn_rshift.40" expl="loop invariant preservation" proved="true">
   <transf name="split_goal_right" proved="true" >
    <goal name="VC wmpn_rshift.40.0" expl="loop invariant preservation" proved="true">
-   <proof prover="0"><result status="valid" time="2.51"/></proof>
+   <proof prover="0"><result status="valid" time="2.98"/></proof>
    </goal>
   </transf>
   </goal>
@@ -1091,7 +1091,7 @@
      <proof prover="2"><result status="valid" time="0.21"/></proof>
      </goal>
      <goal name="VC wmpn_lshift_in_place.40.0.0.15" expl="apply premises" proved="true">
-     <proof prover="2"><result status="valid" time="0.19"/></proof>
+     <proof prover="2"><result status="valid" time="0.14"/></proof>
      </goal>
      <goal name="VC wmpn_lshift_in_place.40.0.0.16" expl="apply premises" proved="true">
      <proof prover="2"><result status="valid" time="0.14"/></proof>
@@ -1100,7 +1100,7 @@
      <proof prover="2"><result status="valid" time="0.15"/></proof>
      </goal>
      <goal name="VC wmpn_lshift_in_place.40.0.0.18" expl="apply premises" proved="true">
-     <proof prover="2"><result status="valid" time="0.14"/></proof>
+     <proof prover="2"><result status="valid" time="0.18"/></proof>
      </goal>
      <goal name="VC wmpn_lshift_in_place.40.0.0.19" expl="apply premises" proved="true">
      <proof prover="2"><result status="valid" time="0.18"/></proof>
@@ -1124,7 +1124,7 @@
      <proof prover="2"><result status="valid" time="0.16"/></proof>
      </goal>
      <goal name="VC wmpn_lshift_in_place.40.0.0.26" expl="apply premises" proved="true">
-     <proof prover="2"><result status="valid" time="0.18"/></proof>
+     <proof prover="2"><result status="valid" time="0.19"/></proof>
      </goal>
      <goal name="VC wmpn_lshift_in_place.40.0.0.27" expl="apply premises" proved="true">
      <proof prover="2"><result status="valid" time="0.20"/></proof>
@@ -1142,10 +1142,10 @@
      <proof prover="2"><result status="valid" time="0.14"/></proof>
      </goal>
      <goal name="VC wmpn_lshift_in_place.40.0.0.32" expl="apply premises" proved="true">
-     <proof prover="2"><result status="valid" time="0.15"/></proof>
+     <proof prover="2"><result status="valid" time="0.16"/></proof>
      </goal>
      <goal name="VC wmpn_lshift_in_place.40.0.0.33" expl="apply premises" proved="true">
-     <proof prover="2"><result status="valid" time="0.14"/></proof>
+     <proof prover="2"><result status="valid" time="0.15"/></proof>
      </goal>
      <goal name="VC wmpn_lshift_in_place.40.0.0.34" expl="apply premises" proved="true">
      <proof prover="2"><result status="valid" time="0.13"/></proof>
@@ -1154,16 +1154,16 @@
      <proof prover="2"><result status="valid" time="0.14"/></proof>
      </goal>
      <goal name="VC wmpn_lshift_in_place.40.0.0.36" expl="apply premises" proved="true">
-     <proof prover="2"><result status="valid" time="0.16"/></proof>
+     <proof prover="2"><result status="valid" time="0.15"/></proof>
      </goal>
      <goal name="VC wmpn_lshift_in_place.40.0.0.37" expl="apply premises" proved="true">
-     <proof prover="2"><result status="valid" time="0.15"/></proof>
+     <proof prover="2"><result status="valid" time="0.14"/></proof>
      </goal>
      <goal name="VC wmpn_lshift_in_place.40.0.0.38" expl="apply premises" proved="true">
      <proof prover="2"><result status="valid" time="0.23"/></proof>
      </goal>
      <goal name="VC wmpn_lshift_in_place.40.0.0.39" expl="apply premises" proved="true">
-     <proof prover="2"><result status="valid" time="0.17"/></proof>
+     <proof prover="2"><result status="valid" time="0.20"/></proof>
      </goal>
      <goal name="VC wmpn_lshift_in_place.40.0.0.40" expl="apply premises" proved="true">
      <proof prover="2"><result status="valid" time="0.14"/></proof>
@@ -1175,10 +1175,10 @@
      <proof prover="2"><result status="valid" time="0.18"/></proof>
      </goal>
      <goal name="VC wmpn_lshift_in_place.40.0.0.43" expl="apply premises" proved="true">
-     <proof prover="2"><result status="valid" time="0.20"/></proof>
+     <proof prover="2"><result status="valid" time="0.14"/></proof>
      </goal>
      <goal name="VC wmpn_lshift_in_place.40.0.0.44" expl="apply premises" proved="true">
-     <proof prover="2"><result status="valid" time="0.18"/></proof>
+     <proof prover="2"><result status="valid" time="0.21"/></proof>
      </goal>
      <goal name="VC wmpn_lshift_in_place.40.0.0.45" expl="apply premises" proved="true">
      <proof prover="2"><result status="valid" time="0.16"/></proof>
@@ -1244,7 +1244,7 @@
      <proof prover="2"><result status="valid" time="0.14"/></proof>
      </goal>
      <goal name="VC wmpn_lshift_in_place.40.0.0.66" expl="apply premises" proved="true">
-     <proof prover="2"><result status="valid" time="0.20"/></proof>
+     <proof prover="2"><result status="valid" time="0.17"/></proof>
      </goal>
      <goal name="VC wmpn_lshift_in_place.40.0.0.67" expl="apply premises" proved="true">
      <proof prover="2"><result status="valid" time="0.14"/></proof>
@@ -1265,7 +1265,7 @@
      <proof prover="2"><result status="valid" time="0.14"/></proof>
      </goal>
      <goal name="VC wmpn_lshift_in_place.40.0.0.73" expl="apply premises" proved="true">
-     <proof prover="2"><result status="valid" time="0.14"/></proof>
+     <proof prover="2"><result status="valid" time="0.21"/></proof>
      </goal>
      <goal name="VC wmpn_lshift_in_place.40.0.0.74" expl="apply premises" proved="true">
      <proof prover="2"><result status="valid" time="0.13"/></proof>
@@ -1277,7 +1277,7 @@
      <proof prover="2"><result status="valid" time="0.15"/></proof>
      </goal>
      <goal name="VC wmpn_lshift_in_place.40.0.0.77" expl="apply premises" proved="true">
-     <proof prover="2"><result status="valid" time="0.21"/></proof>
+     <proof prover="2"><result status="valid" time="0.14"/></proof>
      </goal>
      <goal name="VC wmpn_lshift_in_place.40.0.0.78" expl="apply premises" proved="true">
      <proof prover="2"><result status="valid" time="0.16"/></proof>
@@ -1286,10 +1286,10 @@
      <proof prover="2"><result status="valid" time="0.19"/></proof>
      </goal>
      <goal name="VC wmpn_lshift_in_place.40.0.0.80" expl="apply premises" proved="true">
-     <proof prover="2"><result status="valid" time="0.14"/></proof>
+     <proof prover="2"><result status="valid" time="0.20"/></proof>
      </goal>
      <goal name="VC wmpn_lshift_in_place.40.0.0.81" expl="apply premises" proved="true">
-     <proof prover="2"><result status="valid" time="0.21"/></proof>
+     <proof prover="2"><result status="valid" time="0.18"/></proof>
      </goal>
      <goal name="VC wmpn_lshift_in_place.40.0.0.82" expl="apply premises" proved="true">
      <proof prover="2"><result status="valid" time="0.12"/></proof>
@@ -1369,10 +1369,10 @@
   <goal name="VC wmpn_lshift_in_place.42" expl="assertion" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="VC wmpn_lshift_in_place.42.0" expl="assertion" proved="true">
-   <proof prover="0"><result status="valid" time="0.18"/></proof>
+   <proof prover="0"><result status="valid" time="0.19"/></proof>
    </goal>
    <goal name="VC wmpn_lshift_in_place.42.1" expl="assertion" proved="true">
-   <proof prover="0"><result status="valid" time="0.61"/></proof>
+   <proof prover="0"><result status="valid" time="0.68"/></proof>
    </goal>
    <goal name="VC wmpn_lshift_in_place.42.2" expl="VC for wmpn_lshift_in_place" proved="true">
    <proof prover="2"><result status="valid" time="0.11"/></proof>
@@ -1641,7 +1641,7 @@
    <proof prover="0"><result status="valid" time="0.16"/></proof>
    </goal>
    <goal name="VC wmpn_rshift_in_place.42.1" expl="assertion" proved="true">
-   <proof prover="0"><result status="valid" time="0.42"/></proof>
+   <proof prover="0"><result status="valid" time="0.52"/></proof>
    </goal>
    <goal name="VC wmpn_rshift_in_place.42.2" expl="VC for wmpn_rshift_in_place" proved="true">
    <proof prover="2" timelimit="5"><result status="valid" time="0.06"/></proof>
diff --git a/examples/multiprecision/logical/why3shapes.gz b/examples/multiprecision/logical/why3shapes.gz
index d0ead94d618a9b98b25c62805286ffa1017b3035..9555d1bbfcc752ffd47b42e9ab81c184fbfd8d73 100644
Binary files a/examples/multiprecision/logical/why3shapes.gz and b/examples/multiprecision/logical/why3shapes.gz differ
diff --git a/examples/multiprecision/mul/why3session.xml b/examples/multiprecision/mul/why3session.xml
index 8bfec7f630169e657b668107a8377d18ea701561..ad6dffc4cb40f8cc5d5eee13f1fb973fe5cfb8c2 100644
--- a/examples/multiprecision/mul/why3session.xml
+++ b/examples/multiprecision/mul/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Eprover" version="1.9.1-001" timelimit="5" steplimit="0" memlimit="2000"/>
 <prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
@@ -656,7 +656,7 @@
   <proof prover="5"><result status="valid" time="0.02" steps="35"/></proof>
   </goal>
   <goal name="VC wmpn_addmul_n.11" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="1.96"/></proof>
+  <proof prover="0"><result status="valid" time="2.34"/></proof>
   </goal>
   <goal name="VC wmpn_addmul_n.12" expl="precondition" proved="true">
   <proof prover="5"><result status="valid" time="0.03" steps="53"/></proof>
@@ -1172,7 +1172,7 @@
          <proof prover="3"><result status="valid" time="0.02"/></proof>
          </goal>
          <goal name="VC wmpn_mul_basecase.38.0.0.0.0.0.0.43" expl="apply premises" proved="true">
-         <proof prover="2"><result status="valid" time="0.17"/></proof>
+         <proof prover="3"><result status="valid" time="0.02"/></proof>
          </goal>
          <goal name="VC wmpn_mul_basecase.38.0.0.0.0.0.0.44" expl="apply premises" proved="true">
          <proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -1220,10 +1220,10 @@
          <proof prover="3"><result status="valid" time="0.02"/></proof>
          </goal>
          <goal name="VC wmpn_mul_basecase.38.0.0.0.0.0.0.59" expl="apply premises" proved="true">
-         <proof prover="3"><result status="valid" time="0.03"/></proof>
+         <proof prover="3"><result status="valid" time="0.02"/></proof>
          </goal>
          <goal name="VC wmpn_mul_basecase.38.0.0.0.0.0.0.60" expl="apply premises" proved="true">
-         <proof prover="3"><result status="valid" time="0.04"/></proof>
+         <proof prover="3"><result status="valid" time="0.02"/></proof>
          </goal>
          <goal name="VC wmpn_mul_basecase.38.0.0.0.0.0.0.61" expl="apply premises" proved="true">
          <proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -1277,7 +1277,7 @@
          <proof prover="3"><result status="valid" time="0.02"/></proof>
          </goal>
          <goal name="VC wmpn_mul_basecase.38.0.0.0.0.0.0.78" expl="apply premises" proved="true">
-         <proof prover="3"><result status="valid" time="0.02"/></proof>
+         <proof prover="2"><result status="valid" time="0.17"/></proof>
          </goal>
          <goal name="VC wmpn_mul_basecase.38.0.0.0.0.0.0.79" expl="apply premises" proved="true">
          <proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -1343,10 +1343,10 @@
          <proof prover="3"><result status="valid" time="0.02"/></proof>
          </goal>
          <goal name="VC wmpn_mul_basecase.38.0.0.0.0.0.0.100" expl="apply premises" proved="true">
-         <proof prover="3"><result status="valid" time="0.02"/></proof>
+         <proof prover="3"><result status="valid" time="0.03"/></proof>
          </goal>
          <goal name="VC wmpn_mul_basecase.38.0.0.0.0.0.0.101" expl="apply premises" proved="true">
-         <proof prover="3"><result status="valid" time="0.02"/></proof>
+         <proof prover="3"><result status="valid" time="0.04"/></proof>
          </goal>
          <goal name="VC wmpn_mul_basecase.38.0.0.0.0.0.0.102" expl="apply premises" proved="true">
          <proof prover="3"><result status="valid" time="0.02"/></proof>
diff --git a/examples/multiprecision/mul/why3shapes.gz b/examples/multiprecision/mul/why3shapes.gz
index f1667d5dbc5bc649724fc5b75b476c2349860112..126789eacf720c1445c8f057a9f7ce2de92e45f0 100644
Binary files a/examples/multiprecision/mul/why3shapes.gz and b/examples/multiprecision/mul/why3shapes.gz differ
diff --git a/examples/multiprecision/sub/why3session.xml b/examples/multiprecision/sub/why3session.xml
index 09ae08204f29e6aa3c477dd243e8d7273d7f1131..6e2fdb26b3f3c7b5964768fb02a42ac13da55ae0 100644
--- a/examples/multiprecision/sub/why3session.xml
+++ b/examples/multiprecision/sub/why3session.xml
@@ -1,13 +1,12 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Eprover" version="1.9.1-001" timelimit="5" steplimit="0" memlimit="2000"/>
 <prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="3" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="5" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
-<prover id="6" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
 <file proved="true">
 <path name=".."/>
 <path name="sub.mlw"/>
@@ -309,7 +308,7 @@
     <goal name="VC wmpn_sub_n.12.0.0" expl="assertion" proved="true">
     <transf name="reflection_f" proved="true" arg1="mp_decision">
      <goal name="VC wmpn_sub_n.12.0.0.0" expl="assertion" proved="true">
-     <proof prover="0"><result status="valid" time="3.24"/></proof>
+     <proof prover="0"><result status="valid" time="2.47"/></proof>
      </goal>
      <goal name="VC wmpn_sub_n.12.0.0.1" proved="true">
      <proof prover="3"><result status="valid" time="0.28"/></proof>
@@ -402,7 +401,7 @@
     <goal name="VC wmpn_sub.12.0.0" expl="assertion" proved="true">
     <transf name="reflection_f" proved="true" arg1="mp_decision">
      <goal name="VC wmpn_sub.12.0.0.0" expl="assertion" proved="true">
-     <proof prover="0"><result status="valid" time="2.96"/></proof>
+     <proof prover="0"><result status="valid" time="2.37"/></proof>
      </goal>
      <goal name="VC wmpn_sub.12.0.0.1" proved="true">
      <proof prover="3"><result status="valid" time="0.16"/></proof>
@@ -754,10 +753,10 @@
   <goal name="VC wmpn_sub_in_place.10" expl="assertion" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="VC wmpn_sub_in_place.10.0" expl="assertion" proved="true">
-   <proof prover="6"><result status="valid" time="0.07"/></proof>
+   <proof prover="5"><result status="valid" time="0.02" steps="38"/></proof>
    </goal>
    <goal name="VC wmpn_sub_in_place.10.1" expl="assertion" proved="true">
-   <proof prover="5"><result status="valid" time="0.02" steps="62"/></proof>
+   <proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="62"/></proof>
    </goal>
    <goal name="VC wmpn_sub_in_place.10.2" expl="VC for wmpn_sub_in_place" proved="true">
    <proof prover="5"><result status="valid" time="0.01" steps="39"/></proof>
@@ -783,7 +782,7 @@
     <goal name="VC wmpn_sub_in_place.15.0.0" expl="assertion" proved="true">
     <transf name="reflection_f" proved="true" arg1="mp_decision">
      <goal name="VC wmpn_sub_in_place.15.0.0.0" expl="assertion" proved="true">
-     <proof prover="0"><result status="valid" time="3.14"/></proof>
+     <proof prover="0"><result status="valid" time="2.31"/></proof>
      </goal>
      <goal name="VC wmpn_sub_in_place.15.0.0.1" proved="true">
      <proof prover="3"><result status="valid" time="0.16"/></proof>
@@ -1277,7 +1276,7 @@
   <proof prover="5"><result status="valid" time="0.03" steps="55"/></proof>
   </goal>
   <goal name="VC wmpn_decr_1.18" expl="integer overflow" proved="true">
-  <proof prover="3"><result status="valid" time="0.16"/></proof>
+  <proof prover="3"><result status="valid" time="0.20"/></proof>
   </goal>
   <goal name="VC wmpn_decr_1.19" expl="assertion" proved="true">
   <proof prover="5"><result status="valid" time="0.45" steps="276"/></proof>
@@ -1334,7 +1333,7 @@
   <proof prover="5"><result status="valid" time="0.04" steps="43"/></proof>
   </goal>
   <goal name="VC wmpn_decr_1.37" expl="integer overflow" proved="true">
-  <proof prover="3"><result status="valid" time="0.20"/></proof>
+  <proof prover="3"><result status="valid" time="0.16"/></proof>
   </goal>
   <goal name="VC wmpn_decr_1.38" expl="assertion" proved="true">
   <transf name="split_vc" proved="true" >
diff --git a/examples/multiprecision/sub/why3shapes.gz b/examples/multiprecision/sub/why3shapes.gz
index e17a4004a8dc70134ba521447bd57d35502bda7a..eccf386d049ee912651de206a16799ecd9699c0e 100644
Binary files a/examples/multiprecision/sub/why3shapes.gz and b/examples/multiprecision/sub/why3shapes.gz differ
diff --git a/examples/multiprecision/toom/why3session.xml b/examples/multiprecision/toom/why3session.xml
index 26aa5863fd9e3a8736c9fd1c08827b4c31460aac..1b73da09404e8474d13ad02bb686acd707b620fb 100644
--- a/examples/multiprecision/toom/why3session.xml
+++ b/examples/multiprecision/toom/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Eprover" version="1.9.1-001" timelimit="5" steplimit="0" memlimit="2000"/>
 <prover id="1" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Z3" version="4.7.1" timelimit="1" steplimit="0" memlimit="1000"/>
@@ -381,8 +381,8 @@
   <proof prover="5"><result status="valid" time="0.52" steps="195"/></proof>
   </goal>
   <goal name="VC wmpn_toom22_mul.81" expl="integer overflow" proved="true">
-  <proof prover="4" timelimit="20" memlimit="1000"><result status="valid" time="5.82"/></proof>
-  <proof prover="5" timelimit="20"><result status="valid" time="11.23" steps="385"/></proof>
+  <proof prover="4" timelimit="20" memlimit="1000"><result status="valid" time="6.96"/></proof>
+  <proof prover="5" timelimit="20"><result status="valid" time="12.50" steps="385"/></proof>
   </goal>
   <goal name="VC wmpn_toom22_mul.82" expl="precondition" proved="true">
   <proof prover="1"><result status="valid" time="0.13"/></proof>
@@ -577,7 +577,7 @@
   <proof prover="1"><result status="valid" time="0.28"/></proof>
   </goal>
   <goal name="VC wmpn_toom22_mul.122" expl="assertion" proved="true">
-  <proof prover="3"><result status="valid" time="0.61"/></proof>
+  <proof prover="3"><result status="valid" time="0.43"/></proof>
   </goal>
   <goal name="VC wmpn_toom22_mul.123" expl="precondition" proved="true">
   <proof prover="3"><result status="valid" time="0.06"/></proof>
@@ -654,7 +654,7 @@
    <goal name="VC wmpn_toom22_mul.136.0" expl="precondition" proved="true">
    <transf name="inline_goal" proved="true" >
     <goal name="VC wmpn_toom22_mul.136.0.0" expl="precondition" proved="true">
-    <proof prover="5" memlimit="2000"><result status="valid" time="1.50" steps="254"/></proof>
+    <proof prover="5" memlimit="2000"><result status="valid" time="1.75" steps="254"/></proof>
     </goal>
    </transf>
    </goal>
@@ -670,7 +670,7 @@
   <proof prover="3"><result status="valid" time="0.05"/></proof>
   </goal>
   <goal name="VC wmpn_toom22_mul.140" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="1.06"/></proof>
+  <proof prover="0"><result status="valid" time="1.29"/></proof>
   </goal>
   <goal name="VC wmpn_toom22_mul.141" expl="postcondition" proved="true">
   <proof prover="1"><result status="valid" time="0.08"/></proof>
@@ -755,7 +755,7 @@
   <proof prover="5"><result status="valid" time="1.12" steps="240"/></proof>
   </goal>
   <goal name="VC wmpn_toom22_mul.151" expl="precondition" proved="true">
-  <proof prover="5" memlimit="2000"><result status="valid" time="1.18" steps="254"/></proof>
+  <proof prover="5" memlimit="2000"><result status="valid" time="1.43" steps="254"/></proof>
   </goal>
   <goal name="VC wmpn_toom22_mul.152" expl="precondition" proved="true">
   <transf name="introduce_premises" proved="true" >
@@ -1509,7 +1509,7 @@
   <goal name="VC wmpn_toom22_mul.291" expl="assertion" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="VC wmpn_toom22_mul.291.0" expl="assertion" proved="true">
-   <proof prover="0" memlimit="1000"><result status="valid" time="0.22"/></proof>
+   <proof prover="0" memlimit="1000"><result status="valid" time="0.09"/></proof>
    </goal>
    <goal name="VC wmpn_toom22_mul.291.1" expl="assertion" proved="true">
    <proof prover="0" memlimit="1000"><result status="valid" time="0.03"/></proof>
@@ -2177,7 +2177,7 @@
   <goal name="VC wmpn_toom22_mul.332" expl="precondition" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="VC wmpn_toom22_mul.332.0" expl="precondition" proved="true">
-   <proof prover="1"><result status="valid" time="0.24"/></proof>
+   <proof prover="1"><result status="valid" time="0.11"/></proof>
    </goal>
    <goal name="VC wmpn_toom22_mul.332.1" expl="precondition" proved="true">
    <proof prover="1"><result status="valid" time="0.16"/></proof>
@@ -2241,10 +2241,10 @@
     </transf>
     </goal>
     <goal name="VC wmpn_toom22_mul.335.3.1" expl="rewrite premises" proved="true">
-    <proof prover="3"><result status="valid" time="0.06"/></proof>
+    <proof prover="3"><result status="valid" time="0.04"/></proof>
     </goal>
     <goal name="VC wmpn_toom22_mul.335.3.2" expl="rewrite premises" proved="true">
-    <proof prover="3"><result status="valid" time="0.04"/></proof>
+    <proof prover="3"><result status="valid" time="0.06"/></proof>
     </goal>
    </transf>
    </goal>
@@ -2438,7 +2438,7 @@
    <proof prover="0"><result status="valid" time="0.10"/></proof>
    </goal>
    <goal name="VC wmpn_toom22_mul.351.1" expl="assertion" proved="true">
-   <proof prover="0"><result status="valid" time="0.57"/></proof>
+   <proof prover="0"><result status="valid" time="0.41"/></proof>
    </goal>
    <goal name="VC wmpn_toom22_mul.351.2" expl="VC for wmpn_toom22_mul" proved="true">
    <proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -3020,7 +3020,7 @@
    <goal name="VC wmpn_toom22_mul.351.83" expl="VC for wmpn_toom22_mul" proved="true">
    <transf name="apply" proved="true" arg1="H" arg2="with" arg3="(power 2 k),(power 2 (64*s))">
     <goal name="VC wmpn_toom22_mul.351.83.0" expl="apply premises" proved="true">
-    <proof prover="0" memlimit="1000"><result status="valid" time="2.58"/></proof>
+    <proof prover="0" memlimit="1000"><result status="valid" time="3.18"/></proof>
     <proof prover="3"><result status="valid" time="0.04"/></proof>
     </goal>
     <goal name="VC wmpn_toom22_mul.351.83.1" expl="apply premises" proved="true">
@@ -3044,7 +3044,7 @@
      <proof prover="0"><result status="valid" time="0.04"/></proof>
      </goal>
      <goal name="VC wmpn_toom22_mul.351.83.1.1" expl="asserted formula" proved="true">
-     <proof prover="3"><result status="valid" time="1.84"/></proof>
+     <proof prover="3"><result status="valid" time="2.14"/></proof>
      </goal>
     </transf>
     </goal>
@@ -3072,7 +3072,7 @@
     <proof prover="4"><result status="valid" time="0.47"/></proof>
     </goal>
     <goal name="VC wmpn_toom22_mul.351.83.5" expl="apply premises" proved="true">
-    <proof prover="0"><result status="valid" time="2.74"/></proof>
+    <proof prover="0"><result status="valid" time="3.30"/></proof>
     <proof prover="3"><result status="valid" time="2.15"/></proof>
     </goal>
    </transf>
@@ -3086,7 +3086,7 @@
     <proof prover="6"><result status="valid" time="0.15"/></proof>
     </goal>
     <goal name="VC wmpn_toom22_mul.351.85.1" expl="apply premises" proved="true">
-    <proof prover="0" memlimit="1000"><result status="valid" time="2.16"/></proof>
+    <proof prover="0" memlimit="1000"><result status="valid" time="2.58"/></proof>
     </goal>
     <goal name="VC wmpn_toom22_mul.351.85.2" expl="apply premises" proved="true">
     <transf name="cut" proved="true" arg1="(1 &lt;= power 2 l)">
@@ -3711,7 +3711,7 @@
    <proof prover="1"><result status="valid" time="0.14"/></proof>
    </goal>
    <goal name="VC wmpn_toom22_mul.374.2" expl="VC for wmpn_toom22_mul" proved="true">
-   <proof prover="1"><result status="valid" time="0.26"/></proof>
+   <proof prover="1"><result status="valid" time="0.13"/></proof>
    </goal>
   </transf>
   </goal>
@@ -4025,7 +4025,7 @@
    <proof prover="4"><result status="valid" time="0.46"/></proof>
    </goal>
    <goal name="VC wmpn_toom22_mul.405.1" expl="assertion" proved="true">
-   <proof prover="4"><result status="valid" time="0.54"/></proof>
+   <proof prover="4"><result status="valid" time="0.38"/></proof>
    </goal>
    <goal name="VC wmpn_toom22_mul.405.2" expl="VC for wmpn_toom22_mul" proved="true">
    <proof prover="3"><result status="valid" time="0.05"/></proof>
@@ -5167,7 +5167,7 @@
    <proof prover="1"><result status="valid" time="0.08"/></proof>
    </goal>
    <goal name="VC wmpn_toom32_mul.127.1" expl="VC for wmpn_toom32_mul" proved="true">
-   <proof prover="0"><result status="valid" time="2.02"/></proof>
+   <proof prover="0"><result status="valid" time="2.40"/></proof>
    </goal>
    <goal name="VC wmpn_toom32_mul.127.2" expl="VC for wmpn_toom32_mul" proved="true">
    <proof prover="4"><result status="valid" time="0.87"/></proof>
@@ -5464,7 +5464,7 @@
   <proof prover="1"><result status="valid" time="0.09"/></proof>
   </goal>
   <goal name="VC wmpn_toom32_mul.181" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.20"/></proof>
+  <proof prover="1"><result status="valid" time="0.08"/></proof>
   </goal>
   <goal name="VC wmpn_toom32_mul.182" expl="integer overflow" proved="true">
   <proof prover="1"><result status="valid" time="0.14"/></proof>
@@ -5594,7 +5594,7 @@
   <proof prover="1"><result status="valid" time="0.29"/></proof>
   </goal>
   <goal name="VC wmpn_toom32_mul.207" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="1.00"/></proof>
+  <proof prover="1"><result status="valid" time="0.77"/></proof>
   </goal>
   <goal name="VC wmpn_toom32_mul.208" expl="precondition" proved="true">
   <proof prover="1"><result status="valid" time="0.17"/></proof>
@@ -5836,7 +5836,7 @@
    <proof prover="1"><result status="valid" time="0.06"/></proof>
    </goal>
    <goal name="VC wmpn_toom32_mul.244.15" expl="VC for wmpn_toom32_mul" proved="true">
-   <proof prover="0"><result status="valid" time="2.88"/></proof>
+   <proof prover="0"><result status="valid" time="3.38"/></proof>
    </goal>
    <goal name="VC wmpn_toom32_mul.244.16" expl="VC for wmpn_toom32_mul" proved="true">
    <proof prover="1"><result status="valid" time="0.11"/></proof>
@@ -5851,7 +5851,7 @@
    <proof prover="1"><result status="valid" time="0.05"/></proof>
    </goal>
    <goal name="VC wmpn_toom32_mul.244.20" expl="VC for wmpn_toom32_mul" proved="true">
-   <proof prover="0"><result status="valid" time="2.93"/></proof>
+   <proof prover="0"><result status="valid" time="3.44"/></proof>
    </goal>
    <goal name="VC wmpn_toom32_mul.244.21" expl="VC for wmpn_toom32_mul" proved="true">
    <proof prover="1"><result status="valid" time="0.06"/></proof>
@@ -6212,7 +6212,7 @@
    <proof prover="4"><result status="valid" time="0.26"/></proof>
    </goal>
    <goal name="VC wmpn_toom32_mul.272.18" expl="VC for wmpn_toom32_mul" proved="true">
-   <proof prover="1"><result status="valid" time="0.23"/></proof>
+   <proof prover="1"><result status="valid" time="0.10"/></proof>
    </goal>
    <goal name="VC wmpn_toom32_mul.272.19" expl="VC for wmpn_toom32_mul" proved="true">
    <proof prover="1"><result status="valid" time="0.14"/></proof>
@@ -6821,10 +6821,10 @@
    <proof prover="1"><result status="valid" time="0.23"/></proof>
    </goal>
    <goal name="VC wmpn_toom32_mul.358.1" expl="VC for wmpn_toom32_mul" proved="true">
-   <proof prover="1"><result status="valid" time="0.08"/></proof>
+   <proof prover="1"><result status="valid" time="0.09"/></proof>
    </goal>
    <goal name="VC wmpn_toom32_mul.358.2" expl="VC for wmpn_toom32_mul" proved="true">
-   <proof prover="1"><result status="valid" time="0.09"/></proof>
+   <proof prover="1"><result status="valid" time="0.08"/></proof>
    </goal>
    <goal name="VC wmpn_toom32_mul.358.3" expl="VC for wmpn_toom32_mul" proved="true">
    <proof prover="1"><result status="valid" time="0.09"/></proof>
@@ -7440,7 +7440,7 @@
   <proof prover="1" memlimit="2000"><result status="valid" time="2.47"/></proof>
   </goal>
   <goal name="VC wmpn_toom32_mul.458" expl="precondition" proved="true">
-  <proof prover="1" memlimit="2000"><result status="valid" time="2.53"/></proof>
+  <proof prover="1" memlimit="2000"><result status="valid" time="3.06"/></proof>
   </goal>
   <goal name="VC wmpn_toom32_mul.459" expl="precondition" proved="true">
   <transf name="inline_goal" proved="true" >
@@ -7516,10 +7516,10 @@
    <proof prover="1" timelimit="1"><result status="valid" time="0.16"/></proof>
    </goal>
    <goal name="VC wmpn_toom32_mul.466.1" expl="VC for wmpn_toom32_mul" proved="true">
-   <proof prover="1" timelimit="1"><result status="valid" time="0.28"/></proof>
+   <proof prover="1" timelimit="1"><result status="valid" time="0.15"/></proof>
    </goal>
    <goal name="VC wmpn_toom32_mul.466.2" expl="VC for wmpn_toom32_mul" proved="true">
-   <proof prover="4"><result status="valid" time="0.64"/></proof>
+   <proof prover="4"><result status="valid" time="0.46"/></proof>
    </goal>
    <goal name="VC wmpn_toom32_mul.466.3" expl="VC for wmpn_toom32_mul" proved="true">
    <proof prover="0"><result status="valid" time="0.04"/></proof>
@@ -7586,10 +7586,10 @@
       <proof prover="1" timelimit="1"><result status="valid" time="0.16"/></proof>
       </goal>
       <goal name="VC wmpn_toom32_mul.473.0.0.0.1" expl="rewrite premises" proved="true">
-      <proof prover="1" timelimit="1"><result status="valid" time="0.14"/></proof>
+      <proof prover="1" timelimit="1"><result status="valid" time="0.26"/></proof>
       </goal>
       <goal name="VC wmpn_toom32_mul.473.0.0.0.2" expl="rewrite premises" proved="true">
-      <proof prover="1" timelimit="1"><result status="valid" time="0.26"/></proof>
+      <proof prover="1" timelimit="1"><result status="valid" time="0.14"/></proof>
       </goal>
      </transf>
      </goal>
@@ -7617,7 +7617,7 @@
    <proof prover="4"><result status="valid" time="0.53"/></proof>
    </goal>
    <goal name="VC wmpn_toom32_mul.474.1" expl="assertion" proved="true">
-   <proof prover="0"><result status="valid" time="3.42"/></proof>
+   <proof prover="0"><result status="valid" time="3.88"/></proof>
    <proof prover="4"><result status="valid" time="0.54"/></proof>
    </goal>
    <goal name="VC wmpn_toom32_mul.474.2" expl="assertion" proved="true">
@@ -7714,7 +7714,7 @@
   <proof prover="1" timelimit="1"><result status="valid" time="0.56"/></proof>
   </goal>
   <goal name="VC wmpn_toom32_mul.488" expl="precondition" proved="true">
-  <proof prover="1" timelimit="1"><result status="valid" time="0.30"/></proof>
+  <proof prover="1" timelimit="1"><result status="valid" time="0.16"/></proof>
   </goal>
   <goal name="VC wmpn_toom32_mul.489" expl="integer overflow" proved="true">
   <proof prover="1" memlimit="2000"><result status="valid" time="0.57"/></proof>
@@ -7957,10 +7957,10 @@
   <goal name="VC wmpn_toom32_mul.516" expl="assertion" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="VC wmpn_toom32_mul.516.0" expl="assertion" proved="true">
-   <proof prover="1" memlimit="2000"><result status="valid" time="4.48"/></proof>
+   <proof prover="1" memlimit="2000"><result status="valid" time="5.11"/></proof>
    </goal>
    <goal name="VC wmpn_toom32_mul.516.1" expl="VC for wmpn_toom32_mul" proved="true">
-   <proof prover="1" memlimit="2000"><result status="valid" time="4.52"/></proof>
+   <proof prover="1" memlimit="2000"><result status="valid" time="5.19"/></proof>
    </goal>
    <goal name="VC wmpn_toom32_mul.516.2" expl="VC for wmpn_toom32_mul" proved="true">
    <proof prover="0"><result status="valid" time="0.89"/></proof>
@@ -7990,7 +7990,7 @@
    </goal>
    <goal name="VC wmpn_toom32_mul.516.6" expl="VC for wmpn_toom32_mul" proved="true">
    <proof prover="0"><result status="valid" time="0.06"/></proof>
-   <proof prover="1" memlimit="2000"><result status="valid" time="4.66"/></proof>
+   <proof prover="1" memlimit="2000"><result status="valid" time="5.28"/></proof>
    </goal>
    <goal name="VC wmpn_toom32_mul.516.7" expl="VC for wmpn_toom32_mul" proved="true">
    <proof prover="0"><result status="valid" time="0.62"/></proof>
@@ -8082,10 +8082,10 @@
    </goal>
    <goal name="VC wmpn_toom32_mul.522.5" expl="VC for wmpn_toom32_mul" proved="true">
    <proof prover="0"><result status="valid" time="0.05"/></proof>
-   <proof prover="1" memlimit="2000"><result status="valid" time="4.10"/></proof>
+   <proof prover="1" memlimit="2000"><result status="valid" time="4.66"/></proof>
    </goal>
    <goal name="VC wmpn_toom32_mul.522.6" expl="VC for wmpn_toom32_mul" proved="true">
-   <proof prover="1" memlimit="2000"><result status="valid" time="4.00"/></proof>
+   <proof prover="1" memlimit="2000"><result status="valid" time="4.58"/></proof>
    <transf name="unfold" proved="true" arg1="value">
     <goal name="VC wmpn_toom32_mul.522.6.0" expl="VC for wmpn_toom32_mul" proved="true">
     <proof prover="1" memlimit="2000"><result status="valid" time="1.71"/></proof>
@@ -8094,10 +8094,10 @@
    </goal>
    <goal name="VC wmpn_toom32_mul.522.7" expl="VC for wmpn_toom32_mul" proved="true">
    <proof prover="0"><result status="valid" time="0.03"/></proof>
-   <proof prover="1" memlimit="2000"><result status="valid" time="4.03"/></proof>
+   <proof prover="1" memlimit="2000"><result status="valid" time="4.61"/></proof>
    </goal>
    <goal name="VC wmpn_toom32_mul.522.8" expl="VC for wmpn_toom32_mul" proved="true">
-   <proof prover="1" memlimit="2000"><result status="valid" time="4.10"/></proof>
+   <proof prover="1" memlimit="2000"><result status="valid" time="4.64"/></proof>
    <transf name="unfold" proved="true" arg1="value">
     <goal name="VC wmpn_toom32_mul.522.8.0" expl="VC for wmpn_toom32_mul" proved="true">
     <proof prover="1" memlimit="2000"><result status="valid" time="1.45"/></proof>
@@ -8592,7 +8592,7 @@
   <proof prover="0"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC wmpn_mul.79" expl="assertion" proved="true">
-  <proof prover="1" timelimit="1"><result status="valid" time="0.16"/></proof>
+  <proof prover="1" timelimit="1"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC wmpn_mul.80" expl="precondition" proved="true">
   <proof prover="1" timelimit="1"><result status="valid" time="0.09"/></proof>
@@ -8633,10 +8633,10 @@
   <proof prover="1" timelimit="1"><result status="valid" time="0.15"/></proof>
   </goal>
   <goal name="VC wmpn_mul.85" expl="precondition" proved="true">
-  <proof prover="5" memlimit="2000"><result status="valid" time="3.14" steps="468"/></proof>
+  <proof prover="5" memlimit="2000"><result status="valid" time="3.78" steps="468"/></proof>
   <transf name="inline_goal" proved="true" >
    <goal name="VC wmpn_mul.85.0" expl="precondition" proved="true">
-   <proof prover="5" memlimit="2000"><result status="valid" time="2.15" steps="250"/></proof>
+   <proof prover="5" memlimit="2000"><result status="valid" time="2.66" steps="250"/></proof>
    </goal>
   </transf>
   </goal>
@@ -8645,7 +8645,7 @@
   </goal>
   <goal name="VC wmpn_mul.87" expl="assertion" proved="true">
   <proof prover="1" timelimit="1"><result status="valid" time="0.21"/></proof>
-  <proof prover="5" memlimit="2000"><result status="valid" time="2.18" steps="240"/></proof>
+  <proof prover="5" memlimit="2000"><result status="valid" time="2.50" steps="240"/></proof>
   </goal>
   <goal name="VC wmpn_mul.88" expl="assertion" proved="true">
   <proof prover="0"><result status="valid" time="0.04"/></proof>
@@ -9496,7 +9496,7 @@
    <proof prover="1" timelimit="1"><result status="valid" time="0.05"/></proof>
    </goal>
    <goal name="VC wmpn_mul.223.5" expl="VC for wmpn_mul" proved="true">
-   <proof prover="1" timelimit="1"><result status="valid" time="0.22"/></proof>
+   <proof prover="1" timelimit="1"><result status="valid" time="0.09"/></proof>
    </goal>
   </transf>
   </goal>
diff --git a/examples/multiprecision/toom/why3shapes.gz b/examples/multiprecision/toom/why3shapes.gz
index e3cd8b2b59dddd898d15026b1fb38722c30f09a8..a58edb3156bba4a523b0012ed88eeba605025f0a 100644
Binary files a/examples/multiprecision/toom/why3shapes.gz and b/examples/multiprecision/toom/why3shapes.gz differ
diff --git a/examples/multiprecision/util/why3session.xml b/examples/multiprecision/util/why3session.xml
index 0d06cd3930489cc04a79e7171888bce95bfe8b1e..4357be82dbb9dd7752a0a14cf148293c3bd22ce0 100644
--- a/examples/multiprecision/util/why3session.xml
+++ b/examples/multiprecision/util/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
diff --git a/examples/multiprecision/util/why3shapes.gz b/examples/multiprecision/util/why3shapes.gz
index 7fd604eb20451369eb07b8f177e2f3e59d356ddb..89a08b793d52d8dc2b3d4a9d62f0f1f5e059aa9e 100644
Binary files a/examples/multiprecision/util/why3shapes.gz and b/examples/multiprecision/util/why3shapes.gz differ
diff --git a/examples/my_cosine/why3session.xml b/examples/my_cosine/why3session.xml
index f82cacab93e4240d4b95dcb40a21ec355ddec6cd..f51b3e2d0ee4f030abf22d898dbef5a156e1a263 100644
--- a/examples/my_cosine/why3session.xml
+++ b/examples/my_cosine/why3session.xml
@@ -1,18 +1,20 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="MetiTarski" version="2.4" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="3" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="4" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../my_cosine.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="my_cosine.mlw"/>
 <theory name="M" proved="true">
  <goal name="VC my_cosine" expl="VC for my_cosine" proved="true">
  <transf name="split_goal_right" proved="true" >
   <goal name="VC my_cosine.0" expl="assertion" proved="true">
   <proof prover="2"><result status="valid" time="0.14"/></proof>
-  <proof prover="3" edited="my_cosine_M_VC_my_cosine_1.v"><result status="valid" time="1.78"/></proof>
+  <proof prover="3" edited="my_cosine_M_VC_my_cosine_1.v"><result status="valid" time="2.26"/></proof>
   </goal>
   <goal name="VC my_cosine.1" expl="precondition" proved="true">
   <proof prover="4"><result status="valid" time="0.01" steps="25"/></proof>
diff --git a/examples/my_cosine/why3shapes.gz b/examples/my_cosine/why3shapes.gz
index d522904b9e182b5faaac04ec30ac67a3aaf0d466..0357417c5c1b7aec2a0e99356f81d14f001ebc95 100644
Binary files a/examples/my_cosine/why3shapes.gz and b/examples/my_cosine/why3shapes.gz differ
diff --git a/examples/prover/Firstorder_symbol_impl/why3session.xml b/examples/prover/Firstorder_symbol_impl/why3session.xml
index ffc149125c3d9d71de0da0bd4794411fd15a0b88..268ec4cce9f501a45aeb7f6e143666ea9f4362ad 100644
--- a/examples/prover/Firstorder_symbol_impl/why3session.xml
+++ b/examples/prover/Firstorder_symbol_impl/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
diff --git a/examples/prover/Firstorder_symbol_impl/why3shapes.gz b/examples/prover/Firstorder_symbol_impl/why3shapes.gz
index f30c04e91ee71790bb27f4195c0cbeba7faf63f2..0adfa857351914bd52690e202bab4adcc19c1da4 100644
Binary files a/examples/prover/Firstorder_symbol_impl/why3shapes.gz and b/examples/prover/Firstorder_symbol_impl/why3shapes.gz differ
diff --git a/examples/prover/Firstorder_tableau_impl/why3session.xml b/examples/prover/Firstorder_tableau_impl/why3session.xml
index c3d581859b604eba9e925204c352b088feeffebe..5805cdbd5c670f896cb8918e4922904e8a0b2e60 100644
--- a/examples/prover/Firstorder_tableau_impl/why3session.xml
+++ b/examples/prover/Firstorder_tableau_impl/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
@@ -147,7 +147,7 @@
  <goal name="VC construct_tableau" expl="VC for construct_tableau" proved="true">
  <transf name="split_goal_right" proved="true" >
   <goal name="VC construct_tableau.0" expl="assertion" proved="true">
-  <proof prover="1"><result status="valid" time="0.18" steps="12"/></proof>
+  <proof prover="1"><result status="valid" time="0.06" steps="12"/></proof>
   </goal>
   <goal name="VC construct_tableau.1" expl="assertion" proved="true">
   <proof prover="1"><result status="valid" time="0.07" steps="12"/></proof>
@@ -168,10 +168,10 @@
   <proof prover="1"><result status="valid" time="0.18" steps="41"/></proof>
   </goal>
   <goal name="VC construct_tableau.7" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.07" steps="45"/></proof>
+  <proof prover="1"><result status="valid" time="0.19" steps="45"/></proof>
   </goal>
   <goal name="VC construct_tableau.8" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.19" steps="45"/></proof>
+  <proof prover="1"><result status="valid" time="0.07" steps="45"/></proof>
   </goal>
   <goal name="VC construct_tableau.9" expl="assertion" proved="true">
   <proof prover="1"><result status="valid" time="0.15" steps="94"/></proof>
diff --git a/examples/prover/Firstorder_tableau_impl/why3shapes.gz b/examples/prover/Firstorder_tableau_impl/why3shapes.gz
index 711c35768cbfaf1d8cd984ad34bc8b489053a6da..7a20e0feb3dd9e2363ff91b466a7181a4d2a4d3f 100644
Binary files a/examples/prover/Firstorder_tableau_impl/why3shapes.gz and b/examples/prover/Firstorder_tableau_impl/why3shapes.gz differ
diff --git a/examples/prover/Firstorder_term_impl/why3session.xml b/examples/prover/Firstorder_term_impl/why3session.xml
index fb666b8d36fa4849c34eb8bdd9a72bb68eb39a68..19739616542e54d1a05f6188df0fc4c735376de2 100644
--- a/examples/prover/Firstorder_term_impl/why3session.xml
+++ b/examples/prover/Firstorder_term_impl/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="1" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
@@ -199,7 +199,7 @@
 </theory>
 <theory name="Impl" proved="true">
  <goal name="VC bind_var_symbol_in_fo_term_list" expl="VC for bind_var_symbol_in_fo_term_list" proved="true">
- <proof prover="0"><result status="valid" time="0.26" steps="1209"/></proof>
+ <proof prover="0"><result status="valid" time="0.39" steps="1209"/></proof>
  </goal>
  <goal name="VC bind_var_fo_term_in_fo_term_list" expl="VC for bind_var_fo_term_in_fo_term_list" proved="true">
  <proof prover="10"><result status="valid" time="1.40"/></proof>
diff --git a/examples/prover/Firstorder_term_impl/why3shapes.gz b/examples/prover/Firstorder_term_impl/why3shapes.gz
index 51e8ac6fdbcad8a4de19c0b70b7e5591bfb8996d..3be37c77409984c74c00768dc02adc8597e186da 100644
Binary files a/examples/prover/Firstorder_term_impl/why3shapes.gz and b/examples/prover/Firstorder_term_impl/why3shapes.gz differ
diff --git a/examples/queens_bv/why3session.xml b/examples/queens_bv/why3session.xml
index 633102dc204eb34a09529831861d65fff8a8f9ae..82c784f67b5b3a447706242da356ed28fbe0e961 100644
--- a/examples/queens_bv/why3session.xml
+++ b/examples/queens_bv/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="5" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
@@ -230,16 +230,16 @@
   <proof prover="3"><result status="valid" time="0.51"/></proof>
   </goal>
   <goal name="VC t.32" expl="precondition" proved="true">
-  <proof prover="3"><result status="valid" time="1.62"/></proof>
+  <proof prover="3"><result status="valid" time="2.15"/></proof>
   </goal>
   <goal name="VC t.33" expl="precondition" proved="true">
   <proof prover="3"><result status="valid" time="2.04"/></proof>
   </goal>
   <goal name="VC t.34" expl="precondition" proved="true">
-  <proof prover="3"><result status="valid" time="2.42"/></proof>
+  <proof prover="3"><result status="valid" time="3.38"/></proof>
   </goal>
   <goal name="VC t.35" expl="assertion" proved="true">
-  <proof prover="3"><result status="valid" time="1.99"/></proof>
+  <proof prover="3"><result status="valid" time="2.39"/></proof>
   </goal>
   <goal name="VC t.36" expl="precondition" proved="true">
   <proof prover="3"><result status="valid" time="0.23"/></proof>
@@ -279,13 +279,13 @@
    <proof prover="10" timelimit="1"><result status="valid" time="0.08" steps="174"/></proof>
    </goal>
    <goal name="VC t.45.1" expl="loop invariant preservation" proved="true">
-   <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="8.98"/></proof>
+   <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="11.57"/></proof>
    </goal>
    <goal name="VC t.45.2" expl="loop invariant preservation" proved="true">
    <proof prover="3" timelimit="1"><result status="valid" time="0.62"/></proof>
    </goal>
    <goal name="VC t.45.3" expl="loop invariant preservation" proved="true">
-   <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.95"/></proof>
+   <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="2.74"/></proof>
    </goal>
   </transf>
   </goal>
@@ -299,7 +299,7 @@
    </goal>
    <goal name="VC t.46.2" expl="loop invariant preservation" proved="true">
    <proof prover="3" timelimit="60"><result status="valid" time="17.51"/></proof>
-   <proof prover="6" timelimit="60"><result status="valid" time="12.69"/></proof>
+   <proof prover="6" timelimit="60"><result status="valid" time="14.24"/></proof>
    </goal>
   </transf>
   </goal>
diff --git a/examples/queens_bv/why3shapes.gz b/examples/queens_bv/why3shapes.gz
index 9f0e82f0dd87ac591f2f7dcab9de1a638ab3ab48..58b5035f9d89427dc6603bcfea8b054cff8bede3 100644
Binary files a/examples/queens_bv/why3shapes.gz and b/examples/queens_bv/why3shapes.gz differ
diff --git a/examples/rightmostbittrick/why3session.xml b/examples/rightmostbittrick/why3session.xml
index 1ba335a8071076bc5f7058fe4028b577f70a6f38..cac3dbb5aaf3694d81e7326628e423dbda4c4eb2 100644
--- a/examples/rightmostbittrick/why3session.xml
+++ b/examples/rightmostbittrick/why3session.xml
@@ -1,11 +1,13 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
-<file name="../rightmostbittrick.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="rightmostbittrick.mlw"/>
 <theory name="Rmbt" proved="true">
  <goal name="VC rightmost_position_set" expl="VC for rightmost_position_set" proved="true">
  <transf name="split_goal_right" proved="true" >
diff --git a/examples/rightmostbittrick/why3shapes.gz b/examples/rightmostbittrick/why3shapes.gz
index c7bc8dade39d7cd46414ebaa9f20eb1d621e6160..8824461badae960c9d0e4aaf1325f47a9e68dfca 100644
Binary files a/examples/rightmostbittrick/why3shapes.gz and b/examples/rightmostbittrick/why3shapes.gz differ
diff --git a/examples/sumrange/why3session.xml b/examples/sumrange/why3session.xml
index 58f8ee7b5c17f26d98cc14abc317546a4d30e2a2..c4919719a174b36643b1ac72434fd3778af96c79 100644
--- a/examples/sumrange/why3session.xml
+++ b/examples/sumrange/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
diff --git a/examples/sumrange/why3shapes.gz b/examples/sumrange/why3shapes.gz
index 2a2dd1e29ed3d1ccd055e20057e358c580fe39cd..3ab7983998fece673d9ed5ebe8dc1fdc05417f8f 100644
Binary files a/examples/sumrange/why3shapes.gz and b/examples/sumrange/why3shapes.gz differ
diff --git a/examples/tests-provers/bv/why3session.xml b/examples/tests-provers/bv/why3session.xml
index d25b27dcbf9d77277b0781ccfbc8f2fa3f437894..0ae694067a60af54f7d90c0a8b0bcf526326ecf7 100644
--- a/examples/tests-provers/bv/why3session.xml
+++ b/examples/tests-provers/bv/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="1" name="CVC3" version="2.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="3" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="5" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="1000"/>
@@ -11,7 +11,9 @@
 <prover id="9" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="11" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="12" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
-<file name="../bv.why">
+<file>
+<path name=".."/>
+<path name="bv.why"/>
 <theory name="CheckBV64">
  <goal name="ok_zero" proved="true">
  <proof prover="1"><result status="valid" time="0.02"/></proof>
@@ -191,7 +193,7 @@
  <proof prover="5"><result status="timeout" time="5.00"/></proof>
  <proof prover="7"><result status="valid" time="0.02"/></proof>
  <proof prover="8"><result status="timeout" time="1.00"/></proof>
- <proof prover="9"><result status="valid" time="0.01"/></proof>
+ <proof prover="9"><result status="valid" time="0.12"/></proof>
  <proof prover="11"><result status="valid" time="0.04" steps="372"/></proof>
  <proof prover="12"><result status="timeout" time="1.00"/></proof>
  </goal>
@@ -655,7 +657,7 @@
  <proof prover="12"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="not_and" proved="true">
- <proof prover="1"><result status="unknown" time="0.82"/></proof>
+ <proof prover="1"><result status="unknown" time="1.01"/></proof>
  <proof prover="3"><result status="valid" time="0.04"/></proof>
  <proof prover="5"><result status="valid" time="0.00"/></proof>
  <proof prover="7"><result status="valid" time="0.02"/></proof>
@@ -712,7 +714,7 @@
  <proof prover="8"><result status="valid" time="0.08"/></proof>
  <proof prover="9"><result status="valid" time="0.88"/></proof>
  <proof prover="11"><result status="timeout" time="1.00"/></proof>
- <proof prover="12"><result status="valid" time="0.18"/></proof>
+ <proof prover="12"><result status="valid" time="0.06"/></proof>
  </goal>
  <goal name="Lsl_Bv_nth_bv_low" proved="true">
  <proof prover="1"><result status="valid" time="0.33"/></proof>
@@ -1043,7 +1045,7 @@
  <proof prover="1"><result status="timeout" time="1.00"/></proof>
  <proof prover="3"><result status="timeout" time="1.00"/></proof>
  <proof prover="5"><result status="timeout" time="5.00"/></proof>
- <proof prover="7"><result status="valid" time="0.01"/></proof>
+ <proof prover="7"><result status="valid" time="0.12"/></proof>
  <proof prover="8"><result status="timeout" time="1.00"/></proof>
  <proof prover="9"><result status="valid" time="0.01"/></proof>
  <proof prover="11"><result status="timeout" time="1.00"/></proof>
@@ -1774,7 +1776,7 @@
  <proof prover="12"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="ok17" proved="true">
- <proof prover="1"><result status="unknown" time="0.82"/></proof>
+ <proof prover="1"><result status="unknown" time="1.01"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  <proof prover="5"><result status="valid" time="0.00"/></proof>
  <proof prover="7"><result status="valid" time="0.01"/></proof>
diff --git a/examples/tests-provers/bv/why3shapes.gz b/examples/tests-provers/bv/why3shapes.gz
index bcce2c5245d60661b8364965a30d0ea503086b6e..0c83d18382da764c75dcb2b1ebe32c6b631d357f 100644
Binary files a/examples/tests-provers/bv/why3shapes.gz and b/examples/tests-provers/bv/why3shapes.gz differ
diff --git a/examples/tests-provers/ceil/why3session.xml b/examples/tests-provers/ceil/why3session.xml
index 4ce717dfff0638cd51076b17c7071b9632d473b9..1476f936e8ab199d95df4d762a165aa18c858a3b 100644
--- a/examples/tests-provers/ceil/why3session.xml
+++ b/examples/tests-provers/ceil/why3session.xml
@@ -1,12 +1,14 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="6" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="8" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../ceil.why" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="ceil.why"/>
 <theory name="Ceil" proved="true">
  <goal name="ceil_obvious" proved="true">
  <proof prover="1"><result status="valid" time="0.01" steps="29"/></proof>
diff --git a/examples/tests-provers/ceil/why3shapes.gz b/examples/tests-provers/ceil/why3shapes.gz
index a36abd9d7556aafadf926dd27dc323619ba54ea4..ed608a559626446255c4457866304d35fee7e7e0 100644
Binary files a/examples/tests-provers/ceil/why3shapes.gz and b/examples/tests-provers/ceil/why3shapes.gz differ
diff --git a/examples/tests-provers/coq-interval/why3session.xml b/examples/tests-provers/coq-interval/why3session.xml
index 66569b90ee1f903beec52c2bd7cfc3df2aa524b2..1379ff0911778a176a8b46f514488f4b0b072b3e 100644
--- a/examples/tests-provers/coq-interval/why3session.xml
+++ b/examples/tests-provers/coq-interval/why3session.xml
@@ -1,12 +1,14 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../coq-interval.why" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="coq-interval.why"/>
 <theory name="P" proved="true">
  <goal name="pow_eps2_max_int" proved="true">
- <proof prover="0" edited="coqmninterval_P_pow_eps2_max_int_1.v"><result status="valid" time="0.86"/></proof>
+ <proof prover="0" edited="coqmninterval_P_pow_eps2_max_int_1.v"><result status="valid" time="1.61"/></proof>
  </goal>
 </theory>
 </file>
diff --git a/examples/tests-provers/coq-interval/why3shapes.gz b/examples/tests-provers/coq-interval/why3shapes.gz
index 7b93db001b8b00580fc508be7506870fa20f3b2e..5838c92dd8c5b5875eac523a66fdf9579663e406 100644
Binary files a/examples/tests-provers/coq-interval/why3shapes.gz and b/examples/tests-provers/coq-interval/why3shapes.gz differ
diff --git a/examples/tests-provers/cvc3/why3session.xml b/examples/tests-provers/cvc3/why3session.xml
index 38189d360bd8dd43e6111bb127b754a098a0a22d..8d31714c7a543d1e3ac19076875d9cd74a2163ac 100644
--- a/examples/tests-provers/cvc3/why3session.xml
+++ b/examples/tests-provers/cvc3/why3session.xml
@@ -1,13 +1,15 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="4" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="6" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="7" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../cvc3.why">
+<file>
+<path name=".."/>
+<path name="cvc3.why"/>
 <theory name="Test">
  <goal name="test1">
  <proof prover="1"><result status="unknown" time="0.00"/></proof>
diff --git a/examples/tests-provers/cvc3/why3shapes.gz b/examples/tests-provers/cvc3/why3shapes.gz
index 334386dbeb254274092dae30d5b330e857c3c96c..993bb91063a7633a14732bfcd21a1a5efab4bdf7 100644
Binary files a/examples/tests-provers/cvc3/why3shapes.gz and b/examples/tests-provers/cvc3/why3shapes.gz differ
diff --git a/examples/tests-provers/div_real/why3session.xml b/examples/tests-provers/div_real/why3session.xml
index b364ec174f760ffc71ddd82a3d701e89aca1366a..36173cc770dc30042c2e278a939bd3e9b21b7346 100644
--- a/examples/tests-provers/div_real/why3session.xml
+++ b/examples/tests-provers/div_real/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="CVC3" version="2.4.1" timelimit="2" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
@@ -10,7 +10,9 @@
 <prover id="10" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="11" name="MetiTarski" version="2.4" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="12" name="Eprover" version="1.8-001" timelimit="2" steplimit="0" memlimit="1000"/>
-<file name="../div_real.why">
+<file>
+<path name=".."/>
+<path name="div_real.why"/>
 <theory name="DivTest">
  <goal name="ok1" proved="true">
  <proof prover="0"><result status="valid" time="0.00"/></proof>
diff --git a/examples/tests-provers/div_real/why3shapes.gz b/examples/tests-provers/div_real/why3shapes.gz
index d6a83fd47d045ee3b639e60484d08ecbb3e978a6..05de078ef7a4df5852e90d24a50f7f774a3015b6 100644
Binary files a/examples/tests-provers/div_real/why3shapes.gz and b/examples/tests-provers/div_real/why3shapes.gz differ
diff --git a/examples/tests-provers/gappa/why3session.xml b/examples/tests-provers/gappa/why3session.xml
index b13b892ea7b257e54a270c66fb927b35214240a6..d799a2fa35e9eebb5ac12b70dcd5829064a3378f 100644
--- a/examples/tests-provers/gappa/why3session.xml
+++ b/examples/tests-provers/gappa/why3session.xml
@@ -1,9 +1,11 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="1" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../gappa.why" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="gappa.why"/>
 <theory name="TestGappa" proved="true">
  <goal name="Round_single_01" proved="true">
  <proof prover="1"><result status="valid" time="0.00"/></proof>
diff --git a/examples/tests-provers/gappa/why3shapes.gz b/examples/tests-provers/gappa/why3shapes.gz
index b210e735434e5f2381c138cffd7ddde9b58a31f9..caf4aa3aa6910a3b7e01530dbf3344c8c558b072 100644
Binary files a/examples/tests-provers/gappa/why3shapes.gz and b/examples/tests-provers/gappa/why3shapes.gz differ
diff --git a/examples/tests-provers/ieee_float/why3session.xml b/examples/tests-provers/ieee_float/why3session.xml
index fbdca81d384f72992dfa48b8c9ac1fc02f5fe9c7..d6ea60b63752efe6d252ee63be7a0f76b2645326 100644
--- a/examples/tests-provers/ieee_float/why3session.xml
+++ b/examples/tests-provers/ieee_float/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Z3" version="4.4.1" alternative="noBV" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="3" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="0" memlimit="1000"/>
@@ -12,7 +12,9 @@
 <prover id="8" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="9" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="10" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../ieee_float.mlw">
+<file>
+<path name=".."/>
+<path name="ieee_float.mlw"/>
 <theory name="A" proved="true">
  <goal name="ebsb32" proved="true">
  <proof prover="0"><result status="valid" time="0.06"/></proof>
@@ -55,7 +57,7 @@
   <proof prover="3"><result status="timeout" time="5.00"/></proof>
   <proof prover="4"><result status="valid" time="1.27"/></proof>
   <proof prover="5"><result status="timeout" time="5.00"/></proof>
-  <proof prover="6"><result status="valid" time="2.82"/></proof>
+  <proof prover="6"><result status="valid" time="4.15"/></proof>
   <proof prover="10"><result status="timeout" time="5.00"/></proof>
   </goal>
   <goal name="VC triplet.4" expl="assertion" proved="true">
@@ -76,7 +78,7 @@
   <proof prover="10"><result status="valid" time="0.08" steps="184"/></proof>
   </goal>
   <goal name="VC triplet.7" expl="assertion" proved="true">
-  <proof prover="6"><result status="valid" time="4.36"/></proof>
+  <proof prover="6"><result status="valid" time="5.01"/></proof>
   <proof prover="7"><result status="timeout" time="5.00"/></proof>
   <proof prover="8"><result status="timeout" time="5.00"/></proof>
   <proof prover="9"><result status="timeout" time="5.00"/></proof>
diff --git a/examples/tests-provers/ieee_float/why3shapes.gz b/examples/tests-provers/ieee_float/why3shapes.gz
index d18a81e30d330d51c10b254b320726f2c37a9e8d..10e3679803a4a8ef7d6e3fb870543a922dc13912 100644
Binary files a/examples/tests-provers/ieee_float/why3shapes.gz and b/examples/tests-provers/ieee_float/why3shapes.gz differ
diff --git a/examples/tests-provers/metitarski/why3session.xml b/examples/tests-provers/metitarski/why3session.xml
index a4b542ccf18b11877606ee81aff8364238eca80f..6a891c517cfdc86703186f5175655c9c2fead805 100644
--- a/examples/tests-provers/metitarski/why3session.xml
+++ b/examples/tests-provers/metitarski/why3session.xml
@@ -1,9 +1,11 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="1" name="MetiTarski" version="2.4" timelimit="5" steplimit="0" memlimit="4000"/>
-<file name="../metitarski.why">
+<file>
+<path name=".."/>
+<path name="metitarski.why"/>
 <theory name="P" proved="true">
  <goal name="x_mul_x_pos" proved="true">
  <proof prover="1" memlimit="1000"><result status="valid" time="0.00"/></proof>
diff --git a/examples/tests-provers/metitarski/why3shapes.gz b/examples/tests-provers/metitarski/why3shapes.gz
index 8fa382e7100dacd799b1da0bd0010373a9d21175..71da0137d516de56573d04b32c61e83b8648e738 100644
Binary files a/examples/tests-provers/metitarski/why3shapes.gz and b/examples/tests-provers/metitarski/why3shapes.gz differ
diff --git a/examples/tests-provers/polypaver/why3session.xml b/examples/tests-provers/polypaver/why3session.xml
index 803cbc3b7ce2f7d8cffe6cf752d63e2d8de5d959..3745b460e96f14c65192b6e0d5204fa80d6ed4e2 100644
--- a/examples/tests-provers/polypaver/why3session.xml
+++ b/examples/tests-provers/polypaver/why3session.xml
@@ -1,9 +1,11 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="PolyPaver" version="0.3" timelimit="3600" steplimit="0" memlimit="1000"/>
-<file name="../polypaver.why">
+<file>
+<path name=".."/>
+<path name="polypaver.why"/>
 <theory name="TestReal">
  <goal name="add1">
  <proof prover="0"><result status="unknown" time="0.01"/></proof>
diff --git a/examples/tests-provers/polypaver/why3shapes.gz b/examples/tests-provers/polypaver/why3shapes.gz
index 1904637a293223b064ee57a026c1a5b61a7a9033..21aae37249a19c19d184e692e3215b26e8cac65a 100644
Binary files a/examples/tests-provers/polypaver/why3shapes.gz and b/examples/tests-provers/polypaver/why3shapes.gz differ
diff --git a/examples/verifythis_2018_array_based_queuing_lock_2/why3session.xml b/examples/verifythis_2018_array_based_queuing_lock_2/why3session.xml
index 46556b61874d024da81a98eb0c23581671b018ea..8bce65d0b5a1ec03f7c52c6ad50ad2ca2a6c9c5d 100644
--- a/examples/verifythis_2018_array_based_queuing_lock_2/why3session.xml
+++ b/examples/verifythis_2018_array_based_queuing_lock_2/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="0" name="Eprover" version="1.9.1-001" timelimit="5" steplimit="0" memlimit="2000"/>
 <prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
@@ -300,7 +300,7 @@
   <proof prover="0" timelimit="60" memlimit="1000"><result status="valid" time="0.10"/></proof>
   </goal>
   <goal name="VC main.39" expl="loop invariant preservation" proved="true">
-  <proof prover="0"><result status="valid" time="2.19"/></proof>
+  <proof prover="0"><result status="valid" time="1.71"/></proof>
   </goal>
   <goal name="VC main.40" expl="loop invariant preservation" proved="true">
   <proof prover="4"><result status="valid" time="0.11" steps="34"/></proof>
@@ -1191,7 +1191,7 @@
   <proof prover="4"><result status="valid" time="0.06" steps="80"/></proof>
   </goal>
   <goal name="VC main.144" expl="loop invariant preservation" proved="true">
-  <proof prover="0"><result status="valid" time="1.50"/></proof>
+  <proof prover="0"><result status="valid" time="1.24"/></proof>
   </goal>
   <goal name="VC main.145" expl="loop invariant preservation" proved="true">
   <transf name="split_all_full" proved="true" >
@@ -1217,7 +1217,7 @@
   </transf>
   </goal>
   <goal name="VC main.147" expl="loop invariant preservation" proved="true">
-  <proof prover="0" timelimit="10" memlimit="1000"><result status="valid" time="1.93"/></proof>
+  <proof prover="0" timelimit="10" memlimit="1000"><result status="valid" time="1.62"/></proof>
   <transf name="split_all_full" proved="true" >
    <goal name="VC main.147.0" expl="VC for main" proved="true">
    <proof prover="5"><result status="valid" time="0.18"/></proof>
@@ -1583,7 +1583,7 @@
    <proof prover="4"><result status="valid" time="0.22" steps="284"/></proof>
    </goal>
    <goal name="VC main.213.1" expl="assertion" proved="true">
-   <proof prover="4"><result status="valid" time="0.98" steps="734"/></proof>
+   <proof prover="4"><result status="valid" time="1.18" steps="734"/></proof>
    </goal>
    <goal name="VC main.213.2" expl="assertion" proved="true">
    <proof prover="4" memlimit="2000"><result status="valid" time="0.03" steps="66"/></proof>
@@ -1706,7 +1706,7 @@
    <goal name="VC main.224.0" expl="VC for main" proved="true">
    <transf name="introduce_premises" proved="true" >
     <goal name="VC main.224.0.0" expl="VC for main" proved="true">
-    <proof prover="2" timelimit="30" memlimit="4000"><result status="valid" time="10.20" steps="3253"/></proof>
+    <proof prover="2" timelimit="30" memlimit="4000"><result status="valid" time="10.20" steps="3252"/></proof>
     </goal>
    </transf>
    </goal>
diff --git a/examples/verifythis_2018_array_based_queuing_lock_2/why3shapes.gz b/examples/verifythis_2018_array_based_queuing_lock_2/why3shapes.gz
index f0b598f0681d4838a5fe6c86560e0f5bc9212f5b..d634039228c0e12331c9346e40d23bd66f5c78db 100644
Binary files a/examples/verifythis_2018_array_based_queuing_lock_2/why3shapes.gz and b/examples/verifythis_2018_array_based_queuing_lock_2/why3shapes.gz differ
diff --git a/examples/vstte10_queens/why3session.xml b/examples/vstte10_queens/why3session.xml
index f279436da060bcfff9ff2ee9f2b79dfdc2029e1e..22e5d25a767128d880b1502035a33e2b1dfcef87 100644
--- a/examples/vstte10_queens/why3session.xml
+++ b/examples/vstte10_queens/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="2" name="Z3" version="3.2" timelimit="8" steplimit="0" memlimit="1000"/>
 <prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="4" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
diff --git a/examples/vstte10_queens/why3shapes.gz b/examples/vstte10_queens/why3shapes.gz
index 893871635192c72f1bf966449c6a608a4778a2d6..7e701cbb24964fb2a7dde1800152fcee8cc4be84 100644
Binary files a/examples/vstte10_queens/why3shapes.gz and b/examples/vstte10_queens/why3shapes.gz differ