diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml
index dc207ecee..578361bad 100644
--- a/infer/src/pulse/Pulse.ml
+++ b/infer/src/pulse/Pulse.ml
@@ -22,7 +22,8 @@ let check_error_transform analysis_data ~f = function
   | Ok astate ->
       f astate
   | Error (diagnostic, astate) ->
-      if PulseArithmetic.is_unsat_expensive astate then []
+      let astate, is_unsat = PulseArithmetic.is_unsat_expensive astate in
+      if is_unsat then []
       else (
         report analysis_data diagnostic ;
         [ExecutionDomain.AbortProgram astate] )
diff --git a/infer/src/pulse/PulseArithmetic.ml b/infer/src/pulse/PulseArithmetic.ml
index 136611d2d..2f6dc24a3 100644
--- a/infer/src/pulse/PulseArithmetic.ml
+++ b/infer/src/pulse/PulseArithmetic.ml
@@ -50,4 +50,5 @@ let is_known_zero astate v = PathCondition.is_known_zero astate.AbductiveDomain.
 let is_unsat_cheap astate = PathCondition.is_unsat_cheap astate.AbductiveDomain.path_condition
 
 let is_unsat_expensive astate =
-  PathCondition.is_unsat_expensive astate.AbductiveDomain.path_condition
+  let phi', is_unsat = PathCondition.is_unsat_expensive astate.AbductiveDomain.path_condition in
+  (AbductiveDomain.set_path_condition phi' astate, is_unsat)
diff --git a/infer/src/pulse/PulseArithmetic.mli b/infer/src/pulse/PulseArithmetic.mli
index 138822587..0d5e440ac 100644
--- a/infer/src/pulse/PulseArithmetic.mli
+++ b/infer/src/pulse/PulseArithmetic.mli
@@ -34,4 +34,4 @@ val is_known_zero : AbductiveDomain.t -> AbstractValue.t -> bool
 
 val is_unsat_cheap : AbductiveDomain.t -> bool
 
-val is_unsat_expensive : AbductiveDomain.t -> bool
+val is_unsat_expensive : AbductiveDomain.t -> AbductiveDomain.t * bool
diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml
index 459e44efd..2b8428d7d 100644
--- a/infer/src/pulse/PulseExecutionDomain.ml
+++ b/infer/src/pulse/PulseExecutionDomain.ml
@@ -52,5 +52,10 @@ let of_posts pdesc posts =
   List.filter_mapi posts ~f:(fun i exec_state ->
       let (AbortProgram astate | ContinueProgram astate | ExitProgram astate) = exec_state in
       L.d_printfln "Creating spec out of state #%d:@\n%a" i pp exec_state ;
-      if PulseArithmetic.is_unsat_expensive astate then None
-      else Some (map exec_state ~f:(AbductiveDomain.of_post pdesc)) )
+      let astate, is_unsat = PulseArithmetic.is_unsat_expensive astate in
+      if is_unsat then None
+      else
+        Some
+          (map exec_state ~f:(fun _astate ->
+               (* prefer [astate] since it is an equivalent state that has been normalized *)
+               AbductiveDomain.of_post pdesc astate )) )
diff --git a/infer/src/pulse/PulsePathCondition.ml b/infer/src/pulse/PulsePathCondition.ml
index 40b0262d4..608e8a886 100644
--- a/infer/src/pulse/PulsePathCondition.ml
+++ b/infer/src/pulse/PulsePathCondition.ml
@@ -29,59 +29,60 @@ module CItvs = PrettyPrintable.MakePPMonoMap (AbstractValue) (CItv)
 (** A mash-up of several arithmetic domains. At the moment they are independent, i.e. we don't use
     facts deduced by one domain to inform another. *)
 type t =
-  { satisfiable: bool
-        (** If [true] then [formula] could still be unsatisfiable (asking that question is
+  { is_unsat: bool
+        (** If [false] then [formula] could still be unsatisfiable (asking that question is
             expensive).
 
-            If [false] then the other components of the record can be arbitrary. *)
+            If [true] then the other components of the record can be arbitrary. *)
   ; bo_itvs: BoItvs.t
   ; citvs: CItvs.t
   ; formula: Formula.t }
 
-let pp fmt {satisfiable; bo_itvs; citvs; formula} =
-  F.fprintf fmt "@[<hv>sat:%b,@;bo: @[%a@],@;citv: @[%a@],@;formula: @[%a@]@]" satisfiable BoItvs.pp
+let pp fmt {is_unsat; bo_itvs; citvs; formula} =
+  F.fprintf fmt "@[<hv>unsat:%b,@;bo: @[%a@],@;citv: @[%a@],@;formula: @[%a@]@]" is_unsat BoItvs.pp
     bo_itvs CItvs.pp citvs Formula.pp formula
 
 
-let true_ = {satisfiable= true; bo_itvs= BoItvs.empty; citvs= CItvs.empty; formula= Formula.ttrue}
+let true_ = {is_unsat= false; bo_itvs= BoItvs.empty; citvs= CItvs.empty; formula= Formula.ttrue}
 
-let false_ = {satisfiable= false; bo_itvs= BoItvs.empty; citvs= CItvs.empty; formula= Formula.ttrue}
+let false_ = {is_unsat= true; bo_itvs= BoItvs.empty; citvs= CItvs.empty; formula= Formula.ttrue}
 
-let and_nonnegative v ({satisfiable; bo_itvs; citvs; formula} as phi) =
-  if not satisfiable then phi
+let and_nonnegative v ({is_unsat; bo_itvs; citvs; formula} as phi) =
+  if is_unsat then phi
   else
-    { satisfiable
+    { is_unsat
     ; bo_itvs= BoItvs.add v Itv.ItvPure.nat bo_itvs
     ; citvs= CItvs.add v CItv.zero_inf citvs
     ; formula= Formula.(aand (mk_less_equal Term.zero (Term.of_absval v)) formula) }
 
 
-let and_positive v ({satisfiable; bo_itvs; citvs; formula} as phi) =
-  if not satisfiable then phi
+let and_positive v ({is_unsat; bo_itvs; citvs; formula} as phi) =
+  if is_unsat then phi
   else
-    { satisfiable
+    { is_unsat
     ; bo_itvs= BoItvs.add v Itv.ItvPure.pos bo_itvs
     ; citvs= CItvs.add v (CItv.ge_to IntLit.one) citvs
     ; formula= Formula.(aand (mk_less_than Term.zero (Term.of_absval v)) formula) }
 
 
-let and_eq_int v i ({satisfiable; bo_itvs; citvs; formula} as phi) =
-  if not satisfiable then phi
+let and_eq_int v i ({is_unsat; bo_itvs; citvs; formula} as phi) =
+  if is_unsat then phi
   else
-    { satisfiable
+    { is_unsat
     ; bo_itvs= BoItvs.add v (Itv.ItvPure.of_int_lit i) bo_itvs
     ; citvs= CItvs.add v (CItv.equal_to i) citvs
     ; formula= Formula.(aand (mk_equal (Term.of_absval v) (Term.of_intlit i)) formula) }
 
 
-let simplify ~keep {satisfiable; bo_itvs; citvs; formula} =
-  if not satisfiable then false_
+let simplify ~keep {is_unsat; bo_itvs; citvs; formula} =
+  if is_unsat then false_
   else
     let is_in_keep v _ = AbstractValue.Set.mem v keep in
-    { satisfiable
+    let formula = Formula.simplify ~keep formula in
+    { is_unsat= is_unsat || Formula.is_literal_false formula
     ; bo_itvs= BoItvs.filter is_in_keep bo_itvs
     ; citvs= CItvs.filter is_in_keep citvs
-    ; formula= Formula.simplify ~keep formula }
+    ; formula }
 
 
 let subst_find_or_new subst addr_callee =
@@ -186,7 +187,7 @@ let and_formula_callee subst formula_caller formula_callee =
 
 
 let and_callee subst phi ~callee:phi_callee =
-  if (not phi.satisfiable) || not phi_callee.satisfiable then (subst, false_)
+  if phi.is_unsat || phi_callee.is_unsat then (subst, false_)
   else
     match and_bo_itvs_callee subst phi.bo_itvs phi_callee.bo_itvs with
     | exception Contradiction ->
@@ -201,9 +202,9 @@ let and_callee subst phi ~callee:phi_callee =
           let subst, formula' = and_formula_callee subst phi.formula phi_callee.formula in
           L.d_printfln "conjoined formula post call: %a@\n" Formula.pp formula' ;
           let formula' = Formula.normalize formula' in
-          let satisfiable = not (Formula.is_literal_false formula') in
-          if not satisfiable then L.d_printfln "contradiction found by formulas" ;
-          (subst, {satisfiable; bo_itvs= bo_itvs'; citvs= citvs'; formula= formula'}) )
+          let is_unsat = Formula.is_literal_false formula' in
+          if is_unsat then L.d_printfln "contradiction found by formulas" ;
+          (subst, {is_unsat; bo_itvs= bo_itvs'; citvs= citvs'; formula= formula'}) )
 
 
 (** {2 Operations} *)
@@ -254,10 +255,10 @@ let eval_formula_binop binop_addr binop op_lhs op_rhs formula =
   aand (mk_equal (Term.of_absval binop_addr) t_binop) formula
 
 
-let eval_binop binop_addr binop op_lhs op_rhs ({satisfiable; bo_itvs; citvs; formula} as phi) =
-  if not phi.satisfiable then phi
+let eval_binop binop_addr binop op_lhs op_rhs ({is_unsat; bo_itvs; citvs; formula} as phi) =
+  if phi.is_unsat then phi
   else
-    { satisfiable
+    { is_unsat
     ; bo_itvs= eval_bo_itv_binop binop_addr binop op_lhs op_rhs bo_itvs
     ; citvs= eval_citv_binop binop_addr binop op_lhs op_rhs citvs
     ; formula= eval_formula_binop binop_addr binop op_lhs op_rhs formula }
@@ -286,10 +287,10 @@ let eval_formula_unop unop_addr (unop : Unop.t) addr formula =
   aand (mk_equal (Term.of_absval unop_addr) t_unop) formula
 
 
-let eval_unop unop_addr unop addr ({satisfiable; bo_itvs; citvs; formula} as phi) =
-  if not phi.satisfiable then phi
+let eval_unop unop_addr unop addr ({is_unsat; bo_itvs; citvs; formula} as phi) =
+  if phi.is_unsat then phi
   else
-    { satisfiable
+    { is_unsat
     ; bo_itvs= eval_bo_itv_unop unop_addr unop addr bo_itvs
     ; citvs= eval_citv_unop unop_addr unop addr citvs
     ; formula= eval_formula_unop unop_addr unop addr formula }
@@ -304,7 +305,7 @@ let prune_bo_with_bop ~negated v_opt arith bop arith' phi =
   | None ->
       phi
   | Some (_, Bottom) ->
-      {phi with satisfiable= false}
+      {phi with is_unsat= true}
   | Some (v, NonBottom arith_pruned) ->
       {phi with bo_itvs= BoItvs.add v arith_pruned phi.bo_itvs}
 
@@ -327,10 +328,10 @@ let record_citv_abduced addr_opt arith_opt citvs =
       CItvs.add addr arith citvs
 
 
-let bind_satisfiable phi ~f = if phi.satisfiable then f phi else phi
+let bind_is_unsat phi ~f = if phi.is_unsat then phi else f phi
 
-let prune_binop ~negated bop lhs_op rhs_op ({satisfiable; bo_itvs= _; citvs; formula} as phi) =
-  if not satisfiable then phi
+let prune_binop ~negated bop lhs_op rhs_op ({is_unsat; bo_itvs= _; citvs; formula} as phi) =
+  if is_unsat then phi
   else
     let value_lhs_opt, arith_lhs_opt, bo_itv_lhs, t_lhs = eval_operand phi lhs_op in
     let value_rhs_opt, arith_rhs_opt, bo_itv_rhs, t_rhs = eval_operand phi rhs_op in
@@ -346,38 +347,38 @@ let prune_binop ~negated bop lhs_op rhs_op ({satisfiable; bo_itvs= _; citvs; for
           in
           {phi with citvs}
         in
-        let satisfiable =
+        let is_unsat =
           match Itv.ItvPure.arith_binop bop bo_itv_lhs bo_itv_rhs |> Itv.ItvPure.to_boolean with
           | False ->
-              negated
-          | True ->
               not negated
+          | True ->
+              negated
           | Top ->
-              true
-          | Bottom ->
               false
+          | Bottom ->
+              true
         in
-        if not satisfiable then L.d_printfln "contradiction detected by inferbo intervals" ;
-        let phi = {phi with satisfiable} in
+        if is_unsat then L.d_printfln "contradiction detected by inferbo intervals" ;
+        let phi = {phi with is_unsat} in
         let phi =
-          bind_satisfiable phi ~f:(fun phi ->
+          bind_is_unsat phi ~f:(fun phi ->
               prune_bo_with_bop ~negated value_lhs_opt bo_itv_lhs bop bo_itv_rhs phi )
         in
         let phi =
           Option.value_map (Binop.symmetric bop) ~default:phi ~f:(fun bop' ->
-              bind_satisfiable phi ~f:(fun phi ->
+              bind_is_unsat phi ~f:(fun phi ->
                   prune_bo_with_bop ~negated value_rhs_opt bo_itv_rhs bop' bo_itv_lhs phi ) )
         in
-        if not phi.satisfiable then phi
+        if phi.is_unsat then phi
         else
           let f_positive = Formula.of_term_binop bop t_lhs t_rhs in
           let formula =
             let f = if negated then Formula.nnot f_positive else f_positive in
             Formula.aand f formula |> Formula.normalize
           in
-          let satisfiable = not (Formula.is_literal_false formula) in
-          if not satisfiable then L.d_printfln "contradiction detected by formulas" ;
-          {phi with satisfiable; formula}
+          let is_unsat = Formula.is_literal_false formula in
+          if is_unsat then L.d_printfln "contradiction detected by formulas" ;
+          {phi with is_unsat; formula}
 
 
 (** {2 Queries} *)
@@ -388,9 +389,14 @@ let is_known_zero phi v =
   || BoItvs.find_opt v phi.bo_itvs |> Option.value_map ~default:false ~f:Itv.ItvPure.is_zero
 
 
-let is_unsat_cheap phi = (not phi.satisfiable) || Formula.is_literal_false phi.formula
+let is_unsat_cheap phi = phi.is_unsat || Formula.is_literal_false phi.formula
 
 let is_unsat_expensive phi =
   (* note: contradictions are detected eagerly for all sub-domains except formula, so just
      evaluate that one *)
-  is_unsat_cheap phi || Formula.normalize phi.formula |> Formula.is_literal_false
+  if is_unsat_cheap phi then (phi, true)
+  else
+    let formula = Formula.normalize phi.formula in
+    let is_unsat = Formula.is_literal_false formula in
+    let phi = {phi with is_unsat; formula} in
+    (phi, is_unsat)
diff --git a/infer/src/pulse/PulsePathCondition.mli b/infer/src/pulse/PulsePathCondition.mli
index 55556e818..5c135928f 100644
--- a/infer/src/pulse/PulsePathCondition.mli
+++ b/infer/src/pulse/PulsePathCondition.mli
@@ -55,5 +55,5 @@ val is_known_zero : t -> AbstractValue.t -> bool
 val is_unsat_cheap : t -> bool
 (** whether the state contains a contradiction, call this as often as you want *)
 
-val is_unsat_expensive : t -> bool
+val is_unsat_expensive : t -> t * bool
 (** whether the state contains a contradiction, only call this when you absolutely have to *)