diff --git a/src/funcheck/AnalysisComponent.scala b/src/funcheck/AnalysisComponent.scala
index 332c4629b78c09afee0885acec12c2a252c88935..0497946ec08a211c20907a5ca0701b49f9ea0deb 100644
--- a/src/funcheck/AnalysisComponent.scala
+++ b/src/funcheck/AnalysisComponent.scala
@@ -43,6 +43,9 @@ class AnalysisComponent(val global: Global, val pluginInstance: FunCheckPlugin)
       println("Extracted program for " + unit + ": ")
       println(prog)
 
+      println("Starting analysis.")
+      purescala.Analysis.analyze(prog)
+
       // Mirco your component can do its job here, as I leave the trees
       // unmodified.
       // val (genDef, arbDef) = createGeneratorDefDefs(unit)
diff --git a/src/purescala/Analysis.scala b/src/purescala/Analysis.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1f9809ad9b459edc60f09730ae2fdc015a8898ef
--- /dev/null
+++ b/src/purescala/Analysis.scala
@@ -0,0 +1,36 @@
+package purescala
+
+import Definitions._
+import Trees._
+
+object Analysis {
+    // Analysis should check that:
+    //  - all the postconditions are implied by preconds. + body
+    //  - all callsites satisfy the preconditions
+    //  - all matches are exhaustive
+    // In the future:
+    //  - catamorphisms are catamorphisms (poss. with surjectivity conds.)
+    //  - injective functions are injective
+    //  - all global invariants are satisfied 
+    def analyze(program: Program) : Unit = {
+        program.mainObject.defs.filter(_.isInstanceOf[FunDef]).foreach(df => {
+            val funDef = df.asInstanceOf[FunDef]
+            val vc = postconditionVC(funDef)
+            if(vc != BooleanLiteral(true)) {
+                println("Verification condition for " + funDef.id + ":")
+                println(vc)
+            }
+        }) 
+    }
+
+    def postconditionVC(functionDefinition: FunDef) : Expr = {
+        val prec = functionDefinition.precondition
+        val post = functionDefinition.postcondition
+
+        if(post.isEmpty) {
+            BooleanLiteral(true)
+        } else {
+            BooleanLiteral(false)
+        }
+    }
+}
diff --git a/src/purescala/PrettyPrinter.scala b/src/purescala/PrettyPrinter.scala
index 8a835a8963452efde6ddd47f07eb01f8d482c4ac..c96723707f278ed8a0b0aec944a71a993231e7df 100644
--- a/src/purescala/PrettyPrinter.scala
+++ b/src/purescala/PrettyPrinter.scala
@@ -98,10 +98,10 @@ object PrettyPrinter {
     case GreaterThan(l,r) => ppBinary(sb, l, r, " > ", lvl)
     case LessEquals(l,r) => ppBinary(sb, l, r, " \u2264 ", lvl)      // \leq
     case GreaterEquals(l,r) => ppBinary(sb, l, r, " \u2265 ", lvl)   // \geq
-    case EmptySet(_) => sb.append("Ø")
-    case SetUnion(l,r) => ppBinary(sb, l, r, " U ", lvl)
-    case SetDifference(l,r) => ppBinary(sb, l, r, " \\ ", lvl)
-    case SetIntersection(l,r) => ppBinary(sb, l, r, " INT ", lvl)
+    case EmptySet(_) => sb.append("\u2205")                          // Ø
+    case SetUnion(l,r) => ppBinary(sb, l, r, " \u222A ", lvl)        // \cup
+    case SetDifference(l,r) => ppBinary(sb, l, r, " \\ ", lvl)       
+    case SetIntersection(l,r) => ppBinary(sb, l, r, " \u2229 ", lvl) // \cap
     
     case IfExpr(c, t, e) => {
       var nsb = sb
diff --git a/testcases/BinarySearchTree.scala b/testcases/BinarySearchTree.scala
new file mode 100644
index 0000000000000000000000000000000000000000..329878053f478024ab97733668a91bcf3fe8dd08
--- /dev/null
+++ b/testcases/BinarySearchTree.scala
@@ -0,0 +1,29 @@
+import scala.collection.immutable.Set
+
+object BinarySearchTree {
+    sealed abstract class Tree
+    case class Node(left: Tree, value: Int, right: Tree) extends Tree
+    case class Leaf() extends Tree
+
+    def emptySet() : Tree = Leaf()
+
+    def insert(tree: Tree, value: Int) : Tree = (tree match {
+        case Leaf() => Node(Leaf(), value, Leaf())
+        case n @ Node(_, v, _) if v == value => n
+        case Node(l, v, r) if v < value => Node(l, v, insert(r, value))
+        case Node(l, v, r) if v > value => Node(insert(l, value), v, r)
+    }) ensuring(_ != Leaf())
+
+    def contains(tree: Tree, value: Int) : Boolean = tree match {
+        case Leaf() => false
+        case Node(_, v, _) if v == value => true 
+        case Node(l, v, r) if v < value => contains(r, value)
+        case Node(l, v, r) if v > value => contains(l, value)
+    }
+
+    def contents(tree: Tree) : Set[Int] = tree match {
+        case Leaf() => Set.empty[Int]
+        case Node(l, v, r) => contents(l) /*++ Set(v)*/ ++ contents(r)
+    }
+}
+