Commit 1de56fdb authored by Andrei Paskevich's avatar Andrei Paskevich

update the shapes to v5 in regtests

not updated:
- stdlib/array - the proof is broken
- ring_decision/ - not replayed, proof broken
- in_progress/, util/, prover/bench/ - not replayed
parent 149c9bd9
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="1" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="2" name="Vampire" version="0.6" timelimit="5" steplimit="0" memlimit="0"/>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="0" name="Coq" version="8.7.1" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="0" name="Coq" version="8.7.1" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="1" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="0" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../add_list.mlw" proved="true">
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="0" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../add_list_vc_sp.mlw" proved="true">
<theory name="AddListRec" proved="true">
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../algo63.mlw" proved="true">
<theory name="Algo63" proved="true">
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../algo63.mlw" proved="true">
<theory name="Algo63" proved="true">
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../algo64.mlw" proved="true">
<theory name="Algo64" proved="true">
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../algo65.mlw" proved="true">
<theory name="Algo65" proved="true">
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../all_distinct.mlw" proved="true">
<theory name="AllDistinct" proved="true">
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../arm.mlw" proved="true">
<theory name="M" proved="true">
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../assigning_meanings_to_programs.mlw" proved="true">
<theory name="Sum" proved="true">
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../avl.mlw" proved="true">
<theory name="AVL" proved="true">
......@@ -190,7 +190,7 @@
<proof prover="1"><result status="valid" time="0.01" steps="183"/></proof>
</goal>
<goal name="VC join.6" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.20" steps="460"/></proof>
<proof prover="1"><result status="valid" time="0.08" steps="460"/></proof>
</goal>
<goal name="VC join.7" expl="postcondition" proved="true">
<proof prover="1" timelimit="5"><result status="valid" time="1.59" steps="5680"/></proof>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<file name="../key_type.mlw" proved="true">
</file>
</why3session>
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="1" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../monoid.mlw" proved="true">
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../preorder.mlw" proved="true">
<theory name="Full" proved="true">
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="1" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
......@@ -507,7 +507,7 @@
<proof prover="4"><result status="valid" time="0.03" steps="67"/></proof>
</goal>
<goal name="VC remove_count.1" expl="postcondition" proved="true">
<proof prover="1" timelimit="10"><result status="valid" time="5.65"/></proof>
<proof prover="1" timelimit="10"><result status="valid" time="4.68"/></proof>
</goal>
<goal name="VC remove_count.2" expl="postcondition" proved="true">
<proof prover="1" timelimit="10"><result status="valid" time="0.47"/></proof>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../ral.mlw" proved="true">
<theory name="RAL" proved="true">
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="4" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../tables.mlw" proved="true">
......@@ -134,7 +134,7 @@
<proof prover="5"><result status="valid" time="0.17" steps="294"/></proof>
</goal>
<goal name="VC selected_model.0.8" expl="postcondition" proved="true">
<proof prover="5" timelimit="20"><result status="valid" time="8.76" steps="15210"/></proof>
<proof prover="5" timelimit="20"><result status="valid" time="7.75" steps="15210"/></proof>
</goal>
<goal name="VC selected_model.0.9" expl="postcondition" proved="true">
<proof prover="5" timelimit="20"><result status="valid" time="5.74" steps="8946"/></proof>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="0" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../balance.mlw" proved="true">
<theory name="Puzzle8" proved="true">
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="0" name="Eprover" version="2.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../bellman_ford.mlw" proved="true">
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="0" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.4.0" timelimit="1" steplimit="0" memlimit="1000"/>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../binary_multiplication.mlw" proved="true">
<theory name="BinaryMultiplication" proved="true">
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../binary_search.mlw" proved="true">
<theory name="BinarySearch" proved="true">
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="0" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../binary_search_vc_sp.mlw" proved="true">
<theory name="BinarySearch" proved="true">
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="8" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../binary_sort.mlw" proved="true">
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="2" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../binary_sqrt.mlw" proved="true">
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="0" name="CVC4" version="1.4" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="2" name="Eprover" version="1.8-001" timelimit="10" steplimit="0" memlimit="1000"/>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="2" name="Z3" version="4.4.1" alternative="noBV" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="4" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="0" memlimit="4000"/>
......@@ -595,7 +595,7 @@
</goal>
<goal name="VC count.2" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.64"/></proof>
<proof prover="2"><result status="valid" time="0.46"/></proof>
<proof prover="4"><result status="valid" time="0.08"/></proof>
<proof prover="5"><result status="valid" time="0.12"/></proof>
<proof prover="6"><result status="valid" time="0.05" steps="86"/></proof>
......@@ -642,7 +642,7 @@
<proof prover="6"><result status="valid" time="0.23" steps="450"/></proof>
</goal>
<goal name="numof_ytpmE" proved="true">
<proof prover="0"><result status="valid" time="1.20"/></proof>
<proof prover="0"><result status="valid" time="0.94"/></proof>
<proof prover="4"><result status="valid" time="1.22"/></proof>
</goal>
<goal name="VC separation" expl="VC for separation" proved="true">
......@@ -677,13 +677,13 @@
<transf name="split_goal_right" proved="true" >
<goal name="VC triangleInequalityInt.0.0" expl="VC for triangleInequalityInt" proved="true">
<proof prover="0"><result status="valid" time="0.07"/></proof>
<proof prover="2"><result status="valid" time="0.22"/></proof>
<proof prover="2"><result status="valid" time="0.09"/></proof>
<proof prover="4"><result status="valid" time="0.09"/></proof>
<proof prover="5" memlimit="1000"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.03" steps="79"/></proof>
</goal>
<goal name="VC triangleInequalityInt.0.1" expl="VC for triangleInequalityInt" proved="true">
<proof prover="0" timelimit="10"><result status="valid" time="5.77"/></proof>
<proof prover="0" timelimit="10"><result status="valid" time="4.92"/></proof>
</goal>
</transf>
</goal>
......@@ -751,7 +751,7 @@
<proof prover="5"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC count_or.1" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.23"/></proof>
<proof prover="2"><result status="valid" time="0.10"/></proof>
<proof prover="4"><result status="valid" time="0.10"/></proof>
<proof prover="6"><result status="valid" time="0.03" steps="90"/></proof>
</goal>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../bitvector_examples.mlw" proved="true">
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
......@@ -170,7 +170,7 @@
<proof prover="3" timelimit="3"><result status="valid" time="0.07"/></proof>
<proof prover="4"><result status="valid" time="0.05" steps="71"/></proof>
<proof prover="6"><result status="valid" time="0.05"/></proof>
<proof prover="9" timelimit="9"><result status="valid" time="2.90"/></proof>
<proof prover="9" timelimit="9"><result status="valid" time="2.45"/></proof>
<proof prover="10"><result status="valid" time="0.53"/></proof>
</goal>
<goal name="to_nat_0x00000000" proved="true">
......@@ -178,13 +178,13 @@
<proof prover="10"><result status="valid" time="0.52"/></proof>
</goal>
<goal name="to_nat_0x00000001" proved="true">
<proof prover="4" timelimit="30"><result status="valid" time="7.31" steps="2706"/></proof>
<proof prover="4" timelimit="30"><result status="valid" time="6.45" steps="2706"/></proof>
</goal>
<goal name="to_nat_0x00000003" proved="true">
<proof prover="6" timelimit="120"><result status="valid" time="69.36"/></proof>
<proof prover="6" timelimit="120"><result status="valid" time="53.64"/></proof>
</goal>
<goal name="to_nat_0x00000007" proved="true">
<proof prover="4" timelimit="30"><result status="valid" time="11.44" steps="2976"/></proof>
<proof prover="4" timelimit="30"><result status="valid" time="9.99" steps="2976"/></proof>
</goal>
<goal name="to_nat_0x0000000F" proved="true">
<proof prover="4" timelimit="30"><result status="valid" time="9.19" steps="2846"/></proof>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="0" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Eprover" version="2.0" timelimit="1" steplimit="0" memlimit="1000"/>
......@@ -60,7 +60,7 @@
<proof prover="10"><result status="valid" time="0.11" steps="101"/></proof>
</goal>
<goal name="nth_const6" proved="true">
<proof prover="4"><result status="valid" time="1.68"/></proof>
<proof prover="4"><result status="valid" time="1.36"/></proof>
<proof prover="8"><result status="valid" time="0.79"/></proof>
<proof prover="10"><result status="valid" time="0.09" steps="101"/></proof>
</goal>
......@@ -153,7 +153,7 @@
</goal>
<goal name="to_nat_sub_0_30" proved="true">
<proof prover="4"><result status="valid" time="1.21"/></proof>
<proof prover="6" timelimit="10"><result status="valid" time="3.16"/></proof>
<proof prover="6" timelimit="10"><result status="valid" time="2.64"/></proof>
<proof prover="8"><result status="valid" time="0.84"/></proof>
</goal>
<goal name="jpxorx_pos" proved="true">
......@@ -164,7 +164,7 @@
<proof prover="10"><result status="valid" time="0.13" steps="148"/></proof>
</goal>
<goal name="from_int2c_to_nat_sub_pos" proved="true">
<proof prover="5" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_pos_1.v"><result status="valid" time="0.78"/></proof>
<proof prover="5" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_pos_1.v"><result status="valid" time="0.56"/></proof>
</goal>
<goal name="lemma1_pos" proved="true">
<transf name="split_all_full" proved="true" >
......@@ -230,7 +230,7 @@
</goal>
<goal name="nth_var3" proved="true">
<proof prover="4"><result status="valid" time="1.25"/></proof>
<proof prover="8"><result status="valid" time="0.88"/></proof>
<proof prover="8"><result status="valid" time="0.69"/></proof>
<proof prover="10"><result status="valid" time="0.14" steps="147"/></proof>
</goal>
<goal name="lemma2" proved="true">
......@@ -249,12 +249,12 @@
</transf>
</goal>
<goal name="nth_var4" proved="true">
<proof prover="4"><result status="valid" time="1.88"/></proof>
<proof prover="4"><result status="valid" time="1.50"/></proof>
<proof prover="8"><result status="valid" time="0.85"/></proof>
<proof prover="10"><result status="valid" time="0.14" steps="149"/></proof>
</goal>
<goal name="nth_var5" proved="true">
<proof prover="4"><result status="valid" time="1.88"/></proof>
<proof prover="4"><result status="valid" time="1.51"/></proof>
<proof prover="8"><result status="valid" time="0.85"/></proof>
<proof prover="10"><result status="valid" time="0.16" steps="149"/></proof>
</goal>
......@@ -308,7 +308,7 @@
<goal name="var_value0.0.0.0" proved="true">
<transf name="rewrite" proved="true" arg1="sign_var">
<goal name="var_value0.0.0.0.0" proved="true">
<proof prover="3"><result status="valid" time="0.84"/></proof>
<proof prover="3"><result status="valid" time="0.64"/></proof>
<transf name="split_all_full" proved="true" >
<goal name="var_value0.0.0.0.0.0" proved="true">
<proof prover="10" timelimit="10" memlimit="4000"><result status="valid" time="1.05" steps="271"/></proof>
......@@ -363,7 +363,7 @@
<goal name="MainResult" proved="true">
<proof prover="2"><result status="valid" time="0.26"/></proof>
<proof prover="4"><result status="valid" time="3.62"/></proof>
<proof prover="6" timelimit="11"><result status="valid" time="3.12"/></proof>
<proof prover="6" timelimit="11"><result status="valid" time="2.70"/></proof>
<proof prover="8"><result status="valid" time="0.74"/></proof>
<proof prover="10"><result status="valid" time="0.26" steps="146"/></proof>
</goal>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="3.2" timelimit="10" steplimit="0" memlimit="1000"/>
......@@ -34,7 +34,7 @@
<proof prover="9"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="MainResultBits" proved="true">
<proof prover="0"><result status="valid" time="0.15" steps="104"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="104"/></proof>
<proof prover="3"><result status="valid" time="1.06"/></proof>
</goal>
<goal name="MainResultSign" proved="true">
......@@ -54,7 +54,7 @@
<proof prover="9"><result status="valid" time="0.69"/></proof>
</goal>
<goal name="Mantissa_of_xor_j" proved="true">
<proof prover="3"><result status="valid" time="1.72"/></proof>
<proof prover="3"><result status="valid" time="1.43"/></proof>
<proof prover="5"><result status="valid" time="3.22"/></proof>
<proof prover="9"><result status="valid" time="0.75"/></proof>
</goal>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="0" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Eprover" version="2.0" timelimit="5" steplimit="0" memlimit="2000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
......@@ -272,7 +272,7 @@