Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

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

fix obsolete sessions

parent 169819ed
......@@ -10,26 +10,26 @@
<prover id="5" name="Alt-Ergo" version="0.95.2" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="6" name="CVC4" version="1.3" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="7" name="Alt-Ergo" version="0.99.1" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../gcd.mlw">
<theory name="EuclideanAlgorithm">
<goal name="WP_parameter euclid" expl="VC for euclid">
<transf name="split_goal_wp">
<goal name="WP_parameter euclid.1" expl="postcondition">
<file name="../gcd.mlw" proved="true">
<theory name="EuclideanAlgorithm" proved="true">
<goal name="WP_parameter euclid" expl="VC for euclid" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter euclid.0" expl="postcondition" proved="true">
<proof prover="1" memlimit="0"><result status="valid" time="0.02"/></proof>
<proof prover="5" timelimit="2" memlimit="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="WP_parameter euclid.2" expl="check modulo by zero">
<goal name="WP_parameter euclid.1" expl="check modulo by zero" proved="true">
<proof prover="5" timelimit="5" memlimit="4000"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="WP_parameter euclid.3" expl="variant decrease">
<goal name="WP_parameter euclid.2" expl="variant decrease" proved="true">
<proof prover="1" timelimit="5"><result status="valid" time="0.02"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.03" steps="31"/></proof>
</goal>
<goal name="WP_parameter euclid.4" expl="precondition">
<goal name="WP_parameter euclid.3" expl="precondition" proved="true">
<proof prover="1" memlimit="0"><result status="valid" time="0.02"/></proof>
<proof prover="5" timelimit="10" memlimit="0"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
<goal name="WP_parameter euclid.5" expl="postcondition">
<goal name="WP_parameter euclid.4" expl="postcondition" proved="true">
<proof prover="0" timelimit="10" edited="gcd_WP_EuclideanAlgorithm_WP_parameter_gcd_1.v"><result status="valid" time="0.28"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="5" timelimit="10"><result status="valid" time="0.04" steps="13"/></proof>
......@@ -37,163 +37,163 @@
</transf>
</goal>
</theory>
<theory name="EuclideanAlgorithmIterative">
<goal name="WP_parameter euclid" expl="VC for euclid">
<transf name="split_goal_wp">
<goal name="WP_parameter euclid.1" expl="loop invariant init">
<theory name="EuclideanAlgorithmIterative" proved="true">
<goal name="WP_parameter euclid" expl="VC for euclid" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter euclid.0" expl="loop invariant init" proved="true">
<proof prover="5" timelimit="10"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="WP_parameter euclid.2" expl="check modulo by zero">
<goal name="WP_parameter euclid.1" expl="check modulo by zero" proved="true">
<proof prover="5" timelimit="5" memlimit="4000"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="WP_parameter euclid.3" expl="loop invariant preservation">
<goal name="WP_parameter euclid.2" expl="loop invariant preservation" proved="true">
<proof prover="5" timelimit="10"><result status="valid" time="0.06" steps="20"/></proof>
</goal>
<goal name="WP_parameter euclid.4" expl="loop invariant preservation">
<goal name="WP_parameter euclid.3" expl="loop invariant preservation" proved="true">
<proof prover="5" timelimit="10"><result status="valid" time="0.04" steps="13"/></proof>
</goal>
<goal name="WP_parameter euclid.5" expl="loop variant decrease">
<goal name="WP_parameter euclid.4" expl="loop variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3" timelimit="30"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter euclid.6" expl="postcondition">
<goal name="WP_parameter euclid.5" expl="postcondition" proved="true">
<proof prover="5" timelimit="10"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="BinaryGcd">
<goal name="even1" expl="">
<theory name="BinaryGcd" proved="true">
<goal name="even1" proved="true">
<proof prover="5"><result status="valid" time="0.06" steps="18"/></proof>
</goal>
<goal name="odd1" expl="">
<goal name="odd1" proved="true">
<proof prover="5"><result status="valid" time="0.06" steps="14"/></proof>
</goal>
<goal name="div_nonneg" expl="">
<goal name="div_nonneg" proved="true">
<proof prover="5"><result status="valid" time="0.02" steps="4"/></proof>
</goal>
<goal name="gcd_even_even" expl="">
<goal name="gcd_even_even" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="28"/></proof>
</goal>
<goal name="gcd_even_odd" expl="">
<goal name="gcd_even_odd" proved="true">
<proof prover="0" edited="gcd_BinaryGcd_gcd_even_odd_2.v"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="gcd_even_odd2" expl="">
<goal name="gcd_even_odd2" proved="true">
<proof prover="5"><result status="valid" time="0.17" steps="28"/></proof>
</goal>
<goal name="odd_odd_div2" expl="">
<goal name="odd_odd_div2" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter gcd_odd_odd" expl="VC for gcd_odd_odd">
<goal name="WP_parameter gcd_odd_odd" expl="VC for gcd_odd_odd" proved="true">
<proof prover="5" timelimit="5" memlimit="4000"><result status="valid" time="0.05" steps="31"/></proof>
</goal>
<goal name="gcd_odd_odd2" expl="">
<goal name="gcd_odd_odd2" proved="true">
<proof prover="5"><result status="valid" time="0.12" steps="24"/></proof>
</goal>
<goal name="WP_parameter binary_gcd" expl="VC for binary_gcd">
<transf name="split_goal_wp">
<goal name="WP_parameter binary_gcd.1" expl="variant decrease">
<goal name="WP_parameter binary_gcd" expl="VC for binary_gcd" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter binary_gcd.0" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="WP_parameter binary_gcd.2" expl="precondition">
<goal name="WP_parameter binary_gcd.1" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="WP_parameter binary_gcd.3" expl="postcondition">
<goal name="WP_parameter binary_gcd.2" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="6"/></proof>
</goal>
<goal name="WP_parameter binary_gcd.4" expl="postcondition">
<goal name="WP_parameter binary_gcd.3" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="14"/></proof>
</goal>
<goal name="WP_parameter binary_gcd.5" expl="check division by zero">
<goal name="WP_parameter binary_gcd.4" expl="check division by zero" proved="true">
<proof prover="5" timelimit="5" memlimit="4000"><result status="valid" time="0.02" steps="9"/></proof>
</goal>
<goal name="WP_parameter binary_gcd.6" expl="check division by zero">
<goal name="WP_parameter binary_gcd.5" expl="check division by zero" proved="true">
<proof prover="5" timelimit="5" memlimit="4000"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="WP_parameter binary_gcd.7" expl="variant decrease">
<goal name="WP_parameter binary_gcd.6" expl="variant decrease" proved="true">
<proof prover="5"><result status="valid" time="0.05" steps="24"/></proof>
</goal>
<goal name="WP_parameter binary_gcd.8" expl="precondition">
<goal name="WP_parameter binary_gcd.7" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="16"/></proof>
</goal>
<goal name="WP_parameter binary_gcd.9" expl="postcondition">
<goal name="WP_parameter binary_gcd.8" expl="postcondition" proved="true">
<proof prover="1" timelimit="6"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="WP_parameter binary_gcd.10" expl="check division by zero">
<goal name="WP_parameter binary_gcd.9" expl="check division by zero" proved="true">
<proof prover="5" timelimit="5" memlimit="4000"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="WP_parameter binary_gcd.11" expl="variant decrease">
<goal name="WP_parameter binary_gcd.10" expl="variant decrease" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="20"/></proof>
</goal>
<goal name="WP_parameter binary_gcd.12" expl="precondition">
<goal name="WP_parameter binary_gcd.11" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="14"/></proof>
</goal>
<goal name="WP_parameter binary_gcd.13" expl="postcondition">
<goal name="WP_parameter binary_gcd.12" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.23"/></proof>
<proof prover="6"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter binary_gcd.14" expl="check division by zero">
<goal name="WP_parameter binary_gcd.13" expl="check division by zero" proved="true">
<proof prover="5" timelimit="5" memlimit="4000"><result status="valid" time="0.02" steps="9"/></proof>
</goal>
<goal name="WP_parameter binary_gcd.15" expl="variant decrease">
<goal name="WP_parameter binary_gcd.14" expl="variant decrease" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="19"/></proof>
</goal>
<goal name="WP_parameter binary_gcd.16" expl="precondition">
<goal name="WP_parameter binary_gcd.15" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter binary_gcd.17" expl="postcondition">
<goal name="WP_parameter binary_gcd.16" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.24"/></proof>
<proof prover="6"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="WP_parameter binary_gcd.18" expl="check division by zero">
<goal name="WP_parameter binary_gcd.17" expl="check division by zero" proved="true">
<proof prover="5" timelimit="5" memlimit="4000"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="WP_parameter binary_gcd.19" expl="variant decrease">
<goal name="WP_parameter binary_gcd.18" expl="variant decrease" proved="true">
<proof prover="5"><result status="valid" time="0.08" steps="35"/></proof>
<proof prover="6"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="WP_parameter binary_gcd.20" expl="precondition">
<goal name="WP_parameter binary_gcd.19" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="3.49"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="13"/></proof>
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter binary_gcd.21" expl="postcondition">
<goal name="WP_parameter binary_gcd.20" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.34"/></proof>
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="EuclideanAlgorithm31">
<goal name="WP_parameter euclid" expl="VC for euclid">
<transf name="split_goal_wp">
<goal name="WP_parameter euclid.1" expl="integer overflow">
<theory name="EuclideanAlgorithm31" proved="true">
<goal name="WP_parameter euclid" expl="VC for euclid" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter euclid.0" expl="integer overflow" proved="true">
<proof prover="5" timelimit="5" memlimit="4000"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="WP_parameter euclid.2" expl="postcondition">
<goal name="WP_parameter euclid.1" expl="postcondition" proved="true">
<proof prover="7"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter euclid.3" expl="division by zero">
<goal name="WP_parameter euclid.2" expl="division by zero" proved="true">
<proof prover="7"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="WP_parameter euclid.4" expl="integer overflow">
<goal name="WP_parameter euclid.3" expl="integer overflow" proved="true">
<proof prover="7"><result status="valid" time="0.07" steps="50"/></proof>
</goal>
<goal name="WP_parameter euclid.5" expl="variant decrease">
<goal name="WP_parameter euclid.4" expl="variant decrease" proved="true">
<proof prover="7"><result status="valid" time="0.50" steps="169"/></proof>
</goal>
<goal name="WP_parameter euclid.6" expl="precondition">
<goal name="WP_parameter euclid.5" expl="precondition" proved="true">
<proof prover="7"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="WP_parameter euclid.7" expl="postcondition">
<goal name="WP_parameter euclid.6" expl="postcondition" proved="true">
<proof prover="7"><result status="valid" time="0.11" steps="41"/></proof>
</goal>
</transf>
......
......@@ -181,7 +181,7 @@
<proof prover="3"><result status="valid" time="0.29"/></proof>
</goal>
<goal name="WP_parameter t.21.1" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="5.80"/></proof>
<proof prover="3"><result status="valid" time="5.10"/></proof>
</goal>
</transf>
</goal>
......
......@@ -7,140 +7,140 @@
<prover id="2" name="Z3" version="4.3.2" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="3.2" timelimit="8" steplimit="0" memlimit="1000"/>
<prover id="6" name="Alt-Ergo" version="0.99.1" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../vstte10_queens.mlw">
<theory name="NQueens">
<goal name="eq_board_set" expl="">
<file name="../vstte10_queens.mlw" proved="true">
<theory name="NQueens" proved="true">
<goal name="eq_board_set" proved="true">
<proof prover="6" timelimit="5"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="eq_board_sym" expl="">
<goal name="eq_board_sym" proved="true">
<proof prover="6" timelimit="20" memlimit="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="eq_board_trans" expl="">
<goal name="eq_board_trans" proved="true">
<proof prover="6" timelimit="20" memlimit="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="eq_board_extension" expl="">
<goal name="eq_board_extension" proved="true">
<proof prover="6" timelimit="20" memlimit="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="consistent_row_eq" expl="">
<goal name="consistent_row_eq" proved="true">
<proof prover="6" timelimit="20" memlimit="0"><result status="valid" time="0.06" steps="37"/></proof>
</goal>
<goal name="WP_parameter check_is_consistent" expl="VC for check_is_consistent">
<goal name="WP_parameter check_is_consistent" expl="VC for check_is_consistent" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="solution_eq_board" expl="">
<goal name="solution_eq_board" proved="true">
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter bt_queens" expl="VC for bt_queens">
<goal name="WP_parameter bt_queens" expl="VC for bt_queens" proved="true">
<proof prover="1"><result status="valid" time="1.42"/></proof>
</goal>
<goal name="WP_parameter queens" expl="VC for queens">
<goal name="WP_parameter queens" expl="VC for queens" proved="true">
<proof prover="6" timelimit="20" memlimit="0"><result status="valid" time="0.02" steps="25"/></proof>
</goal>
<goal name="WP_parameter test8" expl="VC for test8">
<goal name="WP_parameter test8" expl="VC for test8" proved="true">
<proof prover="6" timelimit="5"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens" expl="VC for count_bt_queens">
<goal name="WP_parameter count_bt_queens" expl="VC for count_bt_queens" proved="true">
<proof prover="0" timelimit="5" memlimit="4000"><result status="valid" time="0.27"/></proof>
</goal>
<goal name="WP_parameter count_queens" expl="VC for count_queens">
<goal name="WP_parameter count_queens" expl="VC for count_queens" proved="true">
<proof prover="6"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter test_count_8" expl="VC for test_count_8">
<goal name="WP_parameter test_count_8" expl="VC for test_count_8" proved="true">
<proof prover="6"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
</theory>
<theory name="NQueens63">
<goal name="WP_parameter check_is_consistent" expl="VC for check_is_consistent">
<theory name="NQueens63" proved="true">
<goal name="WP_parameter check_is_consistent" expl="VC for check_is_consistent" proved="true">
<proof prover="0"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens" expl="VC for count_bt_queens">
<transf name="split_goal_wp">
<goal name="WP_parameter count_bt_queens.1" expl="postcondition">
<goal name="WP_parameter count_bt_queens" expl="VC for count_bt_queens" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter count_bt_queens.0" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.02" steps="9"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.2" expl="integer overflow">
<goal name="WP_parameter count_bt_queens.1" expl="integer overflow" proved="true">
<proof prover="6"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.3" expl="loop invariant init">
<goal name="WP_parameter count_bt_queens.2" expl="loop invariant init" proved="true">
<proof prover="6"><result status="valid" time="0.02" steps="9"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.4" expl="loop invariant init">
<goal name="WP_parameter count_bt_queens.3" expl="loop invariant init" proved="true">
<proof prover="6"><result status="valid" time="0.02" steps="9"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.5" expl="type invariant">
<goal name="WP_parameter count_bt_queens.4" expl="type invariant" proved="true">
<proof prover="6"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.6" expl="index in array63 bounds">
<goal name="WP_parameter count_bt_queens.5" expl="index in array63 bounds" proved="true">
<proof prover="6"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.7" expl="precondition">
<goal name="WP_parameter count_bt_queens.6" expl="precondition" proved="true">
<proof prover="6"><result status="valid" time="0.02" steps="16"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.8" expl="precondition">
<goal name="WP_parameter count_bt_queens.7" expl="precondition" proved="true">
<proof prover="6"><result status="valid" time="0.17" steps="115"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.9" expl="integer overflow">
<goal name="WP_parameter count_bt_queens.8" expl="integer overflow" proved="true">
<proof prover="6"><result status="valid" time="0.02" steps="21"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.10" expl="integer overflow">
<goal name="WP_parameter count_bt_queens.9" expl="integer overflow" proved="true">
<proof prover="6"><result status="valid" time="0.04" steps="48"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.11" expl="variant decrease">
<goal name="WP_parameter count_bt_queens.10" expl="variant decrease" proved="true">
<proof prover="6"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.12" expl="precondition">
<goal name="WP_parameter count_bt_queens.11" expl="precondition" proved="true">
<proof prover="6"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.13" expl="precondition">
<goal name="WP_parameter count_bt_queens.12" expl="precondition" proved="true">
<proof prover="6"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.14" expl="precondition">
<goal name="WP_parameter count_bt_queens.13" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.05"/></proof>
<proof prover="6"><result status="valid" time="0.00" steps="22"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.15" expl="integer overflow">
<goal name="WP_parameter count_bt_queens.14" expl="integer overflow" proved="true">
<proof prover="6"><result status="valid" time="0.02" steps="26"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.16" expl="integer overflow">
<goal name="WP_parameter count_bt_queens.15" expl="integer overflow" proved="true">
<proof prover="6"><result status="valid" time="0.13" steps="62"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.17" expl="loop invariant preservation">
<goal name="WP_parameter count_bt_queens.16" expl="loop invariant preservation" proved="true">
<proof prover="6"><result status="valid" time="0.02" steps="30"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.18" expl="loop invariant preservation">
<goal name="WP_parameter count_bt_queens.17" expl="loop invariant preservation" proved="true">
<proof prover="6"><result status="valid" time="0.02" steps="58"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.19" expl="loop variant decrease">
<goal name="WP_parameter count_bt_queens.18" expl="loop variant decrease" proved="true">
<proof prover="6"><result status="valid" time="0.02" steps="30"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.20" expl="integer overflow">
<goal name="WP_parameter count_bt_queens.19" expl="integer overflow" proved="true">
<proof prover="6"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.21" expl="integer overflow">
<goal name="WP_parameter count_bt_queens.20" expl="integer overflow" proved="true">
<proof prover="6"><result status="valid" time="0.02" steps="48"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.22" expl="loop invariant preservation">
<goal name="WP_parameter count_bt_queens.21" expl="loop invariant preservation" proved="true">
<proof prover="6"><result status="valid" time="0.02" steps="23"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.23" expl="loop invariant preservation">
<goal name="WP_parameter count_bt_queens.22" expl="loop invariant preservation" proved="true">
<proof prover="6"><result status="valid" time="0.11" steps="46"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.24" expl="loop variant decrease">
<goal name="WP_parameter count_bt_queens.23" expl="loop variant decrease" proved="true">
<proof prover="6"><result status="valid" time="0.02" steps="23"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.25" expl="type invariant">
<goal name="WP_parameter count_bt_queens.24" expl="type invariant" proved="true">
<proof prover="0"><result status="valid" time="0.05"/></proof>
<proof prover="6"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.26" expl="postcondition">
<goal name="WP_parameter count_bt_queens.25" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter count_queens" expl="VC for count_queens">
<goal name="WP_parameter count_queens" expl="VC for count_queens" proved="true">
<proof prover="6"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter test_count_8" expl="VC for test_count_8">
<goal name="WP_parameter test_count_8" expl="VC for test_count_8" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
......
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