diff --git a/src/ast/converters/generic_model_converter.h b/src/ast/converters/generic_model_converter.h
index 18ec16fe0..88c70bef0 100644
--- a/src/ast/converters/generic_model_converter.h
+++ b/src/ast/converters/generic_model_converter.h
@@ -54,8 +54,6 @@ public:
     
     void operator()(model_ref & md) override;
 
-    void operator()(expr_ref& fml) override { UNREACHABLE(); }
-
     void cancel() override {}
 
     void display(std::ostream & out) override;
diff --git a/src/ast/converters/model_converter.cpp b/src/ast/converters/model_converter.cpp
index c309bbb79..af6b44767 100644
--- a/src/ast/converters/model_converter.cpp
+++ b/src/ast/converters/model_converter.cpp
@@ -93,11 +93,6 @@ public:
         this->m_c1->operator()(m);
     }
 
-    void operator()(expr_ref & fml) override {
-        this->m_c2->operator()(fml);
-        this->m_c1->operator()(fml);
-    }
-    
     void operator()(labels_vec & r) override {
         this->m_c2->operator()(r);
         this->m_c1->operator()(r);
@@ -157,11 +152,6 @@ public:
         r.append(m_labels.size(), m_labels.data());
     }
 
-    void operator()(expr_ref& fml) override {
-        model::scoped_model_completion _scm(m_model, false);
-        fml = (*m_model)(fml);
-    }
-
     void get_units(obj_map<expr, bool>& fmls) override {
         // no-op
     }
diff --git a/src/ast/converters/model_converter.h b/src/ast/converters/model_converter.h
index baf5e422d..970de7378 100644
--- a/src/ast/converters/model_converter.h
+++ b/src/ast/converters/model_converter.h
@@ -76,8 +76,6 @@ public:
     virtual void operator()(model_ref & m) = 0;
 
     virtual void operator()(labels_vec & r) {}
-
-    virtual void operator()(expr_ref& fml) { UNREACHABLE(); }
     
     virtual model_converter * translate(ast_translation & translator) = 0;
     
diff --git a/src/sat/tactic/sat2goal.cpp b/src/sat/tactic/sat2goal.cpp
index 7d9c5f4b3..c1835f839 100644
--- a/src/sat/tactic/sat2goal.cpp
+++ b/src/sat/tactic/sat2goal.cpp
@@ -59,7 +59,8 @@ void sat2goal::mc::flush_smc(sat::solver& s, atom2bool_var const& map) {
 void sat2goal::mc::flush_gmc() {
     sat::literal_vector updates;
     m_smc.expand(updates);    
-    if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal");
+    if (!m_gmc) 
+        m_gmc = alloc(generic_model_converter, m, "sat2goal");
     // now gmc owns the model converter
     sat::literal_vector clause;
     expr_ref_vector tail(m);
@@ -124,16 +125,13 @@ void sat2goal::mc::set_env(ast_pp_util* visitor) {
 }
 
 void sat2goal::mc::display(std::ostream& out) {
-    flush_gmc();
     if (m_gmc) m_gmc->display(out);
 }
 
 void sat2goal::mc::get_units(obj_map<expr, bool>& units) {
-    flush_gmc();
     if (m_gmc) m_gmc->get_units(units);
 }
 
-
 void sat2goal::mc::operator()(sat::model& md) {
     m_smc(md);
 }
@@ -145,12 +143,6 @@ void sat2goal::mc::operator()(model_ref & md) {
     CTRACE(sat_mc, m_gmc, m_gmc->display(tout << "after sat_mc\n"); model_v2_pp(tout, *md););
 }
 
-
-void sat2goal::mc::operator()(expr_ref& fml) {
-    flush_gmc();
-    if (m_gmc) (*m_gmc)(fml);
-}
-
 void sat2goal::mc::insert(sat::bool_var v, expr * atom, bool aux) {
     SASSERT(!m_var2expr.get(v, nullptr));
     m_var2expr.reserve(v + 1);
diff --git a/src/sat/tactic/sat2goal.h b/src/sat/tactic/sat2goal.h
index 97a85ff65..fe0e057ae 100644
--- a/src/sat/tactic/sat2goal.h
+++ b/src/sat/tactic/sat2goal.h
@@ -56,7 +56,6 @@ public:
         using model_converter::operator();
         void operator()(sat::model& m);
         void operator()(model_ref& md) override;
-        void operator()(expr_ref& fml) override; 
         model_converter* translate(ast_translation& translator) override;
         void set_env(ast_pp_util* visitor) override;
         void display(std::ostream& out) override;
diff --git a/src/tactic/bv/bit_blaster_model_converter.cpp b/src/tactic/bv/bit_blaster_model_converter.cpp
index 4fbad22dc..50cb63465 100644
--- a/src/tactic/bv/bit_blaster_model_converter.cpp
+++ b/src/tactic/bv/bit_blaster_model_converter.cpp
@@ -191,24 +191,6 @@ struct bit_blaster_model_converter : public model_converter {
         mk_bvs(md.get(), new_model);
         md = new_model;
     }
-
-    /**
-       \brief simplisic expansion operator for formulas.
-       It just adds back bit-vector definitions to the formula whether they are used or not.
-
-     */
-    void operator()(expr_ref& fml) override {
-        unsigned sz = m_vars.size();
-        if (sz == 0) return;
-        expr_ref_vector fmls(m());
-        fmls.push_back(fml);
-        for (unsigned i = 0; i < sz; i++) {
-            fmls.push_back(m().mk_eq(m().mk_const(m_vars.get(i)), m_bits.get(i)));
-        }        
-        m_vars.reset();
-        m_bits.reset();
-        fml = mk_and(fmls);
-    }
     
     void display(std::ostream & out) override {
         for (func_decl * f : m_newbits)