Index: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -1265,28 +1265,44 @@
 
     for (const auto &Range : I.second) {
       const llvm::APSInt &From = Range.From();
-      const llvm::APSInt &To = Range.To();
 
+      // Convert lower bound
       QualType FromTy;
       llvm::APSInt NewFromInt;
       std::tie(NewFromInt, FromTy) = fixAPSInt(From);
       Z3Expr FromExp = Z3Expr::fromAPSInt(NewFromInt);
+
+      // Convert symbol
       QualType SymTy;
       Z3Expr Exp = getZ3Expr(Sym, &SymTy);
       bool IsSignedTy = SymTy->isSignedIntegerOrEnumerationType();
-      QualType ToTy;
-      llvm::APSInt NewToInt;
-      std::tie(NewToInt, ToTy) = fixAPSInt(To);
-      Z3Expr ToExp = Z3Expr::fromAPSInt(NewToInt);
-      assert(FromTy == ToTy && "Range values have different types!");
 
-      Z3Expr LHS =
+      // If the range is a concrete value (lower bound == upper bound),
+      // then generate an equality operation, otherwise convert the range
+      if (Range.getConcreteValue()) {
+        Z3Expr SymValue =
+            getZ3BinExpr(Exp, SymTy, BO_EQ, FromExp, FromTy, /*RetTy=*/nullptr);
+        Constraints =
+          Z3Expr::fromBinOp(Constraints, BO_LOr, SymValue, IsSignedTy);
+      } else {
+        // Convert upper bound
+        QualType ToTy;
+        llvm::APSInt NewToInt;
+        const llvm::APSInt &To = Range.To();
+        std::tie(NewToInt, ToTy) = fixAPSInt(To);
+        Z3Expr ToExp = Z3Expr::fromAPSInt(NewToInt);
+        assert(FromTy == ToTy && "Range values have different types!");
+
+        Z3Expr LHS =
           getZ3BinExpr(Exp, SymTy, BO_GE, FromExp, FromTy, /*RetTy=*/nullptr);
-      Z3Expr RHS =
+        Z3Expr RHS =
           getZ3BinExpr(Exp, SymTy, BO_LE, ToExp, FromTy, /*RetTy=*/nullptr);
-      Z3Expr SymRange = Z3Expr::fromBinOp(LHS, BO_LAnd, RHS, IsSignedTy);
-      Constraints =
+
+        // Generate the expression (symbol >= lower && symbol <= upper)
+        Z3Expr SymRange = Z3Expr::fromBinOp(LHS, BO_LAnd, RHS, IsSignedTy);
+        Constraints =
           Z3Expr::fromBinOp(Constraints, BO_LOr, SymRange, IsSignedTy);
+      }
     }
     Solver.addConstraint(Constraints);
   }