diff --git a/src/main/scala/leon/xlang/XLangDesugaringPhase.scala b/src/main/scala/leon/xlang/XLangDesugaringPhase.scala
index b00935fcd20c1b036f6da749433e20893b60198f..ae216dc62c8f92f715b6d464bd88e6a0fff307cd 100644
--- a/src/main/scala/leon/xlang/XLangDesugaringPhase.scala
+++ b/src/main/scala/leon/xlang/XLangDesugaringPhase.scala
@@ -17,7 +17,9 @@ object XLangDesugaringPhase extends LeonPhase[Program, Program] {
       PrintTreePhase(title).when(ctx.reporter.isDebugEnabled(DebugSectionTrees))
 
     val phases =
+      debugTrees("Program before starting xlang-desugaring") andThen
       IntroduceGlobalStatePhase andThen
+      debugTrees("Program after introduce-global-state") andThen
       AntiAliasingPhase andThen
       debugTrees("Program after anti-aliasing") andThen
       EpsilonElimination andThen
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon7.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon7.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3bbfde20d909d3a8832b9e441d2e5f0edb9f118b
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon7.scala
@@ -0,0 +1,19 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+import leon.lang._
+import leon.lang.xlang._
+
+object Epsilon7 {
+
+  def rand(): Int = epsilon((x: Int) => true)
+
+  //this used to be VALID until the introduction
+  //of a global state that can tracks epsilon calls
+  //and ensure each epsilon is invoked with a different
+  //seed value
+  def wrongProperty1(): Boolean = {
+    rand() == rand() 
+  }.holds
+
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon8.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon8.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a95ff4ea79db3f7e0109017e8fc4646a0a4bc8d0
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon8.scala
@@ -0,0 +1,12 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+import leon.lang._
+import leon.lang.xlang._
+
+object Epsilon8 {
+
+  def wrongProp: Boolean = {
+    epsilon((y: Int) => true) == epsilon((y: Int) => true)
+  } holds
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon9.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon9.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c21e5333e8240e624fe3290441453c65f766e7f5
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon9.scala
@@ -0,0 +1,26 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+import leon.lang._
+import leon.lang.xlang._
+
+object Epsilon9 {
+
+  def random(): BigInt = epsilon((x: BigInt) => true)
+
+  /*
+   * The implementation relies on a potential bug in random(), when
+   * two calls of random with the same args (0 here) will return
+   * the same value. If that's the case, then we can prove the
+   * postcondition. Epsilon should behave really randomly, so that
+   * postcondition should be invalid.
+   */
+  def findPositive(): BigInt = {
+    val x = random()
+    if(x < 0) {
+      -random()
+    } else {
+      x
+    }
+  } ensuring(res => res >= 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala
deleted file mode 100644
index 6506c4d97c71b59c1d3edb16dca33bdc238911eb..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala
+++ /dev/null
@@ -1,16 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-import leon.lang._
-import leon.lang.xlang._
-
-object Epsilon2 {
-
-  def rand(): Int = epsilon((x: Int) => true)
-
-  //this should hold, that is the expected semantic of our epsilon
-  def property1(): Boolean = {
-    rand() == rand() 
-  }.holds
-
-
-}