diff --git a/src/util/map.h b/src/util/map.h index 849c3d24a..e45881fff 100644 --- a/src/util/map.h +++ b/src/util/map.h @@ -115,7 +115,7 @@ public: } entry * find_core(key const & k) const { - return m_table.find_core(key_data{k, value{}}); + return m_table.find_core(key_data{k, value{}}); } bool find(key const & k, value & v) const { @@ -164,7 +164,7 @@ public: void remove(key const & k) { m_table.remove(key_data{k, value{}}); } - + void erase(key const & k) { remove(k); } @@ -184,7 +184,7 @@ public: } return true; } - + #ifdef Z3DEBUG bool check_invariant() { diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h index e158d09cb..3465c91fc 100644 --- a/src/util/obj_hashtable.h +++ b/src/util/obj_hashtable.h @@ -161,8 +161,8 @@ public: obj_map_entry * insert_if_not_there3(Key * k, Value const & v) { return m_table.insert_if_not_there2({k, v}); } - - obj_map_entry *find_core(Key * k) const { + + obj_map_entry * find_core(Key * k) const { return m_table.find_core({k}); } @@ -193,8 +193,8 @@ public: value & operator[](key * k) { return find(k); } - - iterator find_iterator(Key * k) const { + + iterator find_iterator(Key * k) const { return m_table.find(key_data{k}); } @@ -203,7 +203,7 @@ public: } void remove(Key * k) { - m_table.remove(key_data{k, value()}); + m_table.remove(key_data{k, value{}}); } void erase(Key * k) { diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h index 59301f4b2..47026e4eb 100644 --- a/src/util/symbol_table.h +++ b/src/util/symbol_table.h @@ -121,7 +121,7 @@ public: return true; } - bool contains(symbol key) const { + bool contains(symbol key) const { return m_sym_table.contains(key_data{key}); }