add some counter-examples as well

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

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

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

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