diff --git a/BUILD.bazel b/BUILD.bazel
index ca9856dbfb..1f9d8b8846 100644
--- a/BUILD.bazel
+++ b/BUILD.bazel
@@ -246,6 +246,7 @@ cc_library(
         "@com_github_p4lang_p4runtime//:p4info_cc_proto",
         "@com_github_p4lang_p4runtime//:p4runtime_cc_proto",
         "@com_github_p4lang_p4runtime//:p4types_cc_proto",
+        "@com_google_absl//absl/container:btree",
         "@com_google_absl//absl/container:flat_hash_map",
         "@com_google_absl//absl/container:flat_hash_set",
         "@com_google_absl//absl/container:inlined_vector",
diff --git a/backends/p4tools/BUILD.bazel b/backends/p4tools/BUILD.bazel
index 383e198a1e..194c26d272 100644
--- a/backends/p4tools/BUILD.bazel
+++ b/backends/p4tools/BUILD.bazel
@@ -85,6 +85,7 @@ cc_library(
         "@boost//:multiprecision",
         "@com_github_p4lang_p4runtime//:p4info_cc_proto",
         "@com_github_z3prover_z3//:api",
+        "@com_google_absl//absl/container:btree",
     ],
 )
 
@@ -163,6 +164,7 @@ cc_library(
         "//:lib",
         "@boost//:multiprecision",
         "@com_github_pantor_inja//:inja",
+        "@com_google_absl//absl/container:btree",
         "@nlohmann_json//:json",
     ],
 )
@@ -181,7 +183,6 @@ cc_binary(
     deps = [
         ":testgen_lib",
         "//:lib",
-        "@boost//:filesystem",
         "@boost//:multiprecision",
     ],
 )
diff --git a/backends/p4tools/common/lib/ir_compare.h b/backends/p4tools/common/lib/ir_compare.h
new file mode 100644
index 0000000000..96b99bcd9c
--- /dev/null
+++ b/backends/p4tools/common/lib/ir_compare.h
@@ -0,0 +1,29 @@
+#ifndef BACKENDS_P4TOOLS_COMMON_LIB_IR_COMPARE_H_
+#define BACKENDS_P4TOOLS_COMMON_LIB_IR_COMPARE_H_
+
+#include "ir/ir.h"
+
+namespace IR {
+
+/// Equals for StateVariable pointers. We only compare the label.
+struct StateVariableEqual {
+    bool operator()(const IR::StateVariable *s1, const IR::StateVariable *s2) const {
+        return s1->equiv(*s2);
+    }
+    bool operator()(const IR::StateVariable &s1, const IR::StateVariable &s2) const {
+        return s1.equiv(s2);
+    }
+};
+
+/// Less for StateVariable pointers. We only compare the label.
+struct StateVariableLess {
+    bool operator()(const IR::StateVariable *s1, const IR::StateVariable *s2) const {
+        return *s1 < *s2;
+    }
+    bool operator()(const IR::StateVariable &s1, const IR::StateVariable &s2) const {
+        return s1 < s2;
+    }
+};
+
+}  // namespace IR
+#endif /* BACKENDS_P4TOOLS_COMMON_LIB_IR_COMPARE_H_ */
diff --git a/backends/p4tools/common/lib/model.cpp b/backends/p4tools/common/lib/model.cpp
index 382be53164..f5cacf24d3 100644
--- a/backends/p4tools/common/lib/model.cpp
+++ b/backends/p4tools/common/lib/model.cpp
@@ -4,8 +4,6 @@
 #include <string>
 #include <utility>
 
-#include <boost/container/vector.hpp>
-
 #include "frontends/p4/optimizeExpressions.h"
 #include "ir/indexed_vector.h"
 #include "ir/irutils.h"
diff --git a/backends/p4tools/common/lib/model.h b/backends/p4tools/common/lib/model.h
index ffc63aef3e..6fd8cb2da0 100644
--- a/backends/p4tools/common/lib/model.h
+++ b/backends/p4tools/common/lib/model.h
@@ -3,10 +3,8 @@
 
 #include <map>
 #include <utility>
-#include <vector>
-
-#include <boost/container/flat_map.hpp>
 
+#include "absl/container/btree_map.h"
 #include "ir/ir.h"
 #include "ir/solver.h"
 #include "ir/visitor.h"
@@ -14,7 +12,7 @@
 namespace P4Tools {
 
 /// Symbolic maps map a state variable to a IR::Expression.
-using SymbolicMapType = boost::container::flat_map<IR::StateVariable, const IR::Expression *>;
+using SymbolicMapType = absl::btree_map<IR::StateVariable, const IR::Expression *>;
 
 /// Represents a solution found by the solver. A model is a concretized form of a symbolic
 /// environment. All the expressions in a Model must be of type IR::Literal.
diff --git a/backends/p4tools/common/lib/symbolic_env.cpp b/backends/p4tools/common/lib/symbolic_env.cpp
index e66ca624fc..26bf02f063 100644
--- a/backends/p4tools/common/lib/symbolic_env.cpp
+++ b/backends/p4tools/common/lib/symbolic_env.cpp
@@ -3,8 +3,6 @@
 #include <algorithm>
 #include <utility>
 
-#include <boost/container/vector.hpp>
-
 #include "backends/p4tools/common/lib/model.h"
 #include "ir/indexed_vector.h"
 #include "ir/vector.h"
diff --git a/backends/p4tools/common/options.h b/backends/p4tools/common/options.h
index 33f71e5886..1f6e9b2d94 100644
--- a/backends/p4tools/common/options.h
+++ b/backends/p4tools/common/options.h
@@ -1,7 +1,6 @@
 #ifndef BACKENDS_P4TOOLS_COMMON_OPTIONS_H_
 #define BACKENDS_P4TOOLS_COMMON_OPTIONS_H_
 
-// Boost
 #include <cstdint>
 #include <optional>
 #include <tuple>
diff --git a/backends/p4tools/modules/testgen/lib/execution_state.cpp b/backends/p4tools/modules/testgen/lib/execution_state.cpp
index 97e7e4d923..c0dfd7dfa9 100644
--- a/backends/p4tools/modules/testgen/lib/execution_state.cpp
+++ b/backends/p4tools/modules/testgen/lib/execution_state.cpp
@@ -11,7 +11,6 @@
 #include <variant>
 #include <vector>
 
-#include <boost/container/vector.hpp>
 #include <boost/multiprecision/cpp_int.hpp>
 
 #include "backends/p4tools/common/compiler/convert_hs_index.h"
diff --git a/backends/p4tools/modules/testgen/lib/final_state.cpp b/backends/p4tools/modules/testgen/lib/final_state.cpp
index a4eb7436ee..c21069db95 100644
--- a/backends/p4tools/modules/testgen/lib/final_state.cpp
+++ b/backends/p4tools/modules/testgen/lib/final_state.cpp
@@ -5,8 +5,6 @@
 #include <variant>
 #include <vector>
 
-#include <boost/container/vector.hpp>
-
 #include "backends/p4tools/common/lib/model.h"
 #include "backends/p4tools/common/lib/symbolic_env.h"
 #include "backends/p4tools/common/lib/trace_event.h"
diff --git a/backends/p4tools/p4tools.def b/backends/p4tools/p4tools.def
index 87bfd58217..b3848a94f4 100644
--- a/backends/p4tools/p4tools.def
+++ b/backends/p4tools/p4tools.def
@@ -23,12 +23,21 @@ class StateVariable : Expression {
     StateVariable(ArrayIndex arr) : Expression(arr->getSourceInfo(), arr->type), ref(arr) {}
 
     /// Implements comparisons so that StateVariables can be used as map keys.
+    // Delegate to IR's notion of equality.
     bool operator==(const StateVariable &other) const override {
-        // Delegate to IR's notion of equality.
         return *ref == *other.ref;
     }
 
     /// Implements comparisons so that StateVariables can be used as map keys.
+    /// Note that we ignore the type of the variable in the comparison.
+    equiv {
+        // We use a custom compare function.
+        // TODO: Is there a faster way to implement this comparison?
+        return compare(ref, a.ref) == 0;
+    }
+
+    /// Implements comparisons so that StateVariables can be used as map keys.
+    /// Note that we ignore the type of the variable in the comparison.
     bool operator<(const StateVariable &other) const {
         // We use a custom compare function.
         // TODO: Is there a faster way to implement this comparison?
diff --git a/ir/compare.h b/ir/compare.h
new file mode 100644
index 0000000000..8e067f7fee
--- /dev/null
+++ b/ir/compare.h
@@ -0,0 +1,29 @@
+#ifndef IR_COMPARE_H_
+#define IR_COMPARE_H_
+
+#include "ir/ir.h"
+
+namespace IR {
+
+/// Equals for SymbolicVariable pointers. We only compare the label.
+struct SymbolicVariableEqual {
+    bool operator()(const IR::SymbolicVariable *s1, const IR::SymbolicVariable *s2) const {
+        return s1->label == s2->label;
+    }
+    bool operator()(const IR::SymbolicVariable &s1, const IR::SymbolicVariable &s2) const {
+        return s1.label == s2.label;
+    }
+};
+
+/// Less for SymbolicVariable pointers. We only compare the label.
+struct SymbolicVariableLess {
+    bool operator()(const IR::SymbolicVariable *s1, const IR::SymbolicVariable *s2) const {
+        return *s1 < *s2;
+    }
+    bool operator()(const IR::SymbolicVariable &s1, const IR::SymbolicVariable &s2) const {
+        return s1 < s2;
+    }
+};
+
+}  // namespace IR
+#endif /* IR_COMPARE_H_ */
diff --git a/ir/solver.h b/ir/solver.h
index 459be62fa2..7b940685ce 100644
--- a/ir/solver.h
+++ b/ir/solver.h
@@ -4,9 +4,8 @@
 #include <optional>
 #include <vector>
 
-#include <boost/container/flat_map.hpp>
-#include <boost/container/flat_set.hpp>
-
+#include "absl/container/btree_map.h"
+#include "ir/compare.h"
 #include "ir/ir.h"
 #include "lib/castable.h"
 #include "lib/cstring.h"
@@ -15,18 +14,9 @@
 // TODO: This should implement AbstractRepCheckedNode<Constraint>.
 using Constraint = IR::Expression;
 
-/// Comparator to compare SymbolicVariable pointers.
-struct SymbolicVarComp {
-    bool operator()(const IR::SymbolicVariable *s1, const IR::SymbolicVariable *s2) const {
-        return s1->operator<(*s2);
-    }
-};
-
 /// This type maps symbolic variables to their value assigned by the solver.
-using SymbolicMapping = boost::container::flat_map<const IR::SymbolicVariable *,
-                                                   const IR::Expression *, SymbolicVarComp>;
-
-using SymbolicSet = boost::container::flat_set<const IR::SymbolicVariable *, SymbolicVarComp>;
+using SymbolicMapping =
+    absl::btree_map<const IR::SymbolicVariable *, const IR::Expression *, IR::SymbolicVariableLess>;
 
 /// Provides a higher-level interface for an SMT solver.
 class AbstractSolver : public ICastable {