Replace boost::integer_traits with std::numeric_limits. (#2439)

Further, remove redundant gmp.h include in options_handler.cpp.

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 8abe8d5419e223ecfd4079035ad182f104ee64e4..22d944e4c6a43ddbfff4ba1ad68d565a423af4b8 100644 (file)
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -29,7 +29,6 @@
 #include "base/modal_exception.h"
 #include "base/output.h"
 #include "lib/strtok_r.h"
-#include "gmp.h"
 #include "options/arith_heuristic_pivot_rule.h"
 #include "options/arith_propagation_mode.h"
 #include "options/arith_unate_lemma_mode.h"

diff --git a/src/util/dense_map.h b/src/util/dense_map.h
index a3a1573c054c0eed4e1d84ae8607d4f65cca61f6..410fcc8fa55c91d61cb4c956ad61e79562a1f162 100644 (file)
--- a/src/util/dense_map.h
+++ b/src/util/dense_map.h
@@ -26,7 +26,7 @@
 
 #pragma once
 
-#include <boost/integer_traits.hpp>
+#include <limits>
 #include <vector>
 
 #include "base/cvc4_assert.h"
@@ -48,7 +48,8 @@ private:
 
   typedef Index Position;
   typedef std::vector<Position> PositionMap;
-  static const Position POSITION_SENTINEL = boost::integer_traits<Position>::const_max;
+  static const Position POSITION_SENTINEL =
+      std::numeric_limits<Position>::max();
 
   //Each Key in the set is mapped to its position in d_list.
   //Each Key not in the set is mapped to KEY_SENTINEL