Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification