--- a/cbmc/insert_verification/cbmcLLRBContext.c	Sun Jun 19 06:43:25 2016 +0000
+++ b/cbmc/insert_verification/cbmcLLRBContext.c	Tue Jun 21 01:07:31 2016 +0000
@@ -4,6 +4,7 @@
 #include "cbmcLLRBContext.h"
 
 /* for CBMC */
+extern void enumerateInputs_stub(struct Context*);
 extern void verifySpecification_stub(struct Context*);
 
 /* definitions from llrb */
@@ -55,6 +56,7 @@
     context->heapStart = malloc(context->heapLimit);
     memset(context->heapStart, 0, context->heapLimit);
 
+    context->code[EnumerateInputs]     = enumerateInputs_stub;;
     context->code[VerifySpecification] = verifySpecification_stub;
 
     /* definitions from llrb */

--- a/cbmc/insert_verification/include/cbmcLLRBContext.h	Sun Jun 19 06:43:25 2016 +0000
+++ b/cbmc/insert_verification/include/cbmcLLRBContext.h	Tue Jun 21 01:07:31 2016 +0000
@@ -6,6 +6,7 @@
 
 enum Code {
     /* for CBMC */
+    EnumerateInputs,
     VerifySpecification,
 
     /* definitions from llrb */

--- a/cbmc/insert_verification/insert_verification.sh	Sun Jun 19 06:43:25 2016 +0000
+++ b/cbmc/insert_verification/insert_verification.sh	Tue Jun 21 01:07:31 2016 +0000
@@ -23,5 +23,5 @@
 
 copy_and_substitute ${LLRB_PATH}/include/stack.h       ${CBMC_INCLUDE_DIR}
 
-cbmc --unwind 50 -I ${CBMC_INCLUDE_DIR} -I include cbmc_files/*.c *.c
+cbmc --unwind 5 -I ${CBMC_INCLUDE_DIR} -I include cbmc_files/*.c *.c
 #/bin/clang -Wall -O0 -g -I ${CBMC_INCLUDE_DIR} -I include cbmc_files/*.c *.c

--- a/cbmc/insert_verification/main.c	Sun Jun 19 06:43:25 2016 +0000
+++ b/cbmc/insert_verification/main.c	Tue Jun 21 01:07:31 2016 +0000
@@ -6,9 +6,9 @@
 void meta(struct Context*, enum Code);
 
 /* cbmc built in functions */
-int nondet_int() { return 9 ;}
+int nondet_int(); 
 
-// TODO c functions
+/* functions for verification */
 void printTree(struct Node* node, int n) {
     if (node != 0) {
         printTree(node->left, n+1);
@@ -19,16 +19,42 @@
     }
 }
 
+unsigned int minHeight(struct Node* node, unsigned int height) {
+    if ((node->left == NULL) && (node->right == NULL)) return height;
+    if (node->left  == NULL) return minHeight(node->right, height+1);
+    if (node->right == NULL) return minHeight(node->left, height+1);
 
-void verifySpecification(struct Context* context, struct Node* node) {
+    unsigned int left_min  = minHeight(node->left, height+1);
+    unsigned int right_min = minHeight(node->right, height+1);
+
+    if (left_min < right_min) {
+        return left_min;
+    } else {
+        return right_min;
+    }
+}
+
+unsigned int maxHeight(struct Node* node, unsigned int height) {
+    if ((node->left == NULL) && (node->right == NULL)) return height;
+    if (node->left  == NULL) return maxHeight(node->right, height+1);
+    if (node->right == NULL) return maxHeight(node->left, height+1);
+
+    unsigned int left_max  = maxHeight(node->left, height+1);
+    unsigned int right_max = maxHeight(node->right, height+1);
+
+    if (left_max > right_max) {
+        return left_max;
+    } else {
+        return right_max;
+    }
+}
+
+void enumerateInputs(struct Context* context, struct Node* node) {
     if (context->loopCount > LIMIT_OF_VERIFICATION_SIZE) {
         return meta(context, Exit);
     }
-    printTree(context->data[Tree]->tree.root, 0);
-    //assert(context->data[Tree]->tree.root->key == 0);
 
-    int hoge      = nondet_int();
-    node->key     = hoge;
+    node->key     = nondet_int();
     node->value   = node->key;
     context->next = VerifySpecification;
     context->loopCount++;
@@ -36,12 +62,22 @@
     return meta(context, Put);
 }
 
+void enumerateInputs_stub(struct Context* context) {
+    return enumerateInputs(context, &context->data[Node]->node);
+}
+
+
+void verifySpecification(struct Context* context, struct Tree* tree) {
+    assert(!(maxHeight(tree->root, 1) > 2*minHeight(tree->root, 1)));
+    return meta(context, EnumerateInputs);
+}
+
 void verifySpecification_stub(struct Context* context) {
-    return verifySpecification(context, &context->data[Node]->node);
+    return verifySpecification(context, &context->data[Tree]->tree);
 }
 
 
 int main(int argc, char const* argv[]) {
-    startCode(VerifySpecification);
+    startCode(EnumerateInputs);
     return 0;
 }