diff --git a/CMakeLists.txt b/CMakeLists.txt
index fd3a90f3a..b18b7801e 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -1,70 +1,81 @@
 # Copyright (c) Prevail Verifier contributors.
 # SPDX-License-Identifier: MIT
-cmake_minimum_required(VERSION 3.10)
+cmake_minimum_required(VERSION 3.14)
 project(ebpf_verifier)
 
 include(FetchContent)
-FetchContent_Declare(
-  Catch2
-  GIT_REPOSITORY https://github.com/catchorg/Catch2.git
-  GIT_TAG        fa43b77429ba76c462b1898d6cd2f2d7a9416b14 # v3.7.1
+
+FetchContent_Declare(GSL
+        GIT_REPOSITORY "https://github.com/microsoft/GSL"
+        GIT_TAG "v4.0.0"
+        GIT_SHALLOW ON
+)
+FetchContent_MakeAvailable(GSL)
+get_target_property(GSL_INCLUDE_DIRS Microsoft.GSL::GSL INTERFACE_INCLUDE_DIRECTORIES)
+
+FetchContent_Declare(Catch2
+        GIT_REPOSITORY "https://github.com/catchorg/Catch2.git"
+        GIT_TAG "v3.7.1"
+        GIT_SHALLOW ON
 )
 FetchContent_MakeAvailable(Catch2)
 
 if (IS_DIRECTORY "${PROJECT_SOURCE_DIR}/.git")
-  # Install Git pre-commit hook
-  file(COPY scripts/pre-commit scripts/commit-msg
-       DESTINATION "${PROJECT_SOURCE_DIR}/.git/hooks")
+    # Install Git pre-commit hook
+    file(COPY scripts/pre-commit scripts/commit-msg
+            DESTINATION "${PROJECT_SOURCE_DIR}/.git/hooks")
 endif ()
 
 if ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU" OR
-    "${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")
-  find_package(yaml-cpp REQUIRED)
-  find_package(Boost REQUIRED)
-  set(CMAKE_CXX_STANDARD 20)
+        "${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")
+    find_package(yaml-cpp REQUIRED)
+    find_package(Boost REQUIRED)
+    set(CMAKE_CXX_STANDARD 20)
+    set(CMAKE_CXX_STANDARD_REQUIRED ON)
 elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
-  list(APPEND CMAKE_CONFIGURATION_TYPES FuzzerDebug)
-  list(REMOVE_DUPLICATES CMAKE_CONFIGURATION_TYPES)
-  set(CMAKE_CONFIGURATION_TYPES "${CMAKE_CONFIGURATION_TYPES}" CACHE STRING
-      "Add the configurations that we need"
-      FORCE)
-  set(CMAKE_EXE_LINKER_FLAGS_FUZZERDEBUG "${CMAKE_EXE_LINKER_FLAGS_DEBUG}")
-  set(CMAKE_SHARED_LINKER_FLAGS_FUZZERDEBUG "${CMAKE_SHARED_LINKER_FLAGS_DEBUG}")
-  set(CMAKE_C_FLAGS_FUZZERDEBUG "${CMAKE_C_FLAGS_DEBUG} /fsanitize=address /fsanitize=fuzzer /fsanitize-coverage=inline-bool-flag /fsanitize-coverage=edge /fsanitize-coverage=trace-cmp /fsanitize-coverage=trace-div /ZH:SHA_256")
-  set(CMAKE_CXX_FLAGS_FUZZERDEBUG "${CMAKE_CXX_FLAGS_DEBUG} /fsanitize=address /fsanitize=fuzzer /fsanitize-coverage=inline-bool-flag /fsanitize-coverage=edge /fsanitize-coverage=trace-cmp /fsanitize-coverage=trace-div /ZH:SHA_256")
-
-  find_program(NUGET nuget)
-  if (NOT NUGET)
-    message("ERROR: You must first install nuget.exe from https://www.nuget.org/downloads")
-  else ()
-    execute_process(COMMAND ${NUGET} install "Boost" -Version 1.81.0 -ExcludeVersion -OutputDirectory ${CMAKE_BINARY_DIR}/packages)
-    set(BOOST_VERSION 1.81.0)
-  endif()
-  set(Boost_INCLUDE_DIRS ${CMAKE_BINARY_DIR}/packages/boost/lib/native/include)
-  set(Boost_LIBRARY_DIRS ${CMAKE_BINARY_DIR}/packages/boost_filesystem-vc143/lib/native)
-
-  # MSVC's "std:c++20" option is the current standard that supports all the C++17
-  # features we use. However, cmake can't deal with that here, so we set it below.
-
-  set(EXTERNAL_INSTALL_LOCATION ${CMAKE_BINARY_DIR}/packages/yaml-cpp)
-  include(ExternalProject)
-  ExternalProject_Add(yaml-cpp
-          GIT_REPOSITORY https://github.com/jbeder/yaml-cpp.git
-          GIT_TAG "yaml-cpp-0.7.0"
-          GIT_SHALLOW true
-          CMAKE_ARGS -DCMAKE_INSTALL_PREFIX=${EXTERNAL_INSTALL_LOCATION}
-                     -DYAML_MSVC_SHARED_RT=ON
-                     -DYAML_CPP_BUILD_TESTS=OFF
-                     -DYAML_CPP_BUILD_TOOLS=OFF
-          )
-  set(YAML_CPP_LIBRARIES ${EXTERNAL_INSTALL_LOCATION}/lib/yaml-cpp$<$<CONFIG:DEBUG>:d>.lib)
-  set(YAML_CPP_INCLUDE_DIRS ${EXTERNAL_INSTALL_LOCATION}/include/)
+    list(APPEND CMAKE_CONFIGURATION_TYPES FuzzerDebug)
+    list(REMOVE_DUPLICATES CMAKE_CONFIGURATION_TYPES)
+    set(CMAKE_CONFIGURATION_TYPES "${CMAKE_CONFIGURATION_TYPES}" CACHE STRING
+            "Add the configurations that we need"
+            FORCE)
+    set(CMAKE_EXE_LINKER_FLAGS_FUZZERDEBUG "${CMAKE_EXE_LINKER_FLAGS_DEBUG}")
+    set(CMAKE_SHARED_LINKER_FLAGS_FUZZERDEBUG "${CMAKE_SHARED_LINKER_FLAGS_DEBUG}")
+    set(CMAKE_C_FLAGS_FUZZERDEBUG "${CMAKE_C_FLAGS_DEBUG} /fsanitize=address /fsanitize=fuzzer /fsanitize-coverage=inline-bool-flag /fsanitize-coverage=edge /fsanitize-coverage=trace-cmp /fsanitize-coverage=trace-div /ZH:SHA_256")
+    set(CMAKE_CXX_FLAGS_FUZZERDEBUG "${CMAKE_CXX_FLAGS_DEBUG} /fsanitize=address /fsanitize=fuzzer /fsanitize-coverage=inline-bool-flag /fsanitize-coverage=edge /fsanitize-coverage=trace-cmp /fsanitize-coverage=trace-div /ZH:SHA_256")
+
+    find_program(NUGET nuget)
+    if (NOT NUGET)
+        message("ERROR: You must first install nuget.exe from https://www.nuget.org/downloads")
+    else ()
+        execute_process(COMMAND ${NUGET} install "Boost" -Version 1.81.0 -ExcludeVersion -OutputDirectory ${CMAKE_BINARY_DIR}/packages)
+        set(BOOST_VERSION 1.81.0)
+    endif ()
+    set(Boost_INCLUDE_DIRS ${CMAKE_BINARY_DIR}/packages/boost/lib/native/include)
+    set(Boost_LIBRARY_DIRS ${CMAKE_BINARY_DIR}/packages/boost_filesystem-vc143/lib/native)
+
+    # MSVC's "std:c++20" option is the current standard that supports all the C++17
+    # features we use. However, cmake can't deal with that here, so we set it below.
+
+    set(EXTERNAL_INSTALL_LOCATION ${CMAKE_BINARY_DIR}/packages/yaml-cpp)
+    include(ExternalProject)
+    ExternalProject_Add(yaml-cpp
+            GIT_REPOSITORY https://github.com/jbeder/yaml-cpp.git
+            GIT_TAG "yaml-cpp-0.7.0"
+            GIT_SHALLOW true
+            CMAKE_ARGS -DCMAKE_INSTALL_PREFIX=${EXTERNAL_INSTALL_LOCATION}
+            -DYAML_MSVC_SHARED_RT=ON
+            -DYAML_CPP_BUILD_TESTS=OFF
+            -DYAML_CPP_BUILD_TOOLS=OFF
+    )
+    set(YAML_CPP_LIBRARIES ${EXTERNAL_INSTALL_LOCATION}/lib/yaml-cpp$<$<CONFIG:DEBUG>:d>.lib)
+    set(YAML_CPP_INCLUDE_DIRS ${EXTERNAL_INSTALL_LOCATION}/include/)
 endif ()
 
 include_directories(./external)
 include_directories(./external/bpf_conformance/external/elfio)
 include_directories(./src)
 include_directories(./external/libbtf)
+include_directories(${GSL_INCLUDE_DIRS})
 include_directories(${Boost_INCLUDE_DIRS})
 include_directories(${YAML_CPP_INCLUDE_DIRS})
 link_directories(${Boost_LIBRARY_DIRS})
@@ -73,31 +84,30 @@ file(GLOB LIB_SRC
         "./src/*.cpp"
         "./src/crab/*.cpp"
         "./src/crab_utils/*.cpp"
-        "./src/linux/gpl/*.cpp"
+        "./src/linux/gpl/spec_prototypes.cpp"
         "./src/linux/linux_platform.cpp"
-        )
+)
 
 file(GLOB ALL_TEST
-        "./src/test/test.cpp"
         "./src/test/test_conformance.cpp"
         "./src/test/test_marshal.cpp"
         "./src/test/test_print.cpp"
         "./src/test/test_verify.cpp"
         "./src/test/test_wto.cpp"
         "./src/test/test_yaml.cpp"
-        )
+)
 
 if ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU" OR
-    "${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang")
-  set(COMMON_FLAGS -Wall -Wfatal-errors -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8)
+        "${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang")
+    set(COMMON_FLAGS -Wall -Wfatal-errors -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8)
 
-  set(RELEASE_FLAGS -O2 -flto=auto -ffat-lto-objects)
+    set(RELEASE_FLAGS -O2 -flto=auto -ffat-lto-objects)
 
-  set(DEBUG_FLAGS -O0 -g3 -fno-omit-frame-pointer)
+    set(DEBUG_FLAGS -O0 -g3 -fno-omit-frame-pointer)
 
-  set(SANITIZE_FLAGS -fsanitize=address -O1 -fno-omit-frame-pointer)
+    set(SANITIZE_FLAGS -fsanitize=address -O1 -fno-omit-frame-pointer)
 elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
-  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} /std:c++20")
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} /std:c++20")
 endif ()
 
 add_library(ebpfverifier ${LIB_SRC})
@@ -107,6 +117,8 @@ add_executable(tests ${ALL_TEST})
 add_executable(run_yaml src/main/run_yaml.cpp)
 add_executable(conformance_check src/test/conformance_check.cpp)
 
+target_include_directories(ebpfverifier PRIVATE ${GSL_INCLUDE_DIRS})
+
 set_target_properties(check
         PROPERTIES
         RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/..")
@@ -141,6 +153,14 @@ add_subdirectory("external/libbtf")
 set(ebpfverifier_GUID_CMAKE "7d5b4e68-c0fa-3f86-9405-f6400219b440" CACHE INTERNAL "Project GUID")
 set(yaml-cpp_GUID_CMAKE "98d56b8a-d8eb-3d98-b8ee-c83696b4d58a" CACHE INTERNAL "Project GUID")
 
+set(THREADS_PREFER_PTHREAD_FLAG ON)
+find_package(Threads REQUIRED)
+
+target_link_libraries(ebpfverifier PRIVATE ${YAML_CPP_LIBRARIES})
+target_link_libraries(ebpfverifier PRIVATE libbtf)
+target_link_libraries(ebpfverifier PRIVATE Microsoft.GSL::GSL)
+target_compile_options(ebpfverifier PRIVATE ${COMMON_FLAGS})
+
 target_compile_options(check PRIVATE ${COMMON_FLAGS})
 target_compile_options(check PUBLIC "$<$<CONFIG:DEBUG>:${DEBUG_FLAGS}>")
 target_compile_options(check PUBLIC "$<$<CONFIG:RELEASE>:${RELEASE_FLAGS}>")
@@ -155,16 +175,9 @@ target_compile_options(tests PUBLIC "$<$<CONFIG:SANITIZE>:${SANITIZE_FLAGS}>")
 target_link_libraries(tests PRIVATE ebpfverifier)
 target_link_libraries(tests PRIVATE bpf_conformance)
 target_link_libraries(tests PRIVATE ${CMAKE_DL_LIBS})
-
-set(THREADS_PREFER_PTHREAD_FLAG ON)
-find_package(Threads REQUIRED)
-
 target_link_libraries(tests PRIVATE Threads::Threads)
 target_link_libraries(tests PRIVATE Catch2::Catch2WithMain)
 
-target_link_libraries(ebpfverifier PRIVATE ${YAML_CPP_LIBRARIES})
-target_link_libraries(ebpfverifier PRIVATE libbtf)
-target_compile_options(ebpfverifier PRIVATE ${COMMON_FLAGS})
-
 target_link_libraries(run_yaml PRIVATE ebpfverifier)
+
 target_link_libraries(conformance_check PRIVATE ebpfverifier)
diff --git a/src/crab/array_domain.cpp b/src/crab/array_domain.cpp
index de0550849..22c2f0f78 100644
--- a/src/crab/array_domain.cpp
+++ b/src/crab/array_domain.cpp
@@ -489,14 +489,14 @@ void array_domain_t::split_number_var(NumAbsDomain& inv, data_kind_t kind, const
         // We can only split a singleton size.
         return;
     }
-    auto size = static_cast<unsigned int>(*n_bytes);
-    offset_t o(static_cast<index_t>(*n));
+    auto size = n_bytes->narrow<unsigned int>();
+    offset_t o(n->narrow<index_t>());
 
     std::vector<cell_t> cells = offset_map.get_overlap_cells(o, size);
     for (cell_t const& c : cells) {
         interval_t intv = c.to_interval();
-        int cell_start_index = static_cast<int>(*intv.lb().number());
-        int cell_end_index = static_cast<int>(*intv.ub().number());
+        int cell_start_index = intv.lb().narrow<int>();
+        int cell_end_index = intv.ub().narrow<int>();
 
         if (!this->num_bytes.all_num(cell_start_index, cell_end_index + 1) ||
             cell_end_index + 1UL < cell_start_index + sizeof(int64_t)) {
@@ -532,9 +532,9 @@ static std::optional<std::pair<offset_t, unsigned>> kill_and_find_var(NumAbsDoma
     if (std::optional<number_t> n = ii.singleton()) {
         interval_t i_elem_size = inv.eval_interval(elem_size);
         if (auto n_bytes = i_elem_size.singleton()) {
-            auto size = static_cast<unsigned int>(*n_bytes);
+            auto size = n_bytes->narrow<unsigned int>();
             // -- Constant index: kill overlapping cells
-            offset_t o(static_cast<index_t>(*n));
+            offset_t o(n->narrow<index_t>());
             cells = offset_map.get_overlap_cells(o, size);
             res = std::make_pair(o, size);
         }
@@ -576,7 +576,7 @@ bool array_domain_t::all_num(const NumAbsDomain& inv, const linear_expression_t&
         return true;
     }
 
-    return this->num_bytes.all_num(static_cast<int32_t>(*min_lb), static_cast<int32_t>(*max_ub));
+    return this->num_bytes.all_num(min_lb->narrow<int32_t>(), max_ub->narrow<int32_t>());
 }
 
 // Get the number of bytes, starting at offset, that are known to be numbers.
@@ -586,8 +586,8 @@ int array_domain_t::min_all_num_size(const NumAbsDomain& inv, const variable_t o
     if (!min_lb || !max_ub || !min_lb->fits<int32_t>() || !max_ub->fits<int32_t>()) {
         return 0;
     }
-    const auto lb = static_cast<int>(min_lb.value());
-    const auto ub = static_cast<int>(max_ub.value());
+    const auto lb = min_lb->narrow<int>();
+    const auto ub = max_ub->narrow<int>();
     return std::max(0, this->num_bytes.all_num_width(lb) - (ub - lb));
 }
 
@@ -635,7 +635,7 @@ std::optional<linear_expression_t> array_domain_t::load(const NumAbsDomain& inv,
     interval_t ii = inv.eval_interval(i);
     if (std::optional<number_t> n = ii.singleton()) {
         offset_map_t& offset_map = lookup_array_map(kind);
-        int64_t k = static_cast<int64_t>(*n);
+        int64_t k = n->narrow<int64_t>();
         if (kind == data_kind_t::types) {
             auto [only_num, only_non_num] = num_bytes.uniformity(k, width);
             if (only_num) {
@@ -730,9 +730,9 @@ std::optional<linear_expression_t> array_domain_t::load(const NumAbsDomain& inv,
         auto ub = ii.ub().number();
         if (lb.has_value() && ub.has_value()) {
             number_t fullwidth = ub.value() - lb.value() + width;
-            if (lb.value().fits<uint32_t>() && fullwidth.fits<uint32_t>()) {
+            if (lb->fits<uint32_t>() && fullwidth.fits<uint32_t>()) {
                 auto [only_num, only_non_num] =
-                    num_bytes.uniformity(static_cast<uint32_t>(lb.value()), static_cast<uint32_t>(fullwidth));
+                    num_bytes.uniformity(lb->narrow<uint32_t>(), fullwidth.narrow<uint32_t>());
                 if (only_num) {
                     return T_NUM;
                 }
@@ -766,7 +766,7 @@ std::optional<variable_t> array_domain_t::store(NumAbsDomain& inv, const data_ki
         auto [offset, size] = *maybe_cell;
         if (kind == data_kind_t::types) {
             const std::optional<number_t> t = inv.eval_interval(val).singleton();
-            if (t && static_cast<int64_t>(*t) == T_NUM) {
+            if (t == number_t{T_NUM}) {
                 num_bytes.reset(offset, size);
             } else {
                 num_bytes.havoc(offset, size);
@@ -786,7 +786,7 @@ std::optional<variable_t> array_domain_t::store_type(NumAbsDomain& inv, const li
         // perform strong update
         auto [offset, size] = *maybe_cell;
         const std::optional<number_t> t = inv.eval_interval(val).singleton();
-        if (t && static_cast<int64_t>(*t) == T_NUM) {
+        if (t == number_t{T_NUM}) {
             num_bytes.reset(offset, size);
         } else {
             num_bytes.havoc(offset, size);
@@ -837,7 +837,7 @@ void array_domain_t::store_numbers(const NumAbsDomain& inv, const variable_t _id
                   "the number of elements is larger than default limit of ", max_num_elems);
         return;
     }
-    num_bytes.reset(static_cast<int>(*idx_n), static_cast<int>(*width));
+    num_bytes.reset(idx_n->narrow<size_t>(), width->narrow<int>());
 }
 
 void array_domain_t::set_to_top() { num_bytes.set_to_top(); }
diff --git a/src/crab/cfg.hpp b/src/crab/cfg.hpp
index 8ff0792ff..d9527b2d2 100644
--- a/src/crab/cfg.hpp
+++ b/src/crab/cfg.hpp
@@ -20,14 +20,12 @@
 
 #include <boost/iterator/transform_iterator.hpp>
 #include <boost/lexical_cast.hpp>
-#include <boost/range/iterator_range.hpp>
-
-#include "crab/variable.hpp"
-#include "crab_utils/debug.hpp"
-#include "crab_utils/num_big.hpp"
+#include <gsl/gsl>
 
 #include "asm_ostream.hpp"
 #include "asm_syntax.hpp"
+#include "crab_utils/debug.hpp"
+#include "crab_utils/num_big.hpp"
 #include "spec_type_descriptors.hpp"
 
 namespace crab {
@@ -100,7 +98,7 @@ class basic_block_t final {
 
     [[nodiscard]]
     size_t size() const {
-        return static_cast<size_t>(std::distance(begin(), end()));
+        return gsl::narrow<size_t>(std::distance(begin(), end()));
     }
 
     [[nodiscard]]
@@ -195,7 +193,7 @@ class basic_block_rev_t final {
 
     [[nodiscard]]
     std::size_t size() const {
-        return static_cast<size_t>(std::distance(begin(), end()));
+        return gsl::narrow<size_t>(std::distance(begin(), end()));
     }
 
     [[nodiscard]]
@@ -382,7 +380,7 @@ class cfg_t final {
 
     [[nodiscard]]
     size_t size() const {
-        return static_cast<size_t>(std::distance(begin(), end()));
+        return gsl::narrow<size_t>(std::distance(begin(), end()));
     }
 
     void simplify() {
diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp
index f3c35cbf8..d72b6b9cd 100644
--- a/src/crab/ebpf_domain.cpp
+++ b/src/crab/ebpf_domain.cpp
@@ -1449,8 +1449,8 @@ bool ebpf_domain_t::get_map_fd_range(const Reg& map_fd_reg, int32_t* start_fd, i
     if (!lb || !lb->fits<int32_t>() || !ub || !ub->fits<int32_t>()) {
         return false;
     }
-    *start_fd = static_cast<int32_t>(lb.value());
-    *end_fd = static_cast<int32_t>(ub.value());
+    *start_fd = lb->narrow<int32_t>();
+    *end_fd = ub->narrow<int32_t>();
 
     // Cap the maximum range we'll check.
     constexpr int max_range = 32;
@@ -1578,14 +1578,14 @@ void ebpf_domain_t::operator()(const ValidMapKeyValue& s) {
             require(m_inv, linear_constraint_t::false_const(), "Map key size is not singleton");
             return;
         }
-        width = static_cast<int>(key_size.value());
+        width = key_size->narrow<int>();
     } else {
         const auto value_size = get_map_value_size(s.map_fd_reg).singleton();
         if (!value_size.has_value()) {
             require(m_inv, linear_constraint_t::false_const(), "Map value size is not singleton");
             return;
         }
-        width = static_cast<int>(value_size.value());
+        width = value_size->narrow<int>();
     }
 
     m_inv = type_inv.join_over_types(m_inv, s.access_reg, [&](NumAbsDomain& inv, type_encoding_t access_reg_type) {
@@ -1594,11 +1594,9 @@ void ebpf_domain_t::operator()(const ValidMapKeyValue& s) {
             linear_expression_t ub = lb + width;
             if (!stack.all_num(inv, lb, ub)) {
                 auto lb_is = inv[lb].lb().number();
-                std::string lb_s =
-                    lb_is && lb_is->fits<int32_t>() ? std::to_string(static_cast<int32_t>(*lb_is)) : "-oo";
+                std::string lb_s = lb_is && lb_is->fits<int32_t>() ? std::to_string(lb_is->narrow<int32_t>()) : "-oo";
                 auto ub_is = inv.eval_interval(ub).ub().number();
-                std::string ub_s =
-                    ub_is && ub_is->fits<int32_t>() ? std::to_string(static_cast<int32_t>(*ub_is)) : "oo";
+                std::string ub_s = ub_is && ub_is->fits<int32_t>() ? std::to_string(ub_is->narrow<int32_t>()) : "oo";
                 require(inv, linear_constraint_t::false_const(),
                         "Illegal map update with a non-numerical value [" + lb_s + "-" + ub_s + ")");
             } else if (thread_local_options.strict && fd_type.has_value()) {
@@ -2377,7 +2375,7 @@ void ebpf_domain_t::lshr(const Reg& dst_reg, int imm, int finite_width) {
             }
         }
         m_inv.set(dst.uvalue, interval_t{lb_n, ub_n});
-        if (static_cast<int64_t>(ub_n) >= static_cast<int64_t>(lb_n)) {
+        if (ub_n.narrow<int64_t>() >= lb_n.narrow<int64_t>()) {
             // ? m_inv.set(dst.svalue, crab::interval_t{number_t{(int64_t)lb_n}, number_t{(int64_t)ub_n}});
             m_inv.assign(dst.svalue, dst.uvalue);
         } else {
@@ -2453,8 +2451,7 @@ void ebpf_domain_t::ashr(const Reg& dst_reg, const linear_expression_t& right_sv
             int64_t lb_n = std::numeric_limits<int64_t>::min() >> imm;
             int64_t ub_n = std::numeric_limits<int64_t>::max() >> imm;
             if (left_interval.finite_size()) {
-                number_t lb = left_interval.lb().number().value();
-                number_t ub = left_interval.ub().number().value();
+                const auto [lb, ub] = left_interval.pair_number();
                 if (finite_width == 64) {
                     lb_n = lb.cast_to<int64_t>() >> imm;
                     ub_n = ub.cast_to<int64_t>() >> imm;
@@ -2882,8 +2879,8 @@ ebpf_domain_t ebpf_domain_t::from_constraints(const std::set<std::string>& const
         inv += cst;
     }
     for (const interval_t& range : numeric_ranges) {
-        const int start = static_cast<int>(range.lb().number().value());
-        const int width = 1 + static_cast<int>(range.finite_size().value());
+        const int start = range.lb().narrow<int>();
+        const int width = 1 + range.finite_size()->narrow<int>();
         inv.stack.initialize_numbers(start, width);
     }
     // TODO: handle other stack type constraints
diff --git a/src/crab/interval.hpp b/src/crab/interval.hpp
index 22d5124f5..657b8f694 100644
--- a/src/crab/interval.hpp
+++ b/src/crab/interval.hpp
@@ -24,9 +24,9 @@ class interval_t final {
     bound_t _ub;
 
   public:
-    static interval_t top() { return interval_t(bound_t::minus_infinity(), bound_t::plus_infinity()); }
+    static interval_t top() { return interval_t{bound_t::minus_infinity(), bound_t::plus_infinity()}; }
 
-    static interval_t bottom() { return interval_t(); }
+    static interval_t bottom() { return interval_t{}; }
 
     [[nodiscard]]
     std::optional<number_t> finite_size() const {
@@ -86,14 +86,25 @@ class interval_t final {
         return {_lb, _ub};
     }
 
+    template <std::integral T>
+    [[nodiscard]]
+    std::tuple<T, T> pair() const {
+        return {_lb.narrow<T>(), _ub.narrow<T>()};
+    }
+
+    [[nodiscard]]
+    std::tuple<number_t, number_t> pair_number() const {
+        return {_lb.number().value(), _ub.number().value()};
+    }
+
     template <std::integral T>
     [[nodiscard]]
     std::tuple<T, T> bound(T lb, T ub) const {
-        interval_t b = interval_t(lb, ub) & *this;
+        const interval_t b = interval_t{lb, ub} & *this;
         if (b.is_bottom()) {
             CRAB_ERROR("Cannot convert bottom to tuple");
         }
-        return {static_cast<T>(*b._lb.number()), static_cast<T>(*b._ub.number())};
+        return {b._lb.narrow<T>(), b._ub.narrow<T>()};
     }
 
     template <is_enum T>
@@ -139,7 +150,7 @@ class interval_t final {
         } else if (x.is_bottom()) {
             return *this;
         } else {
-            return interval_t(std::min(_lb, x._lb), std::max(_ub, x._ub));
+            return interval_t{std::min(_lb, x._lb), std::max(_ub, x._ub)};
         }
     }
 
@@ -147,7 +158,7 @@ class interval_t final {
         if (is_bottom() || x.is_bottom()) {
             return bottom();
         } else {
-            return interval_t(std::max(_lb, x._lb), std::min(_ub, x._ub));
+            return interval_t{std::max(_lb, x._lb), std::min(_ub, x._ub)};
         }
     }
 
@@ -158,8 +169,8 @@ class interval_t final {
         } else if (x.is_bottom()) {
             return *this;
         } else {
-            return interval_t(x._lb < _lb ? bound_t::minus_infinity() : _lb,
-                              _ub < x._ub ? bound_t::plus_infinity() : _ub);
+            return interval_t{x._lb < _lb ? bound_t::minus_infinity() : _lb,
+                              _ub < x._ub ? bound_t::plus_infinity() : _ub};
         }
     }
 
@@ -170,9 +181,9 @@ class interval_t final {
         } else if (x.is_bottom()) {
             return *this;
         } else {
-            bound_t lb = (x._lb < _lb ? ts.get_prev(x._lb) : _lb);
-            bound_t ub = (_ub < x._ub ? ts.get_next(x._ub) : _ub);
-            return interval_t(lb, ub);
+            bound_t lb = x._lb < _lb ? ts.get_prev(x._lb) : _lb;
+            bound_t ub = _ub < x._ub ? ts.get_next(x._ub) : _ub;
+            return interval_t{lb, ub};
         }
     }
 
@@ -181,8 +192,8 @@ class interval_t final {
         if (is_bottom() || x.is_bottom()) {
             return bottom();
         } else {
-            return interval_t(_lb.is_infinite() && x._lb.is_finite() ? x._lb : _lb,
-                              _ub.is_infinite() && x._ub.is_finite() ? x._ub : _ub);
+            return interval_t{_lb.is_infinite() && x._lb.is_finite() ? x._lb : _lb,
+                              _ub.is_infinite() && x._ub.is_finite() ? x._ub : _ub};
         }
     }
 
@@ -190,7 +201,7 @@ class interval_t final {
         if (is_bottom() || x.is_bottom()) {
             return bottom();
         } else {
-            return interval_t(_lb + x._lb, _ub + x._ub);
+            return interval_t{_lb + x._lb, _ub + x._ub};
         }
     }
 
@@ -200,7 +211,7 @@ class interval_t final {
         if (is_bottom()) {
             return bottom();
         } else {
-            return interval_t(-_ub, -_lb);
+            return interval_t{-_ub, -_lb};
         }
     }
 
@@ -208,7 +219,7 @@ class interval_t final {
         if (is_bottom() || x.is_bottom()) {
             return bottom();
         } else {
-            return interval_t(_lb - x._ub, _ub - x._lb);
+            return interval_t{_lb - x._ub, _ub - x._lb};
         }
     }
 
@@ -222,7 +233,7 @@ class interval_t final {
             bound_t lu = _lb * x._ub;
             bound_t ul = _ub * x._lb;
             bound_t uu = _ub * x._ub;
-            return interval_t(std::min({ll, lu, ul, uu}), std::max({ll, lu, ul, uu}));
+            return interval_t{std::min({ll, lu, ul, uu}), std::max({ll, lu, ul, uu})};
         }
     }
 
@@ -339,7 +350,7 @@ class interval_t final {
                 T lub = ub().number()->truncate_to<T>();
                 if (llb <= lub) {
                     // Interval can be accurately represented in 64 width.
-                    return interval_t(llb, lub);
+                    return interval_t{llb, lub};
                 }
             }
         }
@@ -439,21 +450,21 @@ class interval_t final {
 
 namespace interval_operators {
 
-inline interval_t operator+(const number_t& c, const interval_t& x) { return interval_t(c) + x; }
+inline interval_t operator+(const number_t& c, const interval_t& x) { return interval_t{c} + x; }
 
-inline interval_t operator+(const interval_t& x, const number_t& c) { return x + interval_t(c); }
+inline interval_t operator+(const interval_t& x, const number_t& c) { return x + interval_t{c}; }
 
-inline interval_t operator*(const number_t& c, const interval_t& x) { return interval_t(c) * x; }
+inline interval_t operator*(const number_t& c, const interval_t& x) { return interval_t{c} * x; }
 
-inline interval_t operator*(const interval_t& x, const number_t& c) { return x * interval_t(c); }
+inline interval_t operator*(const interval_t& x, const number_t& c) { return x * interval_t{c}; }
 
-inline interval_t operator/(const number_t& c, const interval_t& x) { return interval_t(c) / x; }
+inline interval_t operator/(const number_t& c, const interval_t& x) { return interval_t{c} / x; }
 
-inline interval_t operator/(const interval_t& x, const number_t& c) { return x / interval_t(c); }
+inline interval_t operator/(const interval_t& x, const number_t& c) { return x / interval_t{c}; }
 
-inline interval_t operator-(const number_t& c, const interval_t& x) { return interval_t(c) - x; }
+inline interval_t operator-(const number_t& c, const interval_t& x) { return interval_t{c} - x; }
 
-inline interval_t operator-(const interval_t& x, const number_t& c) { return x - interval_t(c); }
+inline interval_t operator-(const interval_t& x, const number_t& c) { return x - interval_t{c}; }
 
 } // namespace interval_operators
 
diff --git a/src/crab/linear_constraint.hpp b/src/crab/linear_constraint.hpp
index ed00a6c74..9ed810b1f 100644
--- a/src/crab/linear_constraint.hpp
+++ b/src/crab/linear_constraint.hpp
@@ -2,6 +2,8 @@
 // SPDX-License-Identifier: MIT
 #pragma once
 
+#include <gsl/narrow>
+
 #include "linear_expression.hpp"
 
 // A linear constraint is of the form:
@@ -34,12 +36,12 @@ class linear_constraint_t final {
         if (!_expression.is_constant()) {
             return false;
         }
-        number_t constant = _expression.constant_term();
+        const number_t constant = _expression.constant_term();
         switch (_constraint_kind) {
-        case constraint_kind_t::EQUALS_ZERO: return (constant == 0);
-        case constraint_kind_t::LESS_THAN_OR_EQUALS_ZERO: return (constant <= 0);
-        case constraint_kind_t::LESS_THAN_ZERO: return (constant < 0);
-        case constraint_kind_t::NOT_ZERO: return (constant != 0);
+        case constraint_kind_t::EQUALS_ZERO: return constant == 0;
+        case constraint_kind_t::LESS_THAN_OR_EQUALS_ZERO: return constant <= 0;
+        case constraint_kind_t::LESS_THAN_ZERO: return constant < 0;
+        case constraint_kind_t::NOT_ZERO: return constant != 0;
         default: throw std::exception();
         }
     }
@@ -90,9 +92,9 @@ inline std::ostream& operator<<(std::ostream& o, const linear_constraint_t& cons
         const auto& expression = constraint.expression();
         expression.output_variable_terms(o);
 
-        const char* constraint_kind_label[] = {" == ", " <= ", " < ", " != "};
-        int kind = (int)constraint.kind();
-        if (kind < 0 || kind >= (int)(sizeof(constraint_kind_label) / sizeof(*constraint_kind_label))) {
+        constexpr std::array constraint_kind_label{" == ", " <= ", " < ", " != "};
+        const size_t kind = gsl::narrow<size_t>(constraint.kind());
+        if (kind >= std::size(constraint_kind_label)) {
             throw std::exception();
         }
         o << constraint_kind_label[kind] << -expression.constant_term();
diff --git a/src/crab/split_dbm.cpp b/src/crab/split_dbm.cpp
index 9d844e82b..4272233a3 100644
--- a/src/crab/split_dbm.cpp
+++ b/src/crab/split_dbm.cpp
@@ -2,6 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0
 #include <utility>
 
+#include <gsl/narrow>
+
 #include "crab/split_dbm.hpp"
 #include "crab_utils/debug.hpp"
 #include "crab_utils/stats.hpp"
@@ -11,7 +13,7 @@
 namespace crab::domains {
 
 static std::optional<SplitDBM::vert_id> try_at(const SplitDBM::vert_map_t& map, variable_t v) {
-    auto it = map.find(v);
+    const auto it = map.find(v);
     if (it == map.end()) {
         return std::nullopt;
     }
@@ -19,7 +21,7 @@ static std::optional<SplitDBM::vert_id> try_at(const SplitDBM::vert_map_t& map,
 }
 
 SplitDBM::vert_id SplitDBM::get_vert(variable_t v) {
-    if (auto y = try_at(vert_map, v)) {
+    if (const auto y = try_at(vert_map, v)) {
         return *y;
     }
 
@@ -464,7 +466,7 @@ SplitDBM SplitDBM::operator|(const SplitDBM& o) const& {
     for (auto [v, n] : vert_map) {
         if (auto y = try_at(o.vert_map, v)) {
             // Variable exists in both
-            out_vmap.emplace(v, static_cast<vert_id>(perm_x.size()));
+            out_vmap.emplace(v, gsl::narrow<vert_id>(perm_x.size()));
             out_revmap.push_back(v);
 
             pot_rx.push_back(potential[n] - potential[0]);
@@ -627,7 +629,7 @@ SplitDBM SplitDBM::widen(const SplitDBM& o) const {
     for (auto [v, n] : vert_map) {
         if (auto y = try_at(o.vert_map, v)) {
             // Variable exists in both
-            out_vmap.emplace(v, static_cast<vert_id>(perm_x.size()));
+            out_vmap.emplace(v, gsl::narrow<vert_id>(perm_x.size()));
             out_revmap.push_back(v);
 
             widen_pot.push_back(potential[n] - potential[0]);
@@ -682,7 +684,7 @@ std::optional<SplitDBM> SplitDBM::meet(const SplitDBM& o) const {
     meet_pi.emplace_back(0);
     meet_rev.push_back(std::nullopt);
     for (auto [v, n] : vert_map) {
-        vert_id vv = static_cast<vert_id>(perm_x.size());
+        vert_id vv = gsl::narrow<vert_id>(perm_x.size());
         meet_verts.emplace(v, vv);
         meet_rev.push_back(v);
 
@@ -696,7 +698,7 @@ std::optional<SplitDBM> SplitDBM::meet(const SplitDBM& o) const {
         auto it = meet_verts.find(v);
 
         if (it == meet_verts.end()) {
-            vert_id vv = static_cast<vert_id>(perm_y.size());
+            vert_id vv = gsl::narrow<vert_id>(perm_y.size());
             meet_rev.push_back(v);
 
             perm_y.push_back(n);
@@ -739,7 +741,7 @@ std::optional<SplitDBM> SplitDBM::meet(const SplitDBM& o) const {
 }
 
 void SplitDBM::operator-=(variable_t v) {
-    if (auto y = try_at(vert_map, v)) {
+    if (const auto y = try_at(vert_map, v)) {
         g.forget(*y);
         rev_map[*y] = std::nullopt;
         vert_map.erase(v);
@@ -773,7 +775,7 @@ bool SplitDBM::add_constraint(const linear_constraint_t& cst) {
     case constraint_kind_t::LESS_THAN_ZERO: {
         // We try to convert a strict to non-strict.
         // e < 0 --> e <= -1
-        auto nc = linear_constraint_t(cst.expression().plus(1), constraint_kind_t::LESS_THAN_OR_EQUALS_ZERO);
+        const auto nc = linear_constraint_t(cst.expression().plus(1), constraint_kind_t::LESS_THAN_OR_EQUALS_ZERO);
         if (!add_linear_leq(nc.expression())) {
             return false;
         }
@@ -956,7 +958,7 @@ void SplitDBM::set(variable_t x, const interval_t& intv) {
         return;
     }
 
-    vert_id v = get_vert(x);
+    const vert_id v = get_vert(x);
     if (intv.ub().is_finite()) {
         Weight ub;
         if (convert_NtoW_overflow(*intv.ub().number(), ub)) {
@@ -1168,8 +1170,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 {
-    [[maybe_unused]]
-    bool overflow = convert_NtoW_overflow(e.constant_term(), out);
+    [[maybe_unused]] const bool overflow = convert_NtoW_overflow(e.constant_term(), out);
     assert(!overflow);
     for (const auto& [variable, coefficient] : e.variable_terms()) {
         Weight coef;
@@ -1193,7 +1194,7 @@ interval_t SplitDBM::compute_residual(const linear_expression_t& e, variable_t p
 }
 
 SplitDBM::Weight SplitDBM::pot_value(variable_t v) const {
-    if (auto y = try_at(vert_map, v)) {
+    if (const auto y = try_at(vert_map, v)) {
         return potential[*y];
     }
     return {0};
@@ -1225,7 +1226,7 @@ bool SplitDBM::entail(const linear_constraint_t& rhs) const {
     if (rhs.is_contradiction()) {
         return false;
     }
-    interval_t interval = eval_interval(rhs.expression());
+    const interval_t interval = eval_interval(rhs.expression());
     switch (rhs.kind()) {
     case constraint_kind_t::EQUALS_ZERO:
         if (interval.singleton() == std::optional(number_t(0))) {
@@ -1277,11 +1278,11 @@ void SplitDBM::diffcsts_of_assign(variable_t x, const linear_expression_t& exp,
 
 static interval_t get_interval(const SplitDBM::vert_map_t& m, const SplitDBM::graph_t& r, variable_t x,
                                int finite_width) {
-    auto it = m.find(x);
+    const auto it = m.find(x);
     if (it == m.end()) {
         return interval_t::top();
     }
-    SplitDBM::vert_id v = it->second;
+    const SplitDBM::vert_id v = it->second;
     extended_number lb = extended_number::minus_infinity();
     extended_number ub = extended_number::plus_infinity();
     if (r.elem(v, 0)) {
diff --git a/src/crab/type_domain.cpp b/src/crab/type_domain.cpp
index 09d3de00f..7d0242d58 100644
--- a/src/crab/type_domain.cpp
+++ b/src/crab/type_domain.cpp
@@ -209,7 +209,7 @@ type_encoding_t TypeDomain::get_type(const NumAbsDomain& inv, const Reg& r) cons
     if (!res) {
         return T_UNINIT;
     }
-    return static_cast<type_encoding_t>(*res);
+    return res->narrow<type_encoding_t>();
 }
 
 type_encoding_t TypeDomain::get_type(const NumAbsDomain& inv, const variable_t v) const {
@@ -217,11 +217,11 @@ type_encoding_t TypeDomain::get_type(const NumAbsDomain& inv, const variable_t v
     if (!res) {
         return T_UNINIT;
     }
-    return static_cast<type_encoding_t>(*res);
+    return res->narrow<type_encoding_t>();
 }
 
 type_encoding_t TypeDomain::get_type(const NumAbsDomain& inv, const number_t& t) const {
-    return static_cast<type_encoding_t>(t);
+    return t.narrow<type_encoding_t>();
 }
 
 // Check whether a given type value is within the range of a given type variable's value.
diff --git a/src/crab/var_factory.cpp b/src/crab/var_factory.cpp
index d4fc83c56..f4c243229 100644
--- a/src/crab/var_factory.cpp
+++ b/src/crab/var_factory.cpp
@@ -11,13 +11,12 @@
 namespace crab {
 
 variable_t variable_t::make(const std::string& name) {
-    auto it = std::find(names->begin(), names->end(), name);
+    const auto it = std::find(names->begin(), names->end(), name);
     if (it == names->end()) {
         names->emplace_back(name);
         return variable_t(names->size() - 1);
-    } else {
-        return variable_t(std::distance(names->begin(), it));
     }
+    return variable_t(std::distance(names->begin(), it));
 }
 
 std::vector<std::string> default_variable_names() {
@@ -141,11 +140,13 @@ thread_local lazy_allocator<std::vector<std::string>, default_variable_names> va
 
 void variable_t::clear_thread_local_state() { names.clear(); }
 
-variable_t variable_t::reg(data_kind_t kind, int i) { return make("r" + std::to_string(i) + "." + name_of(kind)); }
+variable_t variable_t::reg(const data_kind_t kind, const int i) {
+    return make("r" + std::to_string(i) + "." + name_of(kind));
+}
 
 std::ostream& operator<<(std::ostream& o, const data_kind_t& s) { return o << name_of(s); }
 
-static std::string mk_scalar_name(data_kind_t kind, const number_t& o, const number_t& size) {
+static std::string mk_scalar_name(const data_kind_t kind, const number_t& o, const number_t& size) {
     std::stringstream os;
     os << "s"
        << "[" << o;
@@ -156,17 +157,17 @@ static std::string mk_scalar_name(data_kind_t kind, const number_t& o, const num
     return os.str();
 }
 
-variable_t variable_t::stack_frame_var(data_kind_t kind, int i, std::string prefix) {
+variable_t variable_t::stack_frame_var(const data_kind_t kind, const int i, const std::string& prefix) {
     return make(prefix + STACK_FRAME_DELIMITER + "r" + std::to_string(i) + "." + name_of(kind));
 }
 
-variable_t variable_t::cell_var(data_kind_t array, const number_t& offset, const number_t& size) {
+variable_t variable_t::cell_var(const data_kind_t array, const number_t& offset, const number_t& size) {
     return make(mk_scalar_name(array, offset.cast_to<uint64_t>(), size));
 }
 
 // Given a type variable, get the associated variable of a given kind.
-variable_t variable_t::kind_var(data_kind_t kind, variable_t type_variable) {
-    std::string name = type_variable.name();
+variable_t variable_t::kind_var(const data_kind_t kind, const variable_t type_variable) {
+    const std::string name = type_variable.name();
     return make(name.substr(0, name.rfind('.') + 1) + name_of(kind));
 }
 
diff --git a/src/crab/variable.hpp b/src/crab/variable.hpp
index 9267f7876..bb0075aea 100644
--- a/src/crab/variable.hpp
+++ b/src/crab/variable.hpp
@@ -69,7 +69,7 @@ class variable_t final {
 
     static std::vector<variable_t> get_type_variables();
     static variable_t reg(data_kind_t, int);
-    static variable_t stack_frame_var(data_kind_t kind, int i, std::string prefix);
+    static variable_t stack_frame_var(data_kind_t kind, int i, const std::string& prefix);
     static variable_t cell_var(data_kind_t array, const number_t& offset, const number_t& size);
     static variable_t kind_var(data_kind_t kind, variable_t type_variable);
     static variable_t meta_offset();
diff --git a/src/crab_utils/num_big.hpp b/src/crab_utils/num_big.hpp
index ae9e6220c..f7ea98a7a 100644
--- a/src/crab_utils/num_big.hpp
+++ b/src/crab_utils/num_big.hpp
@@ -31,7 +31,7 @@ class number_t final {
     explicit number_t(const std::string& s) { _n = cpp_int(s); }
 
     template <std::integral T>
-    explicit operator T() const {
+    T narrow() const {
         if (!fits<T>()) {
             CRAB_ERROR("number_t ", _n, " does not fit into ", typeid(T).name());
         }
@@ -39,7 +39,7 @@ class number_t final {
     }
 
     template <is_enum T>
-    explicit operator T() const {
+    T narrow() const {
         return static_cast<T>(static_cast<std::underlying_type_t<T>>(_n));
     }
 
@@ -241,7 +241,7 @@ class number_t final {
         if (!x.fits<int32_t>()) {
             CRAB_ERROR("number_t ", x._n, " does not fit into an int32");
         }
-        return number_t(_n << static_cast<int32_t>(x));
+        return number_t(_n << x.narrow<int32_t>());
     }
 
     number_t operator>>(const number_t& x) const {
@@ -251,7 +251,7 @@ class number_t final {
         if (!x.fits<int32_t>()) {
             CRAB_ERROR("number_t ", x._n, " does not fit into an int32");
         }
-        return number_t(_n >> static_cast<int32_t>(x));
+        return number_t(_n >> x.narrow<int32_t>());
     }
 
     [[nodiscard]]
diff --git a/src/crab_utils/num_extended.hpp b/src/crab_utils/num_extended.hpp
index f072b11e1..2a922eca3 100644
--- a/src/crab_utils/num_extended.hpp
+++ b/src/crab_utils/num_extended.hpp
@@ -49,6 +49,19 @@ class extended_number final {
 
     extended_number(extended_number&&) noexcept = default;
 
+    template <std::integral T>
+    T narrow() const {
+        if (_is_infinite) {
+            CRAB_ERROR("Bound: cannot narrow infinite value");
+        }
+        return _n.narrow<T>();
+    }
+
+    template <is_enum T>
+    T narrow() const {
+        return static_cast<T>(narrow<std::underlying_type_t<T>>());
+    }
+
     extended_number& operator=(extended_number&&) noexcept = default;
 
     extended_number& operator=(const extended_number& o) {
diff --git a/src/crab_utils/num_safeint.hpp b/src/crab_utils/num_safeint.hpp
index e8c12ed6b..1bcb8ec57 100644
--- a/src/crab_utils/num_safeint.hpp
+++ b/src/crab_utils/num_safeint.hpp
@@ -39,30 +39,30 @@ class safe_i64 {
         return std::numeric_limits<int64_t>::min();
     }
 
-    static std::optional<int64_t> checked_add(int64_t a, int64_t b) {
-        wideint_t lr = (wideint_t)a + (wideint_t)b;
+    static std::optional<int64_t> checked_add(const int64_t a, const int64_t b) {
+        const wideint_t lr = static_cast<wideint_t>(a) + static_cast<wideint_t>(b);
         if (lr > get_max() || lr < get_min()) {
             return {};
         }
         return static_cast<int64_t>(lr);
     }
 
-    static std::optional<int64_t> checked_sub(int64_t a, int64_t b) {
-        wideint_t lr = (wideint_t)a - (wideint_t)b;
+    static std::optional<int64_t> checked_sub(const int64_t a, const int64_t b) {
+        const wideint_t lr = static_cast<wideint_t>(a) - static_cast<wideint_t>(b);
         if (lr > get_max() || lr < get_min()) {
             return {};
         }
         return static_cast<int64_t>(lr);
     }
-    static std::optional<int64_t> checked_mul(int64_t a, int64_t b) {
-        wideint_t lr = (wideint_t)a * (wideint_t)b;
+    static std::optional<int64_t> checked_mul(const int64_t a, const int64_t b) {
+        const wideint_t lr = static_cast<wideint_t>(a) * static_cast<wideint_t>(b);
         if (lr > get_max() || lr < get_min()) {
             return {};
         }
         return static_cast<int64_t>(lr);
     }
-    static std::optional<int64_t> checked_div(int64_t a, int64_t b) {
-        wideint_t lr = (wideint_t)a / (wideint_t)b;
+    static std::optional<int64_t> checked_div(const int64_t a, const int64_t b) {
+        const wideint_t lr = static_cast<wideint_t>(a) / static_cast<wideint_t>(b);
         if (lr > get_max() || lr < get_min()) {
             return {};
         }
@@ -72,39 +72,39 @@ class safe_i64 {
   public:
     safe_i64() : m_num(0) {}
 
-    safe_i64(int64_t num) : m_num(num) {}
+    safe_i64(const int64_t num) : m_num(num) {}
 
-    safe_i64(const number_t& n) : m_num((int64_t)n) {}
+    safe_i64(const number_t& n) : m_num(n.narrow<int64_t>()) {}
 
     operator int64_t() const { return (int64_t)m_num; }
 
     // TODO: output parameters whether operation overflows
-    safe_i64 operator+(safe_i64 x) const {
-        if (auto z = checked_add(m_num, x.m_num)) {
+    safe_i64 operator+(const safe_i64 x) const {
+        if (const auto z = checked_add(m_num, x.m_num)) {
             return safe_i64(*z);
         }
         CRAB_ERROR("Integer overflow during addition");
     }
 
     // TODO: output parameters whether operation overflows
-    safe_i64 operator-(safe_i64 x) const {
-        if (auto z = checked_sub(m_num, x.m_num)) {
+    safe_i64 operator-(const safe_i64 x) const {
+        if (const auto z = checked_sub(m_num, x.m_num)) {
             return safe_i64(*z);
         }
         CRAB_ERROR("Integer overflow during subtraction");
     }
 
     // TODO: output parameters whether operation overflows
-    safe_i64 operator*(safe_i64 x) const {
-        if (auto z = checked_mul(m_num, x.m_num)) {
+    safe_i64 operator*(const safe_i64 x) const {
+        if (const auto z = checked_mul(m_num, x.m_num)) {
             return safe_i64(*z);
         }
         CRAB_ERROR("Integer overflow during multiplication");
     }
 
     // TODO: output parameters whether operation overflows
-    safe_i64 operator/(safe_i64 x) const {
-        if (auto z = checked_div(m_num, x.m_num)) {
+    safe_i64 operator/(const safe_i64 x) const {
+        if (const auto z = checked_div(m_num, x.m_num)) {
             return safe_i64(*z);
         }
         CRAB_ERROR("Integer overflow during division");
@@ -114,22 +114,22 @@ class safe_i64 {
     safe_i64 operator-() const { return safe_i64(0) - *this; }
 
     // TODO: output parameters whether operation overflows
-    safe_i64& operator+=(safe_i64 x) { return *this = *this + x; }
+    safe_i64& operator+=(const safe_i64 x) { return *this = *this + x; }
 
     // TODO: output parameters whether operation overflows
-    safe_i64& operator-=(safe_i64 x) { return *this = *this - x; }
+    safe_i64& operator-=(const safe_i64 x) { return *this = *this - x; }
 
-    bool operator==(safe_i64 x) const { return m_num == x.m_num; }
+    bool operator==(const safe_i64 x) const { return m_num == x.m_num; }
 
-    bool operator!=(safe_i64 x) const { return m_num != x.m_num; }
+    bool operator!=(const safe_i64 x) const { return m_num != x.m_num; }
 
-    bool operator<(safe_i64 x) const { return m_num < x.m_num; }
+    bool operator<(const safe_i64 x) const { return m_num < x.m_num; }
 
-    bool operator<=(safe_i64 x) const { return m_num <= x.m_num; }
+    bool operator<=(const safe_i64 x) const { return m_num <= x.m_num; }
 
-    bool operator>(safe_i64 x) const { return m_num > x.m_num; }
+    bool operator>(const safe_i64 x) const { return m_num > x.m_num; }
 
-    bool operator>=(safe_i64 x) const { return m_num >= x.m_num; }
+    bool operator>=(const safe_i64 x) const { return m_num >= x.m_num; }
 
     friend std::ostream& operator<<(std::ostream& o, const safe_i64& n) { return o << n.m_num; }