Lazy Sequentialization for the Safety Verification of Unbounded Concurrent Programs