Bisect selection_sort

Author: voidc

creusot/tests/should_succeed/selection_sort_generic/why3session.xml

@@ -2,7 +2,6 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="6">
-<prover id="0" name="CVC4" version="1.8" timelimit="30" steplimit="0" memlimit="4000"/>
 <prover id="1" name="Z3" version="4.12.1" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="2" name="CVC5" version="1.0.5" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="5" name="Alt-Ergo" version="2.4.2" timelimit="1" steplimit="0" memlimit="1000"/>
@@ -73,7 +72,11 @@
     <proof prover="5"><result status="valid" time="0.052939" steps="148"/></proof>
     </goal>
     <goal name="selection_sort&#39;vc.18.0.1" expl="assertion" proved="true">
-    <proof prover="0"><result status="valid" time="27.656646" steps="5354841"/></proof>
+    <transf name="remove" proved="true" arg1="one,(-),(&gt;),(&gt;=),uint64&#39;maxInt,uint64&#39;minInt,max_uint64,length1,singleton,cons,snoc,(++),mem,iseq,occ,occ_all,permut,mAX&#39;,is_inhabited,sorted_range,sorted,permutation_of,shallow_model,Mul_distr_r,Comm,Unitary,NonTrivialRing,Total,CompatOrderAdd,CompatOrderMult,Mod_inf,Div_mult,Mod_mult,Numof_append,Numof_left_no_add,Numof_left_add,Empty,Full,numof_increasing,numof_strictly_increasing,numof_change_any,numof_change_some,numof_change_equiv,length_nonnegative,([&lt;-])&#39;def,singleton&#39;spec,cons&#39;spec,snoc&#39;spec,mem_append,occ_cons,occ_tail,append_num_occ,exchange_set,permut_sym,permut_trans,permut_exists,new&#39;spec,produces_trans_spec,produces_refl_spec,is_inhabited_spec">
+     <goal name="selection_sort&#39;vc.18.0.1.0" expl="assertion" proved="true">
+     <proof prover="1"><result status="valid" time="0.074239" steps="284974"/></proof>
+     </goal>
+    </transf>
     </goal>
    </transf>
    </goal>