Commit f3a548ad authored by MARCHE Claude's avatar MARCHE Claude

fix sessions that were broken by last merge

parent 231a5e1e
......@@ -9,15 +9,9 @@
<prover id="6" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="9" name="Z3" version="3.2" timelimit="3" steplimit="0" memlimit="1000"/>
<prover id="10" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<<<<<<< HEAD
<file name="../bitvector.why" proved="true">
<theory name="BitVector" proved="true" sum="95aab3d42f1124158e06d97baf59fb6c">
<goal name="Nth_bw_xor_v1true" proved="true">
=======
<file name="../bitvector.why">
<theory name="BitVector">
<goal name="Nth_bw_xor_v1true" expl="">
>>>>>>> new_ide
<proof prover="2"><result status="valid" time="0.08" steps="85"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.02"/></proof>
......@@ -83,7 +77,6 @@
<proof prover="2"><result status="valid" time="0.33" steps="94"/></proof>
</goal>
</theory>
<<<<<<< HEAD
<theory name="BV32" proved="true" sum="34ed4e77796acb2611bcf8f00bf21d7d">
<goal name="size_positive" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="65"/></proof>
......@@ -98,16 +91,6 @@
</theory>
<theory name="TestBv32" proved="true" sum="0e6817645d330955194c1d0ced9bdb30">
<goal name="Test1" proved="true">
=======
<theory name="BV32">
</theory>
<theory name="BV64">
</theory>
<theory name="BV32_64">
</theory>
<theory name="TestBv32">
<goal name="Test1" expl="">
>>>>>>> new_ide
<proof prover="2"><result status="valid" time="0.06" steps="72"/></proof>
<proof prover="3" timelimit="3"><result status="valid" time="0.07"/></proof>
<proof prover="6"><result status="valid" time="0.04"/></proof>
......
......@@ -7,7 +7,6 @@
<prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Coq" version="8.7.1" timelimit="30" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<<<<<<< HEAD
<file name="../double.why" proved="true">
<theory name="BV_double" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
......@@ -16,16 +15,6 @@
<proof prover="0" timelimit="3"><result status="valid" time="0.05" steps="77"/></proof>
</goal>
<goal name="nth_one2" proved="true">
=======
<file name="../double.why">
<theory name="BV_double">
</theory>
<theory name="TestDouble">
<goal name="nth_one1" expl="">
<proof prover="0" timelimit="3"><result status="valid" time="0.05" steps="77"/></proof>
</goal>
<goal name="nth_one2" expl="">
>>>>>>> new_ide
<proof prover="0" timelimit="3"><result status="valid" time="0.04" steps="77"/></proof>
</goal>
<goal name="nth_one3" proved="true">
......@@ -37,15 +26,9 @@
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="5"><result status="valid" time="0.11"/></proof>
</goal>
<<<<<<< HEAD
<goal name="exp_one" proved="true">
<proof prover="0" timelimit="30"><result status="valid" time="2.21" steps="668"/></proof>
<proof prover="4" edited="double_TestDouble_exp_one_1.v"><result status="valid" time="0.52"/></proof>
=======
<goal name="exp_one" expl="">
<proof prover="0" timelimit="30"><result status="valid" time="2.23" steps="668"/></proof>
<proof prover="4" edited="double_TestDouble_exp_one_1.v"><result status="valid" time="0.38"/></proof>
>>>>>>> new_ide
</goal>
<goal name="mantissa_one" proved="true">
<proof prover="0"><result status="valid" time="0.09" steps="87"/></proof>
......
......@@ -9,15 +9,9 @@
<prover id="5" name="Coq" version="8.7.1" timelimit="60" steplimit="0" memlimit="1000"/>
<prover id="6" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="8" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<<<<<<< HEAD
<file name="../double_of_int.why" proved="true">
<theory name="DoubleOfInt" proved="true" sum="aaf85bdb0d52c15e561af0704672eb5f">
<goal name="nth_j1" proved="true">
=======
<file name="../double_of_int.why">
<theory name="DoubleOfInt">
<goal name="nth_j1" expl="">
>>>>>>> new_ide
<proof prover="1"><result status="valid" time="0.04" steps="78"/></proof>
</goal>
<goal name="nth_j2" proved="true">
......
......@@ -6,13 +6,8 @@
<prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="3.2" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="9" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<<<<<<< HEAD
<file name="../neg_as_xor.why" expanded="true">
<theory name="TestNegAsXOR" sum="692831fdefa67c6dc694b2674e2744e5" expanded="true">
=======
<file name="../neg_as_xor.why">
<theory name="TestNegAsXOR">
>>>>>>> new_ide
<goal name="Nth_j" expl="">
<proof prover="1"><result status="valid" time="0.05" steps="77"/></proof>
</goal>
......
......@@ -9,15 +9,9 @@
<prover id="6" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="9" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="10" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<<<<<<< HEAD
<file name="../power2.why" proved="true">
<theory name="Pow2int" proved="true" sum="89a88024fb38dcd933a68112fe649faf">
<goal name="Power_1" proved="true">
=======
<file name="../power2.why">
<theory name="Pow2int">
<goal name="Power_1" expl="">
>>>>>>> new_ide
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
......@@ -440,13 +434,8 @@
<proof prover="4" edited="power2_Pow2int_Mod_pow2_gen_1.v"><result status="valid" time="0.86"/></proof>
</goal>
</theory>
<<<<<<< HEAD
<theory name="Pow2real" proved="true" sum="e31a44730ea8985818a40fb1e9374bf0">
<goal name="Power_s_all" proved="true">
=======
<theory name="Pow2real">
<goal name="Power_s_all" expl="">
>>>>>>> new_ide
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.01"/></proof>
......
......@@ -5,13 +5,8 @@
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../compiler.mlw" proved="true">
<<<<<<< HEAD
<theory name="Compile_aexpr" proved="true" sum="92a9a5d6f2ec0d9ff94405e1c114f3c3">
<goal name="VC compile_aexpr" expl="VC for compile_aexpr" proved="true">
=======
<theory name="Compile_aexpr" proved="true">
<goal name="WP_parameter compile_aexpr" expl="VC for compile_aexpr" proved="true">
>>>>>>> new_ide
<transf name="split_goal_wp" proved="true" >
<goal name="VC compile_aexpr.0" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.11" steps="63"/></proof>
......@@ -122,13 +117,8 @@
<proof prover="0"><result status="valid" time="0.05" steps="87"/></proof>
</goal>
</theory>
<<<<<<< HEAD
<theory name="Compile_bexpr" proved="true" sum="e2228d736b99d90f78b1518737430864">
<goal name="VC compile_bexpr" expl="VC for compile_bexpr" proved="true">
=======
<theory name="Compile_bexpr" proved="true">
<goal name="WP_parameter compile_bexpr" expl="VC for compile_bexpr" proved="true">
>>>>>>> new_ide
<transf name="split_goal_wp" proved="true" >
<goal name="VC compile_bexpr.0" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.08" steps="39"/></proof>
......@@ -340,16 +330,11 @@
<proof prover="0"><result status="valid" time="0.08" steps="151"/></proof>
</goal>
</theory>
<<<<<<< HEAD
<theory name="Compile_com" proved="true" sum="811cd6941f8ab581067af7bc7f6180e9">
<goal name="loop_variant_lemma" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="29"/></proof>
</goal>
<goal name="loop_variant_acc" proved="true">
=======
<theory name="Compile_com" proved="true">
<goal name="WP_parameter compile_com" expl="VC for compile_com" proved="true">
>>>>>>> new_ide
<transf name="split_goal_wp" proved="true" >
<goal name="loop_variant_acc.0" proved="true">
<proof prover="0"><result status="valid" time="0.12" steps="200"/></proof>
......
......@@ -2,16 +2,9 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<<<<<<< HEAD
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../imp.why">
<theory name="Imp" sum="5697e116b3801a58323ce20e8692f0ba">
=======
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../imp.why">
<theory name="Imp">
>>>>>>> new_ide
<goal name="ceval_deterministic_aux" expl="">
<transf name="induction_pr">
<goal name="ceval_deterministic_aux.1" expl="">
......
......@@ -2,7 +2,6 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<<<<<<< HEAD
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
......@@ -10,16 +9,6 @@
<theory name="Compiler_logic" proved="true" sum="cf4c1068c97dbed0498a4f106d4e05b1">
<goal name="VC hl" expl="VC for hl" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>
=======
<prover id="0" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.3" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../logic.mlw">
<theory name="Compiler_logic">
<goal name="seq_wp_lemma" expl="">
<proof prover="2"><result status="valid" time="0.04" steps="8"/></proof>
>>>>>>> new_ide
</goal>
<goal name="VC wp" expl="VC for wp" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="8"/></proof>
......
......@@ -5,22 +5,9 @@
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../specs.mlw" proved="true">
<<<<<<< HEAD
<theory name="VM_instr_spec" proved="true" sum="255d39ef88534817b912165143dc1783">
<goal name="VC isetvarf" expl="VC for isetvarf" proved="true">
<proof prover="0"><result status="valid" time="0.16" steps="210"/></proof>
=======
<theory name="VM_instr_spec" proved="true">
<goal name="WP_parameter ifunf" expl="VC for ifunf" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter ifunf.0" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="WP_parameter ifunf.1" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="8"/></proof>
</goal>
</transf>
>>>>>>> new_ide
</goal>
<goal name="VC ibgtf" expl="VC for ibgtf" proved="true">
<proof prover="0"><result status="valid" time="0.09" steps="145"/></proof>
......
......@@ -2,13 +2,8 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<<<<<<< HEAD:examples/double_wp/state/why3session.xml
<file name="../state.why">
<theory name="State" sum="d41d8cd98f00b204e9800998ecf8427e">
=======
<file name="../43_range_module.mlw" proved="true">
<theory name="Issue43" proved="true">
>>>>>>> new_ide:examples/bts/43_range_module/why3session.xml
</theory>
</file>
</why3session>
......@@ -2,18 +2,10 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<<<<<<< HEAD
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../vm.mlw">
<theory name="ReflTransClosure" sum="8ac8ed5760e8555c2bce4ced0d223f8b">
=======
<prover id="0" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../vm.mlw">
<theory name="ReflTransClosure">
>>>>>>> new_ide
<goal name="transition_star_one" expl="">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
......@@ -36,11 +28,7 @@
</transf>
</goal>
</theory>
<<<<<<< HEAD
<theory name="Vm" sum="a97f807b42b411f5965ea9e0aaaa483b">
=======
<theory name="Vm">
>>>>>>> new_ide
<goal name="codeseq_at_app_right" expl="">
<proof prover="0"><result status="valid" time="0.01" steps="30"/></proof>
</goal>
......
......@@ -13,13 +13,9 @@
<prover id="8" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="9" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../queens_bv.mlw" proved="true">
<theory name="S" proved="true">
<theory name="S" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<<<<<<< HEAD
<theory name="Solution" proved="true" sum="33e8246862579e1e8655468bf3a248ab">
=======
<theory name="Solution" proved="true">
>>>>>>> new_ide
<goal name="partial_solution_eq_prefix" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="44"/></proof>
</goal>
......@@ -28,7 +24,6 @@
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
</theory>
<<<<<<< HEAD
<theory name="BitsSpec" proved="true" sum="8fbc46ea269d029380a41104bd31dc1e">
<goal name="VC t" expl="VC for t" proved="true">
<proof prover="7"><result status="valid" time="0.03"/></proof>
......@@ -37,13 +32,6 @@
<theory name="Bits" proved="true" sum="6c62e04243120c79ca8d250f6d3a2909">
<goal name="VC t" expl="VC for t" proved="true">
<proof prover="7"><result status="valid" time="0.03"/></proof>
=======
<theory name="BitsSpec" proved="true">
</theory>
<theory name="Bits" proved="true">
<goal name="WP_parameter empty" expl="VC for empty" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="80"/></proof>
>>>>>>> new_ide
</goal>
<goal name="VC empty" expl="VC for empty" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="95"/></proof>
......@@ -130,13 +118,8 @@
<proof prover="6"><result status="valid" time="0.06"/></proof>
</goal>
</theory>
<<<<<<< HEAD
<theory name="NQueensBits" proved="true" sum="758a7663eed2f4fcd885dbfdc36e417b">
<goal name="VC t" expl="VC for t" proved="true">
=======
<theory name="NQueensBits" proved="true">
<goal name="WP_parameter t" expl="VC for t" proved="true">
>>>>>>> new_ide
<transf name="split_goal_wp" proved="true" >
<goal name="VC t.0" expl="assertion" proved="true">
<proof prover="2" timelimit="10" memlimit="4000"><result status="valid" time="0.82" steps="537"/></proof>
......
......@@ -4,13 +4,8 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../quicksort.mlw" proved="true">
<<<<<<< HEAD
<theory name="Quicksort" proved="true" sum="2a868e31374bafdd7feffbd9eccfa58d">
<goal name="VC quick_rec" expl="VC for quick_rec" proved="true">
=======
<theory name="Quicksort" proved="true">
<goal name="WP_parameter quick_rec" expl="VC for quick_rec" proved="true">
>>>>>>> new_ide
<transf name="split_goal_wp" proved="true" >
<goal name="VC quick_rec.0" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
......@@ -108,7 +103,6 @@
<proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
</theory>
<<<<<<< HEAD
<theory name="Shuffle" proved="true" sum="5784873acff0f6be9471667822c9d384">
<goal name="VC shuffle" expl="VC for shuffle" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="53"/></proof>
......@@ -122,20 +116,6 @@
<theory name="Quicksort3way" proved="true" sum="71958d8c4aeb3e8a7700c71c49103067">
<goal name="VC quick_rec" expl="VC for quick_rec" proved="true">
<proof prover="0"><result status="valid" time="3.51" steps="6499"/></proof>
=======
<theory name="Shuffle" proved="true">
<goal name="WP_parameter shuffle" expl="VC for shuffle" proved="true">
<proof prover="4" timelimit="1"><result status="valid" time="0.03" steps="42"/></proof>
</goal>
</theory>
<theory name="QuicksortWithShuffle" proved="true">
<goal name="WP_parameter qs" expl="VC for qs" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
</theory>
<theory name="Quicksort3way" proved="true">
<goal name="WP_parameter quick_rec" expl="VC for quick_rec" proved="true">
>>>>>>> new_ide
<transf name="split_goal_wp" proved="true" >
<goal name="VC quick_rec.0" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="5"/></proof>
......@@ -272,15 +252,9 @@
<proof prover="0"><result status="valid" time="0.00" steps="11"/></proof>
</goal>
</theory>
<<<<<<< HEAD
<theory name="Test" proved="true" sum="d5d60b2323c955244d4f499a3a11e8ce">
<goal name="VC test1" expl="VC for test1" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
=======
<theory name="Test" proved="true">
<goal name="WP_parameter test1" expl="VC for test1" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="6"/></proof>
>>>>>>> new_ide
</goal>
<goal name="VC test2" expl="VC for test2" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="40"/></proof>
......
......@@ -4,7 +4,6 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../register_allocation.mlw" proved="true">
<<<<<<< HEAD
<theory name="Spec" proved="true" sum="d7167b694c01b0aff1b5f69d6678a402">
<goal name="VC exec_append" expl="VC for exec_append" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="40"/></proof>
......@@ -13,16 +12,6 @@
<theory name="DWP" proved="true" sum="e22595fd2574bc3e7eb21556a53b912f">
<goal name="VC nil" expl="VC for nil" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
=======
<theory name="Spec" proved="true">
<goal name="WP_parameter exec_append" expl="VC for exec_append" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
</theory>
<theory name="DWP" proved="true">
<goal name="WP_parameter prefix $" expl="VC for prefix $" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="5"/></proof>
>>>>>>> new_ide
</goal>
<goal name="VC cons" expl="VC for cons" proved="true">
<proof prover="0"><result status="valid" time="0.11" steps="121"/></proof>
......@@ -122,27 +111,7 @@
</goal>
</transf>
</goal>
<<<<<<< HEAD
<goal name="VC compile.13.2" expl="precondition" proved="true">
=======
</transf>
</goal>
</transf>
</goal>
</theory>
<theory name="InfinityOfRegisters" proved="true">
<goal name="WP_parameter compile" expl="VC for compile" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter compile.0" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="WP_parameter compile.1" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="WP_parameter compile.2" expl="precondition" proved="true">
<transf name="prop_curry" proved="true" >
<goal name="WP_parameter compile.2.0" expl="precondition" proved="true">
>>>>>>> new_ide
<transf name="compute_specified" proved="true" >
<goal name="VC compile.13.2.0" expl="precondition" proved="true">
<transf name="simplify_trivial_quantification_in_goal" proved="true" >
......@@ -232,7 +201,6 @@
<goal name="VC compile.18" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
<<<<<<< HEAD
<goal name="VC compile.19" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
......@@ -253,19 +221,6 @@
</goal>
<goal name="VC compile.25" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="24"/></proof>
=======
</transf>
</goal>
<goal name="WP_parameter recover" expl="VC for recover" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
</theory>
<theory name="FiniteNumberOfRegisters" proved="true">
<goal name="WP_parameter compile" expl="VC for compile" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter compile.0" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="6"/></proof>
>>>>>>> new_ide
</goal>
<goal name="VC compile.26" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="8"/></proof>
......@@ -358,19 +313,8 @@
</goal>
</transf>
</goal>
<<<<<<< HEAD
<goal name="VC k" expl="VC for k" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="1"/></proof>
=======
</theory>
<theory name="OptimalNumberOfRegisters" proved="true">
<goal name="measure_nonneg" proved="true">
<transf name="induction_ty_lex" proved="true" >
<goal name="measure_nonneg.0" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
</transf>
>>>>>>> new_ide
</goal>
</theory>
<theory name="OptimalNumberOfRegisters" proved="true" sum="5fb8dd717f71d0a623d142d343b48638">
......
......@@ -4,13 +4,8 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="60" steplimit="0" memlimit="0"/>
<<<<<<< HEAD
<file name="../relabel.mlw" expanded="true">
<theory name="Relabel" sum="0ffa7db15de995f5235293fa725ea460" expanded="true">
=======
<file name="../relabel.mlw">
<theory name="Relabel">
>>>>>>> new_ide
<goal name="labels_Leaf" expl="">
<proof prover="0"><result status="valid" time="0.01" steps="32"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="45"/></proof>
......
......@@ -2,7 +2,6 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<<<<<<< HEAD
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../remove_duplicate.mlw" proved="true">
......@@ -11,18 +10,6 @@
<theory name="RemoveDuplicateQuadratic" proved="true" sum="7f60110f05a5c148e9fc74899a4c6929">
<goal name="VC test_appears" expl="VC for test_appears" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="65"/></proof>
=======
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../remove_duplicate.mlw">
<theory name="Spec">
</theory>
<theory name="RemoveDuplicateQuadratic">
<goal name="WP_parameter test_appears" expl="VC for test_appears">
<proof prover="2"><result status="valid" time="0.02" steps="45"/></proof>
>>>>>>> new_ide
</goal>
<goal name="VC remove_duplicate" expl="VC for remove_duplicate" proved="true">
<transf name="split_goal_wp" proved="true" >
......
......@@ -2,7 +2,6 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<<<<<<< HEAD
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../remove_duplicate_hash.mlw" proved="true">
<theory name="Spec" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
......@@ -14,19 +13,6 @@
<transf name="split_goal_wp" proved="true" >
<goal name="VC remove_duplicate.0" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
=======
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../remove_duplicate_hash.mlw">
<theory name="Spec">
</theory>
<theory name="MutableSet">
</theory>
<theory name="RemoveDuplicate">
<goal name="WP_parameter remove_duplicate" expl="VC for remove_duplicate">
<transf name="split_goal_wp">
<goal name="WP_parameter remove_duplicate.1" expl="index in array bounds">
<proof prover="0"><result status="valid" time="0.02" steps="4"/></proof>
>>>>>>> new_ide
</goal>
<goal name="VC remove_duplicate.1" expl="index in array bounds" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
......
......@@ -8,13 +8,8 @@
<prover id="9" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="10" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../residual.mlw" proved="true">
<<<<<<< HEAD
<theory name="Residuals" proved="true" sum="7626d24dde22aa6bc3fe43cd4373a346">
<goal name="VC accepts_epsilon" expl="VC for accepts_epsilon" proved="true">
=======
<theory name="Residuals" proved="true">
<goal name="WP_parameter accepts_epsilon" expl="VC for accepts_epsilon" proved="true">
>>>>>>> new_ide
<transf name="split_goal_wp" proved="true" >
<goal name="VC accepts_epsilon.0" expl="variant decrease" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="52"/></proof>
......@@ -155,7 +150,6 @@
</transf>
</goal>
</theory>
<<<<<<< HEAD
<theory name="Test" proved="true" sum="023a98c280f1d3500ceb9f682feef513">
<goal name="VC a" expl="VC for a" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="4"/></proof>
......@@ -167,15 +161,11 @@
<proof prover="9"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="VC test_astar" expl="VC for test_astar" proved="true">
=======
<theory name="Test" proved="true">
<goal name="WP_parameter test_astar" expl="VC for test_astar" proved="true">
>>>>>>> new_ide
<transf name="split_goal_wp" proved="true" >
</transf>
</goal>
</theory>
<theory name="DFA" proved="true">
<theory name="DFA" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
</file>
</why3session>
......@@ -2,7 +2,6 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<<<<<<< HEAD
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../resizable_array.mlw" proved="true">
<theory name="ResizableArraySpec" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
......@@ -178,35 +177,6 @@
<proof prover="0"><result status="valid" time="0.01" steps="34"/></proof>
</goal>
</transf>
=======
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../resizable_array.mlw">
<theory name="ResizableArraySpec">
</theory>
<theory name="ResizableArrayImplem">
<goal name="WP_parameter make" expl="VC for make">
<proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="WP_parameter mixfix []" expl="VC for mixfix []">
<proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="WP_parameter mixfix []&lt;-" expl="VC for mixfix []&lt;-">
<proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter resize" expl="VC for resize">
<proof prover="1" timelimit="5"><result status="valid" time="0.07" steps="87"/></proof>
</goal>
<goal name="WP_parameter append" expl="VC for append">
<proof prover="1"><result status="valid" time="0.02" steps="25"/></proof>
</goal>
</theory>
<theory name="Test">
<goal name="WP_parameter test1" expl="VC for test1">
<proof prover="1"><result status="valid" time="0.09" steps="13"/></proof>
</goal>
<goal name="WP_parameter test2" expl="VC for test2">
<proof prover="1"><result status="valid" time="0.02" steps="26"/></proof>
>>>>>>> new_ide
</goal>
</theory>
</file>
......
......@@ -6,13 +6,8 @@
<prover id="4" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../rightmostbittrick.mlw" proved="true">
<<<<<<< HEAD
<theory name="Rmbt" proved="true" sum="56adb784f9e137dcae55be610e66d665">
<goal name="VC rightmost_position_set" expl="VC for rightmost_position_set" proved="true">
=======
<theory name="Rmbt" proved="true">
<goal name="WP_parameter rightmost_position_set" expl="VC for rightmost_position_set" proved="true">
>>>>>>> new_ide
<transf name="split_goal_wp" proved="true" >
<goal name="VC rightmost_position_set.0" expl="loop invariant init" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="73"/></proof>
......
......@@ -7,28 +7,20 @@
<prover id="3" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../ropes.mlw" proved="true">
<<<<<<< HEAD
<theory name="String" proved="true" sum="07d9d0f3e492f325ffbd6a5edfc0223d">
<goal name="VC empty" expl="VC for empty" proved="true">
<proof prover="5"><result status="valid" time="0.00"/></proof>
</goal>
=======
<theory name="String" proved="true">
>>>>>>> new_ide
<goal name="app_assoc" proved="true">
<proof prover="5"><result status="valid" time="0.02"/></proof>