diff --git a/src/muz/spacer/spacer_iuc_solver.h b/src/muz/spacer/spacer_iuc_solver.h
index 9b50b4c4e..c3561a6d4 100644
--- a/src/muz/spacer/spacer_iuc_solver.h
+++ b/src/muz/spacer/spacer_iuc_solver.h
@@ -124,7 +124,6 @@ public:
     expr_ref_vector cube(expr_ref_vector&, unsigned) override { return expr_ref_vector(m); }
     void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override { m_solver.get_levels(vars, depth); }
     expr_ref_vector get_trail() override { return m_solver.get_trail(); }
-    void set_activity(expr* lit, double act) override { m_solver.set_activity(lit, act); }
 
     void push() override;
     void pop(unsigned n) override;
diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h
index be71376ac..9eda063e9 100644
--- a/src/opt/opt_solver.h
+++ b/src/opt/opt_solver.h
@@ -110,7 +110,6 @@ namespace opt {
         lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores) override;
         void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override; 
         expr_ref_vector get_trail() override { return m_context.get_trail(); }
-        void set_activity(expr* lit, double act) override { m_context.set_activity(lit, act); }
         expr_ref_vector cube(expr_ref_vector&, unsigned) override { return expr_ref_vector(m); }
 
         void set_logic(symbol const& logic);
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index bd8a19044..4e87bda95 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -336,16 +336,6 @@ public:
         return result;
     }
 
-    void set_activity(expr* var, double activity) override {
-        m.is_not(var, var);
-        sat::bool_var v = m_map.to_bool_var(var);
-        if (v == sat::null_bool_var) {
-            v = m_solver.add_var(true);
-            m_map.insert(var, v);
-        }
-        m_solver.set_activity(v, static_cast<unsigned>(activity));
-    }
-
     proof * get_proof() override {
         UNREACHABLE();
         return nullptr;
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 578b4266c..8c9510055 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -203,10 +203,6 @@ namespace smt {
             return m_context.get_trail();
         }
 
-        void set_activity(expr* lit, double activity) override {
-            m_context.set_activity(lit, activity);
-        }
-
         struct scoped_minimize_core {
             smt_solver& s;
             expr_ref_vector m_assumptions;
diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index b939efc6b..b602fe6e1 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -328,11 +328,6 @@ public:
             return m_solver2->get_trail();
     }
 
-    void set_activity(expr* lit, double activity) override {
-        m_solver1->set_activity(lit, activity);
-        m_solver2->set_activity(lit, activity);
-    }
-
     proof * get_proof() override {
         if (m_use_solver1_results)
             return m_solver1->get_proof();
diff --git a/src/solver/solver.h b/src/solver/solver.h
index be3751bcd..0c509b8c7 100644
--- a/src/solver/solver.h
+++ b/src/solver/solver.h
@@ -251,8 +251,6 @@ public:
     
     virtual void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) = 0;
 
-    virtual void set_activity(expr* lit, double activity) = 0;
-
     class scoped_push {
         solver& s;
         bool    m_nopop;
diff --git a/src/solver/solver_pool.cpp b/src/solver/solver_pool.cpp
index 4d6724aa7..7f3882447 100644
--- a/src/solver/solver_pool.cpp
+++ b/src/solver/solver_pool.cpp
@@ -127,10 +127,6 @@ public:
         return m_base->get_trail();
     }
 
-    void set_activity(expr* var, double activity) override {
-        m_base->set_activity(var, activity);
-    }
-
     lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override {
         SASSERT(!m_pushed || get_scope_level() > 0);
         m_proof.reset();
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index 06cdac71a..0090cc3b0 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -93,10 +93,6 @@ public:
         throw default_exception("cannot retrieve trail from solvers created using tactcis");
     }
 
-    void set_activity(expr* var, double activity) override {
-        throw default_exception("cannot set activity for solvers created using tactcis");
-    }
-
 
 };
 
diff --git a/src/tactic/fd_solver/bounded_int2bv_solver.cpp b/src/tactic/fd_solver/bounded_int2bv_solver.cpp
index 0decaec82..bfeb48d8b 100644
--- a/src/tactic/fd_solver/bounded_int2bv_solver.cpp
+++ b/src/tactic/fd_solver/bounded_int2bv_solver.cpp
@@ -161,9 +161,6 @@ public:
     expr_ref_vector get_trail() override {
         return m_solver->get_trail();
     }
-    void set_activity(expr* var, double activity) override {
-        m_solver->set_activity(var, activity);
-    }
 
     model_converter* external_model_converter() const {
         return concat(mc0(), local_model_converter());
diff --git a/src/tactic/fd_solver/enum2bv_solver.cpp b/src/tactic/fd_solver/enum2bv_solver.cpp
index b232d8ea3..d8119ddfd 100644
--- a/src/tactic/fd_solver/enum2bv_solver.cpp
+++ b/src/tactic/fd_solver/enum2bv_solver.cpp
@@ -186,10 +186,6 @@ public:
         return m_solver->get_trail();
     }
 
-    void set_activity(expr* var, double activity) override {
-        m_solver->set_activity(var, activity);
-    }
-
     unsigned get_num_assertions() const override {
         return m_solver->get_num_assertions();
     }
diff --git a/src/tactic/fd_solver/pb2bv_solver.cpp b/src/tactic/fd_solver/pb2bv_solver.cpp
index c6866ecf4..9e17dd711 100644
--- a/src/tactic/fd_solver/pb2bv_solver.cpp
+++ b/src/tactic/fd_solver/pb2bv_solver.cpp
@@ -105,10 +105,6 @@ public:
         return m_solver->get_trail();
     }
 
-    void set_activity(expr* var, double activity) override {
-        m_solver->set_activity(var, activity);
-    }
-
     model_converter* external_model_converter() const{
         return concat(mc0(), local_model_converter());
     }