Commit a679c796 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

updated sessions

parent d30ae586
This diff is collapsed.
This diff is collapsed.
......@@ -4,53 +4,45 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="2" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="4" name="Z3" version="4.4.0" timelimit="5" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.4" alternative="noBV" timelimit="5" memlimit="1000"/>
<file name="../hackers-delight.mlw" expanded="true">
<theory name="Utils" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Utils_Spec" sum="48173d335d17e665b5bf6ed0b7333c02" expanded="true">
<theory name="Utils_Spec" sum="a29d5df9ccd8df5209597453ff480d53" expanded="true">
<goal name="countZero">
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="numOfZero">
<proof prover="0"><result status="valid" time="0.47" steps="239"/></proof>
<proof prover="3"><result status="valid" time="0.18"/></proof>
<proof prover="0"><result status="valid" time="0.47" steps="241"/></proof>
</goal>
<goal name="countStep">
<proof prover="1" timelimit="30"><result status="valid" time="4.95"/></proof>
<proof prover="1"><result status="valid" time="4.95"/></proof>
</goal>
<goal name="WP_parameter numof_shift" expl="VC for numof_shift">
<proof prover="1"><result status="valid" time="0.24"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux" expl="VC for countSpec_Aux">
<transf name="split_goal_wp">
<goal name="WP_parameter countSpec_Aux.1" expl="1. postcondition">
<proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.07"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="76"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.2" expl="2. variant decrease">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.66"/></proof>
<proof prover="0"><result status="valid" time="0.65" steps="282"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.3" expl="3. assertion">
<transf name="split_goal_wp">
<goal name="WP_parameter countSpec_Aux.3.1" expl="1. assertion">
<proof prover="3"><result status="valid" time="0.84"/></proof>
<proof prover="0"><result status="valid" time="0.22" steps="150"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.3.2" expl="2. assertion">
<proof prover="3"><result status="valid" time="0.27"/></proof>
<proof prover="0"><result status="valid" time="2.60" steps="535"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.3.3" expl="3. assertion">
<proof prover="0"><result status="valid" time="0.51" steps="158"/></proof>
<proof prover="0"><result status="valid" time="0.51" steps="162"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.3.4" expl="4. assertion">
<proof prover="3" timelimit="15"><result status="valid" time="3.83"/></proof>
<proof prover="5"><result status="valid" time="2.23"/></proof>
</goal>
</transf>
</goal>
......@@ -61,58 +53,46 @@
</goal>
<goal name="countSpec">
<proof prover="0"><result status="valid" time="0.05" steps="74"/></proof>
<proof prover="1"><result status="valid" time="0.10"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter hamming_spec" expl="VC for hamming_spec">
<transf name="split_goal_wp">
<goal name="WP_parameter hamming_spec.1" expl="1. assertion">
<proof prover="0"><result status="valid" time="2.43" steps="956"/></proof>
<proof prover="3"><result status="valid" time="0.06"/></proof>
<proof prover="5"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter hamming_spec.2" expl="2. postcondition">
<proof prover="2"><result status="valid" time="0.14"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="symmetric">
<proof prover="1"><result status="valid" time="0.11"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="separation">
<proof prover="1"><result status="valid" time="0.19"/></proof>
<proof prover="2"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="WP_parameter numof_or" expl="VC for numof_or">
<proof prover="1"><result status="valid" time="0.53"/></proof>
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="WP_parameter triangleInequalityInt" expl="VC for triangleInequalityInt">
<transf name="split_goal_wp">
<goal name="WP_parameter triangleInequalityInt.1" expl="1. assertion">
<proof prover="2" timelimit="70"><result status="valid" time="1.34"/></proof>
<proof prover="4"><result status="valid" time="2.26"/></proof>
</goal>
<goal name="WP_parameter triangleInequalityInt.2" expl="2. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="79"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.09"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="78"/></proof>
</goal>
</transf>
</goal>
<goal name="triangleInequality">
<proof prover="1" timelimit="15"><result status="valid" time="2.35"/></proof>
<proof prover="0"><result status="valid" time="4.65" steps="726"/></proof>
</goal>
</theory>
<theory name="Hackers_delight" sum="144a5949c45c6cffa10ffc47afc51177" expanded="true">
<theory name="Hackers_delight" sum="d473e832977fd6e285755f138e96283d" expanded="true">
<goal name="WP_parameter ascii" expl="VC for ascii">
<proof prover="1"><result status="valid" time="0.09"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="asciiProp">
<proof prover="1" timelimit="20"><result status="valid" time="0.66"/></proof>
<proof prover="2" timelimit="20"><result status="valid" time="1.69"/></proof>
<proof prover="1"><result status="valid" time="0.66"/></proof>
</goal>
<goal name="iso">
<proof prover="1"><result status="valid" time="0.43"/></proof>
......@@ -121,30 +101,25 @@
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="nthGray">
<proof prover="1"><result status="valid" time="0.05"/></proof>
<proof prover="3"><result status="valid" time="1.46"/></proof>
<proof prover="0"><result status="valid" time="1.25" steps="544"/></proof>
</goal>
<goal name="lastNthGray">
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="1.27"/></proof>
</goal>
<goal name="nthBinary">
<proof prover="1" timelimit="30"><result status="valid" time="0.22"/></proof>
<proof prover="1"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="evenOdd">
<proof prover="1"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="DM1">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="DM2">
<proof prover="1"><result status="valid" time="0.05"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="DM3">
<proof prover="1"><result status="valid" time="0.07"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="DM4">
<proof prover="1"><result status="valid" time="0.11"/></proof>
......@@ -163,33 +138,24 @@
</goal>
<goal name="DMtest">
<proof prover="1"><result status="valid" time="0.07"/></proof>
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="Aa">
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Ac">
<proof prover="1"><result status="valid" time="0.07"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="0"><result status="valid" time="0.49" steps="319"/></proof>
</goal>
<goal name="Ad">
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Ae">
<proof prover="0"><result status="valid" time="0.05" steps="72"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.08"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="71"/></proof>
</goal>
<goal name="Af">
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="Aj">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="An">
<proof prover="1"><result status="valid" time="0.12"/></proof>
......@@ -199,7 +165,6 @@
</goal>
<goal name="Aq">
<proof prover="1"><result status="valid" time="0.08"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="At">
<proof prover="1"><result status="valid" time="0.12"/></proof>
......@@ -209,7 +174,6 @@
</goal>
<goal name="Av">
<proof prover="1"><result status="valid" time="0.12"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="IE1">
<proof prover="1"><result status="valid" time="0.02"/></proof>
......@@ -234,11 +198,9 @@
</goal>
<goal name="RS_left">
<proof prover="1"><result status="valid" time="0.11"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="RS_right">
<proof prover="1"><result status="valid" time="0.09"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="BP">
<proof prover="1"><result status="valid" time="0.10"/></proof>
......
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