Formal Verification of Out-of-Order Execution Using Incremental Flushing