diff --git a/src/asm_marshal.cpp b/src/asm_marshal.cpp
index 5e8854474..155b3f665 100644
--- a/src/asm_marshal.cpp
+++ b/src/asm_marshal.cpp
@@ -10,7 +10,7 @@
 
 using std::vector;
 
-static uint8_t op(Condition::Op op) {
+static uint8_t op(const Condition::Op op) {
     using Op = Condition::Op;
     switch (op) {
     case Op::EQ: return 0x1;
@@ -30,7 +30,7 @@ static uint8_t op(Condition::Op op) {
     return {};
 }
 
-static uint8_t op(Bin::Op op) {
+static uint8_t op(const Bin::Op op) {
     using Op = Bin::Op;
     switch (op) {
     case Op::ADD: return 0x0;
@@ -55,7 +55,7 @@ static uint8_t op(Bin::Op op) {
     return {};
 }
 
-static int16_t offset(Bin::Op op) {
+static int16_t offset(const Bin::Op op) {
     using Op = Bin::Op;
     switch (op) {
     case Op::SDIV:
@@ -63,11 +63,11 @@ static int16_t offset(Bin::Op op) {
     case Op::MOVSX8: return 8;
     case Op::MOVSX16: return 16;
     case Op::MOVSX32: return 32;
+    default: return 0;
     }
-    return 0;
 }
 
-static uint8_t imm_endian(Un::Op op) {
+static uint8_t imm_endian(const Un::Op op) {
     using Op = Un::Op;
     switch (op) {
     case Op::NEG: assert(false); return 0;
@@ -87,7 +87,7 @@ static uint8_t imm_endian(Un::Op op) {
 
 struct MarshalVisitor {
   private:
-    static vector<ebpf_inst> makeLddw(Reg dst, bool isFd, int32_t imm, int32_t next_imm) {
+    static vector<ebpf_inst> makeLddw(const Reg dst, const bool isFd, const int32_t imm, const int32_t next_imm) {
         return {ebpf_inst{.opcode = static_cast<uint8_t>(INST_CLS_LD | width_to_opcode(8)),
                           .dst = dst.v,
                           .src = static_cast<uint8_t>(isFd ? 1 : 0),
@@ -100,14 +100,14 @@ struct MarshalVisitor {
     std::function<auto(label_t)->int16_t> label_to_offset16;
     std::function<auto(label_t)->int32_t> label_to_offset32;
 
-    vector<ebpf_inst> operator()(Undefined const& a) {
+    vector<ebpf_inst> operator()(Undefined const& a) const {
         assert(false);
         return {};
     }
 
-    vector<ebpf_inst> operator()(LoadMapFd const& b) { return makeLddw(b.dst, true, b.mapfd, 0); }
+    vector<ebpf_inst> operator()(LoadMapFd const& b) const { return makeLddw(b.dst, true, b.mapfd, 0); }
 
-    vector<ebpf_inst> operator()(Bin const& b) {
+    vector<ebpf_inst> operator()(Bin const& b) const {
         if (b.lddw) {
             const auto pimm = std::get_if<Imm>(&b.v);
             assert(pimm != nullptr);
@@ -120,16 +120,16 @@ struct MarshalVisitor {
                       .src = 0,
                       .offset = offset(b.op),
                       .imm = 0};
-        std::visit(overloaded{[&](Reg right) {
+        std::visit(overloaded{[&](const Reg right) {
                                   res.opcode |= INST_SRC_REG;
                                   res.src = right.v;
                               },
-                              [&](Imm right) { res.imm = static_cast<int32_t>(right.v); }},
+                              [&](const Imm right) { res.imm = static_cast<int32_t>(right.v); }},
                    b.v);
         return {res};
     }
 
-    vector<ebpf_inst> operator()(Un const& b) {
+    vector<ebpf_inst> operator()(Un const& b) const {
         switch (b.op) {
         case Un::Op::NEG:
             return {ebpf_inst{
@@ -174,7 +174,7 @@ struct MarshalVisitor {
         return {};
     }
 
-    vector<ebpf_inst> operator()(Call const& b) {
+    vector<ebpf_inst> operator()(Call const& b) const {
         return {ebpf_inst{.opcode = static_cast<uint8_t>(INST_OP_CALL),
                           .dst = 0,
                           .src = INST_CALL_STATIC_HELPER,
@@ -182,7 +182,7 @@ struct MarshalVisitor {
                           .imm = b.func}};
     }
 
-    vector<ebpf_inst> operator()(CallLocal const& b) {
+    vector<ebpf_inst> operator()(CallLocal const& b) const {
         return {ebpf_inst{.opcode = static_cast<uint8_t>(INST_OP_CALL),
                           .dst = 0,
                           .src = INST_CALL_LOCAL,
@@ -190,7 +190,7 @@ struct MarshalVisitor {
                           .imm = label_to_offset32(b.target)}};
     }
 
-    vector<ebpf_inst> operator()(Callx const& b) {
+    vector<ebpf_inst> operator()(Callx const& b) const {
         // callx is defined to have the register in 'dst' not in 'src'.
         return {ebpf_inst{.opcode = static_cast<uint8_t>(INST_OP_CALLX),
                           .dst = b.func.v,
@@ -198,15 +198,15 @@ struct MarshalVisitor {
                           .offset = 0}};
     }
 
-    vector<ebpf_inst> operator()(Exit const& b) {
+    vector<ebpf_inst> operator()(Exit const& b) const {
         return {ebpf_inst{.opcode = INST_OP_EXIT, .dst = 0, .src = 0, .offset = 0, .imm = 0}};
     }
 
-    vector<ebpf_inst> operator()(Assume const& b) { throw std::invalid_argument("Cannot marshal assumptions"); }
+    vector<ebpf_inst> operator()(Assume const&) const { throw std::invalid_argument("Cannot marshal assumptions"); }
 
-    vector<ebpf_inst> operator()(Assert const& b) { throw std::invalid_argument("Cannot marshal assertions"); }
+    vector<ebpf_inst> operator()(Assert const&) const { throw std::invalid_argument("Cannot marshal assertions"); }
 
-    vector<ebpf_inst> operator()(Jmp const& b) {
+    vector<ebpf_inst> operator()(Jmp const& b) const {
         if (b.cond) {
             ebpf_inst res{
                 .opcode = static_cast<uint8_t>(INST_CLS_JMP | (op(b.cond->op) << 4)),
@@ -214,15 +214,15 @@ struct MarshalVisitor {
                 .src = 0,
                 .offset = label_to_offset16(b.target),
             };
-            visit(overloaded{[&](Reg right) {
+            visit(overloaded{[&](const Reg right) {
                                  res.opcode |= INST_SRC_REG;
                                  res.src = right.v;
                              },
-                             [&](Imm right) { res.imm = static_cast<int32_t>(right.v); }},
+                             [&](const Imm right) { res.imm = static_cast<int32_t>(right.v); }},
                   b.cond->right);
             return {res};
         } else {
-            int32_t imm = label_to_offset32(b.target);
+            const int32_t imm = label_to_offset32(b.target);
             if (imm != 0) {
                 return {ebpf_inst{.opcode = INST_OP_JA32, .imm = imm}};
             } else {
@@ -231,8 +231,8 @@ struct MarshalVisitor {
         }
     }
 
-    vector<ebpf_inst> operator()(Mem const& b) {
-        Deref access = b.access;
+    vector<ebpf_inst> operator()(Mem const& b) const {
+        const Deref access = b.access;
         ebpf_inst res{
             .opcode = static_cast<uint8_t>(INST_MODE_MEM | width_to_opcode(access.width)),
             .dst = 0,
@@ -245,7 +245,7 @@ struct MarshalVisitor {
             }
             res.opcode |= INST_CLS_LD | 0x1;
             res.dst = static_cast<uint8_t>(std::get<Reg>(b.value).v);
-            res.src = static_cast<uint8_t>(access.basereg.v);
+            res.src = access.basereg.v;
         } else {
             res.opcode |= INST_CLS_ST;
             res.dst = access.basereg.v;
@@ -260,7 +260,7 @@ struct MarshalVisitor {
         return {res};
     }
 
-    vector<ebpf_inst> operator()(Packet const& b) {
+    vector<ebpf_inst> operator()(Packet const& b) const {
         ebpf_inst res{
             .opcode = static_cast<uint8_t>(INST_CLS_LD | width_to_opcode(b.width)),
             .dst = 0,
@@ -277,8 +277,8 @@ struct MarshalVisitor {
         return {res};
     }
 
-    vector<ebpf_inst> operator()(Atomic const& b) {
-        int32_t imm = (int32_t)b.op;
+    vector<ebpf_inst> operator()(Atomic const& b) const {
+        int32_t imm = static_cast<int32_t>(b.op);
         if (b.fetch) {
             imm |= INST_FETCH;
         }
@@ -290,25 +290,13 @@ struct MarshalVisitor {
                       .imm = imm}};
     }
 
-    vector<ebpf_inst> operator()(IncrementLoopCounter const& ins) { return {}; }
+    vector<ebpf_inst> operator()(IncrementLoopCounter const&) const { return {}; }
 };
 
-vector<ebpf_inst> marshal(const Instruction& ins, pc_t pc) {
+vector<ebpf_inst> marshal(const Instruction& ins, const pc_t pc) {
     return std::visit(MarshalVisitor{label_to_offset16(pc), label_to_offset32(pc)}, ins);
 }
 
-vector<ebpf_inst> marshal(const vector<Instruction>& insts) {
-    vector<ebpf_inst> res;
-    pc_t pc = 0;
-    for (const auto& ins : insts) {
-        for (auto e : marshal(ins, pc)) {
-            pc++;
-            res.push_back(e);
-        }
-    }
-    return res;
-}
-
 static int size(const Instruction& inst) {
     if (const auto pins = std::get_if<Bin>(&inst)) {
         if (pins->lddw) {
@@ -333,7 +321,7 @@ static auto get_labels(const InstructionSeq& insts) {
 
 vector<ebpf_inst> marshal(const InstructionSeq& insts) {
     vector<ebpf_inst> res;
-    auto pc_of_label = get_labels(insts);
+    const auto pc_of_label = get_labels(insts);
     pc_t pc = 0;
     for (auto [label, ins, _] : insts) {
         (void)label; // unused
diff --git a/src/crab/array_domain.cpp b/src/crab/array_domain.cpp
index 798e626ba..de0550849 100644
--- a/src/crab/array_domain.cpp
+++ b/src/crab/array_domain.cpp
@@ -19,6 +19,8 @@
 
 namespace crab::domains {
 
+using index_t = uint64_t;
+
 static bool maybe_between(const NumAbsDomain& dom, const extended_number& x, const linear_expression_t& symb_lb,
                           const linear_expression_t& symb_ub) {
     using namespace dsl_syntax;
@@ -60,7 +62,7 @@ int radix_length(const offset_t& offset) {
 // Get a range of bits out of the middle of a key, starting at [begin] for a given length.
 [[maybe_unused]]
 offset_t radix_substr(const offset_t& key, const int begin, const int length) {
-    uint64_t mask;
+    index_t mask;
 
     if (length == offset_t::bitsize) {
         mask = 0;
@@ -79,11 +81,8 @@ offset_t radix_substr(const offset_t& key, const int begin, const int length) {
 // Concatenate two bit patterns.
 [[maybe_unused]]
 offset_t radix_join(const offset_t& entry1, const offset_t& entry2) {
-    const index_t value1 = (index_t)entry1;
-    const index_t value2 = (index_t)entry2;
-    const index_t value = value1 | (value2 >> entry1.prefix_length());
+    const index_t value = entry1 | (entry2 >> entry1.prefix_length());
     const int prefix_length = entry1.prefix_length() + entry2.prefix_length();
-
     return offset_t{value, prefix_length};
 }
 
@@ -491,7 +490,7 @@ void array_domain_t::split_number_var(NumAbsDomain& inv, data_kind_t kind, const
         return;
     }
     auto size = static_cast<unsigned int>(*n_bytes);
-    offset_t o(static_cast<uint64_t>(*n));
+    offset_t o(static_cast<index_t>(*n));
 
     std::vector<cell_t> cells = offset_map.get_overlap_cells(o, size);
     for (cell_t const& c : cells) {
@@ -500,7 +499,7 @@ void array_domain_t::split_number_var(NumAbsDomain& inv, data_kind_t kind, const
         int cell_end_index = static_cast<int>(*intv.ub().number());
 
         if (!this->num_bytes.all_num(cell_start_index, cell_end_index + 1) ||
-            cell_end_index + 1 < cell_start_index + sizeof(int64_t)) {
+            cell_end_index + 1UL < cell_start_index + sizeof(int64_t)) {
             // We can only split numeric cells of size 8 or less.
             continue;
         }
@@ -509,11 +508,11 @@ void array_domain_t::split_number_var(NumAbsDomain& inv, data_kind_t kind, const
             // We can only split cells with a singleton value.
             continue;
         }
-        if (cell_start_index < o) {
+        if (static_cast<index_t>(cell_start_index) < o) {
             // Use the bytes to the left of the specified range.
             split_cell(inv, kind, cell_start_index, static_cast<unsigned int>(o - cell_start_index));
         }
-        if (o + size - 1 < cell_end_index) {
+        if (o + size < cell_end_index + 1UL) {
             // Use the bytes to the right of the specified range.
             split_cell(inv, kind, static_cast<int>(o + size),
                        static_cast<unsigned int>(cell_end_index - (o + size - 1)));
@@ -535,7 +534,7 @@ static std::optional<std::pair<offset_t, unsigned>> kill_and_find_var(NumAbsDoma
         if (auto n_bytes = i_elem_size.singleton()) {
             auto size = static_cast<unsigned int>(*n_bytes);
             // -- Constant index: kill overlapping cells
-            offset_t o(static_cast<uint64_t>(*n));
+            offset_t o(static_cast<index_t>(*n));
             cells = offset_map.get_overlap_cells(o, size);
             res = std::make_pair(o, size);
         }
@@ -599,7 +598,7 @@ std::optional<uint8_t> get_value_byte(const NumAbsDomain& inv, const offset_t o,
     if (!t) {
         return {};
     }
-    uint64_t n = t->cast_to<uint64_t>();
+    index_t n = t->cast_to<index_t>();
 
     // Convert value to bytes of the appropriate endian-ness.
     switch (width) {
@@ -618,11 +617,11 @@ std::optional<uint8_t> get_value_byte(const NumAbsDomain& inv, const offset_t o,
             n = boost::endian::native_to_little<uint32_t>(n);
         }
         break;
-    case sizeof(uint64_t):
+    case sizeof(index_t):
         if (thread_local_options.big_endian) {
-            n = boost::endian::native_to_big<uint64_t>(n);
+            n = boost::endian::native_to_big<index_t>(n);
         } else {
-            n = boost::endian::native_to_little<uint64_t>(n);
+            n = boost::endian::native_to_little<index_t>(n);
         }
         break;
     default: CRAB_ERROR("Unexpected width ", width);
@@ -700,11 +699,11 @@ std::optional<linear_expression_t> array_domain_t::load(const NumAbsDomain& inv,
                     return b;
                 }
                 if (size == 8) {
-                    uint64_t b = *reinterpret_cast<uint64_t*>(result_buffer);
+                    index_t b = *reinterpret_cast<index_t*>(result_buffer);
                     if (thread_local_options.big_endian) {
-                        b = boost::endian::native_to_big<uint64_t>(b);
+                        b = boost::endian::native_to_big<index_t>(b);
                     } else {
-                        b = boost::endian::native_to_little<uint64_t>(b);
+                        b = boost::endian::native_to_little<index_t>(b);
                     }
                     return kind == data_kind_t::uvalues ? number_t(b) : number_t(static_cast<int64_t>(b));
                 }
diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp
index a4534c9e8..f3c35cbf8 100644
--- a/src/crab/ebpf_domain.cpp
+++ b/src/crab/ebpf_domain.cpp
@@ -2510,6 +2510,9 @@ void ebpf_domain_t::operator()(const Bin& bin) {
             type_inv.assign_type(m_inv, bin.dst, T_NUM);
             havoc_offsets(bin.dst);
             break;
+        case Bin::Op::MOVSX8:
+        case Bin::Op::MOVSX16:
+        case Bin::Op::MOVSX32: CRAB_ERROR("Unsupported operation");
         case Bin::Op::ADD:
             if (imm == 0) {
                 return;
diff --git a/src/crab/split_dbm.cpp b/src/crab/split_dbm.cpp
index 4baee4589..1672db5c3 100644
--- a/src/crab/split_dbm.cpp
+++ b/src/crab/split_dbm.cpp
@@ -1168,7 +1168,7 @@ string_invariant SplitDBM::to_set() const {
 std::ostream& operator<<(std::ostream& o, const SplitDBM& dom) { return o << dom.to_set(); }
 
 bool SplitDBM::eval_expression_overflow(const linear_expression_t& e, Weight& out) const {
-    bool overflow = convert_NtoW_overflow(e.constant_term(), out);
+    [[maybe_unused]] bool overflow = convert_NtoW_overflow(e.constant_term(), out);
     assert(!overflow);
     for (const auto& [variable, coefficient] : e.variable_terms()) {
         Weight coef;
diff --git a/src/crab/variable.hpp b/src/crab/variable.hpp
index bf768e629..9267f7876 100644
--- a/src/crab/variable.hpp
+++ b/src/crab/variable.hpp
@@ -11,10 +11,6 @@
 #include "crab_utils/lazy_allocator.hpp"
 #include "crab_utils/num_big.hpp"
 
-using index_t = uint64_t;
-
-/* Basic type definitions */
-
 namespace crab {
 
 std::vector<std::string> default_variable_names();
@@ -22,22 +18,22 @@ std::vector<std::string> default_variable_names();
 // Wrapper for typed variables used by the crab abstract domains and linear_constraints.
 // Being a class (instead of a type alias) enables overloading in dsl_syntax
 class variable_t final {
-    index_t _id;
+    uint64_t _id;
 
-    explicit variable_t(index_t id) : _id(id) {}
+    explicit variable_t(const uint64_t id) : _id(id) {}
 
   public:
     [[nodiscard]]
     std::size_t hash() const {
-        return (size_t)_id;
+        return _id;
     }
 
-    bool operator==(variable_t o) const { return _id == o._id; }
+    bool operator==(const variable_t o) const { return _id == o._id; }
 
-    bool operator!=(variable_t o) const { return (!(operator==(o))); }
+    bool operator!=(const variable_t o) const { return (!(operator==(o))); }
 
     // for flat_map
-    bool operator<(variable_t o) const { return _id < o._id; }
+    bool operator<(const variable_t o) const { return _id < o._id; }
 
     [[nodiscard]]
     std::string name() const {
@@ -54,7 +50,7 @@ class variable_t final {
         return names->at(_id).find(".uvalue") != std::string::npos;
     }
 
-    friend std::ostream& operator<<(std::ostream& o, variable_t v) { return o << names->at(v._id); }
+    friend std::ostream& operator<<(std::ostream& o, const variable_t v) { return o << names->at(v._id); }
 
     // var_factory portion.
     // This singleton is eBPF-specific, to avoid lifetime issues and/or passing factory explicitly everywhere: