Commit 14829503 authored by MARCHE Claude's avatar MARCHE Claude

updated sessions after replay

parent b9be34ab
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="fill/why3session.xml">
name="programs/fill/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
......@@ -17,19 +17,19 @@
<file
name="../fill.mlw"
verified="true"
expanded="true">
expanded="false">
<theory
name="WP Fill"
locfile="fill/../fill.mlw"
loclnum="4" loccnumb="7" loccnume="11"
locfile="programs/fill/../fill.mlw"
loclnum="6" loccnumb="7" loccnume="11"
verified="true"
expanded="true">
<goal
name="WP_parameter fill"
locfile="fill/../fill.mlw"
loclnum="16" loccnumb="10" loccnume="14"
locfile="programs/fill/../fill.mlw"
loclnum="19" loccnumb="10" loccnume="14"
expl="parameter fill"
sum="a7f6d0a4fd8b99196978e39ff255fcf5"
sum="0205a584fbde7e79af79a6195619dfa4"
proved="true"
expanded="true"
shape="CV0aNullacontainsV0agetV3V4Iainfix <V4V2Aainfix <=V2V4FAainfix =agetV3V5agetV3V5Iainfix <V5V2Aainfix <=c0V5FAainfix <=V2V1Aainfix <=V2V2aNodeVVViainfix =V10V1NacontainsV0agetV12V14Iainfix <V14V13Aainfix <=V2V14FAainfix =agetV12V15agetV3V15Iainfix <V15V2Aainfix <=c0V15FAainfix <=V13V1Aainfix <=V2V13IacontainsV8agetV12V16Iainfix <V16V13Aainfix <=ainfix +V10c1V16FAainfix =agetV12V17agetV11V17Iainfix <V17ainfix +V10c1Aainfix <=c0V17FAainfix <=V13V1Aainfix <=ainfix +V10c1V13FFAainfix <=ainfix +V10c1V1Aainfix <=c0ainfix +V10c1Iainfix =V11asetV9V10V7FAainfix <V10V1Aainfix <=c0V10acontainsV0agetV9V18Iainfix <V18V10Aainfix <=V2V18FAainfix =agetV9V19agetV3V19Iainfix <V19V2Aainfix <=c0V19FAainfix <=V10V1Aainfix <=V2V10IacontainsV6agetV9V20Iainfix <V20V10Aainfix <=V2V20FAainfix =agetV9V21agetV3V21Iainfix <V21V2Aainfix <=c0V21FAainfix <=V10V1Aainfix <=V2V10FFAainfix <=V2V1Aainfix <=c0V2Iainfix <=V2V1Aainfix <=c0V2FFFF">
......@@ -39,20 +39,23 @@
<proof
prover="1"
timelimit="10"
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
</proof>
<proof
prover="0"
timelimit="10"
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
</proof>
<proof
prover="2"
timelimit="10"
obsolete="false">
<result status="valid" time="0.10"/>
obsolete="false"
archived="false">
<result status="valid" time="0.11"/>
</proof>
</goal>
</theory>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="examples/programs/insertion_sort_list/why3session.xml">
name="programs/insertion_sort_list/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
......@@ -16,16 +16,16 @@
expanded="false">
<theory
name="WP M"
locfile="examples/programs/insertion_sort_list/../insertion_sort_list.mlw"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="4" loccnumb="7" loccnume="8"
verified="true"
expanded="true">
<goal
name="WP_parameter insert"
locfile="examples/programs/insertion_sort_list/../insertion_sort_list.mlw"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="11" loccnumb="10" loccnume="16"
expl="parameter insert"
sum="8a1ed54c3f0c362fb144098bfd668b32"
sum="84e2aa9751598370fc4d9f6f9c5b4a40"
proved="true"
expanded="true"
shape="CV1aNilapermutaConsV0V1aConsV0aNilAasortedaConsV0aNilaConsVViainfix <=V0V2apermutaConsV0V1aConsV0V1AasortedaConsV0V1apermutaConsV0V1aConsV2V4AasortedaConsV2V4IapermutaConsV0V3V4AasortedV4FAasortedV3Aainfix <alengthV3alengthV1Aainfix <=c0alengthV1IasortedV1FF">
......@@ -38,10 +38,10 @@
expanded="true">
<goal
name="WP_parameter insert.1"
locfile="examples/programs/insertion_sort_list/../insertion_sort_list.mlw"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="11" loccnumb="10" loccnume="16"
expl="parameter insert"
sum="221159a13d4206a4460d1723c7561f5b"
sum="4a69f68c5d460749f0ef438e15442acf"
proved="true"
expanded="true"
shape="CV1aNilapermutaConsV0V1aConsV0aNilAasortedaConsV0aNilaConsVVtIasortedV1FF">
......@@ -53,15 +53,15 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter insert.2"
locfile="examples/programs/insertion_sort_list/../insertion_sort_list.mlw"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="11" loccnumb="10" loccnume="16"
expl="parameter insert"
sum="03780f98738f0a4d31b9f5cdafef018f"
sum="ca1192523c9f6846cbe0519ed7977850"
proved="true"
expanded="true"
shape="CV1aNiltaConsVVapermutaConsV0V1aConsV0V1AasortedaConsV0V1Iainfix <=V0V2IasortedV1FF">
......@@ -78,10 +78,10 @@
</goal>
<goal
name="WP_parameter insert.3"
locfile="examples/programs/insertion_sort_list/../insertion_sort_list.mlw"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="11" loccnumb="10" loccnume="16"
expl="parameter insert"
sum="bd15c5616f0e48a457c665b7daeb5133"
sum="323ba14021e983aedaa70f389a6f9ca2"
proved="true"
expanded="true"
shape="CV1aNiltaConsVVasortedV3Aainfix <alengthV3alengthV1Aainfix <=c0alengthV1Iainfix <=V0V2NIasortedV1FF">
......@@ -93,15 +93,15 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter insert.4"
locfile="examples/programs/insertion_sort_list/../insertion_sort_list.mlw"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="11" loccnumb="10" loccnume="16"
expl="parameter insert"
sum="17df99648aa521a75f2047df4cf0c6f0"
sum="3dd8034ce59793f25f60f2f400095552"
proved="true"
expanded="true"
shape="CV1aNiltaConsVVapermutaConsV0V1aConsV2V4AasortedaConsV2V4IapermutaConsV0V3V4AasortedV4FIasortedV3Aainfix <alengthV3alengthV1Aainfix <=c0alengthV1Iainfix <=V0V2NIasortedV1FF">
......@@ -113,17 +113,17 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.11"/>
<result status="valid" time="0.17"/>
</proof>
</goal>
</transf>
</goal>
<goal
name="WP_parameter insertion_sort"
locfile="examples/programs/insertion_sort_list/../insertion_sort_list.mlw"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="19" loccnumb="10" loccnume="24"
expl="parameter insertion_sort"
sum="d28eefc56d379c5156175265bf010598"
sum="16d8a43872423232fe7bd6e35d3a5ba5"
proved="true"
expanded="true"
shape="CV0aNilapermutV0aNilAasortedaNilaConsVVapermutV0V4AasortedV4IapermutaConsV1V3V4AasortedV4FAasortedV3IapermutV2V3AasortedV3FAainfix <alengthV2alengthV0Aainfix <=c0alengthV0F">
......@@ -136,10 +136,10 @@
expanded="true">
<goal
name="WP_parameter insertion_sort.1"
locfile="examples/programs/insertion_sort_list/../insertion_sort_list.mlw"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="19" loccnumb="10" loccnume="24"
expl="parameter insertion_sort"
sum="71173457dcb476b018a44d47d231ad49"
sum="94c7e6b8ec2a0a739033d3bd222c577f"
proved="true"
expanded="true"
shape="CV0aNilapermutV0aNilAasortedaNilaConsVVtF">
......@@ -156,10 +156,10 @@
</goal>
<goal
name="WP_parameter insertion_sort.2"
locfile="examples/programs/insertion_sort_list/../insertion_sort_list.mlw"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="19" loccnumb="10" loccnume="24"
expl="parameter insertion_sort"
sum="17e9acde476c648319587d89cd36c1c8"
sum="59f3bde7dbb179dd4ba4e0943bb955c7"
proved="true"
expanded="true"
shape="CV0aNiltaConsVVainfix <alengthV2alengthV0Aainfix <=c0alengthV0F">
......@@ -183,10 +183,10 @@
</goal>
<goal
name="WP_parameter insertion_sort.3"
locfile="examples/programs/insertion_sort_list/../insertion_sort_list.mlw"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="19" loccnumb="10" loccnume="24"
expl="parameter insertion_sort"
sum="80b0842e233ef20ca04bf6ed7b47e326"
sum="01a3a1139967fc619194daefb574ad7e"
proved="true"
expanded="true"
shape="CV0aNiltaConsVVasortedV3IapermutV2V3AasortedV3FIainfix <alengthV2alengthV0Aainfix <=c0alengthV0F">
......@@ -198,7 +198,7 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="0"
......@@ -210,10 +210,10 @@
</goal>
<goal
name="WP_parameter insertion_sort.4"
locfile="examples/programs/insertion_sort_list/../insertion_sort_list.mlw"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="19" loccnumb="10" loccnume="24"
expl="parameter insertion_sort"
sum="70da74d76767b2269d36aef985b01798"
sum="0664d39ce85984eefbde659a0dd4e23a"
proved="true"
expanded="true"
shape="CV0aNiltaConsVVapermutV0V4AasortedV4IapermutaConsV1V3V4AasortedV4FIasortedV3IapermutV2V3AasortedV3FIainfix <alengthV2alengthV0Aainfix <=c0alengthV0F">
......@@ -225,14 +225,14 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.04"/>
</proof>
<proof
prover="0"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.08"/>
</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