diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml
index b7e60cadc..04ba0f721 100644
--- a/infer/src/backend/prop.ml
+++ b/infer/src/backend/prop.ml
@@ -685,7 +685,7 @@ module Normalize = struct
 
   let ( ++ ) = IntLit.add
 
-  let sym_eval tenv abs e =
+  let sym_eval ?(destructive= false) tenv abs e =
     let lookup = Tenv.lookup tenv in
     let rec eval (e: Exp.t) : Exp.t =
       (* L.d_str " ["; Sil.d_exp e; L.d_str"] "; *)
@@ -699,6 +699,8 @@ module Normalize = struct
           Closure {c with captured_vars}
       | Const _
        -> e
+      | Sizeof {nbytes= Some n} when destructive
+       -> Exp.Const (Const.Cint (IntLit.of_int n))
       | Sizeof {typ= {desc= Tarray ({desc= Tint ik}, _, _)}; dynamic_length= Some l}
         when Typ.ikind_is_char ik && Config.curr_language_is Config.Clang
        -> eval l
@@ -1084,9 +1086,10 @@ module Normalize = struct
     (* L.d_str "sym_eval "; Sil.d_exp e; L.d_str" --> "; Sil.d_exp e'; L.d_ln (); *)
     e'
 
-  let exp_normalize tenv sub exp =
+  let exp_normalize ?destructive tenv sub exp =
     let exp' = Sil.exp_sub sub exp in
-    if !Config.abs_val >= 1 then sym_eval tenv true exp' else sym_eval tenv false exp'
+    let abstract_expressions = !Config.abs_val >= 1 in
+    sym_eval ?destructive tenv abstract_expressions exp'
 
   let texp_normalize tenv sub (exp: Exp.t) : Exp.t =
     match exp with
@@ -1675,8 +1678,10 @@ end
 
 (* End of module Normalize *)
 
-let exp_normalize_prop tenv prop exp =
-  Config.run_with_abs_val_equal_zero (Normalize.exp_normalize tenv (`Exp prop.sub)) exp
+let exp_normalize_prop ?destructive tenv prop exp =
+  Config.run_with_abs_val_equal_zero
+    (Normalize.exp_normalize ?destructive tenv (`Exp prop.sub))
+    exp
 
 let lexp_normalize_prop tenv p lexp =
   let root = Exp.root_of_lexp lexp in
diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli
index f6c238612..ce8a73ad5 100644
--- a/infer/src/backend/prop.mli
+++ b/infer/src/backend/prop.mli
@@ -158,10 +158,12 @@ val atom_exp_le_const : Sil.atom -> (Exp.t * IntLit.t) option
 val atom_const_lt_exp : Sil.atom -> (IntLit.t * Exp.t) option
 (** If the atom is [n<e] return [n,e] *)
 
-val exp_normalize_prop : Tenv.t -> 'a t -> Exp.t -> Exp.t
-(** Normalize [exp] using the pure part of [prop].  Later, we should
-    change this such that the normalization exposes offsets of [exp]
-    as much as possible. *)
+val exp_normalize_prop : ?destructive:bool -> Tenv.t -> 'a t -> Exp.t -> Exp.t
+(** Normalize [exp] using the pure part of [prop].  Later, we should change this such that the
+    normalization exposes offsets of [exp] as much as possible.
+
+    If [destructive] is true then normalize more aggressively, which may lose some useful structure
+    or types. *)
 
 val exp_normalize_noabs : Tenv.t -> Sil.subst -> Exp.t -> Exp.t
 (** Normalize the expression without abstracting complex subexpressions *)
diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml
index aed018db9..273bd6044 100644
--- a/infer/src/backend/prover.ml
+++ b/infer/src/backend/prover.ml
@@ -473,11 +473,11 @@ end = struct
     match (e1, e2) with
     | Exp.Const Const.Cint n1, Exp.Const Const.Cint n2
      -> IntLit.leq n1 n2
-    | ( Exp.BinOp
-          ( Binop.MinusA
-          , Exp.Sizeof {typ= t1; dynamic_length= None}
-          , Exp.Sizeof {typ= t2; dynamic_length= None} )
+    | ( Exp.BinOp (Binop.MinusA, Exp.Sizeof {nbytes= Some nb1}, Exp.Sizeof {nbytes= Some nb2})
       , Exp.Const Const.Cint n2 )
+     -> (* [ sizeof(t1) - sizeof(t2) <= n2 ] *)
+        IntLit.(leq (sub (of_int nb1) (of_int nb2)) n2)
+    | Exp.BinOp (Binop.MinusA, Exp.Sizeof {typ= t1}, Exp.Sizeof {typ= t2}), Exp.Const Const.Cint n2
       when IntLit.isminusone n2 && type_size_comparable t1 t2
      -> (* [ sizeof(t1) - sizeof(t2) <= -1 ] *)
         check_type_size_lt t1 t2
@@ -550,6 +550,8 @@ end = struct
     match e1 with
     | Exp.Const Const.Cint n1
      -> Some (n1 -- IntLit.one)
+    | Exp.Sizeof {nbytes= Some n1}
+     -> Some (IntLit.of_int n1 -- IntLit.one)
     | Exp.Sizeof _
      -> Some IntLit.zero
     | _
@@ -597,9 +599,9 @@ end
 (* End of module Inequalities *)
 
 (** Check [prop |- e1=e2]. Result [false] means "don't know". *)
-let check_equal tenv prop e1 e2 =
-  let n_e1 = Prop.exp_normalize_prop tenv prop e1 in
-  let n_e2 = Prop.exp_normalize_prop tenv prop e2 in
+let check_equal tenv prop e1_0 e2_0 =
+  let n_e1 = Prop.exp_normalize_prop ~destructive:true tenv prop e1_0 in
+  let n_e2 = Prop.exp_normalize_prop ~destructive:true tenv prop e2_0 in
   let check_equal () = Exp.equal n_e1 n_e2 in
   let check_equal_const () =
     match (n_e1, n_e2) with
@@ -651,8 +653,8 @@ let is_root tenv prop base_exp exp =
   f [] exp
 
 (** Get upper and lower bounds of an expression, if any *)
-let get_bounds tenv prop _e =
-  let e_norm = Prop.exp_normalize_prop tenv prop _e in
+let get_bounds tenv prop e0 =
+  let e_norm = Prop.exp_normalize_prop ~destructive:true tenv prop e0 in
   let e_root, off =
     match e_norm with
     | Exp.BinOp (Binop.PlusA, e, Exp.Const Const.Cint n1)
@@ -671,8 +673,8 @@ let get_bounds tenv prop _e =
 (** Check whether [prop |- e1!=e2]. *)
 let check_disequal tenv prop e1 e2 =
   let spatial_part = prop.Prop.sigma in
-  let n_e1 = Prop.exp_normalize_prop tenv prop e1 in
-  let n_e2 = Prop.exp_normalize_prop tenv prop e2 in
+  let n_e1 = Prop.exp_normalize_prop ~destructive:true tenv prop e1 in
+  let n_e2 = Prop.exp_normalize_prop ~destructive:true tenv prop e2 in
   let rec check_expr_disequal ce1 ce2 =
     match (ce1, ce2) with
     | Exp.Const c1, Exp.Const c2
@@ -874,7 +876,7 @@ let check_le tenv prop e1 e2 =
 
 (** Check whether [prop |- allocated(e)]. *)
 let check_allocatedness tenv prop e =
-  let n_e = Prop.exp_normalize_prop tenv prop e in
+  let n_e = Prop.exp_normalize_prop ~destructive:true tenv prop e in
   let spatial_part = prop.Prop.sigma in
   let f = function
     | Sil.Hpointsto (base, _, _)
@@ -915,7 +917,7 @@ let check_inconsistency_two_hpreds tenv prop =
           let prop' = Prop.normalize tenv (Prop.from_sigma (sigma_seen @ sigma_rest)) in
           let prop_new = Prop.conjoin_eq tenv e1 e2 prop' in
           let sigma_new = prop_new.Prop.sigma in
-          let e_new = Prop.exp_normalize_prop tenv prop_new e in
+          let e_new = Prop.exp_normalize_prop ~destructive:true tenv prop_new e in
           f e_new [] sigma_new
         else f e (hpred :: sigma_seen) sigma_rest
     | (Sil.Hdllseg (Sil.Lseg_PE, _, e1, _, Exp.Const Const.Cint i, _, _) as hpred) :: sigma_rest
@@ -926,7 +928,7 @@ let check_inconsistency_two_hpreds tenv prop =
           let prop' = Prop.normalize tenv (Prop.from_sigma (sigma_seen @ sigma_rest)) in
           let prop_new = Prop.conjoin_eq tenv e1 e3 prop' in
           let sigma_new = prop_new.Prop.sigma in
-          let e_new = Prop.exp_normalize_prop tenv prop_new e in
+          let e_new = Prop.exp_normalize_prop ~destructive:true tenv prop_new e in
           f e_new [] sigma_new
         else f e (hpred :: sigma_seen) sigma_rest
   in
@@ -1319,7 +1321,9 @@ let exp_imply tenv calc_missing (subs: subst2) e1_in e2_in : subst2 =
      -> let occurs_check v e =
           (* check whether [v] occurs in normalized [e] *)
           if Sil.fav_mem (Sil.exp_fav e) v
-             && Sil.fav_mem (Sil.exp_fav (Prop.exp_normalize_prop tenv Prop.prop_emp e)) v
+             && Sil.fav_mem
+                  (Sil.exp_fav (Prop.exp_normalize_prop ~destructive:true tenv Prop.prop_emp e))
+                  v
           then raise (IMPL_EXC ("occurs check", subs, EXC_FALSE_EXPS (e1, e2)))
         in
         if Ident.is_primed v2 then
diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml
index 45811a14c..2ee20ee4c 100644
--- a/infer/src/backend/symExec.ml
+++ b/infer/src/backend/symExec.ml
@@ -331,7 +331,7 @@ let prune_ineq tenv ~is_strict ~positive prop e1 e2 =
       Propset.singleton tenv prop_with_ineq
 
 let rec prune tenv ~positive condition prop =
-  match condition with
+  match Prop.exp_normalize_prop ~destructive:true tenv prop condition with
   | Exp.Var _ | Exp.Lvar _
    -> prune_ne tenv ~positive condition Exp.zero prop
   | Exp.Const Const.Cint i when IntLit.iszero i
diff --git a/infer/tests/codetoanalyze/c/errors/issues.exp b/infer/tests/codetoanalyze/c/errors/issues.exp
index 706ed445d..a0c7b3c49 100644
--- a/infer/tests/codetoanalyze/c/errors/issues.exp
+++ b/infer/tests/codetoanalyze/c/errors/issues.exp
@@ -91,6 +91,7 @@ codetoanalyze/c/errors/null_dereference/short.c, l_error, 2, NULL_DEREFERENCE
 codetoanalyze/c/errors/null_dereference/short.c, m, 2, NULL_TEST_AFTER_DEREFERENCE
 codetoanalyze/c/errors/resource_leaks/leak.c, fileNotClosed, 5, RESOURCE_LEAK
 codetoanalyze/c/errors/resource_leaks/leak.c, socketNotClosed, 5, RESOURCE_LEAK
+codetoanalyze/c/errors/sizeof/sizeof_706.c, sentinel_bad, 0, DIVIDE_BY_ZERO
 codetoanalyze/c/frontend/enumeration/other_enum.c, other_enum_test, 4, DIVIDE_BY_ZERO
 codetoanalyze/c/frontend/offsetof_expr/offsetof_expr.c, test_offsetof_expr, 3, DIVIDE_BY_ZERO
 codetoanalyze/c/frontend/offsetof_expr/offsetof_expr.c, test_offsetof_expr, 5, DIVIDE_BY_ZERO
diff --git a/infer/tests/codetoanalyze/c/errors/sizeof/sizeof_706.c b/infer/tests/codetoanalyze/c/errors/sizeof/sizeof_706.c
new file mode 100644
index 000000000..40d15debc
--- /dev/null
+++ b/infer/tests/codetoanalyze/c/errors/sizeof/sizeof_706.c
@@ -0,0 +1,29 @@
+/*
+ * Copyright (c) 2017 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+int sizeof_eval_good(void) {
+  int a = 4;
+  int b = sizeof(a);
+  char c[2];
+
+  if (a % 4) {
+    return a / 0;
+  }
+  if (b % sizeof(a)) {
+    return a / 0;
+  }
+  if (sizeof(c) > 2) {
+    return a / 0;
+  }
+  if ((sizeof(c) / sizeof(c[0])) != 2) {
+    return a / 0;
+  }
+  return 0;
+}
+
+void sentinel_bad(void) { return 1 / 0; }