Commit 61e9958d authored by MARCHE Claude's avatar MARCHE Claude

Replayable proof session for hello_proof stored under git

parent c3593b6d
......@@ -147,7 +147,6 @@ why.conf
# /examples/
/examples/my_cosine/
/examples/scottish-private-club/
/examples/hello_proof/
/examples/einstein/
/examples/genealogy/
/examples/programs/isqrt/
......
......@@ -2,7 +2,7 @@ theory HelloProof "My very first Why3 theory"
goal G1 : true
goal G2 : (false -> false) and (true or false)
goal G2 : (true -> false) and (true or false)
use import int.Int
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/hello_proof/why3session.xml">
<file name="../hello_proof.why" verified="false" expanded="true">
<theory name="HelloProof" verified="false" expanded="true">
<goal name="G1" sum="f81584706e28397114f2508adf6dd2ff" proved="true" expanded="true">
<proof prover="simplify" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="G2" sum="0bb17dc8e6f26a1a6aaf5ecf8ed5a5a8" proved="false" expanded="true">
<proof prover="alt-ergo" edited="" obsolete="false">
<result status="unknown" time="0.02"/>
</proof>
<proof prover="simplify" edited="" obsolete="false">
<result status="unknown" time="0.01"/>
</proof>
<transf name="split_goal" proved="false" expanded="true">
<goal name="G2.1" sum="54b5fc27ec93fbe413651f6064794e54" proved="false" expanded="true">
<proof prover="coq" edited="" obsolete="false">
<result status="unknown" time="0.46"/>
</proof>
<proof prover="alt-ergo" edited="" obsolete="false">
<result status="unknown" time="0.02"/>
</proof>
<proof prover="simplify" edited="" obsolete="false">
<result status="unknown" time="0.01"/>
</proof>
</goal>
<goal name="G2.2" sum="6cdd03a110385f45423b1683748dce81" proved="true" expanded="true">
<proof prover="simplify" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</transf>
</goal>
<goal name="G3" sum="b3b51b7bb0acfa332bfb937bfa017230" proved="true" expanded="true">
<proof prover="alt-ergo" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="simplify" edited="" obsolete="false">
<result status="unknown" time="0.01"/>
</proof>
</goal>
</theory>
</file>
</why3session>
......@@ -986,10 +986,12 @@ let load_result r =
try float_of_string (List.assoc "time" r.Xml.attributes)
with Not_found -> 0.0
in
{ Call_provers.pr_answer = answer;
Done {
Call_provers.pr_answer = answer;
Call_provers.pr_time = time;
Call_provers.pr_output = "";
}
| "undone" -> Undone
| s ->
eprintf "Session.load_result: unexpected element '%s'@." s;
assert false
......@@ -1032,7 +1034,7 @@ and load_proof_or_transf ~env ~provers mg a =
with Not_found -> assert false (* TODO *)
in
let res = match a.Xml.elements with
| [r] -> Done (load_result r)
| [r] -> load_result r
| [] -> Undone
| _ -> assert false
in
......
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