leon finds data racing counter-example

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)

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)
 
 }