Skip to content

GitLab

why3
why3
Commit 26776eb9 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

updated sessions

parent d7a230da
Hide whitespace changes
Inline Side-by-side
Showing with 11 additions and 11 deletions
examples/logic/genealogy/why3session.xml
View file @ 26776eb9
......@@ -37,7 +37,7 @@
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="unknown" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.01"/></proof>
......@@ -90,7 +90,7 @@
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="unknown" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.01"/></proof>
<proof prover="9"><result status="valid" time="0.01"/></proof>
......
examples/vacid_0_red_black_trees/why3session.xml
View file @ 26776eb9
......@@ -672,7 +672,7 @@
<proof prover="7" memlimit="1000"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="WP_parameter lbalance.9.2" expl="2. VC for lbalance">
<proof prover="4"><result status="timeout" time="5.03"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="7" memlimit="1000"><result status="valid" time="0.34" steps="304"/></proof>
</goal>
<goal name="WP_parameter lbalance.9.3" expl="3. VC for lbalance">
......@@ -696,7 +696,7 @@
<proof prover="7" memlimit="1000"><result status="valid" time="0.02" steps="18"/></proof>
</goal>
<goal name="WP_parameter lbalance.10.2" expl="2. VC for lbalance">
<proof prover="4"><result status="timeout" time="5.03"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="7" memlimit="1000"><result status="valid" time="0.12" steps="169"/></proof>
</goal>
<goal name="WP_parameter lbalance.10.3" expl="3. VC for lbalance">
......@@ -714,18 +714,18 @@
</transf>
</goal>
<goal name="WP_parameter lbalance.11" expl="11. postcondition" expanded="true">
<proof prover="0"><result status="valid" time="1.20" steps="1173"/></proof>
<proof prover="0"><result status="valid" time="0.68" steps="1173"/></proof>
</goal>
<goal name="WP_parameter lbalance.12" expl="12. postcondition">
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="7" memlimit="1000"><result status="valid" time="0.07" steps="159"/></proof>
</goal>
<goal name="WP_parameter lbalance.13" expl="13. postcondition">
<proof prover="4"><result status="timeout" time="6.01"/></proof>
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="7" memlimit="1000"><result status="valid" time="2.57" steps="763"/></proof>
</goal>
<goal name="WP_parameter lbalance.14" expl="14. postcondition">
<proof prover="4"><result status="timeout" time="5.06"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="7" memlimit="1000"><result status="valid" time="0.18" steps="202"/></proof>
</goal>
<goal name="WP_parameter lbalance.15" expl="15. postcondition">
......@@ -1244,7 +1244,7 @@
<proof prover="7" memlimit="1000"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter rbalance.9.2" expl="2. VC for rbalance">
<proof prover="4"><result status="timeout" time="5.03"/></proof>
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="7" memlimit="1000"><result status="valid" time="0.36" steps="304"/></proof>
</goal>
<goal name="WP_parameter rbalance.9.3" expl="3. VC for rbalance">
......@@ -1268,7 +1268,7 @@
<proof prover="7" memlimit="1000"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="WP_parameter rbalance.10.2" expl="2. VC for rbalance">
<proof prover="4"><result status="timeout" time="5.04"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="7" memlimit="1000"><result status="valid" time="0.15" steps="192"/></proof>
</goal>
<goal name="WP_parameter rbalance.10.3" expl="3. VC for rbalance">
......@@ -1299,7 +1299,7 @@
<proof prover="7" memlimit="1000"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="WP_parameter rbalance.13.2" expl="2. VC for rbalance">
<proof prover="4"><result status="timeout" time="5.03"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="7" memlimit="1000"><result status="valid" time="0.18" steps="235"/></proof>
</goal>
<goal name="WP_parameter rbalance.13.3" expl="3. VC for rbalance">
......@@ -1317,7 +1317,7 @@
</transf>
</goal>
<goal name="WP_parameter rbalance.14" expl="14. postcondition">
<proof prover="4"><result status="timeout" time="5.45"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="7" memlimit="1000"><result status="valid" time="0.17" steps="202"/></proof>
</goal>
<goal name="WP_parameter rbalance.15" expl="15. postcondition">
......
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