diff --git a/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h b/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
--- a/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
+++ b/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
@@ -386,6 +386,7 @@
 
   void finalizeVisitor(BugReporterContext &BRC, const ExplodedNode *EndPathNode,
                        PathSensitiveBugReport &BR) override;
+  void addConstraints(const ExplodedNode *N, bool OnlyForNewSymbols);
 };
 
 
diff --git a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp b/clang/lib/StaticAnalyzer/Core/BugReporter.cpp
--- a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp
+++ b/clang/lib/StaticAnalyzer/Core/BugReporter.cpp
@@ -38,6 +38,7 @@
 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/MemRegion.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h"
 #include "llvm/ADT/ArrayRef.h"
@@ -2782,7 +2783,7 @@
         R->clearVisitors();
         R->addVisitor(std::make_unique<FalsePositiveRefutationBRVisitor>());
 
-        // We don't overrite the notes inserted by other visitors because the
+        // We don't overwrite the notes inserted by other visitors because the
         // refutation manager does not add any new note to the path
         generateVisitorsDiagnostics(R, BugPath->ErrorNode, BRC);
       }
diff --git a/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp b/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
--- a/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
+++ b/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
@@ -2820,7 +2820,7 @@
     BugReporterContext &BRC, const ExplodedNode *EndPathNode,
     PathSensitiveBugReport &BR) {
   // Collect new constraints
-  VisitNode(EndPathNode, BRC, BR);
+  addConstraints(EndPathNode, /*OnlyForNewSymbols=*/false);
 
   // Create a refutation manager
   llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();
@@ -2831,30 +2831,30 @@
     const SymbolRef Sym = I.first;
     auto RangeIt = I.second.begin();
 
-    llvm::SMTExprRef Constraints = SMTConv::getRangeExpr(
+    llvm::SMTExprRef SMTConstraints = SMTConv::getRangeExpr(
         RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(),
         /*InRange=*/true);
     while ((++RangeIt) != I.second.end()) {
-      Constraints = RefutationSolver->mkOr(
-          Constraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym,
-                                             RangeIt->From(), RangeIt->To(),
-                                             /*InRange=*/true));
+      SMTConstraints = RefutationSolver->mkOr(
+          SMTConstraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym,
+                                                RangeIt->From(), RangeIt->To(),
+                                                /*InRange=*/true));
     }
 
-    RefutationSolver->addConstraint(Constraints);
+    RefutationSolver->addConstraint(SMTConstraints);
   }
 
   // And check for satisfiability
-  Optional<bool> isSat = RefutationSolver->check();
-  if (!isSat.hasValue())
+  Optional<bool> IsSAT = RefutationSolver->check();
+  if (!IsSAT.hasValue())
     return;
 
-  if (!isSat.getValue())
+  if (!IsSAT.getValue())
     BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext());
 }
 
-PathDiagnosticPieceRef FalsePositiveRefutationBRVisitor::VisitNode(
-    const ExplodedNode *N, BugReporterContext &, PathSensitiveBugReport &) {
+void FalsePositiveRefutationBRVisitor::addConstraints(const ExplodedNode *N,
+                                                      bool OnlyForNewSymbols) {
   // Collect new constraints
   const ConstraintRangeTy &NewCs = N->getState()->get<ConstraintRange>();
   ConstraintRangeTy::Factory &CF =
@@ -2864,10 +2864,19 @@
   for (auto const &C : NewCs) {
     const SymbolRef &Sym = C.first;
     if (!Constraints.contains(Sym)) {
+      // This symbol is new, just add the constraint.
+      Constraints = CF.add(Constraints, Sym, C.second);
+    } else if (!OnlyForNewSymbols) {
+      // Overwrite the associated constraint of the Symbol.
+      Constraints = CF.remove(Constraints, Sym);
       Constraints = CF.add(Constraints, Sym, C.second);
     }
   }
+}
 
+PathDiagnosticPieceRef FalsePositiveRefutationBRVisitor::VisitNode(
+    const ExplodedNode *N, BugReporterContext &, PathSensitiveBugReport &) {
+  addConstraints(N, /*OnlyForNewSymbols=*/true);
   return nullptr;
 }
 
diff --git a/clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp b/clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp
--- a/clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp
+++ b/clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp
@@ -169,6 +169,54 @@
             "test.FalsePositiveGenerator:CAN_BE_TRUE\n");
 }
 
+TEST(FalsePositiveRefutationBRVisitor,
+     UnSatAtErrorNodeDueToRefinedConstraintNoReport) {
+  SKIP_WITHOUT_Z3;
+  constexpr auto Code = R"(
+    void reportIfCanBeTrue(bool);
+    void reachedWithNoContradiction();
+    void test(unsigned x, unsigned n) {
+      if (n >= 1 && n <= 2) {
+        if (x >= 3)
+          return;
+        // x: [0,2] and n: [1,2]
+        int y = x + n; // y: '(x+n)' Which is in approximately between 1 and 4.
+
+        // Registers the symbol 'y' with the constraint [1, MAX] in the true
+        // branch.
+        if (y > 0) {
+          // Since the x: [0,2] and n: [1,2], the 'y' is indeed greater than
+          // zero. If we emit a warning here, the constraints on the BugPath is
+          // SAT. Therefore that report is NOT invalidated.
+          reachedWithNoContradiction(); // 'y' can be greater than zero. OK
+
+          // If we ask the analyzer whether the 'y' can be 5. It won't know,
+          // therefore, the state will be created where the 'y' expression is 5.
+          // Although, this assumption is false!
+          // 'y' can not be 5 if the maximal value of both x and y is 2.
+          // The BugPath which become UnSAT in the ErrorNode with a refined
+          // constraint, should be invalidated.
+          reportIfCanBeTrue(y == 5);
+        }
+      }
+    })";
+
+  std::string Diags;
+  EXPECT_TRUE(runCheckerOnCodeWithArgs<addFalsePositiveGenerator>(
+      Code, LazyAssumeAndCrossCheckArgs, Diags));
+  EXPECT_EQ(Diags,
+            "test.FalsePositiveGenerator:REACHED_WITH_NO_CONTRADICTION\n");
+  // Single warning. The second report was invalidated by the visitor.
+
+  // Without enabling the crosscheck-with-z3 both reports are displayed.
+  std::string Diags2;
+  EXPECT_TRUE(runCheckerOnCodeWithArgs<addFalsePositiveGenerator>(
+      Code, LazyAssumeArgs, Diags2));
+  EXPECT_EQ(Diags2,
+            "test.FalsePositiveGenerator:REACHED_WITH_NO_CONTRADICTION\n"
+            "test.FalsePositiveGenerator:CAN_BE_TRUE\n");
+}
+
 } // namespace
 } // namespace ento
 } // namespace clang