diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp
new file mode 100644
index 000000000..05edd582f
--- /dev/null
+++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp
@@ -0,0 +1,123 @@
+/*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+#include <stddef.h>
+
+void conditional_buffer_access(int* ptr, unsigned int size) {
+  int i;
+  if (size < 1) {
+  } else if (size < 2) {
+    i = *(ptr++);
+  } else if (size < 3) {
+    i = *(ptr++);
+    i = *(ptr++);
+  } else if (size < 4) {
+    i = *(ptr++);
+    i = *(ptr++);
+    i = *(ptr++);
+  } else if (size < 5) {
+    i = *(ptr++);
+    i = *(ptr++);
+    i = *(ptr++);
+    i = *(ptr++);
+  }
+}
+
+void call_conditional_buffer_access_Good_FP() {
+  int a[1];
+  conditional_buffer_access(a, 1);
+}
+
+void call_conditional_buffer_access_Bad() {
+  int a[1];
+  conditional_buffer_access(a, 3);
+}
+
+void conditional_buffer_access2(unsigned int n) {
+  int a[n];
+  conditional_buffer_access(a, n);
+}
+
+void call_conditional_buffer_access2_1_Good_FP() {
+  conditional_buffer_access2(1);
+}
+
+void call_conditional_buffer_access2_2_Good_FP() {
+  conditional_buffer_access2(3);
+}
+
+void conditional_minus(int* ptr, unsigned int size) {
+  int i = 0;
+  if (ptr != NULL && (i < size - 1)) {
+  }
+}
+
+void call_conditional_minus_1_Good_FP() { conditional_minus(NULL, 0); }
+
+void call_conditional_minus_2_Good() {
+  int a[3];
+  conditional_minus(a, 3);
+}
+
+void call_conditional_minus_2_Bad() {
+  int a[3];
+  conditional_minus(a, 0);
+}
+
+unsigned int conditional_minus2(int* ptr, unsigned int size) {
+  if (ptr != NULL) {
+    return (size - 1);
+  }
+}
+
+void call_conditional_minus2_1_Good_FP() { conditional_minus2(NULL, 0); }
+
+void call_conditional_minus2_2_Good() {
+  int a[3];
+  conditional_minus2(a, 3);
+}
+
+void call_conditional_minus2_2_Bad() {
+  int a[3];
+  conditional_minus2(a, 0);
+}
+
+enum E {
+  E_SIZEONE = 0,
+  E_SIZETWO = 1,
+};
+
+void conditional_buffer_access3(int* ptr, int size) {
+  int i;
+  switch (ptr[0]) {
+    case E_SIZETWO:
+      i = ptr[size - 2];
+      i = ptr[size - 1];
+      break;
+
+    case E_SIZEONE:
+      i = ptr[size - 1];
+      break;
+  }
+}
+
+void call_conditional_buffer_access3_1_Good() {
+  int a[2];
+  a[0] = E_SIZETWO;
+  conditional_buffer_access3(a, 2);
+}
+
+void call_conditional_buffer_access3_2_Good_FP() {
+  int a[1];
+  a[0] = E_SIZEONE;
+  conditional_buffer_access3(a, 1);
+}
+
+void call_conditional_buffer_access3_Bad() {
+  int a[1];
+  a[0] = E_SIZETWO;
+  conditional_buffer_access3(a, 1);
+}
diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
index 0da5151af..1932c6aef 100644
--- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
+++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
@@ -28,6 +28,16 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_overload1_Bad, 3, BUFFE
 codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_overload2_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5]
 codetoanalyze/cpp/bufferoverrun/class.cpp, return_class_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Call,Array access: Offset: 5 Size: 5]
 codetoanalyze/cpp/bufferoverrun/class.cpp, use_global_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 32 Size: 30]
+codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access2_1_Good_FP, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter `n`,Array declaration,Call,<Length trace>,Parameter `*ptr`,Assignment,Assignment,Assignment,Array access: Offset: 3 Size: 1 by call to `conditional_buffer_access2` ]
+codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access2_2_Good_FP, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter `n`,Array declaration,Call,<Length trace>,Parameter `*ptr`,Assignment,Assignment,Assignment,Array access: Offset: 3 Size: 3 by call to `conditional_buffer_access2` ]
+codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access3_2_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Parameter `size`,<Length trace>,Parameter `*ptr`,Array access: Offset: -1 Size: 1 by call to `conditional_buffer_access3` ]
+codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access3_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Parameter `size`,<Length trace>,Parameter `*ptr`,Array access: Offset: -1 Size: 1 by call to `conditional_buffer_access3` ]
+codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `*ptr`,Assignment,Assignment,Assignment,Array access: Offset: 3 Size: 1 by call to `conditional_buffer_access` ]
+codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access_Good_FP, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `*ptr`,Assignment,Assignment,Assignment,Array access: Offset: 3 Size: 1 by call to `conditional_buffer_access` ]
+codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus2_1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus2` ]
+codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus2_2_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus2` ]
+codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus_1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus` ]
+codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus_2_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus` ]
 codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,<Length trace>,Parameter `*__il`,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Call,Call,Unknown value from: std::distance<const_int_*>,Call,Parameter `__n`,Assignment,Call,Parameter `__x->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Assignment,Binary operation: (1 - [0, +oo]):unsigned64]
 codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: lib,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]]