Commit bd9e99e3 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Merge branch 'bugfix/v0.88' into next

parents 0d579596 4e28b60c
......@@ -6,7 +6,7 @@
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="2" name="Eprover" version="1.8-001" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../binomial_heap.mlw" expanded="true">
<theory name="BinomialHeap" sum="8d64901bf73863fd85973498d6d63561" expanded="true">
<theory name="BinomialHeap" sum="e529b5f86b07a70c7e69f057b8c23d32" expanded="true">
<goal name="WP_parameter size_nonnneg" expl="VC for size_nonnneg">
<proof prover="0"><result status="valid" time="0.09"/></proof>
</goal>
......
......@@ -6,7 +6,7 @@
<prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../bitvector_examples.mlw" expanded="true">
<theory name="Test_proofinuse" sum="0005f9b0b6dd327d79b9311dcc38bc63">
<theory name="Test_proofinuse" sum="3cc2de54971d83964e2af7c5db544676">
<goal name="WP_parameter shift_is_div" expl="VC for shift_is_div">
<transf name="split_goal_wp">
<goal name="WP_parameter shift_is_div.1" expl="assertion">
......
......@@ -5,7 +5,7 @@
<prover id="0" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../braun_trees.mlw" expanded="true">
<theory name="BraunHeaps" sum="e88a215097d30ab497fc4242af794eb6" expanded="true">
<theory name="BraunHeaps" sum="01ce4495e1108eea8a986b97a904ef17" expanded="true">
<goal name="WP_parameter root_is_min" expl="VC for root_is_min">
<proof prover="0"><result status="valid" time="0.10"/></proof>
</goal>
......@@ -385,7 +385,7 @@
<proof prover="2"><result status="valid" time="0.02" steps="30"/></proof>
</goal>
<goal name="WP_parameter inv_height.6" expl="variant decrease">
<proof prover="2"><result status="valid" time="0.00" steps="38"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="37"/></proof>
</goal>
<goal name="WP_parameter inv_height.7" expl="precondition">
<proof prover="2"><result status="valid" time="0.02" steps="29"/></proof>
......
......@@ -106,7 +106,7 @@
<proof prover="14"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
<theory name="PowerIntTest" sum="cd11768ecfe24cfa9c0b61d85ea97e9c" expanded="true">
<theory name="PowerIntTest" sum="f226939a990c795aae51223e358ddf04" expanded="true">
<goal name="Pow_2_2" expl="" expanded="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.01"/></proof>
......
......@@ -442,7 +442,7 @@
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
</theory>
<theory name="FibonacciLogarithmic" sum="ad390afd20cc0d933ea9d8a3fcfae903">
<theory name="FibonacciLogarithmic" sum="08180c1ec2645e883aa224eeab1abe8a">
<goal name="WP_parameter logfib" expl="VC for logfib">
<transf name="split_goal_wp">
<goal name="WP_parameter logfib.1" expl="postcondition">
......
......@@ -2,67 +2,65 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.01" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="3" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="6" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="7" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../power.mlw" expanded="true">
<theory name="FastExponentiation" sum="372e3fedff8ee241c0b52de2f675ae3a" expanded="true">
<goal name="WP_parameter fast_exp" expl="VC for fast_exp" expanded="true">
<proof prover="4" timelimit="3"><result status="valid" time="0.57" steps="55"/></proof>
<theory name="FastExponentiation" sum="b571612c8c075ebc18bdee600ab0d856" expanded="true">
<goal name="WP_parameter fast_exp" expl="VC for fast_exp">
<proof prover="2"><result status="valid" time="0.13" steps="44"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative" expl="VC for fast_exp_imperative" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter fast_exp_imperative.1" expl="loop invariant init" expanded="true">
<proof prover="1" timelimit="10"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00" steps="1"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<goal name="WP_parameter fast_exp_imperative.1" expl="loop invariant init">
<proof prover="2"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.2" expl="assertion" expanded="true">
<proof prover="0"><result status="valid" time="0.19" steps="14"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<goal name="WP_parameter fast_exp_imperative.2" expl="assertion">
<proof prover="7"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.3" expl="loop invariant preservation" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter fast_exp_imperative.3.1" expl="VC for fast_exp_imperative" expanded="true">
<proof prover="4" timelimit="10" memlimit="1000"><result status="valid" time="0.13" steps="13"/></proof>
<goal name="WP_parameter fast_exp_imperative.3" expl="loop invariant preservation">
<transf name="split_goal_wp">
<goal name="WP_parameter fast_exp_imperative.3.1" expl="VC for fast_exp_imperative">
<proof prover="2"><result status="valid" time="0.04" steps="11"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="7"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.3.2" expl="VC for fast_exp_imperative" expanded="true">
<proof prover="0"><result status="valid" time="0.80" steps="19"/></proof>
<goal name="WP_parameter fast_exp_imperative.3.2" expl="VC for fast_exp_imperative">
<proof prover="2"><result status="valid" time="0.50" steps="20"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter fast_exp_imperative.4" expl="loop variant decrease" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="4" timelimit="10"><result status="valid" time="0.09" steps="13"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
<goal name="WP_parameter fast_exp_imperative.4" expl="loop variant decrease">
<proof prover="2"><result status="valid" time="0.56" steps="11"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="7"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.5" expl="assertion">
<proof prover="0"><result status="valid" time="0.10" steps="21"/></proof>
<proof prover="7"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.6" expl="loop invariant preservation" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter fast_exp_imperative.6.1" expl="VC for fast_exp_imperative" expanded="true">
<proof prover="0"><result status="valid" time="0.08" steps="16"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="16"/></proof>
<proof prover="6"><result status="valid" time="0.02"/></proof>
<goal name="WP_parameter fast_exp_imperative.6" expl="loop invariant preservation">
<transf name="split_goal_wp">
<goal name="WP_parameter fast_exp_imperative.6.1" expl="VC for fast_exp_imperative">
<proof prover="2"><result status="valid" time="0.02" steps="17"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="7"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.6.2" expl="VC for fast_exp_imperative" expanded="true">
<proof prover="0"><result status="valid" time="1.81" steps="25"/></proof>
<goal name="WP_parameter fast_exp_imperative.6.2" expl="VC for fast_exp_imperative">
<proof prover="2"><result status="valid" time="0.49" steps="24"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter fast_exp_imperative.7" expl="loop variant decrease" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="4" timelimit="10"><result status="valid" time="1.15" steps="21"/></proof>
<proof prover="6"><result status="valid" time="0.02"/></proof>
<goal name="WP_parameter fast_exp_imperative.7" expl="loop variant decrease">
<proof prover="2"><result status="valid" time="0.29" steps="22"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="7"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.8" expl="postcondition" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter fast_exp_imperative.8.1" expl="postcondition" expanded="true">
<proof prover="4"><result status="valid" time="0.01" steps="5"/></proof>
<goal name="WP_parameter fast_exp_imperative.8" expl="postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter fast_exp_imperative.8.1" expl="postcondition">
<proof prover="2"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
</transf>
</goal>
......
......@@ -7,7 +7,7 @@
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../sum_of_digits.mlw" expanded="true">
<theory name="Euler290" sum="983835c6b3afb74dc6896a5de1ee7386" expanded="true">
<theory name="Euler290" sum="509e8c131cb9b5f422e46305bcec67e2" expanded="true">
<goal name="Base" expl="">
<proof prover="4" timelimit="10"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="1" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../coq-interval.why" expanded="true">
<theory name="P" sum="72361b88738cd9a546e50ed08ba8c423" expanded="true">
<theory name="P" sum="1e4fe85b7d4e5d74721c865ee586cec8" expanded="true">
<goal name="pow_eps2_max_int" expl="" expanded="true">
<proof prover="1" edited="coqmninterval_P_pow_eps2_max_int_1.v"><result status="valid" time="1.21"/></proof>
</goal>
......
......@@ -4,8 +4,9 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../tree_of_array.mlw" expanded="true">
<theory name="TreeOfArray" sum="e6cc07771b58c81603582477098238ac" expanded="true">
<theory name="TreeOfArray" sum="415ae15d24148530a5b2281791ece1b0" expanded="true">
<goal name="WP_parameter tree_of_array_aux" expl="VC for tree_of_array_aux" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter tree_of_array_aux.1" expl="postcondition">
......@@ -26,16 +27,16 @@
<goal name="WP_parameter tree_of_array_aux.6" expl="index in array bounds">
<proof prover="0"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter tree_of_array_aux.7" expl="postcondition" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter tree_of_array_aux.7" expl="postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter tree_of_array_aux.7.1" expl="postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="WP_parameter tree_of_array_aux.7.2" expl="postcondition">
<proof prover="0"><result status="valid" time="0.17" steps="274"/></proof>
<proof prover="0"><result status="valid" time="0.17" steps="270"/></proof>
</goal>
<goal name="WP_parameter tree_of_array_aux.7.3" expl="postcondition">
<proof prover="0"><result status="valid" time="2.41" steps="1188"/></proof>
<proof prover="2"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="WP_parameter tree_of_array_aux.7.4" expl="postcondition">
<proof prover="1"><result status="valid" time="0.13"/></proof>
......@@ -44,7 +45,7 @@
</goal>
</transf>
</goal>
<goal name="WP_parameter tree_of_array" expl="VC for tree_of_array" expanded="true">
<goal name="WP_parameter tree_of_array" expl="VC for tree_of_array">
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
</theory>
......
......@@ -5,7 +5,7 @@
<prover id="0" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../tree_of_list.mlw">
<theory name="TreeOfList" sum="12d1a0ff628823b4f6f62c68ba956168">
<theory name="TreeOfList" sum="3f48d5a018203de070ba283a1f39f87a">
<goal name="WP_parameter tree_of_list_aux" expl="VC for tree_of_list_aux">
<transf name="split_goal_wp">
<goal name="WP_parameter tree_of_list_aux.1" expl="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