diff --git a/CMakeLists.txt b/CMakeLists.txt
index 2f1c82543..26d9ae3bf 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -80,10 +80,8 @@ file(GLOB LIB_SRC
 file(GLOB ALL_TEST
         "./src/test/test.cpp"
         "./src/test/test_conformance.cpp"
-        "./src/test/test_loop.cpp"
         "./src/test/test_marshal.cpp"
         "./src/test/test_print.cpp"
-        "./src/test/test_termination.cpp"
         "./src/test/test_verify.cpp"
         "./src/test/test_wto.cpp"
         "./src/test/test_yaml.cpp"
diff --git a/src/asm_marshal.cpp b/src/asm_marshal.cpp
index 82e4bc207..36bbe783e 100644
--- a/src/asm_marshal.cpp
+++ b/src/asm_marshal.cpp
@@ -229,6 +229,10 @@ struct MarshalVisitor {
             .offset = static_cast<int16_t>(b.access.offset),
             .imm = 0}};
     }
+
+    vector<ebpf_inst> operator()(IncrementLoopCounter const& ins) {
+        return {};
+    }
 };
 
 vector<ebpf_inst> marshal(const Instruction& ins, pc_t pc) { return std::visit(MarshalVisitor{label_to_offset(pc)}, ins); }
diff --git a/src/asm_ostream.cpp b/src/asm_ostream.cpp
index 1abf83fd9..2ecdda978 100644
--- a/src/asm_ostream.cpp
+++ b/src/asm_ostream.cpp
@@ -329,6 +329,9 @@ struct InstructionPrinterVisitor {
         os_ << "assert " << a.cst;
     }
 
+    void operator()(IncrementLoopCounter const& a) {
+        os_ << crab::variable_t::instruction_count(to_string(a.name)) << "++";
+    }
 };
 
 string to_string(label_t const& label) {
diff --git a/src/asm_ostream.hpp b/src/asm_ostream.hpp
index 2766c16bf..7ab2c059e 100644
--- a/src/asm_ostream.hpp
+++ b/src/asm_ostream.hpp
@@ -48,5 +48,6 @@ inline std::ostream& operator<<(std::ostream& os, Mem const& a) { return os << (
 inline std::ostream& operator<<(std::ostream& os, LockAdd const& a) { return os << (Instruction)a; }
 inline std::ostream& operator<<(std::ostream& os, Assume const& a) { return os << (Instruction)a; }
 inline std::ostream& operator<<(std::ostream& os, Assert const& a) { return os << (Instruction)a; }
+inline std::ostream& operator<<(std::ostream& os, IncrementLoopCounter const& a) { return os << (Instruction)a; }
 std::ostream& operator<<(std::ostream& os, AssertionConstraint const& a);
 std::string to_string(AssertionConstraint const& constraint);
diff --git a/src/asm_syntax.hpp b/src/asm_syntax.hpp
index 0e4ba3a2a..09da5b6a4 100644
--- a/src/asm_syntax.hpp
+++ b/src/asm_syntax.hpp
@@ -309,7 +309,11 @@ struct Assert {
     Assert(AssertionConstraint cst): cst(cst) { }
 };
 
-using Instruction = std::variant<Undefined, Bin, Un, LoadMapFd, Call, Exit, Jmp, Mem, Packet, LockAdd, Assume, Assert>;
+struct IncrementLoopCounter {
+    label_t name;
+};
+
+using Instruction = std::variant<Undefined, Bin, Un, LoadMapFd, Call, Exit, Jmp, Mem, Packet, LockAdd, Assume, Assert, IncrementLoopCounter>;
 
 using LabeledInstruction = std::tuple<label_t, Instruction, std::optional<btf_line_info_t>>;
 using InstructionSeq = std::vector<LabeledInstruction>;
@@ -382,6 +386,7 @@ DECLARE_EQ5(ValidAccess, reg, offset, width, or_null, access_type)
 DECLARE_EQ3(ValidMapKeyValue, access_reg, map_fd_reg, key)
 DECLARE_EQ1(ZeroCtxOffset, reg)
 DECLARE_EQ1(Assert, cst)
+DECLARE_EQ1(IncrementLoopCounter, name)
 
 }
 
diff --git a/src/assertions.cpp b/src/assertions.cpp
index e3c55ae9d..a76d5906d 100644
--- a/src/assertions.cpp
+++ b/src/assertions.cpp
@@ -38,6 +38,8 @@ class AssertExtractor {
 
     vector<Assert> operator()(Assert const& ins) const { assert(false); return {}; }
 
+    vector<Assert> operator()(IncrementLoopCounter ins) const { assert(false); return {}; }
+
     vector<Assert> operator()(LoadMapFd const& ins) const { return {}; }
 
     /// Packet access implicitly uses R6, so verify that R6 still has a pointer to the context.
diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp
index d49d23977..072ffad67 100644
--- a/src/crab/ebpf_domain.cpp
+++ b/src/crab/ebpf_domain.cpp
@@ -909,8 +909,39 @@ ebpf_domain_t ebpf_domain_t::operator&(const ebpf_domain_t& other) const {
     return ebpf_domain_t(m_inv & other.m_inv, stack & other.stack);
 }
 
-ebpf_domain_t ebpf_domain_t::widen(const ebpf_domain_t& other) {
-    return ebpf_domain_t(m_inv.widen(other.m_inv), stack | other.stack);
+ebpf_domain_t ebpf_domain_t::calculate_constant_limits() {
+    ebpf_domain_t inv;
+    using namespace crab::dsl_syntax;
+    for (int i : {0, 1, 2, 3, 4, 5, 6, 7, 8, 9}) {
+        auto r = reg_pack(i);
+        inv += r.svalue <= std::numeric_limits<int32_t>::max();
+        inv += r.svalue >= std::numeric_limits<int32_t>::min();
+        inv += r.uvalue <= std::numeric_limits<uint32_t>::max();
+        inv += r.uvalue >= 0;
+        inv += r.stack_offset <= EBPF_STACK_SIZE;
+        inv += r.stack_offset >= 0;
+        inv += r.shared_offset <= r.shared_region_size;
+        inv += r.shared_offset >= 0;
+        inv += r.packet_offset <= variable_t::packet_size();
+        inv += r.packet_offset >= 0;
+        if (thread_local_options.check_termination) {
+            for (variable_t counter : variable_t::get_instruction_counters()) {
+                inv += counter <= std::numeric_limits<int32_t>::max();
+                inv += counter >= 0;
+                inv += counter <= r.svalue;
+            }
+        }
+    }
+    return inv;
+}
+
+static const ebpf_domain_t constant_limits = ebpf_domain_t::calculate_constant_limits();
+
+ebpf_domain_t ebpf_domain_t::widen(const ebpf_domain_t& other, bool to_constants) {
+    ebpf_domain_t res{m_inv.widen(other.m_inv), stack | other.stack};
+    if (to_constants)
+        return res & constant_limits;
+    return res;
 }
 
 ebpf_domain_t ebpf_domain_t::narrow(const ebpf_domain_t& other) {
@@ -1333,19 +1364,10 @@ void ebpf_domain_t::overflow_unsigned(NumAbsDomain& inv, variable_t lhs, int fin
     overflow_bounds(inv, lhs, span, finite_width, false);
 }
 
-void ebpf_domain_t::operator()(const basic_block_t& bb, bool check_termination) {
+void ebpf_domain_t::operator()(const basic_block_t& bb) {
     for (const Instruction& statement : bb) {
         std::visit(*this, statement);
     }
-    if (check_termination) {
-        // +1 to avoid being tricked by empty loops
-        add(variable_t::instruction_count(), crab::number_t((unsigned)bb.size() + 1));
-    }
-}
-
-bound_t ebpf_domain_t::get_instruction_count_upper_bound() {
-    const auto& ub = m_inv[variable_t::instruction_count()].ub();
-    return ub;
 }
 
 void ebpf_domain_t::check_access_stack(NumAbsDomain& inv, const linear_expression_t& lb,
@@ -2681,7 +2703,7 @@ void ebpf_domain_t::initialize_packet(ebpf_domain_t& inv) {
 ebpf_domain_t ebpf_domain_t::from_constraints(const std::set<std::string>& constraints, bool setup_constraints) {
     ebpf_domain_t inv;
     if (setup_constraints) {
-        inv = ebpf_domain_t::setup_entry(false, false);
+        inv = ebpf_domain_t::setup_entry(false);
     }
     auto numeric_ranges = std::vector<crab::interval_t>();
     for (const auto& cst : parse_linear_constraints(constraints, numeric_ranges)) {
@@ -2696,7 +2718,7 @@ ebpf_domain_t ebpf_domain_t::from_constraints(const std::set<std::string>& const
     return inv;
 }
 
-ebpf_domain_t ebpf_domain_t::setup_entry(bool check_termination, bool init_r1) {
+ebpf_domain_t ebpf_domain_t::setup_entry(bool init_r1) {
     using namespace crab::dsl_syntax;
 
     ebpf_domain_t inv;
@@ -2719,10 +2741,21 @@ ebpf_domain_t ebpf_domain_t::setup_entry(bool check_termination, bool init_r1) {
     }
 
     initialize_packet(inv);
-    if (check_termination) {
-        inv.assign(variable_t::instruction_count(), 0);
-    }
     return inv;
 }
 
+void ebpf_domain_t::initialize_instruction_count(const label_t label) {
+    m_inv.assign(variable_t::instruction_count(to_string(label)), 0);
+}
+
+bound_t ebpf_domain_t::get_instruction_count_upper_bound() {
+    crab::bound_t ub{number_t{0}};
+    for (variable_t counter : variable_t::get_instruction_counters())
+        ub += std::max(ub, m_inv[counter].ub());
+    return ub;
+}
+
+void ebpf_domain_t::operator()(const IncrementLoopCounter& ins) {
+    this->add(variable_t::instruction_count(to_string(ins.name)), 1);
+}
 } // namespace crab
diff --git a/src/crab/ebpf_domain.hpp b/src/crab/ebpf_domain.hpp
index 4e4aa3710..c8bba9197 100644
--- a/src/crab/ebpf_domain.hpp
+++ b/src/crab/ebpf_domain.hpp
@@ -41,20 +41,20 @@ class ebpf_domain_t final {
     ebpf_domain_t operator|(const ebpf_domain_t& other) const&;
     ebpf_domain_t operator|(const ebpf_domain_t& other) &&;
     ebpf_domain_t operator&(const ebpf_domain_t& other) const;
-    ebpf_domain_t widen(const ebpf_domain_t& other);
+    ebpf_domain_t widen(const ebpf_domain_t& other, bool to_constants);
     ebpf_domain_t widening_thresholds(const ebpf_domain_t& other, const crab::iterators::thresholds_t& ts);
     ebpf_domain_t narrow(const ebpf_domain_t& other);
 
     typedef bool check_require_func_t(NumAbsDomain&, const linear_constraint_t&, std::string);
     void set_require_check(std::function<check_require_func_t> f);
     bound_t get_instruction_count_upper_bound();
-    static ebpf_domain_t setup_entry(bool check_termination, bool init_r1);
+    static ebpf_domain_t setup_entry(bool init_r1);
 
     static ebpf_domain_t from_constraints(const std::set<std::string>& constraints, bool setup_constraints);
     string_invariant to_set();
 
     // abstract transformers
-    void operator()(const basic_block_t& bb, bool check_termination);
+    void operator()(const basic_block_t& bb);
 
     void operator()(const Addable&);
     void operator()(const Assert&);
@@ -77,7 +77,10 @@ class ebpf_domain_t final {
     void operator()(const ValidSize&);
     void operator()(const ValidStore&);
     void operator()(const ZeroCtxOffset&);
+    void operator()(const IncrementLoopCounter&);
 
+    void initialize_instruction_count(label_t label);
+    static ebpf_domain_t calculate_constant_limits();
   private:
     // private generic domain functions
     void operator+=(const linear_constraint_t& cst);
diff --git a/src/crab/fwd_analyzer.cpp b/src/crab/fwd_analyzer.cpp
index f79e86135..5a760bae4 100644
--- a/src/crab/fwd_analyzer.cpp
+++ b/src/crab/fwd_analyzer.cpp
@@ -48,44 +48,37 @@ class interleaved_fwd_fixpoint_iterator_t final {
     wto_t _wto;
     invariant_table_t _pre, _post;
 
-    /// number of iterations until triggering widening
-    const unsigned int _widening_delay{1};
-
     /// number of narrowing iterations. If the narrowing operator is
     /// indeed a narrowing operator this parameter is not
     /// needed. However, there are abstract domains for which an actual
     /// narrowing operation is not available so we must enforce
     /// termination.
-    const unsigned int _descending_iterations;
+    static constexpr unsigned int _descending_iterations = 2000000;
 
     /// Used to skip the analysis until _entry is found
     bool _skip{true};
 
-    /// Whether the domain tracks instruction count; the invariants are somewhat easier to read without it
-    /// Generally corresponds to the check_termination flag in ebpf_verifier_options_t
-    const bool check_termination;
-
   private:
-    inline void set_pre(const label_t& label, const ebpf_domain_t& v) { _pre[label] = v; }
+    void set_pre(const label_t& label, const ebpf_domain_t& v) { _pre[label] = v; }
 
-    inline void transform_to_post(const label_t& label, ebpf_domain_t pre) {
+    void transform_to_post(const label_t& label, ebpf_domain_t pre) {
         basic_block_t& bb = _cfg.get_node(label);
-        pre(bb, check_termination);
+        pre(bb);
         _post[label] = std::move(pre);
     }
 
-    [[nodiscard]]
-    ebpf_domain_t extrapolate(const label_t& node, unsigned int iteration, ebpf_domain_t before,
-                              const ebpf_domain_t& after) const {
-        if (iteration <= _widening_delay) {
+    [[nodiscard]] static ebpf_domain_t extrapolate(ebpf_domain_t before, const ebpf_domain_t& after,
+                                                   unsigned int iteration) {
+        /// number of iterations until triggering widening
+        constexpr auto _widening_delay = 2;
+
+        if (iteration < _widening_delay) {
             return before | after;
-        } else {
-            return before.widen(after);
         }
+        return before.widen(after, iteration == _widening_delay);
     }
 
-    static ebpf_domain_t refine(const label_t& node, unsigned int iteration, ebpf_domain_t before,
-                                const ebpf_domain_t& after) {
+    static ebpf_domain_t refine(ebpf_domain_t before, const ebpf_domain_t& after, unsigned int iteration) {
         if (iteration == 1) {
             return before & after;
         } else {
@@ -102,8 +95,7 @@ class interleaved_fwd_fixpoint_iterator_t final {
     }
 
   public:
-    explicit interleaved_fwd_fixpoint_iterator_t(cfg_t& cfg, unsigned int descending_iterations, bool check_termination)
-        : _cfg(cfg), _wto(cfg), _descending_iterations(descending_iterations), check_termination(check_termination) {
+    explicit interleaved_fwd_fixpoint_iterator_t(cfg_t& cfg) : _cfg(cfg), _wto(cfg) {
         for (const auto& label : _cfg.labels()) {
             _pre.emplace(label, ebpf_domain_t::bottom());
             _post.emplace(label, ebpf_domain_t::bottom());
@@ -114,17 +106,28 @@ class interleaved_fwd_fixpoint_iterator_t final {
 
     ebpf_domain_t get_post(const label_t& node) { return _post.at(node); }
 
-    void operator()(const label_t& vertex);
+    void operator()(const label_t& node);
 
     void operator()(std::shared_ptr<wto_cycle_t>& cycle);
 
-    friend std::pair<invariant_table_t, invariant_table_t> run_forward_analyzer(cfg_t& cfg, const ebpf_domain_t& entry_inv, bool check_termination);
+    friend std::pair<invariant_table_t, invariant_table_t> run_forward_analyzer(cfg_t& cfg, ebpf_domain_t entry_inv);
 };
 
-std::pair<invariant_table_t, invariant_table_t> run_forward_analyzer(cfg_t& cfg, const ebpf_domain_t& entry_inv, bool check_termination) {
+std::pair<invariant_table_t, invariant_table_t> run_forward_analyzer(cfg_t& cfg, ebpf_domain_t entry_inv) {
     // Go over the CFG in weak topological order (accounting for loops).
-    constexpr unsigned int descending_iterations = 2000000;
-    interleaved_fwd_fixpoint_iterator_t analyzer(cfg, descending_iterations, check_termination);
+    interleaved_fwd_fixpoint_iterator_t analyzer(cfg);
+    if (thread_local_options.check_termination) {
+        std::vector<label_t> cycle_heads;
+        for (auto& component : analyzer._wto) {
+            if (std::holds_alternative<std::shared_ptr<wto_cycle_t>>(*component)) {
+                cycle_heads.push_back(std::get<std::shared_ptr<wto_cycle_t>>(*component)->head());
+            }
+        }
+        for (const label_t& label : cycle_heads) {
+            entry_inv.initialize_instruction_count(label);
+            cfg.get_node(label).insert(IncrementLoopCounter{label});
+        }
+    }
     analyzer.set_pre(cfg.entry_label(), entry_inv);
     for (auto& component : analyzer._wto) {
         std::visit(analyzer, *component);
@@ -164,46 +167,41 @@ void interleaved_fwd_fixpoint_iterator_t::operator()(std::shared_ptr<wto_cycle_t
         }
     }
 
-    ebpf_domain_t pre = ebpf_domain_t::bottom();
+    ebpf_domain_t invariant = ebpf_domain_t::bottom();
     if (entry_in_this_cycle) {
-        pre = get_pre(_cfg.entry_label());
+        invariant = get_pre(_cfg.entry_label());
     } else {
         wto_nesting_t cycle_nesting = _wto.nesting(head);
         for (const label_t& prev : _cfg.prev_nodes(head)) {
             if (!(_wto.nesting(prev) > cycle_nesting)) {
-                pre |= get_post(prev);
+                invariant |= get_post(prev);
             }
         }
     }
 
     for (unsigned int iteration = 1;; ++iteration) {
         // Increasing iteration sequence with widening
-        set_pre(head, pre);
-        transform_to_post(head, pre);
+        set_pre(head, invariant);
+        transform_to_post(head, invariant);
         for (auto& component : *cycle) {
             wto_component_t c = *component;
             if (!std::holds_alternative<label_t>(c) || (std::get<label_t>(c) != head))
                 std::visit(*this, *component);
         }
         ebpf_domain_t new_pre = join_all_prevs(head);
-        if (new_pre <= pre) {
+        if (new_pre <= invariant) {
             // Post-fixpoint reached
             set_pre(head, new_pre);
-            pre = std::move(new_pre);
+            invariant = std::move(new_pre);
             break;
         } else {
-            pre = extrapolate(head, iteration, pre, new_pre);
+            invariant = extrapolate(invariant, new_pre, iteration);
         }
     }
 
-    if (this->_descending_iterations == 0) {
-        // no narrowing
-        return;
-    }
-
     for (unsigned int iteration = 1;; ++iteration) {
         // Decreasing iteration sequence with narrowing
-        transform_to_post(head, pre);
+        transform_to_post(head, invariant);
 
         for (auto& component : *cycle) {
             wto_component_t c = *component;
@@ -211,14 +209,14 @@ void interleaved_fwd_fixpoint_iterator_t::operator()(std::shared_ptr<wto_cycle_t
                 std::visit(*this, *component);
         }
         ebpf_domain_t new_pre = join_all_prevs(head);
-        if (pre <= new_pre) {
+        if (invariant <= new_pre) {
             // No more refinement possible(pre == new_pre)
             break;
         } else {
             if (iteration > _descending_iterations)
                 break;
-            pre = refine(head, iteration, pre, new_pre);
-            set_pre(head, pre);
+            invariant = refine(invariant, new_pre, iteration);
+            set_pre(head, invariant);
         }
     }
 }
diff --git a/src/crab/fwd_analyzer.hpp b/src/crab/fwd_analyzer.hpp
index 4f01c3841..a6e35e476 100644
--- a/src/crab/fwd_analyzer.hpp
+++ b/src/crab/fwd_analyzer.hpp
@@ -13,7 +13,6 @@ namespace crab {
 
 using invariant_table_t = std::map<label_t, ebpf_domain_t>;
 
-std::pair<invariant_table_t, invariant_table_t> run_forward_analyzer(cfg_t& cfg, const ebpf_domain_t& entry_inv,
-                                                                     bool check_termination);
+std::pair<invariant_table_t, invariant_table_t> run_forward_analyzer(cfg_t& cfg, ebpf_domain_t entry_inv);
 
 } // namespace crab
diff --git a/src/crab/var_factory.cpp b/src/crab/var_factory.cpp
index 94d55d5d3..2418a0b96 100644
--- a/src/crab/var_factory.cpp
+++ b/src/crab/var_factory.cpp
@@ -88,7 +88,7 @@ variable_t variable_t::kind_var(data_kind_t kind, variable_t type_variable) {
 
 variable_t variable_t::meta_offset() { return make("meta_offset"); }
 variable_t variable_t::packet_size() { return make("packet_size"); }
-variable_t variable_t::instruction_count() { return make("instruction_count"); }
+variable_t variable_t::instruction_count(const std::string& label) { return make("pc[" + label + "]"); }
 
 static bool ends_with(const std::string& str, const std::string& suffix)
 {
@@ -108,4 +108,12 @@ bool variable_t::is_in_stack() const {
     return this->name()[0] == 's';
 }
 
+std::vector<variable_t> variable_t::get_instruction_counters() {
+    std::vector<variable_t> res;
+    for (const std::string& name: *names) {
+        if (name.find("pc") == 0)
+            res.push_back(make(name));
+    }
+    return res;
+}
 } // end namespace crab
diff --git a/src/crab/variable.hpp b/src/crab/variable.hpp
index 12dd13671..f51055c42 100644
--- a/src/crab/variable.hpp
+++ b/src/crab/variable.hpp
@@ -75,8 +75,8 @@ class variable_t final {
     static variable_t kind_var(data_kind_t kind, variable_t type_variable);
     static variable_t meta_offset();
     static variable_t packet_size();
-    static variable_t instruction_count();
-
+    static std::vector<variable_t> get_instruction_counters();
+    static variable_t instruction_count(const std::string& label);
     [[nodiscard]] bool is_in_stack() const;
 
     struct Hasher {
diff --git a/src/crab_verifier.cpp b/src/crab_verifier.cpp
index f4702869b..7904415cd 100644
--- a/src/crab_verifier.cpp
+++ b/src/crab_verifier.cpp
@@ -4,10 +4,7 @@
  *  This module is about selecting the numerical and memory domains, initiating
  *  the verification process and returning the results.
  **/
-#include <cinttypes>
 
-#include <ctime>
-#include <functional>
 #include <iostream>
 #include <map>
 #include <string>
@@ -23,8 +20,8 @@
 #include "crab_verifier.hpp"
 #include "string_constraints.hpp"
 
-using std::string;
 using crab::ebpf_domain_t;
+using std::string;
 
 thread_local crab::lazy_allocator<program_info> global_program_info;
 thread_local ebpf_verifier_options_t thread_local_options;
@@ -34,12 +31,9 @@ struct checks_db final {
     std::map<label_t, std::vector<std::string>> m_db{};
     int total_warnings{};
     int total_unreachable{};
-    crab::bound_t max_instruction_count{crab::number_t{0}};;
-    std::set<label_t> maybe_nonterminating;
+    crab::bound_t max_instruction_count{crab::number_t{0}};
 
-    void add(const label_t& label, const std::string& msg) {
-        m_db[label].emplace_back(msg);
-    }
+    void add(const label_t& label, const std::string& msg) { m_db[label].emplace_back(msg); }
 
     void add_warning(const label_t& label, const std::string& msg) {
         add(label, msg);
@@ -51,11 +45,6 @@ struct checks_db final {
         total_unreachable++;
     }
 
-    void add_nontermination(const label_t& label) {
-        maybe_nonterminating.insert(label);
-        total_warnings++;
-    }
-
     [[nodiscard]] int get_max_instruction_count() const {
         auto m = this->max_instruction_count.number();
         if (m && m->fits_sint32())
@@ -66,60 +55,47 @@ struct checks_db final {
     checks_db() = default;
 };
 
-static checks_db generate_report(cfg_t& cfg,
-                                 crab::invariant_table_t& pre_invariants,
+static checks_db generate_report(cfg_t& cfg, crab::invariant_table_t& pre_invariants,
                                  crab::invariant_table_t& post_invariants) {
     checks_db m_db;
     for (const label_t& label : cfg.sorted_labels()) {
         basic_block_t& bb = cfg.get_node(label);
         ebpf_domain_t from_inv(pre_invariants.at(label));
-        from_inv.set_require_check([&m_db, label](auto& inv, const crab::linear_constraint_t& cst,
-                                                     const std::string& s) {
-            if (inv.is_bottom())
-                return true;
-            if (cst.is_contradiction()) {
-                m_db.add_warning(label, s);
-                return false;
-            }
-
-            if (inv.entail(cst)) {
-                // add_redundant(s);
-                return true;
-            } else if (inv.intersect(cst)) {
-                // TODO: add_error() if imply negation
-                m_db.add_warning(label, s);
-                return false;
-            } else {
-                m_db.add_warning(label, s);
-                return false;
-            }
-        });
-
-        if (thread_local_options.check_termination) {
-            // Pinpoint the places where divergence might occur.
-            crab::bound_t min_instruction_count_upper_bound{crab::bound_t::plus_infinity()};
-            for (const label_t& prev_label : bb.prev_blocks_set()) {
-                crab::bound_t instruction_count = pre_invariants.at(prev_label).get_instruction_count_upper_bound();
-                min_instruction_count_upper_bound = std::min(min_instruction_count_upper_bound, instruction_count);
-            }
-
-            crab::bound_t max_instructions{100000};
-            crab::bound_t instruction_count_upper_bound = from_inv.get_instruction_count_upper_bound();
-            if ((min_instruction_count_upper_bound < max_instructions) &&
-                (instruction_count_upper_bound >= max_instructions))
-                m_db.add_nontermination(label);
-
-            m_db.max_instruction_count = std::max(m_db.max_instruction_count, instruction_count_upper_bound);
-        }
+        from_inv.set_require_check(
+            [&m_db, label](auto& inv, const crab::linear_constraint_t& cst, const std::string& s) {
+                if (inv.is_bottom())
+                    return true;
+                if (cst.is_contradiction()) {
+                    m_db.add_warning(label, s);
+                    return false;
+                }
+
+                if (inv.entail(cst)) {
+                    // add_redundant(s);
+                    return true;
+                } else if (inv.intersect(cst)) {
+                    // TODO: add_error() if imply negation
+                    m_db.add_warning(label, s);
+                    return false;
+                } else {
+                    m_db.add_warning(label, s);
+                    return false;
+                }
+            });
 
         bool pre_bot = from_inv.is_bottom();
 
-        from_inv(bb, thread_local_options.check_termination);
+        from_inv(bb);
 
         if (!pre_bot && from_inv.is_bottom()) {
             m_db.add_unreachable(label, std::string("Code is unreachable after ") + to_string(bb.label()));
         }
     }
+
+    if (thread_local_options.check_termination) {
+        auto last_inv = post_invariants.at(cfg.exit_label());
+        m_db.max_instruction_count = last_inv.get_instruction_count_upper_bound();
+    }
     return m_db;
 }
 
@@ -146,12 +122,9 @@ static void print_report(std::ostream& os, const checks_db& db, const Instructio
         }
     }
     os << "\n";
-    if (!db.maybe_nonterminating.empty()) {
-        os << "Could not prove termination on join into: ";
-        for (const label_t& label : db.maybe_nonterminating) {
-            os << label << ", ";
-        }
-        os << "\n";
+    crab::number_t max_instructions{100000};
+    if (db.max_instruction_count > max_instructions) {
+        os << "Could not prove termination.\n";
     }
 }
 
@@ -178,9 +151,8 @@ static checks_db get_ebpf_report(std::ostream& s, cfg_t& cfg, program_info info,
 
     try {
         // Get dictionaries of pre-invariants and post-invariants for each basic block.
-        ebpf_domain_t entry_dom = ebpf_domain_t::setup_entry(options->check_termination, true);
-        auto [pre_invariants, post_invariants] =
-            crab::run_forward_analyzer(cfg, std::move(entry_dom), options->check_termination);
+        ebpf_domain_t entry_dom = ebpf_domain_t::setup_entry(true);
+        auto [pre_invariants, post_invariants] = crab::run_forward_analyzer(cfg, std::move(entry_dom));
         return get_analysis_report(s, cfg, pre_invariants, post_invariants);
     } catch (std::runtime_error& e) {
         // Convert verifier runtime_error exceptions to failure.
@@ -206,15 +178,19 @@ bool run_ebpf_analysis(std::ostream& s, cfg_t& cfg, const program_info& info, co
 
 static string_invariant_map to_string_invariant_map(crab::invariant_table_t& inv_table) {
     string_invariant_map res;
-    for (auto& [label, inv]: inv_table) {
+    for (auto& [label, inv] : inv_table) {
         res.insert_or_assign(label, inv.to_set());
     }
     return res;
 }
 
-std::tuple<string_invariant, bool>
-ebpf_analyze_program_for_test(std::ostream& os, const InstructionSeq& prog, const string_invariant& entry_invariant,
-                              const program_info& info, const ebpf_verifier_options_t& options) {
+std::tuple<string_invariant, bool> ebpf_analyze_program_for_test(std::ostream& os, const InstructionSeq& prog,
+                                                                 const string_invariant& entry_invariant,
+                                                                 const program_info& info,
+                                                                 const ebpf_verifier_options_t& options) {
+    crab::domains::clear_global_state();
+    crab::variable_t::clear_thread_local_state();
+
     thread_local_options = options;
     global_program_info = info;
     assert(!entry_invariant.is_bottom());
@@ -222,16 +198,13 @@ ebpf_analyze_program_for_test(std::ostream& os, const InstructionSeq& prog, cons
     if (entry_inv.is_bottom())
         throw std::runtime_error("Entry invariant is inconsistent");
     cfg_t cfg = prepare_cfg(prog, info, !options.no_simplify, false);
-    auto [pre_invariants, post_invariants] = crab::run_forward_analyzer(cfg, entry_inv, options.check_termination);
+    auto [pre_invariants, post_invariants] = crab::run_forward_analyzer(cfg, std::move(entry_inv));
     checks_db report = get_analysis_report(std::cerr, cfg, pre_invariants, post_invariants);
     print_report(os, report, prog, false);
 
     auto pre_invariant_map = to_string_invariant_map(pre_invariants);
 
-    return {
-        pre_invariant_map.at(label_t::exit),
-        (report.total_warnings == 0)
-    };
+    return {pre_invariant_map.at(label_t::exit), (report.total_warnings == 0)};
 }
 
 /// Returned value is true if the program passes verification.
diff --git a/src/ebpf_yaml.cpp b/src/ebpf_yaml.cpp
index 28d8a2fa9..25b27a006 100644
--- a/src/ebpf_yaml.cpp
+++ b/src/ebpf_yaml.cpp
@@ -29,11 +29,11 @@ static EbpfMapType ebpf_get_map_type(uint32_t platform_specific_type) {
 
 static EbpfHelperPrototype ebpf_get_helper_prototype(int32_t n) {
     return {};
-};
+}
 
 static bool ebpf_is_helper_usable(int32_t n){
     return false;
-};
+}
 
 static void ebpf_parse_maps_section(vector<EbpfMapDescriptor>& map_descriptors, const char* data, size_t map_record_size, int map_count,
                                     const struct ebpf_platform_t* platform, ebpf_verifier_options_t options) {
@@ -225,15 +225,14 @@ static Diff<T> make_diff(const T& actual, const T& expected) {
     };
 }
 
-std::optional<Failure> run_yaml_test_case(const TestCase& _test_case, bool debug) {
-    TestCase test_case = _test_case;
+std::optional<Failure> run_yaml_test_case(TestCase test_case, bool debug) {
     if (debug) {
         test_case.options.print_failures = true;
         test_case.options.print_invariants = true;
         test_case.options.no_simplify = true;
     }
 
-    ebpf_context_descriptor_t context_descriptor{64, 0, 8, -1};
+    ebpf_context_descriptor_t context_descriptor{64, 0, 4, -1};
     EbpfProgramType program_type = make_program_type(test_case.name, &context_descriptor);
 
     program_info info{&g_platform_test, {}, program_type};
diff --git a/src/ebpf_yaml.hpp b/src/ebpf_yaml.hpp
index af45ce642..183ea3daa 100644
--- a/src/ebpf_yaml.hpp
+++ b/src/ebpf_yaml.hpp
@@ -32,7 +32,7 @@ struct Failure {
 
 void print_failure(const Failure& failure, std::ostream& out);
 
-std::optional<Failure> run_yaml_test_case(const TestCase& test_case, bool debug = false);
+std::optional<Failure> run_yaml_test_case(TestCase test_case, bool debug = false);
 
 struct ConformanceTestResult {
     bool success{};
diff --git a/src/test/test_loop.cpp b/src/test/test_loop.cpp
deleted file mode 100644
index e265baa4a..000000000
--- a/src/test/test_loop.cpp
+++ /dev/null
@@ -1,33 +0,0 @@
-// Copyright (c) Prevail Verifier contributors.
-// SPDX-License-Identifier: MIT
-#include <catch2/catch_all.hpp>
-
-#include "ebpf_verifier.hpp"
-
-using namespace crab;
-
-TEST_CASE("Trivial loop: middle", "[sanity][loop]") {
-    cfg_t cfg;
-
-    basic_block_t& entry = cfg.insert(label_t(0));
-    basic_block_t& middle = cfg.insert(label_t(1));
-    basic_block_t& exit = cfg.get_node(cfg.exit_label());
-
-    entry.insert(Bin{.op = Bin::Op::MOV, .dst = Reg{0}, .v = Imm{0}, .is64 = true});
-    middle.insert(Bin{.op = Bin::Op::ADD, .dst = Reg{0}, .v = Imm{1}, .is64 = true});
-
-    cfg.get_node(cfg.entry_label()) >> entry;
-    entry >> middle;
-    middle >> middle;
-    middle >> exit;
-
-    ebpf_verifier_options_t options{
-        .check_termination=false
-    };
-    program_info info{
-        .platform = &g_ebpf_platform_linux,
-        .type = g_ebpf_platform_linux.get_program_type("unspec", "unspec")
-    };
-    bool pass = run_ebpf_analysis(std::cout, cfg, info, &options, nullptr);
-    REQUIRE(pass);
-}
diff --git a/src/test/test_termination.cpp b/src/test/test_termination.cpp
deleted file mode 100644
index 6188b08a7..000000000
--- a/src/test/test_termination.cpp
+++ /dev/null
@@ -1,69 +0,0 @@
-// Copyright (c) Prevail Verifier contributors.
-// SPDX-License-Identifier: MIT
-#include <catch2/catch_all.hpp>
-
-#include "crab/cfg.hpp"
-#include "crab_verifier.hpp"
-#include "config.hpp"
-#include "platform.hpp"
-
-using namespace crab;
-
-TEST_CASE("Trivial infinite loop", "[loop][termination]") {
-    cfg_t cfg;
-
-    basic_block_t& entry = cfg.get_node(cfg.entry_label());
-    basic_block_t& middle = cfg.insert(label_t(0));
-    basic_block_t& exit = cfg.get_node(cfg.exit_label());
-
-    entry >> middle;
-    middle >> middle;
-    middle >> exit;
-
-    ebpf_verifier_options_t options{
-        .check_termination = true,
-    };
-    program_info info{
-        .platform = &g_ebpf_platform_linux,
-        .type = g_ebpf_platform_linux.get_program_type("unspec", "unspec")
-    };
-    ebpf_verifier_stats_t stats;
-    bool pass = run_ebpf_analysis(std::cout, cfg, info, &options, &stats);
-    REQUIRE_FALSE(pass);
-    REQUIRE(stats.max_instruction_count == INT_MAX);
-    REQUIRE(stats.total_unreachable == 0);
-    REQUIRE(stats.total_warnings == 1);
-}
-
-TEST_CASE("Trivial finite loop", "[loop][termination]") {
-    cfg_t cfg;
-
-    basic_block_t& entry = cfg.get_node(cfg.entry_label());
-    basic_block_t& start = cfg.insert(label_t(0));
-    basic_block_t& middle = cfg.insert(label_t(1));
-    basic_block_t& exit = cfg.get_node(cfg.exit_label());
-
-    Reg r{0};
-    start.insert(Bin{.op = Bin::Op::MOV, .dst = r, .v = Imm{0}, .is64 = true});
-    middle.insert(Assume{{.op=Condition::Op::GT, .left=r, .right=Imm{10}, .is64=true}});
-    middle.insert(Bin{.op = Bin::Op::ADD, .dst = r, .v = Imm{1}, .is64 = true});
-
-    entry >> start;
-    start >> middle;
-    middle >> middle;
-    middle >> exit;
-
-    ebpf_verifier_options_t options{
-        .check_termination = true,
-    };
-    program_info info{
-        .platform = &g_ebpf_platform_linux,
-        .type = g_ebpf_platform_linux.get_program_type("unspec", "unspec")
-    };
-    ebpf_verifier_stats_t stats;
-    bool pass = run_ebpf_analysis(std::cout, cfg, info, &options, &stats);
-    REQUIRE(pass);
-    REQUIRE(stats.max_instruction_count == 3);
-    REQUIRE(stats.total_unreachable == 1);
-    REQUIRE(stats.total_warnings == 0);
-}
diff --git a/src/test/test_yaml.cpp b/src/test/test_yaml.cpp
index 86f572c37..e77f0ed05 100644
--- a/src/test/test_yaml.cpp
+++ b/src/test/test_yaml.cpp
@@ -26,6 +26,7 @@ YAML_CASE("test-data/call.yaml")
 YAML_CASE("test-data/divmod.yaml")
 YAML_CASE("test-data/full64.yaml")
 YAML_CASE("test-data/jump.yaml")
+YAML_CASE("test-data/loop.yaml")
 YAML_CASE("test-data/packet.yaml")
 YAML_CASE("test-data/parse.yaml")
 YAML_CASE("test-data/shift.yaml")
diff --git a/test-data/assign.yaml b/test-data/assign.yaml
index 918102ae0..4385c0ceb 100644
--- a/test-data/assign.yaml
+++ b/test-data/assign.yaml
@@ -219,7 +219,7 @@ pre: ["r1.ctx_offset=0", "r1.type=ctx", "r1.svalue=[1, 2147418112]", "r1.uvalue=
 
 code:
   <start>: |
-    r2 = *(u32 *)(r1 + 8)
+    r2 = *(u32 *)(r1 + 4)
 
 post:
   - packet_size=r2.packet_offset
diff --git a/test-data/loop.yaml b/test-data/loop.yaml
new file mode 100644
index 000000000..643cb4b16
--- /dev/null
+++ b/test-data/loop.yaml
@@ -0,0 +1,268 @@
+# Copyright (c) Prevail Verifier contributors.
+# SPDX-License-Identifier: MIT
+---
+test-case: while loop, unsigned gte
+options: ["termination"]
+pre: []
+
+code:
+  <start>: |
+    r0 = 0
+  <loop>: |
+    if r0 >= 4 goto <out>
+    r0 += 1
+    goto <loop>
+  <out>: |
+    exit
+
+post:
+  - "r0.type=number"
+  - "r0.svalue=4"
+  - "r0.uvalue=4"
+  - "r0.svalue=r0.uvalue"
+  - "pc[1]=5"
+  - "pc[1]=r0.svalue+1"
+  - "pc[1]=r0.uvalue+1"
+---
+test-case: until loop, unsigned leq
+options: ["termination"]
+pre: []
+
+code:
+  <start>: |
+    r0 = 0
+  <loop>: |
+    r0 += 1
+    if r0 <= 3 goto <loop>
+  <out>: |
+    exit
+
+post:
+  - "r0.type=number"
+  - "r0.svalue=4"
+  - "r0.uvalue=4"
+  - "r0.svalue=r0.uvalue"
+  - "pc[1]=4"
+  - "pc[1]=r0.svalue"
+  - "pc[1]=r0.uvalue"
+---
+test-case: while loop, signed gte
+options: ["termination"]
+pre: []
+
+code:
+  <start>: |
+    r0 = 0
+  <loop>: |
+    if r0 s>= 4 goto <out>
+    r0 += 1
+    goto <loop>
+  <out>: |
+    exit
+
+post:
+  - "r0.type=number"
+  - "r0.svalue=4"
+  - "r0.uvalue=4"
+  - "r0.svalue=r0.uvalue"
+  - "pc[1]=5"
+  - "pc[1]=r0.svalue+1"
+  - "pc[1]=r0.uvalue+1"
+---
+test-case: until loop, signed leq
+options: ["termination"]
+
+pre: []
+
+code:
+  <start>: |
+    r0 = 0
+  <loop>: |
+    r0 += 1
+    if r0 s<= 3 goto <loop>
+  <out>: |
+    exit
+
+post:
+  - "r0.type=number"
+  - "r0.svalue=4"
+  - "r0.uvalue=4"
+  - "r0.svalue=r0.uvalue"
+  - "pc[1]=4"
+  - "pc[1]=r0.svalue"
+  - "pc[1]=r0.uvalue"
+---
+test-case: loop with data dependence, unsigned leq
+options: ["termination"]
+
+pre: ["r1.type=number", "r2.type=number", "r3.type=number"]
+
+code:
+  <start>: |
+    r0 = 0
+  <loop>: |
+    r0 += 1
+    r1 += r2
+    if r1 > r3 goto <out>
+    if r0 <= 3 goto <loop>
+  <out>: |
+    exit
+
+post:
+  - "r0.type=number"
+  - "r0.svalue=[1, 4]"
+  - "r0.uvalue=[1, 4]"
+  - "r0.svalue=r0.uvalue"
+  - "r1.type=number"
+  - "r2.type=number"
+  - "r3.type=number"
+  - "pc[1]=[1, 4]"
+  - "pc[1]=r0.svalue"
+  - "pc[1]=r0.uvalue"
+---
+test-case: while loop, eq
+#options: ["termination"]
+pre: []
+
+code:
+  <start>: |
+    r0 = 0
+  <loop>: |
+    if r0 == 4 goto <out>
+    r0 += 1
+    goto <loop>
+  <out>: |
+    exit
+
+post:
+  - "r0.type=number"
+  - "r0.svalue=4"
+  - "r0.uvalue=4"
+#  - "r0.svalue=r0.uvalue"
+#  - "pc[1]=4"
+#  - "pc[1]=r0.value"
+---
+test-case: until loop, neq
+#options: ["termination"]
+
+pre: []
+
+code:
+  <start>: |
+    r0 = 0
+  <loop>: |
+    r0 += 1
+    if r0 != 9 goto <loop>
+  <out>: |
+    exit
+
+post:
+  - "r0.type=number"
+  - "r0.svalue=9"
+  - "r0.uvalue=9"
+#  - "r0.svalue=r0.uvalue"
+#  - "pc[1]=9"
+#  - "pc[1]=r0.value"
+---
+test-case: simple infinite loop, neq
+options: ["termination"]
+
+pre: []
+
+code:
+  <start>: |
+    r0 = 0
+  <loop>: |
+    r0 += 2
+    if r0 != 9 goto <loop>
+  <out>: |
+    exit
+
+post:
+  - "r0.type=number"
+  - "r0.svalue=9"
+  - "r0.uvalue=9"
+#  - "r0.svalue=r0.uvalue"
+  - "pc[1]=[1, +oo]"
+
+messages:
+  - "Could not prove termination."
+
+---
+test-case: realistic forward loop
+options: ["termination"]
+
+pre: [
+  "meta_offset=[-4098, 0]",
+  "packet_size=[0, 65534]",
+  "r1.ctx_offset=0", "r1.svalue=[1, 2147418112]", "r1.type=ctx",
+]
+
+code:
+  <start>: |
+    r0 = 0
+    r2 = *(u32 *)(r1 + 4)
+    r1 = *(u32 *)(r1 + 0)
+    assume r2 != r1
+    r2 -= r1
+    r3 = 0
+    r0 = 0
+#    r2 <<= 32; this fails with "11: Upper bound must be at most packet_size (valid_access(r4.offset, width=1) for read)"
+#    r2 >>= 32
+  <loop>: |
+    r4 = r1
+    r4 += r3
+    r4 = *(u8 *)(r4 + 0)
+    r0 += r4
+    r3 += 1
+    if r4 == r3 goto <exit>
+    assume r2 > r3
+    goto <loop>
+  <exit>: |
+    exit
+
+post:
+  - meta_offset=[-oo, 0]
+  - packet_size=[1, 65534]
+  - packet_size=r2.svalue
+  - packet_size=r2.uvalue
+  - pc[7]-packet_size<=0
+  - pc[7]-r2.svalue<=0
+  - pc[7]-r2.uvalue<=0
+  - pc[7]=[1, 255]
+  - pc[7]=r3.svalue
+  - pc[7]=r3.uvalue
+  - pc[7]=r4.svalue
+  - pc[7]=r4.uvalue
+  - r0.type=number
+  - r1.packet_offset=0
+  - r1.svalue=[4098, 2147418112]
+  - r1.type=packet
+  - r2.svalue=[1, 65534]
+  - r2.svalue=r2.uvalue
+  - r2.type=number
+  - r2.uvalue=[1, 65534]
+  - r3.svalue-packet_size<=0
+  - r3.svalue-r2.svalue<=0
+  - r3.svalue-r2.uvalue<=0
+  - r3.svalue=[1, 255]
+  - r3.svalue=r3.uvalue
+  - r3.svalue=r4.svalue
+  - r3.svalue=r4.uvalue
+  - r3.type=number
+  - r3.uvalue-packet_size<=0
+  - r3.uvalue-r2.svalue<=0
+  - r3.uvalue-r2.uvalue<=0
+  - r3.uvalue=[1, 255]
+  - r3.uvalue=r4.svalue
+  - r3.uvalue=r4.uvalue
+  - r4.svalue-packet_size<=0
+  - r4.svalue-r2.svalue<=0
+  - r4.svalue-r2.uvalue<=0
+  - r4.svalue=[1, 255]
+  - r4.svalue=r4.uvalue
+  - r4.type=number
+  - r4.uvalue-packet_size<=0
+  - r4.uvalue-r2.svalue<=0
+  - r4.uvalue-r2.uvalue<=0
+  - r4.uvalue=[1, 255]