diff --git a/examples/hoare_logic/blocking_semantics/why3session.xml b/examples/hoare_logic/blocking_semantics/why3session.xml deleted file mode 100644 index 8babd651ef24bab06f6b5b0eb90cc7012e688103..0000000000000000000000000000000000000000 --- a/examples/hoare_logic/blocking_semantics/why3session.xml +++ /dev/null @@ -1,858 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd"> -<why3session - name="hoare_logic/blocking_semantics/why3session.xml" shape_version="2"> - <prover - id="0" - name="Alt-Ergo" - version="0.94"/> - <prover - id="1" - name="CVC3" - version="2.2"/> - <prover - id="2" - name="CVC3" - version="2.4.1"/> - <prover - id="3" - name="Coq" - version="8.3pl4"/> - <prover - id="4" - name="Z3" - version="2.19"/> - <prover - id="5" - name="Z3" - version="3.2"/> - <file - name="../blocking_semantics.mlw" - verified="false" - expanded="true"> - <theory - name="ImpExpr" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="6" loccnumb="7" loccnume="14" - verified="false" - expanded="false"> - <goal - name="get_stack_eq" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="51" loccnumb="6" loccnume="18" - sum="2054c78e942347bdfcb126bba8c86eb2" - proved="true" - expanded="false" - shape="ainfix =aget_stackV0aConsaTuple2V0V1V2V1F"> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="valid" time="0.01"/> - </proof> - </goal> - <goal - name="get_stack_neq" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="55" loccnumb="6" loccnume="19" - sum="291b4b08997d46940896a5c9d708fc53" - proved="true" - expanded="false" - shape="ainfix =aget_stackV1aConsaTuple2V0V2V3aget_stackV1V3Iainfix =V0V1NF"> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="valid" time="0.01"/> - </proof> - </goal> - <goal - name="eval_subst_term" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="117" loccnumb="6" loccnume="21" - sum="b401377b2ae52264e6ca10b621796d93" - proved="false" - expanded="false" - shape="ainfix =aeval_termV0V1asubst_termV2V3V4aeval_termasetV0V3aget_stackV4V1V1V2Iafresh_in_termV4V2F"> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="unknown" time="0.16"/> - </proof> - </goal> - <goal - name="eval_term_change_free" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="123" loccnumb="6" loccnume="27" - sum="82ff2a97a985b592800a976e73a31ffd" - proved="false" - expanded="false" - shape="ainfix =aeval_termV1aConsaTuple2V3V4V2V0aeval_termV1V2V0Iafresh_in_termV3V0F"> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="unknown" time="1.58"/> - </proof> - </goal> - <goal - name="subst_fresh" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="148" loccnumb="6" loccnume="17" - sum="19bdd34cd7fb60cdf86f3b51bf7c7e3a" - proved="false" - expanded="false" - shape="ainfix =asubstV0V1V2V0Iafresh_in_fmlaV1V0F"> - </goal> - <goal - name="let_subst" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="152" loccnumb="6" loccnume="15" - sum="325f8c907c803c20c53fe7908fe57a4f" - proved="true" - expanded="false" - shape="ainfix =asubstaFletV2V0V1V3V4aFletV2asubst_termV0V3V4asubstV1V3V4F"> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="valid" time="0.01"/> - </proof> - </goal> - <goal - name="eval_subst" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="156" loccnumb="6" loccnume="16" - sum="d8f0d33e085baa6ce6fac7b7a4f5451c" - proved="false" - expanded="false" - shape="aeval_fmlaasetV1V3aget_stackV4V2V2V0qaeval_fmlaV1V2asubstV0V3V4Iafresh_in_fmlaV4V0F"> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="unknown" time="0.09"/> - </proof> - </goal> - <goal - name="eval_swap" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="162" loccnumb="6" loccnume="15" - sum="64d2921eec6182742e950abcdafaa527" - proved="false" - expanded="false" - shape="aeval_fmlaV1aConsaTuple2V4V6aConsaTuple2V3V5V2V0qaeval_fmlaV1aConsaTuple2V3V5aConsaTuple2V4V6V2V0Iainfix =V3V4NF"> - <proof - prover="0" - timelimit="10" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="unknown" time="4.50"/> - </proof> - </goal> - <goal - name="eval_change_free" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="168" loccnumb="6" loccnume="22" - sum="3ef8329f134e003f2ab6a1033e953662" - proved="false" - expanded="false" - shape="aeval_fmlaV1V2V0qaeval_fmlaV1aConsaTuple2V3V4V2V0Iafresh_in_fmlaV3V0F"> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="unknown" time="1.41"/> - </proof> - </goal> - <goal - name="let_equiv" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="177" loccnumb="6" loccnume="15" - sum="4d79524d1fca6afe1244220502090934" - proved="false" - expanded="false" - shape="aeval_fmlaV4V5aFletV0V2V3Iaeval_fmlaV4V5aFletV1V2asubstV3V0V1FF"> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.01"/> - </proof> - </goal> - <goal - name="steps_non_neg" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="307" loccnumb="8" loccnume="21" - sum="f8b67cf92b6a1a36b89db6aaa4c9775b" - proved="false" - expanded="false" - shape="ainfix >=V6c0Iamany_stepsV0V2V4V1V3V5V6F"> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.01"/> - </proof> - </goal> - <goal - name="many_steps_seq" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="311" loccnumb="8" loccnume="22" - sum="189a69d852a6dc40ebfa8cb09267024e" - proved="false" - expanded="false" - shape="ainfix =V6ainfix +ainfix +c1V9V10Aamany_stepsV7V8V5V1V3avoidV10Aamany_stepsV0V2V4V7V8avoidV9EIamany_stepsV0V2aEseqV4V5V1V3avoidV6F"> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.02"/> - </proof> - </goal> - <goal - name="many_steps_let" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="319" loccnumb="8" loccnume="22" - sum="826c2947596a798beb870ef959bdfe2f" - proved="false" - expanded="false" - shape="ainfix =V8ainfix +ainfix +c1V12V13Aamany_stepsV9aConsaTuple2V4V11V10V6V1V3aEvalueV7V13Aamany_stepsV0V2V5V9V10aEvalueV11V12EIamany_stepsV0V2aEletV4V5V6V1V3aEvalueV7V8F"> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.02"/> - </proof> - </goal> - <goal - name="one_step_change_free" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="327" loccnumb="7" loccnume="27" - sum="f46cba627287468a8a595f3019ebe95b" - proved="false" - expanded="false" - shape="aone_stepV2V4V0V3V5V1Iaone_stepV2aConsaTuple2V6V7V4V0V3V5V1Iafresh_in_exprV6V0F"> - </goal> - </theory> - <theory - name="TestSemantics" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="354" loccnumb="7" loccnume="20" - verified="false" - expanded="false"> - <goal - name="Test13" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="362" loccnumb="5" loccnume="11" - sum="195bd113d8822c94293d192b87fcf4ec" - proved="true" - expanded="false" - shape="ainfix =aeval_termamy_sigmaamy_piaTvalueaVintc13aVintc13"> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="valid" time="0.03"/> - </proof> - </goal> - <goal - name="Test13expr" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="365" loccnumb="5" loccnume="15" - sum="aaf0be282e72c670579aa80848562bc7" - proved="true" - expanded="false" - shape="amany_stepsamy_sigmaamy_piaEvalueaVintc13amy_sigmaamy_piaEvalueaVintc13c0"> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="valid" time="0.03"/> - </proof> - </goal> - <goal - name="Test42" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="368" loccnumb="5" loccnume="11" - sum="dd8b2977b19ef9124ac9a1ecdbf16eab" - proved="true" - expanded="false" - shape="ainfix =aeval_termamy_sigmaamy_piaTvaraxaVintc42"> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="valid" time="0.02"/> - </proof> - </goal> - <goal - name="Test42expr" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="371" loccnumb="5" loccnume="15" - sum="e3ba7dba27418993d6ce568a96a32bef" - proved="false" - expanded="false" - shape="amany_stepsamy_sigmaamy_piaEvaraxamy_sigmaamy_piaEvalueaVintc42c1"> - <proof - prover="4" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.02"/> - </proof> - <proof - prover="1" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.01"/> - </proof> - <proof - prover="0" - timelimit="10" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="unknown" time="4.77"/> - </proof> - <proof - prover="2" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.02"/> - </proof> - <proof - prover="5" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.02"/> - </proof> - </goal> - <goal - name="Test0" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="374" loccnumb="5" loccnume="10" - sum="44c3dcbfa0d7fd2523933b37881a5e93" - proved="true" - expanded="false" - shape="ainfix =aeval_termamy_sigmaamy_piaTderefaxaVintc0"> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="valid" time="0.04"/> - </proof> - </goal> - <goal - name="Test0expr" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="377" loccnumb="5" loccnume="14" - sum="d58d3160618b3701bbd15ba24d85fa37" - proved="false" - expanded="false" - shape="amany_stepsamy_sigmaamy_piaEderefaxamy_sigmaamy_piaEvalueaVintc0c1"> - <proof - prover="4" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.12"/> - </proof> - <proof - prover="1" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.02"/> - </proof> - <proof - prover="0" - timelimit="10" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="unknown" time="4.74"/> - </proof> - <proof - prover="2" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.01"/> - </proof> - <proof - prover="5" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.01"/> - </proof> - </goal> - <goal - name="Test55" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="380" loccnumb="5" loccnume="11" - sum="2f43cea369b8f22c835b0768de360912" - proved="false" - expanded="false" - shape="ainfix =aeval_termamy_sigmaamy_piaTbinaTvaraxaOplusaTvalueaVintc13aVintc55"> - <proof - prover="4" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.01"/> - </proof> - <proof - prover="1" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.01"/> - </proof> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.01"/> - </proof> - <proof - prover="2" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.01"/> - </proof> - <proof - prover="5" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.01"/> - </proof> - </goal> - <goal - name="Test55expr" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="383" loccnumb="5" loccnume="15" - sum="e1716581728240a91b4ffe73b507c6e9" - proved="false" - expanded="false" - shape="amany_stepsamy_sigmaamy_piaEbinaEvaraxaOplusaEvalueaVintc13amy_sigmaamy_piaEvalueaVintc55c2"> - <proof - prover="4" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.11"/> - </proof> - <proof - prover="1" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.01"/> - </proof> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.01"/> - </proof> - <proof - prover="2" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.02"/> - </proof> - <proof - prover="5" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.02"/> - </proof> - </goal> - <goal - name="Ass42" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="386" loccnumb="5" loccnume="10" - sum="66fb03c097d237559dfd979893cd582e" - proved="true" - expanded="false" - shape="ainfix =agetV0axaVintc42Iaone_stepamy_sigmaamy_piaEassignaxaEvalueaVintc42V0V1avoidF"> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="valid" time="0.50"/> - </proof> - </goal> - <goal - name="If42" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="391" loccnumb="5" loccnume="9" - sum="68e056ca201c08240a61ec0d132b47f0" - proved="false" - expanded="false" - shape="ainfix =agetV1axaVintc13Iaone_stepV0V2V4V1V3avoidIaone_stepamy_sigmaamy_piaEifaEbinaEderefaxaOleaEvalueaVintc10aEassignaxaEvalueaVintc13aEassignaxaEvalueaVintc42V0V2V4F"> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.01"/> - </proof> - </goal> - </theory> - <theory - name="HoareLogic" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="405" loccnumb="7" loccnume="17" - verified="false" - expanded="false"> - <goal - name="consequence_rule" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="412" loccnumb="6" loccnume="22" - sum="eebb4c1c1614a6a2f9699172d99f1cc2" - proved="false" - expanded="false" - shape="avalid_tripleV1V4V3Iavalid_fmlaaFimpliesV2V3Iavalid_tripleV0V4V2Iavalid_fmlaaFimpliesV1V0F"> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.01"/> - </proof> - </goal> - <goal - name="value_rule" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="419" loccnumb="6" loccnume="16" - sum="3711be7f6d551e8ad03fb8b3a59d7d52" - proved="true" - expanded="false" - shape="avalid_tripleV0aEvalueV1V0Iafresh_in_fmlaaresultV0F"> - <proof - prover="0" - timelimit="20" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="valid" time="9.94"/> - </proof> - </goal> - <goal - name="assign_rule" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="423" loccnumb="6" loccnume="17" - sum="0211a1d5814b370558009368996ad45f" - proved="false" - expanded="false" - shape="avalid_tripleV0aEassignV2V3V1Iavalid_tripleV0V3asubstV1V2aresultF"> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.01"/> - </proof> - </goal> - <goal - name="seq_rule" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="428" loccnumb="6" loccnume="14" - sum="65bdedaeb23dd6b3fe289d1d371e04a7" - proved="false" - expanded="false" - shape="avalid_tripleV0aEseqV3V4V1Iavalid_tripleV2V4V1Aavalid_tripleV0V3V2F"> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.01"/> - </proof> - </goal> - <goal - name="let_rule" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="433" loccnumb="6" loccnume="14" - sum="5fecb27a5574656aba48572dbd3af266" - proved="false" - expanded="false" - shape="avalid_tripleV0aEletV3V4V5V1Iavalid_tripleaFletaresultaTvarV3V2V5V1Aavalid_tripleV0V4V2Iafresh_in_fmlaV3V2Iainfix =V3aresultNF"> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.01"/> - </proof> - </goal> - <goal - name="assert_rule" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="447" loccnumb="6" loccnume="17" - sum="e1fcd3566753351574acdf5f8444ebe1" - proved="false" - expanded="false" - shape="avalid_tripleV1aEassertV0V1Iavalid_fmlaaFimpliesV1V0F"> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.02"/> - </proof> - </goal> - <goal - name="assert_rule_ext" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="451" loccnumb="6" loccnume="21" - sum="d9e939be7d3a49dcb84052c6ed74326d" - proved="false" - expanded="false" - shape="avalid_tripleaFimpliesV0V1aEassertV0V1F"> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="timeout" time="5.02"/> - </proof> - </goal> - </theory> - <theory - name="WP" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="474" loccnumb="7" loccnume="9" - verified="false" - expanded="true"> - <goal - name="assigns_refl" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="487" loccnumb="6" loccnume="18" - sum="207b728f8e24b65cfdf8155d73ac7f24" - proved="true" - expanded="false" - shape="aassignsV0V1V0F"> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="valid" time="0.02"/> - </proof> - </goal> - <goal - name="assigns_trans" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="490" loccnumb="6" loccnume="19" - sum="1b5d0a35d5321935c26f7b6d6da5bcef" - proved="true" - expanded="false" - shape="aassignsV0V3V2IaassignsV1V3V2AaassignsV0V3V1F"> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="valid" time="0.03"/> - </proof> - </goal> - <goal - name="assigns_union_left" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="495" loccnumb="6" loccnume="24" - sum="ab97a79a4547f31f351fc9572a7ade02" - proved="true" - expanded="false" - shape="aassignsV0aunionV2V3V1IaassignsV0V2V1F"> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="valid" time="0.03"/> - </proof> - </goal> - <goal - name="assigns_union_right" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="499" loccnumb="6" loccnume="25" - sum="ef1c986fe8a7ffd355888623cef2a3d0" - proved="true" - expanded="false" - shape="aassignsV0aunionV2V3V1IaassignsV0V3V1F"> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="valid" time="0.03"/> - </proof> - </goal> - <goal - name="wp_subst" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="563" loccnumb="8" loccnume="16" - sum="265a766a7cb0365bb47d47e77f5c319c" - proved="false" - expanded="false" - shape="ainfix =asubstawpV0V1V2V3awpV0asubstV1V2V3Iafresh_in_exprV2V0F"> - </goal> - <goal - name="wp_implies" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="568" loccnumb="8" loccnume="18" - sum="092a912cf70664d783c8c0837fa769a3" - proved="false" - expanded="false" - shape="aeval_fmlaV2V3awpV4V1Iaeval_fmlaV2V3awpV4V0FIaeval_fmlaV5V6V1Iaeval_fmlaV5V6V0FF"> - </goal> - <goal - name="wp_conj" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="577" loccnumb="8" loccnume="15" - sum="943dfa37ab963fe3c947bb1e22881337" - proved="false" - expanded="false" - shape="aeval_fmlaV0V1awpV2V4Aaeval_fmlaV0V1awpV2V3qaeval_fmlaV0V1awpV2aFandV3V4F"> - <proof - prover="3" - timelimit="25" - memlimit="1000" - edited="blocking_semantics_WP_wp_conj_1.v" - obsolete="false" - archived="false"> - <result status="unknown" time="11.85"/> - </proof> - </goal> - <goal - name="wp_reduction" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="584" loccnumb="8" loccnume="20" - sum="ad4fe21da86e1900cd2dc0d5f3954060" - proved="true" - expanded="false" - shape="aeval_fmlaV1V3awpV5V6Iaeval_fmlaV0V2awpV4V6FIaone_stepV0V2V4V1V3V5F"> - <proof - prover="3" - timelimit="5" - memlimit="1000" - edited="blocking_semantics_WP_wp_reduction_1.v" - obsolete="false" - archived="false"> - <result status="valid" time="0.76"/> - </proof> - </goal> - <goal - name="decide_value" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="597" loccnumb="8" loccnume="20" - sum="a2a1d1223a4e12a635ddf027163acde4" - proved="true" - expanded="false" - shape="ainfix =V0aEvalueV1EOanot_a_valueV0F"> - <proof - prover="0" - timelimit="5" - memlimit="1000" - obsolete="false" - archived="false"> - <result status="valid" time="0.04"/> - </proof> - </goal> - <goal - name="progress" - locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw" - loclnum="600" loccnumb="8" loccnume="16" - sum="9841f706af20265bae5147921eece1ba" - proved="true" - expanded="true" - shape="aone_stepV1V2V0V4V5V6EIanot_a_valueV0Aaeval_fmlaV1V2awpV0V3F"> - <proof - prover="3" - timelimit="3" - memlimit="0" - edited="blocking_semantics_WP_progress_1.v" - obsolete="false" - archived="false"> - <result status="valid" time="0.85"/> - </proof> - </goal> - </theory> - </file> -</why3session> diff --git a/examples/hoare_logic/blocking_semantics2/why3session.xml b/examples/hoare_logic/blocking_semantics2/why3session.xml index 173a6ea18e798e8d7558cd2daa61d667e1db913f..4a5a21d79a4d58f08c96688297c1b7d8f6a9b448 100644 --- a/examples/hoare_logic/blocking_semantics2/why3session.xml +++ b/examples/hoare_logic/blocking_semantics2/why3session.xml @@ -1,7 +1,7 @@ <?xml version="1.0" encoding="UTF-8"?> -<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd"> +<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd"> <why3session - name="blocking_semantics2/why3session.xml" shape_version="2"> + name="hoare_logic/blocking_semantics2/why3session.xml" shape_version="2"> <prover id="0" name="Alt-Ergo" @@ -36,13 +36,13 @@ expanded="true"> <theory name="ImpExpr" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="6" loccnumb="7" loccnume="14" verified="false" expanded="false"> <goal name="get_stack_eq" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="197" loccnumb="6" loccnume="18" sum="ca50d483ea94ddb7d95754423ecb2a16" proved="true" @@ -59,7 +59,7 @@ </goal> <goal name="get_stack_neq" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="201" loccnumb="6" loccnume="19" sum="4316e6ee20bd5461b7dc1d7b01698404" proved="true" @@ -71,12 +71,12 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.02"/> + <result status="valid" time="0.03"/> </proof> </goal> <goal name="eval_msubst_term" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="269" loccnumb="6" loccnume="22" sum="311742494eee9c100f92af210d63464d" proved="false" @@ -88,7 +88,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.02"/> + <result status="timeout" time="3.11"/> </proof> <proof prover="2" @@ -96,7 +96,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.02"/> + <result status="timeout" time="3.10"/> </proof> <proof prover="0" @@ -104,7 +104,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="unknown" time="0.20"/> + <result status="unknown" time="0.19"/> </proof> <proof prover="3" @@ -112,7 +112,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.09"/> + <result status="timeout" time="3.05"/> </proof> <proof prover="6" @@ -120,12 +120,12 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.02"/> + <result status="timeout" time="3.01"/> </proof> </goal> <goal name="eval_subst_term" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="275" loccnumb="6" loccnume="21" sum="5642fea185a2f1e0a5c35bf02f3270a8" proved="false" @@ -137,7 +137,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.06"/> + <result status="timeout" time="3.01"/> </proof> <proof prover="2" @@ -145,7 +145,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.05"/> + <result status="timeout" time="3.01"/> </proof> <proof prover="0" @@ -161,7 +161,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.04"/> + <result status="timeout" time="3.01"/> </proof> <proof prover="6" @@ -169,12 +169,12 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.10"/> + <result status="timeout" time="3.01"/> </proof> </goal> <goal name="eval_term_change_free" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="281" loccnumb="6" loccnume="27" sum="f523b13f28d89dffbfe9be90f7ce5480" proved="false" @@ -186,7 +186,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.12"/> + <result status="timeout" time="3.11"/> </proof> <proof prover="2" @@ -194,7 +194,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.03"/> + <result status="timeout" time="3.01"/> </proof> <proof prover="0" @@ -202,7 +202,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="unknown" time="1.66"/> + <result status="unknown" time="1.60"/> </proof> <proof prover="3" @@ -210,7 +210,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.02"/> + <result status="timeout" time="3.01"/> </proof> <proof prover="6" @@ -223,7 +223,7 @@ </goal> <goal name="subst_fresh" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="316" loccnumb="6" loccnume="17" sum="197b0533e6284e2f9905d0db1a845a46" proved="false" @@ -235,7 +235,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.10"/> + <result status="timeout" time="3.01"/> </proof> <proof prover="2" @@ -243,7 +243,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.03"/> + <result status="timeout" time="3.01"/> </proof> <proof prover="0" @@ -251,7 +251,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="unknown" time="0.03"/> + <result status="unknown" time="0.04"/> </proof> <proof prover="3" @@ -259,7 +259,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.03"/> + <result status="timeout" time="3.02"/> </proof> <proof prover="6" @@ -267,12 +267,12 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.03"/> + <result status="timeout" time="3.02"/> </proof> </goal> <goal name="let_subst" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="320" loccnumb="6" loccnume="15" sum="ba5285f6dbaa61985ca341d8b81a0074" proved="true" @@ -289,7 +289,7 @@ </goal> <goal name="eval_msubst" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="324" loccnumb="6" loccnume="17" sum="b8094c44743abc74f9e2c2fb397c8c48" proved="false" @@ -298,7 +298,7 @@ </goal> <goal name="eval_subst" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="330" loccnumb="6" loccnume="16" sum="5cadd16df627334d52116e03e24026cd" proved="false" @@ -310,7 +310,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.09"/> + <result status="timeout" time="3.01"/> </proof> <proof prover="2" @@ -318,7 +318,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.02"/> + <result status="timeout" time="3.01"/> </proof> <proof prover="0" @@ -326,7 +326,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="unknown" time="1.77"/> + <result status="unknown" time="1.78"/> </proof> <proof prover="3" @@ -347,7 +347,7 @@ </goal> <goal name="eval_swap" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="336" loccnumb="6" loccnume="15" sum="b94ce41a631e88b80d108cbd6dac2d46" proved="false" @@ -359,7 +359,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.03"/> + <result status="timeout" time="3.01"/> </proof> <proof prover="2" @@ -367,7 +367,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.10"/> + <result status="timeout" time="3.01"/> </proof> <proof prover="0" @@ -375,7 +375,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.10"/> + <result status="timeout" time="3.01"/> </proof> <proof prover="3" @@ -383,7 +383,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.10"/> + <result status="timeout" time="3.02"/> </proof> <proof prover="6" @@ -396,7 +396,7 @@ </goal> <goal name="eval_same_var" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="342" loccnumb="6" loccnume="19" sum="a4ac24b52516b9b916cb6d873a9fec35" proved="false" @@ -405,7 +405,7 @@ </goal> <goal name="eval_change_free" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="347" loccnumb="6" loccnume="22" sum="7352d215a729f3de25bd68ac6a642728" proved="false" @@ -417,7 +417,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.02"/> + <result status="timeout" time="3.11"/> </proof> <proof prover="2" @@ -425,7 +425,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.02"/> + <result status="timeout" time="3.01"/> </proof> <proof prover="0" @@ -449,12 +449,12 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.09"/> + <result status="timeout" time="3.01"/> </proof> </goal> <goal name="let_equiv" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="357" loccnumb="6" loccnume="15" sum="6a26f5fad187fc70a55d9902908469df" proved="true" @@ -466,7 +466,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="5.01"/> + <result status="timeout" time="5.02"/> </proof> <proof prover="2" @@ -474,7 +474,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="5.01"/> + <result status="timeout" time="5.02"/> </proof> <proof prover="0" @@ -490,7 +490,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="5.03"/> + <result status="timeout" time="5.11"/> </proof> <proof prover="6" @@ -498,7 +498,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="5.04"/> + <result status="timeout" time="5.02"/> </proof> <proof prover="1" @@ -511,7 +511,7 @@ </goal> <goal name="let_equiv2" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="364" loccnumb="6" loccnume="16" sum="e59c4b8b2276313d93bb2bc24fc0a994" proved="false" @@ -520,7 +520,7 @@ </goal> <goal name="let_implies" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="371" loccnumb="6" loccnume="17" sum="6f5b988a3173b9c0aa73bd82307a2c67" proved="false" @@ -529,7 +529,7 @@ </goal> <goal name="steps_non_neg" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="486" loccnumb="8" loccnume="21" sum="7066c6c11bc31bb26036501c0279c789" proved="false" @@ -541,7 +541,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.09"/> + <result status="timeout" time="3.11"/> </proof> <proof prover="2" @@ -557,7 +557,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.10"/> + <result status="timeout" time="3.01"/> </proof> <proof prover="3" @@ -565,7 +565,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.02"/> + <result status="timeout" time="3.01"/> </proof> <proof prover="6" @@ -573,12 +573,12 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.12"/> + <result status="timeout" time="3.11"/> </proof> </goal> <goal name="many_steps_seq" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="490" loccnumb="8" loccnume="22" sum="4c82632a7bddd75eeb21cce8e9adae02" proved="false" @@ -590,7 +590,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.04"/> + <result status="timeout" time="3.01"/> </proof> <proof prover="2" @@ -598,7 +598,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.10"/> + <result status="timeout" time="3.01"/> </proof> <proof prover="0" @@ -606,7 +606,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.09"/> + <result status="timeout" time="3.01"/> </proof> <proof prover="3" @@ -614,7 +614,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.09"/> + <result status="timeout" time="3.01"/> </proof> <proof prover="6" @@ -622,12 +622,12 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.02"/> + <result status="timeout" time="3.01"/> </proof> </goal> <goal name="many_steps_let" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="498" loccnumb="8" loccnume="22" sum="aa87f90ace146a57084c1232f8884a0e" proved="false" @@ -639,7 +639,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.02"/> + <result status="timeout" time="3.01"/> </proof> <proof prover="2" @@ -647,7 +647,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.02"/> + <result status="timeout" time="3.01"/> </proof> <proof prover="0" @@ -671,12 +671,12 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.09"/> + <result status="timeout" time="3.11"/> </proof> </goal> <goal name="one_step_change_free" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="506" loccnumb="7" loccnume="27" sum="c3846064bf3d2f839f69581c4aa37a64" proved="false" @@ -688,7 +688,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.10"/> + <result status="timeout" time="3.01"/> </proof> <proof prover="2" @@ -696,7 +696,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.10"/> + <result status="timeout" time="3.01"/> </proof> <proof prover="0" @@ -704,7 +704,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="unknown" time="2.33"/> + <result status="unknown" time="2.25"/> </proof> <proof prover="3" @@ -726,13 +726,13 @@ </theory> <theory name="TestSemantics" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="533" loccnumb="7" loccnume="20" verified="false" expanded="false"> <goal name="Test13" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="543" loccnumb="5" loccnume="11" sum="952f3464939ccf9802785a242e7a3987" proved="true" @@ -749,7 +749,7 @@ </goal> <goal name="Test13expr" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="546" loccnumb="5" loccnume="15" sum="78f57a8ab0cbfa8d228a73ab61c23f7d" proved="true" @@ -766,7 +766,7 @@ </goal> <goal name="Test42" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="549" loccnumb="5" loccnume="11" sum="157bdbdba5ab98f33f07ac4c63febd85" proved="true" @@ -783,7 +783,7 @@ </goal> <goal name="Test42expr" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="552" loccnumb="5" loccnume="15" sum="07c90be98b9c9eb35c046d362d15f563" proved="false" @@ -795,12 +795,12 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.01"/> + <result status="timeout" time="3.02"/> </proof> </goal> <goal name="Test0" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="555" loccnumb="5" loccnume="10" sum="67b17376508c291ac0139bef63aad166" proved="true" @@ -817,7 +817,7 @@ </goal> <goal name="Test0expr" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="558" loccnumb="5" loccnume="14" sum="97fdd1002502d509cf7aab84c29a4ab6" proved="false" @@ -829,12 +829,12 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.02"/> + <result status="timeout" time="3.01"/> </proof> </goal> <goal name="Test55" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="561" loccnumb="5" loccnume="11" sum="69120e26f26bf12dea4e27b0518d93eb" proved="false" @@ -846,12 +846,12 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.09"/> + <result status="timeout" time="3.02"/> </proof> </goal> <goal name="Test55expr" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="564" loccnumb="5" loccnume="15" sum="ee0206b464ecae09872dcf01ae28b771" proved="false" @@ -863,12 +863,12 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.09"/> + <result status="timeout" time="3.02"/> </proof> </goal> <goal name="Ass42" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="567" loccnumb="5" loccnume="10" sum="ee1779812b4cdc3947d212b28911a71d" proved="true" @@ -880,12 +880,12 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.53"/> + <result status="valid" time="0.54"/> </proof> </goal> <goal name="If42" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="572" loccnumb="5" loccnume="9" sum="ccc148c581aa50d7eeff8a0b88ba5273" proved="false" @@ -897,19 +897,19 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.11"/> + <result status="timeout" time="3.01"/> </proof> </goal> </theory> <theory name="HoareLogic" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="586" loccnumb="7" loccnume="17" verified="false" expanded="false"> <goal name="consequence_rule" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="593" loccnumb="6" loccnume="22" sum="9eb549a80119bf433df5f59b8162847d" proved="false" @@ -926,7 +926,7 @@ </goal> <goal name="value_rule" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="600" loccnumb="6" loccnume="16" sum="4f83a7066ccc3e754b120c9bf7f03c9a" proved="false" @@ -943,7 +943,7 @@ </goal> <goal name="assign_rule" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="604" loccnumb="6" loccnume="17" sum="aef8aefa15ae7083f02d56d6eb99430d" proved="false" @@ -955,12 +955,12 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.01"/> + <result status="timeout" time="3.02"/> </proof> </goal> <goal name="seq_rule" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="609" loccnumb="6" loccnume="14" sum="07f32b97a18a0898eedf88a030d64322" proved="false" @@ -972,12 +972,12 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.09"/> + <result status="timeout" time="3.01"/> </proof> </goal> <goal name="let_rule" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="614" loccnumb="6" loccnume="14" sum="bb084b761ed946f91c3af9cc6c4baf75" proved="false" @@ -989,12 +989,12 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.10"/> + <result status="timeout" time="3.01"/> </proof> </goal> <goal name="assert_rule" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="628" loccnumb="6" loccnume="17" sum="74a1f43e5c2d56692dd98a92f6f663e7" proved="false" @@ -1006,12 +1006,12 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.01"/> + <result status="timeout" time="3.03"/> </proof> </goal> <goal name="assert_rule_ext" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="632" loccnumb="6" loccnume="21" sum="bcaf89d16ce16b93f00d780d86118e77" proved="false" @@ -1023,19 +1023,19 @@ memlimit="0" obsolete="false" archived="false"> - <result status="timeout" time="3.01"/> + <result status="timeout" time="3.04"/> </proof> </goal> </theory> <theory name="Simpl_tautology" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="653" loccnumb="7" loccnume="22" verified="true" expanded="false"> <goal name="simpl_tautology" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="658" loccnumb="8" loccnume="23" sum="4e337593f2731debe350aaa609d33d2d" proved="true" @@ -1047,21 +1047,21 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.00"/> + <result status="valid" time="0.01"/> </proof> </goal> </theory> <theory name="WP" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="665" loccnumb="7" loccnume="9" verified="false" expanded="true"> <goal name="assigns_refl" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="679" loccnumb="6" loccnume="18" - sum="33a23759ca5225e5c875938290184776" + sum="5cbb1271471bc1132d4cc41966c9cdd9" proved="true" expanded="true" shape="aassignsV0V1V0F"> @@ -1071,14 +1071,14 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.04"/> + <result status="valid" time="0.05"/> </proof> </goal> <goal name="assigns_trans" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="682" loccnumb="6" loccnume="19" - sum="a6bbaa0f8b6ad8f3f254dd808591ee64" + sum="80ef856161427663cb4ddd8ba3214054" proved="true" expanded="true" shape="aassignsV0V3V2IaassignsV1V3V2AaassignsV0V3V1F"> @@ -1088,14 +1088,14 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.05"/> + <result status="valid" time="0.04"/> </proof> </goal> <goal name="assigns_union_left" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="687" loccnumb="6" loccnume="24" - sum="8d48d8fa3b84c9331e381a592a993833" + sum="1051f24c1dffe713749d7571a6d0b2c8" proved="true" expanded="true" shape="aassignsV0aunionV2V3V1IaassignsV0V2V1F"> @@ -1110,9 +1110,9 @@ </goal> <goal name="assigns_union_right" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="691" loccnumb="6" loccnume="25" - sum="9b9de497b4b231068c0671997c7cfe41" + sum="503ceaa1e4ccdebdaeb1300fb46dac55" proved="true" expanded="true" shape="aassignsV0aunionV2V3V1IaassignsV0V3V1F"> @@ -1122,14 +1122,14 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.05"/> + <result status="valid" time="0.04"/> </proof> </goal> <goal name="result_always_fresh_in_wp" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="759" loccnumb="8" loccnume="33" - sum="a20c796acea768bb14d1a400965642b6" + sum="3dd5a1c19c5595231d4d05e1951a7ea0" proved="false" expanded="true" shape="afresh_in_fmlaaresultawpV0V1F"> @@ -1140,23 +1140,23 @@ edited="blocking_semantics2_WP_result_always_fresh_in_wp_1.v" obsolete="false" archived="false"> - <result status="unknown" time="0.66"/> + <result status="unknown" time="0.62"/> </proof> </goal> <goal name="distrib_conj" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="767" loccnumb="8" loccnume="20" - sum="b32ad021aba6f3f0c411e037a19a658f" + sum="a7990eecd796430555140c201962f6ac" proved="false" expanded="false" shape="aeval_fmlaV0V1awpV2V4Aaeval_fmlaV0V1awpV2V3qaeval_fmlaV0V1awpV2aFandV3V4F"> </goal> <goal name="monotonicity" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="773" loccnumb="8" loccnume="20" - sum="154821f0d2c2eb9da9af1e42aed1c876" + sum="2c8f57f83dcfa8258ca21e69ae5900a9" proved="false" expanded="true" shape="avalid_fmlaaFimpliesawpV0V1awpV0V2Iavalid_fmlaaFimpliesV1V2F"> @@ -1167,14 +1167,14 @@ edited="blocking_semantics2_WP_monotonicity_1.v" obsolete="false" archived="false"> - <result status="unknown" time="0.67"/> + <result status="unknown" time="0.66"/> </proof> </goal> <goal name="wp_reduction" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="778" loccnumb="8" loccnume="20" - sum="0856a4d05985f1de63d26697756626bb" + sum="dc2dfea4c843979023db3346719b73e5" proved="true" expanded="true" shape="aeval_fmlaV1V3awpV5V6Iaeval_fmlaV0V2awpV4V6FIaone_stepV0V2V4V1V3V5F"> @@ -1185,14 +1185,14 @@ edited="blocking_semantics2_WP_wp_reduction_2.v" obsolete="false" archived="false"> - <result status="valid" time="0.83"/> + <result status="valid" time="0.81"/> </proof> </goal> <goal name="decide_value" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="791" loccnumb="8" loccnume="20" - sum="59ea866807362cb0a1e9f735d9276523" + sum="80ba423abe7808575ec671b9dd5d2ddb" proved="true" expanded="true" shape="ainfix =V0aEvalueV1EOais_valueV0NF"> @@ -1215,9 +1215,9 @@ </goal> <goal name="bool_value" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="794" loccnumb="8" loccnume="18" - sum="07877a83915b2aaa6790b12d9b5b4826" + sum="c21c40a73241bda2a2270a91685f84db" proved="true" expanded="true" shape="ainfix =V0aVboolaTrueOainfix =V0aVboolaFalseIatype_exprV1V2aEvalueV0aTYboolF"> @@ -1228,14 +1228,14 @@ edited="blocking_semantics2_WP_bool_value_1.v" obsolete="false" archived="false"> - <result status="valid" time="0.70"/> + <result status="valid" time="0.68"/> </proof> </goal> <goal name="unit_value" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="799" loccnumb="8" loccnume="18" - sum="6f598a06d8881ffccf84bf0bacca8380" + sum="671b6f1b0f06e6fa0d001d2299efd703" proved="true" expanded="true" shape="ainfix =V0aVvoidIatype_exprV1V2aEvalueV0aTYunitF"> @@ -1245,14 +1245,14 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.66"/> + <result status="valid" time="0.67"/> </proof> </goal> <goal name="progress" - locfile="blocking_semantics2/../blocking_semantics2.mlw" + locfile="hoare_logic/blocking_semantics2/../blocking_semantics2.mlw" loclnum="803" loccnumb="8" loccnume="16" - sum="6721d4b21f716ba4f249d5e6048747b7" + sum="2e18d5fff1187f8dd6532fa34091c2e4" proved="true" expanded="true" shape="aone_stepV1V2V0V7V8V9EIais_valueV0NIaeval_fmlaV1V2awpV0V6Iatype_fmlaV3aConsaTuple2aresultV5V4V6Iatype_exprV3V4V0V5F"> @@ -1263,7 +1263,7 @@ edited="blocking_semantics2_WP_progress_1.v" obsolete="false" archived="false"> - <result status="valid" time="1.15"/> + <result status="valid" time="1.12"/> </proof> </goal> </theory> diff --git a/examples/hoare_logic/wp3.mlw b/examples/hoare_logic/wp3.mlw index de15a2b93a1a46431b99fb3e1bfed469bf50656d..053a2f89e155869c668a9204860794b31269ff12 100644 --- a/examples/hoare_logic/wp3.mlw +++ b/examples/hoare_logic/wp3.mlw @@ -189,7 +189,7 @@ inductive one_step env env expr env env expr = one_step sigma pi (Eseq e1 e2) sigma' pi' (Eseq e1' e2) | one_step_seq_value: - forall sigma pi:env, id:ident, e:expr. + forall sigma pi:env, e:expr. one_step sigma pi (Eseq void e) sigma pi e | one_step_let_ctxt: @@ -202,16 +202,16 @@ inductive one_step env env expr env env expr = one_step sigma pi (Elet id (Evalue v) e) sigma (IdMap.set pi id v) e | one_step_if_ctxt: - forall sigma pi sigma' pi':env, id:ident, e1 e1' e2 e3:expr. + forall sigma pi sigma' pi':env, e1 e1' e2 e3:expr. one_step sigma pi e1 sigma' pi' e1' -> one_step sigma pi (Eif e1 e2 e3) sigma' pi' (Eif e1' e2 e3) | one_step_if_true: - forall sigma pi:env, e:term, e1 e2:expr. + forall sigma pi:env, e1 e2:expr. one_step sigma pi (Eif (Evalue (Vbool True)) e1 e2) sigma pi e1 | one_step_if_false: - forall sigma pi:env, e:term, e1 e2:expr. + forall sigma pi:env, e1 e2:expr. one_step sigma pi (Eif (Evalue (Vbool False)) e1 e2) sigma pi e2 | one_step_assert: diff --git a/examples/hoare_logic/wp3/why3session.xml b/examples/hoare_logic/wp3/why3session.xml index a7855e7496f29005450e5bfc8a3168d180d18c50..d2bb0d9c1b4969934923d2a041b950f338999a0e 100644 --- a/examples/hoare_logic/wp3/why3session.xml +++ b/examples/hoare_logic/wp3/why3session.xml @@ -1,7 +1,7 @@ <?xml version="1.0" encoding="UTF-8"?> -<!DOCTYPE why3session SYSTEM "/users/demons/melquion/src/why3/share/why3session.dtd"> +<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd"> <why3session - name="hoare_logic/wp3/why3session.xml" shape_version="2"> + name="wp3/why3session.xml" shape_version="2"> <prover id="0" name="Alt-Ergo" @@ -24,13 +24,13 @@ expanded="true"> <theory name="ImpExpr" - locfile="hoare_logic/wp3/../wp3.mlw" + locfile="wp3/../wp3.mlw" loclnum="6" loccnumb="7" loccnume="14" verified="false" expanded="false"> <goal name="eval_subst_term" - locfile="hoare_logic/wp3/../wp3.mlw" + locfile="wp3/../wp3.mlw" loclnum="101" loccnumb="6" loccnume="21" sum="9e34d8d7464801759bc7c027e8974e19" proved="false" @@ -63,7 +63,7 @@ </goal> <goal name="eval_term_change_free" - locfile="hoare_logic/wp3/../wp3.mlw" + locfile="wp3/../wp3.mlw" loclnum="107" loccnumb="6" loccnume="27" sum="ec95ad78268f62f07e785f129651afaf" proved="false" @@ -96,7 +96,7 @@ </goal> <goal name="eval_subst" - locfile="hoare_logic/wp3/../wp3.mlw" + locfile="wp3/../wp3.mlw" loclnum="133" loccnumb="6" loccnume="16" sum="9536899932fca871e16547ba1f0a6f26" proved="false" @@ -129,7 +129,7 @@ </goal> <goal name="eval_swap" - locfile="hoare_logic/wp3/../wp3.mlw" + locfile="wp3/../wp3.mlw" loclnum="139" loccnumb="6" loccnume="15" sum="12564bad48e60bc69c29042d78d9efb6" proved="true" @@ -162,7 +162,7 @@ </goal> <goal name="eval_change_free" - locfile="hoare_logic/wp3/../wp3.mlw" + locfile="wp3/../wp3.mlw" loclnum="145" loccnumb="6" loccnume="22" sum="8289123789ee1faf6ab01786198f4cc4" proved="false" @@ -195,9 +195,9 @@ </goal> <goal name="steps_non_neg" - locfile="hoare_logic/wp3/../wp3.mlw" + locfile="wp3/../wp3.mlw" loclnum="247" loccnumb="6" loccnume="19" - sum="9fff4ff64f5b2c108980b5b05d6c6758" + sum="0b842807fe72171018f20465074ad820" proved="false" expanded="false" shape="ainfix >=V6c0Iamany_stepsV0V1V4V2V3V5V6F"> @@ -207,7 +207,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="2.01"/> + <result status="timeout" time="2.05"/> </proof> <proof prover="1" @@ -215,7 +215,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="2.01"/> + <result status="timeout" time="2.09"/> </proof> <proof prover="3" @@ -223,23 +223,23 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="2.11"/> + <result status="timeout" time="2.08"/> </proof> </goal> <goal name="many_steps_seq" - locfile="hoare_logic/wp3/../wp3.mlw" + locfile="wp3/../wp3.mlw" loclnum="251" loccnumb="6" loccnume="20" - sum="72180792ce0eaa52efadd656cdd3336c" + sum="642e0427495c4ccadfa860c7162de042" proved="false" expanded="false" shape="ainfix =V6ainfix +ainfix +c1V9V10Aamany_stepsV7V8V5V2V3avoidV10Aamany_stepsV0V1V4V7V8avoidV9EIamany_stepsV0V1aEseqV4V5V2V3avoidV6F"> </goal> <goal name="many_steps_let" - locfile="hoare_logic/wp3/../wp3.mlw" + locfile="wp3/../wp3.mlw" loclnum="259" loccnumb="6" loccnume="20" - sum="aa9ea7158f28cb20c8a48b7a9cce393a" + sum="a746ceccf49b01a6390b7ce2f9f6412a" proved="false" expanded="false" shape="ainfix =V8ainfix +ainfix +c1V12V13Aamany_stepsV9asetV10V4V11V6V2V3aEvalueV7V13Aamany_stepsV0V1V5V9V10aEvalueV11V12EIamany_stepsV0V1aEletV4V5V6V2V3aEvalueV7V8F"> @@ -249,7 +249,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="30.09"/> + <result status="timeout" time="30.11"/> </proof> <proof prover="3" @@ -257,21 +257,21 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="30.09"/> + <result status="timeout" time="30.07"/> </proof> </goal> </theory> <theory name="TestSemantics" - locfile="hoare_logic/wp3/../wp3.mlw" + locfile="wp3/../wp3.mlw" loclnum="291" loccnumb="7" loccnume="20" verified="false" expanded="true"> <goal name="Test13" - locfile="hoare_logic/wp3/../wp3.mlw" + locfile="wp3/../wp3.mlw" loclnum="298" loccnumb="5" loccnume="11" - sum="4b1b3e95e8d4d4aeee871bd16f5b91b0" + sum="78ce2e48414e1416812cd8beb785abd3" proved="true" expanded="false" shape="ainfix =aeval_termamy_sigmaamy_piaTvalueaVintc13aVintc13"> @@ -289,14 +289,14 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="valid" time="0.04"/> + <result status="valid" time="0.03"/> </proof> </goal> <goal name="Test13expr" - locfile="hoare_logic/wp3/../wp3.mlw" + locfile="wp3/../wp3.mlw" loclnum="301" loccnumb="5" loccnume="15" - sum="9b014c90e00d59a39c0656b2be32bfff" + sum="c4e5ad12badf7238d604bdfa6cf27332" proved="true" expanded="false" shape="amany_stepsamy_sigmaamy_piaEvalueaVintc13amy_sigmaamy_piaEvalueaVintc13c0"> @@ -322,14 +322,14 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="valid" time="0.27"/> + <result status="valid" time="0.28"/> </proof> </goal> <goal name="Test42" - locfile="hoare_logic/wp3/../wp3.mlw" + locfile="wp3/../wp3.mlw" loclnum="304" loccnumb="5" loccnume="11" - sum="96f6df244a951ce44d0cc0d249044f49" + sum="74e41c3124ea50bde20475a273b0c4d5" proved="true" expanded="false" shape="ainfix =aeval_termamy_sigmaamy_piaTvarc0aVintc42"> @@ -339,7 +339,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="valid" time="0.03"/> + <result status="valid" time="0.02"/> </proof> <proof prover="1" @@ -352,9 +352,9 @@ </goal> <goal name="Test42expr" - locfile="hoare_logic/wp3/../wp3.mlw" + locfile="wp3/../wp3.mlw" loclnum="307" loccnumb="5" loccnume="15" - sum="7437c9c5d58b5628672ea52743289d9d" + sum="48f13711530403778d430a9c612b985d" proved="false" expanded="true" shape="amany_stepsamy_sigmaamy_piaEvarc0amy_sigmaamy_piaEvalueaVintc42c1"> @@ -364,7 +364,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="unknown" time="1.64"/> + <result status="unknown" time="1.62"/> </proof> <proof prover="1" @@ -372,7 +372,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="2.38"/> + <result status="timeout" time="2.01"/> </proof> <proof prover="3" @@ -380,14 +380,14 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="2.28"/> + <result status="timeout" time="2.01"/> </proof> </goal> <goal name="Test0" - locfile="hoare_logic/wp3/../wp3.mlw" + locfile="wp3/../wp3.mlw" loclnum="310" loccnumb="5" loccnume="10" - sum="5ab19d0f23bcb76b96bcb24a6968d8b9" + sum="26077302b601909d672c167060acf213" proved="true" expanded="false" shape="ainfix =aeval_termamy_sigmaamy_piaTderefc0aVintc0"> @@ -397,7 +397,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="valid" time="0.03"/> + <result status="valid" time="0.02"/> </proof> <proof prover="1" @@ -405,14 +405,14 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="valid" time="0.06"/> + <result status="valid" time="0.05"/> </proof> </goal> <goal name="Test0expr" - locfile="hoare_logic/wp3/../wp3.mlw" + locfile="wp3/../wp3.mlw" loclnum="313" loccnumb="5" loccnume="14" - sum="600fb689a3585058761559d02ad9adbe" + sum="0f1de39a171484f87e38e9559372f193" proved="false" expanded="true" shape="amany_stepsamy_sigmaamy_piaEderefc0amy_sigmaamy_piaEvalueaVintc0c1"> @@ -422,7 +422,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="unknown" time="1.64"/> + <result status="unknown" time="1.80"/> </proof> <proof prover="1" @@ -430,7 +430,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="2.32"/> + <result status="timeout" time="2.10"/> </proof> <proof prover="3" @@ -438,14 +438,14 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="2.22"/> + <result status="timeout" time="2.10"/> </proof> </goal> <goal name="Test55" - locfile="hoare_logic/wp3/../wp3.mlw" + locfile="wp3/../wp3.mlw" loclnum="316" loccnumb="5" loccnume="11" - sum="e0223cfe6a4ba3e01d5cf21122cd9c89" + sum="f6fade931a67cb8924f67b334ade967e" proved="false" expanded="false" shape="ainfix =aeval_termamy_sigmaamy_piaTbinaTvarc0aOplusaTvalueaVintc13aVintc55"> @@ -455,7 +455,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="2.22"/> + <result status="timeout" time="2.01"/> </proof> <proof prover="1" @@ -476,9 +476,9 @@ </goal> <goal name="Test55expr" - locfile="hoare_logic/wp3/../wp3.mlw" + locfile="wp3/../wp3.mlw" loclnum="319" loccnumb="5" loccnume="15" - sum="26de6358a35d3cb414efbf5753f7dd2b" + sum="3325f23445d76083f98c917cd05865fc" proved="false" expanded="false" shape="amany_stepsamy_sigmaamy_piaEbinaEvarc0aOplusaEvalueaVintc13amy_sigmaamy_piaEvalueaVintc55c3"> @@ -496,7 +496,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="2.04"/> + <result status="timeout" time="2.10"/> </proof> <proof prover="3" @@ -504,14 +504,14 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="2.04"/> + <result status="timeout" time="2.10"/> </proof> </goal> <goal name="Ass42" - locfile="hoare_logic/wp3/../wp3.mlw" + locfile="wp3/../wp3.mlw" loclnum="322" loccnumb="5" loccnume="10" - sum="74e919cdc6a9c3f64e29e2fcdd7a5cc4" + sum="9da34a7af3745ade19716f4534798e84" proved="true" expanded="false" shape="ainfix =agetV1V0aVintc42Iaone_stepamy_sigmaamy_piaEassignV0aEvalueaVintc42V1V2avoidFLc0"> @@ -529,7 +529,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="valid" time="0.24"/> + <result status="valid" time="0.22"/> </proof> <proof prover="3" @@ -537,14 +537,14 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="valid" time="0.30"/> + <result status="valid" time="0.32"/> </proof> </goal> <goal name="If42" - locfile="hoare_logic/wp3/../wp3.mlw" + locfile="wp3/../wp3.mlw" loclnum="328" loccnumb="5" loccnume="9" - sum="a72290349e116b84d3fd58bef2e9a3ff" + sum="7ad11bbc05106a380ed6460205636196" proved="true" expanded="false" shape="ainfix =agetV3V0aVintc13Iaone_stepV1V2V5V3V4avoidIaone_stepamy_sigmaamy_piaEifaEbinaEderefV0aOleaEvalueaVintc10aEassignV0aEvalueaVintc13aEassignV0aEvalueaVintc42V1V2V5FLc0"> @@ -568,15 +568,15 @@ </theory> <theory name="HoareLogic" - locfile="hoare_logic/wp3/../wp3.mlw" + locfile="wp3/../wp3.mlw" loclnum="343" loccnumb="7" loccnume="17" verified="false" expanded="true"> <goal name="consequence_rule" - locfile="hoare_logic/wp3/../wp3.mlw" + locfile="wp3/../wp3.mlw" loclnum="350" loccnumb="6" loccnume="22" - sum="bfcae856d6942a2c4743cf98aa56f8ba" + sum="59baf06455ce7cd9391c6f6734930df7" proved="true" expanded="true" shape="avalid_tripleV1V4V3Iavalid_fmlaaFimpliesV2V3Iavalid_tripleV0V4V2Iavalid_fmlaaFimpliesV1V0F"> @@ -586,7 +586,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="valid" time="2.84"/> + <result status="valid" time="2.76"/> </proof> <proof prover="2" @@ -595,14 +595,14 @@ edited="wp3_HoareLogic_consequence_rule_1.v" obsolete="false" archived="false"> - <result status="valid" time="0.68"/> + <result status="valid" time="0.52"/> </proof> </goal> <goal name="value_rule" - locfile="hoare_logic/wp3/../wp3.mlw" + locfile="wp3/../wp3.mlw" loclnum="357" loccnumb="6" loccnume="16" - sum="d2b54f4cf888fb88064f31e6576fb01f" + sum="170e7aa94418813b93da3aad6f91e5c4" proved="true" expanded="true" shape="avalid_tripleV0aEvalueV1V0Iafresh_in_fmlaaresultV0F"> @@ -612,14 +612,14 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="valid" time="3.83"/> + <result status="valid" time="3.78"/> </proof> </goal> <goal name="assign_rule" - locfile="hoare_logic/wp3/../wp3.mlw" + locfile="wp3/../wp3.mlw" loclnum="361" loccnumb="6" loccnume="17" - sum="4354900db77953db66fa2223572d67d1" + sum="1e664a21dd5a8893dfa7b3eb407bbc29" proved="false" expanded="true" shape="avalid_tripleV0aEassignV2V3V1Iavalid_tripleV0V3asubstV1V2aresultF"> @@ -629,7 +629,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="5.10"/> + <result status="timeout" time="5.04"/> </proof> <proof prover="1" @@ -637,7 +637,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="5.38"/> + <result status="timeout" time="5.04"/> </proof> <proof prover="3" @@ -645,14 +645,14 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="5.10"/> + <result status="timeout" time="5.03"/> </proof> </goal> <goal name="seq_rule" - locfile="hoare_logic/wp3/../wp3.mlw" + locfile="wp3/../wp3.mlw" loclnum="366" loccnumb="6" loccnume="14" - sum="950c32ca874ad0c091a9ea12fc35873b" + sum="252b30198a9a37d6abb673c4fd8c8599" proved="false" expanded="true" shape="avalid_tripleV0aEseqV3V4V1Iavalid_tripleV2V4V1Aavalid_tripleV0V3V2F"> @@ -662,7 +662,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="5.40"/> + <result status="timeout" time="5.02"/> </proof> <proof prover="1" @@ -670,7 +670,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="5.12"/> + <result status="timeout" time="5.02"/> </proof> <proof prover="3" @@ -678,14 +678,14 @@ memlimit="2000" obsolete="false" archived="false"> - <result status="outofmemory" time="17.48"/> + <result status="outofmemory" time="17.07"/> </proof> </goal> <goal name="let_rule" - locfile="hoare_logic/wp3/../wp3.mlw" + locfile="wp3/../wp3.mlw" loclnum="371" loccnumb="6" loccnume="14" - sum="b65358c05fd16670ee012353c39a908f" + sum="6d142cd3d4f60a1c5ca9b1a911f74381" proved="false" expanded="true" shape="avalid_tripleV0aEletV3V4V5V1Iavalid_tripleaFletaresultaTvarV3V2V5V1Aavalid_tripleV0V4V2Iafresh_in_fmlaaresultV0F"> @@ -695,7 +695,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="5.22"/> + <result status="timeout" time="5.04"/> </proof> <proof prover="1" @@ -703,7 +703,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="5.12"/> + <result status="timeout" time="5.04"/> </proof> <proof prover="3" @@ -711,7 +711,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="outofmemory" time="19.24"/> + <result status="outofmemory" time="19.14"/> </proof> <proof prover="2" @@ -720,14 +720,14 @@ edited="wp3_HoareLogic_let_rule_1.v" obsolete="false" archived="false"> - <result status="unknown" time="0.62"/> + <result status="unknown" time="0.53"/> </proof> </goal> <goal name="assert_rule" - locfile="hoare_logic/wp3/../wp3.mlw" + locfile="wp3/../wp3.mlw" loclnum="385" loccnumb="6" loccnume="17" - sum="66c865bc911c9db0ee0eead30d090ca4" + sum="826029318617070c512bd214ac1c47c1" proved="false" expanded="true" shape="avalid_tripleV1aEassertV0V1Iavalid_fmlaaFimpliesV1V0F"> @@ -737,7 +737,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="5.16"/> + <result status="timeout" time="5.02"/> </proof> <proof prover="1" @@ -745,7 +745,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="5.05"/> + <result status="timeout" time="5.02"/> </proof> <proof prover="3" @@ -753,14 +753,14 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="5.36"/> + <result status="timeout" time="5.03"/> </proof> </goal> <goal name="assert_rule_ext" - locfile="hoare_logic/wp3/../wp3.mlw" + locfile="wp3/../wp3.mlw" loclnum="389" loccnumb="6" loccnume="21" - sum="5510677fc26de727712195b8efb0339b" + sum="2a2d8ede1fb5737bc66d46d5d8198129" proved="false" expanded="true" shape="avalid_tripleaFimpliesV0V1aEassertV0V1F"> @@ -770,7 +770,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="5.02"/> + <result status="timeout" time="5.04"/> </proof> <proof prover="1" @@ -778,7 +778,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="5.12"/> + <result status="timeout" time="5.04"/> </proof> <proof prover="3" @@ -786,7 +786,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="timeout" time="5.02"/> + <result status="timeout" time="5.04"/> </proof> </goal> </theory> diff --git a/examples/programs/vstte12_bfs/why3session.xml b/examples/programs/vstte12_bfs/why3session.xml index eac7ff52c0f9bcb413cd96c886c5b343e5ad36d4..f3dd6fcdbd1d74862638c9776c8d9f0ebb80c3dd 100644 --- a/examples/programs/vstte12_bfs/why3session.xml +++ b/examples/programs/vstte12_bfs/why3session.xml @@ -32,7 +32,7 @@ name="path_nonneg" locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="26" loccnumb="8" loccnume="19" - sum="4442850e2c5d7873dc0ef02f8076de1a" + sum="79fa28a0bd80a544e7d9e1839f10bfbd" proved="true" expanded="false" shape="ainfix >=V2c0IapathV0V1V2F"> @@ -43,14 +43,14 @@ edited="vstte12_bfs_Graph_path_nonneg_1.v" obsolete="false" archived="false"> - <result status="valid" time="0.50"/> + <result status="valid" time="0.49"/> </proof> </goal> <goal name="path_inversion" locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="30" loccnumb="8" loccnume="22" - sum="3635d145c92c2073cee1e520ded4989a" + sum="b14dea0726537e9ca43b39857f0417af" proved="true" expanded="false" shape="amemV1asuccV3AapathV0V3V2EIapathV0V1ainfix +V2c1Iainfix >=V2c0F"> @@ -61,14 +61,14 @@ edited="vstte12_bfs_Graph_path_inversion_1.v" obsolete="false" archived="false"> - <result status="valid" time="0.48"/> + <result status="valid" time="0.50"/> </proof> </goal> <goal name="path_closure" locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="36" loccnumb="8" loccnume="20" - sum="0eb95912593071555702e6b27697389d" + sum="ef402bb2f01dfe3e13fc45a70e24474c" proved="true" expanded="false" shape="amemV2V0IamemV1V0IapathV1V2V3FIamemV5V0IamemV5asuccV4FIamemV4V0FF"> @@ -79,7 +79,7 @@ edited="vstte12_bfs_Graph_path_closure_1.v" obsolete="false" archived="false"> - <result status="valid" time="0.49"/> + <result status="valid" time="0.47"/> </proof> </goal> </theory> @@ -94,7 +94,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="82" loccnumb="6" loccnume="15" expl="parameter fill_next" - sum="57b922160f0568efc83f181646b3debb" + sum="31745b6c4b86c993be4fb6baac23e524" proved="false" expanded="true" shape="iainfix =V10aTrueNiamemV12V9NaclosureV13V5V14V15Iainfix =V15V2NFAasubsetadiffasuccV2V11V13AasubsetV11asuccV2AainvV0V1V13V5V14V3Iainfix =V14aaddV12V8FIainfix =V13aaddV12V9FaclosureV9V5V8V16Iainfix =V16V2NFAasubsetadiffasuccV2V11V9AasubsetV11asuccV2AainvV0V1V9V5V8V3Iainfix =V11aremoveV12V7AamemV12V7FFAais_emptyV7NaclosureV9V5V8V17FAasubsetasuccV2V9AainvV0V1V9V5V8V3Iais_emptyV7qainfix =V10aTrueFIaclosureV9V5V8V18Iainfix =V18V2NFAasubsetadiffasuccV2V7V9AasubsetV7asuccV2AainvV0V1V9V5V8V3FAaclosureV6V5V4V19Iainfix =V19V2NFAasubsetadiffasuccV2asuccV2V6AasubsetasuccV2asuccV2AainvV0V1V6V5V4V3IaclosureV6V5V4V20Iainfix =V20V2NFAashortest_pathV0V2V3AainvV0V1V6V5V4V3FF"> @@ -109,7 +109,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="82" loccnumb="6" loccnume="15" expl="loop invariant init" - sum="af60d979a2c5f096d12bf08343e4df79" + sum="73ce6850c8980fe483e0356331d5329a" proved="true" expanded="false" shape="aclosureV6V5V4V7Iainfix =V7V2NFAasubsetadiffasuccV2asuccV2V6AasubsetasuccV2asuccV2AainvV0V1V6V5V4V3IaclosureV6V5V4V8Iainfix =V8V2NFAashortest_pathV0V2V3AainvV0V1V6V5V4V3FF"> @@ -129,7 +129,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="82" loccnumb="6" loccnume="15" expl="precondition" - sum="0fd6edb006e6b270aa3d58147aa858f5" + sum="903825ecb2144dcd115a16fcd84a2e83" proved="true" expanded="false" shape="ais_emptyV7NIainfix =V10aTrueNIais_emptyV7qainfix =V10aTrueFIaclosureV9V5V8V11Iainfix =V11V2NFAasubsetadiffasuccV2V7V9AasubsetV7asuccV2AainvV0V1V9V5V8V3FIaclosureV6V5V4V12Iainfix =V12V2NFAashortest_pathV0V2V3AainvV0V1V6V5V4V3FF"> @@ -141,7 +141,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.02"/> + <result status="valid" time="0.01"/> </proof> </goal> <goal @@ -149,7 +149,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="82" loccnumb="6" loccnume="15" expl="loop invariant preservation" - sum="126f16c0b48a01ab7ebc2a03b6e05fcb" + sum="7ae12aa0d2957a04732f21e24aa4edf7" proved="true" expanded="true" shape="aclosureV13V5V14V15Iainfix =V15V2NFAasubsetadiffasuccV2V11V13AasubsetV11asuccV2AainvV0V1V13V5V14V3Iainfix =V14aaddV12V8FIainfix =V13aaddV12V9FIamemV12V9NIainfix =V11aremoveV12V7AamemV12V7FFIais_emptyV7NIainfix =V10aTrueNIais_emptyV7qainfix =V10aTrueFIaclosureV9V5V8V16Iainfix =V16V2NFAasubsetadiffasuccV2V7V9AasubsetV7asuccV2AainvV0V1V9V5V8V3FIaclosureV6V5V4V17Iainfix =V17V2NFAashortest_pathV0V2V3AainvV0V1V6V5V4V3FF"> @@ -164,7 +164,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="82" loccnumb="6" loccnume="15" expl="parameter fill_next" - sum="a50d7339a0bdcbaa578768dba8383fff" + sum="7dc02bcb9edcd3abaab3df4ced166d5b" proved="true" expanded="false" shape="ainvV0V1V13V5V14V3Iainfix =V14aaddV12V8FIainfix =V13aaddV12V9FIamemV12V9NIainfix =V11aremoveV12V7AamemV12V7FFIais_emptyV7NIainfix =V10aTrueNIais_emptyV7qainfix =V10aTrueFIaclosureV9V5V8V15Iainfix =V15V2NFAasubsetadiffasuccV2V7V9AasubsetV7asuccV2AainvV0V1V9V5V8V3FIaclosureV6V5V4V16Iainfix =V16V2NFAashortest_pathV0V2V3AainvV0V1V6V5V4V3FF"> @@ -176,7 +176,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="2.28"/> + <result status="valid" time="7.83"/> </proof> </goal> <goal @@ -184,7 +184,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="82" loccnumb="6" loccnume="15" expl="parameter fill_next" - sum="0759c9740f401ce3ca1488afb54b5a2b" + sum="1b887b8efd6c7975d79853dbfa331b67" proved="true" expanded="false" shape="asubsetV11asuccV2Iainfix =V14aaddV12V8FIainfix =V13aaddV12V9FIamemV12V9NIainfix =V11aremoveV12V7AamemV12V7FFIais_emptyV7NIainfix =V10aTrueNIais_emptyV7qainfix =V10aTrueFIaclosureV9V5V8V15Iainfix =V15V2NFAasubsetadiffasuccV2V7V9AasubsetV7asuccV2AainvV0V1V9V5V8V3FIaclosureV6V5V4V16Iainfix =V16V2NFAashortest_pathV0V2V3AainvV0V1V6V5V4V3FF"> @@ -204,7 +204,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="82" loccnumb="6" loccnume="15" expl="parameter fill_next" - sum="c88cf42e57bb46bd9625eebbd15b8983" + sum="5ed9d505e26b238fb8e709b69fa7b5ab" proved="true" expanded="false" shape="asubsetadiffasuccV2V11V13Iainfix =V14aaddV12V8FIainfix =V13aaddV12V9FIamemV12V9NIainfix =V11aremoveV12V7AamemV12V7FFIais_emptyV7NIainfix =V10aTrueNIais_emptyV7qainfix =V10aTrueFIaclosureV9V5V8V15Iainfix =V15V2NFAasubsetadiffasuccV2V7V9AasubsetV7asuccV2AainvV0V1V9V5V8V3FIaclosureV6V5V4V16Iainfix =V16V2NFAashortest_pathV0V2V3AainvV0V1V6V5V4V3FF"> @@ -216,7 +216,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.43"/> + <result status="valid" time="0.24"/> </proof> </goal> <goal @@ -224,7 +224,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="82" loccnumb="6" loccnume="15" expl="parameter fill_next" - sum="66c441e05c776a893cf858e1187be305" + sum="45016b24c457bb4677b9cfc74ce2b938" proved="true" expanded="false" shape="aclosureV13V5V14V15Iainfix =V15V2NFIainfix =V14aaddV12V8FIainfix =V13aaddV12V9FIamemV12V9NIainfix =V11aremoveV12V7AamemV12V7FFIais_emptyV7NIainfix =V10aTrueNIais_emptyV7qainfix =V10aTrueFIaclosureV9V5V8V16Iainfix =V16V2NFAasubsetadiffasuccV2V7V9AasubsetV7asuccV2AainvV0V1V9V5V8V3FIaclosureV6V5V4V17Iainfix =V17V2NFAashortest_pathV0V2V3AainvV0V1V6V5V4V3FF"> @@ -236,7 +236,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.04"/> + <result status="valid" time="0.05"/> </proof> </goal> </transf> @@ -246,7 +246,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="82" loccnumb="6" loccnume="15" expl="loop invariant preservation" - sum="ea978df1bbf992d891769b71eeb64f13" + sum="aca8a54d7ad77584079824ef21d4f836" proved="false" expanded="true" shape="aclosureV9V5V8V13Iainfix =V13V2NFAasubsetadiffasuccV2V11V9AasubsetV11asuccV2AainvV0V1V9V5V8V3IamemV12V9NNIainfix =V11aremoveV12V7AamemV12V7FFIais_emptyV7NIainfix =V10aTrueNIais_emptyV7qainfix =V10aTrueFIaclosureV9V5V8V14Iainfix =V14V2NFAasubsetadiffasuccV2V7V9AasubsetV7asuccV2AainvV0V1V9V5V8V3FIaclosureV6V5V4V15Iainfix =V15V2NFAashortest_pathV0V2V3AainvV0V1V6V5V4V3FF"> @@ -261,7 +261,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="82" loccnumb="6" loccnume="15" expl="parameter fill_next" - sum="040dd8b2220342da80f20c097888387c" + sum="e569d7dfaf2dac12bdf06b2d65ad16b4" proved="true" expanded="false" shape="ainvV0V1V9V5V8V3IamemV12V9NNIainfix =V11aremoveV12V7AamemV12V7FFIais_emptyV7NIainfix =V10aTrueNIais_emptyV7qainfix =V10aTrueFIaclosureV9V5V8V13Iainfix =V13V2NFAasubsetadiffasuccV2V7V9AasubsetV7asuccV2AainvV0V1V9V5V8V3FIaclosureV6V5V4V14Iainfix =V14V2NFAashortest_pathV0V2V3AainvV0V1V6V5V4V3FF"> @@ -281,7 +281,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="82" loccnumb="6" loccnume="15" expl="parameter fill_next" - sum="df55b722207bc0bd834c3ef9e3e361e3" + sum="4f3fe0f16fecacdb8b15abc7a1a5d0b3" proved="false" expanded="false" shape="asubsetV11asuccV2IamemV12V9NNIainfix =V11aremoveV12V7AamemV12V7FFIais_emptyV7NIainfix =V10aTrueNIais_emptyV7qainfix =V10aTrueFIaclosureV9V5V8V13Iainfix =V13V2NFAasubsetadiffasuccV2V7V9AasubsetV7asuccV2AainvV0V1V9V5V8V3FIaclosureV6V5V4V14Iainfix =V14V2NFAashortest_pathV0V2V3AainvV0V1V6V5V4V3FF"> @@ -293,7 +293,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="82" loccnumb="6" loccnume="15" expl="parameter fill_next" - sum="e2ed127f4a86ce2aeb6d0e49054f58e2" + sum="ebd6451e93b84bf3eb307d0ade594b63" proved="true" expanded="false" shape="asubsetadiffasuccV2V11V9IamemV12V9NNIainfix =V11aremoveV12V7AamemV12V7FFIais_emptyV7NIainfix =V10aTrueNIais_emptyV7qainfix =V10aTrueFIaclosureV9V5V8V13Iainfix =V13V2NFAasubsetadiffasuccV2V7V9AasubsetV7asuccV2AainvV0V1V9V5V8V3FIaclosureV6V5V4V14Iainfix =V14V2NFAashortest_pathV0V2V3AainvV0V1V6V5V4V3FF"> @@ -305,7 +305,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.06"/> + <result status="valid" time="0.03"/> </proof> </goal> <goal @@ -313,7 +313,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="82" loccnumb="6" loccnume="15" expl="parameter fill_next" - sum="5bab7122781894586e76247d3328696f" + sum="0dbf57d2a697d541a91d50f251de97f8" proved="true" expanded="true" shape="aclosureV9V5V8V13Iainfix =V13V2NFIamemV12V9NNIainfix =V11aremoveV12V7AamemV12V7FFIais_emptyV7NIainfix =V10aTrueNIais_emptyV7qainfix =V10aTrueFIaclosureV9V5V8V14Iainfix =V14V2NFAasubsetadiffasuccV2V7V9AasubsetV7asuccV2AainvV0V1V9V5V8V3FIaclosureV6V5V4V15Iainfix =V15V2NFAashortest_pathV0V2V3AainvV0V1V6V5V4V3FF"> @@ -328,7 +328,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="82" loccnumb="6" loccnume="15" expl="parameter fill_next" - sum="a81b1caeb18ffd406430a3b00c40a90b" + sum="c159eabf528e7427d3c26bf72bb5a4d8" proved="true" expanded="false" shape="amemV14V9IamemV14asuccV13FIamemV13V8NIamemV13V5NIamemV13V9Iainfix =V13V2NFIamemV12V9NNIainfix =V11aremoveV12V7AamemV12V7FFIamemV15V7NFNIainfix =V10aTrueNIamemV16V7NFqainfix =V10aTrueFIamemV18V9IamemV18asuccV17FIamemV17V8NIamemV17V5NIamemV17V9Iainfix =V17V2NFAamemV19V9IamemV19adiffasuccV2V7FAamemV20asuccV2IamemV20V7FAamemV1V8OamemV1V5IamemV1V9AamemV21V9NOamemV21V8Iashortest_pathV0V21ainfix +V3c1FAainfix <=V23ainfix +V3c1AapathV0V22V23EIamemV22V9FAamemV24V9Iainfix <=V25V3IapathV0V24V25FAashortest_pathV0V26ainfix +V3c1IamemV26V8FAasubsetV8V9Aashortest_pathV0V27V3IamemV27V5FAasubsetV5V9FIamemV29V6IamemV29asuccV28FIamemV28V4NIamemV28V5NIamemV28V6Iainfix =V28V2NFAapathV0V2V30NIainfix <V30V3FAapathV0V2V3AamemV1V4OamemV1V5IamemV1V6AamemV31V6NOamemV31V4Iashortest_pathV0V31ainfix +V3c1FAainfix <=V33ainfix +V3c1AapathV0V32V33EIamemV32V6FAamemV34V6Iainfix <=V35V3IapathV0V34V35FAashortest_pathV0V36ainfix +V3c1IamemV36V4FAasubsetV4V6Aashortest_pathV0V37V3IamemV37V5FAasubsetV5V6FF"> @@ -340,7 +340,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.53"/> + <result status="valid" time="0.38"/> </proof> </goal> </transf> @@ -351,8 +351,8 @@ name="WP_parameter fill_next.5" locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="82" loccnumb="6" loccnume="15" - expl="normal postcondition" - sum="ed62821c33595545bf4177fdb62ae7c8" + expl="postcondition" + sum="7bb16c12e54fc2772685838deea79bb8" proved="true" expanded="true" shape="aclosureV9V5V8V11FAasubsetasuccV2V9AainvV0V1V9V5V8V3Iainfix =V10aTrueNNIais_emptyV7qainfix =V10aTrueFIaclosureV9V5V8V12Iainfix =V12V2NFAasubsetadiffasuccV2V7V9AasubsetV7asuccV2AainvV0V1V9V5V8V3FIaclosureV6V5V4V13Iainfix =V13V2NFAashortest_pathV0V2V3AainvV0V1V6V5V4V3FF"> @@ -367,7 +367,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="82" loccnumb="6" loccnume="15" expl="parameter fill_next" - sum="03f673170c6958813bf7a2cc03a8690f" + sum="4a609634c053bb134ef3f7454edd3be8" proved="true" expanded="false" shape="ainvV0V1V9V5V8V3Iainfix =V10aTrueNNIais_emptyV7qainfix =V10aTrueFIaclosureV9V5V8V11Iainfix =V11V2NFAasubsetadiffasuccV2V7V9AasubsetV7asuccV2AainvV0V1V9V5V8V3FIaclosureV6V5V4V12Iainfix =V12V2NFAashortest_pathV0V2V3AainvV0V1V6V5V4V3FF"> @@ -387,7 +387,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="82" loccnumb="6" loccnume="15" expl="parameter fill_next" - sum="ba027b450ceb922a66b3777ab310b7d6" + sum="74332d9983b2d96dec8199e2cc4a9e24" proved="true" expanded="false" shape="asubsetasuccV2V9Iainfix =V10aTrueNNIais_emptyV7qainfix =V10aTrueFIaclosureV9V5V8V11Iainfix =V11V2NFAasubsetadiffasuccV2V7V9AasubsetV7asuccV2AainvV0V1V9V5V8V3FIaclosureV6V5V4V12Iainfix =V12V2NFAashortest_pathV0V2V3AainvV0V1V6V5V4V3FF"> @@ -399,7 +399,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="3.06"/> + <result status="valid" time="1.05"/> </proof> </goal> <goal @@ -407,7 +407,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="82" loccnumb="6" loccnume="15" expl="parameter fill_next" - sum="e5e86dbf38b1421eb43a518003b28abf" + sum="ba88cc390716930b2d1ac096367afc60" proved="true" expanded="false" shape="aclosureV9V5V8V11FIainfix =V10aTrueNNIais_emptyV7qainfix =V10aTrueFIaclosureV9V5V8V12Iainfix =V12V2NFAasubsetadiffasuccV2V7V9AasubsetV7asuccV2AainvV0V1V9V5V8V3FIaclosureV6V5V4V13Iainfix =V13V2NFAashortest_pathV0V2V3AainvV0V1V6V5V4V3FF"> @@ -419,7 +419,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="1.34"/> + <result status="valid" time="0.38"/> </proof> </goal> </transf> @@ -431,7 +431,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="parameter bfs" - sum="64c03955a57bc552434bc04c11c9e611" + sum="3ed1616d32cb4f72f7cca8a22369491a" proved="true" expanded="true" shape="iainfix =V6aTrueNiainfix =V8V1ashortest_pathV0V1V2iainfix =V11aTrueainfix <=c0V14AaclosureV10V12V13V15FAais_emptyV13Iais_emptyV12AainvV0V1V10V12V13V14Iainfix =V14ainfix +V2c1FIainfix =V13aemptyFIainfix =V12V9Fainfix <=c0V2AaclosureV10V7V9V16FAais_emptyV9Iais_emptyV7AainvV0V1V10V7V9V2Iais_emptyV7qainfix =V11aTrueFIaclosureV10V7V9V17FAasubsetasuccV8V10AainvV0V1V10V7V9V2FAaclosureV5V7V3V18Iainfix =V18V8NFAashortest_pathV0V8V2AainvV0V1V5V7V3V2Iainfix =V7aremoveV8V4AamemV8V4FFAais_emptyV4NapathV0V1V19NFAamemV1V5NIais_emptyV4qainfix =V6aTrueFIainfix <=c0V2AaclosureV5V4V3V20FAais_emptyV3Iais_emptyV4AainvV0V1V5V4V3V2FAainfix <=c0c0AaclosureasingletonV0asingletonV0aemptyV21FAais_emptyaemptyIais_emptyasingletonV0AainvV0V1asingletonV0asingletonV0aemptyc0F"> @@ -446,7 +446,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="loop invariant init" - sum="a1addcb35e0c35bed146b4d83d4ec81f" + sum="137a0881252d3d22effe133b610740a9" proved="true" expanded="true" shape="ainfix <=c0c0AaclosureasingletonV0asingletonV0aemptyV2FAais_emptyaemptyIais_emptyasingletonV0AainvV0V1asingletonV0asingletonV0aemptyc0F"> @@ -461,7 +461,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="parameter bfs" - sum="a735cf50e600c729b0b220a8292e5093" + sum="84ca72fe7149a071450c0071a9aa0ba3" proved="true" expanded="false" shape="ainvV0V1asingletonV0asingletonV0aemptyc0F"> @@ -473,7 +473,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.42"/> + <result status="valid" time="0.32"/> </proof> </goal> <goal @@ -481,7 +481,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="parameter bfs" - sum="ecb7aca754c58738ec6ee3c63c9ba4c3" + sum="33ea4b859ea8a3d51d488cc33bb043e0" proved="true" expanded="false" shape="ais_emptyaemptyIais_emptyasingletonV0F"> @@ -493,7 +493,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.01"/> + <result status="valid" time="0.02"/> </proof> </goal> <goal @@ -501,7 +501,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="parameter bfs" - sum="558f950431783cb897fb3aac8beab5a1" + sum="fc730c99319c3d75da264e038dd4399c" proved="true" expanded="true" shape="aclosureasingletonV0asingletonV0aemptyV2FF"> @@ -516,7 +516,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="parameter bfs" - sum="b73bf8618d4eeaf86e71a70b2a2865c6" + sum="ced18c7247bd980ad17165f6d4ae8067" proved="true" expanded="false" shape="amemV3asingletonV0IamemV3asuccV2FIamemV2aemptyNIamemV2asingletonV0NIamemV2asingletonV0FF"> @@ -538,7 +538,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="parameter bfs" - sum="e83ac3e699395db0d96c43e234013dee" + sum="df60d66975f7aebf9a74dede19862d47" proved="true" expanded="false" shape="ainfix <=c0c0F"> @@ -560,7 +560,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="precondition" - sum="244ac7e4c1547766f530c93bd320d319" + sum="101118ab43fc391c4b2cded990254c15" proved="true" expanded="false" shape="ais_emptyV4NIainfix =V6aTrueNIais_emptyV4qainfix =V6aTrueFIainfix <=c0V2AaclosureV5V4V3V7FAais_emptyV3Iais_emptyV4AainvV0V1V5V4V3V2FF"> @@ -572,7 +572,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.01"/> + <result status="valid" time="0.02"/> </proof> </goal> <goal @@ -580,7 +580,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="exceptional postcondition" - sum="1da4c8a8c320f7e52bb359fc4a84636d" + sum="3045c0eed9bf41fdd9ee74217facf69e" proved="true" expanded="false" shape="ashortest_pathV0V1V2Iainfix =V8V1Iainfix =V7aremoveV8V4AamemV8V4FFIais_emptyV4NIainfix =V6aTrueNIais_emptyV4qainfix =V6aTrueFIainfix <=c0V2AaclosureV5V4V3V9FAais_emptyV3Iais_emptyV4AainvV0V1V5V4V3V2FF"> @@ -592,7 +592,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.02"/> + <result status="valid" time="0.01"/> </proof> </goal> <goal @@ -600,7 +600,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="precondition" - sum="e884fc819d8ccf10ee0d51a34056d8d1" + sum="8c684545cc5b5e3d11ad22885c3d9252" proved="true" expanded="true" shape="aclosureV5V7V3V9Iainfix =V9V8NFAashortest_pathV0V8V2AainvV0V1V5V7V3V2Iainfix =V8V1NIainfix =V7aremoveV8V4AamemV8V4FFIais_emptyV4NIainfix =V6aTrueNIais_emptyV4qainfix =V6aTrueFIainfix <=c0V2AaclosureV5V4V3V10FAais_emptyV3Iais_emptyV4AainvV0V1V5V4V3V2FF"> @@ -615,7 +615,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="parameter bfs" - sum="fa98fd5253415937c8d8ba32163335cb" + sum="d3d8414ad4fbc82646f704786636a424" proved="true" expanded="false" shape="ainvV0V1V5V7V3V2Iainfix =V8V1NIainfix =V7aremoveV8V4AamemV8V4FFIais_emptyV4NIainfix =V6aTrueNIais_emptyV4qainfix =V6aTrueFIainfix <=c0V2AaclosureV5V4V3V9FAais_emptyV3Iais_emptyV4AainvV0V1V5V4V3V2FF"> @@ -627,7 +627,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.30"/> + <result status="valid" time="0.20"/> </proof> </goal> <goal @@ -635,7 +635,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="parameter bfs" - sum="4071feff765c08ee463511572bd76045" + sum="8e7e3487e492a7746b86f099c9b157fe" proved="true" expanded="false" shape="ashortest_pathV0V8V2Iainfix =V8V1NIainfix =V7aremoveV8V4AamemV8V4FFIais_emptyV4NIainfix =V6aTrueNIais_emptyV4qainfix =V6aTrueFIainfix <=c0V2AaclosureV5V4V3V9FAais_emptyV3Iais_emptyV4AainvV0V1V5V4V3V2FF"> @@ -647,7 +647,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.00"/> + <result status="valid" time="0.01"/> </proof> </goal> <goal @@ -655,7 +655,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="parameter bfs" - sum="eb14c3aca130af7c7806aee8f9cffc6f" + sum="ab7bf578cc7d3c5a63de6f78ac4335dd" proved="true" expanded="true" shape="aclosureV5V7V3V9Iainfix =V9V8NFIainfix =V8V1NIainfix =V7aremoveV8V4AamemV8V4FFIais_emptyV4NIainfix =V6aTrueNIais_emptyV4qainfix =V6aTrueFIainfix <=c0V2AaclosureV5V4V3V10FAais_emptyV3Iais_emptyV4AainvV0V1V5V4V3V2FF"> @@ -670,7 +670,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="parameter bfs" - sum="f7638110d2aa7a6e93909098d30317a7" + sum="7fe8c2da48f33012188d4b5e73843c30" proved="true" expanded="false" shape="amemV10V5IamemV10asuccV9FIamemV9V3NIamemV9V7NIamemV9V5Iainfix =V9V8NFIainfix =V8V1NIainfix =V7aremoveV8V4AamemV8V4FFIamemV11V4NFNIainfix =V6aTrueNIamemV12V4NFqainfix =V6aTrueFIainfix =c0V2Oainfix <c0V2AamemV14V5IamemV14asuccV13FIamemV13V3NIamemV13V4NIamemV13V5FAamemV15V3NFIamemV16V4NFAamemV1V3OamemV1V4IamemV1V5AamemV17V5NOamemV17V3Iashortest_pathV0V17ainfix +V2c1FAainfix <=V19ainfix +V2c1AapathV0V18V19EIamemV18V5FAamemV20V5Iainfix <=V21V2IapathV0V20V21FAashortest_pathV0V22ainfix +V2c1IamemV22V3FAasubsetV3V5Aashortest_pathV0V23V2IamemV23V4FAasubsetV4V5FF"> @@ -682,7 +682,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.03"/> + <result status="valid" time="0.02"/> </proof> </goal> </transf> @@ -694,7 +694,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="loop invariant preservation" - sum="4aee1d20f2f2545d2236a3269bc6f09f" + sum="1e11aae350a89f35cdf0af29bda434e3" proved="true" expanded="true" shape="ainfix <=c0V14AaclosureV10V12V13V15FAais_emptyV13Iais_emptyV12AainvV0V1V10V12V13V14Iainfix =V14ainfix +V2c1FIainfix =V13aemptyFIainfix =V12V9FIainfix =V11aTrueIais_emptyV7qainfix =V11aTrueFIaclosureV10V7V9V16FAasubsetasuccV8V10AainvV0V1V10V7V9V2FIaclosureV5V7V3V17Iainfix =V17V8NFAashortest_pathV0V8V2AainvV0V1V5V7V3V2Iainfix =V8V1NIainfix =V7aremoveV8V4AamemV8V4FFIais_emptyV4NIainfix =V6aTrueNIais_emptyV4qainfix =V6aTrueFIainfix <=c0V2AaclosureV5V4V3V18FAais_emptyV3Iais_emptyV4AainvV0V1V5V4V3V2FF"> @@ -709,7 +709,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="parameter bfs" - sum="14cec615ac8f891c06c1852a9f197b3c" + sum="c82fbd22a32bd9ed4ab77e0b479dfc15" proved="true" expanded="true" shape="ainvV0V1V10V12V13V14Iainfix =V14ainfix +V2c1FIainfix =V13aemptyFIainfix =V12V9FIainfix =V11aTrueIais_emptyV7qainfix =V11aTrueFIaclosureV10V7V9V15FAasubsetasuccV8V10AainvV0V1V10V7V9V2FIaclosureV5V7V3V16Iainfix =V16V8NFAashortest_pathV0V8V2AainvV0V1V5V7V3V2Iainfix =V8V1NIainfix =V7aremoveV8V4AamemV8V4FFIais_emptyV4NIainfix =V6aTrueNIais_emptyV4qainfix =V6aTrueFIainfix <=c0V2AaclosureV5V4V3V17FAais_emptyV3Iais_emptyV4AainvV0V1V5V4V3V2FF"> @@ -724,7 +724,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="parameter bfs" - sum="cfc00f93de5c97b380ffa979c80664a6" + sum="52703e04456c16c2e2a365c5d12ac16c" proved="true" expanded="true" shape="amemV1V13OamemV1V12IamemV1V10AamemV15V10NOamemV15V13Iashortest_pathV0V15ainfix +V14c1FAainfix <=V17ainfix +V14c1AapathV0V16V17EIamemV16V10FAamemV18V10Iainfix <=V19V14IapathV0V18V19FAashortest_pathV0V20ainfix +V14c1IamemV20V13FAasubsetV13V10Aashortest_pathV0V21V14IamemV21V12FAasubsetV12V10Iainfix =V14ainfix +V2c1FIainfix =V13aemptyFIainfix =V12V9FIainfix =V11aTrueIamemV22V7NFqainfix =V11aTrueFIamemV24V10IamemV24asuccV23FIamemV23V9NIamemV23V7NIamemV23V10FAamemV25V10IamemV25asuccV8FAamemV1V9OamemV1V7IamemV1V10AamemV26V10NOamemV26V9Iashortest_pathV0V26ainfix +V2c1FAainfix <=V28ainfix +V2c1AapathV0V27V28EIamemV27V10FAamemV29V10Iainfix <=V30V2IapathV0V29V30FAashortest_pathV0V31ainfix +V2c1IamemV31V9FAasubsetV9V10Aashortest_pathV0V32V2IamemV32V7FAasubsetV7V10FIamemV34V5IamemV34asuccV33FIamemV33V3NIamemV33V7NIamemV33V5Iainfix =V33V8NFAapathV0V8V35NIainfix <V35V2FAapathV0V8V2AamemV1V3OamemV1V7IamemV1V5AamemV36V5NOamemV36V3Iashortest_pathV0V36ainfix +V2c1FAainfix <=V38ainfix +V2c1AapathV0V37V38EIamemV37V5FAamemV39V5Iainfix <=V40V2IapathV0V39V40FAashortest_pathV0V41ainfix +V2c1IamemV41V3FAasubsetV3V5Aashortest_pathV0V42V2IamemV42V7FAasubsetV7V5Iainfix =V8V1NIainfix =V7aremoveV8V4AamemV8V4FFIamemV43V4NFNIainfix =V6aTrueNIamemV44V4NFqainfix =V6aTrueFIainfix =c0V2Oainfix <c0V2AamemV46V5IamemV46asuccV45FIamemV45V3NIamemV45V4NIamemV45V5FAamemV47V3NFIamemV48V4NFAamemV1V3OamemV1V4IamemV1V5AamemV49V5NOamemV49V3Iashortest_pathV0V49ainfix +V2c1FAainfix <=V51ainfix +V2c1AapathV0V50V51EIamemV50V5FAamemV52V5Iainfix <=V53V2IapathV0V52V53FAashortest_pathV0V54ainfix +V2c1IamemV54V3FAasubsetV3V5Aashortest_pathV0V55V2IamemV55V4FAasubsetV4V5FF"> @@ -739,7 +739,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="parameter bfs" - sum="ccf8de8e0768b8e4fae0f006ec7497d2" + sum="bee895155b5abfc1921ec701d03fb0c3" proved="true" expanded="false" shape="asubsetV12V10Iainfix =V14ainfix +V2c1FIainfix =V13aemptyFIainfix =V12V9FIainfix =V11aTrueIamemV15V7NFqainfix =V11aTrueFIamemV17V10IamemV17asuccV16FIamemV16V9NIamemV16V7NIamemV16V10FAamemV18V10IamemV18asuccV8FAamemV1V9OamemV1V7IamemV1V10AamemV19V10NOamemV19V9Iashortest_pathV0V19ainfix +V2c1FAainfix <=V21ainfix +V2c1AapathV0V20V21EIamemV20V10FAamemV22V10Iainfix <=V23V2IapathV0V22V23FAashortest_pathV0V24ainfix +V2c1IamemV24V9FAasubsetV9V10Aashortest_pathV0V25V2IamemV25V7FAasubsetV7V10FIamemV27V5IamemV27asuccV26FIamemV26V3NIamemV26V7NIamemV26V5Iainfix =V26V8NFAapathV0V8V28NIainfix <V28V2FAapathV0V8V2AamemV1V3OamemV1V7IamemV1V5AamemV29V5NOamemV29V3Iashortest_pathV0V29ainfix +V2c1FAainfix <=V31ainfix +V2c1AapathV0V30V31EIamemV30V5FAamemV32V5Iainfix <=V33V2IapathV0V32V33FAashortest_pathV0V34ainfix +V2c1IamemV34V3FAasubsetV3V5Aashortest_pathV0V35V2IamemV35V7FAasubsetV7V5Iainfix =V8V1NIainfix =V7aremoveV8V4AamemV8V4FFIamemV36V4NFNIainfix =V6aTrueNIamemV37V4NFqainfix =V6aTrueFIainfix =c0V2Oainfix <c0V2AamemV39V5IamemV39asuccV38FIamemV38V3NIamemV38V4NIamemV38V5FAamemV40V3NFIamemV41V4NFAamemV1V3OamemV1V4IamemV1V5AamemV42V5NOamemV42V3Iashortest_pathV0V42ainfix +V2c1FAainfix <=V44ainfix +V2c1AapathV0V43V44EIamemV43V5FAamemV45V5Iainfix <=V46V2IapathV0V45V46FAashortest_pathV0V47ainfix +V2c1IamemV47V3FAasubsetV3V5Aashortest_pathV0V48V2IamemV48V4FAasubsetV4V5FF"> @@ -759,7 +759,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="parameter bfs" - sum="50abe3bbc2750f61c89363ae117a9d61" + sum="4fd9efc61a08435ffbd858f390f69230" proved="true" expanded="false" shape="ashortest_pathV0V15V14IamemV15V12FIainfix =V14ainfix +V2c1FIainfix =V13aemptyFIainfix =V12V9FIainfix =V11aTrueIamemV16V7NFqainfix =V11aTrueFIamemV18V10IamemV18asuccV17FIamemV17V9NIamemV17V7NIamemV17V10FAamemV19V10IamemV19asuccV8FAamemV1V9OamemV1V7IamemV1V10AamemV20V10NOamemV20V9Iashortest_pathV0V20ainfix +V2c1FAainfix <=V22ainfix +V2c1AapathV0V21V22EIamemV21V10FAamemV23V10Iainfix <=V24V2IapathV0V23V24FAashortest_pathV0V25ainfix +V2c1IamemV25V9FAasubsetV9V10Aashortest_pathV0V26V2IamemV26V7FAasubsetV7V10FIamemV28V5IamemV28asuccV27FIamemV27V3NIamemV27V7NIamemV27V5Iainfix =V27V8NFAapathV0V8V29NIainfix <V29V2FAapathV0V8V2AamemV1V3OamemV1V7IamemV1V5AamemV30V5NOamemV30V3Iashortest_pathV0V30ainfix +V2c1FAainfix <=V32ainfix +V2c1AapathV0V31V32EIamemV31V5FAamemV33V5Iainfix <=V34V2IapathV0V33V34FAashortest_pathV0V35ainfix +V2c1IamemV35V3FAasubsetV3V5Aashortest_pathV0V36V2IamemV36V7FAasubsetV7V5Iainfix =V8V1NIainfix =V7aremoveV8V4AamemV8V4FFIamemV37V4NFNIainfix =V6aTrueNIamemV38V4NFqainfix =V6aTrueFIainfix =c0V2Oainfix <c0V2AamemV40V5IamemV40asuccV39FIamemV39V3NIamemV39V4NIamemV39V5FAamemV41V3NFIamemV42V4NFAamemV1V3OamemV1V4IamemV1V5AamemV43V5NOamemV43V3Iashortest_pathV0V43ainfix +V2c1FAainfix <=V45ainfix +V2c1AapathV0V44V45EIamemV44V5FAamemV46V5Iainfix <=V47V2IapathV0V46V47FAashortest_pathV0V48ainfix +V2c1IamemV48V3FAasubsetV3V5Aashortest_pathV0V49V2IamemV49V4FAasubsetV4V5FF"> @@ -779,7 +779,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="parameter bfs" - sum="44c0f77fe409540709db3f45450c3d93" + sum="02596d92203049e7c675fe9b9eb091b2" proved="true" expanded="false" shape="asubsetV13V10Iainfix =V14ainfix +V2c1FIainfix =V13aemptyFIainfix =V12V9FIainfix =V11aTrueIamemV15V7NFqainfix =V11aTrueFIamemV17V10IamemV17asuccV16FIamemV16V9NIamemV16V7NIamemV16V10FAamemV18V10IamemV18asuccV8FAamemV1V9OamemV1V7IamemV1V10AamemV19V10NOamemV19V9Iashortest_pathV0V19ainfix +V2c1FAainfix <=V21ainfix +V2c1AapathV0V20V21EIamemV20V10FAamemV22V10Iainfix <=V23V2IapathV0V22V23FAashortest_pathV0V24ainfix +V2c1IamemV24V9FAasubsetV9V10Aashortest_pathV0V25V2IamemV25V7FAasubsetV7V10FIamemV27V5IamemV27asuccV26FIamemV26V3NIamemV26V7NIamemV26V5Iainfix =V26V8NFAapathV0V8V28NIainfix <V28V2FAapathV0V8V2AamemV1V3OamemV1V7IamemV1V5AamemV29V5NOamemV29V3Iashortest_pathV0V29ainfix +V2c1FAainfix <=V31ainfix +V2c1AapathV0V30V31EIamemV30V5FAamemV32V5Iainfix <=V33V2IapathV0V32V33FAashortest_pathV0V34ainfix +V2c1IamemV34V3FAasubsetV3V5Aashortest_pathV0V35V2IamemV35V7FAasubsetV7V5Iainfix =V8V1NIainfix =V7aremoveV8V4AamemV8V4FFIamemV36V4NFNIainfix =V6aTrueNIamemV37V4NFqainfix =V6aTrueFIainfix =c0V2Oainfix <c0V2AamemV39V5IamemV39asuccV38FIamemV38V3NIamemV38V4NIamemV38V5FAamemV40V3NFIamemV41V4NFAamemV1V3OamemV1V4IamemV1V5AamemV42V5NOamemV42V3Iashortest_pathV0V42ainfix +V2c1FAainfix <=V44ainfix +V2c1AapathV0V43V44EIamemV43V5FAamemV45V5Iainfix <=V46V2IapathV0V45V46FAashortest_pathV0V47ainfix +V2c1IamemV47V3FAasubsetV3V5Aashortest_pathV0V48V2IamemV48V4FAasubsetV4V5FF"> @@ -799,7 +799,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="parameter bfs" - sum="274dcdb743ab10df718aa11eb9d35a36" + sum="d516807d2d58f066cef3926116f0b91a" proved="true" expanded="false" shape="ashortest_pathV0V15ainfix +V14c1IamemV15V13FIainfix =V14ainfix +V2c1FIainfix =V13aemptyFIainfix =V12V9FIainfix =V11aTrueIamemV16V7NFqainfix =V11aTrueFIamemV18V10IamemV18asuccV17FIamemV17V9NIamemV17V7NIamemV17V10FAamemV19V10IamemV19asuccV8FAamemV1V9OamemV1V7IamemV1V10AamemV20V10NOamemV20V9Iashortest_pathV0V20ainfix +V2c1FAainfix <=V22ainfix +V2c1AapathV0V21V22EIamemV21V10FAamemV23V10Iainfix <=V24V2IapathV0V23V24FAashortest_pathV0V25ainfix +V2c1IamemV25V9FAasubsetV9V10Aashortest_pathV0V26V2IamemV26V7FAasubsetV7V10FIamemV28V5IamemV28asuccV27FIamemV27V3NIamemV27V7NIamemV27V5Iainfix =V27V8NFAapathV0V8V29NIainfix <V29V2FAapathV0V8V2AamemV1V3OamemV1V7IamemV1V5AamemV30V5NOamemV30V3Iashortest_pathV0V30ainfix +V2c1FAainfix <=V32ainfix +V2c1AapathV0V31V32EIamemV31V5FAamemV33V5Iainfix <=V34V2IapathV0V33V34FAashortest_pathV0V35ainfix +V2c1IamemV35V3FAasubsetV3V5Aashortest_pathV0V36V2IamemV36V7FAasubsetV7V5Iainfix =V8V1NIainfix =V7aremoveV8V4AamemV8V4FFIamemV37V4NFNIainfix =V6aTrueNIamemV38V4NFqainfix =V6aTrueFIainfix =c0V2Oainfix <c0V2AamemV40V5IamemV40asuccV39FIamemV39V3NIamemV39V4NIamemV39V5FAamemV41V3NFIamemV42V4NFAamemV1V3OamemV1V4IamemV1V5AamemV43V5NOamemV43V3Iashortest_pathV0V43ainfix +V2c1FAainfix <=V45ainfix +V2c1AapathV0V44V45EIamemV44V5FAamemV46V5Iainfix <=V47V2IapathV0V46V47FAashortest_pathV0V48ainfix +V2c1IamemV48V3FAasubsetV3V5Aashortest_pathV0V49V2IamemV49V4FAasubsetV4V5FF"> @@ -811,7 +811,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.03"/> + <result status="valid" time="0.04"/> </proof> </goal> <goal @@ -819,7 +819,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="parameter bfs" - sum="02eb452bc52be1e2ce26af4110b85bf5" + sum="79872893781a55c7902d00b3cbaf9975" proved="true" expanded="false" shape="amemV15V10Iainfix <=V16V14IapathV0V15V16FIainfix =V14ainfix +V2c1FIainfix =V13aemptyFIainfix =V12V9FIainfix =V11aTrueIamemV17V7NFqainfix =V11aTrueFIamemV19V10IamemV19asuccV18FIamemV18V9NIamemV18V7NIamemV18V10FAamemV20V10IamemV20asuccV8FAamemV1V9OamemV1V7IamemV1V10AamemV21V10NOamemV21V9Iashortest_pathV0V21ainfix +V2c1FAainfix <=V23ainfix +V2c1AapathV0V22V23EIamemV22V10FAamemV24V10Iainfix <=V25V2IapathV0V24V25FAashortest_pathV0V26ainfix +V2c1IamemV26V9FAasubsetV9V10Aashortest_pathV0V27V2IamemV27V7FAasubsetV7V10FIamemV29V5IamemV29asuccV28FIamemV28V3NIamemV28V7NIamemV28V5Iainfix =V28V8NFAapathV0V8V30NIainfix <V30V2FAapathV0V8V2AamemV1V3OamemV1V7IamemV1V5AamemV31V5NOamemV31V3Iashortest_pathV0V31ainfix +V2c1FAainfix <=V33ainfix +V2c1AapathV0V32V33EIamemV32V5FAamemV34V5Iainfix <=V35V2IapathV0V34V35FAashortest_pathV0V36ainfix +V2c1IamemV36V3FAasubsetV3V5Aashortest_pathV0V37V2IamemV37V7FAasubsetV7V5Iainfix =V8V1NIainfix =V7aremoveV8V4AamemV8V4FFIamemV38V4NFNIainfix =V6aTrueNIamemV39V4NFqainfix =V6aTrueFIainfix =c0V2Oainfix <c0V2AamemV41V5IamemV41asuccV40FIamemV40V3NIamemV40V4NIamemV40V5FAamemV42V3NFIamemV43V4NFAamemV1V3OamemV1V4IamemV1V5AamemV44V5NOamemV44V3Iashortest_pathV0V44ainfix +V2c1FAainfix <=V46ainfix +V2c1AapathV0V45V46EIamemV45V5FAamemV47V5Iainfix <=V48V2IapathV0V47V48FAashortest_pathV0V49ainfix +V2c1IamemV49V3FAasubsetV3V5Aashortest_pathV0V50V2IamemV50V4FAasubsetV4V5FF"> @@ -831,7 +831,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.03"/> + <result status="valid" time="0.04"/> </proof> </goal> <goal @@ -839,7 +839,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="parameter bfs" - sum="06ee49cff98ed500a602fec7621215c1" + sum="12ebca8701e8acc54d05da3b5758e2cd" proved="true" expanded="false" shape="ainfix <=V16ainfix +V14c1AapathV0V15V16EIamemV15V10FIainfix =V14ainfix +V2c1FIainfix =V13aemptyFIainfix =V12V9FIainfix =V11aTrueIamemV17V7NFqainfix =V11aTrueFIamemV19V10IamemV19asuccV18FIamemV18V9NIamemV18V7NIamemV18V10FAamemV20V10IamemV20asuccV8FAamemV1V9OamemV1V7IamemV1V10AamemV21V10NOamemV21V9Iashortest_pathV0V21ainfix +V2c1FAainfix <=V23ainfix +V2c1AapathV0V22V23EIamemV22V10FAamemV24V10Iainfix <=V25V2IapathV0V24V25FAashortest_pathV0V26ainfix +V2c1IamemV26V9FAasubsetV9V10Aashortest_pathV0V27V2IamemV27V7FAasubsetV7V10FIamemV29V5IamemV29asuccV28FIamemV28V3NIamemV28V7NIamemV28V5Iainfix =V28V8NFAapathV0V8V30NIainfix <V30V2FAapathV0V8V2AamemV1V3OamemV1V7IamemV1V5AamemV31V5NOamemV31V3Iashortest_pathV0V31ainfix +V2c1FAainfix <=V33ainfix +V2c1AapathV0V32V33EIamemV32V5FAamemV34V5Iainfix <=V35V2IapathV0V34V35FAashortest_pathV0V36ainfix +V2c1IamemV36V3FAasubsetV3V5Aashortest_pathV0V37V2IamemV37V7FAasubsetV7V5Iainfix =V8V1NIainfix =V7aremoveV8V4AamemV8V4FFIamemV38V4NFNIainfix =V6aTrueNIamemV39V4NFqainfix =V6aTrueFIainfix =c0V2Oainfix <c0V2AamemV41V5IamemV41asuccV40FIamemV40V3NIamemV40V4NIamemV40V5FAamemV42V3NFIamemV43V4NFAamemV1V3OamemV1V4IamemV1V5AamemV44V5NOamemV44V3Iashortest_pathV0V44ainfix +V2c1FAainfix <=V46ainfix +V2c1AapathV0V45V46EIamemV45V5FAamemV47V5Iainfix <=V48V2IapathV0V47V48FAashortest_pathV0V49ainfix +V2c1IamemV49V3FAasubsetV3V5Aashortest_pathV0V50V2IamemV50V4FAasubsetV4V5FF"> @@ -851,7 +851,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="2.93"/> + <result status="valid" time="2.39"/> </proof> </goal> <goal @@ -859,7 +859,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="parameter bfs" - sum="165c88279bbbfdba6a991a59942cf694" + sum="c72db32d71bfab12f696a8f0b86978a8" proved="true" expanded="false" shape="amemV15V10NOamemV15V13Iashortest_pathV0V15ainfix +V14c1FIainfix =V14ainfix +V2c1FIainfix =V13aemptyFIainfix =V12V9FIainfix =V11aTrueIamemV16V7NFqainfix =V11aTrueFIamemV18V10IamemV18asuccV17FIamemV17V9NIamemV17V7NIamemV17V10FAamemV19V10IamemV19asuccV8FAamemV1V9OamemV1V7IamemV1V10AamemV20V10NOamemV20V9Iashortest_pathV0V20ainfix +V2c1FAainfix <=V22ainfix +V2c1AapathV0V21V22EIamemV21V10FAamemV23V10Iainfix <=V24V2IapathV0V23V24FAashortest_pathV0V25ainfix +V2c1IamemV25V9FAasubsetV9V10Aashortest_pathV0V26V2IamemV26V7FAasubsetV7V10FIamemV28V5IamemV28asuccV27FIamemV27V3NIamemV27V7NIamemV27V5Iainfix =V27V8NFAapathV0V8V29NIainfix <V29V2FAapathV0V8V2AamemV1V3OamemV1V7IamemV1V5AamemV30V5NOamemV30V3Iashortest_pathV0V30ainfix +V2c1FAainfix <=V32ainfix +V2c1AapathV0V31V32EIamemV31V5FAamemV33V5Iainfix <=V34V2IapathV0V33V34FAashortest_pathV0V35ainfix +V2c1IamemV35V3FAasubsetV3V5Aashortest_pathV0V36V2IamemV36V7FAasubsetV7V5Iainfix =V8V1NIainfix =V7aremoveV8V4AamemV8V4FFIamemV37V4NFNIainfix =V6aTrueNIamemV38V4NFqainfix =V6aTrueFIainfix =c0V2Oainfix <c0V2AamemV40V5IamemV40asuccV39FIamemV39V3NIamemV39V4NIamemV39V5FAamemV41V3NFIamemV42V4NFAamemV1V3OamemV1V4IamemV1V5AamemV43V5NOamemV43V3Iashortest_pathV0V43ainfix +V2c1FAainfix <=V45ainfix +V2c1AapathV0V44V45EIamemV44V5FAamemV46V5Iainfix <=V47V2IapathV0V46V47FAashortest_pathV0V48ainfix +V2c1IamemV48V3FAasubsetV3V5Aashortest_pathV0V49V2IamemV49V4FAasubsetV4V5FF"> @@ -871,7 +871,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.06"/> + <result status="valid" time="0.05"/> </proof> </goal> <goal @@ -879,7 +879,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="parameter bfs" - sum="2eb6b18f20e6101965d5792fd84ce48c" + sum="ee537851324723667d3a3c955ec0517c" proved="true" expanded="false" shape="amemV1V13OamemV1V12IamemV1V10Iainfix =V14ainfix +V2c1FIainfix =V13aemptyFIainfix =V12V9FIainfix =V11aTrueIamemV15V7NFqainfix =V11aTrueFIamemV17V10IamemV17asuccV16FIamemV16V9NIamemV16V7NIamemV16V10FAamemV18V10IamemV18asuccV8FAamemV1V9OamemV1V7IamemV1V10AamemV19V10NOamemV19V9Iashortest_pathV0V19ainfix +V2c1FAainfix <=V21ainfix +V2c1AapathV0V20V21EIamemV20V10FAamemV22V10Iainfix <=V23V2IapathV0V22V23FAashortest_pathV0V24ainfix +V2c1IamemV24V9FAasubsetV9V10Aashortest_pathV0V25V2IamemV25V7FAasubsetV7V10FIamemV27V5IamemV27asuccV26FIamemV26V3NIamemV26V7NIamemV26V5Iainfix =V26V8NFAapathV0V8V28NIainfix <V28V2FAapathV0V8V2AamemV1V3OamemV1V7IamemV1V5AamemV29V5NOamemV29V3Iashortest_pathV0V29ainfix +V2c1FAainfix <=V31ainfix +V2c1AapathV0V30V31EIamemV30V5FAamemV32V5Iainfix <=V33V2IapathV0V32V33FAashortest_pathV0V34ainfix +V2c1IamemV34V3FAasubsetV3V5Aashortest_pathV0V35V2IamemV35V7FAasubsetV7V5Iainfix =V8V1NIainfix =V7aremoveV8V4AamemV8V4FFIamemV36V4NFNIainfix =V6aTrueNIamemV37V4NFqainfix =V6aTrueFIainfix =c0V2Oainfix <c0V2AamemV39V5IamemV39asuccV38FIamemV38V3NIamemV38V4NIamemV38V5FAamemV40V3NFIamemV41V4NFAamemV1V3OamemV1V4IamemV1V5AamemV42V5NOamemV42V3Iashortest_pathV0V42ainfix +V2c1FAainfix <=V44ainfix +V2c1AapathV0V43V44EIamemV43V5FAamemV45V5Iainfix <=V46V2IapathV0V45V46FAashortest_pathV0V47ainfix +V2c1IamemV47V3FAasubsetV3V5Aashortest_pathV0V48V2IamemV48V4FAasubsetV4V5FF"> @@ -891,7 +891,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.11"/> + <result status="valid" time="0.08"/> </proof> </goal> </transf> @@ -903,7 +903,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="parameter bfs" - sum="2dafea62332c7a738c23559b1b9ef407" + sum="8184c481251162323e5037b6df45f435" proved="true" expanded="false" shape="ais_emptyV13Iais_emptyV12Iainfix =V14ainfix +V2c1FIainfix =V13aemptyFIainfix =V12V9FIainfix =V11aTrueIais_emptyV7qainfix =V11aTrueFIaclosureV10V7V9V15FAasubsetasuccV8V10AainvV0V1V10V7V9V2FIaclosureV5V7V3V16Iainfix =V16V8NFAashortest_pathV0V8V2AainvV0V1V5V7V3V2Iainfix =V8V1NIainfix =V7aremoveV8V4AamemV8V4FFIais_emptyV4NIainfix =V6aTrueNIais_emptyV4qainfix =V6aTrueFIainfix <=c0V2AaclosureV5V4V3V17FAais_emptyV3Iais_emptyV4AainvV0V1V5V4V3V2FF"> @@ -915,7 +915,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.01"/> + <result status="valid" time="0.02"/> </proof> </goal> <goal @@ -923,7 +923,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="parameter bfs" - sum="538e4e3f99210ff24e60a3ee7af40615" + sum="adfc9035219db4d3193f0012e579213f" proved="true" expanded="false" shape="aclosureV10V12V13V15FIainfix =V14ainfix +V2c1FIainfix =V13aemptyFIainfix =V12V9FIainfix =V11aTrueIais_emptyV7qainfix =V11aTrueFIaclosureV10V7V9V16FAasubsetasuccV8V10AainvV0V1V10V7V9V2FIaclosureV5V7V3V17Iainfix =V17V8NFAashortest_pathV0V8V2AainvV0V1V5V7V3V2Iainfix =V8V1NIainfix =V7aremoveV8V4AamemV8V4FFIais_emptyV4NIainfix =V6aTrueNIais_emptyV4qainfix =V6aTrueFIainfix <=c0V2AaclosureV5V4V3V18FAais_emptyV3Iais_emptyV4AainvV0V1V5V4V3V2FF"> @@ -935,7 +935,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.08"/> + <result status="valid" time="0.11"/> </proof> </goal> <goal @@ -943,7 +943,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="parameter bfs" - sum="65f54c84962574d99e130f4959020e2b" + sum="84421e1bd9c749b948373e906c242901" proved="true" expanded="false" shape="ainfix <=c0V14Iainfix =V14ainfix +V2c1FIainfix =V13aemptyFIainfix =V12V9FIainfix =V11aTrueIais_emptyV7qainfix =V11aTrueFIaclosureV10V7V9V15FAasubsetasuccV8V10AainvV0V1V10V7V9V2FIaclosureV5V7V3V16Iainfix =V16V8NFAashortest_pathV0V8V2AainvV0V1V5V7V3V2Iainfix =V8V1NIainfix =V7aremoveV8V4AamemV8V4FFIais_emptyV4NIainfix =V6aTrueNIais_emptyV4qainfix =V6aTrueFIainfix <=c0V2AaclosureV5V4V3V17FAais_emptyV3Iais_emptyV4AainvV0V1V5V4V3V2FF"> @@ -965,7 +965,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="loop invariant preservation" - sum="9d275e6f40d94de4a8cc73ed53de3653" + sum="ca044d2601ef3e5ff0ddcc59e579fa4f" proved="true" expanded="true" shape="ainfix <=c0V2AaclosureV10V7V9V12FAais_emptyV9Iais_emptyV7AainvV0V1V10V7V9V2Iainfix =V11aTrueNIais_emptyV7qainfix =V11aTrueFIaclosureV10V7V9V13FAasubsetasuccV8V10AainvV0V1V10V7V9V2FIaclosureV5V7V3V14Iainfix =V14V8NFAashortest_pathV0V8V2AainvV0V1V5V7V3V2Iainfix =V8V1NIainfix =V7aremoveV8V4AamemV8V4FFIais_emptyV4NIainfix =V6aTrueNIais_emptyV4qainfix =V6aTrueFIainfix <=c0V2AaclosureV5V4V3V15FAais_emptyV3Iais_emptyV4AainvV0V1V5V4V3V2FF"> @@ -980,7 +980,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="parameter bfs" - sum="1b899a2a427063111f6257e5fb266e4f" + sum="8c99963be40d685e695150947fb6ee3d" proved="true" expanded="false" shape="ainvV0V1V10V7V9V2Iainfix =V11aTrueNIais_emptyV7qainfix =V11aTrueFIaclosureV10V7V9V12FAasubsetasuccV8V10AainvV0V1V10V7V9V2FIaclosureV5V7V3V13Iainfix =V13V8NFAashortest_pathV0V8V2AainvV0V1V5V7V3V2Iainfix =V8V1NIainfix =V7aremoveV8V4AamemV8V4FFIais_emptyV4NIainfix =V6aTrueNIais_emptyV4qainfix =V6aTrueFIainfix <=c0V2AaclosureV5V4V3V14FAais_emptyV3Iais_emptyV4AainvV0V1V5V4V3V2FF"> @@ -992,7 +992,7 @@ memlimit="0" obsolete="false" archived="false"> - <result status="valid" time="0.01"/> + <result status="valid" time="0.00"/> </proof> </goal> <goal @@ -1000,7 +1000,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="parameter bfs" - sum="c0e0088c049d87ad5b0c24545cda5cba" + sum="794b7aa4207e30b28a3ffbb4842d1533" proved="true" expanded="false" shape="ais_emptyV9Iais_emptyV7Iainfix =V11aTrueNIais_emptyV7qainfix =V11aTrueFIaclosureV10V7V9V12FAasubsetasuccV8V10AainvV0V1V10V7V9V2FIaclosureV5V7V3V13Iainfix =V13V8NFAashortest_pathV0V8V2AainvV0V1V5V7V3V2Iainfix =V8V1NIainfix =V7aremoveV8V4AamemV8V4FFIais_emptyV4NIainfix =V6aTrueNIais_emptyV4qainfix =V6aTrueFIainfix <=c0V2AaclosureV5V4V3V14FAais_emptyV3Iais_emptyV4AainvV0V1V5V4V3V2FF"> @@ -1020,7 +1020,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="parameter bfs" - sum="5edfa3d02d2bbc7770bd37fe13317579" + sum="82bdc55e958c2ae0fbce57f6438a1860" proved="true" expanded="false" shape="aclosureV10V7V9V12FIainfix =V11aTrueNIais_emptyV7qainfix =V11aTrueFIaclosureV10V7V9V13FAasubsetasuccV8V10AainvV0V1V10V7V9V2FIaclosureV5V7V3V14Iainfix =V14V8NFAashortest_pathV0V8V2AainvV0V1V5V7V3V2Iainfix =V8V1NIainfix =V7aremoveV8V4AamemV8V4FFIais_emptyV4NIainfix =V6aTrueNIais_emptyV4qainfix =V6aTrueFIainfix <=c0V2AaclosureV5V4V3V15FAais_emptyV3Iais_emptyV4AainvV0V1V5V4V3V2FF"> @@ -1040,7 +1040,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="parameter bfs" - sum="7cc397f6887cbe1718b2def03e39b855" + sum="acc695fb325722b0de6daad8f6a0ebbf" proved="true" expanded="false" shape="ainfix <=c0V2Iainfix =V11aTrueNIais_emptyV7qainfix =V11aTrueFIaclosureV10V7V9V12FAasubsetasuccV8V10AainvV0V1V10V7V9V2FIaclosureV5V7V3V13Iainfix =V13V8NFAashortest_pathV0V8V2AainvV0V1V5V7V3V2Iainfix =V8V1NIainfix =V7aremoveV8V4AamemV8V4FFIais_emptyV4NIainfix =V6aTrueNIais_emptyV4qainfix =V6aTrueFIainfix <=c0V2AaclosureV5V4V3V14FAais_emptyV3Iais_emptyV4AainvV0V1V5V4V3V2FF"> @@ -1062,7 +1062,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="assertion" - sum="f8ffffb19d960a09fda45fd4d4f31103" + sum="4c143433aac4d2c32716e8a3f3bf9eb3" proved="true" expanded="true" shape="amemV1V5NIainfix =V6aTrueNNIais_emptyV4qainfix =V6aTrueFIainfix <=c0V2AaclosureV5V4V3V7FAais_emptyV3Iais_emptyV4AainvV0V1V5V4V3V2FF"> @@ -1077,7 +1077,7 @@ locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" expl="assertion" - sum="f8ffffb19d960a09fda45fd4d4f31103" + sum="4c143433aac4d2c32716e8a3f3bf9eb3" proved="true" expanded="false" shape="amemV1V5NIainfix =V6aTrueNNIais_emptyV4qainfix =V6aTrueFIainfix <=c0V2AaclosureV5V4V3V7FAais_emptyV3Iais_emptyV4AainvV0V1V5V4V3V2FF"> @@ -1106,8 +1106,8 @@ name="WP_parameter bfs.8" locfile="programs/vstte12_bfs/../vstte12_bfs.mlw" loclnum="104" loccnumb="6" loccnume="9" - expl="normal postcondition" - sum="cc98cbfa7743081167c38c8c8d2bf88c" + expl="postcondition" + sum="95b204a12556c04f1f7ac6546934750b" proved="true" expanded="false" shape="apathV0V1V7NFIamemV1V5NIainfix =V6aTrueNNIais_emptyV4qainfix =V6aTrueFIainfix <=c0V2AaclosureV5V4V3V8FAais_emptyV3Iais_emptyV4AainvV0V1V5V4V3V2FF"> @@ -1120,7 +1120,7 @@ edited="vstte12_bfs_WP_BFS_WP_parameter_bfs_1.v" obsolete="false" archived="false"> - <result status="valid" time="0.61"/> + <result status="valid" time="0.60"/> </proof> </goal> </transf>