ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity

updated sessions after change of shape computation

Browse Source
This commit is contained in:
Claude Marche
2011-10-12 21:47:20 +02:00
parent 67b11a5667
commit 70f13db7a1
63 changed files with 7807 additions and 3695 deletions
Download Patch File Download Diff File Expand all files Collapse all files

84
examples/programs/decrease1/why3session.xml
View File

@@ -1,11 +1,11 @@
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="examples/programs/decrease1/why3session.xml">
name="programs/decrease1/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93.1"/>
version="0.93"/>
<prover
id="coq"
name="Coq"
@@ -17,11 +17,11 @@
<prover
id="eprover"
name="Eprover"
version="0.8 Steinthal"/>
version="1.4 Namring"/>
<prover
id="gappa"
name="Gappa"
version="0.15.0"/>
version="0.15.1"/>
<prover
id="simplify"
name="Simplify"
@@ -34,10 +34,14 @@
id="vampire"
name="Vampire"
version="0.6"/>
<prover
id="verit"
name="veriT"
version="dev"/>
<prover
id="yices"
name="Yices"
version="1.0.27"/>
version="1.0.25"/>
<prover
id="z3"
name="Z3"
@@ -52,7 +56,7 @@
expanded="true">
<goal
name="decrease1_induction"
sum="0b5a5fde45e86c1bc677f99c692e19db"
sum="053c051a8223cc1da2c161531d36f1cd"
proved="true"
expanded="true"
shape="ainfix >=amixfix []V0V2ainfix -ainfix +amixfix []V0V1V1V2Iainfix <V2alengthV0Aainfix <=V1V2Aainfix <=c0V1FIadecrease1V0F">
@@ -61,13 +65,13 @@
timelimit="10"
edited="decrease1_Decrease1_decrease1_induction_2.v"
obsolete="false">
<result status="valid" time="0.65"/>
<result status="valid" time="0.60"/>
</proof>
</goal>
<goal
name="WP_parameter search"
expl="parameter search"
sum="32db91f9d0b74d7901921f96c785e138"
sum="29e4473301b2a81f142af045a1685940"
proved="true"
expanded="true"
shape="iainfix <V2V0iainfix =agetV1V2c0ainfix =agetV1V3c0NIainfix <V3V2Aainfix <=c0V3FAainfix =agetV1V2c0Aainfix <V2V0Aainfix <=c0V2Oainfix =agetV1V4c0NIainfix <V4V0Aainfix <=c0V4FAainfix =V2aprefix -c1iainfix >agetV1V2c0ainfix <ainfix -V0V5ainfix -V0V2Aainfix <=c0ainfix -V0V2Aainfix =agetV1V6c0NIainfix <V6V0Iainfix <V6V5Aainfix <=c0V6FAainfix <=c0V5Iainfix =V5ainfix +V2agetV1V2FAainfix <V2V0Aainfix <=c0V2ainfix <ainfix -V0V7ainfix -V0V2Aainfix <=c0ainfix -V0V2Aainfix =agetV1V8c0NIainfix <V8V0Iainfix <V8V7Aainfix <=c0V8FAainfix <=c0V7Iainfix =V7ainfix +V2c1FAainfix <V2V0Aainfix <=c0V2Aainfix <V2V0Aainfix <=c0V2ainfix =agetV1V9c0NIainfix <V9aprefix -c1Aainfix <=c0V9FAainfix =agetV1aprefix -c1c0Aainfix <aprefix -c1V0Aainfix <=c0aprefix -c1Oainfix =agetV1V10c0NIainfix <V10V0Aainfix <=c0V10FAainfix =aprefix -c1aprefix -c1Iainfix =agetV1V11c0NIainfix <V11V0Iainfix <V11V2Aainfix <=c0V11FAainfix <=c0V2FAainfix =agetV1V12c0NIainfix <V12V0Iainfix <V12c0Aainfix <=c0V12FAainfix <=c0c0Iadecrease1amk arrayV0V1FF">
@@ -78,7 +82,7 @@
<goal
name="WP_parameter search.1"
expl="loop invariant init"
sum="f429462d6359f2a28844ffc1a8f1eec0"
sum="a8dc9bfac076fd8a9ee3d1415604f6d7"
proved="true"
expanded="true"
shape="ainfix =agetV1V2c0NIainfix <V2V0Iainfix <V2c0Aainfix <=c0V2FAainfix <=c0c0Iadecrease1amk arrayV0V1FF">
@@ -94,7 +98,7 @@
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="z3"
@@ -107,7 +111,7 @@
<goal
name="WP_parameter search.2"
expl="precondition"
sum="00f49e69817e47e187436aba2e90adce"
sum="0a8df33fc212a987081d51ce20531528"
proved="true"
expanded="true"
shape="ainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V3c0NIainfix <V3V0Iainfix <V3V2Aainfix <=c0V3FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
@@ -123,20 +127,20 @@
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"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter search.3"
expl="normal postcondition"
sum="1f5739e3fba1f66944af9f0ce685a8af"
sum="bb82101d072c392400f5660be27afded"
proved="true"
expanded="true"
shape="ainfix =agetV1V3c0NIainfix <V3V2Aainfix <=c0V3FAainfix =agetV1V2c0Aainfix <V2V0Aainfix <=c0V2Oainfix =agetV1V4c0NIainfix <V4V0Aainfix <=c0V4FAainfix =V2aprefix -c1Iainfix =agetV1V2c0Iainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
@@ -152,7 +156,7 @@
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="z3"
@@ -165,7 +169,7 @@
<goal
name="WP_parameter search.4"
expl="precondition"
sum="95604080b163273becaafe2a7359ed70"
sum="c89fd40dabe25380fc91b8c195bcef29"
proved="true"
expanded="true"
shape="ainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V3c0NIainfix <V3V0Iainfix <V3V2Aainfix <=c0V3FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
@@ -181,7 +185,7 @@
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="z3"
@@ -194,7 +198,7 @@
<goal
name="WP_parameter search.5"
expl="precondition"
sum="2b8983833e9bb6c69fd2af502f0fc8f1"
sum="3680f2628864eaa6165267466dfc3ec8"
proved="true"
expanded="true"
shape="ainfix <V2V0Aainfix <=c0V2Iainfix >agetV1V2c0Iainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V3c0NIainfix <V3V0Iainfix <V3V2Aainfix <=c0V3FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
@@ -223,7 +227,7 @@
<goal
name="WP_parameter search.6"
expl="loop invariant preservation"
sum="6a36a0475249bf791db39eb5c7d764dd"
sum="654fecd7a941c9131baaccb9cdcae3ee"
proved="true"
expanded="true"
shape="ainfix =agetV1V4c0NIainfix <V4V0Iainfix <V4V3Aainfix <=c0V4FAainfix <=c0V3Iainfix =V3ainfix +V2agetV1V2FIainfix <V2V0Aainfix <=c0V2Iainfix >agetV1V2c0Iainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
@@ -238,7 +242,7 @@
<goal
name="WP_parameter search.7"
expl="loop variant decreases"
sum="398b995dc98dce086663c5b3c6574fa4"
sum="d0425d28e5be2f1c7f1b371d3c0a9154"
proved="true"
expanded="true"
shape="ainfix <ainfix -V0V3ainfix -V0V2Aainfix <=c0ainfix -V0V2Iainfix =agetV1V4c0NIainfix <V4V0Iainfix <V4V3Aainfix <=c0V4FAainfix <=c0V3Iainfix =V3ainfix +V2agetV1V2FIainfix <V2V0Aainfix <=c0V2Iainfix >agetV1V2c0Iainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
@@ -254,7 +258,7 @@
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="z3"
@@ -267,7 +271,7 @@
<goal
name="WP_parameter search.8"
expl="loop invariant preservation"
sum="1a3bff3b15bb3fdf49ebc51902f24106"
sum="5cc45678d1cfa831d5a30c3ea34aa19a"
proved="true"
expanded="true"
shape="ainfix =agetV1V4c0NIainfix <V4V0Iainfix <V4V3Aainfix <=c0V4FAainfix <=c0V3Iainfix =V3ainfix +V2c1FIainfix >agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
@@ -283,7 +287,7 @@
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="z3"
@@ -296,7 +300,7 @@
<goal
name="WP_parameter search.9"
expl="loop variant decreases"
sum="03a9f221f0aee9832c97b32f4d081dff"
sum="9f554633086dd8c82f6a28922daea82c"
proved="true"
expanded="true"
shape="ainfix <ainfix -V0V3ainfix -V0V2Aainfix <=c0ainfix -V0V2Iainfix =agetV1V4c0NIainfix <V4V0Iainfix <V4V3Aainfix <=c0V4FAainfix <=c0V3Iainfix =V3ainfix +V2c1FIainfix >agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
@@ -312,7 +316,7 @@
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="z3"
@@ -325,7 +329,7 @@
<goal
name="WP_parameter search.10"
expl="normal postcondition"
sum="b7a4163603ffae8e388b3b584fa1c482"
sum="4e7352acfb66fbfd63ff96bfc325ca32"
proved="true"
expanded="true"
shape="ainfix =agetV1V3c0NIainfix <V3aprefix -c1Aainfix <=c0V3FAainfix =agetV1aprefix -c1c0Aainfix <aprefix -c1V0Aainfix <=c0aprefix -c1Oainfix =agetV1V4c0NIainfix <V4V0Aainfix <=c0V4FAainfix =aprefix -c1aprefix -c1Iainfix <V2V0NIainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
@@ -341,7 +345,7 @@
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="z3"
@@ -356,7 +360,7 @@
<goal
name="WP_parameter search_rec"
expl="parameter search_rec"
sum="218de42f33228231b48bf03e7dd8c864"
sum="10712319507d5d205c409d0f1e16c2e1"
proved="true"
expanded="true"
shape="Lamk arrayV0V2iainfix <V1V0iainfix =agetV2V1c0ainfix =agetV2V4c0NIainfix <V4V1Aainfix <=V1V4FAainfix =agetV2V1c0Aainfix <V1V0Aainfix <=V1V1Oainfix =agetV2V5c0NIainfix <V5V0Aainfix <=V1V5FAainfix =V1aprefix -c1iainfix >agetV2V1c0LagetV2V1ainfix =agetV2V8c0NIainfix <V8V7Aainfix <=V1V8FAainfix =agetV2V7c0Aainfix <V7V0Aainfix <=V1V7Oainfix =agetV2V9c0NIainfix <V9V0Aainfix <=V1V9FAainfix =V7aprefix -c1Iainfix =agetV2V10c0NIainfix <V10V7Aainfix <=ainfix +V1V6V10FAainfix =agetV2V7c0Aainfix <V7V0Aainfix <=ainfix +V1V6V7Oainfix =agetV2V11c0NIainfix <V11V0Aainfix <=ainfix +V1V6V11FAainfix =V7aprefix -c1FAainfix <=c0ainfix +V1V6Aadecrease1V3Aainfix <V1V0Aainfix <=c0V1ainfix =agetV2V13c0NIainfix <V13V12Aainfix <=V1V13FAainfix =agetV2V12c0Aainfix <V12V0Aainfix <=V1V12Oainfix =agetV2V14c0NIainfix <V14V0Aainfix <=V1V14FAainfix =V12aprefix -c1Iainfix =agetV2V15c0NIainfix <V15V12Aainfix <=ainfix +V1c1V15FAainfix =agetV2V12c0Aainfix <V12V0Aainfix <=ainfix +V1c1V12Oainfix =agetV2V16c0NIainfix <V16V0Aainfix <=ainfix +V1c1V16FAainfix =V12aprefix -c1FAainfix <=c0ainfix +V1c1Aadecrease1V3Aainfix <V1V0Aainfix <=c0V1Aainfix <V1V0Aainfix <=c0V1ainfix =agetV2V17c0NIainfix <V17aprefix -c1Aainfix <=V1V17FAainfix =agetV2aprefix -c1c0Aainfix <aprefix -c1V0Aainfix <=V1aprefix -c1Oainfix =agetV2V18c0NIainfix <V18V0Aainfix <=V1V18FAainfix =aprefix -c1aprefix -c1Iainfix <=c0V1Aadecrease1V3FFF">
@@ -367,7 +371,7 @@
<goal
name="WP_parameter search_rec.1"
expl="precondition"
sum="d73590a15ec326b1799b3f5e0bfd8a07"
sum="b6f17cc1f88cb8f471edea7550f41d22"
proved="true"
expanded="true"
shape="Lamk arrayV0V2ainfix <V1V0Aainfix <=c0V1Iainfix <V1V0Iainfix <=c0V1Aadecrease1V3FFF">
@@ -396,7 +400,7 @@
<goal
name="WP_parameter search_rec.2"
expl="normal postcondition"
sum="cfc30e116e2d4b3eafc20cc5574fa133"
sum="062f7a79036e53113b93289c00f2a6e9"
proved="true"
expanded="true"
shape="Lamk arrayV0V2ainfix =agetV2V4c0NIainfix <V4V1Aainfix <=V1V4FAainfix =agetV2V1c0Aainfix <V1V0Aainfix <=V1V1Oainfix =agetV2V5c0NIainfix <V5V0Aainfix <=V1V5FAainfix =V1aprefix -c1Iainfix =agetV2V1c0Iainfix <V1V0Aainfix <=c0V1Iainfix <V1V0Iainfix <=c0V1Aadecrease1V3FFF">
@@ -412,7 +416,7 @@
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="z3"
@@ -425,7 +429,7 @@
<goal
name="WP_parameter search_rec.3"
expl="precondition"
sum="25a22039bc7fd9c5d248bbf31f4116cf"
sum="5c98b224af83d1e6d66513db59415627"
proved="true"
expanded="true"
shape="Lamk arrayV0V2ainfix <V1V0Aainfix <=c0V1Iainfix =agetV2V1c0NIainfix <V1V0Aainfix <=c0V1Iainfix <V1V0Iainfix <=c0V1Aadecrease1V3FFF">
@@ -454,7 +458,7 @@
<goal
name="WP_parameter search_rec.4"
expl="precondition"
sum="df6a7c082197b93687b09ec86cebc4fc"
sum="35a44f108d19a179a51b18d27dc93047"
proved="true"
expanded="true"
shape="Lamk arrayV0V2ainfix <V1V0Aainfix <=c0V1Iainfix >agetV2V1c0Iainfix <V1V0Aainfix <=c0V1Iainfix =agetV2V1c0NIainfix <V1V0Aainfix <=c0V1Iainfix <V1V0Iainfix <=c0V1Aadecrease1V3FFF">
@@ -483,7 +487,7 @@
<goal
name="WP_parameter search_rec.5"
expl="precondition"
sum="f31fa9539847d6b18ae221934087ea5e"
sum="a20e1055b9e81281dd9e7e995764b018"
proved="true"
expanded="true"
shape="Lamk arrayV0V2LagetV2V1ainfix <=c0ainfix +V1V4Aadecrease1V3Iainfix <V1V0Aainfix <=c0V1Iainfix >agetV2V1c0Iainfix <V1V0Aainfix <=c0V1Iainfix =agetV2V1c0NIainfix <V1V0Aainfix <=c0V1Iainfix <V1V0Iainfix <=c0V1Aadecrease1V3FFF">
@@ -512,7 +516,7 @@
<goal
name="WP_parameter search_rec.6"
expl="normal postcondition"
sum="829516cb4dd6801ad69e14bdc31565cd"
sum="dc030314d373479dd7f096a2f6bd1366"
proved="true"
expanded="true"
shape="Lamk arrayV0V2LagetV2V1ainfix =agetV2V6c0NIainfix <V6V5Aainfix <=V1V6FAainfix =agetV2V5c0Aainfix <V5V0Aainfix <=V1V5Oainfix =agetV2V7c0NIainfix <V7V0Aainfix <=V1V7FAainfix =V5aprefix -c1Iainfix =agetV2V8c0NIainfix <V8V5Aainfix <=ainfix +V1V4V8FAainfix =agetV2V5c0Aainfix <V5V0Aainfix <=ainfix +V1V4V5Oainfix =agetV2V9c0NIainfix <V9V0Aainfix <=ainfix +V1V4V9FAainfix =V5aprefix -c1FIainfix <=c0ainfix +V1V4Aadecrease1V3Iainfix <V1V0Aainfix <=c0V1Iainfix >agetV2V1c0Iainfix <V1V0Aainfix <=c0V1Iainfix =agetV2V1c0NIainfix <V1V0Aainfix <=c0V1Iainfix <V1V0Iainfix <=c0V1Aadecrease1V3FFF">
@@ -521,13 +525,13 @@
timelimit="10"
edited="decrease1_WP_Decrease1_WP_parameter_search_rec_1.v"
obsolete="false">
<result status="valid" time="1.58"/>
<result status="valid" time="1.59"/>
</proof>
</goal>
<goal
name="WP_parameter search_rec.7"
expl="precondition"
sum="74e17e1b5b8562e2329750548ba8b7dc"
sum="332108dedf5c37866961a7fb1331344d"
proved="true"
expanded="true"
shape="Lamk arrayV0V2ainfix <=c0ainfix +V1c1Aadecrease1V3Iainfix >agetV2V1c0NIainfix <V1V0Aainfix <=c0V1Iainfix =agetV2V1c0NIainfix <V1V0Aainfix <=c0V1Iainfix <V1V0Iainfix <=c0V1Aadecrease1V3FFF">
@@ -556,7 +560,7 @@
<goal
name="WP_parameter search_rec.8"
expl="normal postcondition"
sum="0753a63864a318601818633033c5c922"
sum="68cc8d7c0fadbea59aa9f3eefd766ff7"
proved="true"
expanded="true"
shape="Lamk arrayV0V2ainfix =agetV2V5c0NIainfix <V5V4Aainfix <=V1V5FAainfix =agetV2V4c0Aainfix <V4V0Aainfix <=V1V4Oainfix =agetV2V6c0NIainfix <V6V0Aainfix <=V1V6FAainfix =V4aprefix -c1Iainfix =agetV2V7c0NIainfix <V7V4Aainfix <=ainfix +V1c1V7FAainfix =agetV2V4c0Aainfix <V4V0Aainfix <=ainfix +V1c1V4Oainfix =agetV2V8c0NIainfix <V8V0Aainfix <=ainfix +V1c1V8FAainfix =V4aprefix -c1FIainfix <=c0ainfix +V1c1Aadecrease1V3Iainfix >agetV2V1c0NIainfix <V1V0Aainfix <=c0V1Iainfix =agetV2V1c0NIainfix <V1V0Aainfix <=c0V1Iainfix <V1V0Iainfix <=c0V1Aadecrease1V3FFF">
@@ -565,7 +569,7 @@
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="alt-ergo"
@@ -585,7 +589,7 @@
<goal
name="WP_parameter search_rec.9"
expl="normal postcondition"
sum="d0f3f258ada86e676fe42c6f6d4cba7c"
sum="191848f2a951b9a0435c7d46b7e7fdc2"
proved="true"
expanded="true"
shape="Lamk arrayV0V2ainfix =agetV2V4c0NIainfix <V4aprefix -c1Aainfix <=V1V4FAainfix =agetV2aprefix -c1c0Aainfix <aprefix -c1V0Aainfix <=V1aprefix -c1Oainfix =agetV2V5c0NIainfix <V5V0Aainfix <=V1V5FAainfix =aprefix -c1aprefix -c1Iainfix <V1V0NIainfix <=c0V1Aadecrease1V3FFF">