diff --git a/src/asm_cfg.cpp b/src/asm_cfg.cpp
index a3b4cad8..acaf689f 100644
--- a/src/asm_cfg.cpp
+++ b/src/asm_cfg.cpp
@@ -24,7 +24,7 @@ struct cfg_builder_t final {
     Program prog;
 
     // TODO: ins should be inserted elsewhere
-    void insert_after(const label_t& prev_label, const label_t& new_label, const GuardedInstruction& ins) {
+    void insert_after(const label_t& prev_label, const label_t& new_label, const Instruction& ins) {
         if (prev_label == new_label) {
             CRAB_ERROR("Cannot insert after the same label ", to_string(new_label));
         }
@@ -43,7 +43,7 @@ struct cfg_builder_t final {
     }
 
     // TODO: ins should be inserted elsewhere
-    void insert(const label_t& _label, const GuardedInstruction& ins) {
+    void insert(const label_t& _label, const Instruction& ins) {
         if (const auto it = prog.m_cfg.neighbours.find(_label); it != prog.m_cfg.neighbours.end()) {
             CRAB_ERROR("Label ", to_string(_label), " already exists");
         }
@@ -52,7 +52,7 @@ struct cfg_builder_t final {
     }
 
     // TODO: ins should be inserted elsewhere
-    label_t insert_jump(const label_t& from, const label_t& to, const GuardedInstruction& ins) {
+    label_t insert_jump(const label_t& from, const label_t& to, const Instruction& ins) {
         const label_t jump_label = label_t::make_jump(from, to);
         if (prog.m_cfg.contains(jump_label)) {
             CRAB_ERROR("Jump label ", to_string(jump_label), " already exists");
@@ -76,10 +76,10 @@ struct cfg_builder_t final {
     }
 
     void set_assertions(const label_t& label, const std::vector<Assertion>& assertions) {
-        if (!prog.m_instructions.contains(label)) {
+        if (!prog.m_cfg.contains(label)) {
             CRAB_ERROR("Label ", to_string(label), " not found in the CFG: ");
         }
-        prog.m_instructions.at(label).preconditions = assertions;
+        prog.m_assertions.insert_or_assign(label, assertions);
     }
 };
 
@@ -164,7 +164,7 @@ static void add_cfg_nodes(cfg_builder_t& builder, const label_t& caller_label, c
         } else if (const auto pcall = std::get_if<Call>(&inst)) {
             pcall->stack_frame_prefix = label.stack_frame_prefix;
         }
-        builder.insert(label, {.cmd = inst});
+        builder.insert(label, inst);
 
         if (first) {
             // Add an edge from the caller to the new block.
@@ -226,7 +226,7 @@ static cfg_builder_t instruction_seq_to_cfg(const InstructionSeq& insts, const b
         if (std::holds_alternative<Undefined>(inst)) {
             continue;
         }
-        builder.insert(label, GuardedInstruction{.cmd = inst});
+        builder.insert(label, inst);
     }
 
     if (insts.size() == 0) {
@@ -262,10 +262,8 @@ static cfg_builder_t instruction_seq_to_cfg(const InstructionSeq& insts, const b
                 if (!builder.prog.cfg().contains(target_label)) {
                     throw InvalidControlFlow{"jump to undefined label " + to_string(target_label)};
                 }
-                builder.insert_jump(label, target_label,
-                                    GuardedInstruction{.cmd = Assume{.cond = *cond, .is_implicit = true}});
-                builder.insert_jump(label, fallthrough,
-                                    GuardedInstruction{.cmd = Assume{.cond = reverse(*cond), .is_implicit = true}});
+                builder.insert_jump(label, target_label, Assume{.cond = *cond, .is_implicit = true});
+                builder.insert_jump(label, fallthrough, Assume{.cond = reverse(*cond), .is_implicit = true});
             } else {
                 builder.add_child(label, jmp->target);
             }
@@ -304,8 +302,7 @@ Program Program::from_sequence(const InstructionSeq& inst_seq, const program_inf
     if (options.check_for_termination) {
         const crab::wto_t wto{builder.prog.cfg()};
         wto.for_each_loop_head([&](const label_t& label) -> void {
-            builder.insert_after(label, label_t::make_increment_counter(label),
-                                 GuardedInstruction{.cmd = IncrementLoopCounter{label}});
+            builder.insert_after(label, label_t::make_increment_counter(label), IncrementLoopCounter{label});
         });
     }
 
@@ -455,7 +452,7 @@ crab::cfg_t crab::cfg_from_adjacency_list(const std::map<label_t, std::vector<la
         if (label == label_t::entry || label == label_t::exit) {
             continue;
         }
-        builder.insert(label, {.cmd = Undefined{}});
+        builder.insert(label, Undefined{});
     }
     for (const auto& [label, children] : adj_list) {
         for (const auto& child : children) {
diff --git a/src/asm_syntax.hpp b/src/asm_syntax.hpp
index f3f64d48..3c257919 100644
--- a/src/asm_syntax.hpp
+++ b/src/asm_syntax.hpp
@@ -353,12 +353,6 @@ struct BoundedLoopCount {
 using Assertion = std::variant<Comparable, Addable, ValidDivisor, ValidAccess, ValidStore, ValidSize, ValidMapKeyValue,
                                ValidCall, TypeConstraint, FuncConstraint, ZeroCtxOffset, BoundedLoopCount>;
 
-struct GuardedInstruction {
-    Instruction cmd;
-    std::vector<Assertion> preconditions;
-    bool operator==(const GuardedInstruction&) const = default;
-};
-
 std::ostream& operator<<(std::ostream& os, Instruction const& ins);
 std::string to_string(Instruction const& ins);
 
diff --git a/src/program.hpp b/src/program.hpp
index a26700a1..ec721ff1 100644
--- a/src/program.hpp
+++ b/src/program.hpp
@@ -14,8 +14,10 @@
 class Program {
     friend struct cfg_builder_t;
 
-    std::map<label_t, GuardedInstruction> m_instructions{{label_t::entry, {.cmd = Undefined{}}},
-                                                         {label_t::exit, {.cmd = Undefined{}}}};
+    std::map<label_t, Instruction> m_instructions{{label_t::entry, Undefined{}}, {label_t::exit, Undefined{}}};
+
+    // This is a cache. The assertions can also be computed on the fly.
+    std::map<label_t, std::vector<Assertion>> m_assertions{{label_t::entry, {}}, {label_t::exit, {}}};
     crab::cfg_t m_cfg;
 
     // TODO: add program_info field
@@ -33,21 +35,21 @@ class Program {
         if (!m_instructions.contains(label)) {
             CRAB_ERROR("Label ", to_string(label), " not found in the CFG: ");
         }
-        return m_instructions.at(label).cmd;
+        return m_instructions.at(label);
     }
 
     Instruction& instruction_at(const label_t& label) {
         if (!m_instructions.contains(label)) {
             CRAB_ERROR("Label ", to_string(label), " not found in the CFG: ");
         }
-        return m_instructions.at(label).cmd;
+        return m_instructions.at(label);
     }
 
     std::vector<Assertion> assertions_at(const label_t& label) const {
         if (!m_instructions.contains(label)) {
             CRAB_ERROR("Label ", to_string(label), " not found in the CFG: ");
         }
-        return m_instructions.at(label).preconditions;
+        return m_assertions.at(label);
     }
 
     static Program from_sequence(const InstructionSeq& inst_seq, const program_info& info,