Commit 773f4802 authored by MARCHE Claude's avatar MARCHE Claude

fix wp3 proofs

parent bbd4898a
......@@ -13,13 +13,9 @@
<prover
id="2"
name="Coq"
version="8.3pl3"/>
<prover
id="3"
name="Coq"
version="8.3pl4"/>
<prover
id="4"
id="3"
name="Z3"
version="3.2"/>
<file
......@@ -31,14 +27,14 @@
locfile="examples/hoare_logic/wp3/../wp3.mlw"
loclnum="6" loccnumb="7" loccnume="14"
verified="false"
expanded="true">
expanded="false">
<goal
name="eval_subst_term"
locfile="examples/hoare_logic/wp3/../wp3.mlw"
loclnum="101" loccnumb="6" loccnume="21"
sum="ef98d2b97884863e1cbe533969818f1f"
proved="false"
expanded="true"
expanded="false"
shape="ainfix =aeval_termV0V1asubst_termV2V3V4aeval_termasetV0V3agetV1V4V1V2Iafresh_in_termV4V2F">
<proof
prover="0"
......@@ -57,7 +53,7 @@
<result status="timeout" time="2.08"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="2"
memlimit="1000"
obsolete="false"
......@@ -71,7 +67,7 @@
loclnum="107" loccnumb="6" loccnume="27"
sum="430b7d02bdb3f2e8cec81e288e46c026"
proved="false"
expanded="true"
expanded="false"
shape="ainfix =aeval_termV1asetV2V3V4V0aeval_termV1V2V0Iafresh_in_termV3V0F">
<proof
prover="0"
......@@ -90,7 +86,7 @@
<result status="timeout" time="2.06"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="2"
memlimit="1000"
obsolete="false"
......@@ -104,7 +100,7 @@
loclnum="133" loccnumb="6" loccnume="16"
sum="b9e2179371c7b6be3e45cd792f8954a3"
proved="false"
expanded="true"
expanded="false"
shape="aeval_fmlaasetV1V3agetV2V4V2V0qaeval_fmlaV1V2asubstV0V3V4Iafresh_in_fmlaV4V0F">
<proof
prover="0"
......@@ -123,7 +119,7 @@
<result status="timeout" time="2.06"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="2"
memlimit="1000"
obsolete="false"
......@@ -137,7 +133,7 @@
loclnum="139" loccnumb="6" loccnume="15"
sum="c507b815677e32c2dc3fa56fcbc973f8"
proved="true"
expanded="true"
expanded="false"
shape="aeval_fmlaV1asetasetV2V4V6V3V5V0qaeval_fmlaV1asetasetV2V3V5V4V6V0Iainfix =V3V4NF">
<proof
prover="0"
......@@ -156,7 +152,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="2"
memlimit="1000"
obsolete="false"
......@@ -170,7 +166,7 @@
loclnum="145" loccnumb="6" loccnume="22"
sum="7bbed035dda60f5a6987d1f3fd286823"
proved="false"
expanded="true"
expanded="false"
shape="aeval_fmlaV1V2V0qaeval_fmlaV1asetV2V3V4V0Iafresh_in_fmlaV3V0F">
<proof
prover="0"
......@@ -189,7 +185,7 @@
<result status="timeout" time="2.06"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="2"
memlimit="1000"
obsolete="false"
......@@ -203,7 +199,7 @@
loclnum="247" loccnumb="6" loccnume="19"
sum="47ef5cdb603762b8f2a23ff84df56ff1"
proved="false"
expanded="true"
expanded="false"
shape="ainfix &gt;=V6c0Iamany_stepsV0V1V4V2V3V5V6F">
<proof
prover="0"
......@@ -222,7 +218,7 @@
<result status="timeout" time="2.09"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="2"
memlimit="1000"
obsolete="false"
......@@ -236,7 +232,7 @@
loclnum="251" loccnumb="6" loccnume="20"
sum="a9a72fc851bf1edc92c0860aaa3c1c30"
proved="false"
expanded="true"
expanded="false"
shape="ainfix =V6ainfix +ainfix +c1V9V10Aamany_stepsV7V8V5V2V3avoidV10Aamany_stepsV0V1V4V7V8avoidV9EIamany_stepsV0V1aEseqV4V5V2V3avoidV6F">
</goal>
<goal
......@@ -245,7 +241,7 @@
loclnum="259" loccnumb="6" loccnume="20"
sum="23aae6e7f5564e085f32d44b76c12a71"
proved="false"
expanded="true"
expanded="false"
shape="ainfix =V8ainfix +ainfix +c1V12V13Aamany_stepsV9asetV10V4V11V6V2V3aEvalueV7V13Aamany_stepsV0V1V5V9V10aEvalueV11V12EIamany_stepsV0V1aEletV4V5V6V2V3aEvalueV7V8F">
<proof
prover="1"
......@@ -256,7 +252,7 @@
<result status="timeout" time="32.39"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="30"
memlimit="1000"
obsolete="false"
......@@ -270,7 +266,7 @@
locfile="examples/hoare_logic/wp3/../wp3.mlw"
loclnum="291" loccnumb="7" loccnume="20"
verified="false"
expanded="false">
expanded="true">
<goal
name="Test13"
locfile="examples/hoare_logic/wp3/../wp3.mlw"
......@@ -321,7 +317,7 @@
<result status="valid" time="0.05"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="2"
memlimit="1000"
obsolete="false"
......@@ -360,15 +356,15 @@
loclnum="307" loccnumb="5" loccnume="15"
sum="179b541d8affa3ce648a884ef118425a"
proved="false"
expanded="false"
expanded="true"
shape="amany_stepsamy_sigmaamy_piaEvarc0amy_sigmaamy_piaEvalueaVintc42c1">
<proof
prover="0"
timelimit="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="2.18"/>
<result status="unknown" time="1.54"/>
</proof>
<proof
prover="1"
......@@ -379,7 +375,7 @@
<result status="timeout" time="2.09"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="2"
memlimit="1000"
obsolete="false"
......@@ -418,15 +414,15 @@
loclnum="313" loccnumb="5" loccnume="14"
sum="fa65c99c66ede71e6f39f0f8bfaeae8d"
proved="false"
expanded="false"
expanded="true"
shape="amany_stepsamy_sigmaamy_piaEderefc0amy_sigmaamy_piaEvalueaVintc0c1">
<proof
prover="0"
timelimit="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="2.10"/>
<result status="unknown" time="1.53"/>
</proof>
<proof
prover="1"
......@@ -437,7 +433,7 @@
<result status="timeout" time="2.10"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="2"
memlimit="1000"
obsolete="false"
......@@ -470,7 +466,7 @@
<result status="timeout" time="2.02"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="2"
memlimit="1000"
obsolete="false"
......@@ -503,7 +499,7 @@
<result status="timeout" time="2.09"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="2"
memlimit="1000"
obsolete="false"
......@@ -536,7 +532,7 @@
<result status="valid" time="0.33"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="2"
memlimit="1000"
obsolete="false"
......@@ -561,7 +557,7 @@
<result status="valid" time="1.26"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="2"
memlimit="1000"
obsolete="false"
......@@ -585,20 +581,12 @@
expanded="true"
shape="avalid_tripleV1V4V3Iavalid_fmlaaFimpliesV2V3Iavalid_tripleV0V4V2Iavalid_fmlaaFimpliesV1V0F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.05"/>
</proof>
<proof
prover="1"
timelimit="5"
prover="3"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.10"/>
<result status="valid" time="2.22"/>
</proof>
<proof
prover="2"
......@@ -607,15 +595,7 @@
edited="wp3_HoareLogic_consequence_rule_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.92"/>
</proof>
<proof
prover="4"
timelimit="9"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="4.64"/>
<result status="valid" time="0.50"/>
</proof>
</goal>
<goal
......@@ -660,7 +640,7 @@
<result status="timeout" time="5.11"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -693,7 +673,7 @@
<result status="timeout" time="5.13"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="30"
memlimit="2000"
obsolete="false"
......@@ -726,7 +706,7 @@
<result status="timeout" time="5.22"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="30"
memlimit="1000"
obsolete="false"
......@@ -734,7 +714,7 @@
<result status="outofmemory" time="27.71"/>
</proof>
<proof
prover="3"
prover="2"
timelimit="30"
memlimit="1000"
edited="wp3_HoareLogic_let_rule_1.v"
......@@ -768,7 +748,7 @@
<result status="timeout" time="5.10"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -801,7 +781,7 @@
<result status="timeout" time="5.67"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment