update epsilon tests

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

src/test/resources/regression/verification/xlang/valid/Epsilon2.scala → src/test/resources/regression/verification/xlang/invalid/Epsilon7.scala

@@ -3,12 +3,15 @@
 import leon.lang._
 import leon.lang.xlang._
 
-object Epsilon2 {
+object Epsilon7 {
 
   def rand(): Int = epsilon((x: Int) => true)
 
-  //this should hold, that is the expected semantic of our epsilon
-  def property1(): Boolean = {
+  //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
 

src/test/resources/regression/verification/xlang/invalid/Epsilon8.scala

+/* 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
+
+}

src/test/resources/regression/verification/xlang/invalid/Epsilon9.scala

+/* 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)
+
+}