Commit 7054c4ca authored by MARCHE Claude's avatar MARCHE Claude

update obsolete sessions

parent 8618deeb
......@@ -22,87 +22,87 @@
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
</theory>
<theory name="BinarySearchInt32" sum="3bccc1a191f702802bbee521528e559c" expanded="true">
<theory name="BinarySearchInt32" sum="2089995b9d71a591dc8d378af11dce53" expanded="true">
<goal name="WP_parameter binary_search" expl="VC for binary_search" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter binary_search.1" expl="1. integer overflow">
<proof prover="3"><result status="valid" time="0.02" steps="5"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="70"/></proof>
</goal>
<goal name="WP_parameter binary_search.2" expl="2. integer overflow">
<proof prover="3"><result status="valid" time="0.01" steps="7"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="72"/></proof>
</goal>
<goal name="WP_parameter binary_search.3" expl="3. integer overflow">
<proof prover="3"><result status="valid" time="0.01" steps="25"/></proof>
<proof prover="3"><result status="valid" time="0.12" steps="88"/></proof>
</goal>
<goal name="WP_parameter binary_search.4" expl="4. loop invariant init">
<proof prover="3"><result status="valid" time="0.01" steps="10"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="75"/></proof>
</goal>
<goal name="WP_parameter binary_search.5" expl="5. loop invariant init">
<proof prover="3"><result status="valid" time="0.01" steps="13"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="78"/></proof>
</goal>
<goal name="WP_parameter binary_search.6" expl="6. integer overflow">
<proof prover="3"><result status="valid" time="0.02" steps="15"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="80"/></proof>
</goal>
<goal name="WP_parameter binary_search.7" expl="7. integer overflow">
<proof prover="3"><result status="valid" time="0.02" steps="21"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="86"/></proof>
</goal>
<goal name="WP_parameter binary_search.8" expl="8. division by zero">
<proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="83"/></proof>
</goal>
<goal name="WP_parameter binary_search.9" expl="9. integer overflow">
<proof prover="3"><result status="valid" time="0.04" steps="34"/></proof>
<proof prover="3"><result status="valid" time="0.04" steps="99"/></proof>
</goal>
<goal name="WP_parameter binary_search.10" expl="10. integer overflow">
<proof prover="3"><result status="valid" time="0.52" steps="51"/></proof>
<proof prover="3"><result status="valid" time="0.52" steps="114"/></proof>
</goal>
<goal name="WP_parameter binary_search.11" expl="11. assertion">
<proof prover="3"><result status="valid" time="0.91" steps="72"/></proof>
<proof prover="3"><result status="valid" time="1.48" steps="133"/></proof>
</goal>
<goal name="WP_parameter binary_search.12" expl="12. index in array bounds">
<proof prover="3"><result status="valid" time="0.01" steps="25"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="90"/></proof>
</goal>
<goal name="WP_parameter binary_search.13" expl="13. integer overflow">
<proof prover="3"><result status="valid" time="0.01" steps="29"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="94"/></proof>
</goal>
<goal name="WP_parameter binary_search.14" expl="14. integer overflow">
<proof prover="3"><result status="valid" time="0.03" steps="46"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="111"/></proof>
</goal>
<goal name="WP_parameter binary_search.15" expl="15. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.02" steps="33"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="98"/></proof>
</goal>
<goal name="WP_parameter binary_search.16" expl="16. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="6.24" steps="115"/></proof>
<proof prover="3"><result status="valid" time="8.76" steps="176"/></proof>
</goal>
<goal name="WP_parameter binary_search.17" expl="17. loop variant decrease">
<proof prover="3"><result status="valid" time="0.02" steps="33"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="98"/></proof>
</goal>
<goal name="WP_parameter binary_search.18" expl="18. index in array bounds">
<proof prover="3"><result status="valid" time="0.01" steps="29"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="94"/></proof>
</goal>
<goal name="WP_parameter binary_search.19" expl="19. integer overflow">
<proof prover="3"><result status="valid" time="0.01" steps="31"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="96"/></proof>
</goal>
<goal name="WP_parameter binary_search.20" expl="20. integer overflow">
<proof prover="3"><result status="valid" time="0.02" steps="35"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="100"/></proof>
</goal>
<goal name="WP_parameter binary_search.21" expl="21. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.02" steps="35"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="100"/></proof>
</goal>
<goal name="WP_parameter binary_search.22" expl="22. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3" timelimit="60"><result status="valid" time="9.69" steps="116"/></proof>
<proof prover="3" timelimit="60"><result status="valid" time="14.15" steps="177"/></proof>
</goal>
<goal name="WP_parameter binary_search.23" expl="23. loop variant decrease">
<proof prover="3"><result status="valid" time="0.02" steps="35"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="100"/></proof>
</goal>
<goal name="WP_parameter binary_search.24" expl="24. postcondition">
<proof prover="3"><result status="valid" time="1.22" steps="63"/></proof>
<proof prover="3"><result status="valid" time="2.32" steps="126"/></proof>
</goal>
<goal name="WP_parameter binary_search.25" expl="25. exceptional postcondition">
<proof prover="3"><result status="valid" time="0.01" steps="24"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="89"/></proof>
</goal>
</transf>
</goal>
......
This diff is collapsed.
......@@ -17,7 +17,7 @@
<file name="../real.why" expanded="true">
<theory name="Test" sum="cf206e9b789e3b16bbeee98ff5359bb7" expanded="true">
<goal name="G1" expanded="true">
<proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.01" steps="0"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
......@@ -26,7 +26,7 @@
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="G2" expanded="true">
<proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.01" steps="0"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
......@@ -34,7 +34,7 @@
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="G3" expanded="true">
<proof prover="1" memlimit="0"><result status="valid" time="0.00"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
......@@ -43,7 +43,7 @@
</theory>
<theory name="TestInfix" sum="9929e0fb7685505424762277d915662a" expanded="true">
<goal name="Add" expanded="true">
<proof prover="1" memlimit="0"><result status="valid" time="0.00"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
......@@ -51,7 +51,7 @@
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Sub" expanded="true">
<proof prover="1" memlimit="0"><result status="valid" time="0.00"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
......@@ -59,7 +59,7 @@
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Neg" expanded="true">
<proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.01" steps="0"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
......@@ -67,7 +67,7 @@
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Mul" expanded="true">
<proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.01" steps="0"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
......@@ -75,7 +75,7 @@
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Div" expanded="true">
<proof prover="1" memlimit="0"><result status="valid" time="0.00"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
......@@ -83,7 +83,7 @@
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Inv" expanded="true">
<proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.01" steps="0"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
......@@ -92,7 +92,7 @@
</theory>
<theory name="SquareTest" sum="b399f090ec659c1b880d355f5452fbc9" expanded="true">
<goal name="Sqrt_zero" expanded="true">
<proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.01" steps="3"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4" timelimit="60"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
......@@ -100,7 +100,7 @@
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Sqrt_one" expanded="true">
<proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
......@@ -108,17 +108,17 @@
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Sqrt_four" expanded="true">
<proof prover="1" timelimit="5"><result status="valid" time="0.00"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.00" steps="8"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="valid" time="1.27"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="8" timelimit="67"><result status="valid" time="32.60"/></proof>
<proof prover="8" timelimit="67"><result status="valid" time="26.09"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
</theory>
<theory name="ExpLogTest" sum="b87cf6a8ae7e92621e77bacb7a1fd605" expanded="true">
<goal name="Log_e" expanded="true">
<proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.01" steps="3"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
......@@ -127,7 +127,7 @@
</theory>
<theory name="PowerIntTest" sum="a44ed7f266568491fd1a5efcfad78047" expanded="true">
<goal name="Pow_2_2" expanded="true">
<proof prover="1" timelimit="60"><result status="valid" time="0.02"/></proof>
<proof prover="1" timelimit="60"><result status="valid" time="0.02" steps="6"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
......@@ -135,23 +135,23 @@
<proof prover="9"><result status="unknown" time="0.00"/></proof>
</goal>
</theory>
<theory name="PowerRealTest" sum="747061f2b592f0feb89bb09cb7faca73" expanded="true">
<theory name="PowerRealTest" sum="eb0bbfff015add810d5cc4a17172919b" expanded="true">
<goal name="Pow_2_2" expanded="true">
<proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.01" steps="6"/></proof>
<proof prover="4" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="8" memlimit="0"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
<theory name="TrigonometryTest" sum="dd9fe92c2a107d45cbcce7b6e297404f" expanded="true">
<goal name="Cos_2_pi" expanded="true">
<proof prover="1" memlimit="0"><result status="valid" time="0.12"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.12" steps="42"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="valid" time="0.11"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="8" memlimit="0"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="Sin_2_pi" expanded="true">
<proof prover="1" timelimit="60"><result status="valid" time="0.60"/></proof>
<proof prover="1" timelimit="60"><result status="valid" time="0.60" steps="181"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4" memlimit="0"><result status="valid" time="0.04"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
......@@ -161,7 +161,7 @@
<proof prover="0" edited="real_TrigonometryTest_Tan_pi_4_1.v"><result status="valid" time="1.47"/></proof>
<proof prover="3"><result status="unknown" time="0.26"/></proof>
<proof prover="5"><result status="timeout" time="4.99"/></proof>
<proof prover="10"><result status="timeout" time="4.98"/></proof>
<proof prover="10"><result status="timeout" time="5.99"/></proof>
<proof prover="11"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="Tan_pi_3" expanded="true">
......
......@@ -171,29 +171,29 @@
</transf>
</goal>
</theory>
<theory name="EuclideanAlgorithm31" sum="82e091181a4d11848b760d8549c12df1" expanded="true">
<theory name="EuclideanAlgorithm31" sum="91fea75d1ece6ac0571a9d40b9bdc3dc" expanded="true">
<goal name="WP_parameter euclid" expl="VC for euclid">
<transf name="split_goal_wp">
<goal name="WP_parameter euclid.1" expl="1. integer overflow">
<proof prover="5" timelimit="5"><result status="valid" time="0.01" steps="6"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="WP_parameter euclid.2" expl="2. postcondition">
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="16"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter euclid.3" expl="3. division by zero">
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="9"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="WP_parameter euclid.4" expl="4. integer overflow">
<proof prover="5" timelimit="5"><result status="valid" time="0.10" steps="52"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.10" steps="47"/></proof>
</goal>
<goal name="WP_parameter euclid.5" expl="5. variant decrease">
<proof prover="5" timelimit="5"><result status="valid" time="0.80" steps="185"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.49" steps="114"/></proof>
</goal>
<goal name="WP_parameter euclid.6" expl="6. precondition">
<proof prover="5" timelimit="5"><result status="valid" time="0.03" steps="27"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.03" steps="21"/></proof>
</goal>
<goal name="WP_parameter euclid.7" expl="7. postcondition">
<proof prover="5" timelimit="5"><result status="valid" time="0.52" steps="45"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.52" steps="42"/></proof>
</goal>
</transf>
</goal>
......
......@@ -6,13 +6,13 @@
<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"/>
<file name="../hackers-delight.mlw" expanded="true">
<theory name="Hackers_delight" sum="820a4c97e42cff42b083e7359e8c7425" expanded="true">
<theory name="Hackers_delight" sum="f68afbb08101be54ae51e015e4048def" expanded="true">
<goal name="countZero" expanded="true">
<proof prover="1"><result status="valid" time="0.05"/></proof>
<proof prover="2"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="countStep" expanded="true">
<proof prover="1"><result status="valid" time="7.86"/></proof>
<proof prover="1"><result status="valid" time="4.98"/></proof>
</goal>
<goal name="symmetric" expanded="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
......@@ -27,16 +27,16 @@
<proof prover="2"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="WP_parameter ascii" expl="VC for ascii" expanded="true">
<proof prover="1"><result status="valid" time="0.18"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="asciiProp" expanded="true">
<proof prover="1"><result status="valid" time="1.95"/></proof>
<proof prover="1"><result status="valid" time="1.41"/></proof>
</goal>
<goal name="iso" expanded="true">
<proof prover="1"><result status="valid" time="0.40"/></proof>
</goal>
<goal name="grayIsGray" expanded="true">
<proof prover="1"><result status="valid" time="0.17"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="nthGray" expanded="true">
<proof prover="1"><result status="valid" time="0.05"/></proof>
......@@ -45,13 +45,13 @@
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="nthBinary" expanded="true">
<proof prover="1"><result status="valid" time="0.84"/></proof>
<proof prover="1"><result status="valid" time="0.48"/></proof>
</goal>
<goal name="evenOdd" expanded="true">
<proof prover="1"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="DM1" expanded="true">
<proof prover="1"><result status="valid" time="0.15"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="DM2" expanded="true">
......@@ -108,7 +108,7 @@
<proof prover="1"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="Ao" expanded="true">
<proof prover="1"><result status="valid" time="0.14"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Aq" expanded="true">
<proof prover="1"><result status="valid" time="0.08"/></proof>
......
......@@ -7,7 +7,7 @@
<prover id="2" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="3" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../bitvectors.why" expanded="true">
<theory name="TestBV" sum="fa2ee38ac18722cb5bafd96ed112adc3" expanded="true">
<theory name="TestBV" sum="362573c1d9c043dd414d1edaaa78f89f" expanded="true">
<goal name="g1" expanded="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
......@@ -67,7 +67,7 @@
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="g4b" expanded="true">
<proof prover="0"><result status="valid" time="0.35" steps="159"/></proof>
<proof prover="0"><result status="valid" time="0.19" steps="159"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
......
......@@ -320,37 +320,37 @@
<transf name="inline_goal">
<goal name="WP_parameter merge.53.1" expl="1. postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter merge.53.1.1" expl="1.">
<goal name="WP_parameter merge.53.1.1" expl="1. VC for merge">
<proof prover="2"><result status="valid" time="0.01" steps="2"/></proof>
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="8" timelimit="40"><result status="valid" time="0.03" steps="2"/></proof>
<proof prover="9"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter merge.53.1.2" expl="2.">
<goal name="WP_parameter merge.53.1.2" expl="2. VC for merge">
<proof prover="2"><result status="valid" time="0.02" steps="3"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="8" timelimit="40"><result status="valid" time="0.05" steps="3"/></proof>
<proof prover="9"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter merge.53.1.3" expl="3.">
<goal name="WP_parameter merge.53.1.3" expl="3. VC for merge">
<proof prover="2"><result status="valid" time="0.03" steps="20"/></proof>
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="8" timelimit="40"><result status="valid" time="0.04" steps="8"/></proof>
<proof prover="9"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter merge.53.1.4" expl="4.">
<goal name="WP_parameter merge.53.1.4" expl="4. VC for merge">
<proof prover="2"><result status="valid" time="0.02" steps="6"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="8" timelimit="40"><result status="valid" time="0.05" steps="8"/></proof>
<proof prover="9"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter merge.53.1.5" expl="5.">
<goal name="WP_parameter merge.53.1.5" expl="5. VC for merge">
<proof prover="2"><result status="valid" time="0.02" steps="3"/></proof>
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="8" timelimit="40"><result status="valid" time="0.04" steps="3"/></proof>
<proof prover="9"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter merge.53.1.6" expl="6.">
<goal name="WP_parameter merge.53.1.6" expl="6. VC for merge">
<proof prover="4"><result status="valid" time="0.24"/></proof>
<proof prover="6" timelimit="40"><result status="valid" time="0.06"/></proof>
<proof prover="9"><result status="valid" time="0.02"/></proof>
......@@ -435,20 +435,20 @@
<transf name="inline_goal">
<goal name="WP_parameter merge_using.11.1" expl="1. assertion">
<transf name="split_goal_wp">
<goal name="WP_parameter merge_using.11.1.1" expl="1.">
<goal name="WP_parameter merge_using.11.1.1" expl="1. VC for merge_using">
<proof prover="2"><result status="valid" time="0.03" steps="21"/></proof>
<proof prover="4"><result status="valid" time="0.05"/></proof>
<proof prover="8" timelimit="20"><result status="valid" time="0.08" steps="21"/></proof>
<proof prover="9"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter merge_using.11.1.2" expl="2.">
<goal name="WP_parameter merge_using.11.1.2" expl="2. VC for merge_using">
<proof prover="1"><result status="valid" time="0.26"/></proof>
<proof prover="2"><result status="valid" time="1.15" steps="379"/></proof>
<proof prover="4"><result status="valid" time="0.12"/></proof>
<proof prover="6"><result status="valid" time="1.15"/></proof>
<proof prover="9"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter merge_using.11.1.3" expl="3.">
<goal name="WP_parameter merge_using.11.1.3" expl="3. VC for merge_using">
<proof prover="2"><result status="valid" time="0.02" steps="21"/></proof>
<proof prover="4"><result status="valid" time="0.06"/></proof>
<proof prover="8" timelimit="20"><result status="valid" time="0.05" steps="21"/></proof>
......@@ -1008,13 +1008,13 @@
</goal>
<goal name="WP_parameter natural_mergesort.13" expl="13. loop variant decrease">
<transf name="split_goal_wp">
<goal name="WP_parameter natural_mergesort.13.1" expl="1.">
<goal name="WP_parameter natural_mergesort.13.1" expl="1. VC for natural_mergesort">
<proof prover="2"><result status="valid" time="0.02" steps="23"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="8"><result status="valid" time="0.02" steps="23"/></proof>
<proof prover="9"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter natural_mergesort.13.2" expl="2.">
<goal name="WP_parameter natural_mergesort.13.2" expl="2. VC for natural_mergesort">
<proof prover="2"><result status="valid" time="0.02" steps="23"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="8"><result status="valid" time="0.06" steps="23"/></proof>
......@@ -1110,7 +1110,6 @@
<goal name="WP_parameter natural_mergesort.29" expl="29. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.18" steps="267"/></proof>
<proof prover="4"><result status="valid" time="0.37"/></proof>
<proof prover="8"><result status="valid" time="5.30" steps="2461"/></proof>
<proof prover="9"><result status="valid" time="0.29"/></proof>
</goal>
<goal name="WP_parameter natural_mergesort.30" expl="30. loop invariant preservation">
......@@ -1145,13 +1144,13 @@
</goal>
<goal name="WP_parameter natural_mergesort.35" expl="35. loop variant decrease">
<transf name="split_goal_wp">
<goal name="WP_parameter natural_mergesort.35.1" expl="1.">
<goal name="WP_parameter natural_mergesort.35.1" expl="1. VC for natural_mergesort">
<proof prover="2"><result status="valid" time="0.01" steps="15"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="8"><result status="valid" time="0.05" steps="15"/></proof>
<proof prover="9"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter natural_mergesort.35.2" expl="2.">
<goal name="WP_parameter natural_mergesort.35.2" expl="2. VC for natural_mergesort">
<proof prover="2"><result status="valid" time="0.02" steps="21"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="8"><result status="valid" time="0.06" steps="21"/></proof>
......@@ -1287,31 +1286,31 @@
</goal>
<goal name="WP_parameter naturalrec.20" expl="20. precondition">
<transf name="split_goal_wp">
<goal name="WP_parameter naturalrec.20.1" expl="1.">
<goal name="WP_parameter naturalrec.20.1" expl="1. VC for naturalrec">
<proof prover="2"><result status="valid" time="0.02" steps="25"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="8"><result status="valid" time="0.02" steps="25"/></proof>
<proof prover="9"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter naturalrec.20.2" expl="2.">
<goal name="WP_parameter naturalrec.20.2" expl="2. VC for naturalrec">
<proof prover="2"><result status="valid" time="0.02" steps="25"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="8"><result status="valid" time="0.03" steps="25"/></proof>
<proof prover="9"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter naturalrec.20.3" expl="3.">
<goal name="WP_parameter naturalrec.20.3" expl="3. VC for naturalrec">
<proof prover="2"><result status="valid" time="0.02" steps="35"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="8"><result status="valid" time="0.03" steps="35"/></proof>
<proof prover="9"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter naturalrec.20.4" expl="4.">
<goal name="WP_parameter naturalrec.20.4" expl="4. VC for naturalrec">
<proof prover="2"><result status="valid" time="0.02" steps="36"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="8"><result status="valid" time="0.02" steps="36"/></proof>
<proof prover="9"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter naturalrec.20.5" expl="5.">
<goal name="WP_parameter naturalrec.20.5" expl="5. VC for naturalrec">
<proof prover="2"><result status="valid" time="0.02" steps="25"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="8"><result status="valid" time="0.02" steps="25"/></proof>
......
......@@ -57,7 +57,7 @@
<proof prover="6"><result status="valid" time="0.00"/></proof>
</goal>
</theory>
<theory name="NQueensSets" sum="21ba9f04704df48b44f79a7e140ea9f4" expanded="true">
<theory name="NQueensSets" sum="9c0bbd6174a933f1b5286251b86db37a" expanded="true">
<goal name="WP_parameter t3" expl="VC for t3" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter t3.1" expl="1. loop invariant init" expanded="true">
......@@ -107,7 +107,7 @@
<proof prover="10"><result status="valid" time="2.23" steps="409"/></proof>
</goal>
<goal name="WP_parameter t3.3.7" expl="7. VC for t3" expanded="true">
<proof prover="0" memlimit="1000" edited="queens_WP_NQueensSets_WP_parameter_t3_1.v"><result status="valid" time="2.07"/></proof>
<proof prover="0" memlimit="1000" edited="queens_WP_NQueensSets_WP_parameter_t3_1.v"><result status="valid" time="1.76"/></proof>
<proof prover="3"><result status="valid" time="5.43" steps="618"/></proof>
<proof prover="10"><result status="valid" time="2.08" steps="562"/></proof>
</goal>
......@@ -137,7 +137,7 @@
<proof prover="10"><result status="valid" time="1.68" steps="285"/></proof>
</goal>
<goal name="WP_parameter t3.3.12.1.3" expl="3. VC for t3" expanded="true">
<proof prover="1"><result status="valid" time="9.75"/></proof>
<proof prover="1"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="WP_parameter t3.3.12.1.4" expl="4. VC for t3" expanded="true">
<metas
......@@ -819,8 +819,8 @@
<goal name="WP_parameter t3.3.12.1.4" expl="4. VC for t3" expanded="true">
<transf name="eliminate_builtin" expanded="true">
<goal name="WP_parameter t3.3.12.1.4.1" expl="1. VC for t3" expanded="true">
<proof prover="5" timelimit="25" obsolete="true"><result status="valid" time="0.12"/></proof>
<proof prover="9" obsolete="true"><result status="valid" time="0.01"/></proof>
<proof prover="5" timelimit="25"><result status="valid" time="0.12"/></proof>
<proof prover="9"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
......@@ -868,7 +868,7 @@
<proof prover="7"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter t3.4.6" expl="6. VC for t3" expanded="true">
<proof prover="0" timelimit="10" edited="queens_WP_NQueensSets_WP_parameter_t3_5.v"><result status="valid" time="3.32"/></proof>
<proof prover="0" timelimit="10" edited="queens_WP_NQueensSets_WP_parameter_t3_5.v"><result status="valid" time="2.87"/></proof>
</goal>
<goal name="WP_parameter t3.4.7" expl="7. VC for t3" expanded="true">
<proof prover="0" timelimit="10" edited="queens_WP_NQueensSets_WP_parameter_t3_6.v"><result status="valid" time="1.60"/></proof>
......@@ -877,7 +877,7 @@
<proof prover="6" timelimit="55"><result status="valid" time="1.92"/></proof>
</goal>
<goal name="WP_parameter t3.4.9" expl="9. VC for t3" expanded="true">
<proof prover="1"><result status="valid" time="0.20"/></proof>
<proof prover="1"><result status="valid" time="0.08"/></proof>
<proof prover="6"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="WP_parameter t3.4.10" expl="10. VC for t3" expanded="true">
......@@ -1032,30 +1032,30 @@
</theory>
<theory name="Bits" sum="87ba23b038d8da5026df22be3839311c" expanded="true">
<goal name="WP_parameter zero" expl="VC for zero" expanded="true">
<proof prover="11" obsolete="true"><result status="valid" time="0.03" steps="80"/></proof>
<proof prover="11"><result status="valid" time="0.03" steps="80"/></proof>
</goal>
<goal name="WP_parameter remove_singleton" expl="VC for remove_singleton" expanded="true">
<proof prover="11" obsolete="true"><result status="valid" time="1.25" steps="578"/></proof>
<proof prover="11"><result status="valid" time="0.80" steps="578"/></proof>
</goal>
<goal name="WP_parameter add_singleton" expl="VC for add_singleton" expanded="true">
<proof prover="2" obsolete="true"><result status="valid" time="1.30"/></proof>
<proof prover="2"><result status="valid" time="1.30"/></proof>
</goal>
<goal name="WP_parameter mul2" expl="VC for mul2" expanded="true">
<proof prover="11" obsolete="true"><result status="valid" time="0.48" steps="218"/></proof>
<proof prover="11"><result status="valid" time="0.27" steps="218"/></proof>
</goal>
<goal name="WP_parameter div2" expl="VC for div2" expanded="true">
<proof prover="11" obsolete="true"><result status="valid" time="0.31" steps="109"/></proof>
<proof prover="11"><result status="valid" time="0.18" steps="109"/></proof>
</goal>
<goal name="WP_parameter diff" expl="VC for diff" expanded="true">
<proof prover="11" obsolete="true"><result status="valid" time="0.46" steps="228"/></proof>
<proof prover="11"><result status="valid" time="0.27" steps="228"/></proof>
</goal>
<goal name="WP_parameter rightmost_bit_trick" expl="VC for rightmost_bit_trick" expanded="true">
<proof prover="2" timelimit="20" obsolete="true"><result status="timeout" time="19.98"/></proof>
<proof prover="5" obsolete="true"><result status="timeout" time="5.05"/></proof>
<proof prover="11" obsolete="true"><result status="timeout" time="4.98"/></proof>