Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study