diff --git a/infer/src/absint/AbstractDomain.mli b/infer/src/absint/AbstractDomain.mli
index bf2188c2e..145e5b6d9 100644
--- a/infer/src/absint/AbstractDomain.mli
+++ b/infer/src/absint/AbstractDomain.mli
@@ -76,7 +76,11 @@ end
 module TopLifted (Domain : S) : WithTop with type t = Domain.t top_lifted
 
 module TopLiftedUtils : sig
+  val ( <= ) : le:(lhs:'a -> rhs:'a -> bool) -> lhs:'a top_lifted -> rhs:'a top_lifted -> bool
+
   val pp_top : Format.formatter -> unit
+
+  val pp : pp:(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a top_lifted -> unit
 end
 
 (** Cartesian product of two domains. *)
@@ -129,11 +133,19 @@ module type MapS = sig
   include WithBottom with type t := t
 end
 
-(** Map domain ordered by union over the set of bindings, so the bottom element is the empty map.
+include
+  sig
+    [@@@warning "-60"]
+
+    (** Map domain ordered by union over the set of bindings, so the bottom element is the empty map.
     Every element implicitly maps to bottom unless it is explicitly bound to something else.
     Uses PPMap as the underlying map *)
-module MapOfPPMap (PPMap : PrettyPrintable.PPMap) (ValueDomain : S) :
-  MapS with type key = PPMap.key and type value = ValueDomain.t and type t = ValueDomain.t PPMap.t
+    module MapOfPPMap (PPMap : PrettyPrintable.PPMap) (ValueDomain : S) :
+      MapS
+      with type key = PPMap.key
+       and type value = ValueDomain.t
+       and type t = ValueDomain.t PPMap.t
+end
 
 (** Map domain ordered by union over the set of bindings, so the bottom element is the empty map.
     Every element implicitly maps to bottom unless it is explicitly bound to something else *)
diff --git a/infer/src/bufferoverrun/ints.ml b/infer/src/bufferoverrun/ints.ml
index e4bcbdefb..765e5156f 100644
--- a/infer/src/bufferoverrun/ints.ml
+++ b/infer/src/bufferoverrun/ints.ml
@@ -83,8 +83,6 @@ module NonNegativeInt = struct
 
   let ( * ) = Z.( * )
 
-  let max = Z.max
-
   let pp = Z.pp_print
 end
 
diff --git a/infer/src/bufferoverrun/ints.mli b/infer/src/bufferoverrun/ints.mli
index 9a0c7a6b3..63daa80ed 100644
--- a/infer/src/bufferoverrun/ints.mli
+++ b/infer/src/bufferoverrun/ints.mli
@@ -73,8 +73,6 @@ module NonNegativeInt : sig
 
   val ( * ) : t -> t -> t
 
-  val max : t -> t -> t
-
   val pp : F.formatter -> t -> unit
 end
 
diff --git a/infer/src/bufferoverrun/polynomials.ml b/infer/src/bufferoverrun/polynomials.ml
index ff27900bf..d94242297 100644
--- a/infer/src/bufferoverrun/polynomials.ml
+++ b/infer/src/bufferoverrun/polynomials.ml
@@ -298,15 +298,6 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
     PartialOrder.join cmp_const cmp_terms
 
 
-  (* Possible optimization for later: x join x^2 = x^2 instead of x + x^2 *)
-  let rec join : t -> t -> t =
-   fun p1 p2 ->
-    if phys_equal p1 p2 then p1
-    else
-      { const= NonNegativeInt.max p1.const p2.const
-      ; terms= M.increasing_union ~f:join p1.terms p2.terms }
-
-
   (* assumes symbols are not comparable *)
   (* TODO: improve this for comparable symbols *)
   let min_default_left : t -> t -> t =
@@ -320,10 +311,6 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
         if is_constant p1 then p1 else if is_constant p2 then p2 else p1
 
 
-  let widen : prev:t -> next:t -> num_iters:int -> t =
-   fun ~prev:_ ~next:_ ~num_iters:_ -> assert false
-
-
   let subst callee_pname loc =
     let exception ReturnTop in
     (* avoids top-lifting everything *)
@@ -422,7 +409,13 @@ module NonNegativeBoundWithDegreeKind = MakeSymbolWithDegreeKind (Bounds.NonNega
 module NonNegativeNonTopPolynomial = MakePolynomial (NonNegativeBoundWithDegreeKind)
 
 module NonNegativePolynomial = struct
-  include AbstractDomain.TopLifted (NonNegativeNonTopPolynomial)
+  type t = NonNegativeNonTopPolynomial.t top_lifted
+
+  let top = Top
+
+  let ( <= ) = AbstractDomain.TopLiftedUtils.( <= ) ~le:NonNegativeNonTopPolynomial.( <= )
+
+  let pp = AbstractDomain.TopLiftedUtils.pp ~pp:NonNegativeNonTopPolynomial.pp
 
   let zero = NonTop NonNegativeNonTopPolynomial.zero
 
@@ -460,8 +453,6 @@ module NonNegativePolynomial = struct
         NonTop (NonNegativeNonTopPolynomial.min_default_left p1 p2)
 
 
-  let widen ~prev ~next ~num_iters:_ = if ( <= ) ~lhs:next ~rhs:prev then prev else Top
-
   let subst callee_pname loc p eval_sym =
     match p with
     | Top ->
diff --git a/infer/src/bufferoverrun/polynomials.mli b/infer/src/bufferoverrun/polynomials.mli
index a576064e5..05484500d 100644
--- a/infer/src/bufferoverrun/polynomials.mli
+++ b/infer/src/bufferoverrun/polynomials.mli
@@ -30,7 +30,11 @@ module NonNegativeNonTopPolynomial : sig
 end
 
 module NonNegativePolynomial : sig
-  include AbstractDomain.WithTop
+  include PrettyPrintable.PrintableType
+
+  val ( <= ) : lhs:t -> rhs:t -> bool
+
+  val top : t
 
   val zero : t
 
diff --git a/infer/src/checkers/costDomain.ml b/infer/src/checkers/costDomain.ml
index 24a0f03dd..dcc181849 100644
--- a/infer/src/checkers/costDomain.ml
+++ b/infer/src/checkers/costDomain.ml
@@ -49,7 +49,7 @@ end
     {OperationCost, AllocationCost, IOCost} -> BasicCost.t
 *)
 module VariantCostMap = struct
-  include AbstractDomain.MapOfPPMap (CostKindMap) (BasicCost)
+  include PrettyPrintable.PPMonoMapOfPPMap (CostKindMap) (BasicCost)
 
   let[@warning "-32"] add _ = Logging.die InternalError "Don't call me"
 
diff --git a/infer/src/istd/PrettyPrintable.mli b/infer/src/istd/PrettyPrintable.mli
index 941cf1396..83e283783 100644
--- a/infer/src/istd/PrettyPrintable.mli
+++ b/infer/src/istd/PrettyPrintable.mli
@@ -140,5 +140,8 @@ module MakePPSet (Ord : PrintableOrderedType) : PPSet with type elt = Ord.t
 
 module MakePPMap (Ord : PrintableOrderedType) : PPMap with type key = Ord.t
 
+module PPMonoMapOfPPMap (M : PPMap) (Val : PrintableType) :
+  PPMonoMap with type key = M.key and type value = Val.t and type t = Val.t M.t
+
 module MakePPMonoMap (Ord : PrintableOrderedType) (Val : PrintableType) :
   PPMonoMap with type key = Ord.t and type value = Val.t