testing weird cases that causes issues with xlang

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

+package test.resources.regression.verification.xlang.invalid
+
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+object Assert1 {
+
+  def foo(): Int = {
+    var a = 0
+    a += 1
+    assert(a == 0)
+    a
+  }
+
+}

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

+/* Copyright 2009-2015 EPFL, Lausanne */
+
+object Assert2 {
+
+  def foo(): Int = {
+    var a = 0
+    assert(a == 1)
+    a += 1
+    a
+  }
+
+}

src/test/resources/regression/verification/xlang/valid/Assert1.scala

+/* Copyright 2009-2015 EPFL, Lausanne */
+
+object Assert1 {
+
+  def foo(): Int = {
+    var a = 0
+    a += 1
+    assert(a == 1)
+    a
+  }
+
+}

src/test/resources/regression/verification/xlang/valid/Assert2.scala

+/* Copyright 2009-2015 EPFL, Lausanne */
+
+object Assert2 {
+
+  def foo(): Int = {
+    var a = 0
+    assert(a == 0)
+    a += 1
+    a
+  }
+
+}

src/test/resources/regression/verification/xlang/valid/Assert3.scala

+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.lang._
+
+object Assert3 {
+
+  def test(i: Int): Int = {
+    var j = i
+
+    assert(j == i)
+    j += 1
+    assert(j == i + 1)
+    j += 2
+    assert(j == i + 2)
+
+    j
+
+  }
+
+}

src/test/resources/regression/verification/xlang/valid/Sequencing1.scala

+object Sequencing1 {
+
+  def test(): Int = {
+    var x = 0
+    x += 1
+    x *= 2
+    x
+  } ensuring(x => x == 2)
+
+}

src/test/resources/regression/verification/xlang/valid/Sequencing2.scala

+object Sequencing2 {
+
+  def test(): Int = {
+    var x = 0
+    x += 5
+    x *= 10
+    x
+  } ensuring(x => x == 50)
+
+}

src/test/resources/regression/verification/xlang/valid/Sequencing3.scala

+object Sequencing3 {
+
+  def f(x: Int): Int = {
+    require(x < 10)
+    x
+  }
+
+  def test(): Int = {
+    var x = 0
+    f(x)
+    x += 5
+    f(x)
+    x += 5
+
+    x
+  }
+
+}

src/test/resources/regression/verification/xlang/valid/Sequencing4.scala

+object Sequencing4 {
+
+  def test(): Int = {
+    var x = 5
+
+    {x = x + 1; x} + {x = x * 2; x}
+
+  } ensuring(res => res == 18)
+
+}

src/test/resources/regression/verification/xlang/valid/Sequencing5.scala

+object Sequencing5 {
+
+
+  def test(): (Int, Int, Int) = {
+    var x = 5
+
+    (
+      {x = x + 1; x},
+      {x = x * 2; x},
+      {x = x - 1; x}
+    )
+
+  } ensuring(res => res._1 == 6 && res._2 == 12 && res._3 == 11)
+
+}

src/test/resources/regression/verification/xlang/valid/Sequencing6.scala

+object Sequencing6 {
+
+  def f(x1: Int, x2: Int, x3: Int): Int = {
+    require(x1 == 6 && x2 == 12 && x3 == 11)
+    x3
+  }
+
+  def test(): Int = {
+    var x = 5
+
+    f(
+      {x = x + 1; x},
+      {x = x * 2; x},
+      {x = x - 1; x}
+    )
+
+    x
+
+  } ensuring(res => res == 11)
+
+}

src/test/resources/regression/verification/xlang/valid/Sequencing7.scala

+package test.resources.regression.verification.xlang.valid
+
+object Sequencing7 {
+
+
+  def test(): Int = {
+    var x = 5
+
+    {x = x + 1; x}
+    {x = x * 2; x}
+    {x = x - 1; x}
+
+    x
+
+  } ensuring(res => res == 11)
+
+}

src/test/resources/regression/verification/xlang/valid/Sequencing8.scala

+object Sequencing8 {
+
+  def test(): Int = {
+    var x = 5
+
+    (x = x + 1, (x = x * 2, (x = x - 1, x = x * 2)))
+
+    x
+  } ensuring(res => res == 22)
+
+}