Towards completeness in Bounded Model Checking through Automatic Recursion Depth Detection