diff --git a/src/test/resources/regression/verification/xlang/invalid/Assert1.scala b/src/test/resources/regression/verification/xlang/invalid/Assert1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8027179df9bcda58c7300e571506f481bb78791e
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Assert1.scala
@@ -0,0 +1,14 @@
+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
+  }
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Assert2.scala b/src/test/resources/regression/verification/xlang/invalid/Assert2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..cc8b2a591015ea765a1549a75b51821770c3c9bf
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Assert2.scala
@@ -0,0 +1,12 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+object Assert2 {
+
+  def foo(): Int = {
+    var a = 0
+    assert(a == 1)
+    a += 1
+    a
+  }
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Assert1.scala b/src/test/resources/regression/verification/xlang/valid/Assert1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d9ae5c6753320b35d193042044144a91ecf19070
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Assert1.scala
@@ -0,0 +1,12 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+object Assert1 {
+
+  def foo(): Int = {
+    var a = 0
+    a += 1
+    assert(a == 1)
+    a
+  }
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Assert2.scala b/src/test/resources/regression/verification/xlang/valid/Assert2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0f5131346f9e9b56ab3a08198cc8a3bb87049fd3
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Assert2.scala
@@ -0,0 +1,12 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+object Assert2 {
+
+  def foo(): Int = {
+    var a = 0
+    assert(a == 0)
+    a += 1
+    a
+  }
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Assert3.scala b/src/test/resources/regression/verification/xlang/valid/Assert3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..58af2ef087119b2dc55160028dab5bb87e11f345
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Assert3.scala
@@ -0,0 +1,20 @@
+/* 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
+
+  }
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Sequencing1.scala b/src/test/resources/regression/verification/xlang/valid/Sequencing1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d1041aef525a2837fcbf9e9e4059d78308b773b7
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Sequencing1.scala
@@ -0,0 +1,10 @@
+object Sequencing1 {
+
+  def test(): Int = {
+    var x = 0
+    x += 1
+    x *= 2
+    x
+  } ensuring(x => x == 2)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Sequencing2.scala b/src/test/resources/regression/verification/xlang/valid/Sequencing2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e152b00adb31cfa38183972c8d565c952b686730
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Sequencing2.scala
@@ -0,0 +1,10 @@
+object Sequencing2 {
+
+  def test(): Int = {
+    var x = 0
+    x += 5
+    x *= 10
+    x
+  } ensuring(x => x == 50)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Sequencing3.scala b/src/test/resources/regression/verification/xlang/valid/Sequencing3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..cd9d94c465a6b47d2d0ee080fd8693a41bb58bd0
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Sequencing3.scala
@@ -0,0 +1,18 @@
+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
+  }
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Sequencing4.scala b/src/test/resources/regression/verification/xlang/valid/Sequencing4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..fb6802192e0fd9e96531b4d886443e7a7efbdbdd
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Sequencing4.scala
@@ -0,0 +1,10 @@
+object Sequencing4 {
+
+  def test(): Int = {
+    var x = 5
+
+    {x = x + 1; x} + {x = x * 2; x}
+
+  } ensuring(res => res == 18)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Sequencing5.scala b/src/test/resources/regression/verification/xlang/valid/Sequencing5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1a958a5ffd5ce919b6f3f0f49b29abee1ab83050
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Sequencing5.scala
@@ -0,0 +1,15 @@
+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)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Sequencing6.scala b/src/test/resources/regression/verification/xlang/valid/Sequencing6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..26dd91b8db8c1965991d1f49fa9eae9f549c69d8
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Sequencing6.scala
@@ -0,0 +1,21 @@
+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)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Sequencing7.scala b/src/test/resources/regression/verification/xlang/valid/Sequencing7.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f3628703bf5c0a073a05797b773246d8ff01960c
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Sequencing7.scala
@@ -0,0 +1,17 @@
+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)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Sequencing8.scala b/src/test/resources/regression/verification/xlang/valid/Sequencing8.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a37092ecffa8a91f589bc2ec7e32328d1b56ceca
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Sequencing8.scala
@@ -0,0 +1,11 @@
+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)
+
+}