diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt
index 7ac6f5a5c..6bd9a43d3 100644
--- a/infer/man/man1/infer-full.txt
+++ b/infer/man/man1/infer-full.txt
@@ -1690,11 +1690,6 @@ INTERNAL OPTIONS
        --profiler-samples-reset
            Cancel the effect of --profiler-samples.
 
-       --pudge
-           Activates: Experimental flag to enable sledge arithmetic on path
-           conditions. This is intended for Pulse development only and will
-           be removed once the feature is stable. (Conversely: --no-pudge)
-
        --pulse-cut-to-one-path-procedures-pattern-reset
            Cancel the effect of --pulse-cut-to-one-path-procedures-pattern.
 
@@ -1814,11 +1809,6 @@ INTERNAL OPTIONS
        --skip-translation-headers-reset
            Set --skip-translation-headers to the empty list.
 
-       --sledge-timers
-           Activates: Enable debug timing info from sledge on stderr (you
-           probably want --no-progress-bar as well). (Conversely:
-           --no-sledge-timers)
-
        --source-files-filter-reset
            Cancel the effect of --source-files-filter.
 
diff --git a/infer/src/Makefile b/infer/src/Makefile
index d8560dbc8..5c6ce4576 100644
--- a/infer/src/Makefile
+++ b/infer/src/Makefile
@@ -153,7 +153,7 @@ roots:=Infer
 ifeq ($(IS_FACEBOOK_TREE),yes)
 roots += $(INFER_CREATE_TRACEVIEW_LINKS_MODULE)
 endif
-clusters:=absint al atd backend base biabduction bufferoverrun checkers clang clang_stubs concurrency cost c_stubs deadcode integration IR istd java labs llvm nullsafe opensource pulse quandary scripts test_determinator third-party topl unit
+clusters:=absint al atd backend base biabduction bufferoverrun checkers clang clang_stubs concurrency cost c_stubs deadcode integration IR istd java labs llvm nullsafe opensource pulse quandary scripts test_determinator topl unit
 
 ml_src_files:=$(shell find . -not -path "./*stubs*" -regex '\./[a-zA-Z].*\.ml\(i\)*')
 inc_flags:=$(foreach dir,$(shell find . -not -path './_build*' -type d),-I $(dir))
diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml
index dc0a1cda4..fdc135e86 100644
--- a/infer/src/base/Config.ml
+++ b/infer/src/base/Config.ml
@@ -1825,12 +1825,6 @@ and project_root =
     ~meta:"dir" "Specify the root directory of the project"
 
 
-and pudge =
-  CLOpt.mk_bool ~long:"pudge" ~default:false
-    "Experimental flag to enable sledge arithmetic on path conditions. This is intended for Pulse \
-     development only and will be removed once the feature is stable."
-
-
 and pulse_cut_to_one_path_procedures_pattern =
   CLOpt.mk_string_opt ~long:"pulse-cut-to-one-path-procedures-pattern"
     ~in_help:InferCommand.[(Analyze, manual_generic)]
@@ -2114,12 +2108,6 @@ and skip_translation_headers =
     ~meta:"path_prefix" "Ignore headers whose path matches the given prefix"
 
 
-and sledge_timers =
-  CLOpt.mk_bool ~long:"sledge-timers"
-    "Enable debug timing info from sledge on stderr (you probably want $(b,--no-progress-bar) as \
-     well)."
-
-
 and source_preview =
   CLOpt.mk_bool ~long:"source-preview" ~default:true
     ~in_help:InferCommand.[(Explore, manual_explore_bugs)]
@@ -2993,8 +2981,6 @@ and progress_bar =
 
 and project_root = !project_root
 
-and pudge = !pudge
-
 and pulse_cut_to_one_path_procedures_pattern =
   Option.map ~f:Str.regexp !pulse_cut_to_one_path_procedures_pattern
 
@@ -3110,8 +3096,6 @@ and skip_duplicated_types = !skip_duplicated_types
 
 and skip_translation_headers = !skip_translation_headers
 
-and sledge_timers = !sledge_timers
-
 and source_preview = !source_preview
 
 and source_files = !source_files
diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli
index ca0dc3278..bfc793138 100644
--- a/infer/src/base/Config.mli
+++ b/infer/src/base/Config.mli
@@ -451,8 +451,6 @@ val progress_bar : [`MultiLine | `Plain | `Quiet]
 
 val project_root : string
 
-val pudge : bool
-
 val pulse_cut_to_one_path_procedures_pattern : Str.regexp option
 
 val pulse_recency_limit : int
@@ -541,8 +539,6 @@ val skip_duplicated_types : bool
 
 val skip_translation_headers : string list
 
-val sledge_timers : bool
-
 val source_files : bool
 
 val source_files_cfg : bool
diff --git a/infer/src/cost/dune b/infer/src/cost/dune
index 52bfdd928..f637acecb 100644
--- a/infer/src/cost/dune
+++ b/infer/src/cost/dune
@@ -9,6 +9,6 @@
  (flags
   (:standard -open Core -open OpenSource -open IR -open IStdlib -open IStd
     -open ATDGenerated -open IBase -open Absint -open BO -open Checkers))
- (libraries core sledge IStdlib ATDGenerated IBase IR Absint BO Checkers)
+ (libraries core IStdlib ATDGenerated IBase IR Absint BO Checkers)
  (preprocess (pps ppx_compare))
 )
diff --git a/infer/src/deadcode/dune.in b/infer/src/deadcode/dune.in
index d22d66aa6..2d1123cba 100644
--- a/infer/src/deadcode/dune.in
+++ b/infer/src/deadcode/dune.in
@@ -8,7 +8,7 @@
  (modes byte)
  (flags (:standard -w +60))
  (libraries javalib ANSITerminal async atdgen base base64 cmdliner core
-   mtime.clock.os ocamlgraph oUnit parmap re sawja sledge sqlite3 str unix xmlm
+   mtime.clock.os ocamlgraph oUnit parmap re sawja sqlite3 str unix xmlm
    yojson zarith zip CStubs)
  (modules All_infer_in_one_file)
  (preprocess (pps ppx_blob ppx_compare ppx_enumerate ppx_fields_conv ppx_hash ppx_sexp_conv ppx_variants_conv -no-check))
diff --git a/infer/src/pulse/Pudge.ml b/infer/src/pulse/Pudge.ml
deleted file mode 100644
index 5e77c3f5d..000000000
--- a/infer/src/pulse/Pudge.ml
+++ /dev/null
@@ -1,13 +0,0 @@
-(*
- * Copyright (c) Facebook, Inc. and its affiliates.
- *
- * This source code is licensed under the MIT license found in the
- * LICENSE file in the root directory of this source tree.
- *)
-
-open! IStd
-
-module Pudge = ( val if Config.pudge then (module PulseSledge) else (module PulseDummySledge)
-                   : Pudge_intf.S )
-
-include Pudge
diff --git a/infer/src/pulse/Pudge.mli b/infer/src/pulse/Pudge.mli
deleted file mode 100644
index d61ffc8d3..000000000
--- a/infer/src/pulse/Pudge.mli
+++ /dev/null
@@ -1,10 +0,0 @@
-(*
- * Copyright (c) Facebook, Inc. and its affiliates.
- *
- * This source code is licensed under the MIT license found in the
- * LICENSE file in the root directory of this source tree.
- *)
-
-open! IStd
-
-include Pudge_intf.S
diff --git a/infer/src/pulse/Pudge_intf.ml b/infer/src/pulse/Pudge_intf.ml
deleted file mode 100644
index 132fa87d4..000000000
--- a/infer/src/pulse/Pudge_intf.ml
+++ /dev/null
@@ -1,73 +0,0 @@
-(*
- * Copyright (c) Facebook, Inc. and its affiliates.
- *
- * This source code is licensed under the MIT license found in the
- * LICENSE file in the root directory of this source tree.
- *)
-
-open! IStd
-module F = Format
-module AbstractValue = PulseAbstractValue
-
-module type S = sig
-  type t
-
-  val pp : F.formatter -> t -> unit
-
-  val true_ : t
-
-  module Var : sig
-    type t
-
-    val of_absval : AbstractValue.t -> t
-
-    val to_absval : t -> AbstractValue.t
-    (** use with caution: will crash the program if the given variable wasn't generated from an
-        [AbstractValue.t] using [Var.of_absval] *)
-  end
-
-  module Term : sig
-    type t
-
-    val zero : t
-
-    val of_intlit : IntLit.t -> t
-
-    val of_absval : AbstractValue.t -> t
-
-    val of_unop : Unop.t -> t -> t option
-
-    val of_binop : Binop.t -> t -> t -> t option
-  end
-
-  module Formula : sig
-    type t
-
-    val eq : Term.t -> Term.t -> t
-
-    val lt : Term.t -> Term.t -> t
-
-    val not_ : t -> t
-
-    val term_binop : Binop.t -> Term.t -> Term.t -> t option
-  end
-
-  val and_formula : Formula.t -> t -> t
-
-  val and_ : t -> t -> t
-
-  (** queries *)
-
-  val is_unsat : t -> bool
-
-  val is_known_zero : Term.t -> t -> bool
-  (** [is_known_zero phi t] returns [true] if [phi |- t = 0], [false] if we don't know for sure *)
-
-  (** operations *)
-
-  val fold_map_variables : t -> init:'a -> f:('a -> Var.t -> 'a * Var.t) -> 'a * t
-
-  val simplify : keep:AbstractValue.Set.t -> t -> t
-  (** [simplify ~keep phi] attempts to get rid of as many variables in [fv phi] but not in [keep] as
-      possible *)
-end
diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml
index 69e543112..dc207ecee 100644
--- a/infer/src/pulse/Pulse.ml
+++ b/infer/src/pulse/Pulse.ml
@@ -299,23 +299,6 @@ module DisjunctiveAnalyzer =
       let widen_policy = `UnderApproximateAfterNumIterations Config.pulse_widen_threshold
     end)
 
-(* Output cases that sledge was unhappy with in files for later replay or inclusion as sledge test
-   cases. We create one file for each PID to avoid all analysis processes racing on writing to the same
-   file. *)
-let sledge_test_fmt =
-  lazy
-    (let sledge_test_output =
-       Out_channel.create
-         ( ResultsDir.get_path Debug
-         ^/ Printf.sprintf "sledge_test-%d.ml" (Pid.to_int (Unix.getpid ())) )
-     in
-     let f = F.formatter_of_out_channel sledge_test_output in
-     Epilogues.register ~description:"closing sledge debug fd" ~f:(fun () ->
-         F.pp_print_flush f () ;
-         Out_channel.close sledge_test_output ) ;
-     f )
-
-
 let checker ({InterproceduralAnalysis.proc_desc} as analysis_data) =
   AbstractValue.State.reset () ;
   let initial = [ExecutionDomain.mk_initial proc_desc] in
@@ -324,29 +307,3 @@ let checker ({InterproceduralAnalysis.proc_desc} as analysis_data) =
       Some (PulseSummary.of_posts proc_desc posts)
   | None ->
       None
-  | exception exn ->
-      (* output sledge replay tests, see comment on [sledge_test_fmt] *)
-      IExn.reraise_if exn ~f:(fun () ->
-          match Exn.sexp_of_t exn with
-          | List [exn; replay] ->
-              let exn = Error.t_of_sexp exn in
-              L.internal_error "Analysis of %a FAILED:@\n@[%a@]@\n" Procname.pp
-                (Procdesc.get_proc_name proc_desc)
-                Error.pp exn ;
-              F.fprintf (Lazy.force sledge_test_fmt)
-                "@\n\
-                \    let%%expect_test _ =@\n\
-                \      Equality.replay@\n\
-                \        {|%a|} ;@\n\
-                \      [%%expect {| |}]@\n\
-                 @\n\
-                 %!"
-                Sexp.pp_hum replay ;
-              false
-          | _ | (exception _) ->
-              (* re-raise original exception *)
-              true ) ;
-      None
-
-
-let () = NS.Timer.enabled := Config.sledge_timers
diff --git a/infer/src/pulse/PulseBasicInterface.ml b/infer/src/pulse/PulseBasicInterface.ml
index ea025227e..514462d10 100644
--- a/infer/src/pulse/PulseBasicInterface.ml
+++ b/infer/src/pulse/PulseBasicInterface.ml
@@ -36,8 +36,6 @@ include struct
   [@@deprecated "use the short form PathCondition instead"]
   module PulseSkippedCalls = PulseSkippedCalls
   [@@deprecated "use the short form SkippedCalls instead"]
-  module PulseSledge = PulseSledge [@@deprecated "use Pudge instead"]
-  module PulseDummySledge = PulseDummySledge [@@deprecated "use Pudge instead"]
   module PulseTrace = PulseTrace [@@deprecated "use the short form Trace instead"]
   module PulseValueHistory = PulseValueHistory
   [@@deprecated "use the short form ValueHistory instead"]
diff --git a/infer/src/pulse/PulseDummySledge.ml b/infer/src/pulse/PulseDummySledge.ml
deleted file mode 100644
index a8b2061b4..000000000
--- a/infer/src/pulse/PulseDummySledge.ml
+++ /dev/null
@@ -1,65 +0,0 @@
-(*
- * Copyright (c) Facebook, Inc. and its affiliates.
- *
- * This source code is licensed under the MIT license found in the
- * LICENSE file in the root directory of this source tree.
- *)
-
-open! IStd
-module F = Format
-
-module Var = struct
-  type t = unit
-
-  let of_absval _ = ()
-
-  let to_absval () = assert false
-end
-
-module Term = struct
-  type t = unit
-
-  let zero = ()
-
-  let of_intlit _ = ()
-
-  let of_absval _ = ()
-
-  let of_unop _ () = None
-
-  let of_binop _ () () = None
-end
-
-module Formula = struct
-  type t = unit
-
-  let eq () () = ()
-
-  let lt () () = ()
-
-  let not_ () = ()
-
-  let term_binop _ () () = None
-end
-
-(* same type as {!PulsePathCondition.t} to be nice to summary serialization *)
-type t = {eqs: Ses.Equality.t lazy_t; non_eqs: Ses.Term.t lazy_t}
-
-(* still print to make sure the formula never changes in debug *)
-let pp fmt {eqs= (lazy eqs); non_eqs= (lazy non_eqs)} =
-  F.fprintf fmt "%a∧%a" Ses.Equality.pp eqs Ses.Term.pp non_eqs
-
-
-let true_ = {eqs= Lazy.from_val Ses.Equality.true_; non_eqs= Lazy.from_val Ses.Term.true_}
-
-let and_formula () phi = phi
-
-let and_ phi1 _ = phi1
-
-let is_known_zero () _ = false
-
-let is_unsat _ = false
-
-let fold_map_variables phi ~init ~f:_ = (init, phi)
-
-let simplify ~keep:_ phi = phi
diff --git a/infer/src/pulse/PulseDummySledge.mli b/infer/src/pulse/PulseDummySledge.mli
deleted file mode 100644
index d61ffc8d3..000000000
--- a/infer/src/pulse/PulseDummySledge.mli
+++ /dev/null
@@ -1,10 +0,0 @@
-(*
- * Copyright (c) Facebook, Inc. and its affiliates.
- *
- * This source code is licensed under the MIT license found in the
- * LICENSE file in the root directory of this source tree.
- *)
-
-open! IStd
-
-include Pudge_intf.S
diff --git a/infer/src/pulse/PulsePathCondition.ml b/infer/src/pulse/PulsePathCondition.ml
index 32dcaee84..18ce34725 100644
--- a/infer/src/pulse/PulsePathCondition.ml
+++ b/infer/src/pulse/PulsePathCondition.ml
@@ -376,7 +376,7 @@ let prune_binop ~negated bop lhs_op rhs_op ({satisfiable; bo_itvs= _; citvs; for
 (** {2 Queries} *)
 
 let is_known_zero phi v =
-  (* don't ask sledge because it might be too expensive *)
+  (* TODO: ask [Formula] too *)
   CItvs.find_opt v phi.citvs |> Option.value_map ~default:false ~f:CItv.is_equal_to_zero
   || BoItvs.find_opt v phi.bo_itvs |> Option.value_map ~default:false ~f:Itv.ItvPure.is_zero
 
diff --git a/infer/src/pulse/PulseSledge.ml b/infer/src/pulse/PulseSledge.ml
deleted file mode 100644
index d9a47c529..000000000
--- a/infer/src/pulse/PulseSledge.ml
+++ /dev/null
@@ -1,157 +0,0 @@
-(*
- * Copyright (c) Facebook, Inc. and its affiliates.
- *
- * This source code is licensed under the MIT license found in the
- * LICENSE file in the root directory of this source tree.
- *)
-
-open! IStd
-module L = Logging
-module AbstractValue = PulseAbstractValue
-
-[@@@warning "+9"]
-
-module Var = struct
-  module Var = Sledge.Fol.Var
-
-  let of_absval (v : AbstractValue.t) = Var.identified ~name:"v" ~id:(v :> int)
-
-  let to_absval v =
-    assert (String.equal (Var.name v) "v") ;
-    Var.id v |> AbstractValue.of_id
-
-
-  include Var
-end
-
-module Term = struct
-  module Term = Sledge.Fol.Term
-
-  let of_intlit i = Term.integer (IntLit.to_big_int i)
-
-  let of_absval v = Term.var (Var.of_absval v)
-
-  let of_unop (unop : Unop.t) t = match unop with Neg -> Some (Term.neg t) | BNot | LNot -> None
-
-  let of_binop (binop : Binop.t) t1 t2 =
-    let open Term in
-    match binop with
-    | PlusA _ | PlusPI ->
-        Some (add t1 t2)
-    | MinusA _ | MinusPI | MinusPP ->
-        Some (sub t1 t2)
-    | Mult _ ->
-        Some (mul t1 t2)
-    | Div | Mod | Shiftlt | Shiftrt | Lt | Gt | Le | Ge | Eq | Ne | BAnd | LAnd | BOr | LOr | BXor
-      ->
-        None
-
-
-  include Term
-end
-
-module Formula = struct
-  module Formula = Sledge.Fol.Formula
-
-  let term_binop (binop : Binop.t) t1 t2 =
-    match binop with
-    | BAnd
-    | BOr
-    | BXor
-    | PlusA _
-    | PlusPI
-    | MinusA _
-    | MinusPI
-    | MinusPP
-    | Mult _
-    | Div
-    | Mod
-    | Shiftlt
-    | Shiftrt ->
-        Term.of_binop binop t1 t2 |> Option.map ~f:(fun t -> Formula.dq t Term.zero)
-    | Lt ->
-        Some (Formula.lt t1 t2)
-    | Gt ->
-        Some (Formula.lt t2 t1)
-    | Le ->
-        Some (Formula.le t1 t2)
-    | Ge ->
-        Some (Formula.le t2 t1)
-    | Eq ->
-        Some (Formula.eq t1 t2)
-    | Ne ->
-        Some (Formula.dq t1 t2)
-    | LAnd ->
-        Option.both (Formula.project t1) (Formula.project t2)
-        |> Option.map ~f:(fun (f1, f2) -> Formula.and_ f1 f2)
-    | LOr ->
-        Option.both (Formula.project t1) (Formula.project t2)
-        |> Option.map ~f:(fun (f1, f2) -> Formula.or_ f1 f2)
-
-
-  include Formula
-end
-
-module Context = struct
-  include Sledge.Fol.Context
-
-  let assert_no_new_vars api new_vars =
-    if not (Var.Set.is_empty new_vars) then
-      L.die InternalError "Huho, %s generated fresh new variables %a" api Var.Set.pp new_vars
-
-
-  let and_formula phi r =
-    let new_vars, r' = Sledge.Fol.Context.and_formula Var.Set.empty phi r in
-    assert_no_new_vars "Context.and_formula" new_vars ;
-    r'
-
-
-  let and_ r1 r2 =
-    let new_vars, r' = Sledge.Fol.Context.and_ Var.Set.empty r1 r2 in
-    assert_no_new_vars "Context.and_" new_vars ;
-    r'
-
-
-  let apply_subst subst r =
-    let new_vars, r' = Sledge.Fol.Context.apply_subst Var.Set.empty subst r in
-    assert_no_new_vars "Context.apply_subst" new_vars ;
-    r'
-end
-
-type t = Context.t lazy_t
-
-let pp fmt (lazy phi) = Context.pp fmt phi
-
-let true_ = Lazy.from_val Context.true_
-
-let and_formula f phi = lazy (Context.and_formula f (Lazy.force phi))
-
-let and_ phi1 phi2 = lazy (Context.and_ (Lazy.force phi1) (Lazy.force phi2))
-
-let is_known_zero t phi = Context.entails_eq (Lazy.force phi) t Term.zero
-
-let is_unsat phi = Context.is_false (Lazy.force phi)
-
-let fv (lazy phi) = Context.fv phi
-
-let fold_map_variables phi ~init ~f =
-  let acc, phi' =
-    Context.classes (Lazy.force phi)
-    |> Term.Map.fold ~init:(init, Context.true_) ~f:(fun ~key:t ~data:equal_ts (acc, phi') ->
-           let acc, t' = Term.fold_map_vars ~init:acc ~f t in
-           List.fold equal_ts ~init:(acc, phi') ~f:(fun (acc, phi') equal_t ->
-               let acc, t_mapped = Term.fold_map_vars ~init:acc ~f equal_t in
-               (acc, Context.and_formula (Formula.eq t' t_mapped) phi') ) )
-  in
-  (acc, Lazy.from_val phi')
-
-
-let simplify ~keep phi =
-  let all_vs = fv phi in
-  let keep_vs =
-    AbstractValue.Set.fold
-      (fun v keep_vs -> Var.Set.add keep_vs (Var.of_absval v))
-      keep Var.Set.empty
-  in
-  let simpl_subst = Context.solve_for_vars [keep_vs; all_vs] (Lazy.force phi) in
-  Lazy.from_val (Context.apply_subst simpl_subst (Lazy.force phi))
diff --git a/infer/src/pulse/PulseSledge.mli b/infer/src/pulse/PulseSledge.mli
deleted file mode 100644
index d61ffc8d3..000000000
--- a/infer/src/pulse/PulseSledge.mli
+++ /dev/null
@@ -1,10 +0,0 @@
-(*
- * Copyright (c) Facebook, Inc. and its affiliates.
- *
- * This source code is licensed under the MIT license found in the
- * LICENSE file in the root directory of this source tree.
- *)
-
-open! IStd
-
-include Pudge_intf.S
diff --git a/infer/src/pulse/dune b/infer/src/pulse/dune
index 876a4c628..1f4335d8d 100644
--- a/infer/src/pulse/dune
+++ b/infer/src/pulse/dune
@@ -9,6 +9,6 @@
  (flags
   (:standard -open Core -open IR -open IStdlib -open IStd -open ATDGenerated
     -open IBase -open Absint -open BO))
- (libraries core sledge IStdlib ATDGenerated IBase IR Absint BO)
+ (libraries core IStdlib ATDGenerated IBase IR Absint BO)
  (preprocess (pps ppx_compare ppx_variants_conv))
 )
diff --git a/infer/src/third-party/dune b/infer/src/third-party/dune
deleted file mode 100644
index 84e7688f0..000000000
--- a/infer/src/third-party/dune
+++ /dev/null
@@ -1,5 +0,0 @@
-; Copyright (c) Facebook, Inc. and its affiliates.
-;
-; This source code is licensed under the MIT license found in the
-; LICENSE file in the root directory of this source tree.
-(vendored_dirs *)
diff --git a/infer/src/third-party/sledge b/infer/src/third-party/sledge
deleted file mode 120000
index 312583db0..000000000
--- a/infer/src/third-party/sledge
+++ /dev/null
@@ -1 +0,0 @@
-../../../sledge
\ No newline at end of file