diff --git a/testcases/Account2.scala b/testcases/Account2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e6fb25ce8d840d45490db6c0eef55551f472609f
--- /dev/null
+++ b/testcases/Account2.scala
@@ -0,0 +1,22 @@
+object Account2 {
+  sealed abstract class AccLike 
+  case class Acc(checking : Int, savings : Int) extends AccLike
+
+  def sameTotal(a1 : Acc, a2 : Acc) : Boolean = {
+    a1.checking + a1.savings == a2.checking + a2.savings
+  }
+  def notRed(a : Acc) : Boolean = {
+    a.checking >= 0 && a.savings >= 0
+  }
+
+  def toSavingsOk(x : Int, a : Acc) : Acc = {
+    require (notRed(a) && x >= 0 && a.checking >= x)
+    Acc(a.checking - x, a.savings + x)
+  } ensuring (res => (notRed(res) && sameTotal(a, res)))
+
+  def toSavingsBroken(x : Int, a : Acc) : Acc = {
+    require (notRed(a) && a.checking >= x)
+    Acc(a.checking - x, a.savings + x)
+  } ensuring (res => (notRed(res) && sameTotal(a, res)))
+
+}