diff --git a/src/smt/smt_case_split_queue.cpp b/src/smt/smt_case_split_queue.cpp
index 67f370da0..6cdfed7ea 100644
--- a/src/smt/smt_case_split_queue.cpp
+++ b/src/smt/smt_case_split_queue.cpp
@@ -1112,119 +1112,6 @@ namespace smt {
         }
     };
 
-  /*
-    class theory_aware_branching_queue : public case_split_queue {
-    protected:
-        context & m_context;
-        smt_params & m_params;
-
-        theory_var_priority_map m_theory_var_priority;
-        theory_aware_act_queue m_theory_queue;
-        case_split_queue * m_base_queue;
-        int_hashtable<int_hash, default_eq<bool_var> > m_theory_vars;
-        map<bool_var, lbool, int_hash, default_eq<bool_var> > m_theory_var_phase;
-    public:
-        theory_aware_branching_queue(context & ctx, smt_params & p, case_split_queue * base_queue) :
-            m_context(ctx),
-            m_params(p),
-            m_theory_var_priority(),
-            m_theory_queue(1024, theory_aware_act_lt(m_theory_var_priority)),
-            m_base_queue(base_queue) {
-        }
-
-        virtual void activity_increased_eh(bool_var v) {
-            m_base_queue->activity_increased_eh(v);
-        }
-
-        virtual void mk_var_eh(bool_var v) {
-            // do nothing. we only "react" if/when we learn this is an important theory literal
-            m_base_queue->mk_var_eh(v);
-        }
-
-        virtual void del_var_eh(bool_var v) {
-            if (m_theory_queue.contains(v)) {
-                m_theory_queue.erase(v);
-            }
-            m_base_queue->del_var_eh(v);
-        }
-
-        virtual void assign_lit_eh(literal l) {
-            m_base_queue->assign_lit_eh(l);
-        }
-
-        virtual void unassign_var_eh(bool_var v) {
-            if (m_theory_vars.contains(v) && !m_theory_queue.contains(v)) {
-                m_theory_queue.insert(v);
-            }
-            m_base_queue->unassign_var_eh(v);
-        }
-
-        virtual void relevant_eh(expr * n) {
-            m_base_queue->relevant_eh(n);
-        }
-
-        virtual void init_search_eh() {
-            m_base_queue->init_search_eh();
-        }
-
-        virtual void end_search_eh() {
-            m_base_queue->end_search_eh();
-        }
-
-        virtual void internalize_instance_eh(expr * e, unsigned gen) {
-            m_base_queue->internalize_instance_eh(e, gen);
-        }
-
-        virtual void reset() {
-            m_theory_queue.reset();
-            m_theory_vars.reset();
-            m_theory_var_phase.reset();
-            m_theory_var_priority.reset();
-            m_base_queue->reset();
-        }
-
-        virtual void push_scope() {
-            m_base_queue->push_scope();
-        }
-
-        virtual void pop_scope(unsigned num_scopes) {
-            m_base_queue->pop_scope(num_scopes);
-        }
-
-        virtual void next_case_split(bool_var & next, lbool & phase) {
-            while (!m_theory_queue.empty()) {
-                next = m_theory_queue.erase_min();
-                // if this literal is unassigned, it is the theory literal with the highest priority,
-                // so case split on this
-                if (m_context.get_assignment(next) == l_undef) {
-                    TRACE("theory_aware_branching", tout << "Theory-aware branch on l#" << next << std::endl;);
-                    if (!m_theory_var_phase.find(next, phase)) {
-                        phase = l_undef;
-                    }
-                    return;
-                }
-            }
-            // if we reach this point, the theory literal queue is empty,
-            // so fall back to the base queue
-            m_base_queue->next_case_split(next, phase);
-        }
-
-        virtual void add_theory_aware_branching_info(bool_var v, double priority, lbool phase) {
-            TRACE("theory_aware_branching", tout << "Add theory-aware branching information for l#" << v << ": priority=" << priority << std::endl;);
-            m_theory_vars.insert(v);
-            m_theory_var_phase.insert(v, phase);
-            m_theory_var_priority.insert(v, priority);
-            m_theory_queue.reserve(v+1);
-            m_theory_queue.insert(v);
-        }
-
-        virtual void display(std::ostream & out) {
-            // TODO
-            m_base_queue->display(out);
-        }
-    };
-  */
-
     class theory_aware_branching_queue : public case_split_queue {
     protected:
         context &          m_context;