Commit dbc5ef6e authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

update sessions, part 2

parent 38ce7f9d
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/andrei/prj/why-git/share/why3session.dtd">
<why3session
name="hoare_logic/wp_total/why3session.xml" shape_version="2">
name="examples/hoare_logic/wp_total/why3session.xml" shape_version="2">
<prover
id="0"
name="Alt-Ergo"
......@@ -24,13 +24,13 @@
expanded="false">
<theory
name="Imp"
locfile="hoare_logic/wp_total/../wp_total.mlw"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="3" loccnumb="7" loccnume="10"
verified="false"
expanded="true">
<goal
name="Test13"
locfile="hoare_logic/wp_total/../wp_total.mlw"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="72" loccnumb="5" loccnume="11"
sum="9a8e548828642320bb93623c265bf91a"
proved="true"
......@@ -47,7 +47,7 @@
</goal>
<goal
name="Test42"
locfile="hoare_logic/wp_total/../wp_total.mlw"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="75" loccnumb="5" loccnume="11"
sum="9ddfe147848fcfc2f48bf55a57792b7b"
proved="true"
......@@ -64,7 +64,7 @@
</goal>
<goal
name="Test0"
locfile="hoare_logic/wp_total/../wp_total.mlw"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="78" loccnumb="5" loccnume="10"
sum="2807cc05410b5c472c4fa724c1a8db10"
proved="true"
......@@ -97,7 +97,7 @@
</goal>
<goal
name="Test55"
locfile="hoare_logic/wp_total/../wp_total.mlw"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="81" loccnumb="5" loccnume="11"
sum="3f79a76b9d676a562602cece0860f365"
proved="true"
......@@ -110,12 +110,12 @@
edited="wp_total_Imp_Test55_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.50"/>
<result status="valid" time="0.47"/>
</proof>
</goal>
<goal
name="eval_subst_term"
locfile="hoare_logic/wp_total/../wp_total.mlw"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="119" loccnumb="6" loccnume="21"
sum="40bd4cc38f5bbeb422a3f7b2274dfdd3"
proved="true"
......@@ -128,12 +128,12 @@
edited="wp_total_Imp_eval_subst_term_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.54"/>
<result status="valid" time="0.50"/>
</proof>
</goal>
<goal
name="eval_subst"
locfile="hoare_logic/wp_total/../wp_total.mlw"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="137" loccnumb="6" loccnume="16"
sum="fffb79e884deafec800e64ac3893921b"
proved="false"
......@@ -151,7 +151,7 @@
</goal>
<goal
name="check_skip"
locfile="hoare_logic/wp_total/../wp_total.mlw"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="154" loccnumb="6" loccnume="16"
sum="b6ef3830ebf3316fcfd59374a5cf80d2"
proved="true"
......@@ -163,12 +163,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="Ass42"
locfile="hoare_logic/wp_total/../wp_total.mlw"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="204" loccnumb="7" loccnume="12"
sum="e8c3806e15e351d6c2c750c4108c35d6"
proved="true"
......@@ -185,7 +185,7 @@
</goal>
<goal
name="If42"
locfile="hoare_logic/wp_total/../wp_total.mlw"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="210" loccnumb="7" loccnume="11"
sum="3bd92161c9bf61ca9ddeb39cfe7f1dc9"
proved="true"
......@@ -198,12 +198,12 @@
edited="wp_total_Imp_If42_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.63"/>
<result status="valid" time="0.62"/>
</proof>
</goal>
<goal
name="steps_non_neg"
locfile="hoare_logic/wp_total/../wp_total.mlw"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="241" loccnumb="6" loccnume="19"
sum="7ca6d3e86a9a448740868c50dfd345a4"
proved="true"
......@@ -216,12 +216,12 @@
edited="wp_total_Imp_steps_non_neg_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.50"/>
<result status="valid" time="0.47"/>
</proof>
</goal>
<goal
name="many_steps_seq"
locfile="hoare_logic/wp_total/../wp_total.mlw"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="245" loccnumb="6" loccnume="20"
sum="5b9837831b39bf3a1e7c660539aff222"
proved="true"
......@@ -234,12 +234,12 @@
edited="wp_total_Imp_many_steps_seq_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.61"/>
<result status="valid" time="0.59"/>
</proof>
</goal>
<goal
name="skip_rule"
locfile="hoare_logic/wp_total/../wp_total.mlw"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="274" loccnumb="6" loccnume="15"
sum="a215720e030dac80edb47f94b0046b03"
proved="true"
......@@ -251,12 +251,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="1.73"/>
<result status="valid" time="1.69"/>
</proof>
</goal>
<goal
name="assign_rule"
locfile="hoare_logic/wp_total/../wp_total.mlw"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="277" loccnumb="6" loccnume="17"
sum="11a196c9cc460f612fede251e5a5ac8a"
proved="true"
......@@ -269,12 +269,12 @@
edited="wp_total_Imp_assign_rule_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.58"/>
<result status="valid" time="0.56"/>
</proof>
</goal>
<goal
name="seq_rule"
locfile="hoare_logic/wp_total/../wp_total.mlw"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="281" loccnumb="6" loccnume="14"
sum="3a50a902177833bb8790f1f0367d0079"
proved="true"
......@@ -291,7 +291,7 @@
</goal>
<goal
name="if_rule"
locfile="hoare_logic/wp_total/../wp_total.mlw"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="286" loccnumb="6" loccnume="13"
sum="5c396f3b34ad557d67cf409cd6e5a4f2"
proved="true"
......@@ -304,12 +304,12 @@
edited="wp_total_Imp_if_rule_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.63"/>
<result status="valid" time="0.58"/>
</proof>
</goal>
<goal
name="assert_rule"
locfile="hoare_logic/wp_total/../wp_total.mlw"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="292" loccnumb="6" loccnume="17"
sum="67afeaa718be5f0aa461856171d6706a"
proved="true"
......@@ -322,12 +322,12 @@
edited="wp_total_Imp_assert_rule_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.56"/>
<result status="valid" time="0.55"/>
</proof>
</goal>
<goal
name="assert_rule_ext"
locfile="hoare_logic/wp_total/../wp_total.mlw"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="296" loccnumb="6" loccnume="21"
sum="aaef93d8cede709a5025b6077bf6740d"
proved="true"
......@@ -340,12 +340,12 @@
edited="wp_total_Imp_assert_rule_ext_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.56"/>
<result status="valid" time="0.54"/>
</proof>
</goal>
<goal
name="while_rule"
locfile="hoare_logic/wp_total/../wp_total.mlw"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="300" loccnumb="6" loccnume="16"
sum="96db1357813c52999d4a828cc55d906c"
proved="true"
......@@ -363,7 +363,7 @@
</goal>
<goal
name="while_rule_ext"
locfile="hoare_logic/wp_total/../wp_total.mlw"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="305" loccnumb="6" loccnume="20"
sum="2117233c55303ac1a782a598334ce4c8"
proved="true"
......@@ -376,12 +376,12 @@
edited="wp_total_Imp_while_rule_ext_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.67"/>
<result status="valid" time="0.66"/>
</proof>
</goal>
<goal
name="consequence_rule"
locfile="hoare_logic/wp_total/../wp_total.mlw"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="311" loccnumb="6" loccnume="22"
sum="0ac68b40862905a191b0378bc9bc1dcc"
proved="true"
......@@ -401,25 +401,25 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.70"/>
<result status="valid" time="0.68"/>
</proof>
</goal>
</theory>
<theory
name="WP WP"
locfile="hoare_logic/wp_total/../wp_total.mlw"
name="WP"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="339" loccnumb="7" loccnume="9"
verified="false"
expanded="true">
<goal
name="WP_parameter wp"
locfile="hoare_logic/wp_total/../wp_total.mlw"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="parameter wp"
sum="d772f89217e6589a636ccde1e83c102f"
sum="9c9ea4732e967818668b40f5bbfbc665"
proved="false"
expanded="true"
shape="CV0aSskipavalid_tripleV1V0V1aSseqVVavalid_tripleV5V0V1Iavalid_tripleV5V2V4FIavalid_tripleV4V3V1FaSassignVVavalid_tripleasubstV1V6V7V0V1aSifVVVavalid_tripleaFandaFimpliesaFtermV8V11aFimpliesaFnotaFtermV8V12V0V1Iavalid_tripleV12V10V1FIavalid_tripleV11V9V1FaSassertVavalid_tripleaFimpliesV13V1V0V1aSwhileVVVavalid_tripleaFandV15aFandaFimpliesaFandaFtermV14V15V17aFimpliesaFandaFnotaFtermV14V15V1V0V1Iavalid_tripleV17V16V15FFF">
shape="CV0aSskipavalid_tripleV1V0V1aSseqVVavalid_tripleV5V0V1Iavalid_tripleV5V2V4FIavalid_tripleV4V3V1FaSassignVVavalid_tripleasubstV1V6V7V0V1aSifVVVavalid_tripleaFandaFimpliesaFtermV8V12aFimpliesaFnotaFtermV8V11V0V1Iavalid_tripleV12V9V1FIavalid_tripleV11V10V1FaSassertVavalid_tripleaFimpliesV13V1V0V1aSwhileVVVavalid_tripleaFandV15aFandaFimpliesaFandaFtermV14V15V17aFimpliesaFandaFnotaFtermV14V15V1V0V1Iavalid_tripleV17V16V15FF">
<label
name="expl:parameter wp"/>
<proof
......@@ -429,7 +429,7 @@
edited="wp_total_WP_WP_WP_parameter_wp_2.v"
obsolete="false"
archived="false">
<result status="unknown" time="0.52"/>
<result status="unknown" time="0.51"/>
</proof>
<transf
name="split_goal"
......@@ -437,13 +437,13 @@
expanded="true">
<goal
name="WP_parameter wp.1"
locfile="hoare_logic/wp_total/../wp_total.mlw"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="parameter wp"
sum="40ca0adaa4ee2af9a496594e9fbc980a"
sum="b3b8bdad3bb801651a04fc0fb388e70d"
proved="true"
expanded="false"
shape="CV0aSskipavalid_tripleV1V0V1aSseqVVtaSassignVVtaSifVVVtaSassertVtaSwhileVVVtFF">
shape="CV0aSskipavalid_tripleV1V0V1aSseqVVtaSassignVVtaSifVVVtaSassertVtaSwhileVVVtF">
<label
name="expl:parameter wp"/>
<proof
......@@ -457,13 +457,13 @@
</goal>
<goal
name="WP_parameter wp.2"
locfile="hoare_logic/wp_total/../wp_total.mlw"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="parameter wp"
sum="3ef32fbe6d09920c0f3115061111fdbc"
sum="507f9bc6a02b9af9fc54eb42c211ad6b"
proved="true"
expanded="false"
shape="CV0aSskiptaSseqVVavalid_tripleV5V0V1Iavalid_tripleV5V2V4FIavalid_tripleV4V3V1FaSassignVVtaSifVVVtaSassertVtaSwhileVVVtFF">
shape="CV0aSskiptaSseqVVavalid_tripleV5V0V1Iavalid_tripleV5V2V4FIavalid_tripleV4V3V1FaSassignVVtaSifVVVtaSassertVtaSwhileVVVtF">
<label
name="expl:parameter wp"/>
<proof
......@@ -477,13 +477,13 @@
</goal>
<goal
name="WP_parameter wp.3"
locfile="hoare_logic/wp_total/../wp_total.mlw"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="parameter wp"
sum="009738a4099a4c69b676819f6d3b793b"
sum="23b06dd3883c8fd55a55ffda47ed9afd"
proved="true"
expanded="false"
shape="CV0aSskiptaSseqVVtaSassignVVavalid_tripleasubstV1V4V5V0V1aSifVVVtaSassertVtaSwhileVVVtFF">
shape="CV0aSskiptaSseqVVtaSassignVVavalid_tripleasubstV1V4V5V0V1aSifVVVtaSassertVtaSwhileVVVtF">
<label
name="expl:parameter wp"/>
<proof
......@@ -497,13 +497,13 @@
</goal>
<goal
name="WP_parameter wp.4"
locfile="hoare_logic/wp_total/../wp_total.mlw"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="parameter wp"
sum="7dcde9aa14baafb3dbdc1c5846771313"
sum="fc9020200412c10d0dc90e8dbdc9d48f"
proved="true"
expanded="false"
shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVavalid_tripleaFandaFimpliesaFtermV6V9aFimpliesaFnotaFtermV6V10V0V1Iavalid_tripleV10V8V1FIavalid_tripleV9V7V1FaSassertVtaSwhileVVVtFF">
shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVavalid_tripleaFandaFimpliesaFtermV6V10aFimpliesaFnotaFtermV6V9V0V1Iavalid_tripleV10V7V1FIavalid_tripleV9V8V1FaSassertVtaSwhileVVVtF">
<label
name="expl:parameter wp"/>
<proof
......@@ -512,7 +512,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.57"/>
<result status="valid" time="0.56"/>
</proof>
<proof
prover="1"
......@@ -533,13 +533,13 @@
</goal>
<goal
name="WP_parameter wp.5"
locfile="hoare_logic/wp_total/../wp_total.mlw"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="parameter wp"
sum="89de530f91fbcaa953fb429fae46f0e1"
sum="349dbc9cb23ab5534a125a7b8fe71582"
proved="true"
expanded="true"
shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVtaSassertVavalid_tripleaFimpliesV9V1V0V1aSwhileVVVtFF">
shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVtaSassertVavalid_tripleaFimpliesV9V1V0V1aSwhileVVVtF">
<label
name="expl:parameter wp"/>
<proof
......@@ -573,18 +573,18 @@
edited="wp_total_WP_WP_WP_parameter_wp_3.v"
obsolete="false"
archived="false">
<result status="unknown" time="0.51"/>
<result status="unknown" time="0.50"/>
</proof>
</goal>
<goal
name="WP_parameter wp.6"
locfile="hoare_logic/wp_total/../wp_total.mlw"
locfile="examples/hoare_logic/wp_total/../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="parameter wp"
sum="cf8b2bf6e8eb7e5b80d87c84886cf1b4"
sum="fffbe1f65508f2a22447b45053db2882"
proved="false"
expanded="true"
shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVtaSassertVtaSwhileVVVavalid_tripleaFandV11aFandaFimpliesaFandaFtermV10V11V13aFimpliesaFandaFnotaFtermV10V11V1V0V1Iavalid_tripleV13V12V11FFF">
shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVtaSassertVtaSwhileVVVavalid_tripleaFandV11aFandaFimpliesaFandaFtermV10V11V13aFimpliesaFandaFnotaFtermV10V11V1V0V1Iavalid_tripleV13V12V11FF">
<label
name="expl:parameter wp"/>
<proof
......@@ -593,7 +593,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="5.01"/>
<result status="timeout" time="5.02"/>
</proof>
<proof
prover="1"
......@@ -609,7 +609,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
<result status="timeout" time="5.01"/>
</proof>
</goal>
</transf>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/andrei/prj/why-git/share/why3session.dtd">
<why3session
name="programs/fibonacci/why3session.xml" shape_version="2">
name="examples/programs/fibonacci/why3session.xml" shape_version="2">
<prover
id="0"
name="Alt-Ergo"
......@@ -32,11 +32,11 @@
version="2.19"/>
<file
name="../fibonacci.mlw"
verified="true"
verified="false"
expanded="false">
<theory
name="Fibonacci"
locfile="programs/fibonacci/../fibonacci.mlw"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="2" loccnumb="7" loccnume="16"
verified="true"
expanded="true">
......@@ -45,13 +45,13 @@
</theory>
<theory
name="FibonacciTest"
locfile="programs/fibonacci/../fibonacci.mlw"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="14" loccnumb="7" loccnume="20"
verified="true"
expanded="false">
<goal
name="isfib_2_1"
locfile="programs/fibonacci/../fibonacci.mlw"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="18" loccnumb="8" loccnume="17"
sum="53cb43c962b6ac473353e3b02dc4b67b"
proved="true"
......@@ -68,7 +68,7 @@
</goal>
<goal
name="isfib_6_8"
locfile="programs/fibonacci/../fibonacci.mlw"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="19" loccnumb="8" loccnume="17"
sum="23ec2eb87c0bebe1406c9b91f62e2d92"
proved="true"
......@@ -85,7 +85,7 @@
</goal>
<goal
name="not_isfib_2_2"
locfile="programs/fibonacci/../fibonacci.mlw"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="21" loccnumb="8" loccnume="21"
sum="f3cd71efc59ece547b8cfe0932c063ca"
proved="true"
......@@ -134,20 +134,20 @@
</goal>
</theory>
<theory
name="WP FibonacciLinear"
locfile="programs/fibonacci/../fibonacci.mlw"
name="FibonacciLinear"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="25" loccnumb="7" loccnume="22"
verified="true"
expanded="false">
<goal
name="WP_parameter fib"
locfile="programs/fibonacci/../fibonacci.mlw"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="31" loccnumb="6" loccnume="9"
expl="parameter fib"
sum="b5ea0a58197b74b30c5c380161c411b8"
sum="0524e9e40b90c0c213c0df1110b389f1"
proved="true"
expanded="false"
shape="ainfix =afibV0V2Iainfix =afibainfix +ainfix -V0c1c1V2Aainfix =afibainfix +ainfix +ainfix -V0c1c1c1V1Aainfix &lt;=ainfix +ainfix -V0c1c1V0Aainfix &lt;=c0ainfix +ainfix -V0c1c1Aainfix =afibainfix +V3c1V4Aainfix =afibainfix +ainfix +V3c1c1V5Aainfix &lt;=ainfix +V3c1V0Aainfix &lt;=c0ainfix +V3c1Iainfix =V5ainfix +V1V2FIainfix =V4V1FIainfix =afibV3V2Aainfix =afibainfix +V3c1V1Aainfix &lt;=V3V0Aainfix &lt;=c0V3Iainfix &lt;=V3ainfix -V0c1Aainfix &lt;=c0V3FFFAainfix =afibc0c0Aainfix =afibainfix +c0c1c1Aainfix &lt;=c0V0Aainfix &lt;=c0c0Iainfix &lt;=c0ainfix -V0c1Aainfix =afibV0c0Iainfix &gt;c0ainfix -V0c1Iainfix &gt;=V0c0F">
shape="ainfix =afibV0V2Iainfix =afibainfix +ainfix -V0c1c1V2Aainfix =afibainfix +ainfix +ainfix -V0c1c1c1V1Aainfix &lt;=ainfix +ainfix -V0c1c1V0Aainfix &lt;=c0ainfix +ainfix -V0c1c1Aainfix =afibainfix +V3c1V4Aainfix =afibainfix +ainfix +V3c1c1V5Aainfix &lt;=ainfix +V3c1V0Aainfix &lt;=c0ainfix +V3c1Iainfix =V5ainfix +V1V2FIainfix =V4V1FIainfix =afibV3V2Aainfix =afibainfix +V3c1V1Aainfix &lt;=V3V0Aainfix &lt;=c0V3Iainfix &lt;=V3ainfix -V0c1Aainfix &lt;=c0V3FFAainfix =afibc0c0Aainfix =afibainfix +c0c1c1Aainfix &lt;=c0V0Aainfix &lt;=c0c0Iainfix &lt;=c0ainfix -V0c1Aainfix =afibV0c0Iainfix &gt;c0ainfix -V0c1Iainfix &gt;=V0c0F">
<label
name="expl:parameter fib"/>
<proof
......@@ -162,7 +162,7 @@
</theory>
<theory
name="Mat22"
locfile="programs/fibonacci/../fibonacci.mlw"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="46" loccnumb="7" loccnume="12"
verified="true"
expanded="true">
......@@ -170,32 +170,32 @@
name="2x2 integer matrices"/>
</theory>
<theory
name="WP FibonacciLogarithmic"
locfile="programs/fibonacci/../fibonacci.mlw"
name="FibonacciLogarithmic"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="68" loccnumb="7" loccnume="27"
verified="true"
verified="false"
expanded="true">
<goal
name="WP_parameter logfib"
locfile="programs/fibonacci/../fibonacci.mlw"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="82" loccnumb="10" loccnume="16"
expl="parameter logfib"
sum="479ceaf8cec90f791daac67c63be4e52"
proved="true"
sum="3966dacbc1855018004e996b874f27fa"
proved="false"
expanded="false"
shape="iainfix =V0c0ainfix =apoweramk tc1c1c1c0V0amk tainfix +c1c0c0c0c1iainfix =amodV0c2c0ainfix =apoweramk tc1c1c1c0V0amk tainfix +V3V4V4V4V3Lainfix *V2ainfix +V1ainfix +V1V2Lainfix +ainfix *V1V1ainfix *V2V2ainfix =apoweramk tc1c1c1c0V0amk tainfix +V5V6V6V6V5Lainfix +ainfix *ainfix +V1V2ainfix +V1V2ainfix *V2V2Lainfix *V2ainfix +V1ainfix +V1V2Iainfix =apoweramk tc1c1c1c0adivV0c2amk tainfix +V1V2V2V2V1FAainfix &gt;=adivV0c2c0Aainfix &lt;adivV0c2V0Aainfix &lt;=c0V0Iainfix &gt;=V0c0F">
<label
name="expl:parameter logfib"/>
<transf
name="split_goal"
proved="true"
proved="false"
expanded="true">
<goal
name="WP_parameter logfib.1"
locfile="programs/fibonacci/../fibonacci.mlw"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="82" loccnumb="10" loccnume="16"
expl="normal postcondition"
sum="f4276d4917db9b28cbea9ed6d8f150d3"
sum="adf3fda094b1f16d576b23cf13147c8d"
proved="true"
expanded="false"
shape="ainfix =apoweramk tc1c1c1c0V0amk tainfix +c1c0c0c0c1Iainfix =V0c0Iainfix &gt;=V0c0F">
......@@ -223,7 +223,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
......@@ -236,13 +236,25 @@
</goal>
<goal
name="WP_parameter logfib.2"
locfile="programs/fibonacci/../fibonacci.mlw"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="82" loccnumb="10" loccnume="16"
expl="variant decreases"
sum="4464035e38e634573f8cf479606f0013"
proved="false"
expanded="false"
shape="ainfix &lt;adivV0c2V0Aainfix &lt;=c0V0Iainfix =V0c0NIainfix &gt;=V0c0F">
<label
name="expl:parameter logfib"/>
</goal>
<goal
name="WP_parameter logfib.3"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="82" loccnumb="10" loccnume="16"
expl="precondition"
sum="b7477cd008ec2350ecf7bd7cb3f22896"
sum="914eb29f581e4f81f1dc88e3cd6a2125"
proved="true"
expanded="false"
shape="ainfix &gt;=adivV0c2c0Aainfix &lt;adivV0c2V0Aainfix &lt;=c0V0Iainfix =V0c0NIainfix &gt;=V0c0F">
shape="ainfix &gt;=adivV0c2c0Iainfix =V0c0NIainfix &gt;=V0c0F">
<label
name="expl:parameter logfib"/>
<proof
......@@ -263,11 +275,11 @@
</proof>
</goal>
<goal
name="WP_parameter logfib.3"
locfile="programs/fibonacci/../fibonacci.mlw"
name="WP_parameter logfib.4"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="82" loccnumb="10" loccnume="16"
expl="normal postcondition"
sum="997679ab2cbdc92a2763d1826685ed15"
sum="c8a4a4717b459e34b8d3a05ff9c7fb31"
proved="true"
expanded="false"
shape="iainfix =amodV0c2c0ainfix =apoweramk tc1c1c1c0V0amk tainfix +V3V4V4V4V3Lainfix *V2ainfix +V1ainfix +V1V2Lainfix +ainfix *V1V1ainfix *V2V2ainfix =apoweramk tc1c1c1c0V0amk tainfix +V5V6V6V6V5Lainfix +ainfix *ainfix +V1V2ainfix +V1V2ainfix *V2V2Lainfix *V2ainfix +V1ainfix +V1V2Iainfix =apoweramk tc1c1c1c0adivV0c2amk tainfix +V1V2V2V2V1FIainfix &gt;=adivV0c2c0Aainfix &lt;adivV0c2V0Aainfix &lt;=c0V0Iainfix =V0c0NIainfix &gt;=V0c0F">
......@@ -280,16 +292,16 @@
edited="fibonacci_WP_FibonacciLogarithmic_WP_parameter_logfib_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.63"/>
<result status="valid" time="0.62"/>
</proof>
</goal>
</transf>
</goal>
<goal
name="fib_m"
locfile="programs/fibonacci/../fibonacci.mlw"
locfile="examples/programs/fibonacci/../fibonacci.mlw"
loclnum="105" loccnumb="8" loccnume="13"
sum="fd37af65ffa9767da0fcdec0b4771adf"
sum="e8605b6494a93cb6a637cf1c1f211395"
proved="true"