Commit 1e402289 authored by Andrei Paskevich's avatar Andrei Paskevich

fix session file for programs/zeros.mlw

parent 58d20088
......@@ -3,46 +3,46 @@
<why3session name="examples/programs/zeros/why3session.xml">
<file name="../zeros.mlw" verified="true" expanded="true">
<theory name="SetZeros" verified="true" expanded="true">
<goal name="WP_parameter set_zeros" expl="correctness of parameter set_zeros" sum="61eb8ab27b075cc9f9557662701deb9a" proved="true" expanded="true">
<goal name="WP_parameter set_zeros" expl="correctness of parameter set_zeros" sum="073f2175118a01f71b9d611d5b46b881" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter set_zeros.1" expl="normal postcondition" sum="9934ac330413647e3ce065099e571460" proved="true" expanded="true">
<goal name="WP_parameter set_zeros.1" expl="normal postcondition" sum="8f2cf2592df2b5cf5827ca059b2c741c" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter set_zeros.2" expl="for loop initialization" sum="c54bdc4d37361cc9832d507f67389c90" proved="true" expanded="true">
<goal name="WP_parameter set_zeros.2" expl="for loop initialization" sum="21624731d70695d4156acede0eeffffd" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter set_zeros.3" expl="for loop preservation" sum="ab559f2cafe67190b6b0fdc52183acf0" proved="true" expanded="true">
<goal name="WP_parameter set_zeros.3" expl="for loop preservation" sum="a10e5df95a810ea60757bc69e3dfd9ac" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="zeros.mlw-SetZeros-WP_parameter set_zeros_1.why" obsolete="false">
<result status="unknown" time="0.02"/>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter set_zeros.4" expl="normal postcondition" sum="27a169d744fee28adaefe96cd86be7b4" proved="true" expanded="true">
<goal name="WP_parameter set_zeros.4" expl="normal postcondition" sum="92b3401acb16489815b172129c602e30" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter harness" expl="correctness of parameter harness" sum="71fe54e578e1a17eae1ad025f530eda9" proved="true" expanded="true">
<goal name="WP_parameter harness" expl="correctness of parameter harness" sum="86e3646719139ac2c16631cbce764b98" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter harness.1" expl="assertion" sum="93146ed254dd825c0ac00dbb2643b96d" proved="true" expanded="true">
<goal name="WP_parameter harness.1" expl="assertion" sum="d460e49ab087d3163f7b52c04785c0ce" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter harness.2" expl="assertion" sum="8369f550814b2c44e0725ba455737dd4" proved="true" expanded="true">
<goal name="WP_parameter harness.2" expl="assertion" sum="7684b00aabb5af1e63994f0c261eadd6" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
</transf>
......
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