Skip to content

GitLab

Commit d417b053 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

update sessions, after driver changes for division

parent e4af0ac2
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 830 additions and 1547 deletions
examples/bitvectors/double/why3session.xml
View file @ d417b053
......@@ -7,28 +7,40 @@
version="0.94"/>
<prover
id="1"
name="Alt-Ergo"
version="0.95"/>
<prover
id="2"
name="CVC3"
version="2.2"/>
<prover
id="2"
id="3"
name="CVC3"
version="2.4.1"/>
<prover
id="3"
id="4"
name="CVC4"
version="1.0"/>
<prover
id="5"
name="Coq"
version="8.3pl4"/>
<prover
id="4"
id="6"
name="Z3"
version="2.19"/>
<prover
id="5"
id="7"
name="Z3"
version="3.2"/>
<prover
id="8"
name="Z3"
version="4.2"/>
<file
name="../double.why"
verified="true"
expanded="false">
verified="false"
expanded="true">
<theory
name="BV_double"
locfile="../double.why"
......@@ -40,23 +52,63 @@
name="TestDouble"
locfile="../double.why"
loclnum="65" loccnumb="7" loccnume="17"
verified="true"
expanded="false">
verified="false"
expanded="true">
<goal
name="nth_one1"
locfile="../double.why"
loclnum="73" loccnumb="8" loccnume="16"
sum="68b26f6bd21633cb2cb9250019b673f2"
proved="true"
expanded="false"
proved="false"
expanded="true"
shape="ainfix =anthaoneV0aFalseIainfix &lt;=V0c51Aainfix &lt;=c0V0F">
<proof
prover="0"
timelimit="60"
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="60.46"/>
</proof>
<proof
prover="1"
timelimit="60"
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="59.78"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="5.07"/>
</proof>
<proof
prover="6"
timelimit="60"
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="60.56"/>
</proof>
<proof
prover="7"
timelimit="60"
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="61.10"/>
</proof>
<proof
prover="8"
timelimit="60"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.26"/>
<result status="timeout" time="60.25"/>
</proof>
</goal>
<goal
......@@ -64,16 +116,56 @@
locfile="../double.why"
loclnum="74" loccnumb="8" loccnume="16"
sum="f08cb866a3ab9529aea096452c0c2aba"
proved="true"
expanded="false"
proved="false"
expanded="true"
shape="ainfix =anthaoneV0aTrueIainfix &lt;=V0c61Aainfix &lt;=c52V0F">
<proof
prover="0"
timelimit="60"
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="60.27"/>
</proof>
<proof
prover="1"
timelimit="60"
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="59.61"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="5.07"/>
</proof>
<proof
prover="6"
timelimit="60"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.23"/>
<result status="timeout" time="60.41"/>
</proof>
<proof
prover="7"
timelimit="60"
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="61.00"/>
</proof>
<proof
prover="8"
timelimit="60"
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="60.12"/>
</proof>
</goal>
<goal
......@@ -90,7 +182,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.23"/>
<result status="valid" time="2.22"/>
</proof>
</goal>
<goal
......@@ -110,7 +202,7 @@
<result status="valid" time="0.03"/>
</proof>
<proof
prover="1"
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -118,7 +210,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="2"
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -126,7 +218,7 @@
<result status="valid" time="0.03"/>
</proof>
<proof
prover="4"
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -134,7 +226,7 @@
<result status="valid" time="0.11"/>
</proof>
<proof
prover="5"
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -159,7 +251,7 @@
<result status="valid" time="2.09"/>
</proof>
<proof
prover="3"
prover="5"
timelimit="30"
memlimit="1000"
edited="double_TestDouble_exp_one_1.v"
......@@ -185,7 +277,7 @@
<result status="valid" time="0.09"/>
</proof>
<proof
prover="4"
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -193,7 +285,7 @@
<result status="valid" time="0.69"/>
</proof>
<proof
prover="5"
prover="7"
timelimit="11"
memlimit="1000"
obsolete="false"
......@@ -218,7 +310,7 @@
<result status="valid" time="0.04"/>
</proof>
<proof
prover="1"
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -226,7 +318,7 @@
<result status="valid" time="0.03"/>
</proof>
<proof
prover="2"
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
......
examples/bitvectors/double_of_int/why3session.xml
View file @ d417b053
......@@ -35,20 +35,20 @@
version="3.2"/>
<file
name="../double_of_int.why"
verified="true"
verified="false"
expanded="true">
<theory
name="DoubleOfInt"
locfile="../double_of_int.why"
loclnum="3" loccnumb="7" loccnume="18"
verified="true"
verified="false"
expanded="true">
<goal
name="jp0_30"
locfile="../double_of_int.why"
loclnum="25" loccnumb="8" loccnume="14"
sum="842bc987782a685a12fd36113c0e63a5"
proved="true"
proved="false"
expanded="false"
shape="ainfix =anthaj&apos;V0aFalseIainfix &lt;V0c30Aainfix &lt;=c0V0F">
<proof
......@@ -57,7 +57,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.34"/>
<result status="timeout" time="5.00"/>
</proof>
<proof
prover="1"
......@@ -65,7 +65,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
<result status="timeout" time="2.99"/>
</proof>
</goal>
<goal
......@@ -73,7 +73,7 @@
locfile="../double_of_int.why"
loclnum="41" loccnumb="8" loccnume="18"
sum="daeea5ea737b3241595fcfb708e70f5a"
proved="true"
proved="false"
expanded="false"
shape="ainfix =anthaconstV0aFalseIainfix &lt;=V0c30Aainfix &lt;=c0V0F">
<proof
......@@ -82,7 +82,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.07"/>
<result status="timeout" time="2.99"/>
</proof>
</goal>
<goal
......@@ -90,7 +90,7 @@
locfile="../double_of_int.why"
loclnum="42" loccnumb="8" loccnume="18"
sum="0f6469715ada51e26147ae146acb1d71"
proved="true"
proved="false"
expanded="false"
shape="ainfix =anthaconstc31aTrue">
<proof
......@@ -99,7 +99,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.96"/>
<result status="timeout" time="6.02"/>
</proof>
<proof
prover="1"
......@@ -107,7 +107,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="timeout" time="2.99"/>
</proof>
</goal>
<goal
......@@ -115,7 +115,7 @@
locfile="../double_of_int.why"
loclnum="43" loccnumb="8" loccnume="18"
sum="ddb41e35ebfdd7220dc9a4043bc6199d"
proved="true"
proved="false"
expanded="false"
shape="ainfix =anthaconstV0aFalseIainfix &lt;=V0c51Aainfix &lt;=c32V0F">
<proof
......@@ -124,7 +124,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.07"/>
<result status="timeout" time="2.98"/>
</proof>
</goal>
<goal
......@@ -132,7 +132,7 @@
locfile="../double_of_int.why"
loclnum="44" loccnumb="8" loccnume="18"
sum="cbbaae448dc933d9e751383ed6756170"
proved="true"
proved="false"
expanded="false"
shape="ainfix =anthaconstV0aTrueIainfix &lt;=V0c53Aainfix &lt;=c52V0F">
<proof
......@@ -141,7 +141,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.08"/>
<result status="timeout" time="2.99"/>
</proof>
</goal>
<goal
......@@ -149,7 +149,7 @@
locfile="../double_of_int.why"
loclnum="45" loccnumb="8" loccnume="18"
sum="855bcf07099a9c606761e92a2c43129b"
proved="true"
proved="false"
expanded="false"
shape="ainfix =anthaconstV0aFalseIainfix &lt;=V0c55Aainfix &lt;=c54V0F">
<proof
......@@ -158,7 +158,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.13"/>
<result status="timeout" time="2.98"/>
</proof>
</goal>
<goal
......@@ -166,7 +166,7 @@
locfile="../double_of_int.why"
loclnum="46" loccnumb="8" loccnume="18"
sum="f90f27ea4b8352949efa686898579ba5"
proved="true"
proved="false"
expanded="false"
shape="ainfix =anthaconstV0aTrueIainfix &lt;=V0c57Aainfix &lt;=c56V0F">
<proof
......@@ -175,7 +175,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.20"/>
<result status="timeout" time="2.99"/>
</proof>
</goal>
<goal
......@@ -183,7 +183,7 @@
locfile="../double_of_int.why"
loclnum="47" loccnumb="8" loccnume="18"
sum="33ddded6ac63f36505881e2f6f7daf52"
proved="true"
proved="false"
expanded="false"
shape="ainfix =anthaconstV0aFalseIainfix &lt;=V0c61Aainfix &lt;=c58V0F">
<proof
......@@ -192,7 +192,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.07"/>
<result status="timeout" time="2.99"/>
</proof>
</goal>
<goal
......@@ -200,7 +200,7 @@
locfile="../double_of_int.why"
loclnum="48" loccnumb="8" loccnume="18"
sum="ebbfe86d1919d9c00eedf03bd41df821"
proved="true"
proved="false"
expanded="false"
shape="ainfix =anthaconstc62aTrue">
<proof
......@@ -209,7 +209,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="2.59"/>
<result status="timeout" time="8.01"/>
</proof>
<proof
prover="1"
......@@ -217,7 +217,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="timeout" time="2.98"/>
</proof>
</goal>
<goal
......@@ -225,7 +225,7 @@
locfile="../double_of_int.why"
loclnum="49" loccnumb="8" loccnume="18"
sum="0ac5bc0333128c22f732472517683d73"
proved="true"
proved="false"
expanded="false"
shape="ainfix =anthaconstc63aFalse">
<proof
......@@ -234,7 +234,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="timeout" time="2.99"/>
</proof>
</goal>
<goal
......@@ -497,7 +497,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.48"/>
<result status="valid" time="0.31"/>
</proof>
<proof
prover="2"
......@@ -652,7 +652,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="11.00"/>
<result status="valid" time="13.18"/>
</proof>
</goal>
<goal
......@@ -767,7 +767,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.74"/>
<result status="timeout" time="2.99"/>
</proof>
<proof
prover="2"
......@@ -849,7 +849,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.12"/>
<result status="valid" time="0.52"/>
</proof>
</goal>
<goal
......@@ -898,7 +898,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.60"/>
<result status="valid" time="3.07"/>
</proof>
</goal>
<goal
......@@ -991,7 +991,7 @@
edited="double_of_int_DoubleOfInt_lemma1_pos_1.v"
obsolete="false"
archived="false">
<result status="valid" time="2.67"/>
<result status="valid" time="5.85"/>
</proof>
</goal>
<goal
......@@ -1150,7 +1150,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.06"/>
<result status="valid" time="1.32"/>
</proof>
</goal>
<goal
......@@ -1283,7 +1283,7 @@
locfile="../double_of_int.why"
loclnum="190" loccnumb="8" loccnume="16"
sum="30dd70862616ede77486898cb83c016f"
proved="true"
proved="false"
expanded="false"
shape="ainfix =anthavarV0V1aFalseIainfix &lt;=V1c51Aainfix &lt;=c32V1FF">
<proof
......@@ -1292,7 +1292,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="8.41"/>
<result status="timeout" time="16.94"/>
</proof>
</goal>
<goal
......@@ -1310,7 +1310,7 @@
edited="double_of_int_DoubleOfInt_lemma2_1.v"
obsolete="false"
archived="false">
<result status="valid" time="13.00"/>
<result status="valid" time="16.24"/>
</proof>
</goal>
<goal
......@@ -1318,7 +1318,7 @@
locfile="../double_of_int.why"
loclnum="198" loccnumb="8" loccnume="16"
sum="638b8e3885d0439d703f9bda8e22222e"
proved="true"
proved="false"
expanded="false"
shape="ainfix =anthavarV0V1aTrueIainfix &lt;=V1c53Aainfix &lt;=c52V1FF">
<proof
......@@ -1327,7 +1327,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="11.49"/>
<result status="timeout" time="22.85"/>
</proof>
</goal>
<goal
......@@ -1335,7 +1335,7 @@
locfile="../double_of_int.why"
loclnum="199" loccnumb="8" loccnume="16"
sum="14388e74f36176ffbd91f3cf89c3d28d"
proved="true"
proved="false"
expanded="false"
shape="ainfix =anthavarV0V1aFalseIainfix &lt;=V1c55Aainfix &lt;=c54V1FF">
<proof
......@@ -1344,7 +1344,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="8.46"/>
<result status="timeout" time="16.94"/>
</proof>
</goal>
<goal
......@@ -1352,7 +1352,7 @@
locfile="../double_of_int.why"
loclnum="200" loccnumb="8" loccnume="16"
sum="c5674c241034e37fa247b577f2403a9f"
proved="true"
proved="false"
expanded="false"
shape="ainfix =anthavarV0V1aTrueIainfix &lt;=V1c57Aainfix &lt;=c56V1FF">
<proof
......@@ -1361,7 +1361,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="11.49"/>
<result status="timeout" time="22.88"/>
</proof>
</goal>
<goal
......@@ -1369,7 +1369,7 @@
locfile="../double_of_int.why"
loclnum="201" loccnumb="8" loccnume="16"
sum="2aafe99e1c9185fecf36cb92cd961b06"
proved="true"
proved="false"
expanded="false"
shape="ainfix =anthavarV0V1aFalseIainfix &lt;=V1c61Aainfix &lt;=c58V1FF">
<proof
......@@ -1378,7 +1378,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="8.34"/>
<result status="timeout" time="16.92"/>
</proof>
</goal>
<goal
......@@ -1403,7 +1403,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.26"/>
<result status="valid" time="0.50"/>
</proof>
<proof
prover="2"
......@@ -1478,7 +1478,7 @@
memlimit="1000"
obsolete="false"