From 3584308f734a68e916befdbed105ae60d62e9a98 Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <vkuncak@gmail.com>
Date: Fri, 19 Nov 2010 19:09:27 +0000
Subject: [PATCH] BST is not working

---
 testcases/BSTSimpler.scala | 18 +++++++++++++++++-
 1 file changed, 17 insertions(+), 1 deletion(-)

diff --git a/testcases/BSTSimpler.scala b/testcases/BSTSimpler.scala
index 02957dcbd..f3b2b6893 100644
--- a/testcases/BSTSimpler.scala
+++ b/testcases/BSTSimpler.scala
@@ -49,7 +49,7 @@ object BSTSimpler {
   def emptySet(): Tree = Leaf()
 
   def insert(tree: Tree, value: Int): Node = {
-    require(size(tree) <= 1 && isBST(tree))
+    require(isBST(tree))
     tree match {
       case Leaf() => Node(Leaf(), value, Leaf())
       case Node(l, v, r) => (if (v < value) {
@@ -62,6 +62,22 @@ object BSTSimpler {
     }
   } ensuring(res => isBST(res) && content(res) == content(tree) ++ Set(value))
 
+/*
+  def remove(tree : Tree, value : Int) : Tree = {
+    require(size(tree) <= 1 && isBST(tree))
+    tree match {
+      case Leaf() => Node(Leaf(), value, Leaf())
+      case Node(l, v, r) => (if (v < value) {
+        Node(l, v, insert(r, value))
+      } else if (v > value) {
+        Node(insert(l, value), v, r)
+      } else {
+        Node(l, v, r)
+      })
+    }
+  }
+*/
+
   def createRoot(v: Int): Node = {
     Node(Leaf(), v, Leaf())
   } ensuring (content(_) == Set(v))
-- 
GitLab