diff --git a/src/examples/bst/bst_map.c b/src/examples/bst/bst_map.c
new file mode 100644
index 0000000..d6cbf1e
--- /dev/null
+++ b/src/examples/bst/bst_map.c
@@ -0,0 +1,165 @@
+
+#include "bst_map.h"
+#include "bst_map_cn.h"
+
+
+#if 0
+/* Allocate a new singleton node */
+struct MapNode *newNode(KEY key, VALUE value)
+/*@
+requires
+  true;
+ensures
+  take node = Owned<struct MapNode>(return);
+  node.key == key;
+  node.value == value;
+  is_null(node.smaller);
+  is_null(node.larger);
+@*/
+{
+  struct MapNode *node = malloc_MapNode();
+  node->key = key;
+  node->value = value;
+  node->smaller = NULL;
+  node->larger = NULL;
+  return node;
+}
+#endif
+
+#if 0
+// Demonstrates a recursive traversal of a tree.
+size_t count(struct MapNode const *node)
+/*@
+requires
+  take before = BST(node);
+ensures
+  take after = BST(node);
+  before == after;
+@*/
+{
+  if (node == NULL) return 0;
+  return (size_t)1 + count(node->smaller) + count(node->larger);
+}
+#endif
+
+
+#if 1
+// A no-op function, just shows hows to traverse a tree with a loop.
+void traverse(struct MapNode *node)
+/*@
+requires
+  take start = BST(node, anyKey());
+ensures
+  take end = BST(node, anyKey());
+  // start == end;
+@*/
+{
+  struct MapNode *cur = node;
+
+  /*@ split_case is_null(cur); @*/
+  while (cur)
+  /*@
+  inv
+    {node} unchanged;
+    take focus = BSTFocus(node,cur,anyKey());
+    // start == unfocus(focus);
+    let cur_prev = cur;
+  @*/
+  {
+    cur = cur->smaller;
+    /*@ apply GoSmaller(node,cur_prev,anyKey()); @*/
+  }
+}
+#endif
+
+
+#if 0
+struct MapNode *findLeast(struct MapNode *p)
+/*@
+requires
+  take tree = BST(p);
+ensures
+  take final_tree = BST(p);
+  tree == final_tree;
+@*/
+{
+  struct MapNode *parent = NULL;
+  struct MapNode *cur = p;
+  while(cur != NULL)
+  /*@
+  inv
+    {p} unchanged;
+    take front = BSTUpTo(cur,parent);
+  @*/
+  {
+    parent = cur;
+    cur = p->smaller;
+    
+  }
+  return parent;
+}
+#endif
+
+
+#if 0
+/* Look for a node and its parent */
+struct MapNode *findParent(struct MapNode **node, KEY key)
+{
+  struct MapNode *parent = NULL;
+  struct MapNode *cur = *node;
+  while (cur != NULL)
+  {
+    KEY k = cur->key;
+    if (k == key) { *node = cur; return parent; }
+    parent = cur;
+    cur = k < key? cur->larger : cur->smaller;
+  }
+  *node = cur;
+  return parent;
+}
+#endif
+
+
+#if 0
+/* Create an empty set */
+struct Map map_empty() 
+/*@  @*/
+{
+  return (struct Map) { .root = NULL };
+}
+#endif
+
+#if 0
+/* Lookup a value in a map */
+bool map_lookup(struct Map map, KEY key, VALUE *value) {
+  struct MapNode *search = map.root;
+  findParent(&search, key);
+  if (search == NULL) { return false; }
+  *value = search->value;
+  return true;
+}
+#endif
+
+#if 0
+/* Insert an element into a map. Overwrites previous if already present. */
+void map_insert(struct Map *map, KEY key, VALUE value) {
+  struct MapNode *search = map->root;
+  struct MapNode *parent = findParent(&search, key);
+  if (search != NULL) {
+    search->value = value;
+    return;
+  }
+
+  if (parent == NULL) {
+    map->root = newNode(key,value);
+    return;
+  }
+
+  struct MapNode *new_node = newNode(key,value);
+  if (parent->key < key) {
+    parent->larger = new_node;
+  } else {
+    parent->smaller = new_node;
+  }
+}
+#endif
diff --git a/src/examples/bst/bst_map.h b/src/examples/bst/bst_map.h
new file mode 100644
index 0000000..bc28dd7
--- /dev/null
+++ b/src/examples/bst/bst_map.h
@@ -0,0 +1,29 @@
+#ifndef SET_H
+#define SET_H
+/* A set defined as binary search tree */
+
+#include <stdbool.h>
+
+#define KEY    int
+#define VALUE  long
+
+struct MapNode {
+  KEY key;
+  int ignore;
+  VALUE value; 
+  struct MapNode *smaller;
+  struct MapNode *larger;
+};
+
+struct MapNode* malloc_MapNode();
+
+
+struct Map {
+  struct MapNode *root;
+};
+
+struct Map map_empty();
+bool map_lookup(struct Map map, KEY key, VALUE *value);
+
+
+#endif // SET_H
diff --git a/src/examples/bst/bst_map_cn.c b/src/examples/bst/bst_map_cn.c
new file mode 100644
index 0000000..ac5dbdd
--- /dev/null
+++ b/src/examples/bst/bst_map_cn.c
@@ -0,0 +1,10 @@
+#include <stdlib.h>
+#include <assert.h>
+
+#include "bst_map_cn.h"
+
+struct MapNode *malloc_MapNode() {
+  struct MapNode *result = malloc(sizeof(struct MapNode));
+  assert(result != NULL);
+  return result;
+}
diff --git a/src/examples/bst/bst_map_cn.h b/src/examples/bst/bst_map_cn.h
new file mode 100644
index 0000000..b0296da
--- /dev/null
+++ b/src/examples/bst/bst_map_cn.h
@@ -0,0 +1,153 @@
+#ifndef BST_MAP_CN_H
+#define BST_MAP_CN_H
+
+#include "bst_map.h"
+#include "bst_sem_cn.h"
+
+// Specialized `malloc`
+extern struct MapNode *malloc_MapNode();
+/*@
+spec malloc_MapNode();
+requires
+  true;
+ensures
+  take v = Block<struct MapNode>(return);
+@*/
+
+
+
+/*@
+
+// *****************************************************************************
+// Consuming an entire tree
+// *****************************************************************************
+
+
+// Semantic data stored at a node
+function (NodeData) getNodeData(struct MapNode node) {
+  { key: node.key, value: node.value }
+}
+
+
+// A binary search tree, where all keys are in the given range.
+predicate BST BST(pointer root, Interval range) {
+  if (is_null(root)) {
+    return Leaf {};
+  } else {
+    take node = Owned<struct MapNode>(root);
+    let data = getNodeData(node);
+    assert(inInterval(node.key, range));
+    let ranges = splitInterval(node.key, range);
+    take smaller = BST(node.smaller, ranges.lower);
+    take larger  = BST(node.larger, ranges.upper);
+    return Node { data: data, smaller: smaller, larger: larger };
+  }
+}
+
+
+
+
+// *****************************************************************************
+// Focusing on a node in the tree
+// *****************************************************************************
+
+type_synonym BSTFocus = {
+  // Indicates if we are at a node or a leaf.
+  boolean at_leaf,
+
+  // Rest of the tree
+  BST done,
+
+  // Focused node
+  struct MapNode node,
+  BST smaller,
+  BST larger
+}
+
+predicate BSTFocus BSTFocus(pointer root, pointer child, Interval range) {
+  if (is_null(child)) {
+    take tree = BST(root, range);
+    return { at_leaf: true, done: tree,
+             node: default<struct MapNode>,
+             smaller: default<BST>,
+             larger: default<BST> };
+  } else {
+    take node    = Owned<struct MapNode>(child);
+    take result  = BSTNodeUpTo(root, child, node, range);
+    let ranges   = splitInterval(node.key,result.range);
+    take smaller = BST(node.smaller, ranges.lower);
+    take larger  = BST(node.larger, ranges.upper);
+    return { at_leaf: false, done: result.tree, node: node,
+             smaller: smaller, larger: larger };
+  }
+}
+
+// Consume parts of the tree starting at `p` until we get to `c`.
+// We do not consume `c`.
+// `child` is the node stored at `c`.
+predicate { BST tree, Interval range }
+  BSTNodeUpTo(pointer p, pointer c, struct MapNode child, Interval range) {
+  if (ptr_eq(p,c)) {
+    return { tree: Leaf {}, range: range };
+  } else {
+    take parent = Owned<struct MapNode>(p);
+    assert(inInterval(parent.key, range));
+    let ranges = splitInterval(parent.key, range);
+    take result = BSTNodeChildUpTo(c, child, parent, ranges);
+    return result;
+  }
+}
+
+// Starting at a parent with data `data` and children `smaller` and `larger`,
+// we go toward `c`, guided by its value, `target`.
+predicate { BST tree, Interval range }
+  BSTNodeChildUpTo(pointer c, struct MapNode target, struct MapNode parent, Intervals ranges) {
+  if (parent.key < target.key) {
+    take small = BST(parent.smaller, ranges.lower);
+    take large = BSTNodeUpTo(parent.larger, c, target, ranges.upper);
+    return { tree: Node { data: getNodeData(parent), smaller: small, larger: large.tree },
+             range: large.range };
+  } else {
+  if (parent.key > target.key) {
+    take small = BSTNodeUpTo(parent.smaller, c, target, ranges.lower);
+    take large = BST(parent.larger, ranges.upper);
+    return { tree: Node { data: getNodeData(parent), smaller: small.tree, larger: large },
+             range: small.range };
+  } else {
+    // We should never get here, but asserting `false` is not allowed
+    return default<{ BST tree, Interval range }>;
+  }}
+}
+
+function (BST) unfocus(BSTFocus focus) {
+  if (focus.at_leaf) {
+    focus.done
+  } else {
+    let node = focus.node;
+    let bst = Node { data: getNodeData(node),
+                     smaller: focus.smaller,
+                     larger: focus.larger
+                    };
+    setKey(node.key, focus.done, bst)
+  }
+}
+
+lemma FocusUnfocus(pointer root, pointer cur, Interval range)
+  requires
+    take x = BSTFocus(root,cur,range);
+  ensures
+    take y = BST(root,range);
+    unfocus(x) == y;
+
+lemma GoSmaller(pointer root, pointer cur, Interval range)
+  requires
+    !is_null(cur);
+    take focus = BSTFocus(root,cur,range);
+  ensures
+    take focus_smaller = BSTFocus(root,focus.node.smaller,range);
+    unfocus(focus) == unfocus(focus_smaller);
+
+
+
+@*/
+#endif
diff --git a/src/examples/bst/bst_sem_cn.h b/src/examples/bst/bst_sem_cn.h
new file mode 100644
index 0000000..a26899a
--- /dev/null
+++ b/src/examples/bst/bst_sem_cn.h
@@ -0,0 +1,53 @@
+#ifndef BST_SEM_CN_H
+#define BST_SEM_CN_H
+
+// Functional Sepcification of Binary Search Tree
+
+/*@
+type_synonym KEY = i32
+type_synonym VALUE = i64
+type_synonym NodeData = { KEY key, VALUE value }
+
+function (KEY) minKey() { MINi32() }
+function (KEY) maxKey() { MAXi32() }
+function (KEY) incKey(KEY x) { if (x < maxKey()) { x + 1i32 } else { x } }
+function (KEY) decKey(KEY x) { if (x > minKey()) { x - 1i32 } else { x } }
+
+type_synonym Interval = { KEY lower, KEY upper }
+function (Interval) anyKey() {{ lower: minKey(), upper: maxKey() }}
+
+type_synonym Intervals = { Interval lower, Interval upper }
+function (Intervals) splitInterval(KEY x, Interval i) {
+  { lower: { lower: i.lower, upper: decKey(x) },
+    upper: { lower: incKey(x), upper: i.upper }
+  }
+}
+
+function (boolean) inInterval(KEY x, Interval i) {
+  i.lower <= x && x <= i.upper
+}
+
+
+// A binary dearch tree
+datatype BST {
+  Leaf {},
+  Node { NodeData data, BST smaller, BST larger }
+}
+
+function [rec] (BST) setKey(KEY k, BST root, BST value) {
+  match root {
+    Leaf {} => { value }
+    Node { data: data, smaller: smaller, larger: larger } => {
+      if (k < data.key) {
+        Node { data: data, smaller: setKey(k, smaller, value), larger: larger }
+      } else {
+        Node { data: data, smaller: smaller, larger: setKey(k, larger, value) }
+      }
+    }
+  }
+}
+
+
+@*/
+
+#endif
\ No newline at end of file