Commit 891d3ecb authored by MARCHE Claude's avatar MARCHE Claude

update obsolete sessions

parent d8e3b733
......@@ -11,35 +11,35 @@
<file name="../double.why" expanded="true">
<theory name="BV_double" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="TestDouble" sum="013924b8c2092a5a06b0a8db88480083" expanded="true">
<theory name="TestDouble" sum="6f68b2bb458812f8dac7a682020945e6" expanded="true">
<goal name="nth_one1" expanded="true">
<proof prover="2" timelimit="3"><result status="valid" time="0.33"/></proof>
<proof prover="2" timelimit="3"><result status="valid" time="0.55" steps="107"/></proof>
</goal>
<goal name="nth_one2" expanded="true">
<proof prover="2" timelimit="3"><result status="valid" time="0.23"/></proof>
<proof prover="2" timelimit="3"><result status="valid" time="0.38" steps="105"/></proof>
</goal>
<goal name="nth_one3">
<proof prover="2"><result status="valid" time="0.31"/></proof>
<proof prover="2"><result status="valid" time="0.48" steps="111"/></proof>
</goal>
<goal name="sign_one">
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="75"/></proof>
<proof prover="3"><result status="valid" time="0.11"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="exp_one">
<proof prover="0" edited="double_TestDouble_exp_one_1.v"><result status="valid" time="1.21"/></proof>
<proof prover="2" timelimit="30"><result status="valid" time="1.96"/></proof>
<proof prover="0" edited="double_TestDouble_exp_one_1.v"><result status="valid" time="2.09"/></proof>
<proof prover="2" timelimit="30"><result status="valid" time="2.72" steps="338"/></proof>
</goal>
<goal name="mantissa_one">
<proof prover="2"><result status="valid" time="0.09"/></proof>
<proof prover="3"><result status="valid" time="0.69"/></proof>
<proof prover="5" timelimit="11"><result status="valid" time="3.36"/></proof>
<proof prover="2"><result status="valid" time="0.09" steps="105"/></proof>
<proof prover="3"><result status="valid" time="1.18"/></proof>
<proof prover="5" timelimit="11"><result status="valid" time="3.96"/></proof>
</goal>
<goal name="double_value_of_1">
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="93"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
</theory>
......
......@@ -9,74 +9,74 @@
<prover id="4" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
<prover id="5" name="Z3" version="3.2" timelimit="10" memlimit="1000"/>
<file name="../neg_as_xor.why" expanded="true">
<theory name="TestNegAsXOR" sum="c372382d3a840fe2b5dc98379e370a05" expanded="true">
<theory name="TestNegAsXOR" sum="6138fee1d9542841b21ad746cad9a930" expanded="true">
<goal name="Nth_j" expanded="true">
<proof prover="2" timelimit="3"><result status="valid" time="0.34"/></proof>
<proof prover="2" timelimit="3"><result status="valid" time="0.53" steps="107"/></proof>
</goal>
<goal name="sign_of_j" expanded="true">
<proof prover="2"><result status="valid" time="0.09"/></proof>
<proof prover="2"><result status="valid" time="0.09" steps="100"/></proof>
</goal>
<goal name="mantissa_of_j" expanded="true">
<proof prover="1"><result status="valid" time="0.08"/></proof>
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="0.69"/></proof>
<proof prover="4"><result status="valid" time="0.83"/></proof>
<proof prover="5"><result status="valid" time="3.52"/></proof>
<proof prover="2"><result status="valid" time="0.06" steps="104"/></proof>
<proof prover="3"><result status="valid" time="1.06"/></proof>
<proof prover="4"><result status="valid" time="1.32"/></proof>
<proof prover="5"><result status="valid" time="4.65"/></proof>
</goal>
<goal name="exp_of_j" expanded="true">
<proof prover="1"><result status="valid" time="0.08"/></proof>
<proof prover="2"><result status="valid" time="0.07"/></proof>
<proof prover="3"><result status="valid" time="0.71"/></proof>
<proof prover="4"><result status="valid" time="0.83"/></proof>
<proof prover="5" timelimit="11"><result status="valid" time="3.15"/></proof>
<proof prover="2"><result status="valid" time="0.07" steps="107"/></proof>
<proof prover="3"><result status="valid" time="1.11"/></proof>
<proof prover="4"><result status="valid" time="1.32"/></proof>
<proof prover="5" timelimit="11"><result status="valid" time="3.99"/></proof>
</goal>
<goal name="int_of_bv" expanded="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="93"/></proof>
<proof prover="3"><result status="valid" time="0.11"/></proof>
<proof prover="4"><result status="valid" time="0.13"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="MainResultBits" expanded="true">
<proof prover="1"><result status="valid" time="0.10"/></proof>
<proof prover="2"><result status="valid" time="0.16"/></proof>
<proof prover="2"><result status="valid" time="0.16" steps="128"/></proof>
</goal>
<goal name="MainResultSign" expanded="true">
<proof prover="1"><result status="valid" time="0.05"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="104"/></proof>
</goal>
<goal name="Sign_of_xor_j" expanded="true">
<proof prover="1"><result status="valid" time="0.05"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="96"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Exp_of_xor_j" expanded="true">
<proof prover="1"><result status="valid" time="0.10"/></proof>
<proof prover="3"><result status="valid" time="0.71"/></proof>
<proof prover="4"><result status="valid" time="0.86"/></proof>
<proof prover="3"><result status="valid" time="1.11"/></proof>
<proof prover="4"><result status="valid" time="1.32"/></proof>
<proof prover="5"><result status="valid" time="3.70"/></proof>
</goal>
<goal name="Mantissa_of_xor_j" expanded="true">
<proof prover="1"><result status="valid" time="0.10"/></proof>
<proof prover="3"><result status="valid" time="0.72"/></proof>
<proof prover="4"><result status="valid" time="0.86"/></proof>
<proof prover="5"><result status="valid" time="2.92"/></proof>
<proof prover="3"><result status="valid" time="1.12"/></proof>
<proof prover="4"><result status="valid" time="1.31"/></proof>
<proof prover="5"><result status="valid" time="4.01"/></proof>
</goal>
<goal name="MainResultZero" expanded="true">
<proof prover="1"><result status="valid" time="0.07"/></proof>
<proof prover="2" timelimit="6"><result status="valid" time="1.36"/></proof>
<proof prover="3"><result status="valid" time="1.48"/></proof>
<proof prover="4"><result status="valid" time="1.01"/></proof>
<proof prover="5"><result status="valid" time="3.37"/></proof>
<proof prover="2" timelimit="6"><result status="valid" time="1.86" steps="142"/></proof>
<proof prover="3"><result status="valid" time="1.79"/></proof>
<proof prover="4"><result status="valid" time="1.56"/></proof>
<proof prover="5"><result status="valid" time="4.21"/></proof>
</goal>
<goal name="sign_neg" expanded="true">
<proof prover="1"><result status="valid" time="0.07"/></proof>
<proof prover="2" timelimit="9"><result status="valid" time="0.07"/></proof>
<proof prover="2" timelimit="9"><result status="valid" time="0.07" steps="124"/></proof>
</goal>
<goal name="MainResult" expanded="true">
<proof prover="0" edited="neg_as_xor_TestNegAsXOR_MainResult_1.v"><result status="valid" time="1.60"/></proof>
<proof prover="0" edited="neg_as_xor_TestNegAsXOR_MainResult_1.v"><result status="valid" time="2.75"/></proof>
</goal>
</theory>
</file>
......
......@@ -3,27 +3,27 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.2" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="10" memlimit="0"/>
<prover id="1" name="Alt-Ergo" version="0.94" timelimit="3" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.95.1" timelimit="3" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.94" timelimit="3" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="10" memlimit="0"/>
<prover id="4" name="Z3" version="2.19" timelimit="10" memlimit="0"/>
<prover id="5" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
<prover id="6" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<file name="../euclideandivision.why" expanded="true">
<theory name="Test" sum="3b7720f95864ec7c073afc25cbf14019" expanded="true">
<theory name="Test" sum="34acc475394bbedc4a443071938d84bc" 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>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="1"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="G2" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
......
This diff is collapsed.
......@@ -5,7 +5,7 @@
<prover id="0" name="CVC3" version="2.4.1" timelimit="23" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="3" memlimit="1000"/>
<file name="../bitvectors.why" expanded="true">
<theory name="TestBV" sum="02a0a66ee1427b60874134706846ccbb" expanded="true">
<theory name="TestBV" sum="a3a3c64f3ddb46c570b66630b2934e91" expanded="true">
<goal name="g1">
<proof prover="1"><result status="valid" time="0.00"/></proof>
</goal>
......
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment