Commit 3b7fd768 authored by MARCHE Claude's avatar MARCHE Claude

Update sessions where CVC4 1.2 fails on unknown "Real" sort

parent d3529345
......@@ -278,6 +278,6 @@ end
(*
Local Variables:
compile-command: "why3ide -L . double_of_int.why"
compile-command: "why3 ide -L . double_of_int.why"
End:
*)
......@@ -40,6 +40,6 @@ end
(*
Local Variables:
compile-command: "why3ide -L . neg_as_xor.why"
compile-command: "why3 ide -L . neg_as_xor.why"
End:
*)
......@@ -3,80 +3,105 @@
"http://why3.lri.fr/why3session.dtd">
<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="1" name="Alt-Ergo" version="0.99.1" timelimit="5" 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"/>
<prover id="3" name="CVC4" version="1.4" 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="6" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="7" name="CVC4" version="1.3" 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="5" timelimit="3"><result status="valid" time="0.35" steps="107"/></proof>
<goal name="Nth_j">
<proof prover="1"><result status="valid" time="0.56" steps="114"/></proof>
<proof prover="6" timelimit="3"><result status="valid" time="0.35" steps="107"/></proof>
</goal>
<goal name="sign_of_j" expanded="true">
<proof prover="5"><result status="valid" time="0.09" steps="100"/></proof>
<goal name="sign_of_j">
<proof prover="1"><result status="valid" time="0.15" steps="108"/></proof>
<proof prover="3"><result status="valid" time="0.86"/></proof>
<proof prover="6"><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.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 name="mantissa_of_j">
<proof prover="1"><result status="valid" time="0.16" steps="123"/></proof>
<proof prover="2"><result status="valid" time="0.78"/></proof>
<proof prover="3"><result status="valid" time="0.61"/></proof>
<proof prover="4"><result status="valid" time="0.85"/></proof>
<proof prover="5"><result status="valid" time="3.73"/></proof>
<proof prover="6"><result status="valid" time="0.06" steps="104"/></proof>
<proof prover="7"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="exp_of_j" expanded="true">
<proof prover="1"><result status="valid" time="0.08"/></proof>
<goal name="exp_of_j">
<proof prover="1"><result status="valid" time="0.17" steps="124"/></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>
<proof prover="3"><result status="valid" time="0.59"/></proof>
<proof prover="4"><result status="valid" time="0.92"/></proof>
<proof prover="5" timelimit="11"><result status="valid" time="3.13"/></proof>
<proof prover="6"><result status="valid" time="0.07" steps="107"/></proof>
<proof prover="7"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="int_of_bv" expanded="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
<goal name="int_of_bv">
<proof prover="1"><result status="valid" time="0.06" steps="94"/></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>
<proof prover="3"><result status="valid" time="0.05"/></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="6"><result status="valid" time="0.04" steps="93"/></proof>
<proof prover="7"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="MainResultBits" expanded="true">
<proof prover="1"><result status="valid" time="0.10"/></proof>
<proof prover="5"><result status="valid" time="0.16" steps="128"/></proof>
<goal name="MainResultBits">
<proof prover="1"><result status="valid" time="0.15" steps="132"/></proof>
<proof prover="3"><result status="valid" time="0.55"/></proof>
<proof prover="6"><result status="valid" time="0.16" steps="128"/></proof>
<proof prover="7"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="MainResultSign" expanded="true">
<proof prover="1"><result status="valid" time="0.05"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="104"/></proof>
<goal name="MainResultSign">
<proof prover="1"><result status="valid" time="0.04" steps="102"/></proof>
<proof prover="3"><result status="valid" time="0.06"/></proof>
<proof prover="6"><result status="valid" time="0.03" steps="104"/></proof>
<proof prover="7"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="Sign_of_xor_j" expanded="true">
<proof prover="1"><result status="valid" time="0.05"/></proof>
<goal name="Sign_of_xor_j">
<proof prover="1"><result status="valid" time="0.04" steps="85"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><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>
<proof prover="3"><result status="valid" time="0.05"/></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="6"><result status="valid" time="0.03" steps="96"/></proof>
<proof prover="7"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="Exp_of_xor_j" expanded="true">
<proof prover="1"><result status="valid" time="0.10"/></proof>
<goal name="Exp_of_xor_j">
<proof prover="1"><result status="valid" time="1.53" steps="498"/></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>
<proof prover="3"><result status="valid" time="0.65"/></proof>
<proof prover="4"><result status="valid" time="0.87"/></proof>
<proof prover="5"><result status="valid" time="3.00"/></proof>
<proof prover="7"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="Mantissa_of_xor_j" expanded="true">
<proof prover="1"><result status="valid" time="0.10"/></proof>
<goal name="Mantissa_of_xor_j">
<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>
<proof prover="3"><result status="valid" time="0.66"/></proof>
<proof prover="4"><result status="valid" time="0.72"/></proof>
<proof prover="5"><result status="valid" time="2.69"/></proof>
<proof prover="7"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="MainResultZero" expanded="true">
<proof prover="1"><result status="valid" time="0.07"/></proof>
<goal name="MainResultZero">
<proof prover="1"><result status="valid" time="0.07" steps="104"/></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>
<proof prover="3"><result status="valid" time="0.06"/></proof>
<proof prover="4"><result status="valid" time="0.94"/></proof>
<proof prover="5"><result status="valid" time="3.57"/></proof>
<proof prover="6" timelimit="6"><result status="valid" time="1.20" steps="142"/></proof>
<proof prover="7"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="sign_neg" expanded="true">
<proof prover="1"><result status="valid" time="0.07"/></proof>
<proof prover="5" timelimit="9"><result status="valid" time="0.07" steps="124"/></proof>
<goal name="sign_neg">
<proof prover="1"><result status="valid" time="0.07" steps="107"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="6" timelimit="9"><result status="valid" time="0.07" steps="124"/></proof>
<proof prover="7"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="MainResult" expanded="true">
<proof prover="0" edited="neg_as_xor_TestNegAsXOR_MainResult_1.v"><result status="valid" time="1.44"/></proof>
<goal name="MainResult">
<proof prover="0" edited="neg_as_xor_TestNegAsXOR_MainResult_1.v"><result status="valid" time="2.42"/></proof>
<proof prover="1"><result status="valid" time="2.27" steps="326"/></proof>
</goal>
</theory>
</file>
......
......@@ -3,63 +3,74 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.4pl4" timelimit="5" memlimit="4000"/>
<prover id="1" name="CVC4" version="1.2" timelimit="5" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="3" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.95.1" timelimit="5" memlimit="1000"/>
<prover id="4" name="MetiTarski" version="2.2" timelimit="5" memlimit="1000"/>
<prover id="5" name="MetiTarski" version="2.4" timelimit="5" memlimit="1000"/>
<prover id="6" name="CVC3" version="2.2" timelimit="3" memlimit="1000"/>
<prover id="7" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
<prover id="8" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<prover id="9" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="6" name="MetiTarski" version="2.4" timelimit="5" memlimit="1000"/>
<prover id="7" name="CVC3" version="2.2" timelimit="3" memlimit="1000"/>
<prover id="8" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
<prover id="9" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<prover id="10" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="11" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<prover id="12" name="CVC4" version="1.3" timelimit="5" memlimit="1000"/>
<file name="../lagrange_inequality.why" expanded="true">
<theory name="LagrangeInequality" sum="5e115a67d12d3b9e0cb091836baf8f27" expanded="true">
<goal name="norm2_pos" expanded="true">
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
<goal name="norm2_pos">
<proof prover="6"><result status="valid" time="0.02"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="11"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Lagrange" expanded="true">
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
<goal name="Lagrange">
<proof prover="6"><result status="valid" time="0.01"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="11"><result status="valid" time="0.00"/></proof>
</goal>
</theory>
<theory name="CauchySchwarzInequality" sum="6fcd96c715b7475a71d99c0f82d79af4" expanded="true">
<goal name="CauchySchwarz_aux" expanded="true">
<proof prover="1"><result status="valid" time="1.30"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
<goal name="CauchySchwarz_aux">
<proof prover="6"><result status="valid" time="0.02"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="valid" time="3.19"/></proof>
</goal>
<goal name="norm_pos" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<goal name="norm_pos">
<proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="10"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="11"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="sqr_le_sqrt" expanded="true">
<goal name="sqr_le_sqrt">
<proof prover="0" edited="lagrange_inequality_CauchySchwarzInequality_sqr_le_sqrt_1.v"><result status="valid" time="2.67"/></proof>
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="5"><result status="valid" time="0.04"/></proof>
<proof prover="6"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="CauchySchwarz" expanded="true">
<goal name="CauchySchwarz">
<proof prover="0" edited="lagrange_inequality_CauchySchwarzInequality_CauchySchwarz_1.v"><result status="valid" time="2.55"/></proof>
<proof prover="5"><result status="valid" time="0.22"/></proof>
<proof prover="6"><result status="valid" time="0.22"/></proof>
</goal>
</theory>
<theory name="TriangleInequality" sum="c1ce71fbadfa600580a354699d029b51" expanded="true">
<goal name="triangle_aux" expanded="true">
<proof prover="7"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.01"/></proof>
<goal name="triangle_aux">
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="sqr_sqrt_le" expanded="true">
<goal name="sqr_sqrt_le">
<proof prover="1"><result status="valid" time="0.02" steps="10"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="11"/></proof>
<proof prover="4"><result status="valid" time="0.05"/></proof>
<proof prover="5"><result status="valid" time="0.06"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
<proof prover="9"><result status="valid" time="0.05" steps="11"/></proof>
<proof prover="6"><result status="valid" time="0.06"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
<proof prover="10"><result status="valid" time="0.05" steps="11"/></proof>
</goal>
<goal name="triangle" expanded="true">
<goal name="triangle">
<proof prover="0" memlimit="1000" edited="lagrange_inequality_TriangleInequality_triangle_1.v"><result status="valid" time="2.13"/></proof>
</goal>
</theory>
......
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