Skip to content

GitLab

Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit c0be075f authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files
Options

Update benchs for Alt-Ergo 0.94.

parent 69e25a42
Hide whitespace changes
Inline Side-by-side
Showing with 43 additions and 31 deletions
examples/programs/euler001/why3session.xml
View file @ c0be075f
......@@ -5,7 +5,11 @@
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
version="0.94"/>
<prover
id="alt-ergo-0.93.1"
name="Alt-Ergo"
version="0.93.1"/>
<prover
id="coq"
name="Coq"
......@@ -202,7 +206,7 @@
<goal
name="triangle_numbers"
sum="91486864bac3972d9c4344d34d1fb5c0"
proved="true"
proved="false"
expanded="true"
shape="ainfix =ainfix *c2adivainfix *V0ainfix +V0c1c2ainfix *V0ainfix +V0c1F">
<proof
......@@ -217,7 +221,7 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
<result status="timeout" time="5.04"/>
</proof>
<proof
prover="z3"
......
examples/programs/isqrt/why3session.xml
View file @ c0be075f
......@@ -5,7 +5,11 @@
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
version="0.94"/>
<prover
id="alt-ergo-0.93.1"
name="Alt-Ergo"
version="0.93.1"/>
<prover
id="coq"
name="Coq"
......@@ -143,18 +147,18 @@
</theory>
<theory
name="WP NewtonMethod"
verified="true"
verified="false"
expanded="true">
<goal
name="WP_parameter sqrt"
expl="parameter sqrt"
sum="a278577017294f8049503d587a4b387e"
proved="true"
proved="false"
expanded="true"
shape="iainfix =V0c0ainfix <V0ainfix *ainfix +c0c1ainfix +c0c1Aainfix <=ainfix *c0c0V0iainfix <=V0c3ainfix <V0ainfix *ainfix +c1c1ainfix +c1c1Aainfix <=ainfix *c1c1V0iainfix <V1V2ainfix <V3V2Aainfix <=c0V2Aainfix <V0ainfix *ainfix +V4c1ainfix +V4c1Aainfix <V0ainfix *ainfix +V3c1ainfix +V3c1Aainfix =V4adivainfix +adivV0V3V3c2Aainfix >V3c0Aainfix >V4c0Iainfix =V4adivainfix +adivV0V1V1c2FIainfix =V3V1Fainfix <V0ainfix *ainfix +V2c1ainfix +V2c1Aainfix <=ainfix *V2V2V0Iainfix <V0ainfix *ainfix +V1c1ainfix +V1c1Aainfix <V0ainfix *ainfix +V2c1ainfix +V2c1Aainfix =V1adivainfix +adivV0V2V2c2Aainfix >V2c0Aainfix >V1c0FFAainfix <V0ainfix *ainfix +adivainfix +V0c1c2c1ainfix +adivainfix +V0c1c2c1Aainfix <V0ainfix *ainfix +V0c1ainfix +V0c1Aainfix =adivainfix +V0c1c2adivainfix +adivV0V0V0c2Aainfix >V0c0Aainfix >adivainfix +V0c1c2c0Iainfix >=V0c0F">
<transf
name="split_goal"
proved="true"
proved="false"
expanded="true">
<goal
name="WP_parameter sqrt.1"
......@@ -302,7 +306,7 @@
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.34"/>
<result status="unknown" time="0.26"/>
</proof>
</goal>
<goal
......@@ -489,7 +493,7 @@
name="WP_parameter sqrt.4.5"
expl="parameter sqrt"
sum="24e8edd0d96bfe68af7dced974d83285"
proved="true"
proved="false"
expanded="false"
shape="ainfix <V0ainfix *ainfix +V4c1ainfix +V4c1Iainfix =V4adivainfix +adivV0V1V1c2FIainfix =V3V1FIainfix <V1V2Iainfix <V0ainfix *ainfix +V1c1ainfix +V1c1Aainfix <V0ainfix *ainfix +V2c1ainfix +V2c1Aainfix =V1adivainfix +adivV0V2V2c2Aainfix >V2c0Aainfix >V1c0FFIainfix <=V0c3NIainfix =V0c0NIainfix >=V0c0F">
<proof
......@@ -497,7 +501,7 @@
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="2.23"/>
<result status="unknown" time="1.59"/>
</proof>
</goal>
</transf>
......
examples/programs/mergesort_list/why3session.xml
View file @ c0be075f
......@@ -5,7 +5,11 @@
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
version="0.94"/>
<prover
id="alt-ergo-0.93.1"
name="Alt-Ergo"
version="0.93.1"/>
<prover
id="coq"
name="Coq"
......@@ -86,7 +90,7 @@
name="WP_parameter split"
expl="parameter split"
sum="23d543578112a107fb4f2cea2da7efe2"
proved="true"
proved="false"
expanded="true"
shape="CV3aNilapermutainfix ++V1V2ainfix ++V1ainfix ++V2V3Aainfix =alengthV2ainfix +alengthV1c1Oainfix =alengthV2alengthV1aConsVVapermutainfix ++V6V7ainfix ++V1ainfix ++V2V3Aainfix =alengthV7ainfix +alengthV6c1Oainfix =alengthV7alengthV6Iapermutainfix ++V6V7ainfix ++V2ainfix ++aConsV4V1V5Aainfix =alengthV7ainfix +alengthV6c1Oainfix =alengthV7alengthV6FAainfix =alengthaConsV4V1ainfix +alengthV2c1Oainfix =alengthaConsV4V1alengthV2Aainfix <alengthV5alengthV3Aainfix <=c0alengthV3Iainfix =alengthV2ainfix +alengthV1c1Oainfix =alengthV2alengthV1FFFAapermutV0ainfix ++V8V9Aainfix <=c1alengthV9Aainfix <=c1alengthV8Iapermutainfix ++V8V9ainfix ++aNilainfix ++aNilV0Aainfix =alengthV9ainfix +alengthV8c1Oainfix =alengthV9alengthV8FAainfix =alengthaNilainfix +alengthaNilc1Oainfix =alengthaNilalengthaNilIainfix >=alengthV0c2F">
<proof
......@@ -94,7 +98,7 @@
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="3.74"/>
<result status="timeout" time="10.03"/>
</proof>
</goal>
<goal
......
examples/programs/vacid_0_binary_heaps/proofs/why3session.xml
View file @ c0be075f
......@@ -5,7 +5,7 @@
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
version="0.94"/>
<prover
id="alt-ergo-0.93.1"
name="Alt-Ergo"
......@@ -2664,11 +2664,11 @@
</file>
<file
name="../heap_implem.mlw"
verified="true"
verified="false"
expanded="false">
<theory
name="WP Implementation"
verified="true"
verified="false"
expanded="false">
<goal
name="Is_heap_min"
......@@ -4350,12 +4350,12 @@
name="WP_parameter extractMin.14"
expl="loop invariant preservation"
sum="96dceb3a4a93d025b1dce841e592844a"
proved="true"
proved="false"
expanded="false"
shape="ainfix <amixfix []V5aparentV6amixfix []V0ainfix -V1c1Iainfix >V6c0Aainfix =aelementsV5c0ainfix -V1c1aaddamixfix []V5V6adiffadiffaelementsV0c0V1asingletonamixfix []V0ainfix -V1c1asingletonamixfix []V0c0Iainfix >ainfix -V1c1c0Aainfix =V5V0Iainfix =V6c0Aais_heap_arrayV5c0ainfix -V1c1Aainfix <V6ainfix -V1c1Iainfix >ainfix -V1c1c0Aainfix <=c0V6Iainfix =V6V4FIainfix =V5amixfix [<-]V3V2amixfix []V3V4FIainfix <=amixfix []V0ainfix -V1c1amixfix []V3V4NIainfix =V4ainfix +ainfix *c2V2c2FIainfix >amixfix []V3ainfix +ainfix *c2V2c1amixfix []V3ainfix +ainfix *c2V2c2Iainfix <ainfix +ainfix *c2V2c2ainfix -V1c1Iainfix >=ainfix +ainfix *c2V2c1ainfix -V1c1NIainfix <V2ainfix -V1c1Iainfix <amixfix []V3aparentV2amixfix []V0ainfix -V1c1Iainfix >V2c0Aainfix =aelementsV3c0ainfix -V1c1aaddamixfix []V3V2adiffadiffaelementsV0c0V1asingletonamixfix []V0ainfix -V1c1asingletonamixfix []V0c0Iainfix >ainfix -V1c1c0Aainfix =V3V0Iainfix =V2c0Aais_heap_arrayV3c0ainfix -V1c1Aainfix <V2ainfix -V1c1Iainfix >ainfix -V1c1c0Aainfix <=c0V2FFIainfix >anb_occamixfix []V0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0c0Iainfix >ainfix -V1c1c0Iainfix >V1c0Iais_heapaTuple2V0V1Aainfix =aelementsV0c0V1aempty_bagNF">
<transf
name="split_goal"
proved="true"
proved="false"
expanded="false">
<goal
name="WP_parameter extractMin.14.1"
......@@ -4461,15 +4461,15 @@
name="WP_parameter extractMin.14.3"
expl="parameter extractMin"
sum="66746da7f042240e777d67d7b23b224b"
proved="true"
proved="false"
expanded="false"
shape="ais_heap_arrayV5c0ainfix -V1c1Iainfix =V6V4FIainfix =V5amixfix [<-]V3V2amixfix []V3V4FIainfix <=amixfix []V0ainfix -V1c1amixfix []V3V4NIainfix =V4ainfix +ainfix *c2V2c2FIainfix >amixfix []V3ainfix +ainfix *c2V2c1amixfix []V3ainfix +ainfix *c2V2c2Iainfix <ainfix +ainfix *c2V2c2ainfix -V1c1Iainfix >=ainfix +ainfix *c2V2c1ainfix -V1c1NIainfix <V2ainfix -V1c1Iainfix <amixfix []V3aparentV2amixfix []V0ainfix -V1c1Iainfix >V2c0Aainfix =aelementsV3c0ainfix -V1c1aaddamixfix []V3V2adiffadiffaelementsV0c0V1asingletonamixfix []V0ainfix -V1c1asingletonamixfix []V0c0Iainfix >ainfix -V1c1c0Aainfix =V3V0Iainfix =V2c0Aais_heap_arrayV3c0ainfix -V1c1Aainfix <V2ainfix -V1c1Iainfix >ainfix -V1c1c0Aainfix <=c0V2FFIainfix >anb_occamixfix []V0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0c0Iainfix >ainfix -V1c1c0Iainfix >V1c0Iais_heapaTuple2V0V1Aainfix =aelementsV0c0V1aempty_bagNF">
<proof
prover="alt-ergo"
timelimit="3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.05"/>
<result status="timeout" time="10.03"/>
</proof>
</goal>
<goal
......@@ -4979,12 +4979,12 @@
name="WP_parameter extractMin.21"
expl="loop invariant preservation"
sum="f95c2451d33fd5382ee4cdda82a250bc"
proved="true"
proved="false"
expanded="false"
shape="ainfix <amixfix []V4aparentV5amixfix []V0ainfix -V1c1Iainfix >V5c0Aainfix =aelementsV4c0ainfix -V1c1aaddamixfix []V4V5adiffadiffaelementsV0c0V1asingletonamixfix []V0ainfix -V1c1asingletonamixfix []V0c0Iainfix >ainfix -V1c1c0Aainfix =V4V0Iainfix =V5c0Aais_heap_arrayV4c0ainfix -V1c1Aainfix <V5ainfix -V1c1Iainfix >ainfix -V1c1c0Aainfix <=c0V5Iainfix =V5ainfix +ainfix *c2V2c1FIainfix =V4amixfix [<-]V3V2amixfix []V3ainfix +ainfix *c2V2c1FIainfix <=amixfix []V0ainfix -V1c1amixfix []V3ainfix +ainfix *c2V2c1NIainfix >amixfix []V3ainfix +ainfix *c2V2c1amixfix []V3ainfix +ainfix *c2V2c2NIainfix <ainfix +ainfix *c2V2c2ainfix -V1c1Iainfix >=ainfix +ainfix *c2V2c1ainfix -V1c1NIainfix <V2ainfix -V1c1Iainfix <amixfix []V3aparentV2amixfix []V0ainfix -V1c1Iainfix >V2c0Aainfix =aelementsV3c0ainfix -V1c1aaddamixfix []V3V2adiffadiffaelementsV0c0V1asingletonamixfix []V0ainfix -V1c1asingletonamixfix []V0c0Iainfix >ainfix -V1c1c0Aainfix =V3V0Iainfix =V2c0Aais_heap_arrayV3c0ainfix -V1c1Aainfix <V2ainfix -V1c1Iainfix >ainfix -V1c1c0Aainfix <=c0V2FFIainfix >anb_occamixfix []V0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0c0Iainfix >ainfix -V1c1c0Iainfix >V1c0Iais_heapaTuple2V0V1Aainfix =aelementsV0c0V1aempty_bagNF">
<transf
name="split_goal"
proved="true"
proved="false"
expanded="false">
<goal
name="WP_parameter extractMin.21.1"
......@@ -5090,15 +5090,15 @@
name="WP_parameter extractMin.21.3"
expl="parameter extractMin"
sum="2d0484d5a5eb0ba98bf82c4aef036342"
proved="true"
proved="false"
expanded="false"
shape="ais_heap_arrayV4c0ainfix -V1c1Iainfix =V5ainfix +ainfix *c2V2c1FIainfix =V4amixfix [<-]V3V2amixfix []V3ainfix +ainfix *c2V2c1FIainfix <=amixfix []V0ainfix -V1c1amixfix []V3ainfix +ainfix *c2V2c1NIainfix >amixfix []V3ainfix +ainfix *c2V2c1amixfix []V3ainfix +ainfix *c2V2c2NIainfix <ainfix +ainfix *c2V2c2ainfix -V1c1Iainfix >=ainfix +ainfix *c2V2c1ainfix -V1c1NIainfix <V2ainfix -V1c1Iainfix <amixfix []V3aparentV2amixfix []V0ainfix -V1c1Iainfix >V2c0Aainfix =aelementsV3c0ainfix -V1c1aaddamixfix []V3V2adiffadiffaelementsV0c0V1asingletonamixfix []V0ainfix -V1c1asingletonamixfix []V0c0Iainfix >ainfix -V1c1c0Aainfix =V3V0Iainfix =V2c0Aais_heap_arrayV3c0ainfix -V1c1Aainfix <V2ainfix -V1c1Iainfix >ainfix -V1c1c0Aainfix <=c0V2FFIainfix >anb_occamixfix []V0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0c0Iainfix >ainfix -V1c1c0Iainfix >V1c0Iais_heapaTuple2V0V1Aainfix =aelementsV0c0V1aempty_bagNF">
<proof
prover="alt-ergo"
timelimit="3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.04"/>
<result status="timeout" time="10.03"/>
</proof>
</goal>
<goal
......@@ -5389,12 +5389,12 @@
name="WP_parameter extractMin.28"
expl="loop invariant preservation"
sum="3ac0e5e32d0658c93dc03e6ad58f9e84"
proved="true"
proved="false"
expanded="false"
shape="ainfix <amixfix []V4aparentV5amixfix []V0ainfix -V1c1Iainfix >V5c0Aainfix =aelementsV4c0ainfix -V1c1aaddamixfix []V4V5adiffadiffaelementsV0c0V1asingletonamixfix []V0ainfix -V1c1asingletonamixfix []V0c0Iainfix >ainfix -V1c1c0Aainfix =V4V0Iainfix =V5c0Aais_heap_arrayV4c0ainfix -V1c1Aainfix <V5ainfix -V1c1Iainfix >ainfix -V1c1c0Aainfix <=c0V5Iainfix =V5ainfix +ainfix *c2V2c1FIainfix =V4amixfix [<-]V3V2amixfix []V3ainfix +ainfix *c2V2c1FIainfix <=amixfix []V0ainfix -V1c1amixfix []V3ainfix +ainfix *c2V2c1NIainfix <ainfix +ainfix *c2V2c2ainfix -V1c1NIainfix >=ainfix +ainfix *c2V2c1ainfix -V1c1NIainfix <V2ainfix -V1c1Iainfix <amixfix []V3aparentV2amixfix []V0ainfix -V1c1Iainfix >V2c0Aainfix =aelementsV3c0ainfix -V1c1aaddamixfix []V3V2adiffadiffaelementsV0c0V1asingletonamixfix []V0ainfix -V1c1asingletonamixfix []V0c0Iainfix >ainfix -V1c1c0Aainfix =V3V0Iainfix =V2c0Aais_heap_arrayV3c0ainfix -V1c1Aainfix <V2ainfix -V1c1Iainfix >ainfix -V1c1c0Aainfix <=c0V2FFIainfix >anb_occamixfix []V0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0c0Iainfix >ainfix -V1c1c0Iainfix >V1c0Iais_heapaTuple2V0V1Aainfix =aelementsV0c0V1aempty_bagNF">
<transf
name="split_goal"
proved="true"
proved="false"
expanded="false">
<goal
name="WP_parameter extractMin.28.1"
......@@ -5500,15 +5500,15 @@
name="WP_parameter extractMin.28.3"
expl="parameter extractMin"
sum="c74ee239121c81d8866aea126946c2db"
proved="true"
proved="false"
expanded="false"
shape="ais_heap_arrayV4c0ainfix -V1c1Iainfix =V5ainfix +ainfix *c2V2c1FIainfix =V4amixfix [<-]V3V2amixfix []V3ainfix +ainfix *c2V2c1FIainfix <=amixfix []V0ainfix -V1c1amixfix []V3ainfix +ainfix *c2V2c1NIainfix <ainfix +ainfix *c2V2c2ainfix -V1c1NIainfix >=ainfix +ainfix *c2V2c1ainfix -V1c1NIainfix <V2ainfix -V1c1Iainfix <amixfix []V3aparentV2amixfix []V0ainfix -V1c1Iainfix >V2c0Aainfix =aelementsV3c0ainfix -V1c1aaddamixfix []V3V2adiffadiffaelementsV0c0V1asingletonamixfix []V0ainfix -V1c1asingletonamixfix []V0c0Iainfix >ainfix -V1c1c0Aainfix =V3V0Iainfix =V2c0Aais_heap_arrayV3c0ainfix -V1c1Aainfix <V2ainfix -V1c1Iainfix >ainfix -V1c1c0Aainfix <=c0V2FFIainfix >anb_occamixfix []V0ainfix -V1c1adiffaelementsV0c0V1asingletonamixfix []V0c0c0Iainfix >ainfix -V1c1c0Iainfix >V1c0Iais_heapaTuple2V0V1Aainfix =aelementsV0c0V1aempty_bagNF">
<proof
prover="alt-ergo"
timelimit="3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.05"/>
<result status="timeout" time="10.09"/>
</proof>
</goal>
<goal
......
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