Snugglebug: A Powerful Approach to Weakest Preconditions