From 5d63c35e53e14adf02d8c28048be7157bebe16f4 Mon Sep 17 00:00:00 2001 From: Claude Marche <Claude.Marche@inria.fr> Date: Mon, 18 Jun 2012 23:13:00 +0200 Subject: [PATCH] update sessions --- examples/hoare_logic/wp2/why3session.xml | 144 +++++++++--------- examples/hoare_logic/wp_total/why3session.xml | 76 ++++----- examples/programs/my_cosine/why3session.xml | 54 ++----- 3 files changed, 121 insertions(+), 153 deletions(-) diff --git a/examples/hoare_logic/wp2/why3session.xml b/examples/hoare_logic/wp2/why3session.xml index a7b654b7c6..f4ea8aab48 100644 --- a/examples/hoare_logic/wp2/why3session.xml +++ b/examples/hoare_logic/wp2/why3session.xml @@ -1,5 +1,5 @@ <?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/wp2/why3session.xml"> <prover @@ -17,7 +17,7 @@ <prover id="3" name="Coq" - version="8.3pl3"/> + version="8.3pl4"/> <prover id="4" name="Z3" @@ -51,7 +51,7 @@ edited="wp2_Imp_eval_subst_term_1.v" obsolete="false" archived="false"> - <result status="valid" time="0.95"/> + <result status="valid" time="0.50"/> </proof> </goal> <goal @@ -69,7 +69,7 @@ edited="wp2_Imp_eval_term_change_free_1.v" obsolete="false" archived="false"> - <result status="valid" time="0.92"/> + <result status="valid" time="0.48"/> </proof> </goal> <goal @@ -87,7 +87,7 @@ edited="wp2_Imp_eval_subst_1.v" obsolete="false" archived="false"> - <result status="valid" time="1.06"/> + <result status="valid" time="0.56"/> </proof> </goal> <goal @@ -104,7 +104,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.03"/> + <result status="valid" time="0.02"/> </proof> <proof prover="2" @@ -112,7 +112,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.03"/> + <result status="valid" time="0.02"/> </proof> </goal> <goal @@ -130,7 +130,7 @@ edited="wp2_Imp_eval_change_free_1.v" obsolete="false" archived="false"> - <result status="valid" time="1.04"/> + <result status="valid" time="0.53"/> </proof> </goal> <goal @@ -147,7 +147,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.01"/> + <result status="valid" time="0.00"/> </proof> <proof prover="1" @@ -155,7 +155,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.04"/> + <result status="valid" time="0.02"/> </proof> <proof prover="0" @@ -171,7 +171,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.04"/> + <result status="valid" time="0.02"/> </proof> <proof prover="5" @@ -197,7 +197,7 @@ edited="wp2_Imp_steps_non_neg_1.v" obsolete="false" archived="false"> - <result status="valid" time="0.98"/> + <result status="valid" time="0.47"/> </proof> </goal> <goal @@ -215,7 +215,7 @@ edited="wp2_Imp_many_steps_seq_1.v" obsolete="false" archived="false"> - <result status="valid" time="1.20"/> + <result status="valid" time="0.63"/> </proof> </goal> </theory> @@ -239,7 +239,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="valid" time="0.05"/> + <result status="valid" time="0.03"/> </proof> <proof prover="0" @@ -255,7 +255,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="valid" time="0.06"/> + <result status="valid" time="0.03"/> </proof> </goal> <goal @@ -272,7 +272,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="valid" time="0.05"/> + <result status="valid" time="0.03"/> </proof> <proof prover="0" @@ -280,7 +280,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="valid" time="0.04"/> + <result status="valid" time="0.02"/> </proof> <proof prover="2" @@ -288,7 +288,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="valid" time="0.06"/> + <result status="valid" time="0.03"/> </proof> </goal> <goal @@ -305,7 +305,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="valid" time="0.05"/> + <result status="valid" time="0.03"/> </proof> <proof prover="0" @@ -313,7 +313,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="valid" time="0.03"/> + <result status="valid" time="0.02"/> </proof> <proof prover="2" @@ -321,7 +321,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="valid" time="0.06"/> + <result status="valid" time="0.03"/> </proof> </goal> <goal @@ -339,7 +339,7 @@ edited="wp2_TestSemantics_Test55_1.v" obsolete="false" archived="false"> - <result status="valid" time="0.90"/> + <result status="valid" time="0.47"/> </proof> </goal> <goal @@ -356,7 +356,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="valid" time="0.11"/> + <result status="valid" time="0.06"/> </proof> <proof prover="0" @@ -364,7 +364,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="valid" time="0.09"/> + <result status="valid" time="0.06"/> </proof> <proof prover="2" @@ -372,7 +372,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="valid" time="0.12"/> + <result status="valid" time="0.06"/> </proof> </goal> <goal @@ -390,7 +390,7 @@ edited="wp2_TestSemantics_If42_1.v" obsolete="false" archived="false"> - <result status="valid" time="2.25"/> + <result status="valid" time="1.18"/> </proof> </goal> </theory> @@ -410,11 +410,11 @@ shape="avalid_tripleV1V4V3Iavalid_fmlaaFimpliesV2V3Iavalid_tripleV0V4V2Iavalid_fmlaaFimpliesV1V0F"> <proof prover="4" - timelimit="9" + timelimit="10" memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="4.68"/> + <result status="valid" time="2.45"/> </proof> <proof prover="5" @@ -422,7 +422,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="1.37"/> + <result status="valid" time="0.76"/> </proof> </goal> <goal @@ -440,7 +440,7 @@ edited="wp2_HoareLogic_skip_rule_1.v" obsolete="false" archived="false"> - <result status="valid" time="1.01"/> + <result status="valid" time="0.55"/> </proof> </goal> <goal @@ -458,7 +458,7 @@ edited="wp2_HoareLogic_assign_rule_1.v" obsolete="false" archived="false"> - <result status="valid" time="1.12"/> + <result status="valid" time="0.58"/> </proof> </goal> <goal @@ -471,11 +471,11 @@ shape="avalid_tripleV0aSseqV3V4V1Iavalid_tripleV2V4V1Aavalid_tripleV0V3V2F"> <proof prover="4" - timelimit="4" + timelimit="5" memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="2.06"/> + <result status="valid" time="1.08"/> </proof> <proof prover="5" @@ -483,7 +483,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.70"/> + <result status="valid" time="0.41"/> </proof> </goal> <goal @@ -501,7 +501,7 @@ edited="wp2_HoareLogic_if_rule_1.v" obsolete="false" archived="false"> - <result status="valid" time="1.22"/> + <result status="valid" time="0.60"/> </proof> </goal> <goal @@ -519,7 +519,7 @@ edited="wp2_HoareLogic_assert_rule_1.v" obsolete="false" archived="false"> - <result status="valid" time="1.12"/> + <result status="valid" time="0.61"/> </proof> </goal> <goal @@ -537,7 +537,7 @@ edited="wp2_HoareLogic_assert_rule_ext_1.v" obsolete="false" archived="false"> - <result status="valid" time="1.16"/> + <result status="valid" time="0.61"/> </proof> </goal> <goal @@ -555,7 +555,7 @@ edited="wp2_HoareLogic_while_rule_1.v" obsolete="false" archived="false"> - <result status="valid" time="1.39"/> + <result status="valid" time="0.73"/> </proof> </goal> <goal @@ -573,7 +573,7 @@ edited="wp2_HoareLogic_while_rule_ext_1.v" obsolete="false" archived="false"> - <result status="valid" time="1.32"/> + <result status="valid" time="0.72"/> </proof> </goal> </theory> @@ -597,7 +597,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.03"/> + <result status="valid" time="0.01"/> </proof> </goal> <goal @@ -614,7 +614,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.03"/> + <result status="valid" time="0.02"/> </proof> </goal> <goal @@ -631,7 +631,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.03"/> + <result status="valid" time="0.02"/> </proof> </goal> <goal @@ -648,7 +648,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.04"/> + <result status="valid" time="0.02"/> </proof> </goal> <goal @@ -683,7 +683,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.59"/> + <result status="valid" time="0.38"/> </proof> </goal> <goal @@ -704,7 +704,7 @@ edited="wp2_WP_WP_WP_parameter_compute_writes_1.v" obsolete="false" archived="false"> - <result status="valid" time="1.15"/> + <result status="valid" time="0.65"/> </proof> </goal> <goal @@ -720,11 +720,11 @@ name="expl:parameter compute_writes"/> <proof prover="4" - timelimit="3" + timelimit="5" memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="2.17"/> + <result status="valid" time="1.37"/> </proof> <proof prover="5" @@ -732,7 +732,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.70"/> + <result status="valid" time="0.40"/> </proof> </goal> <goal @@ -753,7 +753,7 @@ edited="wp2_WP_WP_WP_parameter_compute_writes_3.v" obsolete="false" archived="false"> - <result status="valid" time="1.13"/> + <result status="valid" time="0.60"/> </proof> </goal> <goal @@ -774,7 +774,7 @@ edited="wp2_WP_WP_WP_parameter_compute_writes_4.v" obsolete="false" archived="false"> - <result status="valid" time="1.27"/> + <result status="valid" time="0.65"/> </proof> </goal> <goal @@ -795,7 +795,7 @@ edited="wp2_WP_WP_WP_parameter_compute_writes_2.v" obsolete="false" archived="false"> - <result status="valid" time="1.12"/> + <result status="valid" time="0.60"/> </proof> </goal> </transf> @@ -832,7 +832,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.02"/> + <result status="valid" time="0.01"/> </proof> <proof prover="1" @@ -840,7 +840,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.05"/> + <result status="valid" time="0.03"/> </proof> <proof prover="0" @@ -848,7 +848,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.03"/> + <result status="valid" time="0.02"/> </proof> <proof prover="2" @@ -856,7 +856,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.06"/> + <result status="valid" time="0.03"/> </proof> <proof prover="5" @@ -884,7 +884,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.08"/> + <result status="valid" time="0.04"/> </proof> <proof prover="1" @@ -892,7 +892,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.06"/> + <result status="valid" time="0.04"/> </proof> <proof prover="0" @@ -900,7 +900,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.05"/> + <result status="valid" time="0.02"/> </proof> <proof prover="2" @@ -908,7 +908,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.08"/> + <result status="valid" time="0.04"/> </proof> <proof prover="5" @@ -916,7 +916,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.15"/> + <result status="valid" time="0.10"/> </proof> </goal> <goal @@ -936,7 +936,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.07"/> + <result status="valid" time="0.04"/> </proof> <proof prover="1" @@ -944,7 +944,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.06"/> + <result status="valid" time="0.04"/> </proof> <proof prover="0" @@ -952,7 +952,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.04"/> + <result status="valid" time="0.02"/> </proof> <proof prover="2" @@ -960,7 +960,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.07"/> + <result status="valid" time="0.04"/> </proof> <proof prover="5" @@ -968,7 +968,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.17"/> + <result status="valid" time="0.10"/> </proof> </goal> <goal @@ -989,7 +989,7 @@ edited="wp2_WP_WP_WP_parameter_wp_1.v" obsolete="false" archived="false"> - <result status="valid" time="0.99"/> + <result status="valid" time="0.51"/> </proof> </goal> <goal @@ -1009,7 +1009,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.07"/> + <result status="valid" time="0.04"/> </proof> <proof prover="1" @@ -1017,7 +1017,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.06"/> + <result status="valid" time="0.03"/> </proof> <proof prover="0" @@ -1025,7 +1025,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.03"/> + <result status="valid" time="0.02"/> </proof> <proof prover="2" @@ -1033,7 +1033,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.07"/> + <result status="valid" time="0.04"/> </proof> <proof prover="5" @@ -1041,7 +1041,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.16"/> + <result status="valid" time="0.11"/> </proof> </goal> <goal @@ -1062,7 +1062,7 @@ edited="wp2_WP_WP_WP_parameter_wp_2.v" obsolete="false" archived="false"> - <result status="valid" time="1.21"/> + <result status="valid" time="0.68"/> </proof> </goal> </transf> diff --git a/examples/hoare_logic/wp_total/why3session.xml b/examples/hoare_logic/wp_total/why3session.xml index 7d27419e2a..3dd6f31c2d 100644 --- a/examples/hoare_logic/wp_total/why3session.xml +++ b/examples/hoare_logic/wp_total/why3session.xml @@ -1,5 +1,5 @@ <?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" diff --git a/examples/programs/my_cosine/why3session.xml b/examples/programs/my_cosine/why3session.xml index 90eff03052..5f6651b478 100644 --- a/examples/programs/my_cosine/why3session.xml +++ b/examples/programs/my_cosine/why3session.xml @@ -1,15 +1,11 @@ <?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 <=.aabsainfix -.avalueV5acosavalueV0c0x1.p-23Iainfix =avalueV5aroundaNearestTiesToEvenainfix -.avalueV1avalueV4FAainfix <=aabsaroundaNearestTiesToEvenainfix -.avalueV1avalueV4amax_singleIainfix =avalueV4aroundaNearestTiesToEvenainfix *.avalueV2avalueV3FAainfix <=aabsaroundaNearestTiesToEvenainfix *.avalueV2avalueV3amax_singleIainfix =avalueV3c0.5FIainfix =avalueV2aroundaNearestTiesToEvenainfix *.avalueV0avalueV0FAainfix <=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FAainfix <=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix <=.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 <=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix <=.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 <=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FIainfix <=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix <=.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 <=aabsaroundaNearestTiesToEvenainfix *.avalueV2avalueV3amax_singleIainfix =avalueV3c0.5FIainfix =avalueV2aroundaNearestTiesToEvenainfix *.avalueV0avalueV0FIainfix <=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FIainfix <=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix <=.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 <=aabsaroundaNearestTiesToEvenainfix -.avalueV1avalueV4amax_singleIainfix =avalueV4aroundaNearestTiesToEvenainfix *.avalueV2avalueV3FIainfix <=aabsaroundaNearestTiesToEvenainfix *.avalueV2avalueV3amax_singleIainfix =avalueV3c0.5FIainfix =avalueV2aroundaNearestTiesToEvenainfix *.avalueV0avalueV0FIainfix <=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FIainfix <=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix <=.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 <=.aabsainfix -.avalueV5acosavalueV0c0x1.p-23Iainfix =avalueV5aroundaNearestTiesToEvenainfix -.avalueV1avalueV4FIainfix <=aabsaroundaNearestTiesToEvenainfix -.avalueV1avalueV4amax_singleIainfix =avalueV4aroundaNearestTiesToEvenainfix *.avalueV2avalueV3FIainfix <=aabsaroundaNearestTiesToEvenainfix *.avalueV2avalueV3amax_singleIainfix =avalueV3c0.5FIainfix =avalueV2aroundaNearestTiesToEvenainfix *.avalueV0avalueV0FIainfix <=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FIainfix <=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix <=.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> -- GitLab