diff --git a/testcases/verification/xlang/BankTransfer.scala b/testcases/verification/xlang/BankTransfer.scala
new file mode 100644
index 0000000000000000000000000000000000000000..05b27dbc5c3b1aec5fef575ea20b0d689f1f24e8
--- /dev/null
+++ b/testcases/verification/xlang/BankTransfer.scala
@@ -0,0 +1,42 @@
+import leon.lang._
+
+object BankTransfer {
+
+  def okTransaction(): Unit = {
+    var balance: BigInt = 0
+
+    def balanceInvariant: Boolean = balance >= 0
+
+    def deposit(x: BigInt): Unit = {
+      require(balanceInvariant && x >= 0)
+      balance += x
+    } ensuring(_ => balance == old(balance) + x && balanceInvariant)
+
+    def withdrawal(x: BigInt): Unit = {
+      require(balanceInvariant && x >= 0 && x <= balance)
+      balance -= x
+    } ensuring(_ => balance == old(balance) - x && balanceInvariant)
+
+    deposit(35)
+    withdrawal(30)
+  }
+
+  def invalidTransaction(): Unit = {
+    var balance: BigInt = 0
+
+    def balanceInvariant: Boolean = balance >= 0
+
+    def deposit(x: BigInt): Unit = {
+      require(balanceInvariant && x >= 0)
+      balance += x
+    } ensuring(_ => balance == old(balance) + x && balanceInvariant)
+
+    def withdrawal(x: BigInt): Unit = {
+      require(balanceInvariant && x >= 0 && x <= balance)
+      balance -= x
+    } ensuring(_ => balance == old(balance) - x && balanceInvariant)
+
+    deposit(35)
+    withdrawal(40)
+  }
+}