diff --git a/src/test/resources/regression/verification/xlang/valid/NestedFunState7.scala b/src/test/resources/regression/verification/xlang/valid/NestedFunState7.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ff2418a0c972add2d48c08f6319905f35d0493c2
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/NestedFunState7.scala
@@ -0,0 +1,27 @@
+import leon.lang._
+
+object NestedFunState7 {
+
+  def test(x: BigInt): BigInt = {
+
+    var a = BigInt(0)
+
+    def defCase(): Unit = {
+      a = 100
+    }
+
+    if(x >= 0) {
+      a = 2*x
+      if(a < 100) {
+        a = 100 - a
+      } else {
+        defCase()
+      }
+    } else {
+      defCase()
+    }
+
+    a
+  } ensuring(res => res >= 0 && res <= 100)
+
+}