diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index e9aeaddbb..e29a7bcc2 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -353,8 +353,10 @@ namespace sat {
         void init_visited(unsigned lim = 1) { m_visited.init_visited(2 * num_vars(), lim); }
         bool is_visited(sat::bool_var v) const { return is_visited(literal(v, false)); }
         bool is_visited(literal lit) const { return m_visited.is_visited(lit.index()); }
+        unsigned num_visited(bool_var v) const { return m_visited.num_visited(v); }
         void mark_visited(literal lit) { m_visited.mark_visited(lit.index()); }
         void mark_visited(bool_var v) { mark_visited(literal(v, false)); }
+        void inc_visited(bool_var v) { m_visited.inc_visited(v); }
         bool all_distinct(literal_vector const& lits);
         bool all_distinct(clause const& cl);
 
diff --git a/src/util/visit_helper.h b/src/util/visit_helper.h
index a11d7bdc6..5f4591828 100644
--- a/src/util/visit_helper.h
+++ b/src/util/visit_helper.h
@@ -45,5 +45,5 @@ public:
         m_visited[v] = std::min(m_visited_end, std::max(m_visited_begin, m_visited[v]) + 1);
     }
     bool is_visited(unsigned v) const { return m_visited[v] > m_visited_begin; }
-    unsigned num_visited(unsigned v) { return std::max(m_visited_begin, m_visited[v]) - m_visited_begin; }
-};
\ No newline at end of file
+    unsigned num_visited(unsigned v) const { return std::max(m_visited_begin, m_visited[v]) - m_visited_begin; }
+};