diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp
index 8700c1d5c..231c47acc 100644
--- a/src/library/blast/state.cpp
+++ b/src/library/blast/state.cpp
@@ -425,6 +425,7 @@ void state::add_deps(hypothesis & h_user, unsigned hidx_user) {
 
 double state::compute_weight(unsigned hidx, expr const & /* type */) {
     // TODO(Leo): use heuristics and machine learning for computing the weight of a new hypothesis
+    // This method should not be here.
     return 1.0 / (static_cast<double>(hidx) + 1.0);
 }
 
@@ -608,6 +609,21 @@ optional<unsigned> state::activate_hypothesis() {
     }
 }
 
+optional<unsigned> state::select_rec_hypothesis() {
+    while (true) {
+        if (m_branch.m_rec_queue.empty())
+            return optional<unsigned>();
+        unsigned hidx             = m_branch.m_rec_queue.erase_min();
+        hypothesis const * h_decl = get_hypothesis_decl(hidx);
+        if (!h_decl->is_dead())
+            return optional<unsigned>(hidx);
+    }
+}
+
+void state::add_to_rec_queue(hypothesis_idx hidx, double w) {
+    m_branch.m_rec_queue.insert(w, hidx);
+}
+
 bool state::hidx_depends_on(unsigned hidx_user, unsigned hidx_provider) const {
     if (auto s = m_branch.m_forward_deps.find(hidx_provider)) {
         return s->contains(hidx_user);
diff --git a/src/library/blast/state.h b/src/library/blast/state.h
index 019bbd112..de67a0eba 100644
--- a/src/library/blast/state.h
+++ b/src/library/blast/state.h
@@ -105,7 +105,9 @@ class branch {
     struct inv_double_cmp {
         int operator()(double const & d1, double const & d2) const { return d1 > d2 ? -1 : (d1 < d2 ? 1 : 0); }
     };
-    typedef rb_map<double, hypothesis_idx, inv_double_cmp>   todo_queue;
+    typedef rb_map<double, hypothesis_idx, inv_double_cmp>   priority_queue;
+    typedef priority_queue                                   todo_queue;
+    typedef priority_queue                                   rec_queue;
     // Hypothesis/facts in the current state
     hypothesis_decls   m_hyp_decls;
     // We break the set of hypotheses in m_hyp_decls in 4 sets that are not necessarily disjoint:
@@ -126,6 +128,7 @@ class branch {
     hypothesis_idx_set       m_assumption;
     hypothesis_idx_set       m_active;
     todo_queue               m_todo_queue;
+    rec_queue                m_rec_queue;    // priority queue for hypothesis we want to eliminate/recurse
     head_map<hypothesis_idx> m_head_to_hyps;
     forward_deps             m_forward_deps; // given an entry (h -> {h_1, ..., h_n}), we have that each h_i uses h.
     expr                     m_target;
@@ -260,6 +263,10 @@ public:
     /** \brief Activate the next hypothesis in the TODO queue, return none if the TODO queue is empty. */
     optional<hypothesis_idx> activate_hypothesis();
 
+    /** \brief Pick next hypothesis from the rec queue */
+    optional<hypothesis_idx> select_rec_hypothesis();
+    void add_to_rec_queue(hypothesis_idx hidx, double w);
+
     /** \brief Store in \c r the hypotheses in this branch sorted by dependency depth */
     void get_sorted_hypotheses(hypothesis_idx_buffer & r) const;
     /** \brief Sort hypotheses in r */