diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index e765e9071..91f72bbef 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml
@@ -113,7 +113,7 @@ module Val = struct
 
   let neg : t -> t = fun x -> {x with itv= Itv.neg x.itv}
 
-  let lnot : t -> t = fun x -> {x with itv= Itv.lnot x.itv}
+  let lnot : t -> t = fun x -> {x with itv= Itv.lnot x.itv |> Itv.of_bool}
 
   let lift_itv : (Itv.t -> Itv.t -> Itv.t) -> t -> t -> t =
    fun f x y -> {bot with itv= f x.itv y.itv; traces= TraceSet.join x.traces y.traces}
@@ -121,11 +121,11 @@ module Val = struct
 
   let has_pointer : t -> bool = fun x -> not (PowLoc.is_bot x.powloc && ArrayBlk.is_bot x.arrayblk)
 
-  let lift_cmp_itv : (Itv.t -> Itv.t -> Itv.t) -> t -> t -> t =
+  let lift_cmp_itv : (Itv.t -> Itv.t -> Itv.Boolean.t) -> t -> t -> t =
    fun f x y ->
-    if has_pointer x || has_pointer y then
-      {bot with itv= Itv.unknown_bool; traces= TraceSet.join x.traces y.traces}
-    else lift_itv f x y
+    let b = if has_pointer x || has_pointer y then Itv.Boolean.top else f x.itv y.itv in
+    let itv = Itv.of_bool b in
+    {bot with itv; traces= TraceSet.join x.traces y.traces}
 
 
   let plus_a : t -> t -> t = lift_itv Itv.plus
@@ -154,9 +154,9 @@ module Val = struct
 
   let ne_sem : t -> t -> t = lift_cmp_itv Itv.ne_sem
 
-  let land_sem : t -> t -> t = lift_itv Itv.land_sem
+  let land_sem : t -> t -> t = lift_cmp_itv Itv.land_sem
 
-  let lor_sem : t -> t -> t = lift_itv Itv.lor_sem
+  let lor_sem : t -> t -> t = lift_cmp_itv Itv.lor_sem
 
   let lift_prune1 : (Itv.t -> Itv.t) -> t -> t = fun f x -> {x with itv= f x.itv}
 
diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
index 8f517410e..e196190bc 100644
--- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
+++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
@@ -43,14 +43,14 @@ module AllocSizeCondition = struct
     | (`LeftSmallerThanRight | `RightSmallerThanLeft) as cmp ->
         let lpos = ItvPure.le_sem ItvPure.zero lhs in
         let rpos = ItvPure.le_sem ItvPure.zero rhs in
-        if not (ItvPure.equal lpos rpos) then `NotComparable
-        else if ItvPure.is_true lpos then
+        if not (Itv.Boolean.equal lpos rpos) then `NotComparable
+        else if Itv.Boolean.is_true lpos then
           match cmp with
           | `LeftSmallerThanRight ->
               `RightSubsumesLeft
           | `RightSmallerThanLeft ->
               `LeftSubsumesRight
-        else if ItvPure.is_false lpos then
+        else if Itv.Boolean.is_false lpos then
           match cmp with
           | `LeftSmallerThanRight ->
               `LeftSubsumesRight
@@ -147,8 +147,8 @@ module ArrayAccessCondition = struct
     | (`LeftSmallerThanRight | `RightSmallerThanLeft), _ ->
         let lidxpos = ItvPure.le_sem ItvPure.zero lidx in
         let ridxpos = ItvPure.le_sem ItvPure.zero ridx in
-        if not (ItvPure.equal lidxpos ridxpos) then `NotComparable
-        else if ItvPure.is_true lidxpos then
+        if not (Itv.Boolean.equal lidxpos ridxpos) then `NotComparable
+        else if Itv.Boolean.is_true lidxpos then
           (* both idx >= 0 *)
           match (idxcmp, sizcmp) with
           | `LeftSmallerThanRight, (`Equal | `RightSmallerThanLeft | `RightSubsumesLeft) ->
@@ -157,7 +157,7 @@ module ArrayAccessCondition = struct
               `LeftSubsumesRight
           | _ ->
               `NotComparable
-        else if ItvPure.is_false lidxpos then
+        else if Itv.Boolean.is_false lidxpos then
           (* both idx < 0, size doesn't matter *)
           match idxcmp with
           | `LeftSmallerThanRight ->
@@ -211,9 +211,9 @@ module ArrayAccessCondition = struct
     let not_overrun = ItvPure.lt_sem c'.idx c'.size in
     let not_underrun = ItvPure.le_sem ItvPure.zero c'.idx in
     (* il >= 0 and iu < sl, definitely not an error *)
-    if ItvPure.is_one not_overrun && ItvPure.is_one not_underrun then
+    if Itv.Boolean.is_true not_overrun && Itv.Boolean.is_true not_underrun then
       {report_issue_type= None; propagate= false} (* iu < 0 or il >= su, definitely an error *)
-    else if ItvPure.is_zero not_overrun || ItvPure.is_zero not_underrun then
+    else if Itv.Boolean.is_false not_overrun || Itv.Boolean.is_false not_underrun then
       {report_issue_type= Some IssueType.buffer_overrun_l1; propagate= false}
       (* su <= iu < +oo, most probably an error *)
     else if Itv.Bound.is_not_infty (ItvPure.ub c.idx)
diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml
index 4d54258cb..83d4e50b2 100644
--- a/infer/src/bufferoverrun/itv.ml
+++ b/infer/src/bufferoverrun/itv.ml
@@ -32,6 +32,18 @@ module Counter = struct
   let next : t -> int = fun counter -> counter ()
 end
 
+module Boolean = struct
+  type t = Bottom | False | True | Top [@@deriving compare]
+
+  let top = Top
+
+  let equal = [%compare.equal : t]
+
+  let is_false = function False -> true | _ -> false
+
+  let is_true = function True -> true | _ -> false
+end
+
 exception Not_one_symbol
 
 module Symbol = struct
@@ -313,8 +325,6 @@ module Bound = struct
 
   type astate = t
 
-  let equal = [%compare.equal : t]
-
   let pp : F.formatter -> t -> unit =
    fun fmt -> function
     | MInf ->
@@ -682,16 +692,20 @@ module Bound = struct
 
   let widen_l : t -> t -> t =
    fun x y ->
-    if equal x PInf || equal y PInf then L.(die InternalError) "Lower bound cannot be +oo."
-    else if le x y then x
-    else MInf
+    match (x, y) with
+    | PInf, _ | _, PInf ->
+        L.(die InternalError) "Lower bound cannot be +oo."
+    | _ ->
+        if le x y then x else MInf
 
 
   let widen_u : t -> t -> t =
    fun x y ->
-    if equal x MInf || equal y MInf then L.(die InternalError) "Upper bound cannot be -oo."
-    else if le y x then x
-    else PInf
+    match (x, y) with
+    | MInf, _ | _, MInf ->
+        L.(die InternalError) "Upper bound cannot be -oo."
+    | _ ->
+        if le y x then x else PInf
 
 
   let widen ~prev ~next ~num_iters:_ = widen_u prev next
@@ -712,8 +726,6 @@ module Bound = struct
 
   let is_zero : t -> bool = is_some_const 0
 
-  let is_one : t -> bool = is_some_const 1
-
   let is_const : t -> int option =
    fun x -> match x with Linear (c, y) when SymLinear.is_zero y -> Some c | _ -> None
 
@@ -866,8 +878,6 @@ module ItvPure = struct
 
   type t = astate
 
-  let equal = [%compare.equal : astate]
-
   let lb : t -> Bound.t = fst
 
   let ub : t -> Bound.t = snd
@@ -980,8 +990,6 @@ module ItvPure = struct
         None
 
 
-  let is_one : t -> bool = fun (l, u) -> Bound.is_one l && Bound.is_one u
-
   let is_zero : t -> bool = fun (l, u) -> Bound.is_zero l && Bound.is_zero u
 
   let is_true : t -> bool = fun (l, u) -> Bound.le Bound.one l || Bound.le u Bound.mone
@@ -1003,8 +1011,8 @@ module ItvPure = struct
     (l', u')
 
 
-  let lnot : t -> t =
-   fun x -> if is_true x then false_sem else if is_false x then true_sem else unknown_bool
+  let lnot : t -> Boolean.t =
+   fun x -> if is_true x then Boolean.False else if is_false x then Boolean.True else Boolean.Top
 
 
   let plus : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.plus_l l1 l2, Bound.plus_u u1 u2)
@@ -1099,46 +1107,46 @@ module ItvPure = struct
         top
 
 
-  let lt_sem : t -> t -> t =
+  let lt_sem : t -> t -> Boolean.t =
    fun (l1, u1) (l2, u2) ->
-    if Bound.lt u1 l2 then true_sem else if Bound.le u2 l1 then false_sem else unknown_bool
+    if Bound.lt u1 l2 then Boolean.True else if Bound.le u2 l1 then Boolean.False else Boolean.Top
 
 
-  let gt_sem : t -> t -> t = fun x y -> lt_sem y x
+  let gt_sem : t -> t -> Boolean.t = fun x y -> lt_sem y x
 
-  let le_sem : t -> t -> t =
+  let le_sem : t -> t -> Boolean.t =
    fun (l1, u1) (l2, u2) ->
-    if Bound.le u1 l2 then true_sem else if Bound.lt u2 l1 then false_sem else unknown_bool
+    if Bound.le u1 l2 then Boolean.True else if Bound.lt u2 l1 then Boolean.False else Boolean.Top
 
 
-  let ge_sem : t -> t -> t = fun x y -> le_sem y x
+  let ge_sem : t -> t -> Boolean.t = fun x y -> le_sem y x
 
-  let eq_sem : t -> t -> t =
+  let eq_sem : t -> t -> Boolean.t =
    fun (l1, u1) (l2, u2) ->
-    if Bound.eq l1 u1 && Bound.eq u1 l2 && Bound.eq l2 u2 then true_sem
-    else if Bound.lt u1 l2 || Bound.lt u2 l1 then false_sem
-    else unknown_bool
+    if Bound.eq l1 u1 && Bound.eq u1 l2 && Bound.eq l2 u2 then Boolean.True
+    else if Bound.lt u1 l2 || Bound.lt u2 l1 then Boolean.False
+    else Boolean.Top
 
 
-  let ne_sem : t -> t -> t =
+  let ne_sem : t -> t -> Boolean.t =
    fun (l1, u1) (l2, u2) ->
-    if Bound.eq l1 u1 && Bound.eq u1 l2 && Bound.eq l2 u2 then false_sem
-    else if Bound.lt u1 l2 || Bound.lt u2 l1 then true_sem
-    else unknown_bool
+    if Bound.eq l1 u1 && Bound.eq u1 l2 && Bound.eq l2 u2 then Boolean.False
+    else if Bound.lt u1 l2 || Bound.lt u2 l1 then Boolean.True
+    else Boolean.Top
 
 
-  let land_sem : t -> t -> t =
+  let land_sem : t -> t -> Boolean.t =
    fun x y ->
-    if is_true x && is_true y then true_sem
-    else if is_false x || is_false y then false_sem
-    else unknown_bool
+    if is_true x && is_true y then Boolean.True
+    else if is_false x || is_false y then Boolean.False
+    else Boolean.Top
 
 
-  let lor_sem : t -> t -> t =
+  let lor_sem : t -> t -> Boolean.t =
    fun x y ->
-    if is_true x || is_true y then true_sem
-    else if is_false x && is_false y then false_sem
-    else unknown_bool
+    if is_true x || is_true y then Boolean.True
+    else if is_false x && is_false y then Boolean.False
+    else Boolean.Top
 
 
   let min_sem : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.lb l1 l2, Bound.lb ~default:u1 u1 u2)
@@ -1302,15 +1310,7 @@ let ub : t -> Bound.t = function
       L.(die InternalError) "upper bound of bottom"
 
 
-let of_int : int -> astate = fun n -> NonBottom (ItvPure.of_int n)
-
-let of_int_lit n = try of_int (IntLit.to_int n) with _ -> top
-
-let of_int64 : Int64.t -> astate =
- fun n -> Int64.to_int n |> Option.value_map ~f:of_int ~default:top
-
-
-let is_false : t -> bool = function NonBottom x -> ItvPure.is_false x | Bottom -> false
+let false_sem = NonBottom ItvPure.false_sem
 
 let m1_255 = NonBottom ItvPure.m1_255
 
@@ -1320,10 +1320,33 @@ let one = NonBottom ItvPure.one
 
 let pos = NonBottom ItvPure.pos
 
+let true_sem = NonBottom ItvPure.true_sem
+
 let unknown_bool = NonBottom ItvPure.unknown_bool
 
 let zero = NonBottom ItvPure.zero
 
+let of_bool = function
+  | Boolean.Bottom ->
+      bot
+  | Boolean.False ->
+      false_sem
+  | Boolean.True ->
+      true_sem
+  | Boolean.Top ->
+      unknown_bool
+
+
+let of_int : int -> astate = fun n -> NonBottom (ItvPure.of_int n)
+
+let of_int_lit n = try of_int (IntLit.to_int n) with _ -> top
+
+let of_int64 : Int64.t -> astate =
+ fun n -> Int64.to_int n |> Option.value_map ~f:of_int ~default:top
+
+
+let is_false : t -> bool = function NonBottom x -> ItvPure.is_false x | Bottom -> false
+
 let le : lhs:t -> rhs:t -> bool = ( <= )
 
 let eq : t -> t -> bool = fun x y -> ( <= ) ~lhs:x ~rhs:y && ( <= ) ~lhs:y ~rhs:x
@@ -1334,7 +1357,13 @@ let lift1 : (ItvPure.t -> ItvPure.t) -> t -> t =
  fun f -> function Bottom -> Bottom | NonBottom x -> NonBottom (f x)
 
 
-let bind1 : (ItvPure.t -> t) -> t -> t = fun f -> function Bottom -> Bottom | NonBottom x -> f x
+let bind1_gen : bot:'a -> (ItvPure.t -> 'a) -> t -> 'a =
+ fun ~bot f x -> match x with Bottom -> bot | NonBottom x -> f x
+
+
+let bind1 : (ItvPure.t -> t) -> t -> t = bind1_gen ~bot:Bottom
+
+let bind1b : (ItvPure.t -> Boolean.t) -> t -> Boolean.t = bind1_gen ~bot:Boolean.Bottom
 
 let lift2 : (ItvPure.t -> ItvPure.t -> ItvPure.t) -> t -> t -> t =
  fun f x y ->
@@ -1345,9 +1374,15 @@ let lift2 : (ItvPure.t -> ItvPure.t -> ItvPure.t) -> t -> t -> t =
       NonBottom (f x y)
 
 
-let bind2 : (ItvPure.t -> ItvPure.t -> t) -> t -> t -> t =
- fun f x y ->
-  match (x, y) with Bottom, _ | _, Bottom -> Bottom | NonBottom x, NonBottom y -> f x y
+let bind2_gen : bot:'a -> (ItvPure.t -> ItvPure.t -> 'a) -> t -> t -> 'a =
+ fun ~bot f x y ->
+  match (x, y) with Bottom, _ | _, Bottom -> bot | NonBottom x, NonBottom y -> f x y
+
+
+let bind2 : (ItvPure.t -> ItvPure.t -> t) -> t -> t -> t = bind2_gen ~bot:Bottom
+
+let bind2b : (ItvPure.t -> ItvPure.t -> Boolean.t) -> t -> t -> Boolean.t =
+  bind2_gen ~bot:Boolean.Bottom
 
 
 let plus : t -> t -> t = lift2 ItvPure.plus
@@ -1361,7 +1396,7 @@ let make_sym : ?unsigned:bool -> Typ.Procname.t -> Counter.t -> t =
 
 let neg : t -> t = lift1 ItvPure.neg
 
-let lnot : t -> t = lift1 ItvPure.lnot
+let lnot : t -> Boolean.t = bind1b ItvPure.lnot
 
 let mult : t -> t -> t = lift2 ItvPure.mult
 
@@ -1373,21 +1408,21 @@ let shiftlt : t -> t -> t = lift2 ItvPure.shiftlt
 
 let shiftrt : t -> t -> t = lift2 ItvPure.shiftrt
 
-let lt_sem : t -> t -> t = lift2 ItvPure.lt_sem
+let lt_sem : t -> t -> Boolean.t = bind2b ItvPure.lt_sem
 
-let gt_sem : t -> t -> t = lift2 ItvPure.gt_sem
+let gt_sem : t -> t -> Boolean.t = bind2b ItvPure.gt_sem
 
-let le_sem : t -> t -> t = lift2 ItvPure.le_sem
+let le_sem : t -> t -> Boolean.t = bind2b ItvPure.le_sem
 
-let ge_sem : t -> t -> t = lift2 ItvPure.ge_sem
+let ge_sem : t -> t -> Boolean.t = bind2b ItvPure.ge_sem
 
-let eq_sem : t -> t -> t = lift2 ItvPure.eq_sem
+let eq_sem : t -> t -> Boolean.t = bind2b ItvPure.eq_sem
 
-let ne_sem : t -> t -> t = lift2 ItvPure.ne_sem
+let ne_sem : t -> t -> Boolean.t = bind2b ItvPure.ne_sem
 
-let land_sem : t -> t -> t = lift2 ItvPure.land_sem
+let land_sem : t -> t -> Boolean.t = bind2b ItvPure.land_sem
 
-let lor_sem : t -> t -> t = lift2 ItvPure.lor_sem
+let lor_sem : t -> t -> Boolean.t = bind2b ItvPure.lor_sem
 
 let min_sem : t -> t -> t = lift2 ItvPure.min_sem
 
diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli
index 721da7de7..7fd253e99 100644
--- a/infer/src/bufferoverrun/itv.mli
+++ b/infer/src/bufferoverrun/itv.mli
@@ -19,6 +19,18 @@ module Counter : sig
   val next : t -> int
 end
 
+module Boolean : sig
+  type t
+
+  val top : t
+
+  val equal : t -> t -> bool
+
+  val is_false : t -> bool
+
+  val is_true : t -> bool
+end
+
 module Symbol : sig
   type t
 end
@@ -84,8 +96,6 @@ module ItvPure : sig
 
   val ub : t -> Bound.t
 
-  val is_false : t -> bool
-
   val is_finite : t -> bool
 
   val is_invalid : t -> bool
@@ -94,20 +104,12 @@ module ItvPure : sig
 
   val is_nat : t -> bool
 
-  val is_one : t -> bool
-
   val is_symbolic : t -> bool
 
   val is_top : t -> bool
 
-  val is_true : t -> bool
-
-  val is_zero : t -> bool
-
   val ( <= ) : lhs:t -> rhs:t -> bool
 
-  val equal : t -> t -> bool
-
   val have_similar_bounds : t -> t -> bool
 
   val has_infty : t -> bool
@@ -116,9 +118,9 @@ module ItvPure : sig
 
   val join : t -> t -> t
 
-  val le_sem : t -> t -> t
+  val le_sem : t -> t -> Boolean.t
 
-  val lt_sem : t -> t -> t
+  val lt_sem : t -> t -> Boolean.t
 
   val widen : prev:t -> next:t -> num_iters:int -> t
 
@@ -158,12 +160,11 @@ val pos : t
 val top : t
 (** [-oo, +oo] *)
 
-val unknown_bool : t
-(** [0, 1] *)
-
 val zero : t
 (** 0 *)
 
+val of_bool : Boolean.t -> t
+
 val of_int : int -> t
 
 val of_int_lit : IntLit.t -> t
@@ -178,8 +179,6 @@ val ub : t -> Bound.t
 
 val is_false : t -> bool
 
-val lnot : t -> t
-
 val neg : t -> t
 
 val normalize : t -> t
@@ -190,6 +189,8 @@ val eq : t -> t -> bool
 
 val le : lhs:t -> rhs:t -> bool
 
+val lnot : t -> Boolean.t
+
 val range : t -> Bound.t
 
 val div : t -> t -> t
@@ -204,25 +205,25 @@ val shiftlt : t -> t -> t
 
 val shiftrt : t -> t -> t
 
-val eq_sem : t -> t -> t
+val eq_sem : t -> t -> Boolean.t
 
-val ge_sem : t -> t -> t
+val ge_sem : t -> t -> Boolean.t
 
-val gt_sem : t -> t -> t
+val gt_sem : t -> t -> Boolean.t
 
-val land_sem : t -> t -> t
+val land_sem : t -> t -> Boolean.t
 
-val le_sem : t -> t -> t
+val le_sem : t -> t -> Boolean.t
 
-val lor_sem : t -> t -> t
+val lor_sem : t -> t -> Boolean.t
 
-val lt_sem : t -> t -> t
+val lt_sem : t -> t -> Boolean.t
 
 val min_sem : t -> t -> t
 
 val mod_sem : t -> t -> t
 
-val ne_sem : t -> t -> t
+val ne_sem : t -> t -> Boolean.t
 
 val prune_eq_zero : t -> t