diff --git a/src/asm_cfg.cpp b/src/asm_cfg.cpp
index fabd9c2ba..337003323 100644
--- a/src/asm_cfg.cpp
+++ b/src/asm_cfg.cpp
@@ -250,6 +250,57 @@ cfg_t prepare_cfg(const InstructionSeq& prog, const program_info& info, const pr
     return cfg;
 }
 
+std::set<basic_block_t> basic_block_t::collect_basic_blocks(const cfg_t& cfg, const bool simplify) {
+    if (!simplify) {
+        std::set<basic_block_t> res;
+        for (const label_t& label : cfg.labels()) {
+            if (label != cfg.entry_label() && label != cfg.exit_label()) {
+                res.insert(basic_block_t{label});
+            }
+        }
+        return res;
+    }
+
+    std::set<basic_block_t> res;
+    std::set worklist(cfg.label_begin(), cfg.label_end());
+    std::set<label_t> seen;
+    while (!worklist.empty()) {
+        const label_t label = *worklist.begin();
+        worklist.erase(label);
+        if (seen.contains(label)) {
+            continue;
+        }
+        seen.insert(label);
+
+        const value_t* current_value = &cfg.get_node(label);
+        if (current_value->in_degree() == 1 && cfg.get_parent(label).out_degree() == 1) {
+            continue;
+        }
+        basic_block_t bb{label};
+        while (current_value->out_degree() == 1) {
+            const value_t& next_value = cfg.get_child(bb.last_label());
+            const label_t& next_label = next_value.label();
+
+            if (seen.contains(next_label) || next_label == cfg.exit_label() || next_value.in_degree() != 1) {
+                break;
+            }
+
+            if (bb.first_label() == cfg.entry_label()) {
+                // Entry instruction is Undefined. We want to start with 0
+                bb.m_ts.clear();
+            }
+            bb.m_ts.push_back(next_label);
+
+            worklist.erase(next_label);
+            seen.insert(next_label);
+
+            current_value = &next_value;
+        }
+        res.emplace(std::move(bb));
+    }
+    return res;
+}
+
 template <typename T>
 static vector<label_t> unique(const std::pair<T, T>& be) {
     vector<label_t> res;
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 bb8a32a65..8072bcf0e 100644
--- a/src/crab/cfg.hpp
+++ b/src/crab/cfg.hpp
@@ -385,43 +385,7 @@ class basic_block_t final {
   public:
     std::strong_ordering operator<=>(const basic_block_t& other) const { return first_label() <=> other.first_label(); }
 
-    static std::set<basic_block_t> collect_basic_blocks(const cfg_t& cfg) {
-        std::set<basic_block_t> res;
-
-        std::set worklist(cfg.label_begin(), cfg.label_end());
-        std::set<label_t> seen;
-        while (!worklist.empty()) {
-            const label_t label = *worklist.begin();
-            worklist.erase(label);
-            if (seen.contains(label)) {
-                continue;
-            }
-            seen.insert(label);
-
-            const value_t* current_value = &cfg.get_node(label);
-            if (current_value->in_degree() == 1 && cfg.get_parent(label).out_degree() == 1) {
-                continue;
-            }
-            basic_block_t bb{label};
-            while (current_value->out_degree() == 1) {
-                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) {
-                    break;
-                }
-
-                bb.m_ts.push_back(next_label);
-
-                worklist.erase(next_label);
-                seen.insert(next_label);
-
-                current_value = &next_value;
-            }
-            res.emplace(std::move(bb));
-        }
-        return res;
-    }
+    static std::set<basic_block_t> collect_basic_blocks(const cfg_t& cfg, bool simplify);
 
     explicit basic_block_t(const label_t& first_label) : m_ts{first_label} {}
     basic_block_t(basic_block_t&&) noexcept = default;
@@ -455,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 616f0d658..049c091c8 100644
--- a/src/crab_verifier.cpp
+++ b/src/crab_verifier.cpp
@@ -26,61 +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 {
-    if (thread_local_options.verbosity_opts.simplify) {
-        for (const auto& bb : basic_block_t::collect_basic_blocks(cfg)) {
-            os << "\nPre-invariant : " << invariants.at(bb.first_label()).pre << "\n";
-            print_from(os, cfg.get_node(bb.first_label()));
-            print_label(os, cfg.get_node(bb.first_label()));
-            for (const auto& label : bb) {
-                const auto& value = cfg.get_node(label);
-                print_assertions(os, value);
-                print_instruction(os, value);
-            }
-            print_goto(os, cfg.get_node(bb.last_label()));
-            os << "\nPost-invariant: " << invariants.at(bb.last_label()).post << "\n";
-        }
-    } else {
-        LineInfoPrinter printer{os};
-        for (const label_t& label : cfg.sorted_labels()) {
-            printer.print_line_info(label);
-            const auto& inv_pair = invariants.at(label);
-            os << "\nPre-invariant : " << inv_pair.pre << "\n";
-            const auto& value = cfg.get_node(label);
-            print_from(os, value);
-            print_label(os, value);
-            print_assertions(os, value);
-            print_instruction(os, value);
-            print_goto(os, value);
-            os << "\nPost-invariant: " << inv_pair.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(); }
@@ -113,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 b5dc99b89..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) 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 cabfc4155..7503d9c49 100644
--- a/src/main/check.cpp
+++ b/src/main/check.cpp
@@ -238,32 +238,30 @@ 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();
-
-            if (ebpf_verifier_options.verbosity_opts.print_invariants) {
-                invariants.print_invariants(std::cout, cfg);
+            if (verbosity.print_invariants) {
+                print_invariants(std::cout, cfg, verbosity.simplify, invariants);
             }
 
             bool pass;
-            if (ebpf_verifier_options.verbosity_opts.print_failures) {
+            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);
             }
             if (pass && ebpf_verifier_options.cfg_opts.check_for_termination &&
-                (ebpf_verifier_options.verbosity_opts.print_failures ||
-                 ebpf_verifier_options.verbosity_opts.print_invariants)) {
+                (verbosity.print_failures || verbosity.print_invariants)) {
                 std::cout << "Program terminates within " << invariants.max_loop_count() << " loop iterations\n";
             }
             std::cout << pass << "," << seconds << "," << resident_set_size_kb() << "\n";