diff --git a/include/crab/cfg/cfg.hpp b/include/crab/cfg/cfg.hpp
index 7d288129..4eae4f8e 100644
--- a/include/crab/cfg/cfg.hpp
+++ b/include/crab/cfg/cfg.hpp
@@ -48,7 +48,7 @@
 #include <boost/unordered_map.hpp>
 
 #include <crab/common/types.hpp>
-#include <crab/common/bignums.hpp>
+#include <crab/numbers/bignums.hpp>
 #include <crab/domains/linear_constraints.hpp>
 #include <crab/domains/interval.hpp>
 #include <crab/domains/discrete_domains.hpp>
diff --git a/include/crab/domains/array_expansion.hpp b/include/crab/domains/array_expansion.hpp
index 3fbe634f..dae5e710 100644
--- a/include/crab/domains/array_expansion.hpp
+++ b/include/crab/domains/array_expansion.hpp
@@ -1266,13 +1266,12 @@ namespace domains {
 	CRAB_ERROR("array expansion domain expects constant array element sizes");		
       }
 
-      bool ignore_array_store = false;
       interval_t lb_i = to_interval(lb_idx);
       auto lb = lb_i.singleton();
       if (!lb) {
 	CRAB_WARN("array expansion store range ignored because ",
 		  "lower bound is not constant");
-	ignore_array_store = true;
+	return;
       }
       
       interval_t ub_i = to_interval(ub_idx);
@@ -1280,29 +1279,28 @@ namespace domains {
       if (!ub) {
 	CRAB_WARN("array expansion store range ignored because ",
 		  "upper bound is not constant");
-	ignore_array_store = true;	
+	return;
       }
 
-	
       if ((*ub - *lb) % *n != 0) {
 	CRAB_WARN("array expansion store range ignored because ",
 		  "the number of elements must be divisible by ", *n);
-	ignore_array_store = true;		
+	return;
       }
 
+      // TODO: this should be an user parameter.
       const number_t max_num_elems = 512;
+      
       if (*ub - *lb > max_num_elems) {
 	CRAB_WARN("array expansion store range ignored because ",
 		  "the number of elements is larger than default limit of ",
 		  max_num_elems);
-	ignore_array_store = true;			
+	return;
       }
 
-      if (!ignore_array_store) {
-	for(number_t i = *lb, e = *ub; i < e; ) {
-	  array_store(a, elem_size, i, val, false);
-	  i = i + *n;
-	}
+      for(number_t i = *lb, e = *ub; i < e; ) {
+	array_store(a, elem_size, i, val, false);
+	i = i + *n;
       }
     }
     
diff --git a/include/crab/domains/graphs/graph_config.hpp b/include/crab/domains/graphs/graph_config.hpp
new file mode 100644
index 00000000..c3fdd798
--- /dev/null
+++ b/include/crab/domains/graphs/graph_config.hpp
@@ -0,0 +1,166 @@
+#pragma once
+
+#include <type_traits>
+
+#include <crab/numbers/safeint.hpp>
+#include <crab/domains/graphs/adapt_sgraph.hpp>
+#include <crab/domains/graphs/sparse_graph.hpp>
+#include <crab/domains/graphs/ht_graph.hpp>
+#include <crab/domains/graphs/pt_graph.hpp>
+
+namespace crab {
+namespace domains {
+namespace DBM_impl {
+
+// All of these representations are implementations of a
+// sparse weighted graph. They differ on the datastructures
+// used to store successors and predecessors
+enum GraphRep { 
+  // sparse-map and sparse-sets
+  ss = 1,        
+  // adaptive sparse-map and sparse-sets
+  adapt_ss = 2,  
+  // patricia tree-maps and patricia tree-sets
+  pt = 3,           
+  // hash table and hash sets
+  ht = 4
+};          
+
+/** DBM weights (Wt) can be represented using one of the following
+ * types:
+ * 
+ * 1) basic integer type: e.g., long
+ * 2) safei64
+ * 3) z_number
+ * 
+ * 1) is the fastest but things can go wrong if some DBM
+ * operation overflows. 2) is slower than 1) but it checks for
+ * overflow before any DBM operation. 3) is the slowest and it
+ * represents weights using unbounded mathematical integers so
+ * overflow is not a concern but it might not be what you need
+ * when reasoning about programs with wraparound semantics.
+ **/
+
+template<typename Number, GraphRep Graph = GraphRep::adapt_ss>
+class DefaultParams {
+public:
+  enum { chrome_dijkstra = 1 };
+  enum { widen_restabilize = 1 };
+  enum { special_assign = 1 };
+  enum { close_bounds_inline = 0 };	 
+  
+  typedef long Wt;
+  
+  typedef typename std::conditional< 
+    (Graph == ss), 
+    SparseWtGraph<Wt>,
+    typename std::conditional< 
+      (Graph == adapt_ss), 
+      AdaptGraph<Wt>,
+      typename std::conditional< 
+	(Graph == pt), 
+	PtGraph<Wt>, 
+	HtGraph<Wt> 
+	>::type 
+      >::type 
+    >::type graph_t;
+};
+
+// We don't use GraphRep::adapt_ss because having problems
+// realloc'ed Number objects.
+template<typename Number, GraphRep Graph = GraphRep::ss>
+class BigNumDefaultParams {
+public:
+  enum { chrome_dijkstra = 1 };
+  enum { widen_restabilize = 1 };
+  enum { special_assign = 1 };
+  enum { close_bounds_inline = 0 };	 	 
+  
+  // Use Number as graph weights
+  typedef Number Wt;
+  
+  typedef typename std::conditional< 
+    (Graph == ss), 
+    SparseWtGraph<Wt>,
+    typename std::conditional< 
+      (Graph == adapt_ss), 
+      AdaptGraph<Wt>,
+      typename std::conditional< 
+	(Graph == pt), 
+	PtGraph<Wt>, 
+	HtGraph<Wt> 
+	>::type 
+      >::type 
+    >::type graph_t;
+};
+
+template<typename Number, GraphRep Graph = GraphRep::adapt_ss>
+class SafeInt64DefaultParams {
+public:
+  enum { chrome_dijkstra = 1 };
+  enum { widen_restabilize = 1 };
+  enum { special_assign = 1 };
+  enum { close_bounds_inline = 0 };	 
+  
+  typedef safe_i64 Wt;
+  
+  typedef typename std::conditional< 
+    (Graph == ss), 
+    SparseWtGraph<Wt>,
+    typename std::conditional< 
+      (Graph == adapt_ss), 
+      AdaptGraph<Wt>,
+      typename std::conditional< 
+	(Graph == pt), 
+	PtGraph<Wt>, 
+	HtGraph<Wt> 
+	>::type 
+      >::type 
+    >::type graph_t;
+};
+
+
+template<typename Number, GraphRep Graph = GraphRep::adapt_ss>
+class SimpleParams {
+public:
+  enum { chrome_dijkstra = 0 };
+  enum { widen_restabilize = 0 };
+  enum { special_assign = 0 };
+  enum { close_bounds_inline = 1 };	 	 
+  
+  typedef long Wt;
+  
+  typedef typename std::conditional< 
+    (Graph == ss), 
+    SparseWtGraph<Wt>,
+    typename std::conditional< 
+      (Graph == adapt_ss), 
+      AdaptGraph<Wt>,
+      typename std::conditional< 
+	(Graph == pt), 
+	PtGraph<Wt>, 
+	HtGraph<Wt> 
+	>::type 
+      >::type 
+    >::type graph_t;
+};
+
+
+/**
+ * Helper to translate from Number (e.g., ikos::z_number) to DBM
+ * weight.  Number is the template parameter of the DBM-based abstract
+ * domain to represent a number. Note that Number might not fit into
+ * Wt type. If this is the case then a runtime error will be triggered
+ * when Number is casted to Wt
+ **/
+template<typename Number, typename Wt>
+class NtoW {
+public:
+static Wt convert(const Number& n) { 
+  return (Wt) n;
+}
+};
+
+}
+}
+}
diff --git a/include/crab/domains/graphs/graph_ops.hpp b/include/crab/domains/graphs/graph_ops.hpp
index 812c8683..dcaacb15 100644
--- a/include/crab/domains/graphs/graph_ops.hpp
+++ b/include/crab/domains/graphs/graph_ops.hpp
@@ -1202,10 +1202,10 @@ namespace crab {
     */
     template<class G, class P>
     static bool repair_potential(G& g, P& p, vert_id ii, vert_id jj)
-    { 
+    {
       // Ensure there's enough scratch space. 
       unsigned int sz = g.size();
-//      assert(src < (int) sz && dest < (int) sz);
+      // assert(src < (int) sz && dest < (int) sz);
       grow_scratch(sz);
 
       for(vert_id vi : g.verts())
@@ -1249,7 +1249,7 @@ namespace crab {
           }
         }
       }
-      if(dists[ii] < 0)
+      if(dists[ii] < Wt(0))
         return false;
 
       for(vert_id v : g.verts())
diff --git a/include/crab/domains/interval.hpp b/include/crab/domains/interval.hpp
index 68c36c27..a48ee59c 100644
--- a/include/crab/domains/interval.hpp
+++ b/include/crab/domains/interval.hpp
@@ -10,7 +10,7 @@
 #include <boost/optional.hpp>
 #include <crab/common/types.hpp>
 #include <crab/common/stats.hpp>
-#include <crab/common/bignums.hpp>
+#include <crab/numbers/bignums.hpp>
 
 namespace ikos {
 
diff --git a/include/crab/domains/linear_interval_solver.hpp b/include/crab/domains/linear_interval_solver.hpp
index d4f587a2..64d33fea 100644
--- a/include/crab/domains/linear_interval_solver.hpp
+++ b/include/crab/domains/linear_interval_solver.hpp
@@ -52,8 +52,8 @@
 #include <crab/common/types.hpp>
 #include <crab/common/debug.hpp>
 #include <crab/common/stats.hpp>
-#include <crab/common/bignums.hpp>
-#include <crab/common/wrapint.hpp>
+#include <crab/numbers/bignums.hpp>
+#include <crab/numbers/wrapint.hpp>
 #include <crab/domains/linear_constraints.hpp>
 
 namespace ikos {
diff --git a/include/crab/domains/sparse_dbm.hpp b/include/crab/domains/sparse_dbm.hpp
index 75379203..f09c36c2 100644
--- a/include/crab/domains/sparse_dbm.hpp
+++ b/include/crab/domains/sparse_dbm.hpp
@@ -12,10 +12,7 @@
 #include <crab/common/types.hpp>
 #include <crab/common/stats.hpp>
 #include <crab/common/debug.hpp>
-#include <crab/domains/graphs/sparse_graph.hpp>
-#include <crab/domains/graphs/adapt_sgraph.hpp>
-#include <crab/domains/graphs/ht_graph.hpp>
-#include <crab/domains/graphs/pt_graph.hpp>
+#include <crab/domains/graphs/graph_config.hpp>
 #include <crab/domains/graphs/graph_ops.hpp>
 #include <crab/domains/linear_constraints.hpp>
 #include <crab/domains/interval.hpp>
@@ -37,134 +34,8 @@ namespace crab {
 
   namespace domains {
 
-    namespace SpDBM_impl {
-       /*******************************************************************
-	* Translate from Number to dbm val_t type
-	*******************************************************************
-	* Important: Number might not fit into Wt type. If this is the
-        * case then a runtime error will be triggered when Number is
-        * casted to Wt
-	*******************************************************************
-	*/
-       template<typename Number, typename Wt>
-       class NtoV {
-       public:
-         static Wt ntov(const Number& n) { 
-           return (Wt) n;
-         }
-       };
-
-       // All of these representations are implementations of a
-       // sparse weighted graph. They differ on the datastructures
-       // used to store successors and predecessors
-       enum GraphRep { 
-         // sparse-map and sparse-sets
-         ss = 1,        
-         // adaptive sparse-map and sparse-sets
-         adapt_ss = 2,  
-         // patricia tree-maps and patricia tree-sets
-         pt = 3,           
-         // hash table and hash sets
-         ht = 4
-       };          
-
-       template<typename Number, GraphRep Graph = GraphRep::adapt_ss>
-       class DefaultParams {
-       public:
-         enum { chrome_dijkstra = 1 };
-         enum { widen_restabilize = 1 };
-         enum { special_assign = 1 };
-
-	 /***********************************************************/
-	 // Use long as graph weights
-	 /***********************************************************/	 
-	 // The code does not check for overflows on weight
-	 // operations. Thus, use it on your own risk! If you think
-	 // that the program will have large constants then use
-	 // BigNumDefaultParams. Unfortunately, there will be a
-	 // performance penalty.
-	 /***********************************************************/	 
-         typedef long Wt;
-
-         typedef typename std::conditional< 
-           (Graph == ss), 
-           SparseWtGraph<Wt>,
-           typename std::conditional< 
-             (Graph == adapt_ss), 
-             AdaptGraph<Wt>,
-             typename std::conditional< 
-               (Graph == pt), 
-               PtGraph<Wt>, 
-               HtGraph<Wt> 
-               >::type 
-             >::type 
-           >::type graph_t;
-       };
-
-       template<typename Number, GraphRep Graph = GraphRep::adapt_ss>
-       class SimpleParams {
-       public:
-         enum { chrome_dijkstra = 0 };
-         enum { widen_restabilize = 0 };
-         enum { special_assign = 0 };
-
-	 /***********************************************************/
-	 // Use long as graph weights
-	 /***********************************************************/	 
-	 // The code does not check for overflows on weight
-	 // operations. Thus, use it on your own risk! If you think
-	 // that the program will have large constants then use
-	 // BigNumDefaultParams. Unfortunately, there will be a
-	 // performance penalty.
-	 /***********************************************************/	 
-         typedef long Wt;
-
-         typedef typename std::conditional< 
-           (Graph == ss), 
-           SparseWtGraph<Wt>,
-           typename std::conditional< 
-             (Graph == adapt_ss), 
-             AdaptGraph<Wt>,
-             typename std::conditional< 
-               (Graph == pt), 
-               PtGraph<Wt>, 
-               HtGraph<Wt> 
-               >::type 
-             >::type 
-           >::type graph_t;
-       };
-
-       // We don't use GraphRep::adapt_ss because having problems
-       // realloc'ed Number objects.      
-       template<typename Number, GraphRep Graph = GraphRep::ss>
-       class BigNumDefaultParams {
-       public:
-         enum { chrome_dijkstra = 1 };
-         enum { widen_restabilize = 1 };
-         enum { special_assign = 1 };
-
-	 // Use Number as graph weights	 
-         typedef Number Wt;
-	 
-         typedef typename std::conditional< 
-           (Graph == ss), 
-           SparseWtGraph<Wt>,
-           typename std::conditional< 
-             (Graph == adapt_ss), 
-             AdaptGraph<Wt>,
-             typename std::conditional< 
-               (Graph == pt), 
-               PtGraph<Wt>, 
-               HtGraph<Wt> 
-               >::type 
-             >::type 
-           >::type graph_t;
-       };
-      
-     }; // end namespace SpDBM_impl
-
     template<class Number, class VariableName,
-	     class Params = SpDBM_impl::DefaultParams <Number> >
+	     class Params = DBM_impl::DefaultParams<Number>>
     class SparseDBM_ final:
       public abstract_domain<SparseDBM_<Number,VariableName,Params>> {
       typedef SparseDBM_<Number, VariableName, Params> DBM_t;
@@ -189,7 +60,7 @@ namespace crab {
       typedef ikos::bound<number_t>  bound_t;
       typedef typename Params::Wt Wt;
       typedef typename Params::graph_t graph_t;
-      typedef SpDBM_impl::NtoV<number_t, Wt> ntov;
+      typedef DBM_impl::NtoW<number_t, Wt> ntow;
       typedef typename graph_t::vert_id vert_id;
       typedef boost::container::flat_map<variable_t, vert_id> vert_map_t;
       typedef typename vert_map_t::value_type vmap_elt_t;
@@ -338,9 +209,9 @@ namespace crab {
 
       // Evaluate an expression under the chosen potentials
       Wt eval_expression(linear_expression_t e) {
-        Wt v(ntov::ntov(e.constant())); 
+        Wt v(ntow::convert(e.constant())); 
         for(auto p : e) {
-          v += (pot_value(p.second) - potential[0])*(ntov::ntov(p.first));
+          v += (pot_value(p.second) - potential[0])*(ntow::convert(p.first));
         }
         return v;
       }
@@ -395,18 +266,18 @@ namespace crab {
         {
           // Process upper bounds.
           boost::optional<variable_t> unbounded_ubvar;
-          Wt exp_ub(ntov::ntov(exp.constant()));
+          Wt exp_ub(ntow::convert(exp.constant()));
           std::vector<std::pair<variable_t, Wt> > ub_terms;
           for(auto p : exp)
           {
-            Wt coeff(ntov::ntov(p.first));
-            if(p.first < Wt(0))
+            Wt coeff(ntow::convert(p.first));
+            if(coeff < Wt(0))
             {
               // Can't do anything with negative coefficients.
               bound_t y_lb = operator[](p.second).lb();
               if(y_lb.is_infinite())
                 goto assign_ub_finish;
-              exp_ub += ntov::ntov(*(y_lb.number()))*coeff;
+              exp_ub += ntow::convert(*(y_lb.number()))*coeff;
             } else {
               variable_t y(p.second);
               bound_t y_ub = operator[](y).ub(); 
@@ -416,7 +287,7 @@ namespace crab {
                   goto assign_ub_finish;
                 unbounded_ubvar = y;
               } else {
-                Wt ymax(ntov::ntov(*(y_ub.number())));
+                Wt ymax(ntow::convert(*(y_ub.number())));
                 exp_ub += ymax*coeff;
                 ub_terms.push_back(std::make_pair(y, ymax));
               }
@@ -438,18 +309,18 @@ namespace crab {
 
         {
           boost::optional<variable_t> unbounded_lbvar;
-          Wt exp_lb(ntov::ntov(exp.constant()));
+          Wt exp_lb(ntow::convert(exp.constant()));
           std::vector<std::pair<variable_t, Wt> > lb_terms;
           for(auto p : exp)
           {
-            Wt coeff(ntov::ntov(p.first));
-            if(p.first < Wt(0))
+            Wt coeff(ntow::convert(p.first));
+            if(coeff < Wt(0))
             {
               // Again, can't do anything with negative coefficients.
               bound_t y_ub = operator[](p.second).ub();
               if(y_ub.is_infinite())
                 goto assign_lb_finish;
-              exp_lb += (ntov::ntov(*(y_ub.number())))*coeff;
+              exp_lb += (ntow::convert(*(y_ub.number())))*coeff;
             } else {
               variable_t y(p.second);
               bound_t y_lb = operator[](y).lb(); 
@@ -459,7 +330,7 @@ namespace crab {
                   goto assign_lb_finish;
                 unbounded_lbvar = y;
               } else {
-                Wt ymin(ntov::ntov(*(y_lb.number())));
+                Wt ymin(ntow::convert(*(y_lb.number())));
                 exp_lb += ymin*coeff;
                 lb_terms.push_back(std::make_pair(y, ymin));
               }
@@ -490,12 +361,12 @@ namespace crab {
         Wt unbounded_ubcoeff;
         boost::optional<variable_t> unbounded_lbvar;
         boost::optional<variable_t> unbounded_ubvar;
-        Wt exp_ub = - (ntov::ntov(exp.constant()));
+        Wt exp_ub = -(ntow::convert(exp.constant()));
         std::vector<std::pair<std::pair<Wt, variable_t>, Wt> > pos_terms;
         std::vector<std::pair<std::pair<Wt, variable_t>, Wt> > neg_terms;
         for(auto p : exp)
         {
-          Wt coeff(ntov::ntov(p.first));
+          Wt coeff(ntow::convert(p.first));
           if(coeff > Wt(0))
           {
             variable_t y(p.second);
@@ -507,7 +378,7 @@ namespace crab {
               unbounded_lbvar = y;
               unbounded_lbcoeff = coeff;
             } else {
-              Wt ymin(ntov::ntov(*(y_lb.number())));
+              Wt ymin(ntow::convert(*(y_lb.number())));
               // Coeff is negative, so it's still add
               exp_ub -= ymin*coeff;
               pos_terms.push_back(std::make_pair(std::make_pair(coeff, y), ymin));
@@ -520,9 +391,9 @@ namespace crab {
               if(unbounded_ubvar)
                 goto diffcst_finish;
               unbounded_ubvar = y;
-              unbounded_ubcoeff = -(ntov::ntov(coeff));
+              unbounded_ubcoeff = -coeff;
             } else {
-              Wt ymax(ntov::ntov(*(y_ub.number())));
+              Wt ymax(ntow::convert(*(y_ub.number())));
               exp_ub -= ymax*coeff;
               neg_terms.push_back(std::make_pair(std::make_pair(-coeff, y), ymax));
             }
@@ -642,7 +513,7 @@ namespace crab {
 	  typename graph_t::mut_val_ref_t w;
 	  if(new_i.lb().is_finite()) {
 	    // strenghten lb
-	    Wt lb_val = ntov::ntov(-(*(new_i.lb().number())));
+	    Wt lb_val = ntow::convert(-(*(new_i.lb().number())));
 	    if(g.lookup(v, 0, &w) && lb_val < w) {
 	      g.set_edge(v, lb_val, 0);
 	      if(!repair_potential(v, 0)) {
@@ -664,7 +535,7 @@ namespace crab {
 	  }
 	  if(new_i.ub().is_finite()) {	    
 	    // strengthen ub
-	    Wt ub_val = ntov::ntov(*(new_i.ub().number()));
+	    Wt ub_val = ntow::convert(*(new_i.ub().number()));
 	    if(g.lookup(0, v, &w) && (ub_val < w)) {
 	      g.set_edge(0, ub_val, v);
 	      if(!repair_potential(0, v)) {
@@ -1394,10 +1265,10 @@ namespace crab {
               }
               if(x_int.lb().is_finite())
                 delta.push_back(std::make_pair(std::make_pair(v,0),
-					       ntov::ntov(-(*(x_int.lb().number())))));
+					       ntow::convert(-(*(x_int.lb().number())))));
               if(x_int.ub().is_finite())
                 delta.push_back(std::make_pair(std::make_pair(0,v),
-					       ntov::ntov(*(x_int.ub().number()))));
+					       ntow::convert(*(x_int.ub().number()))));
                  
               GrOps::apply_delta(g, delta);
               delta.clear();
@@ -1424,10 +1295,10 @@ namespace crab {
 
               if(x_int.lb().is_finite())
                 cst_edges.push_back(std::make_pair(std::make_pair(v,0),
-						   ntov::ntov(-(*(x_int.lb().number())))));
+						   ntow::convert(-(*(x_int.lb().number())))));
               if(x_int.ub().is_finite())
                 cst_edges.push_back(std::make_pair(std::make_pair(0,v),
-						   ntov::ntov(*(x_int.ub().number()))));
+						   ntow::convert(*(x_int.ub().number()))));
 
               for(auto diff : diffs_lb)
               {
@@ -1677,14 +1548,14 @@ namespace crab {
         vert_id v = get_vert(x);
         if(intv.ub().is_finite())
         {
-          Wt ub = ntov::ntov(*(intv.ub().number()));
+          Wt ub = ntow::convert(*(intv.ub().number()));
           potential[v] = potential[0] + ub;
           g.set_edge(0, ub, v);
           close_over_edge(0, v);
         }
         if(intv.lb().is_finite())
         {
-          Wt lb = ntov::ntov(*(intv.lb().number()));
+          Wt lb = ntow::convert(*(intv.lb().number()));
           potential[v] = potential[0] + lb;
           g.set_edge(v, -lb, 0);
           close_over_edge(v, 0);
@@ -1973,8 +1844,8 @@ namespace crab {
                 // We give priority to equalities since some domains
                 // might not understand inequalities
                 if (g_excl.elem(s, d) && g_excl.elem(d, s) &&
-                    g_excl.edge_val(s, d) == 0 &&
-		    g_excl.edge_val(d, s) == 0) {
+                    g_excl.edge_val(s, d) == Wt(0) &&
+		    g_excl.edge_val(d, s) == Wt(0)) {
                   linear_constraint_t cst(linear_expression_t(vs) == vd);
                   csts += cst;
                 } else {
@@ -2121,7 +1992,7 @@ namespace crab {
     
     #if 1
     template<class Number, class VariableName,
-	       class Params = SpDBM_impl::DefaultParams<Number>>
+	       class Params = DBM_impl::DefaultParams<Number>>
     using SparseDBM = SparseDBM_<Number,VariableName,Params>;    
     #else
 
@@ -2133,7 +2004,7 @@ namespace crab {
     
     // Quick wrapper which uses shared references with copy-on-write.
     template<class Number, class VariableName,
-	     class Params = SpDBM_impl::DefaultParams<Number>>
+	     class Params = DBM_impl::DefaultParams<Number>>
     class SparseDBM final:
       public abstract_domain<SparseDBM<Number,VariableName,Params>> {
       typedef SparseDBM<Number, VariableName, Params> DBM_t;
diff --git a/include/crab/domains/split_dbm.hpp b/include/crab/domains/split_dbm.hpp
index abf06abc..8662c5c5 100644
--- a/include/crab/domains/split_dbm.hpp
+++ b/include/crab/domains/split_dbm.hpp
@@ -20,19 +20,13 @@
 #include <crab/common/types.hpp>
 #include <crab/common/debug.hpp>
 #include <crab/common/stats.hpp>
-#include <crab/domains/graphs/adapt_sgraph.hpp>
-#include <crab/domains/graphs/sparse_graph.hpp>
-#include <crab/domains/graphs/ht_graph.hpp>
-#include <crab/domains/graphs/pt_graph.hpp>
 #include <crab/domains/graphs/graph_ops.hpp>
+#include <crab/domains/graphs/graph_config.hpp>
 #include <crab/domains/linear_constraints.hpp>
 #include <crab/domains/interval.hpp>
-#include <crab/domains/patricia_trees.hpp>
 #include <crab/domains/abstract_domain.hpp>
 #include <crab/domains/abstract_domain_specialized_traits.hpp>
 
-#include <type_traits>
-
 #include <boost/optional.hpp>
 #include <boost/unordered_set.hpp>
 #include <boost/container/flat_map.hpp>
@@ -47,137 +41,7 @@ namespace crab {
 
   namespace domains {
 
-     namespace SDBM_impl {
-       
-       /*******************************************************************
-	* Translate from Number to dbm val_t type
-	*******************************************************************
-	* Important: Number might not fit into Wt type. If this is the
-        * case then a runtime error will be triggered when Number is
-        * casted to Wt
-	*******************************************************************
-	*/
-       template<typename Number, typename Wt>
-       class NtoV {
-       public:
-         static Wt ntov(const Number& n) { 
-           return (Wt) n;
-         }
-       };
-
-       // All of these representations are implementations of a
-       // sparse weighted graph. They differ on the datastructures
-       // used to store successors and predecessors
-       enum GraphRep { 
-         // sparse-map and sparse-sets
-         ss = 1,        
-         // adaptive sparse-map and sparse-sets
-         adapt_ss = 2,  
-         // patricia tree-maps and patricia tree-sets
-         pt = 3,           
-         // hash table and hash sets
-         ht = 4
-       };          
-
-       template<typename Number, GraphRep Graph = GraphRep::adapt_ss>
-       class DefaultParams {
-       public:
-         enum { chrome_dijkstra = 1 };
-         enum { widen_restabilize = 1 };
-         enum { special_assign = 1 };
-         enum { close_bounds_inline = 0 };	 
-
-	 /***********************************************************/
-	 // Use long as graph weights
-	 /***********************************************************/	 
-	 // The code does not check for overflows on weight
-	 // operations. Thus, use it on your own risk! If you think
-	 // that the program will have large constants then use
-	 // BigNumDefaultParams. Unfortunately, there will be a
-	 // performance penalty.
-	 /***********************************************************/	 
-         typedef long Wt; 
-
-         typedef typename std::conditional< 
-           (Graph == ss), 
-           SparseWtGraph<Wt>,
-           typename std::conditional< 
-             (Graph == adapt_ss), 
-             AdaptGraph<Wt>,
-             typename std::conditional< 
-               (Graph == pt), 
-               PtGraph<Wt>, 
-               HtGraph<Wt> 
-               >::type 
-             >::type 
-           >::type graph_t;
-       };
-
-       template<typename Number, GraphRep Graph = GraphRep::adapt_ss>
-       class SimpleParams {
-       public:
-         enum { chrome_dijkstra = 0 };
-         enum { widen_restabilize = 0 };
-         enum { special_assign = 0 };
-         enum { close_bounds_inline = 1 };	 	 
-
-	 /***********************************************************/
-	 // Use long as graph weights
-	 /***********************************************************/	 
-	 // The code does not check for overflows on weight
-	 // operations. Thus, use it on your own risk! If you think
-	 // that the program will have large constants then use
-	 // BigNumDefaultParams. Unfortunately, there will be a
-	 // performance penalty.
-	 /***********************************************************/	 
-         typedef long Wt;
-
-         typedef typename std::conditional< 
-           (Graph == ss), 
-           SparseWtGraph<Wt>,
-           typename std::conditional< 
-             (Graph == adapt_ss), 
-             AdaptGraph<Wt>,
-             typename std::conditional< 
-               (Graph == pt), 
-               PtGraph<Wt>, 
-               HtGraph<Wt> 
-               >::type 
-             >::type 
-           >::type graph_t;
-       };
-
-       // We don't use GraphRep::adapt_ss because having problems
-       // realloc'ed Number objects.
-       template<typename Number, GraphRep Graph = GraphRep::ss>
-       class BigNumDefaultParams {
-       public:
-         enum { chrome_dijkstra = 1 };
-         enum { widen_restabilize = 1 };
-         enum { special_assign = 1 };
-         enum { close_bounds_inline = 0 };	 	 
-
-	 // Use Number as graph weights
-         typedef Number Wt;
-
-         typedef typename std::conditional< 
-           (Graph == ss), 
-           SparseWtGraph<Wt>,
-           typename std::conditional< 
-             (Graph == adapt_ss), 
-             AdaptGraph<Wt>,
-             typename std::conditional< 
-               (Graph == pt), 
-               PtGraph<Wt>, 
-               HtGraph<Wt> 
-               >::type 
-             >::type 
-           >::type graph_t;
-       };
-     }; // end namespace SDBM_impl
-
-
-    template<class Number, class VariableName, class Params = SDBM_impl::DefaultParams<Number>>
+    template<class Number, class VariableName, class Params = DBM_impl::DefaultParams<Number>>
     class SplitDBM_ final:
       public abstract_domain<SplitDBM_<Number,VariableName,Params>> {
       typedef SplitDBM_<Number, VariableName, Params> DBM_t;
@@ -201,7 +65,7 @@ namespace crab {
       typedef bound<number_t>  bound_t;
       typedef typename Params::Wt Wt;
       typedef typename Params::graph_t graph_t;
-      typedef SDBM_impl::NtoV<number_t, Wt> ntov;
+      typedef DBM_impl::NtoW<number_t, Wt> ntow;
       typedef typename graph_t::vert_id vert_id;
       typedef boost::container::flat_map<variable_t, vert_id> vert_map_t;
       typedef typename vert_map_t::value_type vmap_elt_t;
@@ -336,9 +200,9 @@ namespace crab {
 
       // Evaluate an expression under the chosen potentials
       Wt eval_expression(linear_expression_t e) {
-        Wt v(ntov::ntov(e.constant())); 
+        Wt v(ntow::convert(e.constant())); 
         for(auto p : e) {
-          v += (pot_value(p.second) - potential[0])*(ntov::ntov(p.first));
+          v += (pot_value(p.second) - potential[0])*(ntow::convert(p.first));
         }
         return v;
       }
@@ -384,12 +248,12 @@ namespace crab {
 
 	boost::optional<variable_t> unbounded_var;
 	std::vector< std::pair<variable_t, Wt>> terms;	
-	Wt residual(ntov::ntov(exp.constant()));
+	Wt residual(ntow::convert(exp.constant()));
 	for(auto p : exp) {
-	  Wt coeff(ntov::ntov(p.first));
+	  Wt coeff(ntow::convert(p.first));
 	  variable_t y(p.second);	    
 	  
-	  if(p.first < Wt(0)) {
+	  if(coeff < Wt(0)) {
 	    // Can't do anything with negative coefficients.
 	    bound_t y_val = (extract_upper_bounds ?
 			     operator[](y).lb():
@@ -398,7 +262,7 @@ namespace crab {
 	    if(y_val.is_infinite()) {
 	      return;
 	    }
-	    residual += ntov::ntov(*(y_val.number()))*coeff;
+	    residual += ntow::convert(*(y_val.number()))*coeff;
 	  } else {
 	    bound_t y_val = (extract_upper_bounds ?
 			     operator[](y).ub():
@@ -410,7 +274,7 @@ namespace crab {
 	      }
 	      unbounded_var = y;
 	    } else {
-	      Wt ymax(ntov::ntov(*(y_val.number())));
+	      Wt ymax(ntow::convert(*(y_val.number())));
 	      residual += ymax*coeff;
 	      terms.push_back({y, ymax});
 	    }
@@ -452,11 +316,11 @@ namespace crab {
         Wt unbounded_ubcoeff;
         boost::optional<variable_t> unbounded_lbvar;
         boost::optional<variable_t> unbounded_ubvar;
-        Wt exp_ub = - (ntov::ntov(exp.constant()));
+        Wt exp_ub = -(ntow::convert(exp.constant()));
         std::vector<std::pair<std::pair<Wt, variable_t>, Wt>> pos_terms;
         std::vector<std::pair<std::pair<Wt, variable_t>, Wt>> neg_terms;
         for(auto p : exp) {
-          Wt coeff(ntov::ntov(p.first));
+          Wt coeff(ntow::convert(p.first));
           if(coeff > Wt(0)) {
             variable_t y(p.second);
             bound_t y_lb = operator[](y).lb();
@@ -467,7 +331,7 @@ namespace crab {
               unbounded_lbvar = y;
               unbounded_lbcoeff = coeff;
             } else {
-              Wt ymin(ntov::ntov(*(y_lb.number())));
+              Wt ymin(ntow::convert(*(y_lb.number())));
               exp_ub -= ymin*coeff;
               pos_terms.push_back({{coeff, y}, ymin});
             }
@@ -479,9 +343,9 @@ namespace crab {
                 return;
 	      }
               unbounded_ubvar = y;
-              unbounded_ubcoeff = -(ntov::ntov(coeff));
+              unbounded_ubcoeff = -coeff;
             } else {
-              Wt ymax(ntov::ntov(*(y_ub.number())));
+              Wt ymax(ntow::convert(*(y_ub.number())));
               exp_ub -= ymax*coeff;
               neg_terms.push_back({{-coeff, y}, ymax});
             }
@@ -645,7 +509,7 @@ namespace crab {
 	  Wt_min min_op;	  
 	  if(new_i.lb().is_finite()) {
 	    // strenghten lb
-	    Wt lb_val = ntov::ntov(-(*(new_i.lb().number())));
+	    Wt lb_val = ntow::convert(-(*(new_i.lb().number())));
 	    if(g.lookup(v, 0, &w) && lb_val < w.get()) {
 	      g.set_edge(v, lb_val, 0);
 	      if(!repair_potential(v, 0)) {
@@ -667,7 +531,7 @@ namespace crab {
 	  }
 	  if(new_i.ub().is_finite()) {	    
 	    // strengthen ub
-	    Wt ub_val = ntov::ntov(*(new_i.ub().number()));
+	    Wt ub_val = ntow::convert(*(new_i.ub().number()));
 	    if(g.lookup(0, v, &w) && (ub_val < w.get())) {
 	      g.set_edge(0, ub_val, v);
 	      if(!repair_potential(0, v)) {
@@ -925,7 +789,7 @@ namespace crab {
 	
         typename graph_t::mut_val_ref_t w;        
         if (g.lookup(y,x,&w)) {
-          return ((w.get() + k) < 0);
+          return ((w.get() + k) < Wt(0));
         } else {
           interval_t intv_x = interval_t::top();
           interval_t intv_y = interval_t::top();
@@ -942,7 +806,7 @@ namespace crab {
           if (intv_x.is_top() || intv_y.is_top()) {
             return false;
           } else  {
-            return (!((intv_y - intv_x).lb() <= k));
+            return (!((intv_y - intv_x).lb() <= (number_t) k));
           }
         }
       }
@@ -1703,9 +1567,9 @@ namespace crab {
 	      
 	      Wt_min min_op;
 	      if(x_int.lb().is_finite())
-		g.update_edge(v, ntov::ntov(-(*(x_int.lb().number()))), 0, min_op);
+		g.update_edge(v, ntow::convert(-(*(x_int.lb().number()))), 0, min_op);
 	      if(x_int.ub().is_finite())
-		g.update_edge(0, ntov::ntov(*(x_int.ub().number())), v, min_op);
+		g.update_edge(0, ntow::convert(*(x_int.ub().number())), v, min_op);
 	      // Clear the old x vertex
               operator-=(x);
               vert_map.insert(vmap_elt_t(x, v));
@@ -1747,9 +1611,9 @@ namespace crab {
 	      }
 	      
 	      if(x_int.lb().is_finite())
-		g.update_edge(v, ntov::ntov(-(*(x_int.lb().number()))), 0, min_op);
+		g.update_edge(v, ntow::convert(-(*(x_int.lb().number()))), 0, min_op);
 	      if(x_int.ub().is_finite())
-		g.update_edge(0, ntov::ntov(*(x_int.ub().number())), v, min_op);
+		g.update_edge(0, ntow::convert(*(x_int.ub().number())), v, min_op);
 	      
 	      // Clear the old x vertex
 	      operator-=(x);
@@ -1982,13 +1846,13 @@ namespace crab {
         vert_id v = get_vert(x);
         if(intv.ub().is_finite())
         {
-          Wt ub = ntov::ntov(*(intv.ub().number()));
+          Wt ub = ntow::convert(*(intv.ub().number()));
           potential[v] = potential[0] + ub;
           g.set_edge(0, ub, v);
         }
         if(intv.lb().is_finite())
         {
-          Wt lb = ntov::ntov(*(intv.lb().number()));
+          Wt lb = ntow::convert(*(intv.lb().number()));
           potential[v] = potential[0] + lb;
           g.set_edge(v, -lb, 0);
         }
@@ -2261,8 +2125,8 @@ namespace crab {
                 // We give priority to equalities since some domains
                 // might not understand inequalities
                 if (g_excl.elem(s, d) && g_excl.elem(d, s) &&
-                    g_excl.edge_val(s, d) == 0 &&
-		    g_excl.edge_val(d, s) == 0) {
+                    g_excl.edge_val(s, d) == Wt(0) &&
+		    g_excl.edge_val(d, s) == Wt(0)) {
                   linear_constraint_t cst(linear_expression_t(vs) == vd);
                   csts += cst;
                 } else {
@@ -2503,7 +2367,7 @@ namespace crab {
     
     #if 1
     template<class Number, class VariableName,
-	     class Params = SDBM_impl::DefaultParams<Number>>
+	     class Params = DBM_impl::DefaultParams<Number>>
     using SplitDBM = SplitDBM_<Number,VariableName,Params>;    
     #else
 
@@ -2515,7 +2379,7 @@ namespace crab {
     
     // Quick wrapper which uses shared references with copy-on-write.
     template<class Number, class VariableName,
-	     class Params=SDBM_impl::DefaultParams<Number>>
+	     class Params = DBM_impl::DefaultParams<Number>>
     class SplitDBM final:
       public abstract_domain<SplitDBM<Number,VariableName,Params>> {
       typedef SplitDBM<Number, VariableName, Params> DBM_t;
diff --git a/include/crab/domains/term_equiv.hpp b/include/crab/domains/term_equiv.hpp
index 473f2293..9e5a083f 100644
--- a/include/crab/domains/term_equiv.hpp
+++ b/include/crab/domains/term_equiv.hpp
@@ -25,7 +25,7 @@
 #include <crab/common/debug.hpp>
 #include <crab/common/stats.hpp>
 #include <crab/common/types.hpp>
-#include <crab/common/bignums.hpp>
+#include <crab/numbers/bignums.hpp>
 #include <crab/cfg/var_factory.hpp>
 #include <crab/domains/linear_constraints.hpp>
 #include <crab/domains/abstract_domain.hpp>
diff --git a/include/crab/domains/wrapped_interval_domain.hpp b/include/crab/domains/wrapped_interval_domain.hpp
index d7a99a76..f0dbc709 100644
--- a/include/crab/domains/wrapped_interval_domain.hpp
+++ b/include/crab/domains/wrapped_interval_domain.hpp
@@ -7,7 +7,7 @@
  ** P.J.Stuckey published in APLAS'12.
  **/
 
-#include <crab/common/wrapint.hpp>
+#include <crab/numbers/wrapint.hpp>
 #include <crab/common/types.hpp>
 #include <crab/common/stats.hpp>
 #include <crab/domains/abstract_domain.hpp>
diff --git a/include/crab/iterators/thresholds.hpp b/include/crab/iterators/thresholds.hpp
index e87ee9e4..b854617e 100644
--- a/include/crab/iterators/thresholds.hpp
+++ b/include/crab/iterators/thresholds.hpp
@@ -1,6 +1,5 @@
 #pragma once
 
-#include <crab/common/bignums.hpp>
 #include <crab/domains/interval.hpp>
 #include <crab/common/debug.hpp>
 #include <crab/cfg/cfg.hpp>
diff --git a/include/crab/common/bignums.hpp b/include/crab/numbers/bignums.hpp
similarity index 100%
rename from include/crab/common/bignums.hpp
rename to include/crab/numbers/bignums.hpp
diff --git a/include/crab/numbers/safeint.hpp b/include/crab/numbers/safeint.hpp
new file mode 100644
index 00000000..02fc9093
--- /dev/null
+++ b/include/crab/numbers/safeint.hpp
@@ -0,0 +1,177 @@
+#pragma once 
+
+/** 
+ *  Safe signed integers.
+**/
+
+#include <limits>
+
+namespace crab {
+
+class safe_i64 {
+  // Current implementation is based on
+  // https://blog.regehr.org/archives/1139 using wider integers.
+
+  // Both clang and gcc supports __int128 if the targeted architecture
+  // is x86/64, but it wont' work with 32 bits.
+  typedef __int128 wideint_t;
+  
+  inline int64_t get_max() const {
+    return std::numeric_limits<int64_t>::max();
+  }
+  
+  inline int64_t get_min() const {
+    return std::numeric_limits<int64_t>::min();
+  }
+  
+  int checked_add(int64_t a, int64_t b, int64_t *rp) const {
+    #if 1
+    wideint_t lr = (wideint_t)a + (wideint_t)b;
+    *rp = lr;
+    return lr > get_max() || lr < get_min();
+    #else
+    // without wider integers
+    if (b > 0 && a > get_max() - b) {
+      return 1;
+    }
+    if (b < 0 && a < get_min() - b) {
+      return 1;
+    }
+    int64_t lr = a + b;
+    *rp = lr;
+    return 0;
+    #endif 
+  }
+  
+  int checked_sub(int64_t a, int64_t b, int64_t *rp) const {
+    wideint_t lr = (wideint_t)a - (wideint_t)b;
+    *rp = lr;
+    return lr > get_max() || lr < get_min();
+  }
+  
+  int checked_mul(int64_t a, int64_t b, int64_t *rp) const {
+    wideint_t lr = (wideint_t)a * (wideint_t)b;
+    *rp = lr;
+    return lr > get_max() || lr < get_min();
+  }
+  
+  int checked_div(int64_t a, int64_t b, int64_t *rp) const {
+    wideint_t lr = (wideint_t)a / (wideint_t)b;
+    *rp = lr;
+    return lr > get_max() || lr < get_min();
+  }
+  
+public:
+  
+  safe_i64(): m_num(0) {}
+  
+  safe_i64(int64_t num): m_num(num) {}
+  
+  safe_i64(ikos::z_number n): m_num((long) n) {}
+  
+  operator long() const {
+    return (long) m_num;
+  }
+
+  // FIXME: operation should not raise an error.
+  safe_i64 operator+(safe_i64 x) const {
+    int64_t z;
+    int err = checked_add(m_num, x.m_num, &z);
+    if (err) {
+      CRAB_ERROR("Integer overflow during addition");
+    }
+    return safe_i64(z);
+  }
+
+  // FIXME: operation should not raise an error.  
+  safe_i64 operator-(safe_i64 x) const {
+    int64_t z;
+    int err = checked_sub(m_num, x.m_num, &z);
+    if (err) {
+      CRAB_ERROR("Integer overflow during subtraction");
+    }
+    return safe_i64(z);
+  }
+
+  // FIXME: operation should not raise an error.  
+  safe_i64 operator*(safe_i64 x) const {
+    int64_t z;
+    int err = checked_mul(m_num, x.m_num, &z);
+    if (err) {
+      CRAB_ERROR("Integer overflow during multiplication");
+    }
+    return safe_i64(z);
+  }
+
+  // FIXME: operation should not raise an error.  
+  safe_i64 operator/(safe_i64 x) const {
+    int64_t z;
+    int err = checked_div(m_num, x.m_num, &z);
+    if (err) {
+      CRAB_ERROR("Integer overflow during multiplication");
+    }
+    return safe_i64(z);
+  }
+
+  // FIXME: operation should not raise an error.  
+  safe_i64 operator-() const {
+    return safe_i64(0) - *this;
+  }
+
+  // FIXME: operation should not raise an error.  
+  safe_i64& operator+=(safe_i64 x) {
+    int err = checked_add(m_num, x.m_num, &m_num);
+    if (err) {
+      CRAB_ERROR("Integer overflow during addition");
+    }
+    return *this;
+  }
+
+  // FIXME: operation should not raise an error.  
+  safe_i64& operator-=(safe_i64 x) {
+    int err = checked_sub(m_num, x.m_num, &m_num);
+    if (err) {
+      CRAB_ERROR("Integer overflow during subtraction");
+    }
+    return *this;
+  }
+  
+  bool operator==(safe_i64 x) const {
+    return m_num == x.m_num;
+  }
+  
+  bool operator!=(safe_i64 x) const {
+    return m_num != x.m_num;
+  }
+  
+  bool operator<(safe_i64 x) const {
+    return m_num < x.m_num;
+  }
+  
+  bool operator<=(safe_i64 x) const {
+    return m_num <= x.m_num;
+  }
+
+  bool operator>(safe_i64 x) const {
+    return m_num > x.m_num;
+  }
+  
+  bool operator>=(safe_i64 x) const {
+    return m_num >= x.m_num;
+  }
+  
+  void write(crab::crab_os& os) const {
+    os << m_num;
+  }
+  
+  friend crab_os& operator<<(crab_os& o, const safe_i64& n) {
+    n.write(o);
+    return o;
+  }
+  
+private:
+  
+  int64_t m_num;
+};
+
+} // end namespace crab
diff --git a/include/crab/common/wrapint.hpp b/include/crab/numbers/wrapint.hpp
similarity index 99%
rename from include/crab/common/wrapint.hpp
rename to include/crab/numbers/wrapint.hpp
index 199e97d5..a717321f 100644
--- a/include/crab/common/wrapint.hpp
+++ b/include/crab/numbers/wrapint.hpp
@@ -8,7 +8,7 @@
 #include <sstream>
 #include <boost/functional/hash.hpp>
 #include <crab/common/types.hpp>
-#include <crab/common/bignums.hpp>
+#include <crab/numbers/bignums.hpp>
 
 namespace crab {
 
diff --git a/tests/crab_dom.hpp b/tests/crab_dom.hpp
index e903f42d..00fc6ff2 100644
--- a/tests/crab_dom.hpp
+++ b/tests/crab_dom.hpp
@@ -37,10 +37,10 @@ namespace crab {
     // Numerical domains over integers
     typedef interval_domain<ikos::z_number,varname_t> z_interval_domain_t;
     typedef numerical_congruence_domain<z_interval_domain_t> z_ric_domain_t;
-    typedef SpDBM_impl::DefaultParams<ikos::z_number,SpDBM_impl::GraphRep::adapt_ss> z_SparseDBMGraph;
-    typedef SparseDBM<ikos::z_number,varname_t,z_SparseDBMGraph> z_dbm_domain_t;
-    typedef SDBM_impl::DefaultParams<ikos::z_number, SDBM_impl::GraphRep::adapt_ss> z_SplitDBMGraph;
-    typedef SplitDBM<ikos::z_number,varname_t,z_SplitDBMGraph> z_sdbm_domain_t;
+    typedef DBM_impl::DefaultParams<ikos::z_number,DBM_impl::GraphRep::adapt_ss> z_SparseGraph;
+    typedef SparseDBM<ikos::z_number,varname_t,z_SparseGraph> z_dbm_domain_t;
+    typedef DBM_impl::DefaultParams<ikos::z_number,DBM_impl::GraphRep::adapt_ss> z_SplitGraph;
+    typedef SplitDBM<ikos::z_number,varname_t,z_SplitGraph> z_sdbm_domain_t;
     typedef split_octagons_impl::DefaultParams<ikos::z_number,
 					       split_octagons_impl::GraphRep::adapt_ss> z_SplitOctGraph;
     typedef split_oct_domain<ikos::z_number,varname_t,z_SplitOctGraph> z_soct_domain_t;
diff --git a/tests/domains/wrapint/wrapint.cc b/tests/domains/wrapint/wrapint.cc
index 6aa0a1e1..cf7befba 100644
--- a/tests/domains/wrapint/wrapint.cc
+++ b/tests/domains/wrapint/wrapint.cc
@@ -1,6 +1,6 @@
 #include <crab/config.h>
 #include <crab/common/types.hpp>
-#include <crab/common/wrapint.hpp>
+#include <crab/numbers/wrapint.hpp>
 
 #include <iostream>
 
diff --git a/tests/domains/wrapint/wrapped_intervals.cc b/tests/domains/wrapint/wrapped_intervals.cc
index 85ca2aeb..a18868d6 100644
--- a/tests/domains/wrapint/wrapped_intervals.cc
+++ b/tests/domains/wrapint/wrapped_intervals.cc
@@ -1,6 +1,6 @@
 #include <crab/config.h>
 #include <crab/common/types.hpp>
-#include <crab/common/wrapint.hpp>
+#include <crab/numbers/wrapint.hpp>
 #include <crab/domains/wrapped_interval_domain.hpp>
 #include "../../program_options.hpp"