diff --git a/src/test/resources/regression/verification/xlang/invalid/NestedFunState1.scala b/src/test/resources/regression/verification/xlang/invalid/NestedFunState1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9372ea742a278a3da3d476dca57e52c55c09b978
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/NestedFunState1.scala
@@ -0,0 +1,20 @@
+object NestedFunState1 {
+
+  def simpleSideEffect(n: BigInt): BigInt = {
+    require(n > 0)
+
+    var a = BigInt(0)
+
+    def incA(prevA: BigInt): Unit = {
+      require(prevA == a)
+      a += 1
+    } ensuring(_ => a == prevA + 1)
+
+    incA(a)
+    incA(a)
+    incA(a)
+    incA(a)
+    a
+  } ensuring(_ == 5)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/NestedFunState2.scala b/src/test/resources/regression/verification/xlang/invalid/NestedFunState2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..68769df28353c9defa6d33000bb8ae4de21c7ace
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/NestedFunState2.scala
@@ -0,0 +1,23 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+object NestedFunState2 {
+
+  def sum(n: BigInt): BigInt = {
+    require(n > 0)
+    var i = BigInt(0)
+    var res = BigInt(0)
+
+    def iter(): Unit = {
+      require(res >= i && i >= 0)
+      if(i < n) {
+        i += 1
+        res += i
+        iter()
+      }
+    }
+
+    iter()
+    res
+  } ensuring(_ < 0)
+
+}