diff --git a/specifications/btree/MCbtreeExhaustion.cfg b/specifications/btree/MCbtreeExhaustion.cfg
new file mode 100644
index 00000000..851eb30e
--- /dev/null
+++ b/specifications/btree/MCbtreeExhaustion.cfg
@@ -0,0 +1,40 @@
+\* A root split needs two free nodes; this pool has only one left.
+SPECIFICATION Spec
+
+CONSTANTS
+    READY = ready
+    GET_VALUE = get_value
+    FIND_LEAF_TO_ADD = find_leaf_to_add
+    WHICH_TO_SPLIT = which_to_split
+
+    ADD_TO_LEAF = add_to_leaf
+    SPLIT_ROOT_LEAF = split_root_leaf
+    SPLIT_ROOT_INNER = split_root_inner
+    SPLIT_INNER = split_inner
+    SPLIT_LEAF = split_leaf
+    UPDATE_LEAF = update_leaf
+
+
+    NIL = nil
+    MISSING = missing
+
+    Vals = {x}
+
+    MaxOccupancy = 2
+
+CONSTANTS
+    MaxNode = 2
+    MaxKey = 3
+
+CONSTANTS
+    Keys <- MCKeys
+    Nodes <- MCNodes
+
+CHECK_DEADLOCK FALSE
+
+INVARIANT
+TypeOk
+InnersMustHaveLast
+LeavesCantHaveLast
+KeyOrderPreserved
+KeysInLeavesAreUnique
diff --git a/specifications/btree/btree.tla b/specifications/btree/btree.tla
index 64c9a761..79a114f1 100644
--- a/specifications/btree/btree.tla
+++ b/specifications/btree/btree.tla
@@ -98,6 +98,9 @@ IsFree(node) == isLeaf[node] /\ keysOf[node] = {}
 
 ChooseFreeNode == CHOOSE n \in Nodes : IsFree(n)
 
+HasFreeNode == \E n \in Nodes : IsFree(n)
+HasTwoFreeNodes == \E n1, n2 \in Nodes : n1 # n2 /\ IsFree(n1) /\ IsFree(n2)
+
 
 Init == /\ isLeaf = [n \in Nodes |-> TRUE]
         /\ keysOf = [n \in Nodes |-> {}]
@@ -217,6 +220,7 @@ SplitRootLeaf ==
         n2Keys == {x \in keys: x>=pivot} 
         keyToInsert == args[1] IN
     /\ state = SPLIT_ROOT_LEAF
+    /\ HasTwoFreeNodes
     /\ root' = newRoot
     /\ isLeaf' = [isLeaf EXCEPT ![newRoot]=FALSE, ![n2]=TRUE]
     /\ keysOf' = [keysOf EXCEPT ![newRoot]={pivot}, ![n1]=n1Keys, ![n2]=n2Keys]
@@ -248,6 +252,7 @@ SplitRootInner ==
         n1Keys == {x \in keys: x<pivot}
         n2Keys == {x \in keys: x>pivot} IN
     /\ state = SPLIT_ROOT_INNER
+    /\ HasTwoFreeNodes
     /\ root' = newRoot
     /\ isLeaf' = [isLeaf EXCEPT ![newRoot]=FALSE, ![n2]=FALSE]
     /\ keysOf' = [keysOf EXCEPT ![newRoot]={pivot}, ![n1]=n1Keys, ![n2]=n2Keys]
@@ -273,6 +278,7 @@ SplitLeaf ==
         keyToInsert == args[1]
     IN
     /\ state = SPLIT_LEAF
+    /\ HasFreeNode
     /\ isLeaf' = [isLeaf EXCEPT ![n2]=TRUE]
     /\ keysOf' = [keysOf EXCEPT ![parent]=@ \union {pivot}, ![n1]=n1Keys, ![n2]=n2Keys]
     \* In the parent, point the pivot key to n1, and point the parent key to n2.
diff --git a/specifications/btree/manifest.json b/specifications/btree/manifest.json
index 3a4ce245..08be5450 100644
--- a/specifications/btree/manifest.json
+++ b/specifications/btree/manifest.json
@@ -23,8 +23,17 @@
           "mode": "exhaustive search",
           "result": "success",
           "distinctStates": 374727,
-          "totalStates": 2820091,
+          "totalStates": 2892343,
           "stateDepth": 38
+        },
+        {
+          "path": "specifications/btree/MCbtreeExhaustion.cfg",
+          "runtime": "00:00:01",
+          "mode": "exhaustive search",
+          "result": "success",
+          "distinctStates": 202,
+          "totalStates": 778,
+          "stateDepth": 11
         }
       ]
     },
@@ -44,4 +53,4 @@
       ]
     }
   ]
-}
\ No newline at end of file
+}