diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -122,8 +122,7 @@
       // this method tries to get the interpretation (the actual value) from
       // the solver, which is currently not cached.
 
-      llvm::SMTExprRef Exp =
-          SMTConv::fromData(Solver, SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty));
+      llvm::SMTExprRef Exp = SMTConv::fromData(Solver, Ctx, SD);
 
       Solver->reset();
       addStateConstraints(State);
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -319,11 +319,41 @@
   }
 
   /// Construct an SMTSolverRef from a SymbolData.
-  static inline llvm::SMTExprRef fromData(llvm::SMTSolverRef &Solver,
-                                          const SymbolID ID, const QualType &Ty,
-                                          uint64_t BitWidth) {
-    llvm::Twine Name = "$" + llvm::Twine(ID);
-    return Solver->mkSymbol(Name.str().c_str(), mkSort(Solver, Ty, BitWidth));
+  static inline llvm::SMTExprRef
+  fromData(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const SymbolData *Sym) {
+    const SymbolID ID = Sym->getSymbolID();
+    const QualType Ty = Sym->getType();
+    const uint64_t BitWidth = Ctx.getTypeSize(Ty);
+
+    const auto GetPrettyPrefixFor = [](const SymbolData *Sym) -> const char * {
+      switch (Sym->getKind()) {
+      default:
+        llvm_unreachable("There should be no other SymbolData kind.");
+      case SymExpr::SymbolConjuredKind:
+        return "conj_";
+      case SymExpr::SymbolDerivedKind:
+        return "derived_";
+      case SymExpr::SymbolExtentKind:
+        return "extent_";
+      case SymExpr::SymbolMetadataKind:
+        return "meta_";
+      case SymExpr::SymbolRegionValueKind:
+        return "reg_";
+      }
+    };
+    // Suppress unused variable warning in release build.
+    static_cast<void>(GetPrettyPrefixFor);
+
+#if !defined(NDEBUG) || defined(LLVM_ENABLE_DUMP)
+#define PRETTY_SYMBOL_KIND GetPrettyPrefixFor(Sym)
+#else
+#define PRETTY_SYMBOL_KIND ""
+#endif
+    llvm::SmallString<16> Str;
+    llvm::raw_svector_ostream OS(Str);
+    OS << "$" << PRETTY_SYMBOL_KIND << ID;
+#undef PRETTY_SYMBOL_KIND
+    return Solver->mkSymbol(Str.c_str(), mkSort(Solver, Ty, BitWidth));
   }
 
   // Wrapper to generate SMTSolverRef from SymbolCast data.
@@ -422,8 +452,7 @@
       if (RetTy)
         *RetTy = Sym->getType();
 
-      return fromData(Solver, SD->getSymbolID(), Sym->getType(),
-                      Ctx.getTypeSize(Sym->getType()));
+      return fromData(Solver, Ctx, SD);
     }
 
     if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
diff --git a/clang/test/Analysis/z3/pretty-dump.c b/clang/test/Analysis/z3/pretty-dump.c
new file mode 100644
--- /dev/null
+++ b/clang/test/Analysis/z3/pretty-dump.c
@@ -0,0 +1,17 @@
+// RUN: %clang_cc1 -analyze -analyzer-constraints=z3 -setup-static-analyzer \
+// RUN:   -analyzer-checker=core,debug.ExprInspection %s 2>&1 | FileCheck %s
+//
+// REQUIRES: z3
+//
+// Works only with the z3 constraint manager.
+
+void clang_analyzer_printState();
+
+void foo(int x) {
+  if (x == 3) {
+    clang_analyzer_printState();
+    (void)x;
+    // CHECK: "constraints": [
+    // CHECK-NEXT: { "symbol": "(reg_$[[#]]<int x>) == 3", "range": "(= $reg_[[#]] #x00000003)" }
+  }
+}