fix node manager code (bugzilla #15, comment #2) in case where there's a hash collisi...

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 0d3fecac663273986a59d48b9b8a31875a80f304..c9a8197517069da457ee796312cddd374d8cd22c 100644 (file)
--- 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;
   }
 }