- printf("x: %d\n", x.load(std::memory_order_acquire));
- printf("y: %d\n", y.load(std::memory_order_acquire));
- printf("z: %d\n", z.load(std::memory_order_acquire));
- printf("x: %d\n", x.load(std::memory_order_acquire));
+ int x1, y1, z1, x2;
+ x1 = x.load(std::memory_order_acquire);
+ y1 = y.load(std::memory_order_acquire);
+ z1 = z.load(std::memory_order_acquire);
+ x2 = x.load(std::memory_order_acquire);
+ printf("x: %d\n", x1);
+ printf("y: %d\n", y1);
+ printf("z: %d\n", z1);
+ printf("x: %d\n", x2);
+
+ /* If x1 and x2 are the same, even value, then y1 must equal z1 */
+ MODEL_ASSERT(x1 != x2 || x1 & 0x1 || y1 == z1);