Commit 32de13fa authored by MARCHE Claude's avatar MARCHE Claude

update sessions

parent ed2d24e0
This diff is collapsed.
This diff is collapsed.
......@@ -4,79 +4,71 @@
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../logic.mlw">
<theory name="Compiler_logic" sum="597c541efd25a851253c429676f44981">
<goal name="VC hl" expl="VC for hl">
<prover id="2" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../logic.mlw" proved="true">
<theory name="Compiler_logic" proved="true" sum="cf4c1068c97dbed0498a4f106d4e05b1">
<goal name="VC hl" expl="VC for hl" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC wp" expl="VC for wp">
<goal name="VC wp" expl="VC for wp" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="seq_wp_lemma" expl="">
<goal name="seq_wp_lemma" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
<goal name="VC infix --" expl="VC for infix --">
<transf name="split_goal_wp">
<goal name="VC infix --.1" expl="precondition">
<goal name="VC infix --" expl="VC for infix --" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC infix --.0" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="69"/></proof>
</goal>
<goal name="VC infix --.2" expl="assertion">
<goal name="VC infix --.1" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.05" steps="15"/></proof>
</goal>
<goal name="VC infix --.3" expl="postcondition">
<goal name="VC infix --.2" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="VC infix --.4" expl="postcondition">
<goal name="VC infix --.3" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.03" steps="8"/></proof>
</goal>
</transf>
</goal>
<goal name="fork_wp_lemma" expl="">
<goal name="fork_wp_lemma" proved="true">
<proof prover="1"><result status="valid" time="0.03" steps="15"/></proof>
</goal>
<goal name="VC infix %" expl="VC for infix %">
<goal name="VC infix %" expl="VC for infix %" proved="true">
<proof prover="0"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="towp_wp_lemma" expl="">
<goal name="towp_wp_lemma" proved="true">
<proof prover="1"><result status="valid" time="0.04" steps="13"/></proof>
</goal>
<goal name="VC prefix $" expl="VC for prefix $">
<goal name="VC prefix $" expl="VC for prefix $" proved="true">
<proof prover="1"><result status="valid" time="0.05" steps="17"/></proof>
</goal>
<goal name="VC hoare" expl="VC for hoare">
<goal name="VC hoare" expl="VC for hoare" proved="true">
<proof prover="0"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="pconj_lemma" expl="">
<goal name="pconj_lemma" proved="true">
<proof prover="1"><result status="valid" time="0.03" steps="8"/></proof>
</goal>
<goal name="loop_wp_lemma" expl="">
<goal name="loop_wp_lemma" proved="true">
<proof prover="1"><result status="valid" time="0.04" steps="49"/></proof>
</goal>
<goal name="VC make_loop" expl="VC for make_loop">
<transf name="split_goal_wp">
<goal name="VC make_loop.1" expl="assertion">
<transf name="split_goal_wp">
<goal name="VC make_loop.1.1" expl="assertion">
<transf name="induction_pr">
<goal name="VC make_loop.1.1.1" expl="assertion">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="VC make_loop.1.1.1.1" expl="VC for make_loop">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
</transf>
<goal name="VC make_loop" expl="VC for make_loop" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC make_loop.0" expl="assertion" proved="true">
<transf name="induction_pr" proved="true" >
<goal name="VC make_loop.0.0" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.26"/></proof>
</goal>
</transf>
</goal>
<goal name="VC make_loop.2" expl="precondition">
<goal name="VC make_loop.1" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="VC make_loop.3" expl="postcondition">
<goal name="VC make_loop.2" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.05" steps="7"/></proof>
</goal>
<goal name="VC make_loop.4" expl="postcondition">
<goal name="VC make_loop.3" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
</transf>
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
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