diff --git a/clang/lib/StaticAnalyzer/Checkers/CStringChecker.cpp b/clang/lib/StaticAnalyzer/Checkers/CStringChecker.cpp
--- a/clang/lib/StaticAnalyzer/Checkers/CStringChecker.cpp
+++ b/clang/lib/StaticAnalyzer/Checkers/CStringChecker.cpp
@@ -449,6 +449,11 @@
 
   ProgramStateRef stateTrue, stateFalse;
 
+  // Assume different address spaces cannot overlap.
+  if (First.Expression->getType()->getPointeeType().getAddressSpace() !=
+      Second.Expression->getType()->getPointeeType().getAddressSpace())
+    return state;
+
   // Get the buffer values and make sure they're known locations.
   const LocationContext *LCtx = C.getLocationContext();
   SVal firstVal = state->getSVal(First.Expression, LCtx);
diff --git a/clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp b/clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
--- a/clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
+++ b/clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
@@ -715,11 +715,35 @@
   llvm_unreachable("Fields not found in parent record's definition");
 }
 
+static bool assertEqualBitWidths(ProgramStateRef State, Loc RhsLoc,
+                                 Loc LhsLoc) {
+  // Implements a "best effort" check for RhsLoc and LhsLoc bit widths
+  ASTContext &Ctx = State->getStateManager().getContext();
+  uint64_t RhsBitwidth =
+      RhsLoc.getType(Ctx).isNull() ? 0 : Ctx.getTypeSize(RhsLoc.getType(Ctx));
+  uint64_t LhsBitwidth =
+      LhsLoc.getType(Ctx).isNull() ? 0 : Ctx.getTypeSize(LhsLoc.getType(Ctx));
+  if (RhsBitwidth && LhsBitwidth &&
+      (LhsLoc.getSubKind() == RhsLoc.getSubKind())) {
+    assert(RhsBitwidth == LhsBitwidth &&
+           "RhsLoc and LhsLoc bitwidth must be same!");
+    return RhsBitwidth == LhsBitwidth;
+  }
+  return false;
+}
+
 // FIXME: all this logic will change if/when we have MemRegion::getLocation().
 SVal SimpleSValBuilder::evalBinOpLL(ProgramStateRef state,
                                   BinaryOperator::Opcode op,
                                   Loc lhs, Loc rhs,
                                   QualType resultTy) {
+
+  // Assert that bitwidth of lhs and rhs are the same.
+  // This can happen if two different address spaces are used,
+  // and the bitwidths of the address spaces are different.
+  // See LIT case clang/test/Analysis/cstring-checker-addressspace.c
+  assertEqualBitWidths(state, rhs, lhs);
+
   // Only comparisons and subtractions are valid operations on two pointers.
   // See [C99 6.5.5 through 6.5.14] or [C++0x 5.6 through 5.15].
   // However, if a pointer is casted to an integer, evalBinOpNN may end up
diff --git a/clang/test/Analysis/cstring-addrspace.c b/clang/test/Analysis/cstring-addrspace.c
new file mode 100644
--- /dev/null
+++ b/clang/test/Analysis/cstring-addrspace.c
@@ -0,0 +1,64 @@
+// RUN: %clang_analyze_cc1 -triple amdgcn-unknown-unknown \
+// RUN: -analyze -analyzer-checker=core,alpha.unix.cstring \
+// RUN: -analyze -analyzer-checker=debug.ExprInspection \
+// RUN: -analyzer-config crosscheck-with-z3=true -verify %s \
+// RUN: -Wno-incompatible-library-redeclaration
+// REQUIRES: z3
+
+void clang_analyzer_warnIfReached();
+
+// From https://llvm.org/docs/AMDGPUUsage.html#address-spaces,
+// select address space 3 (local), since the pointer size is
+// different than Generic.
+#define DEVICE __attribute__((address_space(3)))
+_Static_assert(sizeof(int *) == 8, "");
+_Static_assert(sizeof(DEVICE int *) == 4, "");
+_Static_assert(sizeof(void *) == 8, "");
+_Static_assert(sizeof(DEVICE void *) == 4, "");
+
+// Copy from host to device memory. Note this is specialized
+// since one of the parameters is assigned an address space such
+// that the sizeof the the pointer is different than the other.
+//
+// Some downstream implementations may have specialized memcpy
+// routines that copy from one address space to another. In cases
+// like that, the address spaces are assumed to not overlap, so the
+// cstring overlap check is not needed. When a static analysis report
+// is generated in as case like this, SMTConv may attempt to create
+// a refutation to Z3 with different bitwidth pointers which lead to
+// a crash. This is not common in directly used upstream compiler builds,
+// but can be seen in specialized downstrean implementations. This case
+// covers those specific instances found and debugged.
+//
+// Since memcpy is a builtin, a specialized builtin instance named like
+// 'memcpy_special' will hit in cstring, triggering this behavior. The
+// best we can do for an upstream test is use the same memcpy function name.
+DEVICE void *memcpy(DEVICE void *dst, const void *src, unsigned long len);
+
+void top1(DEVICE void *dst, void *src, int len) {
+  memcpy(dst, src, len);
+
+  // Create a bugreport for triggering Z3 refutation.
+  clang_analyzer_warnIfReached(); // expected-warning {{REACHABLE}}
+}
+
+void top2(DEVICE int *dst, void *src, int len) {
+  memcpy(dst, src, len);
+
+  // Create a bugreport for triggering Z3 refutation.
+  clang_analyzer_warnIfReached(); // expected-warning {{REACHABLE}}
+}
+
+void top3(DEVICE int *dst, int *src, int len) {
+  memcpy(dst, src, len);
+
+  // Create a bugreport for triggering Z3 refutation.
+  clang_analyzer_warnIfReached(); // expected-warning {{REACHABLE}}
+}
+
+void top4() {
+  memcpy((DEVICE void *)1, (const void *)1, 1);
+
+  // Create a bugreport for triggering Z3 refutation.
+  clang_analyzer_warnIfReached(); // expected-warning {{REACHABLE}}
+}