diff --git a/src/main/scala/leon/xlang/IntroduceGlobalStatePhase.scala b/src/main/scala/leon/xlang/IntroduceGlobalStatePhase.scala
index bf91ff24639a08cc0da615bb9d18ab25fead743b..28e385a9a2308c86cf5f15e395fd8d904e914629 100644
--- a/src/main/scala/leon/xlang/IntroduceGlobalStatePhase.scala
+++ b/src/main/scala/leon/xlang/IntroduceGlobalStatePhase.scala
@@ -54,7 +54,7 @@ object IntroduceGlobalStatePhase extends TransformationPhase {
   }
 
   private def extendFunDefWithState(fd: FunDef, stateCCD: CaseClassDef)(ctx: LeonContext): FunDef = {
-    val newParams = fd.params :+ ValDef(FreshIdentifier("state", stateCCD.typed))
+    val newParams = fd.params :+ ValDef(FreshIdentifier("globalState", stateCCD.typed))
     val newFunDef = new FunDef(fd.id.freshen, fd.tparams, newParams, fd.returnType)
     newFunDef.addFlags(fd.flags)
     newFunDef.setPos(fd)
diff --git a/testcases/verification/xlang/DataRacing.scala b/testcases/verification/xlang/DataRacing.scala
index 2d094a1d5cc6c088d8cde0b6e49551ceea5a0ef8..f5764006168341bc0f2f3a1b1e22d755deb027c5 100644
--- a/testcases/verification/xlang/DataRacing.scala
+++ b/testcases/verification/xlang/DataRacing.scala
@@ -34,12 +34,14 @@ object DataRacing {
     case (RunnableNil(), RunnableNil()) => ()
   }
 
-  def main(): Unit = {
+  //z3 finds counterexample in 0.5
+  //cvc4 needs 130 seconds
+  def main(): Int = {
     val state = SharedState(0)
     val t1 = RunnableCons((s: SharedState) => s.i = s.i + 1, RunnableNil())
     val t2 = RunnableCons((s: SharedState) => s.i = s.i * 2, RunnableNil())
     execute(t1, t2, state)
-    assert(state.i == 2)
-  }
+    state.i
+  } ensuring(_ == 2)
 
 }