diff --git a/src/asm_cfg.cpp b/src/asm_cfg.cpp
index a9303e78a..337003323 100644
--- a/src/asm_cfg.cpp
+++ b/src/asm_cfg.cpp
@@ -281,7 +281,7 @@ std::set<basic_block_t> basic_block_t::collect_basic_blocks(const cfg_t& cfg, co
             const value_t& next_value = cfg.get_child(bb.last_label());
             const label_t& next_label = next_value.label();
 
-            if (next_label == bb.first_label() || next_label == cfg.exit_label() || next_value.in_degree() != 1) {
+            if (seen.contains(next_label) || next_label == cfg.exit_label() || next_value.in_degree() != 1) {
                 break;
             }
 
diff --git a/src/asm_ostream.cpp b/src/asm_ostream.cpp
index d54a4a040..e0f588a61 100644
--- a/src/asm_ostream.cpp
+++ b/src/asm_ostream.cpp
@@ -8,10 +8,12 @@
 
 #include "asm_syntax.hpp"
 #include "crab/cfg.hpp"
+#include "crab/fwd_analyzer.hpp"
 #include "crab/interval.hpp"
 #include "crab/type_encoding.hpp"
 #include "crab/variable.hpp"
 #include "crab_utils/num_big.hpp"
+#include "crab_verifier.hpp"
 #include "helpers.hpp"
 #include "platform.hpp"
 #include "spec_type_descriptors.hpp"
@@ -21,6 +23,23 @@ using std::optional;
 using std::string;
 using std::vector;
 
+struct LineInfoPrinter {
+    std::ostream& os;
+    std::string previous_source_line;
+
+    void print_line_info(const label_t& label) {
+        if (thread_local_options.verbosity_opts.print_line_info) {
+            const auto& line_info_map = thread_local_program_info.get().line_info;
+            const auto& line_info = line_info_map.find(label.from);
+            // Print line info only once.
+            if (line_info != line_info_map.end() && line_info->second.source_line != previous_source_line) {
+                os << "\n" << line_info->second << "\n";
+                previous_source_line = line_info->second.source_line;
+            }
+        }
+    }
+};
+
 namespace crab {
 
 std::string number_t::to_string() const { return _n.str(); }
@@ -134,23 +153,61 @@ void print_from(std::ostream& o, const value_t& value) {
     o << "\n";
 }
 
-std::ostream& operator<<(std::ostream& o, const cfg_t& cfg) {
-    for (const label_t& label : cfg.sorted_labels()) {
-        const auto& value = cfg.get_node(label);
-        print_label(o, value);
-        print_assertions(o, value);
-        print_instruction(o, value);
-        o << "edges to:";
-        for (const label_t& next_label : cfg.next_nodes(label)) {
-            o << " " << next_label;
+static void print_cfg(std::ostream& os, const cfg_t& cfg, const bool simplify, const invariant_table_t* invariants) {
+    LineInfoPrinter printer{os};
+    for (const auto& bb : basic_block_t::collect_basic_blocks(cfg, simplify)) {
+        if (invariants) {
+            os << "\nPre-invariant : " << invariants->at(bb.first_label()).pre << "\n";
+        }
+        const value_t& first_node = cfg.get_node(bb.first_label());
+        print_from(os, first_node);
+        print_label(os, first_node);
+        for (const label_t& label : bb) {
+            printer.print_line_info(label);
+            const value_t& node = cfg.get_node(label);
+            print_assertions(os, node);
+            print_instruction(os, node);
+        }
+        print_goto(os, cfg.get_node(bb.last_label()));
+        if (invariants) {
+            os << "\nPost-invariant: " << invariants->at(bb.last_label()).post << "\n";
         }
-        o << "\n";
     }
-    return o;
+    os << "\n";
 }
+void print_cfg(std::ostream& os, const cfg_t& cfg, const bool simplify) { print_cfg(os, cfg, simplify, nullptr); }
 
 } // namespace crab
 
+void print_reachability(std::ostream& os, const Report& report) {
+    for (const auto& [label, notes] : report.reachability) {
+        for (const auto& msg : notes) {
+            os << label << ": " << msg << "\n";
+        }
+    }
+    os << "\n";
+}
+
+void print_warnings(std::ostream& os, const Report& report) {
+    LineInfoPrinter printer{os};
+    for (const auto& [label, warnings] : report.warnings) {
+        for (const auto& msg : warnings) {
+            printer.print_line_info(label);
+            os << label << ": " << msg << "\n";
+        }
+    }
+    os << "\n";
+}
+
+void print_all_messages(std::ostream& os, const Report& report) {
+    print_reachability(os, report);
+    print_warnings(os, report);
+}
+
+void print_invariants(std::ostream& os, const cfg_t& cfg, const bool simplify, const Invariants& invariants) {
+    print_cfg(os, cfg, simplify, &invariants.invariants);
+}
+
 namespace asm_syntax {
 std::ostream& operator<<(std::ostream& os, const ArgSingle::Kind kind) {
     switch (kind) {
diff --git a/src/crab/cfg.hpp b/src/crab/cfg.hpp
index 538a2ec7f..8072bcf0e 100644
--- a/src/crab/cfg.hpp
+++ b/src/crab/cfg.hpp
@@ -419,7 +419,7 @@ class basic_block_t final {
 void print_dot(const cfg_t& cfg, std::ostream& out);
 void print_dot(const cfg_t& cfg, const std::string& outfile);
 
-std::ostream& operator<<(std::ostream& o, const cfg_t& cfg);
+void print_cfg(std::ostream& os, const cfg_t& cfg, bool simplify);
 
 } // end namespace crab
 
diff --git a/src/crab_verifier.cpp b/src/crab_verifier.cpp
index 1f3585b25..049c091c8 100644
--- a/src/crab_verifier.cpp
+++ b/src/crab_verifier.cpp
@@ -26,48 +26,12 @@ thread_local crab::lazy_allocator<program_info> thread_local_program_info;
 thread_local ebpf_verifier_options_t thread_local_options;
 void ebpf_verifier_clear_before_analysis();
 
-struct LineInfoPrinter {
-    std::ostream& os;
-    std::string previous_source_line;
-
-    void print_line_info(const label_t& label) {
-        if (thread_local_options.verbosity_opts.print_line_info) {
-            const auto& line_info_map = thread_local_program_info.get().line_info;
-            const auto& line_info = line_info_map.find(label.from);
-            // Print line info only once.
-            if (line_info != line_info_map.end() && line_info->second.source_line != previous_source_line) {
-                os << "\n" << line_info->second << "\n";
-                previous_source_line = line_info->second.source_line;
-            }
-        }
-    }
-};
-
 bool Invariants::is_valid_after(const label_t& label, const string_invariant& state) const {
     const ebpf_domain_t abstract_state =
         ebpf_domain_t::from_constraints(state.value(), thread_local_options.setup_constraints);
     return abstract_state <= invariants.at(label).post;
 }
 
-void Invariants::print_invariants(std::ostream& os, const cfg_t& cfg, const bool simplify) const {
-    LineInfoPrinter printer{os};
-    for (const auto& bb : basic_block_t::collect_basic_blocks(cfg, simplify)) {
-        os << "\nPre-invariant : " << invariants.at(bb.first_label()).pre << "\n";
-        const crab::value_t& first_node = cfg.get_node(bb.first_label());
-        print_from(os, first_node);
-        print_label(os, first_node);
-        for (const label_t& label : bb) {
-            printer.print_line_info(label);
-            const crab::value_t& node = cfg.get_node(label);
-            print_assertions(os, node);
-            print_instruction(os, node);
-        }
-        print_goto(os, cfg.get_node(bb.last_label()));
-        os << "\nPost-invariant: " << invariants.at(bb.last_label()).post << "\n";
-    }
-    os << "\n";
-}
-
 string_invariant Invariants::invariant_at(const label_t& label) const { return invariants.at(label).post.to_set(); }
 
 crab::interval_t Invariants::exit_value() const { return invariants.at(label_t::exit).post.get_r0(); }
@@ -100,61 +64,6 @@ Invariants analyze(const cfg_t& cfg, const string_invariant& entry_invariant) {
                    ebpf_domain_t::from_constraints(entry_invariant.value(), thread_local_options.setup_constraints));
 }
 
-void Report::print_reachability(std::ostream& os) const {
-    for (const auto& [label, notes] : reachability) {
-        for (const auto& msg : notes) {
-            os << label << ": " << msg << "\n";
-        }
-    }
-    os << "\n";
-}
-
-void Report::print_warnings(std::ostream& os) const {
-    LineInfoPrinter printer{os};
-    for (const auto& [label, warnings] : warnings) {
-        for (const auto& msg : warnings) {
-            printer.print_line_info(label);
-            os << label << ": " << msg << "\n";
-        }
-    }
-    os << "\n";
-}
-
-void Report::print_all_messages(std::ostream& os) const {
-    print_reachability(os);
-    print_warnings(os);
-}
-
-std::set<std::string> Report::all_messages() const {
-    std::set<std::string> result = warning_set();
-    for (const auto& note : reachability_set()) {
-        result.insert(note);
-    }
-    return result;
-}
-
-std::set<std::string> Report::reachability_set() const {
-    std::set<std::string> result;
-    for (const auto& [label, warnings] : reachability) {
-        for (const auto& msg : warnings) {
-            result.insert(to_string(label) + ": " + msg);
-        }
-    }
-    return result;
-}
-
-std::set<std::string> Report::warning_set() const {
-    std::set<std::string> result;
-    for (const auto& [label, warnings] : warnings) {
-        for (const auto& msg : warnings) {
-            result.insert(to_string(label) + ": " + msg);
-        }
-    }
-    return result;
-}
-
-bool Report::verified() const { return warnings.empty(); }
-
 bool Invariants::verified(const cfg_t& cfg) const {
     for (const auto& [label, inv_pair] : invariants) {
         if (inv_pair.pre.is_bottom()) {
diff --git a/src/crab_verifier.hpp b/src/crab_verifier.hpp
index ded49a57a..b6d3c253a 100644
--- a/src/crab_verifier.hpp
+++ b/src/crab_verifier.hpp
@@ -14,13 +14,39 @@ class Report final {
     friend class Invariants;
 
   public:
-    void print_reachability(std::ostream& os) const;
-    void print_warnings(std::ostream& os) const;
-    void print_all_messages(std::ostream& os) const;
-    std::set<std::string> all_messages() const;
-    std::set<std::string> reachability_set() const;
-    std::set<std::string> warning_set() const;
-    bool verified() const;
+    friend void print_reachability(std::ostream& os, const Report& report);
+    friend void print_warnings(std::ostream& os, const Report& report);
+    friend void print_all_messages(std::ostream& os, const Report& report);
+
+    std::set<std::string> all_messages() const {
+        std::set<std::string> result = warning_set();
+        for (const auto& note : reachability_set()) {
+            result.insert(note);
+        }
+        return result;
+    }
+
+    std::set<std::string> reachability_set() const {
+        std::set<std::string> result;
+        for (const auto& [label, warnings] : reachability) {
+            for (const auto& msg : warnings) {
+                result.insert(to_string(label) + ": " + msg);
+            }
+        }
+        return result;
+    }
+
+    std::set<std::string> warning_set() const {
+        std::set<std::string> result;
+        for (const auto& [label, warnings] : warnings) {
+            for (const auto& msg : warnings) {
+                result.insert(to_string(label) + ": " + msg);
+            }
+        }
+        return result;
+    }
+
+    bool verified() const { return warnings.empty(); }
 };
 
 class Invariants final {
@@ -32,7 +58,6 @@ class Invariants final {
     Invariants(const Invariants& invariants) = default;
 
     bool is_valid_after(const label_t& label, const string_invariant& state) const;
-    void print_invariants(std::ostream& os, const cfg_t& cfg, bool simplify) const;
 
     string_invariant invariant_at(const label_t& label) const;
 
@@ -41,6 +66,8 @@ class Invariants final {
     int max_loop_count() const;
     bool verified(const cfg_t& cfg) const;
     Report check_assertions(const cfg_t& cfg) const;
+
+    friend void print_invariants(std::ostream& os, const cfg_t& cfg, bool simplify, const Invariants& invariants);
 };
 
 Invariants analyze(const cfg_t& cfg);
diff --git a/src/main/check.cpp b/src/main/check.cpp
index 9ac233eae..7503d9c49 100644
--- a/src/main/check.cpp
+++ b/src/main/check.cpp
@@ -238,25 +238,24 @@ int main(int argc, char** argv) {
     if (domain == "zoneCrab" || domain == "cfg") {
         // Convert the instruction sequence to a control-flow graph.
         try {
+            const auto verbosity = ebpf_verifier_options.verbosity_opts;
             const cfg_t cfg = prepare_cfg(prog, raw_prog.info, ebpf_verifier_options.cfg_opts);
             if (domain == "cfg") {
-                std::cout << cfg;
-                std::cout << "\n";
+                print_cfg(std::cout, cfg, verbosity.simplify);
                 return 0;
             }
             const auto begin = std::chrono::steady_clock::now();
             auto invariants = analyze(cfg);
             const auto end = std::chrono::steady_clock::now();
             const auto seconds = std::chrono::duration<double>(end - begin).count();
-            const auto verbosity = ebpf_verifier_options.verbosity_opts;
             if (verbosity.print_invariants) {
-                invariants.print_invariants(std::cout, cfg, verbosity.simplify);
+                print_invariants(std::cout, cfg, verbosity.simplify, invariants);
             }
 
             bool pass;
             if (verbosity.print_failures) {
                 auto report = invariants.check_assertions(cfg);
-                report.print_warnings(std::cout);
+                print_warnings(std::cout, report);
                 pass = report.verified();
             } else {
                 pass = invariants.verified(cfg);