Commit bcee7827 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Update shapes.

parent 7978c59b
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN" <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5"> <why3session shape_version="6">
<prover id="0" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/> <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"/> <prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../add_list.mlw" proved="true"> <file proved="true">
<path name=".."/>
<path name="add_list.mlw"/>
<theory name="AddListRec" proved="true"> <theory name="AddListRec" proved="true">
<goal name="VC sum" expl="VC for sum" proved="true"> <goal name="VC sum" expl="VC for sum" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="92"/></proof> <proof prover="2"><result status="valid" time="0.02" steps="92"/></proof>
......
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN" <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5"> <why3session shape_version="6">
<prover id="0" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="0" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../add_list_vc_sp.mlw" proved="true"> <file proved="true">
<path name=".."/>
<path name="add_list_vc_sp.mlw"/>
<theory name="AddListRec" proved="true"> <theory name="AddListRec" proved="true">
<goal name="VC sum" expl="VC for sum" proved="true"> <goal name="VC sum" expl="VC for sum" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof> <proof prover="0"><result status="valid" time="0.04"/></proof>
......
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN" <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5"> <why3session shape_version="6">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../binary_multiplication.mlw" proved="true"> <file proved="true">
<path name=".."/>
<path name="binary_multiplication.mlw"/>
<theory name="BinaryMultiplication" proved="true"> <theory name="BinaryMultiplication" proved="true">
<goal name="VC binary_mult" expl="VC for binary_mult" proved="true"> <goal name="VC binary_mult" expl="VC for binary_mult" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="63"/></proof> <proof prover="0"><result status="valid" time="0.05" steps="63"/></proof>
......
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN" <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5"> <why3session shape_version="6">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
<file proved="true"> <file proved="true">
<path name=".."/> <path name=".."/>
......
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN" <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5"> <why3session shape_version="6">
<prover id="0" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="0" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file proved="true"> <file proved="true">
<path name=".."/> <path name=".."/>
......
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN" <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5"> <why3session shape_version="6">
<prover id="2" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/> <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"/> <prover id="3" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../binary_sqrt.mlw" proved="true"> <file proved="true">
<path name=".."/>
<path name="binary_sqrt.mlw"/>
<theory name="BinarySqrt" proved="true"> <theory name="BinarySqrt" proved="true">
<goal name="VC sqrt" expl="VC for sqrt" proved="true"> <goal name="VC sqrt" expl="VC for sqrt" proved="true">
<transf name="split_goal_right" proved="true" > <transf name="split_goal_right" proved="true" >
......
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN" <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5"> <why3session shape_version="6">
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="4000"/> <prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="1" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="1" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.4.1" alternative="noBV" 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"/> <prover id="4" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="5" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="4000"/> <prover id="5" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="6" name="Alt-Ergo" version="2.0.0" timelimit="6" steplimit="0" memlimit="4000"/> <prover id="6" name="Alt-Ergo" version="2.0.0" timelimit="6" steplimit="0" memlimit="4000"/>
<file name="../bitcount.mlw" proved="true"> <file proved="true">
<path name=".."/>
<path name="bitcount.mlw"/>
<theory name="BitCount8bit_fact" proved="true"> <theory name="BitCount8bit_fact" proved="true">
<goal name="nth_as_bv_is_int" proved="true"> <goal name="nth_as_bv_is_int" proved="true">
<proof prover="0"><result status="valid" time="0.05"/></proof> <proof prover="0"><result status="valid" time="0.05"/></proof>
...@@ -45,15 +47,11 @@ ...@@ -45,15 +47,11 @@
<proof prover="6"><result status="valid" time="0.04" steps="78"/></proof> <proof prover="6"><result status="valid" time="0.04" steps="78"/></proof>
</goal> </goal>
<goal name="VC step2.1" expl="precondition" proved="true"> <goal name="VC step2.1" expl="precondition" proved="true">
<transf name="split_goal_right" proved="true" > <proof prover="0"><result status="valid" time="0.04"/></proof>
<goal name="VC step2.1.0" expl="precondition" proved="true"> <proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="0"><result status="valid" time="0.04"/></proof> <proof prover="4"><result status="valid" time="0.07"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.07"/></proof> <proof prover="6"><result status="valid" time="0.02" steps="80"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.02" steps="80"/></proof>
</goal>
</transf>
</goal> </goal>
<goal name="VC step2.2" expl="precondition" proved="true"> <goal name="VC step2.2" expl="precondition" proved="true">
<transf name="split_goal_right" proved="true" > <transf name="split_goal_right" proved="true" >
...@@ -74,17 +72,21 @@ ...@@ -74,17 +72,21 @@
</transf> </transf>
</goal> </goal>
<goal name="VC step2.3" expl="precondition" proved="true"> <goal name="VC step2.3" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof> <transf name="split_goal_right" proved="true" >
<proof prover="2"><result status="valid" time="0.02"/></proof> <goal name="VC step2.3.0" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.07"/></proof> <proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.02" steps="83"/></proof> <proof prover="4"><result status="valid" time="0.07"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.02" steps="83"/></proof>
</goal>
</transf>
</goal> </goal>
<goal name="VC step2.4" expl="assertion" proved="true"> <goal name="VC step2.4" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" > <transf name="split_goal_right" proved="true" >
<goal name="VC step2.4.0" expl="assertion" proved="true"> <goal name="VC step2.4.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.11"/></proof> <proof prover="0"><result status="valid" time="0.11"/></proof>
<proof prover="2"><result status="valid" time="0.48"/></proof> <proof prover="2"><result status="valid" time="0.69"/></proof>
<proof prover="4"><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.10" steps="104"/></proof> <proof prover="6"><result status="valid" time="0.10" steps="104"/></proof>
</goal> </goal>
...@@ -101,7 +103,7 @@ ...@@ -101,7 +103,7 @@
<proof prover="0"><result status="valid" time="0.04"/></proof> <proof prover="0"><result status="valid" time="0.04"/></proof>
</goal> </goal>
<goal name="VC step2.4.4" expl="assertion" proved="true"> <goal name="VC step2.4.4" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="2.87"/></proof> <proof prover="0"><result status="valid" time="3.60"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
...@@ -109,7 +111,7 @@ ...@@ -109,7 +111,7 @@
<proof prover="0"><result status="valid" time="0.05"/></proof> <proof prover="0"><result status="valid" time="0.05"/></proof>
<proof prover="4"><result status="valid" time="0.12"/></proof> <proof prover="4"><result status="valid" time="0.12"/></proof>
<proof prover="5"><result status="valid" time="0.04"/></proof> <proof prover="5"><result status="valid" time="0.04"/></proof>
<proof prover="6" timelimit="5" memlimit="1000"><result status="valid" time="2.64" steps="1399"/></proof> <proof prover="6" timelimit="5" memlimit="1000"><result status="valid" time="3.17" steps="1399"/></proof>
</goal> </goal>
<goal name="VC step2.6" expl="postcondition" proved="true"> <goal name="VC step2.6" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.10"/></proof> <proof prover="0"><result status="valid" time="0.10"/></proof>
...@@ -129,8 +131,8 @@ ...@@ -129,8 +131,8 @@
<proof prover="6"><result status="valid" time="0.04" steps="79"/></proof> <proof prover="6"><result status="valid" time="0.04" steps="79"/></proof>
</goal> </goal>
<goal name="VC prove.1" expl="precondition" proved="true"> <goal name="VC prove.1" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof> <proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.06"/></proof> <proof prover="4"><result status="valid" time="0.06"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof> <proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.04" steps="81"/></proof> <proof prover="6"><result status="valid" time="0.04" steps="81"/></proof>
...@@ -139,7 +141,7 @@ ...@@ -139,7 +141,7 @@
<proof prover="0"><result status="valid" time="0.04"/></proof> <proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.06"/></proof> <proof prover="4"><result status="valid" time="0.06"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof> <proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.04" steps="81"/></proof> <proof prover="6"><result status="valid" time="0.04" steps="81"/></proof>
</goal> </goal>
<goal name="VC prove.3" expl="precondition" proved="true"> <goal name="VC prove.3" expl="precondition" proved="true">
...@@ -150,8 +152,8 @@ ...@@ -150,8 +152,8 @@
<proof prover="6"><result status="valid" time="0.04" steps="81"/></proof> <proof prover="6"><result status="valid" time="0.04" steps="81"/></proof>
</goal> </goal>
<goal name="VC prove.4" expl="precondition" proved="true"> <goal name="VC prove.4" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof> <proof prover="0"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.06"/></proof> <proof prover="4"><result status="valid" time="0.06"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof> <proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.04" steps="83"/></proof> <proof prover="6"><result status="valid" time="0.04" steps="83"/></proof>
...@@ -160,7 +162,7 @@ ...@@ -160,7 +162,7 @@
<proof prover="0"><result status="valid" time="0.04"/></proof> <proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.06"/></proof> <proof prover="4"><result status="valid" time="0.06"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof> <proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.04" steps="83"/></proof> <proof prover="6"><result status="valid" time="0.04" steps="83"/></proof>
</goal> </goal>
<goal name="VC prove.6" expl="assertion" proved="true"> <goal name="VC prove.6" expl="assertion" proved="true">
...@@ -300,7 +302,7 @@ ...@@ -300,7 +302,7 @@
<proof prover="5"><result status="valid" time="0.12"/></proof> <proof prover="5"><result status="valid" time="0.12"/></proof>
</goal> </goal>
<goal name="VC proof1.6.2" expl="VC for proof1" proved="true"> <goal name="VC proof1.6.2" expl="VC for proof1" proved="true">
<proof prover="4"><result status="valid" time="1.00"/></proof> <proof prover="4"><result status="valid" time="1.41"/></proof>
<proof prover="6"><result status="valid" time="0.04" steps="96"/></proof> <proof prover="6"><result status="valid" time="0.04" steps="96"/></proof>
</goal> </goal>
</transf> </transf>
...@@ -451,7 +453,7 @@ ...@@ -451,7 +453,7 @@
<proof prover="6"><result status="valid" time="0.04" steps="87"/></proof> <proof prover="6"><result status="valid" time="0.04" steps="87"/></proof>
</goal> </goal>
<goal name="VC proof3.8" expl="assertion" proved="true"> <goal name="VC proof3.8" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.51"/></proof> <proof prover="2"><result status="valid" time="0.67"/></proof>
<proof prover="4"><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.05" steps="114"/></proof> <proof prover="6"><result status="valid" time="0.05" steps="114"/></proof>
</goal> </goal>
...@@ -476,7 +478,7 @@ ...@@ -476,7 +478,7 @@
</goal> </goal>
<goal name="VC proof3.11.2" expl="VC for proof3" proved="true"> <goal name="VC proof3.11.2" expl="VC for proof3" proved="true">
<proof prover="4"><result status="valid" time="0.08"/></proof> <proof prover="4"><result status="valid" time="0.08"/></proof>
<proof prover="5"><result status="valid" time="3.61"/></proof> <proof prover="5"><result status="valid" time="4.08"/></proof>
<proof prover="6"><result status="valid" time="0.03" steps="101"/></proof> <proof prover="6"><result status="valid" time="0.03" steps="101"/></proof>
</goal> </goal>
</transf> </transf>
...@@ -596,7 +598,7 @@ ...@@ -596,7 +598,7 @@
</goal> </goal>
<goal name="VC count.2" expl="precondition" proved="true"> <goal name="VC count.2" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.46"/></proof> <proof prover="2"><result status="valid" time="0.61"/></proof>
<proof prover="4"><result status="valid" time="0.08"/></proof> <proof prover="4"><result status="valid" time="0.08"/></proof>
<proof prover="5"><result status="valid" time="0.12"/></proof> <proof prover="5"><result status="valid" time="0.12"/></proof>
<proof prover="6"><result status="valid" time="0.05" steps="86"/></proof> <proof prover="6"><result status="valid" time="0.05" steps="86"/></proof>
...@@ -620,7 +622,7 @@ ...@@ -620,7 +622,7 @@
<proof prover="2"><result status="valid" time="0.22"/></proof> <proof prover="2"><result status="valid" time="0.22"/></proof>
<proof prover="4"><result status="valid" time="0.09"/></proof> <proof prover="4"><result status="valid" time="0.09"/></proof>
<proof prover="5"><result status="valid" time="0.04"/></proof> <proof prover="5"><result status="valid" time="0.04"/></proof>
<proof prover="6"><result status="valid" time="0.05" steps="159"/></proof> <proof prover="6"><result status="valid" time="0.05" steps="86"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
...@@ -643,8 +645,8 @@ ...@@ -643,8 +645,8 @@
<proof prover="6"><result status="valid" time="0.23" steps="450"/></proof> <proof prover="6"><result status="valid" time="0.23" steps="450"/></proof>
</goal> </goal>
<goal name="numof_ytpmE" proved="true"> <goal name="numof_ytpmE" proved="true">
<proof prover="0"><result status="valid" time="0.94"/></proof> <proof prover="0"><result status="valid" time="1.42"/></proof>
<proof prover="4"><result status="valid" time="1.22"/></proof> <proof prover="4"><result status="valid" time="1.52"/></proof>
</goal> </goal>
<goal name="VC separation" expl="VC for separation" proved="true"> <goal name="VC separation" expl="VC for separation" proved="true">
<transf name="split_goal_right" proved="true" > <transf name="split_goal_right" proved="true" >
...@@ -684,7 +686,7 @@ ...@@ -684,7 +686,7 @@
<proof prover="6"><result status="valid" time="0.03" steps="79"/></proof> <proof prover="6"><result status="valid" time="0.03" steps="79"/></proof>
</goal> </goal>
<goal name="VC triangleInequalityInt.0.1" expl="VC for triangleInequalityInt" proved="true"> <goal name="VC triangleInequalityInt.0.1" expl="VC for triangleInequalityInt" proved="true">
<proof prover="0" timelimit="10"><result status="valid" time="5.72"/></proof> <proof prover="0" timelimit="10"><result status="valid" time="7.41"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
...@@ -742,7 +744,7 @@ ...@@ -742,7 +744,7 @@
</goal> </goal>
<goal name="VC numof_or" expl="VC for numof_or" proved="true"> <goal name="VC numof_or" expl="VC for numof_or" proved="true">
<proof prover="0"><result status="valid" time="0.31"/></proof> <proof prover="0"><result status="valid" time="0.31"/></proof>
<proof prover="4"><result status="valid" time="0.45"/></proof> <proof prover="4"><result status="valid" time="0.60"/></proof>
<proof prover="5"><result status="valid" time="0.06"/></proof> <proof prover="5"><result status="valid" time="0.06"/></proof>
</goal> </goal>
<goal name="VC count_or" expl="VC for count_or" proved="true"> <goal name="VC count_or" expl="VC for count_or" proved="true">
...@@ -760,7 +762,7 @@ ...@@ -760,7 +762,7 @@
<proof prover="5"><result status="valid" time="0.04"/></proof> <proof prover="5"><result status="valid" time="0.04"/></proof>
</goal> </goal>
<goal name="VC count_or.3" expl="assertion" proved="true"> <goal name="VC count_or.3" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="2.02"/></proof> <proof prover="4"><result status="valid" time="2.59"/></proof>
</goal> </goal>
<goal name="VC count_or.4" expl="postcondition" proved="true"> <goal name="VC count_or.4" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.08"/></proof> <proof prover="0"><result status="valid" time="0.08"/></proof>
...@@ -810,10 +812,10 @@ ...@@ -810,10 +812,10 @@
</goal> </goal>
<goal name="VC ascii.5" expl="postcondition" proved="true"> <goal name="VC ascii.5" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.11"/></proof> <proof prover="0"><result status="valid" time="0.11"/></proof>
<proof prover="4"><result status="valid" time="1.58"/></proof> <proof prover="4"><result status="valid" time="1.91"/></proof>
</goal> </goal>
<goal name="VC ascii.6" expl="postcondition" proved="true"> <goal name="VC ascii.6" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.52"/></proof> <proof prover="4"><result status="valid" time="0.71"/></proof>
<proof prover="5"><result status="valid" time="0.06"/></proof> <proof prover="5"><result status="valid" time="0.06"/></proof>
<proof prover="6"><result status="valid" time="0.21" steps="374"/></proof> <proof prover="6"><result status="valid" time="0.21" steps="374"/></proof>
</goal> </goal>
...@@ -836,7 +838,7 @@ ...@@ -836,7 +838,7 @@
<proof prover="6"><result status="valid" time="0.02" steps="80"/></proof> <proof prover="6"><result status="valid" time="0.02" steps="80"/></proof>
</goal> </goal>
<goal name="VC tmp.2" expl="postcondition" proved="true"> <goal name="VC tmp.2" expl="postcondition" proved="true">
<proof prover="5"><result status="valid" time="0.66"/></proof> <proof prover="5"><result status="valid" time="0.87"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
......
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN" <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5"> <why3session shape_version="6">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/> <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"/> <prover id="4" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file proved="true"> <file proved="true">
......
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN" <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5"> <why3session shape_version="6">
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/> <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="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"/> <prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Coq" version="8.7.1" timelimit="30" steplimit="0" memlimit="1000"/> <prover id="4" name="Coq" version="8.7.1" timelimit="30" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="5" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../double.why" proved="true"> <file proved="true">
<path name=".."/>
<path name="double.why"/>
<theory name="TestDouble" proved="true"> <theory name="TestDouble" proved="true">
<goal name="nth_one1" proved="true"> <goal name="nth_one1" proved="true">
<proof prover="2" timelimit="3"><result status="valid" time="0.05" steps="79"/></proof> <proof prover="2" timelimit="3"><result status="valid" time="0.05" steps="79"/></proof>
...@@ -26,7 +28,7 @@ ...@@ -26,7 +28,7 @@
</goal> </goal>
<goal name="exp_one" proved="true"> <goal name="exp_one" proved="true">
<proof prover="2" timelimit="30"><result status="valid" time="0.16" steps="210"/></proof> <proof prover="2" timelimit="30"><result status="valid" time="0.16" steps="210"/></proof>
<proof prover="4" edited="double_TestDouble_exp_one_1.v"><result status="valid" time="0.52"/></proof> <proof prover="4" edited="double_TestDouble_exp_one_1.v"><result status="valid" time="1.23"/></proof>
</goal> </goal>
<goal name="mantissa_one" proved="true"> <goal name="mantissa_one" proved="true">
<proof prover="2"><result status="valid" time="0.09" steps="88"/></proof> <proof prover="2"><result status="valid" time="0.09" steps="88"/></proof>
......
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN" <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5"> <why3session shape_version="6">
<prover id="0" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="1000"/> <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="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"/> <prover id="3" name="Eprover" version="2.0" timelimit="1" steplimit="0" memlimit="1000"/>
...@@ -11,7 +11,9 @@ ...@@ -11,7 +11,9 @@
<prover id="8" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="8" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="10" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="10" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="11" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="11" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../double_of_int.why" proved="true"> <file proved="true">
<path name=".."/>
<path name="double_of_int.why"/>
<theory name="DoubleOfInt" proved="true"> <theory name="DoubleOfInt" proved="true">
<goal name="nth_j1" proved="true"> <goal name="nth_j1" proved="true">
<proof prover="10"><result status="valid" time="0.04" steps="80"/></proof> <proof prover="10"><result status="valid" time="0.04" steps="80"/></proof>
...@@ -60,7 +62,7 @@ ...@@ -60,7 +62,7 @@
<proof prover="10"><result status="valid" time="0.11" steps="101"/></proof> <proof prover="10"><result status="valid" time="0.11" steps="101"/></proof>
</goal> </goal>
<goal name="nth_const6" proved="true"> <goal name="nth_const6" proved="true">
<proof prover="4"><result status="valid" time="1.36"/></proof> <proof prover="4"><result status="valid" time="1.72"/></proof>
<proof prover="8"><result status="valid" time="0.79"/></proof> <proof prover="8"><result status="valid" time="0.79"/></proof>
<proof prover="10"><result status="valid" time="0.09" steps="101"/></proof> <proof prover="10"><result status="valid" time="0.09" steps="101"/></proof>
</goal> </goal>
...@@ -88,7 +90,7 @@ ...@@ -88,7 +90,7 @@
<proof prover="10"><result status="valid" time="0.03" steps="80"/></proof> <proof prover="10"><result status="valid" time="0.03" steps="80"/></proof>
</goal> </goal>
<goal name="exp_const" proved="true">