updated session files for 57a980a9

examples/programs/binary_search/why3session.xml

@@ -2,7 +2,7 @@
 <!DOCTYPE why3session SYSTEM "why3session.dtd">
 <why3session name="examples/programs/binary_search/why3session.xml">
  <file name="../binary_search.mlw" verified="true" expanded="true">
-  <theory name="M" verified="true" expanded="true">
+  <theory name="WP M" verified="true" expanded="true">
    <goal name="WP_parameter binary_search" expl="correctness of parameter binary_search" sum="19c8c227fa34ac77ac920a032e72d19f" proved="true" expanded="true">
     <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
      <result status="valid" time="0.06"/>

examples/programs/decrease1/why3session.xml

@@ -2,7 +2,7 @@
 <!DOCTYPE why3session SYSTEM "why3session.dtd">
 <why3session name="examples/programs/decrease1/why3session.xml">
  <file name="../decrease1.mlw" verified="true" expanded="true">
-  <theory name="Decrease1" verified="true" expanded="true">
+  <theory name="WP Decrease1" verified="true" expanded="true">
    <goal name="decrease1_induction" sum="eb0923143934165c0f02dda5dd1d9064" proved="true" expanded="true">
     <proof prover="coq" timelimit="10" edited="decrease1_Decrease1_decrease1_induction_2.v" obsolete="false">
      <result status="valid" time="0.74"/>

examples/programs/euler001/why3session.xml

@@ -84,7 +84,7 @@
     </proof>
    </goal>
   </theory>
-  <theory name="Euler001" verified="true" expanded="true">
+  <theory name="WP Euler001" verified="true" expanded="true">
    <goal name="WP_parameter solve" expl="normal postcondition" sum="dd6f0e34463bcfbf4b3ca11577b727c6" proved="true" expanded="true">
     <proof prover="cvc3" timelimit="2" edited="" obsolete="false">
      <result status="valid" time="0.46"/>

examples/programs/fact/why3session.xml

@@ -4,14 +4,14 @@
  <file name="../fact.mlw" verified="true" expanded="true">
   <theory name="Fact" verified="true" expanded="true">
   </theory>
-  <theory name="FactRecursive" verified="true" expanded="true">
+  <theory name="WP FactRecursive" verified="true" expanded="true">
    <goal name="WP_parameter fact_rec" expl="correctness of parameter fact_rec" sum="26ddbd98b20d38d8cc8174af1ddddb03" proved="true" expanded="true">
     <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
      <result status="valid" time="0.02"/>
     </proof>
    </goal>
   </theory>
-  <theory name="FactImperative" verified="true" expanded="true">
+  <theory name="WP FactImperative" verified="true" expanded="true">
    <goal name="WP_parameter fact_imp" expl="correctness of parameter fact_imp" sum="e351701b7425629858770982d2abae90" proved="true" expanded="true">
     <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
      <result status="valid" time="0.03"/>

examples/programs/flag/why3session.xml

@@ -2,7 +2,7 @@
 <!DOCTYPE why3session SYSTEM "why3session.dtd">
 <why3session name="examples/programs/flag/why3session.xml">
  <file name="../flag.mlw" verified="true" expanded="true">
-  <theory name="Flag" verified="true" expanded="true">
+  <theory name="WP Flag" verified="true" expanded="true">
    <goal name="WP_parameter swap" expl="correctness of parameter swap" sum="6609450a85dcd0bb3edb249306486e4b" proved="true" expanded="true">
     <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
      <result status="valid" time="0.03"/>

examples/programs/gcd/why3session.xml

@@ -2,7 +2,7 @@
 <!DOCTYPE why3session SYSTEM "why3session.dtd">
 <why3session name="examples/programs/gcd/why3session.xml">
  <file name="../gcd.mlw" verified="false" expanded="true">
-  <theory name="M" verified="false" expanded="true">
+  <theory name="WP M" verified="false" expanded="true">
    <goal name="WP_parameter gcd" expl="correctness of parameter gcd" sum="13686aa7223ccd074e11892070fa497c" proved="false" expanded="true">
     <transf name="split_goal" proved="false" expanded="true">
      <goal name="WP_parameter gcd.1" expl="normal postcondition" sum="e04458a1deb8f46c32e2040984924ab2" proved="true" expanded="true">

examples/programs/gcd_bezout/why3session.xml

@@ -2,7 +2,7 @@
 <!DOCTYPE why3session SYSTEM "why3session.dtd">
 <why3session name="examples/programs/gcd_bezout/why3session.xml">
  <file name="../gcd_bezout.mlw" verified="false" expanded="true">
-  <theory name="M" verified="false" expanded="true">
+  <theory name="WP M" verified="false" expanded="true">
    <goal name="WP_parameter gcd" expl="correctness of parameter gcd" sum="66a8795f899d84ac0583a005fe89ce0a" proved="false" expanded="true">
     <transf name="split_goal" proved="false" expanded="true">
      <goal name="WP_parameter gcd.1" expl="loop invariant init" sum="131bc5920f4ba44c45ffaa828fa737f7" proved="true" expanded="true">

examples/programs/insertion_sort/why3session.xml

@@ -2,7 +2,7 @@
 <!DOCTYPE why3session SYSTEM "why3session.dtd">
 <why3session name="examples/programs/insertion_sort/why3session.xml">
  <file name="../insertion_sort.mlw" verified="false" expanded="true">
-  <theory name="InsertionSort" verified="false" expanded="true">
+  <theory name="WP InsertionSort" verified="false" expanded="true">
    <goal name="WP_parameter insertion_sort" expl="correctness of parameter insertion_sort" sum="57abb18bfe1fef7ae3c780ae9f60e312" proved="false" expanded="true">
     <transf name="split_goal" proved="false" expanded="true">
      <goal name="WP_parameter insertion_sort.1" expl="normal postcondition" sum="9a49382bffbb4e30273c672cda27a668" proved="true" expanded="false">

examples/programs/insertion_sort_list/why3session.xml

@@ -2,7 +2,7 @@
 <!DOCTYPE why3session SYSTEM "why3session.dtd">
 <why3session name="examples/programs/insertion_sort_list/why3session.xml">
  <file name="../insertion_sort_list.mlw" verified="true" expanded="true">
-  <theory name="M" verified="true" expanded="true">
+  <theory name="WP M" verified="true" expanded="true">
    <goal name="WP_parameter insert" expl="correctness of parameter insert" sum="1ab3de41db4f19ec372372833aaeb2c0" proved="true" expanded="true">
     <transf name="split_goal" proved="true" expanded="true">
      <goal name="WP_parameter insert.1" expl="correctness of parameter insert" sum="76ce5493fcb11812e4e0e2698821a9c7" proved="true" expanded="true">

examples/programs/isqrt/why3session.xml

@@ -2,7 +2,7 @@
 <!DOCTYPE why3session SYSTEM "why3session.dtd">
 <why3session name="examples/programs/isqrt/why3session.xml">
  <file name="../isqrt.mlw" verified="true" expanded="true">
-  <theory name="M" verified="true" expanded="true">
+  <theory name="WP M" verified="true" expanded="true">
    <goal name="WP_parameter isqrt" expl="correctness of parameter isqrt" sum="5c9a0a28616c8a34d7fb4e3e77a12070" proved="true" expanded="true">
     <proof prover="cvc3" timelimit="2" edited="" obsolete="false">
      <result status="valid" time="0.01"/>

examples/programs/list_rev/why3session.xml

@@ -2,7 +2,7 @@
 <!DOCTYPE why3session SYSTEM "why3session.dtd">
 <why3session name="examples/programs/list_rev/why3session.xml">
  <file name="../list_rev.mlw" verified="false" expanded="true">
-  <theory name="M" verified="false" expanded="true">
+  <theory name="WP M" verified="false" expanded="true">
    <goal name="acyclic_list" sum="05ff1ad20f5af90fc986f7d1deb8acbf" proved="false" expanded="true">
    </goal>
    <goal name="consistent" sum="678d57b4a5464ed1788c9284cd3deb14" proved="false" expanded="true">
@@ -17,7 +17,7 @@
    <goal name="WP_parameter list_rev_behv" expl="correctness of parameter list_rev_behv" sum="4087cd4ed78b8c5468550eec66d4564d" proved="false" expanded="true">
    </goal>
   </theory>
-  <theory name="M2" verified="false" expanded="true">
+  <theory name="WP M2" verified="false" expanded="true">
    <goal name="is_list_disjoint_case" sum="db8d14254ea7d12f7f7bbb446ee006eb" proved="true" expanded="true">
     <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
      <result status="valid" time="0.01"/>

examples/programs/mac_carthy/why3session.xml

@@ -2,7 +2,7 @@
 <!DOCTYPE why3session SYSTEM "why3session.dtd">
 <why3session name="examples/programs/mac_carthy/why3session.xml">
  <file name="../mac_carthy.mlw" verified="true" expanded="true">
-  <theory name="M" verified="true" expanded="true">
+  <theory name="WP M" verified="true" expanded="true">
    <goal name="WP_parameter f91" expl="correctness of parameter f91" sum="7abacd70509916020a75c246a162149a" proved="true" expanded="true">
     <proof prover="cvc3" timelimit="2" edited="" obsolete="false">
      <result status="valid" time="0.00"/>

examples/programs/meta.why

-theory Partial
-  meta "enco_kept" "instantiate"
-end
-
-theory Partial_incomplete
-  meta "encoding_instantiate : complete" "no"
-end
-
-theory Explicit
-
-end
\ No newline at end of file

examples/programs/my_cosine/why3session.xml

@@ -2,7 +2,7 @@
 <!DOCTYPE why3session SYSTEM "why3session.dtd">
 <why3session name="examples/programs/my_cosine/why3session.xml">
  <file name="../my_cosine.mlw" verified="true" expanded="true">
-  <theory name="M" verified="true" expanded="true">
+  <theory name="WP M" verified="true" expanded="true">
    <goal name="WP_parameter my_cosine" expl="correctness of parameter my_cosine" sum="dd173c4f589edbafa4fba6e5a9ea3037" proved="true" expanded="true">
     <transf name="split_goal" proved="true" expanded="true">
      <goal name="WP_parameter my_cosine.1" expl="assertion" sum="42f9206597da619fa67e4871bf991914" proved="true" expanded="true">

examples/programs/power/why3session.xml

@@ -30,7 +30,7 @@
     </proof>
    </goal>
   </theory>
-  <theory name="M" verified="true" expanded="true">
+  <theory name="WP M" verified="true" expanded="true">
    <goal name="WP_parameter fast_exp" expl="correctness of parameter fast_exp" sum="ada75a97b847f6c89f173745c047f4f6" proved="true" expanded="true">
     <proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
      <result status="valid" time="0.10"/>

examples/programs/quicksort/why3session.xml

@@ -2,7 +2,7 @@
 <!DOCTYPE why3session SYSTEM "why3session.dtd">
 <why3session name="examples/programs/quicksort/why3session.xml">
  <file name="../quicksort.mlw" verified="false" expanded="true">
-  <theory name="Quicksort" verified="false" expanded="true">
+  <theory name="WP Quicksort" verified="false" expanded="true">
    <goal name="WP_parameter swap" expl="correctness of parameter swap" sum="e75f744f287ab933e3389b0e4eef5b9a" proved="true" expanded="false">
     <proof prover="alt-ergo" timelimit="29" edited="" obsolete="false">
      <result status="valid" time="0.02"/>

examples/programs/same_fringe/why3session.xml

@@ -2,7 +2,7 @@
 <!DOCTYPE why3session SYSTEM "why3session.dtd">
 <why3session name="examples/programs/same_fringe/why3session.xml">
  <file name="../same_fringe.mlw" verified="true" expanded="true">
-  <theory name="SameFringe" verified="true" expanded="true">
+  <theory name="WP SameFringe" verified="true" expanded="true">
    <goal name="WP_parameter enum" expl="correctness of parameter enum" sum="837cc2fd8bfff836407e3e8e9f570e95" proved="true" expanded="true">
     <transf name="split_goal" proved="true" expanded="true">
      <goal name="WP_parameter enum.1" expl="correctness of parameter enum" sum="ff13de762a4ee83598a46a358059e421" proved="true" expanded="true">

examples/programs/selection_sort/why3session.xml

@@ -2,7 +2,7 @@
 <!DOCTYPE why3session SYSTEM "why3session.dtd">
 <why3session name="examples/programs/selection_sort/why3session.xml">
  <file name="../selection_sort.mlw" verified="true" expanded="true">
-  <theory name="Quicksort" verified="true" expanded="true">
+  <theory name="WP Quicksort" verified="true" expanded="true">
    <goal name="WP_parameter swap" expl="correctness of parameter swap" sum="c4e2099b76e6218e14497a80c67ee8b1" proved="true" expanded="true">
     <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
      <result status="valid" time="0.04"/>

examples/programs/vacid_0_sparse_array/why3session.xml

@@ -2,7 +2,7 @@
 <!DOCTYPE why3session SYSTEM "why3session.dtd">
 <why3session name="examples/programs/vacid_0_sparse_array/why3session.xml">
  <file name="../vacid_0_sparse_array.mlw" verified="false" expanded="true">
-  <theory name="SparseArray" verified="false" expanded="true">
+  <theory name="WP SparseArray" verified="false" expanded="true">
    <goal name="permutation" sum="943c7f25c8660c6df0bfe43dc914ff71" proved="false" expanded="true">
    </goal>
    <goal name="WP_parameter create" expl="normal postcondition" sum="1f24bd185e1398b437b641f18bc8b070" proved="true" expanded="true">
@@ -89,7 +89,7 @@
     </transf>
    </goal>
   </theory>
-  <theory name="Harness" verified="true" expanded="true">
+  <theory name="WP Harness" verified="true" expanded="true">
    <goal name="WP_parameter harness" expl="correctness of parameter harness" sum="8873e825b12ef6fbb5639c07204eb96d" proved="true" expanded="true">
     <transf name="split_goal" proved="true" expanded="true">
      <goal name="WP_parameter harness.1" expl="precondition" sum="fbbd547dc71f749d05e0e4f15bb5d781" proved="true" expanded="true">

examples/programs/vstte10_aqueue/why3session.xml

@@ -2,7 +2,7 @@
 <!DOCTYPE why3session SYSTEM "why3session.dtd">
 <why3session name="examples/programs/vstte10_aqueue/why3session.xml">
  <file name="../vstte10_aqueue.mlw" verified="true" expanded="true">
-  <theory name="AmortizedQueue" verified="true" expanded="true">
+  <theory name="WP AmortizedQueue" verified="true" expanded="true">
    <goal name="WP_parameter create" expl="correctness of parameter create" sum="94603ee07e585f398458946ecc7a0f0b" proved="true" expanded="true">
     <proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
      <result status="valid" time="0.50"/>