Commit eab93a08 authored by Martin Clochard's avatar Martin Clochard
parents 0773d8c0 7054c4ca
...@@ -22,87 +22,87 @@ ...@@ -22,87 +22,87 @@
<proof prover="4"><result status="valid" time="0.03"/></proof> <proof prover="4"><result status="valid" time="0.03"/></proof>
</goal> </goal>
</theory> </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"> <goal name="WP_parameter binary_search" expl="VC for binary_search" expanded="true">
<transf name="split_goal_wp" expanded="true"> <transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter binary_search.1" expl="1. integer overflow"> <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>
<goal name="WP_parameter binary_search.2" expl="2. integer overflow"> <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>
<goal name="WP_parameter binary_search.3" expl="3. integer overflow"> <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>
<goal name="WP_parameter binary_search.4" expl="4. loop invariant init"> <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>
<goal name="WP_parameter binary_search.5" expl="5. loop invariant init"> <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>
<goal name="WP_parameter binary_search.6" expl="6. integer overflow"> <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>
<goal name="WP_parameter binary_search.7" expl="7. integer overflow"> <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>
<goal name="WP_parameter binary_search.8" expl="8. division by zero"> <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>
<goal name="WP_parameter binary_search.9" expl="9. integer overflow"> <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>
<goal name="WP_parameter binary_search.10" expl="10. integer overflow"> <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>
<goal name="WP_parameter binary_search.11" expl="11. assertion"> <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>
<goal name="WP_parameter binary_search.12" expl="12. index in array bounds"> <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>
<goal name="WP_parameter binary_search.13" expl="13. integer overflow"> <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>
<goal name="WP_parameter binary_search.14" expl="14. integer overflow"> <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>
<goal name="WP_parameter binary_search.15" expl="15. loop invariant preservation"> <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>
<goal name="WP_parameter binary_search.16" expl="16. loop invariant preservation"> <goal name="WP_parameter binary_search.16" expl="16. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.04"/></proof> <proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></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>
<goal name="WP_parameter binary_search.17" expl="17. loop variant decrease"> <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>
<goal name="WP_parameter binary_search.18" expl="18. index in array bounds"> <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>
<goal name="WP_parameter binary_search.19" expl="19. integer overflow"> <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>
<goal name="WP_parameter binary_search.20" expl="20. integer overflow"> <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>
<goal name="WP_parameter binary_search.21" expl="21. loop invariant preservation"> <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>
<goal name="WP_parameter binary_search.22" expl="22. loop invariant preservation"> <goal name="WP_parameter binary_search.22" expl="22. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.04"/></proof> <proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></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>
<goal name="WP_parameter binary_search.23" expl="23. loop variant decrease"> <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>
<goal name="WP_parameter binary_search.24" expl="24. postcondition"> <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>
<goal name="WP_parameter binary_search.25" expl="25. exceptional postcondition"> <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> </goal>
</transf> </transf>
</goal> </goal>
......
This diff is collapsed.
...@@ -17,7 +17,7 @@ ...@@ -17,7 +17,7 @@
<file name="../real.why" expanded="true"> <file name="../real.why" expanded="true">
<theory name="Test" sum="cf206e9b789e3b16bbeee98ff5359bb7" expanded="true"> <theory name="Test" sum="cf206e9b789e3b16bbeee98ff5359bb7" expanded="true">
<goal name="G1" 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="2"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><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> <proof prover="6"><result status="valid" time="0.00"/></proof>
...@@ -26,7 +26,7 @@ ...@@ -26,7 +26,7 @@
<proof prover="9"><result status="valid" time="0.00"/></proof> <proof prover="9"><result status="valid" time="0.00"/></proof>
</goal> </goal>
<goal name="G2" expanded="true"> <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="2"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><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> <proof prover="6"><result status="valid" time="0.00"/></proof>
...@@ -34,7 +34,7 @@ ...@@ -34,7 +34,7 @@
<proof prover="9"><result status="valid" time="0.00"/></proof> <proof prover="9"><result status="valid" time="0.00"/></proof>
</goal> </goal>
<goal name="G3" expanded="true"> <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="2"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><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> <proof prover="6"><result status="valid" time="0.00"/></proof>
...@@ -43,7 +43,7 @@ ...@@ -43,7 +43,7 @@
</theory> </theory>
<theory name="TestInfix" sum="9929e0fb7685505424762277d915662a" expanded="true"> <theory name="TestInfix" sum="9929e0fb7685505424762277d915662a" expanded="true">
<goal name="Add" 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="2"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><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> <proof prover="6"><result status="valid" time="0.00"/></proof>
...@@ -51,7 +51,7 @@ ...@@ -51,7 +51,7 @@
<proof prover="9"><result status="valid" time="0.00"/></proof> <proof prover="9"><result status="valid" time="0.00"/></proof>
</goal> </goal>
<goal name="Sub" expanded="true"> <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="2"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><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> <proof prover="6"><result status="valid" time="0.00"/></proof>
...@@ -59,7 +59,7 @@ ...@@ -59,7 +59,7 @@
<proof prover="9"><result status="valid" time="0.00"/></proof> <proof prover="9"><result status="valid" time="0.00"/></proof>
</goal> </goal>
<goal name="Neg" expanded="true"> <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="2"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><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> <proof prover="6"><result status="valid" time="0.00"/></proof>
...@@ -67,7 +67,7 @@ ...@@ -67,7 +67,7 @@
<proof prover="9"><result status="valid" time="0.00"/></proof> <proof prover="9"><result status="valid" time="0.00"/></proof>
</goal> </goal>
<goal name="Mul" expanded="true"> <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="2"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><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> <proof prover="6"><result status="valid" time="0.00"/></proof>
...@@ -75,7 +75,7 @@ ...@@ -75,7 +75,7 @@
<proof prover="9"><result status="valid" time="0.00"/></proof> <proof prover="9"><result status="valid" time="0.00"/></proof>
</goal> </goal>
<goal name="Div" expanded="true"> <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="2"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><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> <proof prover="6"><result status="valid" time="0.00"/></proof>
...@@ -83,7 +83,7 @@ ...@@ -83,7 +83,7 @@
<proof prover="9"><result status="valid" time="0.00"/></proof> <proof prover="9"><result status="valid" time="0.00"/></proof>
</goal> </goal>
<goal name="Inv" expanded="true"> <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="2"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><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> <proof prover="6"><result status="valid" time="0.00"/></proof>
...@@ -92,7 +92,7 @@ ...@@ -92,7 +92,7 @@
</theory> </theory>
<theory name="SquareTest" sum="b399f090ec659c1b880d355f5452fbc9" expanded="true"> <theory name="SquareTest" sum="b399f090ec659c1b880d355f5452fbc9" expanded="true">
<goal name="Sqrt_zero" 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="2"><result status="valid" time="0.01"/></proof>
<proof prover="4" timelimit="60"><result status="valid" time="0.02"/></proof> <proof prover="4" timelimit="60"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof> <proof prover="6"><result status="valid" time="0.00"/></proof>
...@@ -100,7 +100,7 @@ ...@@ -100,7 +100,7 @@
<proof prover="9"><result status="valid" time="0.00"/></proof> <proof prover="9"><result status="valid" time="0.00"/></proof>
</goal> </goal>
<goal name="Sqrt_one" expanded="true"> <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="2"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="valid" time="0.01"/></proof> <proof prover="4" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof> <proof prover="6"><result status="valid" time="0.00"/></proof>
...@@ -108,17 +108,17 @@ ...@@ -108,17 +108,17 @@
<proof prover="9"><result status="valid" time="0.00"/></proof> <proof prover="9"><result status="valid" time="0.00"/></proof>
</goal> </goal>
<goal name="Sqrt_four" expanded="true"> <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="2"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="valid" time="1.27"/></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="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> <proof prover="9"><result status="valid" time="0.00"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="ExpLogTest" sum="b87cf6a8ae7e92621e77bacb7a1fd605" expanded="true"> <theory name="ExpLogTest" sum="b87cf6a8ae7e92621e77bacb7a1fd605" expanded="true">
<goal name="Log_e" 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="2"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="valid" time="0.01"/></proof> <proof prover="4" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof> <proof prover="6"><result status="valid" time="0.00"/></proof>
...@@ -127,7 +127,7 @@ ...@@ -127,7 +127,7 @@
</theory> </theory>
<theory name="PowerIntTest" sum="a44ed7f266568491fd1a5efcfad78047" expanded="true"> <theory name="PowerIntTest" sum="a44ed7f266568491fd1a5efcfad78047" expanded="true">
<goal name="Pow_2_2" 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="2"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="valid" time="0.01"/></proof> <proof prover="4" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof> <proof prover="6"><result status="valid" time="0.00"/></proof>
...@@ -135,23 +135,23 @@ ...@@ -135,23 +135,23 @@
<proof prover="9"><result status="unknown" time="0.00"/></proof> <proof prover="9"><result status="unknown" time="0.00"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="PowerRealTest" sum="747061f2b592f0feb89bb09cb7faca73" expanded="true"> <theory name="PowerRealTest" sum="eb0bbfff015add810d5cc4a17172919b" expanded="true">
<goal name="Pow_2_2" 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="4" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="8" memlimit="0"><result status="valid" time="0.01"/></proof> <proof prover="8" memlimit="0"><result status="valid" time="0.01"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="TrigonometryTest" sum="dd9fe92c2a107d45cbcce7b6e297404f" expanded="true"> <theory name="TrigonometryTest" sum="dd9fe92c2a107d45cbcce7b6e297404f" expanded="true">
<goal name="Cos_2_pi" 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="2"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="valid" time="0.11"/></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="6"><result status="valid" time="0.00"/></proof>
<proof prover="8" memlimit="0"><result status="valid" time="0.09"/></proof> <proof prover="8" memlimit="0"><result status="valid" time="0.09"/></proof>
</goal> </goal>
<goal name="Sin_2_pi" expanded="true"> <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="2"><result status="valid" time="0.01"/></proof>
<proof prover="4" memlimit="0"><result status="valid" time="0.04"/></proof> <proof prover="4" memlimit="0"><result status="valid" time="0.04"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof> <proof prover="6"><result status="valid" time="0.01"/></proof>
...@@ -161,7 +161,7 @@ ...@@ -161,7 +161,7 @@
<proof prover="0" edited="real_TrigonometryTest_Tan_pi_4_1.v"><result status="valid" time="1.47"/></proof> <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="3"><result status="unknown" time="0.26"/></proof>
<proof prover="5"><result status="timeout" time="4.99"/></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> <proof prover="11"><result status="timeout" time="5.00"/></proof>
</goal> </goal>
<goal name="Tan_pi_3" expanded="true"> <goal name="Tan_pi_3" expanded="true">
......
...@@ -171,29 +171,29 @@ ...@@ -171,29 +171,29 @@
</transf> </transf>
</goal> </goal>
</theory> </theory>
<theory name="EuclideanAlgorithm31" sum="82e091181a4d11848b760d8549c12df1" expanded="true"> <theory name="EuclideanAlgorithm31" sum="91fea75d1ece6ac0571a9d40b9bdc3dc" expanded="true">
<goal name="WP_parameter euclid" expl="VC for euclid"> <goal name="WP_parameter euclid" expl="VC for euclid">
<transf name="split_goal_wp"> <transf name="split_goal_wp">
<goal name="WP_parameter euclid.1" expl="1. integer overflow"> <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>
<goal name="WP_parameter euclid.2" expl="2. postcondition"> <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>
<goal name="WP_parameter euclid.3" expl="3. division by zero"> <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>
<goal name="WP_parameter euclid.4" expl="4. integer overflow"> <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>
<goal name="WP_parameter euclid.5" expl="5. variant decrease"> <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>
<goal name="WP_parameter euclid.6" expl="6. precondition"> <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>
<goal name="WP_parameter euclid.7" expl="7. postcondition"> <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> </goal>
</transf> </transf>
</goal> </goal>
......
...@@ -6,13 +6,13 @@ ...@@ -6,13 +6,13 @@
<prover id="1" name="CVC4" version="1.4" 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="2" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../hackers-delight.mlw" expanded="true"> <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"> <goal name="countZero" expanded="true">
<proof prover="1"><result status="valid" time="0.05"/></proof> <proof prover="1"><result status="valid" time="0.05"/></proof>
<proof prover="2"><result status="valid" time="0.09"/></proof> <proof prover="2"><result status="valid" time="0.09"/></proof>
</goal> </goal>
<goal name="countStep" expanded="true"> <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>
<goal name="symmetric" expanded="true"> <goal name="symmetric" expanded="true">
<proof prover="1"><result status="valid" time="0.02"/></proof> <proof prover="1"><result status="valid" time="0.02"/></proof>
...@@ -27,16 +27,16 @@ ...@@ -27,16 +27,16 @@
<proof prover="2"><result status="timeout" time="5.00"/></proof> <proof prover="2"><result status="timeout" time="5.00"/></proof>
</goal> </goal>
<goal name="WP_parameter ascii" expl="VC for ascii" expanded="true"> <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>
<goal name="asciiProp" expanded="true"> <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>
<goal name="iso" expanded="true"> <goal name="iso" expanded="true">
<proof prover="1"><result status="valid" time="0.40"/></proof> <proof prover="1"><result status="valid" time="0.40"/></proof>
</goal> </goal>
<goal name="grayIsGray" expanded="true"> <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>
<goal name="nthGray" expanded="true"> <goal name="nthGray" expanded="true">
<proof prover="1"><result status="valid" time="0.05"/></proof> <proof prover="1"><result status="valid" time="0.05"/></proof>
...@@ -45,13 +45,13 @@ ...@@ -45,13 +45,13 @@
<proof prover="1"><result status="valid" time="0.04"/></proof> <proof prover="1"><result status="valid" time="0.04"/></proof>
</goal> </goal>
<goal name="nthBinary" expanded="true"> <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>
<goal name="evenOdd" expanded="true"> <goal name="evenOdd" expanded="true">
<proof prover="1"><result status="valid" time="0.14"/></proof> <proof prover="1"><result status="valid" time="0.14"/></proof>
</goal> </goal>
<goal name="DM1" expanded="true"> <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> <proof prover="2"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="DM2" expanded="true"> <goal name="DM2" expanded="true">
...@@ -108,7 +108,7 @@ ...@@ -108,7 +108,7 @@
<proof prover="1"><result status="valid" time="0.12"/></proof> <proof prover="1"><result status="valid" time="0.12"/></proof>
</goal> </goal>
<goal name="Ao" expanded="true"> <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>
<goal name="Aq" expanded="true"> <goal name="Aq" expanded="true">
<proof prover="1"><result status="valid" time="0.08"/></proof> <proof prover="1"><result status="valid" time="0.08"/></proof>
......
...@@ -7,7 +7,7 @@ ...@@ -7,7 +7,7 @@
<prover id="2" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/> <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"/> <prover id="3" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../bitvectors.why" expanded="true"> <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"> <goal name="g1" expanded="true">
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof> <proof prover="3"><result status="valid" time="0.01"/></proof>
...@@ -67,7 +67,7 @@ ...@@ -67,7 +67,7 @@
<proof prover="3"><result status="valid" time="0.00"/></proof> <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal> </goal>
<goal name="g4b" expanded="true"> <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="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof> <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal> </goal>
......
...@@ -320,37 +320,37 @@ ...@@ -320,37 +320,37 @@
<transf name="inline_goal"> <transf name="inline_goal">
<goal name="WP_parameter merge.53.1" expl="1. postcondition"> <goal name="WP_parameter merge.53.1" expl="1. postcondition">
<transf name="split_goal_wp"> <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="2"><result status="valid" time="0.01" steps="2"/></proof>
<proof prover="4"><result status="valid" time="0.04"/></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="8" timelimit="40"><result status="valid" time="0.03" steps="2"/></proof>
<proof prover="9"><result status="valid" time="0.02"/></proof> <proof prover="9"><result status="valid" time="0.02"/></proof>
</goal> </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="2"><result status="valid" time="0.02" steps="3"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></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="8" timelimit="40"><result status="valid" time="0.05" steps="3"/></proof>
<proof prover="9"><result status="valid" time="0.02"/></proof> <proof prover="9"><result status="valid" time="0.02"/></proof>
</goal> </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="2"><result status="valid" time="0.03" steps="20"/></proof>
<proof prover="4"><result status="valid" time="0.04"/></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="8" timelimit="40"><result status="valid" time="0.04" steps="8"/></proof>
<proof prover="9"><result status="valid" time="0.02"/></proof>