Commit 4e28b60c authored by Guillaume Melquiond's avatar Guillaume Melquiond

Update obsolete sessions.

parent 64d7fcb8
......@@ -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="5b1dd2e701903b8fba3c565ace8f367e" expanded="true">
<theory name="BinomialHeap" sum="1a8c8f52e3a5b2c123edd808bf508cd1" 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="ab759a44e440a5696e3be5d5c1002f13">
<theory name="Test_proofinuse" sum="3b40d0771ade481dca5e21ab1783e7b0">
<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="86110d7a411b6691bf6c2b80e6051309">
<theory name="FibonacciLogarithmic" sum="08625b1d5d1914cd59aef8c8eab6754c">
<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="c10df07cf9c0b00877454e7d2b02e8f5" expanded="true">
<theory name="Euler290" sum="6bdd74e0dcf213c8f4a8f4697c6635e6" 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="43519115242b2f2ec5062978bb1601e1" expanded="true">
<theory name="P" sum="58d29be40886499ae9897b7609f72f6b" 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">
......
......@@ -8,7 +8,7 @@
<prover id="6" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="7" name="Z3" version="4.3.2" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../verifythis_PrefixSumRec.mlw" expanded="true">
<theory name="PrefixSumRec" sum="c290986a5a94ad666d3e6cf1f064bcdd" expanded="true">
<theory name="PrefixSumRec" sum="dc9d2193d04034059a14474fc3bb5c44" expanded="true">
<goal name="Div_mod_2" expl="">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof>
......@@ -348,7 +348,7 @@
<proof prover="3" timelimit="30"><result status="valid" time="1.28"/></proof>
</goal>
<goal name="WP_parameter downsweep.18" expl="assertion">
<proof prover="0" timelimit="30"><result status="valid" time="7.83"/></proof>
<proof prover="0" timelimit="30"><result status="valid" time="4.92"/></proof>
<proof prover="1" timelimit="30"><result status="valid" time="3.47"/></proof>
</goal>
<goal name="WP_parameter downsweep.19" expl="variant decrease">
......@@ -459,7 +459,7 @@
<goal name="WP_parameter compute_sums.4" expl="assertion">
<proof prover="0"><result status="valid" time="0.28"/></proof>
<proof prover="1"><result status="valid" time="0.38"/></proof>
<proof prover="6"><result status="valid" time="0.61" steps="141"/></proof>
<proof prover="6"><result status="valid" time="0.61" steps="129"/></proof>
</goal>
<goal name="WP_parameter compute_sums.5" expl="index in array bounds">
<proof prover="0"><result status="valid" time="0.03"/></proof>
......
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