Commit f0217599 authored by MARCHE Claude's avatar MARCHE Claude

last updated proofs, bench should be OK now

parent 906a5e14
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="hello_proof/why3session.xml">
<why3session name="examples/hello_proof/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="spass" name="Spass" version="3.7"/>
<prover id="vampire" name="Vampire" version="0.6"/>
<prover id="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../hello_proof.why" verified="false" expanded="true">
<theory name="HelloProof" verified="false" expanded="true">
<goal name="G1" sum="da0794d2f4de035d230d26e93d3e1afe" proved="true" expanded="true">
<goal name="G1" sum="da0794d2f4de035d230d26e93d3e1afe" proved="true" expanded="true" shape="t">
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="G2" sum="07e54d9a25fa3174d5d5bf7ce71a13dc" proved="false" expanded="true">
<goal name="G2" sum="07e54d9a25fa3174d5d5bf7ce71a13dc" proved="false" expanded="true" shape="fOtAfIt">
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.01"/>
<result status="unknown" time="0.00"/>
</proof>
<transf name="split_goal" proved="false" expanded="true">
<goal name="G2.1" sum="f7915ef009bdd949e4af326643583051" proved="false" expanded="true">
<goal name="G2.1" sum="f7915ef009bdd949e4af326643583051" proved="false" expanded="true" shape="fIt">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.03"/>
<result status="unknown" time="0.01"/>
</proof>
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.01"/>
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal name="G2.2" sum="c53f58872dc3cb71805234ace78f1c2d" proved="true" expanded="true">
<goal name="G2.2" sum="c53f58872dc3cb71805234ace78f1c2d" proved="true" expanded="true" shape="fOt">
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
</transf>
</goal>
<goal name="G3" sum="8813554ea4313f64f3efc3330036b5e9" proved="true" expanded="true">
<goal name="G3" sum="3c319e2d361d8bdd1e51c24c087a2981" proved="true" expanded="true" shape="ainfix >=ainfix *V0V0c0F">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
</theory>
......
This diff is collapsed.
......@@ -12,69 +12,69 @@
<prover id="z3" name="Z3" version="2.19"/>
<file name="../euler001.mlw" verified="false" expanded="true">
<theory name="SumMultiple" verified="false" expanded="true">
<goal name="div_minus1_1" sum="5266791566cb9e131f79837e51b72de8" proved="true" expanded="true" shape="ainfix =adivainfix +V0c1V1ainfix +adivV0V1c1Iainfix =amodainfix +V0c1V1c0Iainfix >V1c0Aainfix >=V0c0F">
<goal name="div_minus1_1" sum="cdd3562f55f63cb611a0132c05ca98ca" proved="true" expanded="true" shape="ainfix =adivainfix +V0c1V1ainfix +adivV0V1c1Iainfix =amodainfix +V0c1V1c0Iainfix >V1c0Aainfix >=V0c0F">
<proof prover="coq" timelimit="5" edited="euler001_SumMultiple_div_minus1_1_1.v" obsolete="false">
<result status="valid" time="0.52"/>
</proof>
</goal>
<goal name="div_minus1_2" sum="b75e15f7119a97ac29920a7a789b8e15" proved="false" expanded="true" shape="ainfix =adivainfix +V0c1V1adivV0V1Iainfix =amodainfix +V0c1V1c0NIainfix >V1c0Aainfix >=V0c0F">
<goal name="div_minus1_2" sum="880a384588861537dd14c6c81ff4c486" proved="false" expanded="true" shape="ainfix =adivainfix +V0c1V1adivV0V1Iainfix =amodainfix +V0c1V1c0NIainfix >V1c0Aainfix >=V0c0F">
<proof prover="simplify" timelimit="5" edited="" obsolete="false">
<result status="unknown" time="0.05"/>
<result status="unknown" time="0.03"/>
</proof>
<proof prover="cvc3" timelimit="5" edited="" obsolete="false">
<result status="timeout" time="5.01"/>
</proof>
<proof prover="alt-ergo" timelimit="5" edited="" obsolete="false">
<result status="unknown" time="0.23"/>
<result status="unknown" time="0.18"/>
</proof>
</goal>
<goal name="Closed_formula_0" sum="9d635abb360eeba223e62aea7d54449e" proved="true" expanded="true" shape="apc0">
<goal name="Closed_formula_0" sum="e571368fcfdafb904b02011fe4738d6d" proved="true" expanded="true" shape="apc0">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.12"/>
<result status="valid" time="0.04"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="Closed_formula_n" sum="14a06794c39f504fc3c7c61434c31a89" proved="true" expanded="true" shape="apV0Iainfix =amodV0c5c0NAainfix =amodV0c3c0NIapainfix -V0c1Iainfix >V0c0F">
<goal name="Closed_formula_n" sum="23e473c22d097771e4c1779a01fa66cd" proved="true" expanded="true" shape="apV0Iainfix =amodV0c5c0NAainfix =amodV0c3c0NIapainfix -V0c1Iainfix >V0c0F">
<proof prover="cvc3" timelimit="5" edited="" obsolete="false">
<result status="valid" time="0.23"/>
<result status="valid" time="0.17"/>
</proof>
</goal>
<goal name="Closed_formula_n_3" sum="759e99918260c7a3c5b1f4b5c33f42dd" proved="true" expanded="true" shape="apV0Iainfix =amodV0c5c0NAainfix =amodV0c3c0Iapainfix -V0c1Iainfix >V0c0F">
<goal name="Closed_formula_n_3" sum="f37ebf469350b84d8fe07680ddb07669" proved="true" expanded="true" shape="apV0Iainfix =amodV0c5c0NAainfix =amodV0c3c0Iapainfix -V0c1Iainfix >V0c0F">
<proof prover="alt-ergo" timelimit="5" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="Closed_formula_n_5" sum="380bc8b386b3035b1711cb23fa17a9da" proved="true" expanded="true" shape="apV0Iainfix =amodV0c5c0Aainfix =amodV0c3c0NIapainfix -V0c1Iainfix >V0c0F">
<goal name="Closed_formula_n_5" sum="920a40be17273efced19afb41780f310" proved="true" expanded="true" shape="apV0Iainfix =amodV0c5c0Aainfix =amodV0c3c0NIapainfix -V0c1Iainfix >V0c0F">
<proof prover="alt-ergo" timelimit="5" edited="" obsolete="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="Closed_formula_n_15" sum="cc0a4b0b292325909c6a8a65262645c3" proved="true" expanded="true" shape="apV0Iainfix =amodV0c5c0Aainfix =amodV0c3c0Iapainfix -V0c1Iainfix >V0c0F">
<goal name="Closed_formula_n_15" sum="f4111c740d97b136384ba23f8b1770b4" proved="true" expanded="true" shape="apV0Iainfix =amodV0c5c0Aainfix =amodV0c3c0Iapainfix -V0c1Iainfix >V0c0F">
<proof prover="alt-ergo" timelimit="5" edited="" obsolete="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="Closed_formula" sum="8e356511ca2b540b119a8650fd1519c4" proved="true" expanded="true" shape="apV0Iainfix <=c0V0F">
<goal name="Closed_formula" sum="01e41bad0857331f96b1adf1cb35d414" proved="true" expanded="true" shape="apV0Iainfix <=c0V0F">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.10"/>
<result status="valid" time="0.05"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.13"/>
<result status="valid" time="0.06"/>
</proof>
</goal>
</theory>
<theory name="WP Euler001" verified="true" expanded="true">
<goal name="WP_parameter solve" expl="normal postcondition" sum="76b404cbe7788d104d79907f50ebed27" proved="true" expanded="true" shape="ainfix =adivainfix -ainfix +ainfix *ainfix *c3adivainfix -V0c1c3ainfix +adivainfix -V0c1c3c1ainfix *ainfix *c5adivainfix -V0c1c5ainfix +adivainfix -V0c1c5c1ainfix *ainfix *c15adivainfix -V0c1c15ainfix +adivainfix -V0c1c15c1c2asum_multiple_3_5_ltV0Iainfix >=V0c1F">
<goal name="WP_parameter solve" expl="normal postcondition" sum="5b5236b942f4942a64a2d54b69346ce7" proved="true" expanded="true" shape="ainfix =adivainfix -ainfix +ainfix *ainfix *c3adivainfix -V0c1c3ainfix +adivainfix -V0c1c3c1ainfix *ainfix *c5adivainfix -V0c1c5ainfix +adivainfix -V0c1c5c1ainfix *ainfix *c15adivainfix -V0c1c15ainfix +adivainfix -V0c1c15c1c2asum_multiple_3_5_ltV0Iainfix >=V0c1F">
<proof prover="cvc3" timelimit="5" edited="" obsolete="false">
<result status="valid" time="2.63"/>
<result status="valid" time="1.80"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.13"/>
<result status="valid" time="0.10"/>
</proof>
</goal>
</theory>
......
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