remove trivial goals from sessions

examples/WP_revisited/wp2/why3session.xml

@@ -9,9 +9,6 @@
 <prover id="10" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <file name="../wp2.mlw" proved="true">
 <theory name="Imp" proved="true">
- <goal name="VC subst_term" expl="VC for subst_term" proved="true">
- <proof prover="2"><result status="valid" time="0.01" steps="1"/></proof>
- </goal>
  <goal name="eval_subst_term" proved="true">
  <transf name="induction_ty_lex" proved="true" >
   <goal name="eval_subst_term.0" proved="true">
@@ -26,9 +23,6 @@
   </goal>
  </transf>
  </goal>
- <goal name="VC subst" expl="VC for subst" proved="true">
- <proof prover="2"><result status="valid" time="0.01" steps="1"/></proof>
- </goal>
  <goal name="eval_subst" proved="true">
  <transf name="induction_ty_lex" proved="true" >
   <goal name="eval_subst.0" proved="true">

examples/avl/avl/why3session.xml

@@ -4,20 +4,6 @@
 <why3session shape_version="4">
 <prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <file name="../avl.mlw" proved="true">
-<theory name="SelectionTypes" proved="true">
- <goal name="VC option_to_seq" expl="VC for option_to_seq" proved="true">
- <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
- </goal>
- <goal name="VC rebuild" expl="VC for rebuild" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="1"/></proof>
- </goal>
- <goal name="VC left_extend" expl="VC for left_extend" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="1"/></proof>
- </goal>
- <goal name="VC right_extend" expl="VC for right_extend" proved="true">
- <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
- </goal>
-</theory>
 <theory name="AVL" proved="true">
  <goal name="M.M.assoc" proved="true">
  <proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
@@ -25,18 +11,6 @@
  <goal name="M.M.neutral" proved="true">
  <proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
  </goal>
- <goal name="VC balancing" expl="VC for balancing" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="3"/></proof>
- </goal>
- <goal name="VC node_model" expl="VC for node_model" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
- </goal>
- <goal name="VC seq_model" expl="VC for seq_model" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
- </goal>
- <goal name="VC real_height" expl="VC for real_height" proved="true">
- <proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
- </goal>
  <goal name="VC real_height_nonnegative" expl="VC for real_height_nonnegative" proved="true">
  <proof prover="1"><result status="valid" time="0.01" steps="56"/></proof>
  </goal>
@@ -226,9 +200,6 @@
  <goal name="VC concat" expl="VC for concat" proved="true">
  <proof prover="1"><result status="valid" time="0.24" steps="765"/></proof>
  </goal>
- <goal name="VC default_split" expl="VC for default_split" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
- </goal>
  <goal name="VC insert" expl="VC for insert" proved="true">
  <transf name="split_goal_right" proved="true" >
   <goal name="VC insert.0" expl="postcondition" proved="true">

examples/avl/priority_queue/why3session.xml

@@ -7,9 +7,6 @@
 <prover id="4" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <file name="../priority_queue.mlw" proved="true">
 <theory name="PQueue" proved="true">
- <goal name="VC balancing" expl="VC for balancing" proved="true">
- <proof prover="4"><result status="valid" time="0.00" steps="3"/></proof>
- </goal>
  <goal name="M.VC assoc_m" expl="VC for assoc_m" proved="true">
  <transf name="split_goal_right" proved="true" >
   <goal name="VC assoc_m.0" expl="assertion" proved="true">
@@ -94,9 +91,6 @@
   </goal>
  </transf>
  </goal>
- <goal name="D.VC measure" expl="VC for measure" proved="true">
- <proof prover="4"><result status="valid" time="0.01" steps="4"/></proof>
- </goal>
  <goal name="VC monoid_sum_is_min" expl="VC for monoid_sum_is_min" proved="true">
  <transf name="split_goal_right" proved="true" >
   <goal name="VC monoid_sum_is_min.0" expl="precondition" proved="true">
@@ -364,9 +358,6 @@
  <goal name="Sel.M.agg_cat" proved="true">
  <proof prover="4"><result status="valid" time="0.02" steps="5"/></proof>
  </goal>
- <goal name="Sel.D.VC measure" expl="VC for measure" proved="true">
- <proof prover="4"><result status="valid" time="0.02" steps="4"/></proof>
- </goal>
  <goal name="Sel.VC balancing" expl="VC for balancing" proved="true">
  <proof prover="4"><result status="valid" time="0.01" steps="4"/></proof>
  </goal>
@@ -376,9 +367,6 @@
  <goal name="Sel.VC selected_part" expl="VC for selected_part" proved="true">
  <proof prover="4"><result status="valid" time="0.04" steps="257"/></proof>
  </goal>
- <goal name="VC to_bag" expl="VC for to_bag" proved="true">
- <proof prover="4"><result status="valid" time="0.01" steps="4"/></proof>
- </goal>
  <goal name="VC to_bag_mem" expl="VC for to_bag_mem" proved="true">
  <transf name="split_goal_right" proved="true" >
   <goal name="VC to_bag_mem.0" expl="assertion" proved="true">

examples/avl/ral/why3session.xml

@@ -5,9 +5,6 @@
 <prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <file name="../ral.mlw" proved="true">
 <theory name="RAL" proved="true">
- <goal name="VC balancing" expl="VC for balancing" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="3"/></proof>
- </goal>
  <goal name="M.assoc" proved="true">
  <proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
  </goal>
@@ -26,9 +23,6 @@
  <goal name="M.VC op" expl="VC for op" proved="true">
  <proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
  </goal>
- <goal name="D.VC measure" expl="VC for measure" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
- </goal>
  <goal name="VC agg_measure_is_length" expl="VC for agg_measure_is_length" proved="true">
  <proof prover="1"><result status="valid" time="0.01" steps="50"/></proof>
  </goal>
@@ -56,9 +50,6 @@
  <goal name="Sel.M.agg_cat" proved="true">
  <proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
  </goal>
- <goal name="Sel.D.VC measure" expl="VC for measure" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
- </goal>
  <goal name="Sel.VC balancing" expl="VC for balancing" proved="true">
  <proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
  </goal>

examples/avl/tables/why3session.xml

@@ -6,12 +6,6 @@
 <prover id="5" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <file name="../tables.mlw" proved="true">
 <theory name="MapBase" proved="true">
- <goal name="VC balancing" expl="VC for balancing" proved="true">
- <proof prover="5"><result status="valid" time="0.01" steps="3"/></proof>
- </goal>
- <goal name="D.VC measure" expl="VC for measure" proved="true">
- <proof prover="5"><result status="valid" time="0.01" steps="4"/></proof>
- </goal>
  <goal name="M.VC neutral_" expl="VC for neutral_" proved="true">
  <proof prover="5"><result status="valid" time="0.01" steps="4"/></proof>
  </goal>
@@ -93,9 +87,6 @@
  <goal name="Sel.M.agg_cat" proved="true">
  <proof prover="5"><result status="valid" time="0.01" steps="4"/></proof>
  </goal>
- <goal name="Sel.D.VC measure" expl="VC for measure" proved="true">
- <proof prover="5"><result status="valid" time="0.01" steps="4"/></proof>
- </goal>
  <goal name="Sel.VC balancing" expl="VC for balancing" proved="true">
  <proof prover="5"><result status="valid" time="0.01" steps="4"/></proof>
  </goal>
@@ -821,18 +812,9 @@
  </goal>
 </theory>
 <theory name="Map" proved="true">
- <goal name="VC balancing" expl="VC for balancing" proved="true">
- <proof prover="5"><result status="valid" time="0.00" steps="3"/></proof>
- </goal>
- <goal name="D.VC key" expl="VC for key" proved="true">
- <proof prover="5"><result status="valid" time="0.01" steps="4"/></proof>
- </goal>
  <goal name="MB.VC balancing" expl="VC for balancing" proved="true">
  <proof prover="5"><result status="valid" time="0.01" steps="4"/></proof>
  </goal>
- <goal name="MB.VC key" expl="VC for key" proved="true">
- <proof prover="5"><result status="valid" time="0.01" steps="4"/></proof>
- </goal>
  <goal name="MB.CO.Refl" proved="true">
  <proof prover="5"><result status="valid" time="0.01" steps="5"/></proof>
  </goal>
@@ -905,18 +887,9 @@
  </goal>
 </theory>
 <theory name="Set" proved="true">
- <goal name="VC balancing" expl="VC for balancing" proved="true">
- <proof prover="5"><result status="valid" time="0.01" steps="3"/></proof>
- </goal>
- <goal name="D.VC key" expl="VC for key" proved="true">
- <proof prover="5"><result status="valid" time="0.01" steps="4"/></proof>
- </goal>
  <goal name="MB.VC balancing" expl="VC for balancing" proved="true">
  <proof prover="5"><result status="valid" time="0.00" steps="4"/></proof>
  </goal>
- <goal name="MB.VC key" expl="VC for key" proved="true">
- <proof prover="5"><result status="valid" time="0.01" steps="4"/></proof>
- </goal>
  <goal name="MB.CO.Refl" proved="true">
  <proof prover="5"><result status="valid" time="0.01" steps="5"/></proof>
  </goal>
@@ -994,9 +967,6 @@
  </goal>
 </theory>
 <theory name="IMapAndSet" proved="true">
- <goal name="VC balancing" expl="VC for balancing" proved="true">
- <proof prover="5"><result status="valid" time="0.00" steps="3"/></proof>
- </goal>
  <goal name="VC compare" expl="VC for compare" proved="true">
  <proof prover="5"><result status="valid" time="0.01" steps="4"/></proof>
  </goal>

examples/bag/why3session.xml

@@ -6,17 +6,6 @@
 <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">
-<theory name="Bag" proved="true">
- <goal name="VC empty" expl="VC for empty" proved="true">
- <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
- </goal>
- <goal name="VC add" expl="VC for add" proved="true">
- <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
- </goal>
- <goal name="VC remove" expl="VC for remove" proved="true">
- <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
- </goal>
-</theory>
 <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/bellman_ford/why3session.xml

@@ -6,15 +6,9 @@
 <prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <file name="../bellman_ford.mlw" proved="true">
 <theory name="Graph" proved="true">
- <goal name="VC s" expl="VC for s" proved="true">
- <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
- </goal>
  <goal name="vertices_cardinal_pos" proved="true">
  <proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
  </goal>
- <goal name="VC nb_vertices" expl="VC for nb_vertices" proved="true">
- <proof prover="1"><result status="valid" time="0.00" steps="3"/></proof>
- </goal>
  <goal name="path_in_vertices" proved="true">
  <proof prover="1"><result status="valid" time="0.01" steps="30"/></proof>
  </goal>

examples/bignum/why3session.xml

@@ -8,9 +8,6 @@
 <prover id="4" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../bignum.mlw" proved="true">
 <theory name="BigNum" proved="true">
- <goal name="VC base" expl="VC for base" proved="true">
- <proof prover="4"><result status="valid" time="0.00" steps="1"/></proof>
- </goal>
  <goal name="VC nonneg" expl="VC for nonneg" proved="true">
  <transf name="split_goal_right" proved="true" >
   <goal name="VC nonneg.0" expl="variant decrease" proved="true">

examples/binomial_heap/why3session.xml

@@ -142,9 +142,6 @@
   </goal>
  </transf>
  </goal>
- <goal name="VC link" expl="VC for link" proved="true">
- <proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
- </goal>
  <goal name="VC add_tree" expl="VC for add_tree" proved="true">
  <transf name="split_goal_right" proved="true" >
   <goal name="VC add_tree.0" expl="assertion" proved="true">

examples/bitwalker/why3session.xml

@@ -13,10 +13,6 @@
  <goal name="nth8" proved="true">
  <proof prover="0"><result status="valid" time="0.06" steps="208"/></proof>
  </goal>
- <goal name="VC maxvalue" expl="VC for maxvalue" proved="true">
- <transf name="compute_in_goal" proved="true" >
- </transf>
- </goal>
  <goal name="VC nth_ultpre0" expl="VC for nth_ultpre0" proved="true">
  <transf name="split_goal_right" proved="true" >
   <goal name="VC nth_ultpre0.0" expl="assertion" proved="true">