diff --git a/examples/contracts/bst/BSTAsSet.scala b/examples/contracts/bst/BSTAsSet.scala
index 6185b843322555e6bfe585341725d2e8f1ec2afa..c3c402098f749e6c36316c1760310132d40e1827 100644
--- a/examples/contracts/bst/BSTAsSet.scala
+++ b/examples/contracts/bst/BSTAsSet.scala
@@ -12,8 +12,10 @@ object BSTAsSet extends Application {
         case Node(_,left,v,right) if (x > v) => Node(content + x, 
 						   left, v, right.add(x))
         case Node(_,_,v,_) if (v == x) => this
+// this is due to limitation of pattern matching check
+	case _ => this
       }
-    } ensuring(result => (result.content == content + x))
+    } ensuring (_.content == content + x)
 
     // patterns are exhaustive, disjoint and all reachable 
     def contains(key: Int): Boolean = {
@@ -22,8 +24,10 @@ object BSTAsSet extends Application {
         case Node(_,_,v,right) if (key > v) => right.contains(key)
         case Node(_,_,v, _) if (key == v) => true
         case Empty(_) => false
+// this is due to limitation of pattern matching check
+	case _ => false
       }
-    } ensuring(res => (res == content.contains(key)))
+    } ensuring (_ == content.contains(key))
   }
   
   case class Empty(override val content : Set[Int]) extends BST(Set.empty)