Commit 98680125 authored by François Bobot's avatar François Bobot

list_rev in regression tests

parent 5d98856f
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/list_rev/why3session.xml">
<file name="../list_rev.mlw" verified="false" expanded="true">
<theory name="M" verified="false" expanded="true">
<goal name="acyclic_list" sum="14b23a72bdf3ddafa531460f9838d56d" proved="false" expanded="true">
</goal>
<goal name="consistent" sum="373d5b25560c53e2797b67419b7ff691" proved="false" expanded="true">
</goal>
<goal name="WP_parameter list_rev" expl="correctness of parameter list_rev" sum="b33dc5e7178219ce350fce83005647ef" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.14"/>
</proof>
</goal>
<goal name="reverse_append" sum="1533f78841b3afe619b329869e8d0af6" proved="false" expanded="true">
</goal>
<goal name="WP_parameter list_rev_behv" expl="correctness of parameter list_rev_behv" sum="e19607dfb73eba248a0c06d25548625d" proved="false" expanded="true">
</goal>
</theory>
<theory name="M2" verified="false" expanded="true">
<goal name="frame_list" sum="6832b0f09ea49b1a68df28ae5d8cc5ba" proved="true" expanded="true">
<proof prover="coq" timelimit="10" edited="list_rev.mlw_M2_frame_list_1.v" obsolete="false">
<result status="valid" time="0.72"/>
</proof>
</goal>
<goal name="frame_list_ft" sum="60296b3f03b1fc700582f4a9e9d6b98b" proved="true" expanded="true">
<proof prover="coq" timelimit="10" edited="list_rev.mlw_M2_frame_list_ft_1.v" obsolete="false">
<result status="valid" time="0.74"/>
</proof>
</goal>
<goal name="acyclic_list" sum="c621805c935ee753897c237a73f10bad" proved="false" expanded="true">
</goal>
<goal name="consistent" sum="08a4374f096f4d7cd99f4f52fc96b3f7" proved="false" expanded="true">
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.04"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.25"/>
</proof>
</goal>
<goal name="WP_parameter list_rev" expl="correctness of parameter list_rev" sum="b0d03c98bb5c3e11156af8522cbb9b03" proved="true" expanded="true">
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="frame_model" sum="9953603df5d42e7cae815cbc5613db81" proved="true" expanded="true">
<proof prover="coq" timelimit="10" edited="list_rev.mlw_M2_frame_model_1.v" obsolete="false">
<result status="valid" time="0.75"/>
</proof>
</goal>
<goal name="consistent_behv" sum="67bef8b4f715a36d1daec8ca46e4d812" proved="false" expanded="true">
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.84"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.56"/>
</proof>
</goal>
<goal name="WP_parameter list_rev_behv" expl="correctness of parameter list_rev_behv" sum="3177c7272f5a46808daf16bb3365415c" proved="true" expanded="true">
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.20"/>
</proof>
</goal>
</theory>
</file>
</why3session>
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