Maj terminée. Pour consulter la release notes associée voici le lien :
https://about.gitlab.com/releases/2021/07/07/critical-security-release-gitlab-14-0-4-released/

Commit 093fbc36 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

more outdated proof session replayed

parent 7cc72e06
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="bts/12475/why3session.xml">
<why3session name="examples/bts/12475/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="spass" name="Spass" version="3.7"/>
<prover id="vampire" name="Vampire" version="0.6"/>
<prover id="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../12475.why" verified="true" expanded="true">
<theory name="Stmt" verified="true" expanded="true">
<goal name="toto" sum="8348f4126989379e5ba647b9d9f0a04d" proved="true" expanded="true">
<goal name="toto" sum="face789c8c32bf3821575b3c51939cd0" proved="true" expanded="true" shape="ainfix <V0ainfix +aroundaUpV0c1.F">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="gappa" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.01"/>
<result status="unknown" time="0.00"/>
</proof>
</goal>
</theory>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/binary_search/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="spass" name="Spass" version="3.7"/>
<prover id="vampire" name="Vampire" version="0.6"/>
<prover id="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../binary_search.mlw" verified="true" expanded="true">
<theory name="WP M" verified="true" expanded="true">
<goal name="WP_parameter binary_search" expl="correctness of parameter binary_search" sum="e076b2dd1e1e2cdff59fe8f2c598efc5" proved="true" expanded="true">
<goal name="WP_parameter binary_search" expl="correctness of parameter binary_search" sum="e9025093975750a5eeb1344fc9d03b19" proved="true" expanded="true" shape="iainfix <=V4V3iainfix <agetV2ainfix +V4adivainfix -V3V4c2V1ainfix <ainfix -V3V5ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V6V3Aainfix <=V5V6Iainfix =agetV2V6V1Iainfix <V6V0Aainfix <=c0V6FAainfix <V3V0Aainfix <=c0V5Iainfix =V5ainfix +ainfix +V4adivainfix -V3V4c2c1Fiainfix >agetV2ainfix +V4adivainfix -V3V4c2V1ainfix <ainfix -V7V4ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V8V7Aainfix <=V4V8Iainfix =agetV2V8V1Iainfix <V8V0Aainfix <=c0V8FAainfix <V7V0Aainfix <=c0V4Iainfix =V7ainfix -ainfix +V4adivainfix -V3V4c2c1Fainfix =agetV2ainfix +V4adivainfix -V3V4c2V1Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <=ainfix +V4adivainfix -V3V4c2V3Aainfix <=V4ainfix +V4adivainfix -V3V4c2ainfix =agetV2V9V1NIainfix <V9V0Aainfix <=c0V9FIainfix <=V10V3Aainfix <=V4V10Iainfix =agetV2V10V1Iainfix <V10V0Aainfix <=c0V10FAainfix <V3V0Aainfix <=c0V4FFAainfix <=V11ainfix -V0c1Aainfix <=c0V11Iainfix =agetV2V11V1Iainfix <V11V0Aainfix <=c0V11FAainfix <ainfix -V0c1V0Aainfix <=c0c0Iainfix <=agetV2V12agetV2V13Iainfix <V13V0Aainfix <=V12V13Aainfix <=c0V12FFFF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</theory>
</file>
......
......@@ -2,57 +2,90 @@
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/bresenham/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="eprover" name="Eprover" version="1.0-004 Temi"/>
<prover id="gappa" name="Gappa" version="0.14.0"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="spass" name="Spass" version="3.5"/>
<prover id="yices" name="Yices" version="1.0.27"/>
<prover id="spass" name="Spass" version="3.7"/>
<prover id="vampire" name="Vampire" version="0.6"/>
<prover id="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../bresenham.mlw" verified="true" expanded="true">
<theory name="WP M" verified="true" expanded="true">
<goal name="invariant_is_ok" sum="a18992b264d84141d8761ca70ad6be8d" proved="true" expanded="true" shape="abestV0V1Iainvariant_V0V1V2F">
<goal name="invariant_is_ok" sum="87247a176582485d3d20264a84801d09" proved="true" expanded="true" shape="abestV0V1Iainvariant_V0V1V2F">
<proof prover="coq" timelimit="10" edited="bresenham_WP_M_invariant_is_ok_1.v" obsolete="false">
<result status="valid" time="1.75"/>
<result status="valid" time="1.23"/>
</proof>
</goal>
<goal name="WP_parameter bresenham" expl="correctness of parameter bresenham" sum="e21d55e7ef3bbb885c18d91e544577f6" proved="true" expanded="true" shape="iainfix <=V2ax2iainfix <V0c0ainfix <ainfix -ainfix +ax2c1V4ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Aainvariant_V4V1V3Aainfix <=V4ainfix +ax2c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2Fainfix <ainfix -ainfix +ax2c1V7ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Aainvariant_V7V5V6Aainfix <=V7ainfix +ax2c1Aainfix <=c0V7Iainfix =V7ainfix +V2c1FIainfix =V6ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V5ainfix +V1c1FAabestV2V1tIainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFFAainvariant_c0c0ainfix -ainfix *c2ay2ax2Aainfix <=c0ainfix +ax2c1Aainfix <=c0c0">
<goal name="WP_parameter bresenham" expl="correctness of parameter bresenham" sum="9eb8c0b7a7b5b8f389c3d8227071b47b" proved="true" expanded="true" shape="iainfix <=V2ax2iainfix <V0c0ainfix <ainfix -ainfix +ax2c1V4ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Aainvariant_V4V1V3Aainfix <=V4ainfix +ax2c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2Fainfix <ainfix -ainfix +ax2c1V7ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Aainvariant_V7V5V6Aainfix <=V7ainfix +ax2c1Aainfix <=c0V7Iainfix =V7ainfix +V2c1FIainfix =V6ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V5ainfix +V1c1FAabestV2V1tIainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFFAainvariant_c0c0ainfix -ainfix *c2ay2ax2Aainfix <=c0ainfix +ax2c1Aainfix <=c0c0">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter bresenham.1" expl="loop invariant init" sum="17124999e917b5c053f6e76b259bcb7c" proved="true" expanded="true" shape="ainvariant_c0c0ainfix -ainfix *c2ay2ax2Aainfix <=c0ainfix +ax2c1Aainfix <=c0c0">
<goal name="WP_parameter bresenham.1" expl="loop invariant init" sum="d74af23f66377fe846029ad998e78c6c" proved="true" expanded="true" shape="ainvariant_c0c0ainfix -ainfix *c2ay2ax2Aainfix <=c0ainfix +ax2c1Aainfix <=c0c0">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter bresenham.2" expl="assertion" sum="6a4211d9f59e4c91dd774b5f26851c4a" proved="true" expanded="true" shape="abestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
<goal name="WP_parameter bresenham.2" expl="assertion" sum="c1a56664066a4030165e2a5c3077267b" proved="true" expanded="true" shape="abestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.16"/>
<result status="valid" time="0.10"/>
</proof>
</goal>
<goal name="WP_parameter bresenham.3" expl="loop invariant preservation" sum="cc7e4371357729bd73f6d31bb228d35e" proved="true" expanded="true" shape="ainvariant_V4V1V3Aainfix <=V4ainfix +ax2c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2FIainfix <V0c0IabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
<goal name="WP_parameter bresenham.3" expl="loop invariant preservation" sum="8d308cad8105399e2924f616643e2e89" proved="true" expanded="true" shape="ainvariant_V4V1V3Aainfix <=V4ainfix +ax2c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2FIainfix <V0c0IabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter bresenham.4" expl="loop variant decreases" sum="38653e4347933a962e5aa5d8faf55aaf" proved="true" expanded="true" shape="ainfix <ainfix -ainfix +ax2c1V4ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Iainvariant_V4V1V3Aainfix <=V4ainfix +ax2c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2FIainfix <V0c0IabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
<goal name="WP_parameter bresenham.4" expl="loop variant decreases" sum="e02880b3f09e515d098e27b3f2643bff" proved="true" expanded="true" shape="ainfix <ainfix -ainfix +ax2c1V4ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Iainvariant_V4V1V3Aainfix <=V4ainfix +ax2c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2FIainfix <V0c0IabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter bresenham.5" expl="loop invariant preservation" sum="694c94aaa6e82005f68c8636fcf6fa15" proved="true" expanded="true" shape="ainvariant_V5V3V4Aainfix <=V5ainfix +ax2c1Aainfix <=c0V5Iainfix =V5ainfix +V2c1FIainfix =V4ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V3ainfix +V1c1FIainfix <V0c0NIabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
<goal name="WP_parameter bresenham.5" expl="loop invariant preservation" sum="519002873ae0e60f95a839d0b74ca095" proved="true" expanded="true" shape="ainvariant_V5V3V4Aainfix <=V5ainfix +ax2c1Aainfix <=c0V5Iainfix =V5ainfix +V2c1FIainfix =V4ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V3ainfix +V1c1FIainfix <V0c0NIabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter bresenham.6" expl="loop variant decreases" sum="169f4e236bbdd35bc03b2b6daf8f3b7f" proved="true" expanded="true" shape="ainfix <ainfix -ainfix +ax2c1V5ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Iainvariant_V5V3V4Aainfix <=V5ainfix +ax2c1Aainfix <=c0V5Iainfix =V5ainfix +V2c1FIainfix =V4ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V3ainfix +V1c1FIainfix <V0c0NIabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
<goal name="WP_parameter bresenham.6" expl="loop variant decreases" sum="d5df027764edf1199402a7c5f84118b7" proved="true" expanded="true" shape="ainfix <ainfix -ainfix +ax2c1V5ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Iainvariant_V5V3V4Aainfix <=V5ainfix +ax2c1Aainfix <=c0V5Iainfix =V5ainfix +V2c1FIainfix =V4ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V3ainfix +V1c1FIainfix <V0c0NIabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter bresenham.7" expl="normal postcondition" sum="bd112799fb9e847a8546c1fac8ba4617" proved="true" expanded="true" shape="tIainfix <=V2ax2NIainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
<goal name="WP_parameter bresenham.7" expl="normal postcondition" sum="8cfb5785a4c9200a53e6dd8a25f8ff56" proved="true" expanded="true" shape="tIainfix <=V2ax2NIainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
</transf>
</goal>
......
......@@ -4,30 +4,41 @@
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="eprover" name="Eprover" version="0.8 Steinthal"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="spass" name="Spass" version="3.7"/>
<prover id="vampire" name="Vampire" version="0.6"/>
<prover id="yices" name="Yices" version="1.0.27"/>
<prover id="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../gcd.mlw" verified="true" expanded="true">
<theory name="WP EuclideanAlgorithm" verified="true" expanded="true">
<goal name="WP_parameter gcd" expl="correctness of parameter gcd" sum="766d5a2cc24a5fd8ece90420c2f75c1f" proved="true" expanded="true" shape="iainfix =V1c0ainfix =V0agcdV0V1ainfix =agcdV1amodV0V1agcdV0V1Aainfix >=amodV0V1c0Aainfix >=V1c0Aainfix <amodV0V1V1Aainfix <=c0V1Iainfix >=V1c0Aainfix >=V0c0FF">
<goal name="WP_parameter gcd" expl="correctness of parameter gcd" sum="ba296793e7239ef781b642b563445c45" proved="true" expanded="true" shape="iainfix =V1c0ainfix =V0agcdV0V1ainfix =agcdV1amodV0V1agcdV0V1Aainfix >=amodV0V1c0Aainfix >=V1c0Aainfix <amodV0V1V1Aainfix <=c0V1Iainfix >=V1c0Aainfix >=V0c0FF">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter gcd.1" expl="normal postcondition" sum="4465e9890b7776b88f461cfd07f6534a" proved="true" expanded="true" shape="ainfix =V0agcdV0V1Iainfix =V1c0Iainfix >=V1c0Aainfix >=V0c0FF">
<goal name="WP_parameter gcd.1" expl="normal postcondition" sum="07b96502c0442e98d6725484d197cc81" proved="true" expanded="true" shape="ainfix =V0agcdV0V1Iainfix =V1c0Iainfix >=V1c0Aainfix >=V0c0FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter gcd.2" expl="precondition" sum="4f12dd81ef67923c17562cf06453d85e" proved="true" expanded="true" shape="ainfix >=amodV0V1c0Aainfix >=V1c0Aainfix <amodV0V1V1Aainfix <=c0V1Iainfix =V1c0NIainfix >=V1c0Aainfix >=V0c0FF">
<goal name="WP_parameter gcd.2" expl="precondition" sum="d2608cdc751cdec6209317d7b3be10f2" proved="true" expanded="true" shape="ainfix >=amodV0V1c0Aainfix >=V1c0Aainfix <amodV0V1V1Aainfix <=c0V1Iainfix =V1c0NIainfix >=V1c0Aainfix >=V0c0FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.06"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter gcd.3" expl="normal postcondition" sum="9d5b42228b6e27b8f3654513a09c01d0" proved="true" expanded="true" shape="ainfix =agcdV1amodV0V1agcdV0V1Iainfix >=amodV0V1c0Aainfix >=V1c0Aainfix <amodV0V1V1Aainfix <=c0V1Iainfix =V1c0NIainfix >=V1c0Aainfix >=V0c0FF">
<goal name="WP_parameter gcd.3" expl="normal postcondition" sum="d131035980e772756a02410f899d17cf" proved="true" expanded="true" shape="ainfix =agcdV1amodV0V1agcdV0V1Iainfix >=amodV0V1c0Aainfix >=V1c0Aainfix <amodV0V1V1Aainfix <=c0V1Iainfix =V1c0NIainfix >=V1c0Aainfix >=V0c0FF">
<proof prover="coq" timelimit="10" edited="gcd_WP_EuclideanAlgorithm_WP_parameter_gcd_1.v" obsolete="false">
<result status="valid" time="0.62"/>
<result status="valid" time="0.55"/>
</proof>
</goal>
</transf>
......
......@@ -4,75 +4,74 @@
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="eprover" name="Eprover" version="0.8 Steinthal"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="spass" name="Spass" version="3.7"/>
<prover id="vampire" name="Vampire" version="0.6"/>
<prover id="yices" name="Yices" version="1.0.27"/>
<prover id="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../gcd_bezout.mlw" verified="true" expanded="true">
<theory name="WP GcdBezout" verified="true" expanded="true">
<goal name="WP_parameter gcd" expl="correctness of parameter gcd" sum="e708de1061369396b2ff1f4113f30e00" proved="true" expanded="true" shape="iainfix >V6c0ainfix <V9V6Aainfix <=c0V6Aainfix =ainfix +ainfix *V12V0ainfix *V13V1V9Aainfix =ainfix +ainfix *V10V0ainfix *V11V1V8Aainfix =agcdV8V9agcdV0V1Aainfix >=V9c0Aainfix >=V8c0Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6Fainfix =ainfix +ainfix *V14V0ainfix *V15V1V7EAainfix =V7agcdV0V1Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFAainfix =ainfix +ainfix *c0V0ainfix *c1V1V1Aainfix =ainfix +ainfix *c1V0ainfix *c0V1V0Aainfix =agcdV0V1agcdV0V1Aainfix >=V1c0Aainfix >=V0c0Iainfix >=V1c0Aainfix >=V0c0FF">
<goal name="WP_parameter gcd" expl="correctness of parameter gcd" sum="c568c661e74cf5b450ed7146c0d40241" proved="true" expanded="true" shape="iainfix >V6c0ainfix <V9V6Aainfix <=c0V6Aainfix =ainfix +ainfix *V12V0ainfix *V13V1V9Aainfix =ainfix +ainfix *V10V0ainfix *V11V1V8Aainfix =agcdV8V9agcdV0V1Aainfix >=V9c0Aainfix >=V8c0Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6Fainfix =ainfix +ainfix *V14V0ainfix *V15V1V7EAainfix =V7agcdV0V1Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFAainfix =ainfix +ainfix *c0V0ainfix *c1V1V1Aainfix =ainfix +ainfix *c1V0ainfix *c0V1V0Aainfix =agcdV0V1agcdV0V1Aainfix >=V1c0Aainfix >=V0c0Iainfix >=V1c0Aainfix >=V0c0FF">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter gcd.1" expl="loop invariant init" sum="44ff89a72fcf725343c0157cb7a7faf8" proved="true" expanded="true" shape="ainfix =ainfix +ainfix *c0V0ainfix *c1V1V1Aainfix =ainfix +ainfix *c1V0ainfix *c0V1V0Aainfix =agcdV0V1agcdV0V1Aainfix >=V1c0Aainfix >=V0c0Iainfix >=V1c0Aainfix >=V0c0FF">
<goal name="WP_parameter gcd.1" expl="loop invariant init" sum="df664bad8ad295c519a647357f650a65" proved="true" expanded="true" shape="ainfix =ainfix +ainfix *c0V0ainfix *c1V1V1Aainfix =ainfix +ainfix *c1V0ainfix *c0V1V0Aainfix =agcdV0V1agcdV0V1Aainfix >=V1c0Aainfix >=V0c0Iainfix >=V1c0Aainfix >=V0c0FF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter gcd.2" expl="loop invariant preservation" sum="838c6f08305500896b8e79edc0ff580f" proved="true" expanded="true" shape="ainfix =ainfix +ainfix *V12V0ainfix *V13V1V9Aainfix =ainfix +ainfix *V10V0ainfix *V11V1V8Aainfix =agcdV8V9agcdV0V1Aainfix >=V9c0Aainfix >=V8c0Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix >V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
<goal name="WP_parameter gcd.2" expl="loop invariant preservation" sum="2ec16c3cee7a09b6ada3e3d0d1cffdd8" proved="true" expanded="true" shape="ainfix =ainfix +ainfix *V12V0ainfix *V13V1V9Aainfix =ainfix +ainfix *V10V0ainfix *V11V1V8Aainfix =agcdV8V9agcdV0V1Aainfix >=V9c0Aainfix >=V8c0Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix >V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter gcd.2.1" expl="correctness of parameter gcd" sum="b046d3dcd5fbba79c535695efd558e94" proved="true" expanded="true" shape="ainfix >=V8c0Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix >V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
<goal name="WP_parameter gcd.2.1" expl="correctness of parameter gcd" sum="515d36058986d6992cf777b083163e53" proved="true" expanded="true" shape="ainfix >=V8c0Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix >V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter gcd.2.2" expl="correctness of parameter gcd" sum="080da6996a2bd84d0819ab2c8db3ce4e" proved="true" expanded="true" shape="ainfix >=V9c0Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix >V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
<goal name="WP_parameter gcd.2.2" expl="correctness of parameter gcd" sum="619daf7d40e4812d1142d21500ef7d87" proved="true" expanded="true" shape="ainfix >=V9c0Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix >V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.07"/>
<result status="valid" time="0.06"/>
</proof>
</goal>
<goal name="WP_parameter gcd.2.3" expl="correctness of parameter gcd" sum="6e974266fad2cd4dc4e4778c9da314d4" proved="true" expanded="true" shape="ainfix =agcdV8V9agcdV0V1Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix >V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
<goal name="WP_parameter gcd.2.3" expl="correctness of parameter gcd" sum="f95d54635cdfc2b2c1120f17c71086db" proved="true" expanded="true" shape="ainfix =agcdV8V9agcdV0V1Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix >V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
<proof prover="coq" timelimit="10" edited="gcd_bezout_WP_GcdBezout_WP_parameter_gcd_1.v" obsolete="false">
<result status="valid" time="0.70"/>
<result status="valid" time="0.59"/>
</proof>
</goal>
<goal name="WP_parameter gcd.2.4" expl="correctness of parameter gcd" sum="bb890d60feb115367a6f034ea18e068e" proved="true" expanded="true" shape="ainfix =ainfix +ainfix *V10V0ainfix *V11V1V8Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix >V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
<goal name="WP_parameter gcd.2.4" expl="correctness of parameter gcd" sum="fda1c46be9dc0cdf2593f6343ba59053" proved="true" expanded="true" shape="ainfix =ainfix +ainfix *V10V0ainfix *V11V1V8Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix >V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter gcd.2.5" expl="correctness of parameter gcd" sum="af06cf21d1578e0cf266716c7f811f36" proved="true" expanded="true" shape="ainfix =ainfix +ainfix *V12V0ainfix *V13V1V9Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix >V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
<goal name="WP_parameter gcd.2.5" expl="correctness of parameter gcd" sum="4938f5242aeab747ed31c5af62416566" proved="true" expanded="true" shape="ainfix =ainfix +ainfix *V12V0ainfix *V13V1V9Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix >V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter gcd.3" expl="loop variant decreases" sum="d4abfa67a7bde89abc856c1564c1aa3d" proved="true" expanded="true" shape="ainfix <V9V6Aainfix <=c0V6Iainfix =ainfix +ainfix *V12V0ainfix *V13V1V9Aainfix =ainfix +ainfix *V10V0ainfix *V11V1V8Aainfix =agcdV8V9agcdV0V1Aainfix >=V9c0Aainfix >=V8c0Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix >V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
<goal name="WP_parameter gcd.3" expl="loop variant decreases" sum="9a3f46c91bdbb24316eca24646cbaed6" proved="true" expanded="true" shape="ainfix <V9V6Aainfix <=c0V6Iainfix =ainfix +ainfix *V12V0ainfix *V13V1V9Aainfix =ainfix +ainfix *V10V0ainfix *V11V1V8Aainfix =agcdV8V9agcdV0V1Aainfix >=V9c0Aainfix >=V8c0Iainfix =V13ainfix -V4ainfix *V2adivV7V6FIainfix =V12ainfix -V5ainfix *V3adivV7V6FIainfix =V11V2FIainfix =V10V3FIainfix =V9amodV7V6FIainfix =V8V6FIainfix >V6c0Iainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.10"/>
</proof>
</goal>
<goal name="WP_parameter gcd.4" expl="normal postcondition" sum="f519c8644e350bf6b4879e17ab8d1f45" proved="true" expanded="true" shape="ainfix =ainfix +ainfix *V8V0ainfix *V9V1V7EAainfix =V7agcdV0V1Iainfix >V6c0NIainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
<goal name="WP_parameter gcd.4" expl="normal postcondition" sum="f5510b8bdbc630f3046364828fe5522b" proved="true" expanded="true" shape="ainfix =ainfix +ainfix *V8V0ainfix *V9V1V7EAainfix =V7agcdV0V1Iainfix >V6c0NIainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter gcd.4.1" expl="correctness of parameter gcd" sum="bb06bfcff41f64c10ab670f8e609fa11" proved="true" expanded="true" shape="ainfix =V7agcdV0V1Iainfix >V6c0NIainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
<goal name="WP_parameter gcd.4.1" expl="correctness of parameter gcd" sum="a09654eb267143ce3a30ce4412ba56ac" proved="true" expanded="true" shape="ainfix =V7agcdV0V1Iainfix >V6c0NIainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter gcd.4.2" expl="correctness of parameter gcd" sum="e7a614e3d26579b68ee56a56869bee59" proved="true" expanded="true" shape="ainfix =ainfix +ainfix *V8V0ainfix *V9V1V7EIainfix >V6c0NIainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
<goal name="WP_parameter gcd.4.2" expl="correctness of parameter gcd" sum="cb71793a4246a150f974e8e06b0f4d9f" proved="true" expanded="true" shape="ainfix =ainfix +ainfix *V8V0ainfix *V9V1V7EIainfix >V6c0NIainfix =ainfix +ainfix *V3V0ainfix *V2V1V6Aainfix =ainfix +ainfix *V5V0ainfix *V4V1V7Aainfix =agcdV7V6agcdV0V1Aainfix >=V6c0Aainfix >=V7c0FFFFFFIainfix >=V1c0Aainfix >=V0c0FF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.04"/>
</proof>
</goal>
</transf>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/isqrt/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="spass" name="Spass" version="3.7"/>
<prover id="vampire" name="Vampire" version="0.6"/>
<prover id="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../isqrt.mlw" verified="true" expanded="true">
<theory name="WP Simple" verified="true" expanded="true">
<goal name="WP_parameter isqrt" expl="correctness of parameter isqrt" sum="71cc23114951a4ecb6b4f3257d65e891" proved="true" expanded="true">
<goal name="WP_parameter isqrt" expl="correctness of parameter isqrt" sum="71cc23114951a4ecb6b4f3257d65e891" proved="true" expanded="false" shape="iainfix <=V1V0ainfix <ainfix -V0V3ainfix -V0V2Aainfix <=c0ainfix -V0V2Aainfix =V4asqrainfix +V3c1Aainfix >=V0asqrV3Aainfix >=V3c0Iainfix =V4ainfix +ainfix +V1ainfix *c2V3c1FIainfix =V3ainfix +V2c1Fainfix <V0asqrainfix +V2c1Aainfix <=asqrV2V0Aainfix >=V2c0Iainfix =V1asqrainfix +V2c1Aainfix >=V0asqrV2Aainfix >=V2c0FFAainfix =c1asqrainfix +c0c1Aainfix >=V0asqrc0Aainfix >=c0c0Iainfix >=V0c0F">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
......@@ -11,65 +20,155 @@
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter main" expl="correctness of parameter main" sum="1c68d9c3079316cc99cf2e1bf49cbce6" proved="true" expanded="true">
<goal name="WP_parameter main" expl="correctness of parameter main" sum="1c68d9c3079316cc99cf2e1bf49cbce6" proved="true" expanded="false" shape="ainfix =V0c4Iainfix <c17asqrainfix +V0c1Aainfix <=asqrV0c17Aainfix >=V0c0FAainfix >=c17c0">
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
<theory name="WP NewtonMethod" verified="true" expanded="true">
<goal name="WP_parameter sqrt" expl="correctness of parameter sqrt" sum="60eaaec813247c8c0f5a815d8255a1ad" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter sqrt.1" expl="normal postcondition" sum="bb87fe0b8434e8d093943f1210b71ec5" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<goal name="WP_parameter sqrt" expl="correctness of parameter sqrt" sum="e4337b042ceaf0bc1e59f1413875d24d" proved="true" expanded="false" shape="iainfix =V0c0ainfix <V0ainfix *ainfix +c0c1ainfix +c0c1Aainfix <=ainfix *c0c0V0iainfix <=V0c3ainfix <V0ainfix *ainfix +c1c1ainfix +c1c1Aainfix <=ainfix *c1c1V0iainfix <V1V2ainfix <V3V2Aainfix <=c0V2Aainfix <V0ainfix *ainfix +V4c1ainfix +V4c1Aainfix <V0ainfix *ainfix +V3c1ainfix +V3c1Aainfix =V4adivainfix +adivV0V3V3c2Aainfix >V3c0Aainfix >V4c0Iainfix =V4adivainfix +adivV0V1V1c2FIainfix =V3V1Fainfix <V0ainfix *ainfix +V2c1ainfix +V2c1Aainfix <=ainfix *V2V2V0Iainfix <V0ainfix *ainfix +V1c1ainfix +V1c1Aainfix <V0ainfix *ainfix +V2c1ainfix +V2c1Aainfix =V1adivainfix +adivV0V2V2c2Aainfix >V2c0Aainfix >V1c0FFAainfix <V0ainfix *ainfix +adivainfix +V0c1c2c1ainfix +adivainfix +V0c1c2c1Aainfix <V0ainfix *ainfix +V0c1ainfix +V0c1Aainfix =adivainfix +V0c1c2adivainfix +adivV0V0V0c2Aainfix >V0c0Aainfix >adivainfix +V0c1c2c0Iainfix >=V0c0F">
<transf name="split_goal" proved="true" expanded="false">
<goal name="WP_parameter sqrt.1" expl="normal postcondition" sum="70dbb7b3b334de43dee419a62bb173e6" proved="true" expanded="false" shape="ainfix <V0ainfix *ainfix +c0c1ainfix +c0c1Aainfix <=ainfix *c0c0V0Iainfix =V0c0Iainfix >=V0c0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="WP_parameter sqrt.2" expl="normal postcondition" sum="84710358cd8ada1454c80929dd0b421a" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter sqrt.2" expl="normal postcondition" sum="d9b3abfe5e2bb93ecc780e0aba0b37e3" proved="true" expanded="false" shape="ainfix <V0ainfix *ainfix +c1c1ainfix +c1c1Aainfix <=ainfix *c1c1V0Iainfix <=V0c3Iainfix =V0c0NIainfix >=V0c0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="WP_parameter sqrt.3" expl="loop invariant init" sum="c11b288394dbf06ca63d6f183eed8902" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter sqrt.3.1" expl="correctness of parameter sqrt" sum="e2c9e9d55c1fb96ff6927b0bf7ea08c3" proved="true" expanded="true">
<goal name="WP_parameter sqrt.3" expl="loop invariant init" sum="5c88829f3f9df68225c2aff6f9084aa0" proved="true" expanded="false" shape="ainfix <V0ainfix *ainfix +adivainfix +V0c1c2c1ainfix +adivainfix +V0c1c2c1Aainfix <V0ainfix *ainfix +V0c1ainfix +V0c1Aainfix =adivainfix +V0c1c2adivainfix +adivV0V0V0c2Aainfix >V0c0Aainfix >adivainfix +V0c1c2c0Iainfix <=V0c3NIainfix =V0c0NIainfix >=V0c0F">
<transf name="split_goal" proved="true" expanded="false">
<goal name="WP_parameter sqrt.3.1" expl="correctness of parameter sqrt" sum="7be6c881690801aea0c8a90f85e30983" proved="true" expanded="false" shape="ainfix >adivainfix +V0c1c2c0Iainfix <=V0c3NIainfix =V0c0NIainfix >=V0c0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter sqrt.3.2" expl="correctness of parameter sqrt" sum="89a7b5a1daf6b4e2519b771a686341ed" proved="true" expanded="true">
<goal name="WP_parameter sqrt.3.2" expl="correctness of parameter sqrt" sum="d6c33551a632859686af3254b27ed285" proved="true" expanded="false" shape="ainfix >V0c0Iainfix <=V0c3NIainfix =V0c0NIainfix >=V0c0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter sqrt.3.3" expl="correctness of parameter sqrt" sum="1e7292150fa5b3ff64df1f967aa339dd" proved="true" expanded="true">
<goal name="WP_parameter sqrt.3.3" expl="correctness of parameter sqrt" sum="7d21ad8d99510a2fcc20f12a93e29fda" proved="true" expanded="false" shape="ainfix =adivainfix +V0c1c2adivainfix +adivV0V0V0c2Iainfix <=V0c3NIainfix =V0c0NIainfix >=V0c0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.34"/>
<result status="valid" time="0.36"/>
</proof>
</goal>
<goal name="WP_parameter sqrt.3.4" expl="correctness of parameter sqrt" sum="7c4b5c925e20094d1a40d385f8888899" proved="true" expanded="true">
<goal name="WP_parameter sqrt.3.4" expl="correctness of parameter sqrt" sum="8b4b2a8ae34c2810e71cdf563c51e310" proved="true" expanded="false" shape="ainfix <V0ainfix *ainfix +V0c1ainfix +V0c1Iainfix <=V0c3NIainfix =V0c0NIainfix >=V0c0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter sqrt.3.5" expl="correctness of parameter sqrt" sum="6ecbaf6ffa704b33dd36c7a1db072d41" proved="true" expanded="true">
<goal name="WP_parameter sqrt.3.5" expl="correctness of parameter sqrt" sum="a252fd5201309879eddd94a6734ab199" proved="true" expanded="false" shape="ainfix <V0ainfix *ainfix +adivainfix +V0c1c2c1ainfix +adivainfix +V0c1c2c1Iainfix <=V0c3NIainfix =V0c0NIainfix >=V0c0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter sqrt.4" expl="loop invariant preservation" sum="0eea8d02017090f9f5ffcb5b933c5c05" proved="true" expanded="false" shape="ainfix <V0ainfix *ainfix +V4c1ainfix +V4c1Aainfix <V0ainfix *ainfix +V3c1ainfix +V3c1Aainfix =V4adivainfix +adivV0V3V3c2Aainfix >V3c0Aainfix >V4c0Iainfix =V4adivainfix +adivV0V1V1c2FIainfix =V3V1FIainfix <V1V2Iainfix <V0ainfix *ainfix +V1c1ainfix +V1c1Aainfix <V0ainfix *ainfix +V2c1ainfix +V2c1Aainfix =V1adivainfix +adivV0V2V2c2Aainfix >V2c0Aainfix >V1c0FFIainfix <=V0c3NIainfix =V0c0NIainfix >=V0c0F">
<transf name="split_goal" proved="true" expanded="false">
<goal name="WP_parameter sqrt.4.1" expl="correctness of parameter sqrt" sum="3846fb7d32e335936ddcce01a4a8d8d1" proved="true" expanded="false" shape="ainfix >V4c0Iainfix =V4adivainfix +adivV0V1V1c2FIainfix =V3V1FIainfix <V1V2Iainfix <V0ainfix *ainfix +V1c1ainfix +V1c1Aainfix <V0ainfix *ainfix +V2c1ainfix +V2c1Aainfix =V1adivainfix +adivV0V2V2c2Aainfix >V2c0Aainfix >V1c0FFIainfix <=V0c3NIainfix =V0c0NIainfix >=V0c0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.06"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="1.65"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter sqrt.4.2" expl="correctness of parameter sqrt" sum="43b2de60e3bc0718779234af61188289" proved="true" expanded="false" shape="ainfix >V3c0Iainfix =V4adivainfix +adivV0V1V1c2FIainfix =V3V1FIainfix <V1V2Iainfix <V0ainfix *ainfix +V1c1ainfix +V1c1Aainfix <V0ainfix *ainfix +V2c1ainfix +V2c1Aainfix =V1adivainfix +adivV0V2V2c2Aainfix >V2c0Aainfix >V1c0FFIainfix <=V0c3NIainfix =V0c0NIainfix >=V0c0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter sqrt.4.3" expl="correctness of parameter sqrt" sum="3cca372df69b81be089cb0c501eda5fd" proved="true" expanded="false" shape="ainfix =V4adivainfix +adivV0V3V3c2Iainfix =V4adivainfix +adivV0V1V1c2FIainfix =V3V1FIainfix <V1V2Iainfix <V0ainfix *ainfix +V1c1ainfix +V1c1Aainfix <V0ainfix *ainfix +V2c1ainfix +V2c1Aainfix =V1adivainfix +adivV0V2V2c2Aainfix >V2c0Aainfix >V1c0FFIainfix <=V0c3NIainfix =V0c0NIainfix >=V0c0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter sqrt.4.4" expl="correctness of parameter sqrt" sum="98feb6dcff36c91c157f650f202a8fc0" proved="true" expanded="false" shape="ainfix <V0ainfix *ainfix +V3c1ainfix +V3c1Iainfix =V4adivainfix +adivV0V1V1c2FIainfix =V3V1FIainfix <V1V2Iainfix <V0ainfix *ainfix +V1c1ainfix +V1c1Aainfix <V0ainfix *ainfix +V2c1ainfix +V2c1Aainfix =V1adivainfix +adivV0V2V2c2Aainfix >V2c0Aainfix >V1c0FFIainfix <=V0c3NIainfix =V0c0NIainfix >=V0c0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter sqrt.4.5" expl="correctness of parameter sqrt" sum="250a938d7ab7e781f7b8a0db605c5175" proved="true" expanded="false" shape="ainfix <V0ainfix *ainfix +V4c1ainfix +V4c1Iainfix =V4adivainfix +adivV0V1V1c2FIainfix =V3V1FIainfix <V1V2Iainfix <V0ainfix *ainfix +V1c1ainfix +V1c1Aainfix <V0ainfix *ainfix +V2c1ainfix +V2c1Aainfix =V1adivainfix +adivV0V2V2c2Aainfix >V2c0Aainfix >V1c0FFIainfix <=V0c3NIainfix =V0c0NIainfix >=V0c0F">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="2.23"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter sqrt.4" expl="loop invariant preservation" sum="635d4755b940a642f5f361e72d63b2ad" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="9.22"/>
<goal name="WP_parameter sqrt.5" expl="loop variant decreases" sum="7c3f10e9b4a4be20d6a2dbb810ddfd31" proved="true" expanded="false" shape="ainfix <V3V2Aainfix <=c0V2Iainfix <V0ainfix *ainfix +V4c1ainfix +V4c1Aainfix <V0ainfix *ainfix +V3c1ainfix +V3c1Aainfix =V4adivainfix +adivV0V3V3c2Aainfix >V3c0Aainfix >V4c0Iainfix =V4adivainfix +adivV0V1V1c2FIainfix =V3V1FIainfix <V1V2Iainfix <V0ainfix *ainfix +V1c1ainfix +V1c1Aainfix <V0ainfix *ainfix +V2c1ainfix +V2c1Aainfix =V1adivainfix +adivV0V2V2c2Aainfix >V2c0Aainfix >V1c0FFIainfix <=V0c3NIainfix =V0c0NIainfix >=V0c0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter sqrt.5" expl="loop variant decreases" sum="0e4fa9a7a38870c021afae8a4e42ba92" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter sqrt.6" expl="normal postcondition" sum="ee09cf3d584c24c45c524135e3d35bf3" proved="true" expanded="true">
<goal name="WP_parameter sqrt.6" expl="normal postcondition" sum="4f8c8a727070a34f014d169e61807c6d" proved="true" expanded="false" shape="ainfix <V0ainfix *ainfix +V2c1ainfix +V2c1Aainfix <=ainfix *V2V2V0Iainfix <V1V2NIainfix <V0ainfix *ainfix +V1c1ainfix +V1c1Aainfix <V0ainfix *ainfix +V2c1ainfix +V2c1Aainfix =V1adivainfix +adivV0V2V2c2Aainfix >V2c0Aainfix >V1c0FFIainfix <=V0c3NIainfix =V0c0NIainfix >=V0c0F">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.18"/>
</proof>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/list_rev/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="spass" name="Spass" version="3.7"/>
<prover id="vampire" name="Vampire" version="0.6"/>
<prover id="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../list_rev.mlw" verified="false" expanded="true">
<theory name="WP M" verified="false" expanded="true">
<goal name="acyclic_list" sum="7db83a937373a8239579a364820ee4d2" proved="false" expanded="true">
<goal name="acyclic_list" sum="7db83a937373a8239579a364820ee4d2" proved="false" expanded="true" shape="asep_node_listV0V1amixfix []V0V1Iais_listV0V1Iainfix =V1anullNF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="3.38"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.06"/>
</proof>
</goal>
<goal name="consistent" sum="590df07cf83264b32e414a773bbd0a39" proved="false" expanded="true">
<goal name="consistent" sum="590df07cf83264b32e414a773bbd0a39" proved="false" expanded="true" shape="fIais_listV0V2Iais_listV0V1F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.18"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.04"