Commit 0beead85 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

update sessions (part 1)

parent 399609b7
......@@ -108,7 +108,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="12.26"/>
<result status="valid" time="20.87"/>
</proof>
<proof
prover="2"
......@@ -213,7 +213,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="6.50"/>
<result status="timeout" time="13.86"/>
</proof>
<proof
prover="2"
......@@ -318,7 +318,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="6.39"/>
<result status="valid" time="13.49"/>
</proof>
<proof
prover="2"
......@@ -334,7 +334,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="2.18"/>
<result status="valid" time="2.58"/>
</proof>
<proof
prover="4"
......
......@@ -244,7 +244,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.49"/>
<result status="valid" time="4.93"/>
</proof>
</goal>
<goal
......@@ -258,12 +258,12 @@
shape="CV0aTvalueVtaTvarVtaTderefVtaTbinVVVaexiste_compatibleV11aeval_termV7V8V0Iatype_termV9V10V0V11Iacompatible_envV7V9V8V10FIaexiste_compatibleV16aeval_termV12V13V4Iatype_termV14V15V4V16Iacompatible_envV12V14V13V15FIaexiste_compatibleV21aeval_termV17V18V6Iatype_termV19V20V6V21Iacompatible_envV17V19V18V20FF">
<proof
prover="5"
timelimit="7"
timelimit="5"
memlimit="1000"
edited="blocking_semantics3_ImpExpr_eval_type_term_1.v"
obsolete="false"
archived="false">
<result status="valid" time="3.63"/>
<result status="valid" time="3.24"/>
</proof>
</goal>
</transf>
......@@ -1336,7 +1336,7 @@
edited="blocking_semantics3_ImpExpr_eval_swap_1.v"
obsolete="false"
archived="false">
<result status="valid" time="2.24"/>
<result status="valid" time="1.81"/>
</proof>
</goal>
<goal
......@@ -1585,7 +1585,7 @@
edited="blocking_semantics3_ImpExpr_eval_swap_2_4.v"
obsolete="false"
archived="false">
<result status="valid" time="3.58"/>
<result status="valid" time="2.32"/>
</proof>
</goal>
<goal
......@@ -1604,7 +1604,7 @@
edited="blocking_semantics3_ImpExpr_eval_swap_2_5.v"
obsolete="false"
archived="false">
<result status="valid" time="2.82"/>
<result status="valid" time="2.42"/>
</proof>
</goal>
</transf>
......@@ -2209,7 +2209,7 @@
edited="blocking_semantics3_ImpExpr_type_preservation_1.v"
obsolete="false"
archived="false">
<result status="unknown" time="0.70"/>
<result status="unknown" time="0.69"/>
</proof>
</goal>
</theory>
......@@ -2441,7 +2441,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.07"/>
<result status="valid" time="1.72"/>
</proof>
<proof
prover="3"
......@@ -2907,7 +2907,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="22.04"/>
<result status="valid" time="19.72"/>
</proof>
<proof
prover="5"
......@@ -2942,7 +2942,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.47"/>
<result status="valid" time="2.05"/>
</proof>
</goal>
<goal
......
......@@ -1319,7 +1319,7 @@
edited="blocking_semantics4_ImpExpr_eval_swap_2.v"
obsolete="false"
archived="false">
<result status="valid" time="2.30"/>
<result status="valid" time="1.79"/>
</proof>
</goal>
<goal
......@@ -1338,7 +1338,7 @@
edited="blocking_semantics4_ImpExpr_eval_swap_3.v"
obsolete="false"
archived="false">
<result status="valid" time="2.19"/>
<result status="valid" time="1.82"/>
</proof>
</goal>
</transf>
......@@ -2948,7 +2948,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.11"/>
<result status="timeout" time="4.98"/>
</proof>
<proof
prover="3"
......@@ -3082,7 +3082,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.10"/>
<result status="timeout" time="4.98"/>
</proof>
<proof
prover="3"
......@@ -3148,7 +3148,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.10"/>
<result status="timeout" time="4.94"/>
</proof>
<proof
prover="3"
......@@ -3214,7 +3214,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.10"/>
<result status="timeout" time="4.97"/>
</proof>
<proof
prover="3"
......@@ -3280,7 +3280,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.38"/>
<result status="timeout" time="4.94"/>
</proof>
<proof
prover="3"
......@@ -3380,7 +3380,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.11"/>
<result status="timeout" time="4.92"/>
</proof>
<proof
prover="3"
......@@ -3533,7 +3533,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.12"/>
<result status="timeout" time="4.98"/>
</proof>
<proof
prover="3"
......@@ -3600,7 +3600,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.16"/>
<result status="valid" time="2.04"/>
</proof>
<proof
prover="5"
......@@ -3643,7 +3643,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.16"/>
<result status="valid" time="2.38"/>
</proof>
<proof
prover="3"
......@@ -3726,7 +3726,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.12"/>
<result status="timeout" time="4.96"/>
</proof>
<proof
prover="3"
......@@ -3809,7 +3809,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="3.83"/>
<result status="timeout" time="7.98"/>
</proof>
<proof
prover="3"
......@@ -3912,7 +3912,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="1.94"/>
<result status="timeout" time="4.97"/>
</proof>
</goal>
<goal
......@@ -3930,7 +3930,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.44"/>
<result status="timeout" time="4.98"/>
</proof>
</goal>
</transf>
......@@ -4053,7 +4053,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.60"/>
<result status="valid" time="0.09"/>
</proof>
<proof
prover="3"
......
......@@ -15,28 +15,24 @@
version="2.4.1"/>
<prover
id="3"
name="CVC4"
version="1.0"/>
<prover
id="4"
name="Coq"
version="8.3pl4"/>
<prover
id="4"
id="5"
name="Eprover"
version="1.4"/>
<prover
id="5"
id="6"
name="Spass"
version="3.7"/>
<prover
id="6"
name="Z3"
version="2.19"/>
<prover
id="7"
name="Z3"
version="3.2"/>
<prover
id="8"
name="Z3"
version="4.2"/>
version="2.19"/>
<file
name="../generate_all_trees.mlw"
verified="true"
......@@ -56,7 +52,7 @@
expanded="true"
shape="ainfix &gt;=asizeV0c0F">
<proof
prover="3"
prover="4"
timelimit="10"
memlimit="0"
edited="generate_all_trees_WP_GenerateAllTrees_size_nonneg_1.v"
......@@ -91,7 +87,7 @@
expanded="true"
shape="aall_treesc0aConsaEmptyaNil">
<proof
prover="3"
prover="4"
timelimit="10"
memlimit="0"
edited="generate_all_trees_WP_GenerateAllTrees_all_trees_0_1.v"
......@@ -264,12 +260,12 @@
<label
name="expl:VC for combine"/>
<proof
prover="0"
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.10"/>
<result status="valid" time="1.05"/>
</proof>
<proof
prover="2"
......@@ -279,22 +275,6 @@
archived="false">
<result status="valid" time="1.61"/>
</proof>
<proof
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.07"/>
</proof>
<proof
prover="8"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.05"/>
</proof>
</goal>
<goal
name="WP_parameter combine.8"
......@@ -323,7 +303,7 @@
<label
name="expl:VC for combine"/>
<proof
prover="3"
prover="4"
timelimit="10"
memlimit="0"
edited="generate_all_trees_WP_GenerateAllTrees_WP_parameter_combine_2.v"
......@@ -332,7 +312,7 @@
<result status="valid" time="0.52"/>
</proof>
<proof
prover="4"
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -340,7 +320,7 @@
<result status="valid" time="0.16"/>
</proof>
<proof
prover="5"
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -477,7 +457,7 @@
<label
name="expl:VC for combine"/>
<proof
prover="6"
prover="7"
timelimit="14"
memlimit="0"
obsolete="false"
......@@ -967,6 +947,14 @@
shape="ainfix &lt;asizeV10ainfix +V6c1Aainfix =asizeV9V3Aainfix =V9aNodeV10V11EIamemV9agetV8V3FIainfix =V8asetV5V3ainfix ++V7agetV5V3FIainfix &lt;V3ainfix +V0c1Aainfix &lt;=c0V3Iainfix =asizeV14ainfix -ainfix -V3c1V6Aainfix =asizeV13V6Aainfix =V12aNodeV13V14EqamemV12V7FAadistinctV7FIaall_treesainfix -ainfix -V3c1V6agetV5ainfix -ainfix -V3c1V6Aainfix &lt;=c0ainfix -ainfix -V3c1V6Aaall_treesV6agetV5V6Aainfix &lt;=c0V6Iainfix &lt;V6ainfix +V0c1Aainfix &lt;=c0V6Iainfix &lt;ainfix -ainfix -V3c1V6ainfix +V0c1Aainfix &lt;=c0ainfix -ainfix -V3c1V6Iainfix &lt;V3ainfix +V0c1Aainfix &lt;=c0V3Iainfix &lt;asizeV16V6Aainfix =asizeV15V3Aainfix =V15aNodeV16V17EqamemV15agetV5V3FAadistinctagetV5V3Aaall_treesV18agetV5V18Iainfix &lt;V18V3Aainfix &lt;=c0V18FIainfix &lt;=V6ainfix -V3c1Aainfix &lt;=c0V6FFIainfix &lt;=c0ainfix -V3c1Iainfix =V4asetV2V3aNilFIainfix &lt;V3ainfix +V0c1Aainfix &lt;=c0V3Iaall_treesV19agetV2V19Iainfix &lt;V19V3Aainfix &lt;=c0V19FIainfix &lt;=V3V0Aainfix &lt;=c1V3FFIainfix &lt;=c1V0Iainfix =V1asetaconstaNilc0aConsaEmptyaNilFIainfix &lt;c0ainfix +V0c1Aainfix &lt;=c0c0Iainfix &gt;=ainfix +V0c1c0Iainfix &gt;=V0c0F">
<label
name="expl:VC for all_trees"/>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.44"/>
</proof>
<proof
prover="2"
timelimit="5"
......@@ -976,12 +964,12 @@
<result status="valid" time="3.29"/>
</proof>
<proof
prover="7"
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="2.41"/>
<result status="valid" time="1.29"/>
</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