Skip to content

why3
why3
Commit 5d63c35e authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

update sessions

parent 6ce2052c
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 121 additions and 153 deletions
examples/hoare_logic/wp2/why3session.xml
View file @ 5d63c35e
This diff is collapsed.
examples/hoare_logic/wp_total/why3session.xml
View file @ 5d63c35e
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/cmarche/recherche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="hoare_logic/wp_total/why3session.xml">
<prover
......@@ -13,7 +13,7 @@
<prover
id="2"
name="Coq"
version="8.3pl3"/>
version="8.3pl4"/>
<prover
id="3"
name="Z3"
......@@ -42,7 +42,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
......@@ -76,7 +76,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
......@@ -84,7 +84,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="0"
......@@ -92,7 +92,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
......@@ -110,7 +110,7 @@
edited="wp_total_Imp_Test55_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.91"/>
<result status="valid" time="0.46"/>
</proof>
</goal>
<goal
......@@ -128,7 +128,7 @@
edited="wp_total_Imp_eval_subst_term_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.95"/>
<result status="valid" time="0.48"/>
</proof>
</goal>
<goal
......@@ -146,7 +146,7 @@
edited="wp_total_Imp_eval_subst_2.v"
obsolete="false"
archived="false">
<result status="unknown" time="0.95"/>
<result status="unknown" time="0.50"/>
</proof>
</goal>
<goal
......@@ -163,7 +163,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
......@@ -180,7 +180,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.15"/>
<result status="valid" time="0.09"/>
</proof>
</goal>
<goal
......@@ -198,7 +198,7 @@
edited="wp_total_Imp_If42_1.v"
obsolete="false"
archived="false">
<result status="valid" time="1.16"/>
<result status="valid" time="0.62"/>
</proof>
</goal>
<goal
......@@ -216,7 +216,7 @@
edited="wp_total_Imp_steps_non_neg_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.94"/>
<result status="valid" time="0.45"/>
</proof>
</goal>
<goal
......@@ -234,7 +234,7 @@
edited="wp_total_Imp_many_steps_seq_1.v"
obsolete="false"
archived="false">
<result status="valid" time="1.08"/>
<result status="valid" time="0.58"/>
</proof>
</goal>
<goal
......@@ -247,11 +247,11 @@
shape="avalid_tripleV0aSskipV0F">
<proof
prover="0"
timelimit="5"
timelimit="6"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="2.69"/>
<result status="valid" time="1.65"/>
</proof>
</goal>
<goal
......@@ -269,7 +269,7 @@
edited="wp_total_Imp_assign_rule_1.v"
obsolete="false"
archived="false">
<result status="valid" time="1.01"/>
<result status="valid" time="0.57"/>
</proof>
</goal>
<goal
......@@ -286,7 +286,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.07"/>
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal
......@@ -304,7 +304,7 @@
edited="wp_total_Imp_if_rule_1.v"
obsolete="false"
archived="false">
<result status="valid" time="1.08"/>
<result status="valid" time="0.57"/>
</proof>
</goal>
<goal
......@@ -322,7 +322,7 @@
edited="wp_total_Imp_assert_rule_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.96"/>
<result status="valid" time="0.55"/>
</proof>
</goal>
<goal
......@@ -340,7 +340,7 @@
edited="wp_total_Imp_assert_rule_ext_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.99"/>
<result status="valid" time="0.53"/>
</proof>
</goal>
<goal
......@@ -358,7 +358,7 @@
edited="wp_total_Imp_while_rule_1.v"
obsolete="false"
archived="false">
<result status="valid" time="1.22"/>
<result status="valid" time="0.65"/>
</proof>
</goal>
<goal
......@@ -376,7 +376,7 @@
edited="wp_total_Imp_while_rule_ext_1.v"
obsolete="false"
archived="false">
<result status="valid" time="1.19"/>
<result status="valid" time="0.66"/>
</proof>
</goal>
<goal
......@@ -393,7 +393,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.10"/>
<result status="valid" time="0.05"/>
</proof>
<proof
prover="1"
......@@ -401,7 +401,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="1.21"/>
<result status="valid" time="0.66"/>
</proof>
</goal>
</theory>
......@@ -429,7 +429,7 @@
edited="wp_total_WP_WP_WP_parameter_wp_2.v"
obsolete="false"
archived="false">
<result status="unknown" time="0.93"/>
<result status="unknown" time="0.52"/>
</proof>
<transf
name="split_goal"
......@@ -452,7 +452,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
......@@ -472,7 +472,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
......@@ -492,7 +492,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
......@@ -512,7 +512,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.92"/>
<result status="valid" time="0.53"/>
</proof>
<proof
prover="1"
......@@ -520,7 +520,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="5.12"/>
<result status="timeout" time="5.02"/>
</proof>
<proof
prover="0"
......@@ -528,7 +528,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="5.24"/>
<result status="timeout" time="5.02"/>
</proof>
</goal>
<goal
......@@ -548,7 +548,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="1"
......@@ -556,7 +556,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="0"
......@@ -564,7 +564,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="2"
......@@ -573,7 +573,7 @@
edited="wp_total_WP_WP_WP_parameter_wp_3.v"
obsolete="false"
archived="false">
<result status="unknown" time="0.92"/>
<result status="unknown" time="0.48"/>
</proof>
</goal>
<goal
......@@ -593,7 +593,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="5.37"/>
<result status="timeout" time="5.01"/>
</proof>
<proof
prover="1"
......@@ -601,7 +601,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="5.06"/>
<result status="timeout" time="5.11"/>
</proof>
<proof
prover="0"
......
examples/programs/my_cosine/why3session.xml
View file @ 5d63c35e
<?xml version="1.0" encoding="UTF-8"?>
<<<<<<< HEAD
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
=======
<!DOCTYPE why3session SYSTEM "/home/cmarche/recherche/why3/share/why3session.dtd">
>>>>>>> More lemmas on floats
<why3session
name="programs/my_cosine/why3session.xml">
name="examples/programs/my_cosine/why3session.xml">
<prover
id="0"
name="Coq"
version="8.3pl3"/>
version="8.3pl4"/>
<prover
id="1"
name="Gappa"
......@@ -20,20 +16,16 @@
expanded="true">
<theory
name="WP M"
locfile="programs/my_cosine/../my_cosine.mlw"
locfile="examples/programs/my_cosine/../my_cosine.mlw"
loclnum="1" loccnumb="7" loccnume="8"
verified="true"
expanded="true">
<goal
name="WP_parameter my_cosine"
locfile="programs/my_cosine/../my_cosine.mlw"
locfile="examples/programs/my_cosine/../my_cosine.mlw"
loclnum="30" loccnumb="4" loccnume="13"
expl="parameter my_cosine"
<<<<<<< HEAD
sum="43a387020a8494975293041bea91d995"
=======
sum="e18349ec1631d3a17eea4de5481cd8cc"
>>>>>>> More lemmas on floats
proved="true"
expanded="true"
shape="ainfix &lt;=.aabsainfix -.avalueV5acosavalueV0c0x1.p-23Iainfix =avalueV5aroundaNearestTiesToEvenainfix -.avalueV1avalueV4FAainfix &lt;=aabsaroundaNearestTiesToEvenainfix -.avalueV1avalueV4amax_singleIainfix =avalueV4aroundaNearestTiesToEvenainfix *.avalueV2avalueV3FAainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV2avalueV3amax_singleIainfix =avalueV3c0.5FIainfix =avalueV2aroundaNearestTiesToEvenainfix *.avalueV0avalueV0FAainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FAainfix &lt;=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix &lt;=.aabsavalueV0c0x1.p-5F">
......@@ -45,14 +37,10 @@
expanded="true">
<goal
name="WP_parameter my_cosine.1"
locfile="programs/my_cosine/../my_cosine.mlw"
locfile="examples/programs/my_cosine/../my_cosine.mlw"
loclnum="30" loccnumb="4" loccnume="13"
expl="assertion"
<<<<<<< HEAD
sum="1847af31ffb0fc79bb3f99eb48677194"
=======
sum="29cbc2fa0e49fc55e087329496e2da77"
>>>>>>> More lemmas on floats
proved="true"
expanded="true"
shape="ainfix &lt;=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix &lt;=.aabsavalueV0c0x1.p-5F">
......@@ -65,23 +53,15 @@
edited="my_cosine_M_WP_parameter_my_cosine_1.v"
obsolete="false"
archived="false">
<<<<<<< HEAD
<result status="valid" time="3.58"/>
=======
<result status="valid" time="5.82"/>
>>>>>>> More lemmas on floats
</proof>
</goal>
<goal
name="WP_parameter my_cosine.2"
locfile="programs/my_cosine/../my_cosine.mlw"
locfile="examples/programs/my_cosine/../my_cosine.mlw"
loclnum="30" loccnumb="4" loccnume="13"
expl="precondition"
<<<<<<< HEAD
sum="ed7fd59f8e3662b57ab5ff723e124166"
=======
sum="d0aced220a37d7b4dddd73141f910e24"
>>>>>>> More lemmas on floats
proved="true"
expanded="true"
shape="ainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FIainfix &lt;=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix &lt;=.aabsavalueV0c0x1.p-5F">
......@@ -98,14 +78,10 @@
</goal>
<goal
name="WP_parameter my_cosine.3"
locfile="programs/my_cosine/../my_cosine.mlw"
locfile="examples/programs/my_cosine/../my_cosine.mlw"
loclnum="30" loccnumb="4" loccnume="13"
expl="precondition"
<<<<<<< HEAD
sum="01c28821422107c03234edd2f723d53e"
=======
sum="02beb0cc288ba7cba469f3db5e3fd908"
>>>>>>> More lemmas on floats
proved="true"
expanded="true"
shape="ainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV2avalueV3amax_singleIainfix =avalueV3c0.5FIainfix =avalueV2aroundaNearestTiesToEvenainfix *.avalueV0avalueV0FIainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FIainfix &lt;=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix &lt;=.aabsavalueV0c0x1.p-5F">
......@@ -122,14 +98,10 @@
</goal>
<goal
name="WP_parameter my_cosine.4"
locfile="programs/my_cosine/../my_cosine.mlw"
locfile="examples/programs/my_cosine/../my_cosine.mlw"
loclnum="30" loccnumb="4" loccnume="13"
expl="precondition"
<<<<<<< HEAD
sum="d30950e1e41f800ca0172d07dda83ad4"
=======
sum="60fab8199ea5cc9a793f777f2fdb559e"
>>>>>>> More lemmas on floats
proved="true"
expanded="true"
shape="ainfix &lt;=aabsaroundaNearestTiesToEvenainfix -.avalueV1avalueV4amax_singleIainfix =avalueV4aroundaNearestTiesToEvenainfix *.avalueV2avalueV3FIainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV2avalueV3amax_singleIainfix =avalueV3c0.5FIainfix =avalueV2aroundaNearestTiesToEvenainfix *.avalueV0avalueV0FIainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FIainfix &lt;=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix &lt;=.aabsavalueV0c0x1.p-5F">
......@@ -141,19 +113,15 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter my_cosine.5"
locfile="programs/my_cosine/../my_cosine.mlw"
locfile="examples/programs/my_cosine/../my_cosine.mlw"
loclnum="30" loccnumb="4" loccnume="13"
expl="normal postcondition"
<<<<<<< HEAD
sum="2eafda4f7656e405bda4587b4c59ab3c"
=======
sum="a0176bc5d22c4a84606639fb3a5ee329"
>>>>>>> More lemmas on floats
proved="true"
expanded="true"
shape="ainfix &lt;=.aabsainfix -.avalueV5acosavalueV0c0x1.p-23Iainfix =avalueV5aroundaNearestTiesToEvenainfix -.avalueV1avalueV4FIainfix &lt;=aabsaroundaNearestTiesToEvenainfix -.avalueV1avalueV4amax_singleIainfix =avalueV4aroundaNearestTiesToEvenainfix *.avalueV2avalueV3FIainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV2avalueV3amax_singleIainfix =avalueV3c0.5FIainfix =avalueV2aroundaNearestTiesToEvenainfix *.avalueV0avalueV0FIainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FIainfix &lt;=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix &lt;=.aabsavalueV0c0x1.p-5F">
......@@ -165,7 +133,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</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