Commit 931cb8e9 authored by MARCHE Claude's avatar MARCHE Claude

update obsolete sessions

parent 185b87df
......@@ -2,11 +2,11 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<prover id="0" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../add_list.mlw" expanded="true">
<theory name="SumList" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="AddListRec" sum="d0925178b08b43ca97d60c4da19b85cc" expanded="true">
<theory name="AddListRec" sum="b22282c439ddd5fa9976e2048ec06a22" expanded="true">
<goal name="VC sum" expl="VC for sum" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
......@@ -14,7 +14,7 @@
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
<theory name="AddListImp" sum="1f63599ecd6b1d6b1c6113dfada8e75b" expanded="true">
<theory name="AddListImp" sum="f7b23f93ac300ff2dca6f1bdf5f7fec6" expanded="true">
<goal name="VC sum" expl="VC for sum" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
......
......@@ -10,7 +10,7 @@
<file name="../double.why" expanded="true">
<theory name="BV_double" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="TestDouble" sum="67e55b147b71189823b73b33c59d4e7d" expanded="true">
<theory name="TestDouble" sum="c89fbb147b776539629dfab2176a2ff7" expanded="true">
<goal name="nth_one1" expanded="true">
<proof prover="0" timelimit="3"><result status="valid" time="0.05" steps="77"/></proof>
</goal>
......
......@@ -10,7 +10,7 @@
<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"/>
<file name="../double_of_int.why" expanded="true">
<theory name="DoubleOfInt" sum="33362b399a2da43d9c14a773b258baeb" expanded="true">
<theory name="DoubleOfInt" sum="1c3d63150b3ece6de4c16efcf90e5b1e" expanded="true">
<goal name="nth_j1">
<proof prover="1"><result status="valid" time="0.04" steps="78"/></proof>
</goal>
......@@ -90,7 +90,7 @@
</goal>
<goal name="to_nat_mantissa_1">
<proof prover="1"><result status="valid" time="0.05" steps="91"/></proof>
<proof prover="4"><result status="valid" time="1.10"/></proof>
<proof prover="4"><result status="valid" time="0.82"/></proof>
<proof prover="6" timelimit="10"><result status="valid" time="2.87"/></proof>
<proof prover="8"><result status="valid" time="0.76"/></proof>
</goal>
......@@ -133,7 +133,7 @@
<proof prover="1"><result status="valid" time="0.04" steps="87"/></proof>
<proof prover="2"><result status="valid" time="0.05"/></proof>
<proof prover="4"><result status="valid" time="0.05"/></proof>
<proof prover="6" timelimit="10"><result status="valid" time="3.28"/></proof>
<proof prover="6" timelimit="10"><result status="valid" time="2.74"/></proof>
<proof prover="8"><result status="valid" time="0.75"/></proof>
</goal>
<goal name="nth_0_30">
......@@ -146,7 +146,7 @@
<proof prover="4"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="nth_var31">
<proof prover="1" timelimit="125"><result status="valid" time="4.27" steps="253"/></proof>
<proof prover="1" timelimit="125"><result status="valid" time="5.40" steps="280"/></proof>
<proof prover="4"><result status="valid" time="1.90"/></proof>
</goal>
<goal name="to_nat_sub_0_30">
......@@ -155,7 +155,7 @@
<proof prover="8"><result status="valid" time="0.84"/></proof>
</goal>
<goal name="jpxorx_pos">
<proof prover="1"><result status="valid" time="0.87" steps="154"/></proof>
<proof prover="1"><result status="valid" time="0.87" steps="153"/></proof>
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="4"><result status="valid" time="0.08"/></proof>
<proof prover="6"><result status="valid" time="0.11"/></proof>
......@@ -243,7 +243,7 @@
<proof prover="8"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="lemma3">
<proof prover="4"><result status="valid" time="2.44"/></proof>
<proof prover="4"><result status="valid" time="2.03"/></proof>
</goal>
<goal name="nth_var9">
<proof prover="1"><result status="valid" time="0.10" steps="95"/></proof>
......@@ -302,8 +302,8 @@
</goal>
<goal name="MainResult">
<proof prover="1"><result status="valid" time="1.56" steps="139"/></proof>
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="4"><result status="valid" time="0.09"/></proof>
<proof prover="2"><result status="valid" time="0.26"/></proof>
<proof prover="4"><result status="valid" time="2.18"/></proof>
<proof prover="6" timelimit="11"><result status="valid" time="2.99"/></proof>
<proof prover="8"><result status="valid" time="0.76"/></proof>
</goal>
......
......@@ -7,24 +7,24 @@
<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"/>
<file name="../neg_as_xor.why" expanded="true">
<theory name="TestNegAsXOR" sum="8ffcc918b8abe3e91a67abb587fbef49" expanded="true">
<theory name="TestNegAsXOR" sum="028ffca9bbc8928ca4030df336908e88" expanded="true">
<goal name="Nth_j">
<proof prover="1"><result status="valid" time="0.05" steps="77"/></proof>
</goal>
<goal name="sign_of_j">
<proof prover="1"><result status="valid" time="0.15" steps="76"/></proof>
<proof prover="3"><result status="valid" time="3.42"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="76"/></proof>
<proof prover="3"><result status="valid" time="2.82"/></proof>
</goal>
<goal name="mantissa_of_j">
<proof prover="1"><result status="valid" time="0.16" steps="121"/></proof>
<proof prover="3"><result status="valid" time="1.10"/></proof>
<proof prover="5"><result status="valid" time="3.37"/></proof>
<proof prover="3"><result status="valid" time="0.85"/></proof>
<proof prover="5"><result status="valid" time="2.61"/></proof>
<proof prover="9"><result status="valid" time="0.78"/></proof>
</goal>
<goal name="exp_of_j">
<proof prover="1"><result status="valid" time="0.17" steps="122"/></proof>
<proof prover="3"><result status="valid" time="1.07"/></proof>
<proof prover="5" timelimit="11"><result status="valid" time="3.10"/></proof>
<proof prover="5" timelimit="11"><result status="valid" time="2.63"/></proof>
<proof prover="9"><result status="valid" time="0.73"/></proof>
</goal>
<goal name="int_of_bv">
......@@ -34,28 +34,28 @@
<proof prover="9"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="MainResultBits">
<proof prover="1"><result status="valid" time="0.15" steps="130"/></proof>
<proof prover="1"><result status="valid" time="0.15" steps="125"/></proof>
<proof prover="3"><result status="valid" time="1.03"/></proof>
</goal>
<goal name="MainResultSign">
<proof prover="1"><result status="valid" time="0.04" steps="102"/></proof>
<proof prover="1"><result status="valid" time="0.04" steps="92"/></proof>
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="Sign_of_xor_j">
<proof prover="1"><result status="valid" time="0.04" steps="85"/></proof>
<proof prover="1"><result status="valid" time="0.04" steps="87"/></proof>
<proof prover="3"><result status="valid" time="0.05"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Exp_of_xor_j">
<proof prover="1"><result status="valid" time="1.72" steps="492"/></proof>
<proof prover="3"><result status="valid" time="1.20"/></proof>
<proof prover="3"><result status="valid" time="0.97"/></proof>
<proof prover="5"><result status="valid" time="2.98"/></proof>
<proof prover="9"><result status="valid" time="0.88"/></proof>
</goal>
<goal name="Mantissa_of_xor_j">
<proof prover="3"><result status="valid" time="1.21"/></proof>
<proof prover="5"><result status="valid" time="3.36"/></proof>
<proof prover="3"><result status="valid" time="0.96"/></proof>
<proof prover="5"><result status="valid" time="2.74"/></proof>
<proof prover="9"><result status="valid" time="0.75"/></proof>
</goal>
<goal name="MainResultZero">
......@@ -65,11 +65,11 @@
<proof prover="9"><result status="valid" time="1.30"/></proof>
</goal>
<goal name="sign_neg">
<proof prover="1"><result status="valid" time="0.07" steps="107"/></proof>
<proof prover="1"><result status="valid" time="0.07" steps="84"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="MainResult">
<proof prover="1"><result status="valid" time="2.21" steps="320"/></proof>
<proof prover="1"><result status="valid" time="1.88" steps="320"/></proof>
</goal>
</theory>
</file>
......
......@@ -10,7 +10,7 @@
<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"/>
<file name="../power2.why" expanded="true">
<theory name="Pow2int" sum="66aadb2d4ebebe837dd89ae394896e69">
<theory name="Pow2int" sum="5a9c50ddf0323dc2305005ff45b6d0f7">
<goal name="Power_1">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
......@@ -357,7 +357,7 @@
</goal>
<goal name="pow2_55">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="6" timelimit="11"><result status="valid" time="3.45"/></proof>
<proof prover="6" timelimit="11"><result status="valid" time="3.00"/></proof>
<proof prover="9"><result status="valid" time="2.11"/></proof>
<proof prover="10"><result status="valid" time="0.03" steps="58"/></proof>
</goal>
......@@ -405,7 +405,7 @@
</goal>
<goal name="pow2_63">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="6" timelimit="9"><result status="valid" time="9.15"/></proof>
<proof prover="6" timelimit="9"><result status="valid" time="7.93"/></proof>
<proof prover="9"><result status="valid" time="2.72"/></proof>
<proof prover="10"><result status="valid" time="0.03" steps="66"/></proof>
</goal>
......@@ -434,7 +434,7 @@
<proof prover="4" edited="power2_Pow2int_Mod_pow2_gen_1.v"><result status="valid" time="0.86"/></proof>
</goal>
</theory>
<theory name="Pow2real" sum="db3613dd703c21eb418036b6239dea64" expanded="true">
<theory name="Pow2real" sum="10697054f915877b6223d448be038d47" expanded="true">
<goal name="Power_s_all">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
......
......@@ -3,7 +3,7 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../11244.why" expanded="true">
<theory name="T1" sum="cd24ef0e074ac2a11b578499c99293b5" expanded="true">
<theory name="T1" sum="4b9cfee725642a6af0dc7fdab261142e" expanded="true">
<goal name="G" expanded="true">
<transf name="inline_goal" expanded="true">
<goal name="G.1" expl="1." expanded="true">
......
......@@ -7,7 +7,7 @@
<prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../12475.why" expanded="true">
<theory name="Stmt" sum="677583f1dc7adc69d11e6ebb2f963be1" expanded="true">
<theory name="Stmt" sum="f2e23bc6c52360c346f78a5be969b6b4" expanded="true">
<goal name="toto" expanded="true">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6" timelimit="10" steplimit="0" memlimit="0"/>
<file name="../12934.why" expanded="true">
<theory name="BTS12934" sum="e32351513bba9a37f680056dd466bcee" expanded="true">
<theory name="BTS12934" sum="a1c52743c237f96f62b5a441ad065efb" expanded="true">
<goal name="t" expanded="true">
<proof prover="0" edited="12934_BTS12934_t_1.v"><result status="valid" time="0.29"/></proof>
</goal>
......
......@@ -6,8 +6,8 @@
<file name="../13375.mlw" expanded="true">
<theory name="Signed" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Spec" sum="842a49486addf486ba4df5d89847a4c5" expanded="true">
<goal name="WP_parameter to_int_" expl="VC for to_int_" expanded="true">
<theory name="Spec" sum="22058b50719d40b4273aecf6b8f9fa7d" expanded="true">
<goal name="VC to_int_" expl="VC for to_int_" expanded="true">
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
</theory>
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6" timelimit="10" steplimit="0" memlimit="0"/>
<file name="../13849.why" expanded="true">
<theory name="T" sum="fe6d0a97ed129807ad9b025e583a359d" expanded="true">
<theory name="T" sum="9002cd307075906fccf3007350013be9" expanded="true">
<goal name="x" expanded="true">
<proof prover="0" edited="13849_T_x_2.v"><result status="valid" time="0.29"/></proof>
</goal>
......
......@@ -4,11 +4,11 @@
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../13853.mlw" expanded="true">
<theory name="T" sum="2430bcb65aef3532d84a6af26f6f2f7d" expanded="true">
<goal name="WP_parameter f" expl="VC for f" expanded="true">
<theory name="T" sum="b85e14f67684c9a27b02859147f7db9d" expanded="true">
<goal name="VC f" expl="VC for f" expanded="true">
<proof prover="1"><result status="valid" time="0.00" steps="0"/></proof>
</goal>
<goal name="WP_parameter g" expl="VC for g" expanded="true">
<goal name="VC g" expl="VC for g" expanded="true">
<proof prover="1"><result status="valid" time="0.00" steps="0"/></proof>
</goal>
</theory>
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="0"/>
<file name="../13854.why">
<theory name="T" sum="e0ed6fa44df780ea63fc8d3dbdece469" expanded="true">
<theory name="T" sum="b5806ff59fa2827b1dd2b7113af851bc" expanded="true">
<goal name="g" expanded="true">
<proof prover="0" edited="13854_T_g_1.v"><result status="valid" time="0.29"/></proof>
</goal>
......
......@@ -4,9 +4,9 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../16972.mlw" expanded="true">
<theory name="M" sum="b40b79efefdda1a37e6543d056f2f5c8" expanded="true">
<goal name="WP_parameter fail" expl="VC for fail" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
<theory name="M" sum="e46e0b90f27007a30c9a171e6ab8dfb8" expanded="true">
<goal name="VC fail" expl="VC for fail" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
</theory>
</file>
......
......@@ -7,7 +7,7 @@
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="5" name="Z3" version="4.3.2" timelimit="10" steplimit="0" memlimit="0"/>
<file name="../ac.why" expanded="true">
<theory name="Test" sum="83d8b556674b949a66206b6d5ca52ded" expanded="true">
<theory name="Test" sum="f7efb6d8dac3d9d67fe5bf05cbc59cfd" expanded="true">
<goal name="G1" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
......
......@@ -8,7 +8,7 @@
<prover id="6" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="7" name="Z3" version="4.3.2" timelimit="10" steplimit="0" memlimit="0"/>
<file name="../array.why" expanded="true">
<theory name="Test_simplify_array" sum="6cb2fd4ede8c2e597266ad5a6f4953c4" expanded="true">
<theory name="Test_simplify_array" sum="3c13dce5e3719508c4d50860f8a45ee8" expanded="true">
<goal name="G1" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
......
......@@ -7,7 +7,7 @@
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="4.3.2" timelimit="10" steplimit="0" memlimit="0"/>
<file name="../bool.why" expanded="true">
<theory name="Test" sum="1df769008ab78b260468adc25cb91f79" expanded="true">
<theory name="Test" sum="e5e96cabd76b36e183b1ec65524d971f" expanded="true">
<goal name="G1" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
......
......@@ -9,12 +9,12 @@
<prover id="8" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="9" name="Z3" version="4.3.2" timelimit="10" steplimit="0" memlimit="0"/>
<file name="../euclideandivision.why" expanded="true">
<theory name="Test" sum="34acc475394bbedc4a443071938d84bc" expanded="true">
<theory name="Test" sum="3cb3c9906da38c258770d7ffcde5a5cd" expanded="true">
<goal name="G1" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="7"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="7"><result status="valid" time="0.01" steps="0"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
......@@ -22,7 +22,7 @@
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="7"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="7"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
......
......@@ -7,7 +7,7 @@
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="5" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="0"/>
<file name="../floats.why" expanded="true">
<theory name="TestGappa" sum="60492cc2e291d829691100bfb714944d" expanded="true">
<theory name="TestGappa" sum="0212aee6ef6d767a0f51ca8a2925a828" expanded="true">
<goal name="Round_single_01" expanded="true">
<proof prover="1"><result status="valid" time="0.00"/></proof>
</goal>
......
......@@ -10,12 +10,12 @@
<prover id="8" name="Eprover" version="1.8-001" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="9" name="Z3" version="4.3.2" timelimit="10" steplimit="0" memlimit="0"/>
<file name="../int.why" expanded="true">
<theory name="Test" sum="fc4f5a5b6868cb7535da7ff9ae921fff" expanded="true">
<theory name="Test" sum="53fb0c3a697322674cfc56b54fd13a6a" expanded="true">
<goal name="G1" expanded="true">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="timeout" time="1.00"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="unknown" time="1.09"/></proof>
<proof prover="6"><result status="unknown" time="2.06"/></proof>
<proof prover="7"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="8"><result status="timeout" time="1.00"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
......@@ -24,7 +24,7 @@
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="timeout" time="0.98"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="unknown" time="1.06"/></proof>
<proof prover="6"><result status="unknown" time="1.99"/></proof>
<proof prover="7"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="8"><result status="timeout" time="1.00"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
......@@ -78,16 +78,16 @@
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="timeout" time="1.00"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="unknown" time="1.08"/></proof>
<proof prover="6"><result status="unknown" time="2.06"/></proof>
<proof prover="7"><result status="valid" time="0.00" steps="1"/></proof>
<proof prover="8"><result status="valid" time="0.04"/></proof>
<proof prover="8"><result status="valid" time="0.58"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="SquareNonNeg" expanded="true">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="timeout" time="0.99"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="unknown" time="1.07"/></proof>
<proof prover="6"><result status="unknown" time="2.07"/></proof>
<proof prover="7"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="8"><result status="valid" time="0.09"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
......@@ -102,12 +102,12 @@
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
</theory>
<theory name="MinMax" sum="5a65a1cfb37258d4746169718f12d1d3" expanded="true">
<theory name="MinMax" sum="6add47dbf3d2322b0ea38a50d911b554" expanded="true">
<goal name="G" expanded="true">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="timeout" time="1.00"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="unknown" time="1.08"/></proof>
<proof prover="6"><result status="unknown" time="1.96"/></proof>
<proof prover="7"><result status="valid" time="0.00" steps="5"/></proof>
<proof prover="8"><result status="timeout" time="1.00"/></proof>
<proof prover="9"><result status="valid" time="0.01"/></proof>
......
......@@ -9,7 +9,7 @@
<prover id="8" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="9" name="Z3" version="4.3.2" timelimit="10" steplimit="0" memlimit="0"/>
<file name="../intreal.why" expanded="true">
<theory name="IntReal" sum="a3fbe528ec2ad0f8c6370c74f29f4c65" expanded="true">
<theory name="IntReal" sum="c554e83e9bde4ee6b64d253c6f27d4d8" expanded="true">
<goal name="G1" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
......
......@@ -7,7 +7,7 @@
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="5" name="Z3" version="4.3.2" timelimit="10" steplimit="0" memlimit="0"/>
<file name="../minmax.why" expanded="true">
<theory name="MinMax" sum="f36cdaa208948cc789cc9e1e3ab076fd" expanded="true">
<theory name="MinMax" sum="d906b00bdf45593fa379225b31a1cbdd" expanded="true">
<goal name="G" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
......
......@@ -7,7 +7,7 @@
<prover id="3" name="Spass" version="3.7" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="0"/>
<file name="../propositional.why">
<theory name="Prop" sum="8b1e7bd663bc5a4ded39c68541ddf2ba" expanded="true">
<theory name="Prop" sum="5ef7b9f44a533c33c748fd44c6a647c2" expanded="true">
<goal name="G" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
......
......@@ -10,7 +10,7 @@
<prover id="12" name="Alt-Ergo" version="0.99.1" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="14" name="Z3" version="4.3.2" timelimit="3" steplimit="0" memlimit="0"/>
<file name="../real.why" expanded="true">
<theory name="Test" sum="cf206e9b789e3b16bbeee98ff5359bb7" expanded="true">
<theory name="Test" sum="f930be850aa22b603301174419cda7db" expanded="true">
<goal name="G1" expanded="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
......@@ -33,7 +33,7 @@
<proof prover="14"><result status="valid" time="0.00"/></proof>
</goal>
</theory>
<theory name="TestInfix" sum="9929e0fb7685505424762277d915662a" expanded="true">
<theory name="TestInfix" sum="2665d48e7626fbbd77985b2f32e0fcf2" expanded="true">
<goal name="Add" expanded="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
......@@ -76,7 +76,7 @@
<proof prover="14"><result status="valid" time="0.00"/></proof>
</goal>
</theory>
<theory name="SquareTest" sum="b399f090ec659c1b880d355f5452fbc9" expanded="true">
<theory name="SquareTest" sum="8ddbcfd1eefeab998320ca66edb520da" expanded="true">
<goal name="Sqrt_zero" expanded="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="8" timelimit="60" memlimit="1000"><result status="valid" time="0.02"/></proof>
......@@ -93,12 +93,12 @@
</goal>
<goal name="Sqrt_four" expanded="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="8" timelimit="67" memlimit="1000"><result status="valid" time="25.68"/></proof>
<proof prover="8" timelimit="67" memlimit="1000"><result status="valid" time="22.56"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
<proof prover="12" timelimit="5" memlimit="1000"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
</theory>
<theory name="ExpLogTest" sum="b87cf6a8ae7e92621e77bacb7a1fd605" expanded="true">
<theory name="ExpLogTest" sum="8e38899dec493f27f7e90a1ddb3d79a8" expanded="true">
<goal name="Log_e" expanded="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.01"/></proof>
......@@ -106,7 +106,7 @@
<proof prover="14"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
<theory name="PowerIntTest" sum="a44ed7f266568491fd1a5efcfad78047" expanded="true">
<theory name="PowerIntTest" sum="6cd993ffabcf431462d22cf3111dd4b2" expanded="true">
<goal name="Pow_2_2" expanded="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.01"/></proof>
......@@ -114,14 +114,14 @@
<proof prover="14"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
<theory name="PowerRealTest" sum="eb0bbfff015add810d5cc4a17172919b" expanded="true">
<theory name="PowerRealTest" sum="1c72c25cc458736ebd1c284dbbad722c" expanded="true">
<goal name="Pow_2_2" expanded="true">
<proof prover="8"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="6"/></proof>
<proof prover="14"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
<theory name="TrigonometryTest" sum="166c58f27a3755c03fcdf81fc1b4a5bf" expanded="true">
<theory name="TrigonometryTest" sum="e9117dcf6465925bcbebf07e3d99bb04" expanded="true">
<goal name="Cos_2_pi" expanded="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.09"/></proof>
......
......@@ -25,7 +25,7 @@
<transf name="simplify_trivial_quantification">
<goal name="reformulation.1.1" expl="1.">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
<proof prover="13" obsolete="true"><result status="valid" time="0.00" steps="3"/></proof>
<proof prover="13"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
</transf>
</goal>
......@@ -33,7 +33,7 @@
<transf name="simplify_trivial_quantification">
<goal name="reformulation.2.1" expl="1.">
<proof prover="0"><result status="valid" time="0.00" steps="13"/></proof>
<proof prover="18" obsolete="true"><result status="valid" time="0.00"/></proof>
<proof prover="18"><result status="valid" time="0.00"/></proof>
</goal>
</transf>
</goal>
......
......@@ -5,7 +5,7 @@
<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" expanded="true">
<theory name="Imp" sum="3b90bd1ffd336bb62782238529a2e860">
<theory name="Imp" sum="5b5d357c792abb7a8c14aed6fba73a7c">
<goal name="ceval_deterministic_aux">
<transf name="induction_pr">
<goal name="ceval_deterministic_aux.1" expl="1.">
......@@ -14,7 +14,7 @@
<proof prover="2"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="ceval_deterministic_aux.1.2" expl="2.">
<proof prover="2"><result status="valid" time="0.03" steps="20"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="22"/></proof>
</goal>
<goal name="ceval_deterministic_aux.1.3" expl="3.">
<proof prover="2"><result status="valid" time="0.02" steps="18"/></proof>
......@@ -36,25 +36,25 @@
<goal name="ceval_deterministic_aux.2" expl="2.">
<transf name="inversion_pr">
<goal name="ceval_deterministic_aux.2.1" expl="1.">
<proof prover="2"><result status="valid" time="0.03" steps="20"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="22"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2.2" expl="2.">
<proof prover="2"><result status="valid" time="0.02" steps="25"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="58"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2.3" expl="3.">
<proof prover="2"><result status="valid" time="0.02" steps="25"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="27"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2.4" expl="4.">
<proof prover="2"><result status="valid" time="0.03" steps="26"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="28"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2.5" expl="5.">
<proof prover="2"><result status="valid" time="0.03" steps="26"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="28"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2.6" expl="6.">
<proof prover="2"><result status="valid" time="0.02" steps="24"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="26"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2.7" expl="7.">
<proof prover="2"><result status="valid" time="0.02" steps="26"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="28"/></proof>
</goal>
</transf>
</goal>
......@@ -64,7 +64,7 @@
<proof prover="2"><result status="valid" time="0.02" steps="18"/></proof>
</goal>
<goal name="ceval_deterministic_aux.3.2" expl="2.">
<proof prover="2"><result status="valid" time="0.02" steps="25"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="27"/></proof>
</goal>
<goal name="ceval_deterministic_aux.3.3" expl="3.">
<proof prover="0"><result status="valid" time="0.11"/></proof>
......@@ -89,7 +89,7 @@
<proof prover="2"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="ceval_deterministic_aux.4.2" expl="2.">
<proof prover="2"><result status="valid" time="0.02" steps="26"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="28"/></proof>
</goal>
<goal name="ceval_deterministic_aux.4.3" expl="3.">
<proof prover="2"><result status="valid" time="0.03" steps="24"/></proof>
......@@ -114,7 +114,7 @@