Stabilize sessions

Author: xldenis

creusot/tests/should_succeed/cell/02/why3session.xml

@@ -50,7 +50,11 @@
   <proof prover="2"><result status="valid" time="0.09" steps="2829"/></proof>
   </goal>
   <goal name="fib_memo&#39;vc.10" expl="assertion" proved="true">
-  <proof prover="1"><result status="valid" time="1.82" steps="181421"/></proof>
+  <transf name="remove" proved="true" arg1="zero,one,(-),(&gt;),(&lt;=),(&gt;=),abs,uint64&#39;maxInt,uint64&#39;minInt,max_uint64,length1,radix,min_unsigned,cell_ghost_inv,([]),singleton,cons,snoc,(++),( *_),(^_),inner,id,fib_ix,mAX&#39;,index_logic,fib_cell,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Div_bound,Mod_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,Mod_inf,Div_mult,Mod_mult,Power_0,Power_s,Power_s_alt,Power_1,Power_sum,Power_mult,Power_comm1,Power_comm2,Power_non_neg,Power_pos,Power_monotonic,to_int_in_bounds,extensionality,zero_unsigned_is_zero,length_nonnegative,(==)&#39;spec,create&#39;spec,empty&#39;def,set&#39;spec,set&#39;def,([&lt;-])&#39;def,singleton&#39;spec,cons&#39;spec,snoc&#39;spec,([..])&#39;spec,([..])&#39;def,([_..])&#39;def,([.._])&#39;def,(++)&#39;spec,new&#39;spec,slice&#39;invariant,some_0&#39;def,shallow_model_spec,def,lemma_fib_bound_spec,lemma_max_int_spec,Requires2,Requires1,Requires">
+   <goal name="fib_memo&#39;vc.10.0" expl="assertion" proved="true">
+   <proof prover="1" timelimit="0.13"><result status="valid" time="0.13" steps="9782"/></proof>
+   </goal>
+  </transf>
   </goal>
   <goal name="fib_memo&#39;vc.11" expl="precondition" proved="true">
   <proof prover="2"><result status="valid" time="0.01" steps="16"/></proof>

creusot/tests/should_succeed/cell/02/why3shapes.gz

@@ -128,12 +128,13 @@
   <proof prover="3"><result status="valid" time="0.06" steps="237768"/></proof>
   </goal>
   <goal name="add&#39;vc.25" expl="postcondition" proved="true">
-  <transf name="split_vc" proved="true" >
+  <transf name="remove" proved="true" arg1="(-),(&gt;),(&lt;=),(&gt;=),([&lt;-]&#39;),([]),singleton,cons,snoc,(++),id,no_double_binding,Unit_def_l,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Abs_le,Mod_bound,Div_unique,Div_bound,Mod_1,Div_1,Div_inf,Div_inf_neg,Mod_0,Div_1_left,Div_minus1_left,Mod_1_left,Mod_minus1_left,Div_mult,Mod_mult,length_nonnegative,(==)&#39;spec,create&#39;spec,empty&#39;def,set&#39;spec,set&#39;def,([&lt;-])&#39;def,singleton&#39;spec,cons&#39;spec,snoc&#39;spec,([..])&#39;spec,([..])&#39;def,([_..])&#39;def,([.._])&#39;def,(++)&#39;spec,new&#39;spec,slice&#39;invariant,shallow_model_spec,Assume,Ensures6,Ensures5,Assert,Ensures4,Ensures3,Ensures">
    <goal name="add&#39;vc.25.0" expl="postcondition" proved="true">
-   <proof prover="1"><result status="valid" time="0.61" steps="111044"/></proof>
-   </goal>
-   <goal name="add&#39;vc.25.1" expl="postcondition" proved="true">
-   <proof prover="1"><result status="valid" time="1.05" steps="213992"/></proof>
+   <transf name="remove" proved="true" arg1="get2,uint64&#39;maxInt,uint64&#39;minInt,max_uint64,length2,radix,Assoc,Unit_def_r,Inv_def_l,Inv_def_r,Trans,Antisymm,Total,CompatOrderAdd,CompatOrderMult,Abs_pos,Div_mod1,Div_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,Mod_inf,Div_mult,Mod_mult,to_int_in_bounds">
+    <goal name="add&#39;vc.25.0.0" expl="postcondition" proved="true">
+    <proof prover="1" timelimit="0.42"><result status="valid" time="0.42" steps="59392"/></proof>
+    </goal>
+   </transf>
    </goal>
   </transf>
   </goal>

creusot/tests/should_succeed/hashmap/why3session.xml

@@ -91,12 +91,9 @@
   <goal name="sift_down&#39;vc.24" expl="loop invariant preservation" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="sift_down&#39;vc.24.0" expl="loop invariant preservation" proved="true">
-   <transf name="split_vc" proved="true" >
+   <transf name="remove" proved="true" arg1="zero,abs,uint64&#39;maxInt,uint64&#39;minInt,max_uint64,singleton,cons,snoc,mem,iseq,occ,occ_all,seq_eq_sub,permut_sub,permut_all,id,mAX&#39;,shallow_model5,heap_frag,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Div_bound,Mod_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Full,numof_increasing,numof_strictly_increasing,numof_change_any,numof_change_some,numof_change_equiv,extensionality,set&#39;spec,set&#39;def,([&lt;-])&#39;def,singleton&#39;spec,cons&#39;spec,snoc&#39;spec,([..])&#39;spec,([..])&#39;def,([_..])&#39;def,mem_append,mem_tail,occ_cons,occ_snoc,occ_tail,exchange_permut_sub,Permut_sub_weakening,permut_refl,permut_sym,permut_trans,permut_exists,permut_all_mem,exchange_permut_all,new&#39;spec,shallow_model_spec1,eq_cmp_spec,antisym2_spec,antisym1_spec,cmp_ge_log_spec,cmp_lt_log_spec,H20,H15,Ensures12,Ensures11,Assert,Ensures10,H14,Ensures9,Ensures8,Ensures7,H13,Ensures6,Assume2,Ensures5,Assume1,H10,H19,H18,H17,H16,H12,H11">
     <goal name="sift_down&#39;vc.24.0.0" expl="loop invariant preservation" proved="true">
-    <proof prover="3" timelimit="5" memlimit="2000"><result status="valid" time="2.66" steps="326805"/></proof>
-    </goal>
-    <goal name="sift_down&#39;vc.24.0.1" expl="loop invariant preservation" proved="true">
-    <proof prover="1"><result status="valid" time="0.81" steps="10288"/></proof>
+    <proof prover="1"><result status="valid" time="0.03" steps="305"/></proof>
     </goal>
    </transf>
    </goal>

creusot/tests/should_succeed/hashmap/why3shapes.gz

@@ -79,7 +79,11 @@
 </theory>
 <theory name="Hillel_Unique" proved="true">
  <goal name="unique&#39;vc" expl="VC for unique" proved="true">
- <proof prover="2"><result status="valid" time="0.26" steps="1290900"/></proof>
+ <transf name="remove" proved="true" arg1="zero,one,(-),(&gt;),(&lt;=),(&gt;=),abs,uint64&#39;maxInt,uint64&#39;minInt,max_uint64,length1,radix,min_unsigned,in_bounds,singleton,cons,snoc,(++),mAX&#39;,index_logic,is_inhabited,resolve2,new,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Div_bound,Mod_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,Mod_inf,Div_mult,Mod_mult,to_int_in_bounds,extensionality,zero_unsigned_is_zero,length_nonnegative,set&#39;spec,set&#39;def,([&lt;-])&#39;def,singleton&#39;spec,cons&#39;spec,([_..])&#39;def,([.._])&#39;def,(++)&#39;spec,new&#39;spec,slice&#39;invariant,shallow_model_spec,produces_trans_spec,produces_refl_spec,is_inhabited_spec">
+  <goal name="unique&#39;vc.0" expl="VC for unique" proved="true">
+  <proof prover="2" timelimit="0.06"><result status="valid" time="0.06" steps="362749"/></proof>
+  </goal>
+ </transf>
  </goal>
 </theory>
 <theory name="Hillel_SumRange_Impl" proved="true">

creusot/tests/should_succeed/heapsort_generic/why3session.xml

@@ -3,7 +3,7 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="6">
 <prover id="0" name="Alt-Ergo" version="2.4.2" timelimit="1" steplimit="0" memlimit="1000"/>
-<prover id="1" name="Z3" version="4.11.2" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="1" name="Z3" version="4.11.2" timelimit="0.01" steplimit="0" memlimit="1000"/>
 <prover id="4" name="CVC5" version="1.0.5" timelimit="1" steplimit="0" memlimit="1000"/>
 <file format="mlcfg" proved="true">
 <path name=".."/><path name="06_map_precond.mlcfg"/>
@@ -203,7 +203,7 @@
    <goal name="produces_one&#39;vc.0.1" expl="postcondition" proved="true">
    <transf name="use_th" proved="true" arg1="seq.FreeMonoid">
     <goal name="produces_one&#39;vc.0.1.0" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.07" steps="307146"/></proof>
+    <proof prover="1" timelimit="1"><result status="valid" time="0.07" steps="307146"/></proof>
     </goal>
    </transf>
    </goal>
@@ -347,7 +347,11 @@
   <proof prover="0"><result status="valid" time="0.00" steps="12"/></proof>
   </goal>
   <goal name="increment&#39;vc.5" expl="assertion" proved="true">
-  <proof prover="1"><result status="valid" time="0.62" steps="2132056"/></proof>
+  <transf name="remove" proved="true" arg1="zero,one,(-),(&gt;),(&lt;=),(&gt;=),abs,uint32&#39;minInt,max_uint32,length1,radix,([]),singleton,cons,snoc,(++),( *_),(^_),inner,map_produced,map_func,subsequence,resolve1,unnest,precondition,postcondition_once,completed,preservation,next_precondition,preservation_inv,reinitialize,produces_trans,produces_refl,invariant&#39;,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Div_bound,Mod_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,Mod_inf,Div_mult,Mod_mult,extensionality,zero_unsigned_is_zero,(==)&#39;spec,create&#39;spec,empty&#39;def,set&#39;spec,set&#39;def,([&lt;-])&#39;def,singleton&#39;spec,cons&#39;spec,snoc&#39;spec,([..])&#39;spec,([..])&#39;def,([_..])&#39;def,([.._])&#39;def,(++)&#39;spec,new&#39;spec,produces_trans_spec1,produces_refl_spec1,is_inhabited_spec,preservation_inv_spec,produces_trans_spec,produces_refl_spec,Requires3,Requires2,Requires,Ensures,Assume">
+   <goal name="increment&#39;vc.5.0" expl="assertion" proved="true">
+   <proof prover="1"><result status="valid" time="0.01" steps="22197"/></proof>
+   </goal>
+  </transf>
   </goal>
  </transf>
  </goal>