diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml
index bc7dea518..a5c39c121 100644
--- a/infer/src/pulse/PulseAbductiveDomain.ml
+++ b/infer/src/pulse/PulseAbductiveDomain.ml
@@ -1052,6 +1052,15 @@ let incorporate_new_eqs new_eqs astate =
         Error (`PotentialInvalidAccess (astate, address, must_be_valid))
 
 
+let incorporate_new_eqs_on_val new_eqs v =
+  List.find_map new_eqs ~f:(function
+    | PulseFormula.Equal (v1, v2) when AbstractValue.equal v1 v ->
+        Some v2
+    | _ ->
+        None )
+  |> Option.value ~default:v
+
+
 module Topl = struct
   let small_step loc event astate =
     {astate with topl= PulseTopl.small_step loc astate.path_condition event astate.topl}
diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli
index 973b19041..12ba0e8d5 100644
--- a/infer/src/pulse/PulseAbductiveDomain.mli
+++ b/infer/src/pulse/PulseAbductiveDomain.mli
@@ -216,6 +216,9 @@ val incorporate_new_eqs :
     and [y] being allocated separately. In those cases, the resulting path condition is
     {!PathCondition.false_}. *)
 
+val incorporate_new_eqs_on_val : PathCondition.new_eqs -> AbstractValue.t -> AbstractValue.t
+(** Similar to [incorporate_new_eqs], but apply to an abstract value. *)
+
 val initialize : AbstractValue.t -> t -> t
 (** Remove "Uninitialized" attribute of the given address *)
 
diff --git a/infer/src/pulse/PulseArithmetic.ml b/infer/src/pulse/PulseArithmetic.ml
index 154c1c9b0..1b3823ece 100644
--- a/infer/src/pulse/PulseArithmetic.ml
+++ b/infer/src/pulse/PulseArithmetic.ml
@@ -10,11 +10,21 @@ open PulseBasicInterface
 module AbductiveDomain = PulseAbductiveDomain
 module AccessResult = PulseAccessResult
 
-let map_path_condition ~f astate =
+let map_path_condition_common ~f astate =
   let phi, new_eqs = f astate.AbductiveDomain.path_condition in
-  AbductiveDomain.set_path_condition phi astate
-  |> AbductiveDomain.incorporate_new_eqs new_eqs
-  |> AccessResult.of_abductive_result
+  let astate = AbductiveDomain.set_path_condition phi astate in
+  let result =
+    AbductiveDomain.incorporate_new_eqs new_eqs astate |> AccessResult.of_abductive_result
+  in
+  (result, new_eqs)
+
+
+let map_path_condition ~f astate = map_path_condition_common ~f astate |> fst
+
+let map_path_condition_with_ret ~f astate ret =
+  let result, new_eqs = map_path_condition_common ~f astate in
+  Result.map result ~f:(fun result ->
+      (result, AbductiveDomain.incorporate_new_eqs_on_val new_eqs ret) )
 
 
 let and_nonnegative v astate =
@@ -39,17 +49,17 @@ let and_equal op1 op2 astate =
 
 
 let eval_binop binop_addr binop op_lhs op_rhs astate =
-  map_path_condition astate ~f:(fun phi ->
+  map_path_condition_with_ret astate binop_addr ~f:(fun phi ->
       PathCondition.eval_binop binop_addr binop op_lhs op_rhs phi )
 
 
 let eval_unop unop_addr unop addr astate =
-  map_path_condition astate ~f:(fun phi -> PathCondition.eval_unop unop_addr unop addr phi)
+  map_path_condition_with_ret astate unop_addr ~f:(fun phi ->
+      PathCondition.eval_unop unop_addr unop addr phi )
 
 
 let prune_binop ~negated bop lhs_op rhs_op astate =
-  map_path_condition astate ~f:(fun phi ->
-      PathCondition.prune_binop ~negated bop lhs_op rhs_op phi )
+  map_path_condition astate ~f:(fun phi -> PathCondition.prune_binop ~negated bop lhs_op rhs_op phi)
 
 
 let prune_eq_zero v astate =
diff --git a/infer/src/pulse/PulseArithmetic.mli b/infer/src/pulse/PulseArithmetic.mli
index 5f489c3fc..8a2d94eaf 100644
--- a/infer/src/pulse/PulseArithmetic.mli
+++ b/infer/src/pulse/PulseArithmetic.mli
@@ -32,14 +32,14 @@ val eval_binop :
   -> operand
   -> operand
   -> AbductiveDomain.t
-  -> AbductiveDomain.t AccessResult.t
+  -> (AbductiveDomain.t * AbstractValue.t) AccessResult.t
 
 val eval_unop :
      AbstractValue.t
   -> Unop.t
   -> AbstractValue.t
   -> AbductiveDomain.t
-  -> AbductiveDomain.t AccessResult.t
+  -> (AbductiveDomain.t * AbstractValue.t) AccessResult.t
 
 val prune_binop :
      negated:bool
diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml
index cc15e3f40..a6e27059f 100644
--- a/infer/src/pulse/PulseModels.ml
+++ b/infer/src/pulse/PulseModels.ml
@@ -480,7 +480,7 @@ module StdAtomicInteger = struct
   let arith_bop path prepost location event ret_id bop this operand astate =
     let* astate, int_addr, (old_int, hist) = load_backing_int path location this astate in
     let bop_addr = AbstractValue.mk_fresh () in
-    let* astate =
+    let* astate, bop_addr =
       PulseArithmetic.eval_binop bop_addr bop (AbstractValueOperand old_int) operand astate
     in
     let+ astate =
@@ -1438,7 +1438,7 @@ module JavaInteger = struct
     let<*> astate, _int_addr1, (int1, hist) = load_backing_int path location this astate in
     let<*> astate, _int_addr2, (int2, _) = load_backing_int path location arg astate in
     let binop_addr = AbstractValue.mk_fresh () in
-    let<+> astate =
+    let<+> astate, binop_addr =
       PulseArithmetic.eval_binop binop_addr Binop.Eq (AbstractValueOperand int1)
         (AbstractValueOperand int2) astate
     in
diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml
index 7aed9e313..167150a41 100644
--- a/infer/src/pulse/PulseOperations.ml
+++ b/infer/src/pulse/PulseOperations.ml
@@ -255,25 +255,18 @@ let eval path mode location exp0 astate =
     | UnOp (unop, exp, _typ) ->
         let* astate, (addr, hist) = eval path Read exp astate in
         let unop_addr = AbstractValue.mk_fresh () in
-        let+ astate = PulseArithmetic.eval_unop unop_addr unop addr astate in
+        let+ astate, unop_addr = PulseArithmetic.eval_unop unop_addr unop addr astate in
         (astate, (unop_addr, hist))
-    | BinOp (bop, e_lhs, e_rhs) -> (
+    | BinOp (bop, e_lhs, e_rhs) ->
         let* astate, (addr_lhs, hist_lhs) = eval path Read e_lhs astate in
-        let* astate, (addr_rhs, hist_rhs) = eval path Read e_rhs astate in
-        match bop with
-        | (PlusA _ | PlusPI | MinusA _ | MinusPI) when PulseArithmetic.is_known_zero astate addr_rhs
-          ->
-            Ok (astate, (addr_lhs, hist_lhs))
-        | PlusA _ when PulseArithmetic.is_known_zero astate addr_lhs ->
-            Ok (astate, (addr_rhs, hist_rhs))
-        | _ ->
-            let binop_addr = AbstractValue.mk_fresh () in
-            let+ astate =
-              PulseArithmetic.eval_binop binop_addr bop (AbstractValueOperand addr_lhs)
-                (AbstractValueOperand addr_rhs) astate
-            in
-            (* NOTE: keeping track of only [hist_lhs] into the binop is not the best *)
-            (astate, (binop_addr, hist_lhs)) )
+        (* NOTE: keeping track of only [hist_lhs] into the binop is not the best *)
+        let* astate, (addr_rhs, _hist_rhs) = eval path Read e_rhs astate in
+        let binop_addr = AbstractValue.mk_fresh () in
+        let+ astate, binop_addr =
+          PulseArithmetic.eval_binop binop_addr bop (AbstractValueOperand addr_lhs)
+            (AbstractValueOperand addr_rhs) astate
+        in
+        (astate, (binop_addr, hist_lhs))
     | Const _ | Sizeof _ | Exn _ ->
         Ok (astate, (AbstractValue.mk_fresh (), (* TODO history *) []))
   in