diff --git a/llvm_mode/dfsan_rt/dfsan/dfsan.cc b/llvm_mode/dfsan_rt/dfsan/dfsan.cc
index 8ee017bc..2d475d6f 100644
--- a/llvm_mode/dfsan_rt/dfsan/dfsan.cc
+++ b/llvm_mode/dfsan_rt/dfsan/dfsan.cc
@@ -51,6 +51,7 @@
 #include <vector>
 
 #define OPTIMISTIC 1
+#define RESTRICT_CONSTRAINT 1
 
 using namespace __dfsan;
 
@@ -99,7 +100,16 @@ struct expr_equal {
     return lhs.id() == rhs.id();
   }
 };
+
+#if RESTRICT_CONSTRAINT
+typedef struct {
+  std::unordered_set<z3::expr,expr_hash,expr_equal> exprs;
+  std::unordered_set<dfsan_label> deps;
+} branch_dep_t;
+#else
 typedef std::unordered_set<z3::expr, expr_hash, expr_equal> branch_dep_t;
+#endif
+
 static std::vector<branch_dep_t*> *__branch_deps;
 
 Flags __dfsan::flags_data;
@@ -704,7 +714,9 @@ static z3::expr serialize(dfsan_label label, std::unordered_set<u32> &deps) {
   }
   z3::expr op2 = __z3_context.bv_val((uint64_t)info->op2, size);
   if (info->l2 >= CONST_OFFSET) {
-    op2 = serialize(info->l2, deps).simplify();
+    std::unordered_set<u32> deps2;
+    op2 = serialize(info->l2, deps2).simplify();
+    deps.insert(deps2.begin(),deps2.end());
   } else if (info->size == 1) {
     op2 = __z3_context.bool_val(info->op2 == 1);
   }
@@ -800,6 +812,30 @@ add_constraints(dfsan_label label) {
   try {
     std::unordered_set<dfsan_label> inputs;
     z3::expr cond = serialize(label, inputs);
+#if RESTRICT_CONSTRAINT
+    branch_dep_t* the_tree = nullptr;
+    for (auto off : inputs) {
+      auto c = __branch_deps->at(off);
+      if (c == nullptr) {
+        c = new branch_dep_t();
+      }
+      if (the_tree == nullptr) {
+        the_tree = c;
+      }
+      else  {
+        the_tree->exprs.insert(c->exprs.begin(),c->exprs.end());
+        the_tree->deps.insert(c->deps.begin(),c->deps.end());
+        for (auto &idx : c->deps) {
+          __branch_deps->at(idx) = the_tree;
+        }
+      }
+      __branch_deps->at(off) = the_tree;
+    }
+    the_tree->exprs.insert(cond);
+    for (auto off : inputs) {
+    the_tree->deps.insert(off);
+  }
+#else
     for (auto off : inputs) {
       auto c = __branch_deps->at(off);
       if (c == nullptr) {
@@ -808,6 +844,7 @@ add_constraints(dfsan_label label) {
       }
       c->insert(cond);
     }
+#endif
   } catch (z3::exception e) {
     Report("WARNING: adding constraints error: %s\n", e.msg());
   }
@@ -833,11 +870,16 @@ static void __solve_cond(dfsan_label label, z3::expr &result, void *addr) {
 
     __z3_solver.reset();
     // add dependencies
-    branch_dep_t added;
+    //branch_dep_t added;
+    std::unordered_set<z3::expr,expr_hash,expr_equal> added;
     for (auto off : inputs) {
       auto c = __branch_deps->at(off);
       if (c) {
+#if RESTRICT_CONSTRAINT
+        for (auto &expr : c->exprs) {
+#else
         for (auto &expr : *c) {
+#endif
           if (added.insert(expr).second) {
             //AOUT("adding expr: %s\n", expr.to_string().c_str());
             __z3_solver.add(expr);
@@ -869,7 +911,31 @@ static void __solve_cond(dfsan_label label, z3::expr &result, void *addr) {
       }
 #endif
     }
-
+#if RESTRICT_CONSTRAINT
+    // nested branch
+    branch_dep_t* the_tree = nullptr;
+    for (auto off : inputs) {
+      auto c = __branch_deps->at(off);
+      if (c == nullptr) {
+        c = new branch_dep_t();
+      }
+      if (the_tree == nullptr) {
+        the_tree = c;
+      }
+      else  {
+        the_tree->exprs.insert(c->exprs.begin(),c->exprs.end());
+        the_tree->deps.insert(c->deps.begin(),c->deps.end());
+        for (auto &idx : c->deps) {
+          __branch_deps->at(idx) = the_tree;
+        }
+      }
+      __branch_deps->at(off) = the_tree;
+    }
+    the_tree->exprs.insert(cond);
+    for (auto off : inputs) {
+      the_tree->deps.insert(off);
+    }
+#else
     // nested branch
     for (auto off : inputs) {
       auto c = __branch_deps->at(off);
@@ -879,7 +945,7 @@ static void __solve_cond(dfsan_label label, z3::expr &result, void *addr) {
       }
       c->insert(cond == result);
     }
-
+#endif
     // mark as flipped
     get_label_info(label)->flags |= B_FLIPPED;
   } catch (z3::exception e) {
@@ -964,11 +1030,16 @@ __taint_trace_gep(dfsan_label label, u64 r) {
 
     __z3_solver.reset();
     // add dependencies
-    branch_dep_t added;
+    //branch_dep_t added;
+    std::unordered_set<z3::expr,expr_hash,expr_equal> added;
     for (auto off : inputs) {
       auto c = __branch_deps->at(off);
       if (c) {
+#if RESTRICT_CONSTRAINT
+        for (auto &expr : c->exprs) {
+#else
         for (auto &expr : *c) {
+#endif
           if (added.insert(expr).second) {
             __z3_solver.add(expr);
           }
@@ -1005,9 +1076,14 @@ __taint_trace_gep(dfsan_label label, u64 r) {
         c = new branch_dep_t();
         __branch_deps->at(off) = c;
       }
+#if RESTRICT_CONSTRAINT
+      c->exprs.insert(index == result);
+#else
       c->insert(index == result);
+#endif
     }
 
+
     // mark as visited
     get_label_info(label)->flags |= B_FLIPPED;
   } catch (z3::exception e) {