diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 6d075ebcd..7409b5851 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -251,11 +251,11 @@ namespace {
             return const_cast<smt::kernel&>(m_context).get_context().get_num_bool_vars();
         }
 
-        unsigned get_bool_var(expr* e) const override {
+        sat::bool_var get_bool_var(expr* e) const override {
             auto& ctx = const_cast<smt::kernel&>(m_context).get_context();
             expr* atom = e;
             get_manager().is_not(e, atom);
-            return ctx.b_internalized(atom) ? ctx.get_bool_var(atom) : UINT_MAX;
+            return ctx.b_internalized(atom) ? ctx.get_bool_var(atom) : sat::null_bool_var;
         }
 
         void pop_to_base_level() override {
@@ -450,9 +450,9 @@ namespace {
             ast_manager& m = get_manager();
             if (!get_params().get_bool("cube.lookahead", false)) {
                 auto& ctx = m_context.get_context();
-                obj_hashtable<expr> selected_vars;
+                expr_mark selected_vars;
                 for (expr* v : vars)
-                    selected_vars.insert(v);
+                    selected_vars.mark(v);
                 expr_ref_vector candidates(m);
                 expr_ref result(m);
                 double score = 0.0;
@@ -465,7 +465,7 @@ namespace {
                     expr* e = ctx.bool_var2expr(v);
                     if (!e)
                         continue;
-                    if (!selected_vars.empty() && !selected_vars.contains(e))
+                    if (!vars.empty() && !selected_vars.is_marked(e))
                         continue;
                     candidates.push_back(e);
                     double new_score = ctx.get_activity(v);
diff --git a/src/solver/solver.h b/src/solver/solver.h
index f1de41880..73a83a6dd 100644
--- a/src/solver/solver.h
+++ b/src/solver/solver.h
@@ -22,6 +22,7 @@ Notes:
 #include "solver/check_sat_result.h"
 #include "solver/progress_callback.h"
 #include "util/params.h"
+#include "util/sat_literal.h"
 
 class solver;
 class model_converter;
@@ -309,11 +310,11 @@ public:
     virtual unsigned get_assign_level(expr* e) const { return UINT_MAX; }
     virtual bool is_relevant(expr* e) const { return true; }
     virtual unsigned get_num_bool_vars() const { return UINT_MAX; }
-    virtual unsigned get_bool_var(expr* e) const { return UINT_MAX; }
-    virtual expr* bool_var2expr(unsigned) const { return nullptr; }
-    virtual lbool get_assignment(unsigned) const { return l_undef; }
-    virtual double get_activity(unsigned) const { return 0.0; }
-    virtual bool was_eliminated(unsigned) const { return false; }
+    virtual sat::bool_var get_bool_var(expr* e) const { return sat::null_bool_var; }
+    virtual expr* bool_var2expr(sat::bool_var) const { return nullptr; }
+    virtual lbool get_assignment(sat::bool_var) const { return l_undef; }
+    virtual double get_activity(sat::bool_var) const { return 0.0; }
+    virtual bool was_eliminated(sat::bool_var) const { return false; }
 
     virtual void pop_to_base_level() {}