Commit 0a24262b authored by MARCHE Claude's avatar MARCHE Claude

updated sessions with Alt-ergo 0.95.2

parent 596bf275
......@@ -4,43 +4,46 @@
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.4pl4" timelimit="30" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.95.1" timelimit="5" memlimit="1000"/>
<prover id="3" name="Z3" version="2.19" timelimit="5" memlimit="1000"/>
<prover id="2" name="Z3" version="2.19" timelimit="5" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="4" name="CVC3" version="2.2" timelimit="5" memlimit="1000"/>
<prover id="5" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<prover id="6" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../double.why" expanded="true">
<theory name="BV_double" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="TestDouble" sum="6f68b2bb458812f8dac7a682020945e6" expanded="true">
<goal name="nth_one1" expanded="true">
<proof prover="2" timelimit="3"><result status="valid" time="0.55" steps="107"/></proof>
<proof prover="6" timelimit="3"><result status="valid" time="0.32" steps="107"/></proof>
</goal>
<goal name="nth_one2" expanded="true">
<proof prover="2" timelimit="3"><result status="valid" time="0.38" steps="105"/></proof>
<proof prover="6" timelimit="3"><result status="valid" time="0.20" steps="105"/></proof>
</goal>
<goal name="nth_one3">
<proof prover="2"><result status="valid" time="0.48" steps="111"/></proof>
<proof prover="6"><result status="valid" time="0.26" 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" steps="75"/></proof>
<proof prover="3"><result status="valid" time="0.11"/></proof>
<proof prover="2"><result status="valid" time="0.11"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.11"/></proof>
<proof prover="6"><result status="valid" time="0.03" steps="75"/></proof>
</goal>
<goal name="exp_one">
<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 name="exp_one" expanded="true">
<proof prover="0" edited="double_TestDouble_exp_one_1.v"><result status="valid" time="1.01"/></proof>
<proof prover="6" timelimit="30"><result status="valid" time="1.44" steps="305"/></proof>
</goal>
<goal name="mantissa_one">
<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>
<proof prover="2"><result status="valid" time="0.63"/></proof>
<proof prover="3"><result status="valid" time="0.36"/></proof>
<proof prover="5" timelimit="11"><result status="valid" time="2.74"/></proof>
<proof prover="6"><result status="valid" time="0.09" steps="105"/></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" steps="93"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="6"><result status="valid" time="0.04" steps="93"/></proof>
</goal>
</theory>
</file>
......
......@@ -4,79 +4,79 @@
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.4pl4" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.2" timelimit="5" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.95.1" timelimit="5" memlimit="1000"/>
<prover id="3" name="Z3" version="2.19" timelimit="5" memlimit="1000"/>
<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"/>
<prover id="2" name="Z3" version="2.19" timelimit="5" memlimit="1000"/>
<prover id="3" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
<prover id="4" name="Z3" version="3.2" timelimit="10" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../neg_as_xor.why" 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.53" steps="107"/></proof>
<proof prover="5" timelimit="3"><result status="valid" time="0.35" steps="107"/></proof>
</goal>
<goal name="sign_of_j" expanded="true">
<proof prover="2"><result status="valid" time="0.09" steps="100"/></proof>
<proof prover="5"><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" 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>
<proof prover="2"><result status="valid" time="0.61"/></proof>
<proof prover="3"><result status="valid" time="0.67"/></proof>
<proof prover="4"><result status="valid" time="3.22"/></proof>
<proof prover="5"><result status="valid" time="0.06" steps="104"/></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" 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>
<proof prover="2"><result status="valid" time="0.62"/></proof>
<proof prover="3"><result status="valid" time="0.70"/></proof>
<proof prover="4" timelimit="11"><result status="valid" time="2.67"/></proof>
<proof prover="5"><result status="valid" time="0.07" steps="107"/></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" 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>
<proof prover="2"><result status="valid" time="0.11"/></proof>
<proof prover="3"><result status="valid" time="0.13"/></proof>
<proof prover="4" timelimit="5"><result status="valid" time="0.10"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="93"/></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" steps="128"/></proof>
<proof prover="5"><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" steps="104"/></proof>
<proof prover="5"><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" steps="96"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></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>
<proof prover="4" timelimit="5"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="96"/></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="1.11"/></proof>
<proof prover="4"><result status="valid" time="1.32"/></proof>
<proof prover="5"><result status="valid" time="3.70"/></proof>
<proof prover="2"><result status="valid" time="0.63"/></proof>
<proof prover="3"><result status="valid" time="0.69"/></proof>
<proof prover="4"><result status="valid" time="2.62"/></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="1.12"/></proof>
<proof prover="4"><result status="valid" time="1.31"/></proof>
<proof prover="5"><result status="valid" time="4.01"/></proof>
<proof prover="2"><result status="valid" time="0.67"/></proof>
<proof prover="3"><result status="valid" time="0.72"/></proof>
<proof prover="4"><result status="valid" time="2.69"/></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.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>
<proof prover="2"><result status="valid" time="1.36"/></proof>
<proof prover="3"><result status="valid" time="0.94"/></proof>
<proof prover="4"><result status="valid" time="3.15"/></proof>
<proof prover="5" timelimit="6"><result status="valid" time="1.20" steps="142"/></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" steps="124"/></proof>
<proof prover="5" 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="2.75"/></proof>
<proof prover="0" edited="neg_as_xor_TestNegAsXOR_MainResult_1.v"><result status="valid" time="1.44"/></proof>
</goal>
</theory>
</file>
......
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