From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 1 Feb 2010 17:28:15 +0000 (+0000)
Subject: fix node manager code (bugzilla #15, comment #2) in case where there's a hash collisi... 
X-Git-Tag: cvc5-1.0.0~9320
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1b1e9acfad453c50151f6c6465e5eabbac075f19;p=cvc5.git

fix node manager code (bugzilla #15, comment #2) in case where there's a hash collision for distinct objects
---

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;
   }
 }