Commit f3a91eff authored by MARCHE Claude's avatar MARCHE Claude

upgrade Z3 4.0 to 4.2, update sessions

parent f59baedf
......@@ -48,10 +48,6 @@
<prover
id="11"
name="Z3"
version="4.0"/>
<prover
id="12"
name="Z3"
version="4.2"/>
<file
name="../einstein.why"
......@@ -194,14 +190,6 @@
archived="false">
<result status="valid" time="0.07"/>
</proof>
<proof
prover="12"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.08"/>
</proof>
</goal>
<goal
name="Wrong"
......@@ -307,14 +295,6 @@
archived="false">
<result status="timeout" time="5.05"/>
</proof>
<proof
prover="12"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="5.04"/>
</proof>
</goal>
<goal
name="G2"
......@@ -420,14 +400,6 @@
archived="false">
<result status="valid" time="0.07"/>
</proof>
<proof
prover="12"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.07"/>
</proof>
</goal>
</theory>
</file>
......
......@@ -40,13 +40,9 @@
<prover
id="9"
name="Z3"
version="4.0"/>
<prover
id="10"
name="Z3"
version="4.2"/>
<prover
id="11"
id="10"
name="Zenon"
version="0.7.1"/>
<file
......@@ -145,18 +141,10 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="10"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="11"
prover="10"
timelimit="5"
memlimit="4000"
obsolete="false"
......@@ -258,14 +246,6 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="11"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="2.10"/>
</proof>
</goal>
......@@ -363,14 +343,6 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="11"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.30"/>
</proof>
</goal>
......@@ -444,18 +416,10 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="10"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="11"
prover="10"
timelimit="5"
memlimit="4000"
obsolete="false"
......@@ -549,23 +513,15 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="10"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="11"
prover="10"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="6.59"/>
<result status="timeout" time="5.14"/>
</proof>
</goal>
<goal
......@@ -654,18 +610,10 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="10"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="11"
prover="10"
timelimit="5"
memlimit="4000"
obsolete="false"
......@@ -751,23 +699,15 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="10"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="11"
prover="10"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="5.38"/>
<result status="timeout" time="6.35"/>
</proof>
</goal>
</theory>
......
......@@ -32,7 +32,7 @@
<prover
id="7"
name="Z3"
version="4.0"/>
version="4.2"/>
<file
name="../blocking_semantics3.mlw"
verified="false"
......
......@@ -40,7 +40,7 @@
<prover
id="9"
name="Z3"
version="4.0"/>
version="4.2"/>
<file
name="../blocking_semantics4.mlw"
verified="false"
......@@ -3890,7 +3890,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.99"/>
<result status="valid" time="0.20"/>
</proof>
</goal>
<goal
......
......@@ -28,7 +28,7 @@
<prover
id="6"
name="Z3"
version="4.0"/>
version="4.2"/>
<file
name="../blocking_semantics5.mlw"
verified="true"
......@@ -1767,7 +1767,7 @@
edited="blocking_semantics5_FreshVariables_eval_msubst_2.v"
obsolete="false"
archived="false">
<result status="valid" time="1.70"/>
<result status="valid" time="1.99"/>
</proof>
<proof
prover="5"
......@@ -2081,7 +2081,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="5.72"/>
<result status="valid" time="19.46"/>
</proof>
<proof
prover="3"
......@@ -2089,7 +2089,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="22.00"/>
<result status="valid" time="24.35"/>
</proof>
<proof
prover="5"
......@@ -2166,7 +2166,7 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.26"/>
<result status="valid" time="0.44"/>
</proof>
<proof
prover="3"
......@@ -2223,7 +2223,7 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.44"/>
<result status="valid" time="0.25"/>
</proof>
<proof
prover="3"
......@@ -2280,7 +2280,7 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="7.69"/>
<result status="valid" time="8.86"/>
</proof>
<proof
prover="3"
......@@ -2288,7 +2288,7 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="9.21"/>
<result status="valid" time="4.25"/>
</proof>
<proof
prover="5"
......@@ -2451,7 +2451,7 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="2.66"/>
<result status="valid" time="5.05"/>
</proof>
<proof
prover="3"
......@@ -2565,7 +2565,7 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="8.53"/>
<result status="valid" time="4.12"/>
</proof>
<proof
prover="3"
......@@ -3617,7 +3617,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="2.32"/>
<result status="valid" time="2.71"/>
</proof>
<proof
prover="3"
......
......@@ -36,7 +36,7 @@
<prover
id="8"
name="Z3"
version="4.0"/>
version="4.2"/>
<file
name="../alphaBeta.mlw"
verified="false"
......
......@@ -8,7 +8,7 @@
<prover
id="1"
name="Z3"
version="4.0"/>
version="4.2"/>
<file
name="../binary_sqrt.mlw"
verified="true"
......
......@@ -28,7 +28,7 @@
<prover
id="6"
name="Z3"
version="4.0"/>
version="4.2"/>
<file
name="../counting_sort.mlw"
verified="true"
......
......@@ -28,7 +28,7 @@
<prover
id="6"
name="Z3"
version="4.0"/>
version="4.2"/>
<file
name="../decrease1.mlw"
verified="true"
......@@ -1115,7 +1115,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.31"/>
<result status="valid" time="0.45"/>
</proof>
</goal>
<goal
......
......@@ -36,7 +36,7 @@
<prover
id="8"
name="Z3"
version="4.0"/>
version="4.2"/>
<file
name="../generate_all_trees.mlw"
verified="true"
......
......@@ -32,10 +32,6 @@
<prover
id="7"
name="Z3"
version="4.0"/>
<prover
id="8"
name="Z3"
version="4.2"/>
<file
name="../isqrt.mlw"
......@@ -46,7 +42,7 @@
locfile="../isqrt.mlw"
loclnum="4" loccnumb="7" loccnume="13"
verified="true"
expanded="true">
expanded="false">
<goal
name="WP_parameter isqrt"
locfile="../isqrt.mlw"
......@@ -54,7 +50,7 @@
expl="parameter isqrt"
sum="64277e54f36ba5a32dedb1a194a25f0d"
proved="true"
expanded="true"
expanded="false"
shape="iainfix &lt;=V1V0ainfix &lt;ainfix -V0V3ainfix -V0V2Aainfix &lt;=c0ainfix -V0V2Aainfix =V4asqrainfix +V3c1Aainfix &gt;=V0asqrV3Aainfix &gt;=V3c0Iainfix =V4ainfix +ainfix +V1ainfix *c2V3c1FIainfix =V3ainfix +V2c1Fainfix &lt;V0asqrainfix +V2c1Aainfix &lt;=asqrV2V0Aainfix &gt;=V2c0Iainfix =V1asqrainfix +V2c1Aainfix &gt;=V0asqrV2Aainfix &gt;=V2c0FAainfix =c1asqrainfix +c0c1Aainfix &gt;=V0asqrc0Aainfix &gt;=c0c0Iainfix &gt;=V0c0F">
<label
name="expl:parameter isqrt"/>
......@@ -82,14 +78,6 @@
archived="false">
<result status="valid" time="0.10"/>
</proof>
<proof
prover="8"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.10"/>
</proof>
</goal>
<goal
name="WP_parameter main"
......@@ -98,7 +86,7 @@
expl="parameter main"
sum="27febadb619ab97b0f5570efb544d5b3"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =V0c4Iainfix &lt;c17asqrainfix +V0c1Aainfix &lt;=asqrV0c17Aainfix &gt;=V0c0FAainfix &gt;=c17c0">
<label
name="expl:parameter main"/>
......@@ -118,14 +106,6 @@
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="8"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</theory>
<theory
......@@ -156,7 +136,7 @@
expl="postcondition"
sum="11395e2e0807e0a152ae8659ec21bd93"
proved="true"
expanded="true"
expanded="false"
shape="ainfix &lt;V0ainfix *ainfix +c0c1ainfix +c0c1Aainfix &lt;=ainfix *c0c0V0Iainfix =V0c0Iainfix &gt;=V0c0F">
<label
name="expl:parameter sqrt"/>
......@@ -190,14 +170,6 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="8"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
......@@ -208,7 +180,7 @@
expl="postcondition"
sum="3ab61eabd3d2a91edcf1daa5821658bf"
proved="true"
expanded="true"
expanded="false"
shape="ainfix &lt;V0ainfix *ainfix +c1c1ainfix +c1c1Aainfix &lt;=ainfix *c1c1V0Iainfix &lt;=V0c3Iainfix =V0c0NIainfix &gt;=V0c0F">
<label
name="expl:parameter sqrt"/>
......@@ -242,14 +214,6 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="8"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
......@@ -260,14 +224,14 @@
expl="loop invariant init"
sum="bd17f15cea53a783a80db1b3fa200b2f"
proved="true"
expanded="true"
expanded="false"
shape="ainfix &lt;V0ainfix *ainfix +adivainfix +V0c1c2c1ainfix +adivainfix +V0c1c2c1Aainfix &lt;V0ainfix *ainfix +V0c1ainfix +V0c1Aainfix =adivainfix +V0c1c2adivainfix +adivV0V0V0c2Aainfix &gt;V0c0Aainfix &gt;adivainfix +V0c1c2c0Iainfix &lt;=V0c3NIainfix =V0c0NIainfix &gt;=V0c0F">
<label
name="expl:parameter sqrt"/>
<transf
name="split_goal"
proved="true"
expanded="true">
expanded="false">
<goal
name="WP_parameter sqrt.3.1"
locfile="../isqrt.mlw"
......@@ -275,7 +239,7 @@
expl="parameter sqrt"
sum="24aeef4693626abd3583f6b6921aba3d"
proved="true"
expanded="true"
expanded="false"
shape="ainfix &gt;adivainfix +V0c1c2c0Iainfix &lt;=V0c3NIainfix =V0c0NIainfix &gt;=V0c0F">
<label
name="expl:parameter sqrt"/>
......@@ -311,14 +275,6 @@
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="8"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter sqrt.3.2"
......@@ -327,7 +283,7 @@
expl="parameter sqrt"
sum="92c82885df59e2741ce4df823ca7822c"
proved="true"
expanded="true"
expanded="false"
shape="ainfix &gt;V0c0Iainfix &lt;=V0c3NIainfix =V0c0NIainfix &gt;=V0c0F">
<label
name="expl:parameter sqrt"/>
......@@ -363,14 +319,6 @@
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="8"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter sqrt.3.3"
......@@ -379,7 +327,7 @@
expl="parameter sqrt"
sum="fb51c594670b2b8984a4e1f8acf2af68"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =adivainfix +V0c1c2adivainfix +adivV0V0V0c2Iainfix &lt;=V0c3NIainfix =V0c0NIainfix &gt;=V0c0F">
<label
name="expl:parameter sqrt"/>
......@@ -397,14 +345,6 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="5.04"/>
</proof>
<proof
prover="8"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="5.05"/>
</proof>
</goal>
......@@ -415,7 +355,7 @@
expl="parameter sqrt"
sum="1f2b528636f5a3179f0d71f5ce38fb47"
proved="true"
expanded="true"
expanded="false"
shape="ainfix &lt;V0ainfix *ainfix +V0c1ainfix +V0c1Iainfix &lt;=V0c3NIainfix =V0c0NIainfix &gt;=V0c0F">
<label
name="expl:parameter sqrt"/>
......@@ -449,14 +389,6 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="8"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
......@@ -467,7 +399,7 @@
expl="parameter sqrt"
sum="ca389f1cbcafdb15628b4e6e6c6538b1"
proved="true"
expanded="true"
expanded="false"
shape="ainfix &lt;V0ainfix *ainfix +adivainfix +V0c1c2c1ainfix +adivainfix +V0c1c2c1Iainfix &lt;=V0c3NIainfix =V0c0NIainfix &gt;=V0c0F">
<label
name="expl:parameter sqrt"/>
......@@ -503,14 +435,6 @@
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="8"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>