4 files changed, 19 insertions, 13 deletions
diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
index 537c783a..141060d0 100644
--- a/lib/Core/Memory.h
+++ b/lib/Core/Memory.h
@@ -71,7 +71,7 @@ public:
   MemoryObject(uint64_t _address) 
     : id(counter++),
       address(_address),
-      array(new Array("arr" + llvm::utostr(id), this, 0, id)),
+      array(new Array("arr" + llvm::utostr(id), this, id)),
       size(0),
       isFixed(true),
       allocSite(0) {
@@ -82,7 +82,7 @@ public:
                const llvm::Value *_allocSite) 
     : id(counter++),
       address(_address),
-      array(new Array("arr" + llvm::utostr(id), this, id, _size)),
+      array(new Array("arr" + llvm::utostr(id), this, _size)),
       size(_size),
       name("unnamed"),
       isLocal(_isLocal),
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index 8c18fe73..856541ee 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -517,11 +517,9 @@ DeclResult ParserImpl::ParseArrayDecl() {
   if (!RangeType.isValid())
     RangeType = 8;
 
-  // FIXME: Array should take name, not id.
   // FIXME: Array should take domain and range.
   const Identifier *Label = GetOrCreateIdentifier(Name);
-  static int counter = 0;
-  Array *Root = new Array(Label->Name, 0, ++counter, Size.get());
+  Array *Root = new Array(Label->Name, 0, Size.get());
   ArrayDecl *AD = new ArrayDecl(Label, Size.get(), 
                                 DomainType.get(), RangeType.get(), Root);
 
@@ -1300,7 +1298,7 @@ VersionResult ParserImpl::ParseVersionSpecifier() {
   VersionResult Res = ParseVersion();
   // Define update list to avoid use-of-undef errors.
   if (!Res.isValid()) {
-    Res = VersionResult(true, UpdateList(new Array("", 0, -1, 0), NULL));
+    Res = VersionResult(true, UpdateList(new Array("", 0, 0), NULL));
   }
   
   if (Label)
diff --git a/lib/Expr/Updates.cpp b/lib/Expr/Updates.cpp
index 22544820..379f1c8d 100644
--- a/lib/Expr/Updates.cpp
+++ b/lib/Expr/Updates.cpp
@@ -94,10 +94,14 @@ void UpdateList::extend(const ref<Expr> &index, const ref<Expr> &value) {
 }
 
 int UpdateList::compare(const UpdateList &b) const {
-  // use object id to increase determinism
-  if (root->id != b.root->id) 
-    return root->id < b.root->id ? -1 : 1;
-  
+  if (root->name != b.root->name)
+    return root->name < b.root->name ? -1 : 1;
+
+  // Check the root itself in case we have separate objects with the
+  // same name.
+  if (root != b.root)
+    return root < b.root ? -1 : 1;
+
   if (getSize() < b.getSize()) return -1;
   else if (getSize() > b.getSize()) return 1;    
 
@@ -111,12 +115,14 @@ int UpdateList::compare(const UpdateList &b) const {
         return res;
     }
   }
-  assert(!an && !bn);
+  assert(!an && !bn);  
   return 0;
 }
 
 unsigned UpdateList::hash() const {
-  unsigned res = root->id * Expr::MAGIC_HASH_CONSTANT;
+  unsigned res = 0;
+  for (unsigned i = 0, e = root->name.size(); i != e; ++i)
+    res = (res * Expr::MAGIC_HASH_CONSTANT) + root->name[i];
   if (head)
     res ^= head->hash();
   return res;
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 680b7d43..856540fe 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -388,8 +388,10 @@ ExprHandle STPBuilder::constructSDivByConstant(ExprHandle expr_n, unsigned width
   if (root->stpInitialArray) {
     return root->stpInitialArray;
   } else {
+    // STP uniques arrays by name, so we make sure the name is unique by
+    // including the address.
     char buf[32];
-    sprintf(buf, "arr%d", root->id);
+    sprintf(buf, "%s_%p", root->name.c_str(), (void*) root);
     root->stpInitialArray = buildArray(buf, 32, 8);
     return root->stpInitialArray;
   }