From 1b1e9acfad453c50151f6c6465e5eabbac075f19 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 1 Feb 2010 17:28:15 +0000
Subject: [PATCH] fix node manager code (bugzilla #15, comment #2) in case
 where there's a hash collision for distinct objects

---
 src/expr/node_manager.cpp | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 0d3fecac6..c9a819751 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -60,10 +60,8 @@ Node NodeManager::lookup(uint64_t hash, NodeValue* ev) {
     }
 
     // didn't find it, insert
-    std::vector<Node> v;
     Node e(ev);
-    v.push_back(e);
-    d_hash.insert(std::make_pair(hash, v));
+    i->second.push_back(e);
     return e;
   }
 }
-- 
2.30.2