diff -r f53ea4c8621c -r e984cfdf3b10 util/symtable.cc
--- a/util/symtable.cc	Sat Nov 29 12:10:34 2014 +0000
+++ b/util/symtable.cc	Sat Nov 29 13:43:20 2014 +0000
@@ -116,12 +116,13 @@
   }
 
   // std::cout << "store_identifier(" << identifier_str << "): \n";
+  iterator i = _base.find(identifier_str);
+  if ((i != _base.end()) && (i->second != new_value)) {ERROR;}  /* error inserting new identifier: identifier already in map associated to a different value */
+  if ((i != _base.end()) && (i->second == new_value)) {return;} /* identifier already in map associated with the same value */
+
   std::pair<const char *, value_t> new_element(identifier_str, new_value);
   std::pair<iterator, bool> res = _base.insert(new_element);
-  if (!res.second)
-    /* error inserting new identifier... */
-    /* identifier already in map?        */
-    ERROR;
+  if (!res.second) {ERROR;} /* unknown error inserting new identifier */
 }
 
 template<typename value_type, value_type null_value>