diff --git a/src/crab/fwd_analyzer.cpp b/src/crab/fwd_analyzer.cpp
index 268f7e158..72fbbb42c 100644
--- a/src/crab/fwd_analyzer.cpp
+++ b/src/crab/fwd_analyzer.cpp
@@ -13,43 +13,9 @@
 
 namespace crab {
 
-// Simple visitor to check if node is a member of the wto component.
-class member_component_visitor final {
-    label_t _node;
-    bool _found;
-
-  public:
-    explicit member_component_visitor(const label_t& node) : _node(node), _found(false) {}
-
-    void operator()(const label_t& vertex) {
-        if (!_found) {
-            _found = (vertex == _node);
-        }
-    }
-
-    void operator()(const std::shared_ptr<wto_cycle_t>& c) {
-        if (!_found) {
-            _found = (c->head() == _node);
-            if (!_found) {
-                for (const auto& component : *c) {
-                    if (_found) {
-                        break;
-                    }
-                    std::visit(*this, component);
-                }
-            }
-        }
-    }
-
-    [[nodiscard]]
-    bool is_member() const {
-        return _found;
-    }
-};
-
 class interleaved_fwd_fixpoint_iterator_t final {
     const cfg_t& _cfg;
-    wto_t _wto;
+    const wto_t _wto;
     invariant_table_t _inv;
 
     /// number of narrowing iterations. If the narrowing operator is
@@ -62,12 +28,11 @@ class interleaved_fwd_fixpoint_iterator_t final {
     /// Used to skip the analysis until _entry is found
     bool _skip{true};
 
-  private:
     void set_pre(const label_t& label, const ebpf_domain_t& v) { _inv.at(label).pre = v; }
 
-    ebpf_domain_t get_pre(const label_t& node) { return _inv.at(node).pre; }
+    ebpf_domain_t get_pre(const label_t& node) const { return _inv.at(node).pre; }
 
-    ebpf_domain_t get_post(const label_t& node) { return _inv.at(node).post; }
+    ebpf_domain_t get_post(const label_t& node) const { return _inv.at(node).post; }
 
     void transform_to_post(const label_t& label, ebpf_domain_t pre) {
         const GuardedInstruction& ins = _cfg.at(label);
@@ -83,27 +48,7 @@ class interleaved_fwd_fixpoint_iterator_t final {
         _inv.at(label).post = std::move(pre);
     }
 
-    [[nodiscard]]
-    static ebpf_domain_t extrapolate(const ebpf_domain_t& before, const ebpf_domain_t& after,
-                                     const unsigned int iteration) {
-        /// number of iterations until triggering widening
-        constexpr auto _widening_delay = 2;
-
-        if (iteration < _widening_delay) {
-            return before | after;
-        }
-        return before.widen(after, iteration == _widening_delay);
-    }
-
-    static ebpf_domain_t refine(const ebpf_domain_t& before, const ebpf_domain_t& after, const unsigned int iteration) {
-        if (iteration == 1) {
-            return before & after;
-        } else {
-            return before.narrow(after);
-        }
-    }
-
-    ebpf_domain_t join_all_prevs(const label_t& node) {
+    ebpf_domain_t join_all_prevs(const label_t& node) const {
         if (node == _cfg.entry_label()) {
             return get_pre(node);
         }
@@ -114,13 +59,13 @@ class interleaved_fwd_fixpoint_iterator_t final {
         return res;
     }
 
-  public:
     explicit interleaved_fwd_fixpoint_iterator_t(const cfg_t& cfg) : _cfg(cfg), _wto(cfg) {
         for (const auto& label : _cfg.labels()) {
             _inv.emplace(label, invariant_map_pair{ebpf_domain_t::bottom(), ebpf_domain_t::bottom()});
         }
     }
 
+  public:
     void operator()(const label_t& node);
 
     void operator()(const std::shared_ptr<wto_cycle_t>& cycle);
@@ -146,6 +91,25 @@ invariant_table_t run_forward_analyzer(const cfg_t& cfg, ebpf_domain_t entry_inv
     return std::move(analyzer._inv);
 }
 
+static ebpf_domain_t extrapolate(const ebpf_domain_t& before, const ebpf_domain_t& after,
+                                 const unsigned int iteration) {
+    /// number of iterations until triggering widening
+    constexpr auto _widening_delay = 2;
+
+    if (iteration < _widening_delay) {
+        return before | after;
+    }
+    return before.widen(after, iteration == _widening_delay);
+}
+
+static ebpf_domain_t refine(const ebpf_domain_t& before, const ebpf_domain_t& after, const unsigned int iteration) {
+    if (iteration == 1) {
+        return before & after;
+    } else {
+        return before.narrow(after);
+    }
+}
+
 void interleaved_fwd_fixpoint_iterator_t::operator()(const label_t& node) {
     /** decide whether skip vertex or not **/
     if (_skip && node == _cfg.entry_label()) {
@@ -167,11 +131,9 @@ void interleaved_fwd_fixpoint_iterator_t::operator()(const std::shared_ptr<wto_c
     /** decide whether to skip cycle or not **/
     bool entry_in_this_cycle = false;
     if (_skip) {
-        // We only skip the analysis of cycle if _entry is not a
+        // We only skip the analysis of cycle if entry_label is not a
         // component of it, included nested components.
-        member_component_visitor vis(_cfg.entry_label());
-        vis(cycle);
-        entry_in_this_cycle = vis.is_member();
+        entry_in_this_cycle = is_component_member(_cfg.entry_label(), cycle);
         _skip = !entry_in_this_cycle;
         if (_skip) {
             return;
diff --git a/src/crab/wto.cpp b/src/crab/wto.cpp
index 4dc3e2018..fdf87e4d3 100644
--- a/src/crab/wto.cpp
+++ b/src/crab/wto.cpp
@@ -10,6 +10,22 @@
 // where _visit_stack is roughly equivalent to a stack trace in the recursive algorithm.
 // However, this scales much higher since it does not run out of stack memory.
 
+bool is_component_member(const label_t& label, const cycle_or_label& component) {
+    if (const auto plabel = std::get_if<label_t>(&component)) {
+        return *plabel == label;
+    }
+    const auto cycle = std::get<std::shared_ptr<wto_cycle_t>>(component);
+    if (cycle->head() == label) {
+        return true;
+    }
+    for (const auto& sub_component : *cycle) {
+        if (is_component_member(label, sub_component)) {
+            return true;
+        }
+    }
+    return false;
+}
+
 bool wto_nesting_t::operator>(const wto_nesting_t& nesting) const {
     const size_t this_size = this->_heads.size();
     const size_t other_size = nesting._heads.size();
@@ -249,7 +265,7 @@ std::ostream& operator<<(std::ostream& o, const wto_t& wto) {
 // is itself a head of a component, we want the head of whatever
 // contains that entire component.  Returns nullopt if the label is
 // not nested, i.e., the head is logically the entry point of the CFG.
-std::optional<label_t> wto_t::head(const label_t& label) {
+std::optional<label_t> wto_t::head(const label_t& label) const {
     const auto it = _containing_cycle.find(label);
     if (it == _containing_cycle.end()) {
         // Label is not in any cycle.
@@ -273,7 +289,7 @@ std::optional<label_t> wto_t::head(const label_t& label) {
 
 wto_t::wto_t(const cfg_t& cfg) : wto_t{std::move(wto_builder_t(cfg).wto)} {}
 
-std::vector<label_t> wto_t::collect_heads(const label_t& label) {
+std::vector<label_t> wto_t::collect_heads(const label_t& label) const {
     std::vector<label_t> heads;
     for (auto h = head(label); h; h = head(*h)) {
         heads.push_back(*h);
@@ -283,7 +299,7 @@ std::vector<label_t> wto_t::collect_heads(const label_t& label) {
 
 // Compute the set of heads of the nested components containing a given label.
 // See section 3.1 of the paper for discussion, which uses the notation w(c).
-const wto_nesting_t& wto_t::nesting(const label_t& label) {
+const wto_nesting_t& wto_t::nesting(const label_t& label) const {
     if (!_nesting.contains(label)) {
         // Not found in the cache yet, so construct the list of heads of the
         // nested components containing the label, stored in reverse order.
diff --git a/src/crab/wto.hpp b/src/crab/wto.hpp
index 33bb7e908..f825ad97f 100644
--- a/src/crab/wto.hpp
+++ b/src/crab/wto.hpp
@@ -92,6 +92,9 @@ class wto_cycle_t final {
     }
 };
 
+// Check if node is a member of the wto component.
+bool is_component_member(const label_t& label, const cycle_or_label& component);
+
 class wto_t final {
     // Top level components, in reverse order.
     wto_partition_t _components;
@@ -102,10 +105,10 @@ class wto_t final {
     // Table mapping label to the list of heads of cycles containing the label.
     // This is an on-demand cache, since for most vertices the nesting is never
     // looked at so we only create a wto_nesting_t for cases we actually need it.
-    std::map<label_t, wto_nesting_t> _nesting;
+    mutable std::map<label_t, wto_nesting_t> _nesting;
 
-    std::vector<label_t> collect_heads(const label_t& label);
-    std::optional<label_t> head(const label_t& label);
+    std::vector<label_t> collect_heads(const label_t& label) const;
+    std::optional<label_t> head(const label_t& label) const;
 
     wto_t() = default;
     friend class wto_builder_t;
@@ -124,7 +127,7 @@ class wto_t final {
     }
 
     friend std::ostream& operator<<(std::ostream& o, const wto_t& wto);
-    const wto_nesting_t& nesting(const label_t& label);
+    const wto_nesting_t& nesting(const label_t& label) const;
 
     /**
      * Visit the heads of all loops in the WTO.