diff --git a/src/arith/lra/linear_expr_intf.ml b/src/arith/lra/linear_expr_intf.ml
index 3e9b5142..29ad15b5 100644
--- a/src/arith/lra/linear_expr_intf.ml
+++ b/src/arith/lra/linear_expr_intf.ml
@@ -55,6 +55,8 @@ module type VAR = sig
   type lit
 
   val pp_lit : lit Fmt.printer
+
+  val not_lit : lit -> lit option
 end
 
 type bool_op = Predicate.t = Leq | Geq | Lt | Gt | Eq | Neq
diff --git a/src/arith/lra/sidekick_arith_lra.ml b/src/arith/lra/sidekick_arith_lra.ml
index ee06e9b6..46f3f0c3 100644
--- a/src/arith/lra/sidekick_arith_lra.ml
+++ b/src/arith/lra/sidekick_arith_lra.ml
@@ -120,6 +120,9 @@ module Make(A : ARG) : S with module A = A = struct
     let compare = A.S.T.Term.compare
     type lit = Tag.t
     let pp_lit = Tag.pp
+    let not_lit = function
+      | Tag.Lit l -> Some (Tag.Lit (Lit.neg l))
+      | _ -> None
   end
 
   module LE_ = Linear_expr.Make(struct include Q let pp=pp_print end)(SimpVar)
@@ -213,8 +216,10 @@ module Make(A : ARG) : S with module A = A = struct
         if LE_.Comb.is_empty le_comb then (
           Log.debug 50 "(lra.encode-le.is-trivially-0)";
           SimpSolver.add_constraint self.simplex
+            ~on_propagate:(fun _ ~reason:_ -> ())
             (SimpSolver.Constraint.leq proxy Q.zero) Tag.By_def;
           SimpSolver.add_constraint self.simplex
+            ~on_propagate:(fun _ ~reason:_ -> ())
             (SimpSolver.Constraint.geq proxy Q.zero) Tag.By_def;
         ) else (
           LE_.Comb.iter (fun v _ -> SimpSolver.add_var self.simplex v) le_comb;
@@ -280,6 +285,11 @@ module Make(A : ARG) : S with module A = A = struct
           in
 
           let new_t = A.mk_lra tst (LRA_simplex_pred (proxy, op, le_const)) in
+          begin
+            let lit = mk_lit new_t in
+            let constr = SimpSolver.Constraint.mk proxy op le_const in
+            SimpSolver.declare_bound self.simplex constr (Tag.Lit lit);
+          end;
 
           Log.debugf 10 (fun k->k "lra.preprocess:@ %a@ :into %a" T.pp t T.pp new_t);
           Some new_t
@@ -300,6 +310,11 @@ module Make(A : ARG) : S with module A = A = struct
           let op = if Q.(coeff < zero) then S_op.neg_sign op else op in
 
           let new_t = A.mk_lra tst (LRA_simplex_pred (v, op, q)) in
+          begin
+            let lit = mk_lit new_t in
+            let constr = SimpSolver.Constraint.mk v op q in
+            SimpSolver.declare_bound self.simplex constr (Tag.Lit lit);
+          end;
 
           Log.debugf 10 (fun k->k "lra.preprocess@ :%a@ :into %a" T.pp t T.pp new_t);
           Some new_t
@@ -387,9 +402,21 @@ module Make(A : ARG) : S with module A = A = struct
     in
     SI.raise_conflict si acts confl SI.P.default
 
+  let on_propagate_ si acts lit ~reason =
+    match lit with
+    | Tag.Lit lit ->
+      SI.propagate si acts lit
+        (fun() -> CCList.flat_map (Tag.to_lits si) reason)
+    | _ -> ()
+
   let check_simplex_ self si acts : SimpSolver.Subst.t =
     Log.debug 5 "lra: call arith solver";
-    let res = Profile.with1 "simplex.solve" SimpSolver.check self.simplex in
+    let res =
+      Profile.with_ "simplex.solve"
+        (fun () ->
+           SimpSolver.check self.simplex
+             ~on_propagate:(on_propagate_ si acts))
+    in
     begin match res with
       | SimpSolver.Sat m -> m
       | SimpSolver.Unsat cert ->
@@ -416,9 +443,11 @@ module Make(A : ARG) : S with module A = A = struct
     begin
       try
         let c1 = SimpSolver.Constraint.geq v le_const in
-        SimpSolver.add_constraint self.simplex c1 lit;
+        SimpSolver.add_constraint self.simplex c1 lit
+          ~on_propagate:(on_propagate_ si acts);
         let c2 = SimpSolver.Constraint.leq v le_const in
-        SimpSolver.add_constraint self.simplex c2 lit;
+        SimpSolver.add_constraint self.simplex c2 lit
+          ~on_propagate:(on_propagate_ si acts);
       with SimpSolver.E_unsat cert ->
         fail_with_cert si acts cert
     end;
@@ -492,6 +521,8 @@ module Make(A : ARG) : S with module A = A = struct
       (fun lit ->
          let sign = SI.Lit.sign lit in
          let lit_t = SI.Lit.term lit in
+         Log.debugf 50 (fun k->k "(@[lra.partial-check.add@ :lit %a@ :lit-t %a@])"
+                           SI.Lit.pp lit T.pp lit_t);
          match A.view_as_lra lit_t with
          | LRA_simplex_pred (v, op, q) ->
 
@@ -508,6 +539,7 @@ module Make(A : ARG) : S with module A = A = struct
              try
                SimpSolver.add_var self.simplex v;
                SimpSolver.add_constraint self.simplex constr (Tag.Lit lit)
+                 ~on_propagate:(on_propagate_ si acts);
              with SimpSolver.E_unsat cert ->
                Log.debugf 10
                  (fun k->k "(@[lra.partial-check.unsat@ :cert %a@])"
diff --git a/src/arith/lra/simplex2.ml b/src/arith/lra/simplex2.ml
index 1ddf1f37..faba6681 100644
--- a/src/arith/lra/simplex2.ml
+++ b/src/arith/lra/simplex2.ml
@@ -93,22 +93,37 @@ module type S = sig
 
   exception E_unsat of Unsat_cert.t
 
+  type ev_on_propagate = V.lit -> reason:V.lit list -> unit
+
   val add_var : t -> V.t -> unit
   (** Make sure the variable exists in the simplex. *)
 
-  val add_constraint : t -> Constraint.t -> V.lit -> unit
+  val add_constraint :
+    on_propagate:ev_on_propagate ->
+    t -> Constraint.t -> V.lit -> unit
   (** Add a constraint to the simplex.
       @raise Unsat if it's immediately obvious that this is not satisfiable. *)
 
-  val check_exn : t -> unit
+  val declare_bound : t -> Constraint.t -> V.lit -> unit
+  (** Declare that this constraint exists, so we can possibly propagate it.
+      Unlike {!add_constraint} this does {b NOT} assert that the constraint
+      is true *)
+
+  val check_exn :
+    on_propagate:(V.lit -> reason:V.lit list -> unit) ->
+    t -> unit
   (** Check the whole simplex for satisfiability.
+      @param on_propagate is called with arguments [lit, reason] whenever
+      [reason => lit] is found to be true by the simplex.
       @raise Unsat if the constraints are not satisfiable. *)
 
   type result =
     | Sat of Subst.t
     | Unsat of Unsat_cert.t
 
-  val check : t -> result
+  val check :
+    on_propagate:(V.lit -> reason:V.lit list -> unit) ->
+    t -> result
   (** Call {!check_exn} and return a model or a proof of unsat. *)
 
   (**/**)
@@ -218,6 +233,7 @@ module Make(Var: VAR)
     b_lit: Var.lit;
   }
 
+  type is_lower = bool
   type var_state = {
     var: V.t;
     mutable value: erat;
@@ -225,6 +241,7 @@ module Make(Var: VAR)
     mutable basic_idx: int; (* index of the row in the matrix, if any. -1 otherwise *)
     mutable l_bound: bound option;
     mutable u_bound: bound option;
+    mutable all_bound_lits : (is_lower * bound) list; (* all known literals on this var *)
   }
 
   (** {2 Matrix}
@@ -375,6 +392,7 @@ module Make(Var: VAR)
     stat_check: int Stat.counter;
     stat_unsat: int Stat.counter;
     stat_define: int Stat.counter;
+    stat_propagate: int Stat.counter;
   }
 
   let push_level self : unit =
@@ -462,6 +480,7 @@ module Make(Var: VAR)
               basic_idx=row_idx;
               l_bound=None;
               u_bound=None;
+              all_bound_lits=[];
             })
     in
     Log.debugf 5 (fun k->k "(@[simplex.define@ @[v%d :var %a@]@ :linexpr %a@])"
@@ -516,6 +535,7 @@ module Make(Var: VAR)
         l_bound=None;
         u_bound=None;
         value=Erat.zero;
+        all_bound_lits=[];
       } in
       assert (Var_state.is_n_basic vs);
       self.var_tbl <- V_map.add x vs self.var_tbl;
@@ -666,11 +686,13 @@ module Make(Var: VAR)
 
   exception E_unsat of Unsat_cert.t
 
+  type ev_on_propagate = V.lit -> reason:V.lit list -> unit
+
   let add_var self (v:V.t) : unit =
     ignore (find_or_create_n_basic_var_ self v : var_state);
     ()
 
-  let add_constraint (self:t) (c:Constraint.t) (lit:V.lit) : unit =
+  let add_constraint ~on_propagate (self:t) (c:Constraint.t) (lit:V.lit) : unit =
     let open Constraint in
 
     let vs = find_or_create_n_basic_var_ self c.lhs in
@@ -700,6 +722,23 @@ module Make(Var: VAR)
           Backtrack_stack.push self.bound_stack (vs, `Lower, vs.l_bound);
           vs.l_bound <- Some new_bnd;
 
+          (* propagate *)
+          List.iter
+            (fun (is_lower', bnd) ->
+               if is_lower' && Erat.(bnd.b_val < new_bnd.b_val) then (
+                 (* subsumed *)
+                 Stat.incr self.stat_propagate;
+                 on_propagate (bnd.b_lit) ~reason:[new_bnd.b_lit];
+               ) else if not is_lower' && Erat.(bnd.b_val < new_bnd.b_val) then (
+                 (* incompatible upper bound *)
+                 match V.not_lit bnd.b_lit with
+                 | Some l' ->
+                   Stat.incr self.stat_propagate;
+                   on_propagate l' ~reason:[new_bnd.b_lit];
+                 | None -> ()
+               )
+            ) vs.all_bound_lits;
+
           if Var_state.is_n_basic vs &&
              Erat.(vs.value < new_bnd.b_val) then (
             (* line 5: need to update non-basic variable *)
@@ -719,6 +758,23 @@ module Make(Var: VAR)
           Backtrack_stack.push self.bound_stack (vs, `Upper, vs.u_bound);
           vs.u_bound <- Some new_bnd;
 
+          (* propagate *)
+          List.iter
+            (fun (is_lower', bnd) ->
+               if not is_lower' && Erat.(bnd.b_val > new_bnd.b_val) then (
+                 (* subsumed *)
+                 Stat.incr self.stat_propagate;
+                 on_propagate (bnd.b_lit) ~reason:[new_bnd.b_lit];
+               ) else if is_lower' && Erat.(bnd.b_val > new_bnd.b_val) then (
+                 (* incompatible lower bound *)
+                 match V.not_lit bnd.b_lit with
+                 | Some l' ->
+                   Stat.incr self.stat_propagate;
+                   on_propagate l' ~reason:[new_bnd.b_lit];
+                 | None -> ()
+               )
+            ) vs.all_bound_lits;
+
           if Var_state.is_n_basic vs &&
              Erat.(vs.value > new_bnd.b_val) then (
             (* line 5: need to update non-basic variable *)
@@ -727,6 +783,22 @@ module Make(Var: VAR)
       end
     )
 
+  let declare_bound (self:t) (c:Constraint.t) (lit:V.lit) : unit =
+    let vs = find_or_create_n_basic_var_ self c.lhs in
+    Log.debugf 10
+      (fun k->k "(@[simplex2.declare-bound@ %a@ :lit %a@])"
+          Constraint.pp c V.pp_lit lit);
+
+    let is_lower_bnd, new_bnd_val =
+      match c.op with
+      | Leq -> false, Erat.make_q c.rhs
+      | Lt -> false, Erat.make c.rhs Q.minus_one
+      | Geq -> true, Erat.make_q c.rhs
+      | Gt -> true, Erat.make c.rhs Q.one
+    in
+    let new_bnd = is_lower_bnd, {b_val=new_bnd_val; b_lit=lit} in
+    vs.all_bound_lits <- new_bnd :: vs.all_bound_lits
+
   (* try to find basic variable that doesn't respect one of its bounds *)
   let find_basic_var_ (self:t) : (var_state * [`Lower | `Upper] * bound) option =
     let n = Matrix.n_rows self.matrix in
@@ -815,7 +887,7 @@ module Make(Var: VAR)
 
   (* main satisfiability check.
      page 15, figure 3.2 *)
-  let check_exn (self:t) : unit =
+  let check_exn ~on_propagate:_ (self:t) : unit =
     let exception Stop in
     Log.debugf 20 (fun k->k "(@[simplex2.check@ %a@])" pp_stats self);
     Stat.incr self.stat_check;
@@ -894,6 +966,7 @@ module Make(Var: VAR)
       stat_check=Stat.mk_int stat "simplex.check";
       stat_unsat=Stat.mk_int stat "simplex.unsat";
       stat_define=Stat.mk_int stat "simplex.define";
+      stat_propagate=Stat.mk_int stat "simplex.propagate";
     } in
     self
 
@@ -987,9 +1060,9 @@ module Make(Var: VAR)
       (fun k->k "(@[simplex2.model@ %a@])" Subst.pp subst);
     subst
 
-  let check (self:t) : result =
+  let check ~on_propagate (self:t) : result =
     try
-      check_exn self;
+      check_exn ~on_propagate self;
       let m = model_ self in
       Sat m
     with E_unsat c -> Unsat c
diff --git a/src/arith/tests/test_simplex2.ml b/src/arith/tests/test_simplex2.ml
index f22959d8..4920cc18 100644
--- a/src/arith/tests/test_simplex2.ml
+++ b/src/arith/tests/test_simplex2.ml
@@ -14,6 +14,7 @@ module Var = struct
   let rand n : t QC.arbitrary = QC.make ~print:(Fmt.to_string pp) @@ QC.Gen.(0--n)
   type lit = int
   let pp_lit = Fmt.int
+  let not_lit i = Some (- i)
 end
 
 module Spl = Sidekick_arith_lra.Simplex2.Make(Var)
@@ -155,18 +156,20 @@ module Step = struct
   let rand : t list QC.arbitrary = rand_for 1 100
 end
 
+let on_propagate _ ~reason:_ = ()
+
 (* add a single step to the simplexe *)
 let add_step simplex (s:Step.t) : unit =
   begin match s with
     | Step.S_new_var v -> Spl.add_var simplex v
     | Step.S_leq (v,n) ->
-      Spl.add_constraint simplex (Spl.Constraint.leq v n) 0
+      Spl.add_constraint simplex (Spl.Constraint.leq v n) 0 ~on_propagate
     | Step.S_lt (v,n) ->
-      Spl.add_constraint simplex (Spl.Constraint.lt v n) 0
+      Spl.add_constraint simplex (Spl.Constraint.lt v n) 0 ~on_propagate
     | Step.S_geq (v,n) ->
-      Spl.add_constraint simplex (Spl.Constraint.geq v n) 0
+      Spl.add_constraint simplex (Spl.Constraint.geq v n) 0 ~on_propagate
     | Step.S_gt (v,n) ->
-      Spl.add_constraint simplex (Spl.Constraint.gt v n) 0
+      Spl.add_constraint simplex (Spl.Constraint.gt v n) 0 ~on_propagate
     | Step.S_define (x,le) ->
       Spl.define simplex x le
   end
@@ -179,18 +182,18 @@ let add_steps ?(f=fun()->()) (simplex:Spl.t) l : unit =
 
 (* is this simplex's state sat? *)
 let check_simplex_is_sat simplex : bool =
-  (try Spl.check_exn simplex; true
+  (try Spl.check_exn ~on_propagate simplex; true
    with Spl.E_unsat _ -> false)
 
 (* is this problem sat? *)
 let check_pb_is_sat pb : bool =
   let simplex = Spl.create() in
-  (try add_steps simplex pb; Spl.check_exn simplex; true
+  (try add_steps simplex pb; Spl.check_exn ~on_propagate simplex; true
    with Spl.E_unsat _ -> false)
 
 let check_steps l : bool =
   let simplex = Spl.create () in
-  try add_steps simplex l; Spl.check_exn simplex; true
+  try add_steps simplex l; Spl.check_exn ~on_propagate simplex; true
   with _ -> false
 
 (* basic debug printer for Q.t *)
@@ -200,7 +203,7 @@ let prop_sound ?(inv=false) pb =
   let simplex = Spl.create () in
   begin match
       add_steps simplex pb;
-      Spl.check simplex
+      Spl.check ~on_propagate simplex
     with
     | Sat subst ->
 
@@ -279,7 +282,7 @@ let prop_invariants pb =
   let simplex = Spl.create () in
   (try
     add_steps simplex pb ~f:(fun () -> Spl._check_invariants simplex);
-    Spl.check_exn simplex
+    Spl.check_exn ~on_propagate simplex
    with Spl.E_unsat _ -> ());
   Spl._check_invariants simplex;
   true
@@ -337,7 +340,7 @@ let check_scalable =
     let simplex = Spl.create () in
     (try
       add_steps simplex pb;
-      Spl.check_exn simplex
+      Spl.check_exn ~on_propagate simplex
      with _ -> ());
     true
   in