diff --git a/src/tactic/generic_model_converter.cpp b/src/tactic/generic_model_converter.cpp
index 0790c962a..a64a3a79d 100644
--- a/src/tactic/generic_model_converter.cpp
+++ b/src/tactic/generic_model_converter.cpp
@@ -33,10 +33,9 @@ generic_model_converter::~generic_model_converter() {
 
 void generic_model_converter::add(func_decl * d, expr* e) {
     VERIFY(e);
-    entry et(d, e, m, ADD);
     VERIFY(d->get_range() == m.get_sort(e));
-    m_first_idx.insert_if_not_there(et.m_f, m_entries.size());
-    m_entries.push_back(et);
+    m_first_idx.insert_if_not_there(d, m_entries.size());
+    m_entries.push_back(entry(d, e, m, ADD));
 }
 
 void generic_model_converter::operator()(model_ref & md) {
@@ -250,7 +249,6 @@ void generic_model_converter::get_units(obj_map<expr, bool>& units) {
 
  */
 expr_ref generic_model_converter::simplify_def(entry const& e) {
-    expr_ref result(m);
     expr_ref c(m.mk_const(e.m_f), m);
     if (m.is_bool(c) && occurs(c, e.m_def)) {
         expr_safe_replace rep(m);
diff --git a/src/tactic/generic_model_converter.h b/src/tactic/generic_model_converter.h
index a190b8525..c67dd5eff 100644
--- a/src/tactic/generic_model_converter.h
+++ b/src/tactic/generic_model_converter.h
@@ -30,13 +30,6 @@ class generic_model_converter : public model_converter {
         instruction   m_instruction;
         entry(func_decl* f, expr* d, ast_manager& m, instruction i):
             m_f(f, m), m_def(d, m), m_instruction(i) {}
-
-        entry& operator=(entry const& other) {
-            m_f = other.m_f;
-            m_def = other.m_def;
-            m_instruction = other.m_instruction;
-            return *this;
-        }
     };
     ast_manager& m;
     std::string  m_orig;