diff --git a/src/util/debug.cpp b/src/util/debug.cpp
index 3e40e412c..1b85fbbbb 100644
--- a/src/util/debug.cpp
+++ b/src/util/debug.cpp
@@ -56,17 +56,17 @@ void finalize_debug() {
 
 void enable_debug(const char * tag) {
     init_debug_table();
-    g_enabled_debug_tags->insert(const_cast<char *>(tag));
+    g_enabled_debug_tags->insert(tag);
 }
 
 void disable_debug(const char * tag) {
     init_debug_table();
-    g_enabled_debug_tags->erase(const_cast<char *>(tag));
+    g_enabled_debug_tags->erase(tag);
 }
 
 bool is_debug_enabled(const char * tag) {
     init_debug_table();
-    return g_enabled_debug_tags->contains(const_cast<char *>(tag));
+    return g_enabled_debug_tags->contains(tag);
 }
 
 #if !defined(_WINDOWS) && !defined(NO_Z3_DEBUGGER)
diff --git a/src/util/str_hashtable.h b/src/util/str_hashtable.h
index e12cdc7a7..111d54ac8 100644
--- a/src/util/str_hashtable.h
+++ b/src/util/str_hashtable.h
@@ -28,7 +28,7 @@ struct str_hash_proc {
     unsigned operator()(char const * s) const { return string_hash(s, static_cast<unsigned>(strlen(s)), 17); } 
 };
 struct str_eq_proc { bool operator()(char const * s1, char const * s2) const { return strcmp(s1, s2) == 0; } }; 
-typedef ptr_hashtable<char, str_hash_proc, str_eq_proc> str_hashtable;
+typedef ptr_hashtable<const char, str_hash_proc, str_eq_proc> str_hashtable;
 
 #endif /* STR_HASHTABLE_H_ */
 
diff --git a/src/util/symbol.cpp b/src/util/symbol.cpp
index 90b245e6c..3f0e7c967 100644
--- a/src/util/symbol.cpp
+++ b/src/util/symbol.cpp
@@ -35,20 +35,19 @@ class internal_symbol_table {
 public:
 
     char const * get_str(char const * d) {
-        char * result;
+        const char * result;
         #pragma omp critical (cr_symbol) 
         {
-        char * r_d = const_cast<char *>(d);
         str_hashtable::entry * e;
-        if (m_table.insert_if_not_there_core(r_d, e)) {
+        if (m_table.insert_if_not_there_core(d, e)) {
             // new entry
             size_t l   = strlen(d);
             // store the hash-code before the string
             size_t * mem = static_cast<size_t*>(m_region.allocate(l + 1 + sizeof(size_t)));
             *mem = e->get_hash();
             mem++;
-            result = reinterpret_cast<char*>(mem);
-            memcpy(result, d, l+1);
+            result = reinterpret_cast<const char*>(mem);
+            memcpy(mem, d, l+1);
             // update the entry with the new ptr.
             e->set_data(result);
         }
diff --git a/src/util/trace.cpp b/src/util/trace.cpp
index 68437ab92..e4b210021 100644
--- a/src/util/trace.cpp
+++ b/src/util/trace.cpp
@@ -38,7 +38,7 @@ void finalize_trace() {
 }
 
 void enable_trace(const char * tag) {
-    get_enabled_trace_tags().insert(const_cast<char *>(tag));
+    get_enabled_trace_tags().insert(tag);
 }
 
 void enable_all_trace(bool flag) {
@@ -46,12 +46,12 @@ void enable_all_trace(bool flag) {
 }
 
 void disable_trace(const char * tag) {
-    get_enabled_trace_tags().erase(const_cast<char *>(tag));
+    get_enabled_trace_tags().erase(tag);
 }
 
 bool is_trace_enabled(const char * tag) {
     return g_enable_all_trace_tags || 
-        (g_enabled_trace_tags && get_enabled_trace_tags().contains(const_cast<char *>(tag)));
+        (g_enabled_trace_tags && get_enabled_trace_tags().contains(tag));
 }
 
 void close_trace() {