Commit 1d18fce0 authored by MARCHE Claude's avatar MARCHE Claude

more proofs in bitvector example

parent a2fa050c
......@@ -811,33 +811,17 @@
proved="false"
expanded="true"
shape="ainfix =ato_nat_subafrom_int2cV1ainfix -V0c1c0V1Iainfix <V1apow2V0Aainfix <=c0V1FIainfix <=V0c30Aainfix <=c0V0F">
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.12"/>
</proof>
<proof
prover="0"
timelimit="5"
timelimit="120"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
<result status="timeout" time="120.12"/>
</proof>
<proof
prover="3"
timelimit="30"
timelimit="120"
memlimit="1000"
edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_gen_1.v"
obsolete="false"
......@@ -853,45 +837,13 @@
proved="false"
expanded="true"
shape="ainfix =ato_nat_subafrom_int2cV0c30c0V0Iainfix &gt;=V0c0Aais_int32V0F">
<proof
prover="5"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="highfailure" time="13.35"/>
</proof>
<proof
prover="1"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="highfailure" time="0.19"/>
</proof>
<proof
prover="0"
timelimit="30"
timelimit="120"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="30.10"/>
</proof>
<proof
prover="2"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="highfailure" time="0.42"/>
</proof>
<proof
prover="6"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="highfailure" time="17.06"/>
<result status="timeout" time="120.02"/>
</proof>
</goal>
<goal
......@@ -899,32 +851,16 @@
locfile="double_of_int/../double_of_int.why"
loclnum="129" loccnumb="8" loccnume="18"
sum="d139a96e73e962725d19413c55cb8b14"
proved="false"
expanded="true"
proved="true"
expanded="false"
shape="ainfix =ato_nat_subajpxorV0c31c0ainfix +apow2c31V0Iainfix &gt;=V0c0Aais_int32V0F">
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.12"/>
</proof>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
</proof>
<proof
prover="6"
timelimit="5"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
<result status="valid" time="5.26"/>
</proof>
</goal>
<goal
......@@ -981,32 +917,16 @@
locfile="double_of_int/../double_of_int.why"
loclnum="136" loccnumb="8" loccnume="28"
sum="7700539e32b8c609dda46df0274b2fa4"
proved="false"
expanded="true"
proved="true"
expanded="false"
shape="ainfix =ato_nat_subafrom_int2cV0c30c0ainfix +apow2c31V0Iainfix &lt;V0c0Aais_int32V0F">
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.12"/>
</proof>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
</proof>
<proof
prover="6"
timelimit="5"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
<result status="valid" time="17.28"/>
</proof>
</goal>
<goal
......@@ -1097,32 +1017,17 @@
locfile="double_of_int/../double_of_int.why"
loclnum="152" loccnumb="8" loccnume="28"
sum="4f0805d04df63d971aea75ebaf9472c3"
proved="false"
expanded="true"
proved="true"
expanded="false"
shape="ainfix =ato_nat_subaconcatV0V1V2c0ato_nat_subV1V2c0Iainfix &lt;V2c32Aainfix &lt;=c0V2FFF">
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.12"/>
</proof>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
</proof>
<proof
prover="6"
prover="3"
timelimit="5"
memlimit="1000"
edited="double_of_int_DoubleOfInt_to_nat_bv32_bv64_aux_1.v"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
<result status="valid" time="2.21"/>
</proof>
</goal>
<goal
......@@ -1221,32 +1126,16 @@
locfile="double_of_int/../double_of_int.why"
loclnum="160" loccnumb="8" loccnume="16"
sum="7003f9037a411fde4f723ff382153471"
proved="false"
expanded="true"
proved="true"
expanded="false"
shape="ainfix =anthavarV0V1aFalseIainfix &lt;=V1c51Aainfix &lt;=c32V1FF">
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.12"/>
</proof>
<proof
prover="0"
timelimit="5"
timelimit="15"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
<result status="valid" time="8.77"/>
</proof>
</goal>
<goal
......@@ -1254,32 +1143,17 @@
locfile="double_of_int/../double_of_int.why"
loclnum="162" loccnumb="8" loccnume="14"
sum="a2ab954dcfb69d430e68e06f3bb5b7c4"
proved="false"
expanded="true"
proved="true"
expanded="false"
shape="ainfix =amantissaavarV0ainfix +apow2c31V0Iais_int32V0F">
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.12"/>
</proof>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
</proof>
<proof
prover="6"
prover="3"
timelimit="5"
memlimit="1000"
edited="double_of_int_DoubleOfInt_lemma2_1.v"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
<result status="valid" time="3.81"/>
</proof>
</goal>
<goal
......@@ -1287,32 +1161,16 @@
locfile="double_of_int/../double_of_int.why"
loclnum="168" loccnumb="8" loccnume="16"
sum="ca60d399662644602dcdc5e7eb7b5c99"
proved="false"
expanded="true"
proved="true"
expanded="false"
shape="ainfix =anthavarV0V1aTrueIainfix &lt;=V1c53Aainfix &lt;=c52V1FF">
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.12"/>
</proof>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
</proof>
<proof
prover="6"
timelimit="5"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
<result status="valid" time="10.67"/>
</proof>
</goal>
<goal
......@@ -1320,32 +1178,16 @@
locfile="double_of_int/../double_of_int.why"
loclnum="169" loccnumb="8" loccnume="16"
sum="1311aceb05d56d608a31019c9b8fc853"
proved="false"
expanded="true"
proved="true"
expanded="false"
shape="ainfix =anthavarV0V1aFalseIainfix &lt;=V1c55Aainfix &lt;=c54V1FF">
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.12"/>
</proof>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
</proof>
<proof
prover="6"
timelimit="5"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
<result status="valid" time="8.97"/>
</proof>
</goal>
<goal
......@@ -1353,32 +1195,16 @@
locfile="double_of_int/../double_of_int.why"
loclnum="170" loccnumb="8" loccnume="16"
sum="62a990ea451884ad814dc65f26b68723"
proved="false"
expanded="true"
proved="true"
expanded="false"
shape="ainfix =anthavarV0V1aTrueIainfix &lt;=V1c57Aainfix &lt;=c56V1FF">
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.11"/>
</proof>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
</proof>
<proof
prover="6"
timelimit="5"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
<result status="valid" time="10.65"/>
</proof>
</goal>
<goal
......@@ -1386,32 +1212,16 @@
locfile="double_of_int/../double_of_int.why"
loclnum="171" loccnumb="8" loccnume="16"
sum="0ca87efa235ad32388d508d439a1c584"
proved="false"
expanded="true"
proved="true"
expanded="false"
shape="ainfix =anthavarV0V1aFalseIainfix &lt;=V1c61Aainfix &lt;=c58V1FF">
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.12"/>
</proof>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
</proof>
<proof
prover="6"
timelimit="5"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
<result status="valid" time="9.02"/>
</proof>
</goal>
<goal
......@@ -1468,32 +1278,17 @@
locfile="double_of_int/../double_of_int.why"
loclnum="174" loccnumb="8" loccnume="14"
sum="f208cabda76433852818607ea179a12a"
proved="false"
expanded="true"
proved="true"
expanded="false"
shape="ainfix =aexpavarV0c1075F">
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.12"/>
</proof>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
</proof>
<proof
prover="6"
timelimit="5"
prover="3"
timelimit="30"
memlimit="1000"
edited="double_of_int_DoubleOfInt_lemma3_1.v"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
<result status="valid" time="1.88"/>
</proof>
</goal>
<goal
......@@ -1648,32 +1443,17 @@
locfile="double_of_int/../double_of_int.why"
loclnum="189" loccnumb="8" loccnume="18"
sum="1521fd264894011a23d1b2278b59ffab"
proved="false"
expanded="true"
proved="true"
expanded="false"
shape="ainfix =avar_as_doubleV0ainfix *.apow2ainfix -c1075c1023ainfix +.c1.0ainfix *.afrom_intainfix +apow2c31V0apow2aprefix -c52Iais_int32V0F">
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.12"/>
</proof>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
</proof>
<proof
prover="6"
timelimit="5"
prover="3"
timelimit="30"
memlimit="1000"
edited="double_of_int_DoubleOfInt_var_value0_1.v"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
<result status="valid" time="1.27"/>
</proof>
</goal>
<goal
......
This diff is collapsed.
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