Merge branch 'model_record' into 'master'

Model record

See merge request !83

bench/ce/oracles/double_projection_CVC4,1.5_SP.oracle

@@ -2,13 +2,10 @@ Strongest Postcondition
 bench/ce/double_projection.mlw Test VC f: Timeout or Unknown
 Counter-example model:File double_projection.mlw:
 Line 17:
-x, [[@introduced]] = {"type" : "Record" ,
-"val" : {"Field" : [{"field" : "c" , "value" : {"type" : "Integer" ,
-"val" : "1" } }, {"field" : "d" , "value" : {"type" : "Integer" ,
-"val" : "0" } }] } }
+x, [[@introduced]] = {"proj_name" : "c" , "type" : "Proj" ,
+"value" : {"type" : "Integer" , "val" : "1" } }
 Line 19:
-x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
-"val" : {"Field" : [{"field" : "c" , "value" : {"type" : "Integer" ,
-"val" : "1" } }, {"field" : "d" , "value" : {"type" : "Integer" ,
-"val" : "0" } }] } }
+x, [[@introduced], [@model_trace:x]] = {"proj_name" : "c" , "type" : "Proj" ,
+"value" : {"type" : "Integer" ,
+"val" : "1" } }
 

bench/ce/oracles/double_projection_CVC4,1.5_WP.oracle

@@ -2,13 +2,10 @@ Weakest Precondition
 bench/ce/double_projection.mlw Test VC f: Timeout or Unknown
 Counter-example model:File double_projection.mlw:
 Line 17:
-x, [[@introduced]] = {"type" : "Record" ,
-"val" : {"Field" : [{"field" : "c" , "value" : {"type" : "Integer" ,
-"val" : "1" } }, {"field" : "d" , "value" : {"type" : "Integer" ,
-"val" : "0" } }] } }
+x, [[@introduced]] = {"proj_name" : "c" , "type" : "Proj" ,
+"value" : {"type" : "Integer" , "val" : "1" } }
 Line 19:
-x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
-"val" : {"Field" : [{"field" : "c" , "value" : {"type" : "Integer" ,
-"val" : "1" } }, {"field" : "d" , "value" : {"type" : "Integer" ,
-"val" : "0" } }] } }
+x, [[@introduced], [@model_trace:x]] = {"proj_name" : "c" , "type" : "Proj" ,
+"value" : {"type" : "Integer" ,
+"val" : "1" } }
 

bench/ce/oracles/double_projection_Z3,4.6.0_SP.oracle

@@ -2,13 +2,10 @@ Strongest Postcondition
 bench/ce/double_projection.mlw Test VC f: Unknown (sat)
 Counter-example model:File double_projection.mlw:
 Line 17:
-x, [[@introduced]] = {"type" : "Record" ,
-"val" : {"Field" : [{"field" : "c" , "value" : {"type" : "Integer" ,
-"val" : "1" } }, {"field" : "d" , "value" : {"type" : "Integer" ,
-"val" : "0" } }] } }
+x, [[@introduced]] = {"proj_name" : "c" , "type" : "Proj" ,
+"value" : {"type" : "Integer" , "val" : "1" } }
 Line 19:
-x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
-"val" : {"Field" : [{"field" : "c" , "value" : {"type" : "Integer" ,
-"val" : "1" } }, {"field" : "d" , "value" : {"type" : "Integer" ,
-"val" : "0" } }] } }
+x, [[@introduced], [@model_trace:x]] = {"proj_name" : "c" , "type" : "Proj" ,
+"value" : {"type" : "Integer" ,
+"val" : "1" } }
 

bench/ce/oracles/double_projection_Z3,4.6.0_WP.oracle

@@ -2,13 +2,10 @@ Weakest Precondition
 bench/ce/double_projection.mlw Test VC f: Unknown (sat)
 Counter-example model:File double_projection.mlw:
 Line 17:
-x, [[@introduced]] = {"type" : "Record" ,
-"val" : {"Field" : [{"field" : "c" , "value" : {"type" : "Integer" ,
-"val" : "1" } }, {"field" : "d" , "value" : {"type" : "Integer" ,
-"val" : "0" } }] } }
+x, [[@introduced]] = {"proj_name" : "c" , "type" : "Proj" ,
+"value" : {"type" : "Integer" , "val" : "1" } }
 Line 19:
-x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
-"val" : {"Field" : [{"field" : "c" , "value" : {"type" : "Integer" ,
-"val" : "1" } }, {"field" : "d" , "value" : {"type" : "Integer" ,
-"val" : "0" } }] } }
+x, [[@introduced], [@model_trace:x]] = {"proj_name" : "c" , "type" : "Proj" ,
+"value" : {"type" : "Integer" ,
+"val" : "1" } }
 

examples/algo63/why3session.xml

@@ -3,7 +3,9 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="5">
 <prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
-<file name="../algo63.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="algo63.mlw"/>
 <theory name="Algo63" proved="true">
  <goal name="VC exchange" expl="VC for exchange" proved="true">
  <proof prover="0"><result status="valid" time="0.03" steps="63"/></proof>

examples/algo63_fastwp/why3session.xml

@@ -3,7 +3,9 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="5">
 <prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../algo63.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="algo63.mlw"/>
 <theory name="Algo63" proved="true">
  <goal name="VC exchange" expl="VC for exchange" proved="true">
  <transf name="split_goal_right" proved="true" >

examples/algo64/why3session.xml

@@ -3,7 +3,9 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="5">
 <prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
-<file name="../algo64.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="algo64.mlw"/>
 <theory name="Algo64" proved="true">
  <goal name="VC quicksort" expl="VC for quicksort" proved="true">
  <proof prover="1"><result status="valid" time="0.67" steps="1799"/></proof>

examples/algo65/why3session.xml

@@ -3,7 +3,9 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="5">
 <prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
-<file name="../algo65.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="algo65.mlw"/>
 <theory name="Algo65" proved="true">
  <goal name="VC find" expl="VC for find" proved="true">
  <proof prover="1"><result status="valid" time="0.52" steps="1756"/></proof>

examples/all_distinct/why3session.xml

@@ -3,7 +3,9 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="5">
 <prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
-<file name="../all_distinct.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="all_distinct.mlw"/>
 <theory name="AllDistinct" proved="true">
  <goal name="VC all_distinct" expl="VC for all_distinct" proved="true">
  <proof prover="1"><result status="valid" time="0.06" steps="263"/></proof>

examples/arm/why3session.xml

@@ -3,7 +3,9 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="5">
 <prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../arm.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="arm.mlw"/>
 <theory name="M" proved="true">
  <goal name="VC insertion_sort" expl="VC for insertion_sort" proved="true">
  <proof prover="1"><result status="valid" time="0.11" steps="137"/></proof>

examples/assigning_meanings_to_programs/why3session.xml

@@ -3,7 +3,9 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="5">
 <prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
-<file name="../assigning_meanings_to_programs.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="assigning_meanings_to_programs.mlw"/>
 <theory name="Sum" proved="true">
  <goal name="VC sum" expl="VC for sum" proved="true">
  <proof prover="0"><result status="valid" time="0.01" steps="39"/></proof>

examples/avl/priority_queue/why3session.xml

@@ -5,7 +5,9 @@
 <prover id="1" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="3" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="4" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
-<file name="../priority_queue.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="priority_queue.mlw"/>
 <theory name="PQueue" proved="true">
  <goal name="M.VC assoc_m" expl="VC for assoc_m" proved="true">
  <transf name="split_goal_right" proved="true" >
@@ -507,7 +509,7 @@
   <proof prover="4"><result status="valid" time="0.03" steps="67"/></proof>
   </goal>
   <goal name="VC remove_count.1" expl="postcondition" proved="true">
-  <proof prover="1" timelimit="10"><result status="valid" time="5.42"/></proof>
+  <proof prover="1" timelimit="10"><result status="valid" time="4.69"/></proof>
   </goal>
   <goal name="VC remove_count.2" expl="postcondition" proved="true">
   <proof prover="1" timelimit="10"><result status="valid" time="0.47"/></proof>

examples/avl/ral/why3session.xml

@@ -3,7 +3,9 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="5">
 <prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
-<file name="../ral.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="ral.mlw"/>
 <theory name="RAL" proved="true">
  <goal name="M.assoc" proved="true">
  <proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>

examples/avl/tables/why3session.xml

@@ -4,7 +4,9 @@
 <why3session shape_version="5">
 <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="1" steplimit="0" memlimit="1000"/>
-<file name="../tables.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="tables.mlw"/>
 <theory name="MapBase" proved="true">
  <goal name="M.VC neutral_" expl="VC for neutral_" proved="true">
  <proof prover="5"><result status="valid" time="0.01" steps="4"/></proof>
@@ -410,25 +412,25 @@
   <proof prover="5"><result status="valid" time="0.29" steps="569"/></proof>
   </goal>
   <goal name="VC join.1" expl="precondition" proved="true">
-  <proof prover="5" timelimit="5"><result status="valid" time="1.86" steps="2988"/></proof>
+  <proof prover="5" timelimit="5"><result status="valid" time="1.86" steps="3052"/></proof>
   </goal>
   <goal name="VC join.2" expl="postcondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.63" steps="875"/></proof>
+  <proof prover="5"><result status="valid" time="0.63" steps="880"/></proof>
   </goal>
   <goal name="VC join.3" expl="postcondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.86" steps="960"/></proof>
+  <proof prover="5"><result status="valid" time="0.86" steps="963"/></proof>
   </goal>
   <goal name="VC join.4" expl="postcondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.71" steps="1068"/></proof>
+  <proof prover="5"><result status="valid" time="0.71" steps="1073"/></proof>
   </goal>
   <goal name="VC join.5" expl="postcondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.70" steps="917"/></proof>
+  <proof prover="5"><result status="valid" time="0.70" steps="929"/></proof>
   </goal>
   <goal name="VC join.6" expl="postcondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.51" steps="790"/></proof>
+  <proof prover="5"><result status="valid" time="0.51" steps="772"/></proof>
   </goal>
   <goal name="VC join.7" expl="postcondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.04" steps="51"/></proof>
+  <proof prover="5"><result status="valid" time="0.04" steps="52"/></proof>
   </goal>
  </transf>
  </goal>

examples/bag/why3session.xml

@@ -5,7 +5,9 @@
 <prover id="0" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../bag.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="bag.mlw"/>
 <theory name="BagSpec" proved="true">
  <goal name="VC t" expl="VC for t" proved="true">
  <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>

examples/balance/why3session.xml

@@ -3,7 +3,9 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="5">
 <prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../balance.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="balance.mlw"/>
 <theory name="Puzzle8" proved="true">
  <goal name="VC solve3" expl="VC for solve3" proved="true">
  <proof prover="1"><result status="valid" time="0.02" steps="52"/></proof>

examples/bellman_ford/why3session.xml

@@ -4,7 +4,9 @@
 <why3session shape_version="5">
 <prover id="0" name="Eprover" version="2.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
-<file name="../bellman_ford.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="bellman_ford.mlw"/>
 <theory name="Graph" proved="true">
  <goal name="vertices_cardinal_pos" proved="true">
  <proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
@@ -103,7 +105,7 @@
 </theory>
 <theory name="BellmanFord" proved="true">
  <goal name="VC initialize_single_source" expl="VC for initialize_single_source" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="7"/></proof>
  </goal>
  <goal name="VC inv2_path" expl="VC for inv2_path" proved="true">
  <transf name="split_goal_right" proved="true" >

examples/binary_search/why3session.xml

@@ -3,7 +3,9 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="5">
 <prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
-<file name="../binary_search.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="binary_search.mlw"/>
 <theory name="BinarySearch" proved="true">
  <goal name="VC binary_search" expl="VC for binary_search" proved="true">
  <proof prover="0"><result status="valid" time="0.05" steps="132"/></proof>

examples/binary_search_vc_sp/why3session.xml

@@ -3,7 +3,9 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="5">
 <prover id="0" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
-<file name="../binary_search_vc_sp.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="binary_search_vc_sp.mlw"/>
 <theory name="BinarySearch" proved="true">
  <goal name="VC binary_search" expl="VC for binary_search" proved="true">
  <proof prover="0"><result status="valid" time="0.04"/></proof>

examples/binary_sort/why3session.xml

@@ -4,7 +4,9 @@
 <why3session shape_version="5">
 <prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="8" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../binary_sort.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="binary_sort.mlw"/>
 <theory name="BinarySort" proved="true">
  <goal name="VC occ_shift" expl="VC for occ_shift" proved="true">
  <proof prover="0"><result status="valid" time="0.54"/></proof>

examples/binomial_heap/why3session.xml

@@ -6,7 +6,9 @@
 <prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Eprover" version="1.8-001" timelimit="10" steplimit="0" memlimit="1000"/>
 <prover id="4" name="Z3" version="4.5.0" timelimit="10" steplimit="0" memlimit="1000"/>
-<file name="../binomial_heap.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="binomial_heap.mlw"/>
 <theory name="BinomialHeap" proved="true">
  <goal name="VC size_nonnneg" expl="VC for size_nonnneg" proved="true">
  <proof prover="4"><result status="valid" time="0.02"/></proof>

examples/bitvector_examples/why3session.xml

@@ -4,7 +4,9 @@
 <why3session shape_version="5">
 <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 name="../bitvector_examples.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="bitvector_examples.mlw"/>
 <theory name="Test_proofinuse" proved="true">
  <goal name="VC shift_is_div" expl="VC for shift_is_div" proved="true">
  <proof prover="0"><result status="valid" time="0.06" steps="117"/></proof>

examples/bitwalker/why3session.xml

@@ -8,7 +8,9 @@
 <prover id="3" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="11" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="12" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
-<file name="../bitwalker.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="bitwalker.mlw"/>
 <theory name="Bitwalker" proved="true">
  <goal name="nth64" proved="true">
  <proof prover="0"><result status="valid" time="0.02" steps="90"/></proof>

examples/bts/116_array_access/why3session.xml

@@ -2,7 +2,9 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="5">
-<file name="../116_array_access.mlw">
+<file>
+<path name=".."/>
+<path name="116_array_access.mlw"/>
 <theory name="Test">
  <goal name="a">
  </goal>

examples/bts/16972/why3session.xml

@@ -3,7 +3,9 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="5">
 <prover id="1" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../16972.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="16972.mlw"/>
 <theory name="M" proved="true">
  <goal name="VC fail" expl="VC for fail" proved="true">
  <proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>

examples/bubble_sort/why3session.xml

@@ -3,7 +3,9 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="5">
 <prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../bubble_sort.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="bubble_sort.mlw"/>
 <theory name="BubbleSort" proved="true">
  <goal name="VC bubble_sort" expl="VC for bubble_sort" proved="true">
  <transf name="split_goal_right" proved="true" >

examples/coincidence_count/why3session.xml

@@ -3,7 +3,9 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="5">
 <prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
-<file name="../coincidence_count.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="coincidence_count.mlw"/>
 <theory name="CoincidenceCount" proved="true">
  <goal name="drop_left" proved="true">
  <proof prover="0" timelimit="5"><result status="valid" time="0.15" steps="288"/></proof>

examples/conjugate/why3session.xml

@@ -3,7 +3,9 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="5">
 <prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../conjugate.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="conjugate.mlw"/>
 <theory name="Conjugate" proved="true">
  <goal name="VC conjugate" expl="VC for conjugate" proved="true">
  <proof prover="1"><result status="valid" time="0.13" steps="277"/></proof>

examples/counting_sort/why3session.xml

@@ -4,7 +4,9 @@
 <why3session shape_version="5">
 <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"/>
-<file name="../counting_sort.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="counting_sort.mlw"/>
 <theory name="Spec" proved="true">
  <goal name="VC eqlt" expl="VC for eqlt" proved="true">
  <proof prover="1"><result status="valid" time="0.76" steps="777"/></proof>

examples/cursor_examples/why3session.xml

@@ -5,7 +5,9 @@
 <prover id="3" name="Z3" version="4.6.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="4" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="5" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../cursor_examples.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="cursor_examples.mlw"/>
 <theory name="TestCursor" proved="true">
  <goal name="VC sum" expl="VC for sum" proved="true">
  <proof prover="4"><result status="valid" time="2.86" steps="903"/></proof>

examples/decrease1/why3session.xml

@@ -4,7 +4,9 @@
 <why3session shape_version="5">
 <prover id="1" 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="../decrease1.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="decrease1.mlw"/>
 <theory name="Decrease1" proved="true">
  <goal name="VC decrease1_induction" expl="VC for decrease1_induction" proved="true">
  <proof prover="2"><result status="valid" time="0.02" steps="35"/></proof>

examples/dfa_example/why3session.xml

@@ -7,10 +7,12 @@
 <prover id="5" name="Z3" version="4.6.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="9" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../dfa_example.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="dfa_example.mlw"/>
 <theory name="DfaExample" proved="true">
  <goal name="nil_notin_r1" proved="true">
- <proof prover="0" edited="dfa_example_DfaExample_nil_notin_r1_1.v"><result status="valid" time="0.26"/></proof>
+ <proof prover="0" edited="dfa_example_DfaExample_nil_notin_r1_1.v"><result status="valid" time="1.04"/></proof>
  <proof prover="4"><result status="valid" time="0.10"/></proof>
  <proof prover="6" memlimit="4000"><result status="valid" time="0.08" steps="436"/></proof>
  </goal>

examples/dijkstra/why3session.xml

@@ -8,7 +8,9 @@
 <prover id="5" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="7" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="8" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
-<file name="../dijkstra.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="dijkstra.mlw"/>
 <theory name="DijkstraShortestPath" proved="true">
  <goal name="VC relax" expl="VC for relax" proved="true">
  <transf name="split_goal_right" proved="true" >

examples/double_wp/compiler/why3session.xml

@@ -4,7 +4,9 @@
 <why3session shape_version="5">
 <prover id="1" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
-<file name="../compiler.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="compiler.mlw"/>
 <theory name="Compile_aexpr" proved="true">
  <goal name="VC compile_aexpr" expl="VC for compile_aexpr" proved="true">
  <transf name="split_goal_right" proved="true" >
@@ -573,7 +575,7 @@
        <proof prover="2"><result status="valid" time="0.14" steps="55"/></proof>
        </goal>
        <goal name="VC compile_com.5.4.0.0.0.22" expl="VC for compile_com" proved="true">
-       <proof prover="2"><result status="valid" time="0.39" steps="364"/></proof>
+       <proof prover="2"><result status="valid" time="0.25" steps="364"/></proof>
        </goal>
        <goal name="VC compile_com.5.4.0.0.0.23" expl="VC for compile_com" proved="true">
        <proof prover="2"><result status="valid" time="0.12" steps="55"/></proof>

examples/double_wp/logic/why3session.xml

@@ -5,7 +5,9 @@
 <prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="3" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
-<file name="../logic.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="logic.mlw"/>
 <theory name="Compiler_logic" proved="true">
  <goal name="VC hl" expl="VC for hl" proved="true">
  <proof prover="3"><result status="valid" time="0.01" steps="6"/></proof>

examples/double_wp/specs/why3session.xml

@@ -4,7 +4,9 @@
 <why3session shape_version="5">
 <prover id="1" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
-<file name="../specs.mlw" proved="true">
+<file proved="true">
+<path name=".."/>
+<path name="specs.mlw"/>
 <theory name="VM_instr_spec" proved="true">
  <goal name="VC ifunf" expl="VC for ifunf" proved="true">
  <transf name="split_goal_right" proved="true" >

examples/edit_distance/why3session.xml

@@ -6,7 +6,9 @@
 <prover id="2" name="Coq" version="8.7.1" timelimit="10" steplimit="0" memlimit="0"/>