diff --git a/library/util/Random.scala b/library/util/Random.scala
index e055dc51bf2e0ffa6426fa2b2ddbddb2888b2f8f..8a942e31be0d8ec4df6a9914bb83e5799982404f 100644
--- a/library/util/Random.scala
+++ b/library/util/Random.scala
@@ -29,4 +29,3 @@ object Random {
   } ensuring(res => res >= 0 && res < max)
 
 }
-
diff --git a/testcases/verification/xlang/DataRacing.scala b/testcases/verification/xlang/DataRacing.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2592955948059fa7a237bed6a89858786f527790
--- /dev/null
+++ b/testcases/verification/xlang/DataRacing.scala
@@ -0,0 +1,42 @@
+import leon.lang._
+import leon.lang.xlang._
+import leon.util.Random
+
+import leon.collection._
+
+object DataRacing {
+  
+  case class SharedState(var i: Int)
+
+  case class AtomicInstr(instr: (SharedState) => Unit)
+
+  implicit def toInstr(instr: (SharedState) => Unit): AtomicInstr = AtomicInstr(instr)
+
+
+  def execute(t1: List[AtomicInstr], t2: List[AtomicInstr], state: SharedState): Unit = (t1, t2) match {
+    case (x::xs, y::ys) =>
+      if(Random.nextBoolean) {
+        x.instr(state)
+        execute(xs, y::ys, state)
+      } else {
+        y.instr(state)
+        execute(x::xs, ys, state)
+      }
+    case (Nil(), y::ys) =>
+      y.instr(state)
+      execute(Nil(), ys, state)
+    case (x::xs, Nil()) =>
+      x.instr(state)
+      execute(xs, Nil(), state)
+    case (Nil(), Nil()) => ()
+  }
+
+  def main(): Unit = {
+    val state = SharedState(0)
+    val t1 = List[AtomicInstr]((s: SharedState) => s.i = s.i + 1)
+    val t2 = List[AtomicInstr]((s: SharedState) => s.i = s.i * 2)
+    execute(t1, t2, state)
+    assert(state.i == 2)
+  }
+
+}