Commit b2fedb65 authored by MARCHE Claude's avatar MARCHE Claude

update proofs of hello_proof.why

parent aa554a31
......@@ -44,6 +44,11 @@
* Add more examples in the regression tests and in the proval gallery
* prover support
** avoid bug of CVC3, e.g in examples/my_cosine.why
** test/debug TPTP output, make Vampire work
** understand bug reports 12792-12794 and 12907
* Papers to write
* DONE Encodings and transformations (Andrei+Francois)
......@@ -80,6 +85,9 @@
- IDE: not necessary to exit to change the input file: just use "reload"
** as soon as possible: update why3 output of Why2, release Why 2.30
* fix bug 12934 : Coq syntax
https://gforge.inria.fr/tracker/index.php?func=detail&aid=12934&group_id=2990&atid=10293
* increment the magic number in config (A)
* distribute bench files (A + F)
......
......@@ -9,9 +9,24 @@
</proof>
</goal>
<goal name="G2" sum="07e54d9a25fa3174d5d5bf7ce71a13dc" proved="false" expanded="true">
<proof prover="simplify" timelimit="10" edited="" obsolete="true">
<result status="valid" time="0.01"/>
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.01"/>
</proof>
<transf name="split_goal" proved="false" expanded="true">
<goal name="G2.1" sum="f7915ef009bdd949e4af326643583051" proved="false" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.03"/>
</proof>
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.01"/>
</proof>
</goal>
<goal name="G2.2" sum="c53f58872dc3cb71805234ace78f1c2d" proved="true" expanded="true">
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</transf>
</goal>
<goal name="G3" sum="8813554ea4313f64f3efc3330036b5e9" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
......
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