Index: include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
===================================================================
--- include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
+++ include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
@@ -17,6 +17,7 @@
 
 #include "clang/Basic/LLVM.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
 #include "llvm/ADT/FoldingSet.h"
 #include "llvm/ADT/STLExtras.h"
@@ -338,8 +339,11 @@
   /// Holds the constraints in a given path
   ConstraintRangeTy Constraints;
 
+  /// Holds the Refutation Manager
+  ConstraintManager &RefutationMgr;
+
 public:
-  FalsePositiveRefutationBRVisitor();
+  FalsePositiveRefutationBRVisitor(ConstraintManager &R);
 
   void Profile(llvm::FoldingSetNodeID &ID) const override;
 
Index: include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
===================================================================
--- include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -24,6 +24,8 @@
 class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
   SMTSolverRef &Solver;
 
+  llvm::SmallVector<ConstraintRangeTy, 32> AllPathConstraints;
+
 public:
   SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB,
                        SMTSolverRef &S)
@@ -60,7 +62,7 @@
   void addRangeConstraints(clang::ento::ConstraintRangeTy CR);
 
   /// Checks if the added constraints are satisfiable
-  clang::ento::ConditionTruthVal isModelFeasible();
+  clang::ento::ConditionTruthVal areConstraintsFeasible();
 
   /// Dumps SMT formula
   LLVM_DUMP_METHOD void dump() const { Solver->dump(); }
Index: lib/StaticAnalyzer/Core/BugReporter.cpp
===================================================================
--- lib/StaticAnalyzer/Core/BugReporter.cpp
+++ lib/StaticAnalyzer/Core/BugReporter.cpp
@@ -2586,18 +2586,24 @@
 /// Find a non-invalidated report for a given equivalence class,
 /// and return together with a cache of visitors notes.
 /// If none found, return a nullptr paired with an empty cache.
-static
-std::pair<BugReport*, std::unique_ptr<VisitorsDiagnosticsTy>> findValidReport(
-  TrimmedGraph &TrimG,
-  ReportGraph &ErrorGraph,
-  ArrayRef<BugReport *> &bugReports,
-  AnalyzerOptions &Opts,
-  GRBugReporter &Reporter) {
+static std::pair<BugReport *, std::unique_ptr<VisitorsDiagnosticsTy>>
+findValidReport(TrimmedGraph &TrimG, ReportGraph &ErrorGraph,
+                ArrayRef<BugReport *> &bugReports, AnalyzerOptions &Opts,
+                GRBugReporter &Reporter) {
 
+  std::unique_ptr<ConstraintManager> RefutationMgr = nullptr;
+  if (Opts.shouldCrosscheckWithZ3()) {
+    RefutationMgr =
+        CreateZ3ConstraintManager(Reporter.getStateManager(),
+                                  Reporter.getStateManager().getOwningEngine());
+  }
+
+  BugReport *R = nullptr;
+  std::unique_ptr<VisitorsDiagnosticsTy> visitorNotes = nullptr;
   while (TrimG.popNextReportGraph(ErrorGraph)) {
     // Find the BugReport with the original location.
     assert(ErrorGraph.Index < bugReports.size());
-    BugReport *R = bugReports[ErrorGraph.Index];
+    R = bugReports[ErrorGraph.Index];
     assert(R && "No original report found for sliced graph.");
     assert(R->isValid() && "Report selected by trimmed graph marked invalid.");
     const ExplodedNode *ErrorNode = ErrorGraph.ErrorNode;
@@ -2606,7 +2612,8 @@
     // further analysis is required
     R->addVisitor(llvm::make_unique<LikelyFalsePositiveSuppressionBRVisitor>());
     if (Opts.shouldCrosscheckWithZ3())
-      R->addVisitor(llvm::make_unique<FalsePositiveRefutationBRVisitor>());
+      R->addVisitor(
+          llvm::make_unique<FalsePositiveRefutationBRVisitor>(*RefutationMgr));
 
     // Register additional node visitors.
     R->addVisitor(llvm::make_unique<NilReceiverBRVisitor>());
@@ -2616,12 +2623,24 @@
     BugReporterContext BRC(Reporter, ErrorGraph.BackMap);
 
     // Run all visitors on a given graph, once.
-    std::unique_ptr<VisitorsDiagnosticsTy> visitorNotes =
-        generateVisitorsDiagnostics(R, ErrorNode, BRC);
+    visitorNotes = generateVisitorsDiagnostics(R, ErrorNode, BRC);
 
     if (R->isValid())
-      return std::make_pair(R, std::move(visitorNotes));
+      break;
+  }
+
+  if (Opts.shouldCrosscheckWithZ3()) {
+    SMTConstraintManager *SMTRefutationMgr =
+        static_cast<SMTConstraintManager *>(RefutationMgr.get());
+
+    if (SMTRefutationMgr->areConstraintsFeasible().isConstrainedFalse())
+      R->markInvalid("Infeasible constraints",
+                     R->getErrorNode()->getLocationContext());
   }
+
+  if (R->isValid())
+    return std::make_pair(R, std::move(visitorNotes));
+
   return std::make_pair(nullptr, llvm::make_unique<VisitorsDiagnosticsTy>());
 }
 
Index: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
===================================================================
--- lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
+++ lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
@@ -44,7 +44,6 @@
 #include "clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
 #include "llvm/ADT/ArrayRef.h"
 #include "llvm/ADT/None.h"
 #include "llvm/ADT/Optional.h"
@@ -2370,45 +2369,22 @@
   return std::make_shared<PathDiagnosticEventPiece>(L, "Taint originated here");
 }
 
-static bool areConstraintsUnfeasible(BugReporterContext &BRC,
-                                     const ConstraintRangeTy &Cs) {
-  // Create a refutation manager
-  std::unique_ptr<ConstraintManager> RefutationMgr = CreateZ3ConstraintManager(
-      BRC.getStateManager(), BRC.getStateManager().getOwningEngine());
-
-  SMTConstraintManager *SMTRefutationMgr =
-      static_cast<SMTConstraintManager *>(RefutationMgr.get());
-
-  // Add constraints to the solver
-  SMTRefutationMgr->addRangeConstraints(Cs);
-
-  // And check for satisfiability
-  return SMTRefutationMgr->isModelFeasible().isConstrainedFalse();
-}
-
-static void addNewConstraints(ConstraintRangeTy &Cs,
-                              const ConstraintRangeTy &NewCs,
-                              ConstraintRangeTy::Factory &CF) {
-  // Add constraints if we don't have them yet
-  for (auto const &C : NewCs) {
-    const SymbolRef &Sym = C.first;
-    if (!Cs.contains(Sym)) {
-      Cs = CF.add(Cs, Sym, C.second);
-    }
-  }
-}
-
-FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor()
-    : Constraints(ConstraintRangeTy::Factory().getEmptyMap()) {}
+FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor(
+    ConstraintManager &R)
+    : Constraints(ConstraintRangeTy::Factory().getEmptyMap()),
+      RefutationMgr(R) {}
 
 void FalsePositiveRefutationBRVisitor::finalizeVisitor(
     BugReporterContext &BRC, const ExplodedNode *EndPathNode, BugReport &BR) {
   // Collect new constraints
   VisitNode(EndPathNode, nullptr, BRC, BR);
 
-  // Create a new refutation manager and check feasibility
-  if (areConstraintsUnfeasible(BRC, Constraints))
-    BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext());
+  // Adds constraints to the Solver
+  SMTConstraintManager &SMTRefutationMgr =
+    static_cast<SMTConstraintManager &>(RefutationMgr);
+
+  // Add constraints to the solver
+  SMTRefutationMgr.addRangeConstraints(Constraints);
 }
 
 std::shared_ptr<PathDiagnosticPiece>
@@ -2416,9 +2392,17 @@
                                             const ExplodedNode *PrevN,
                                             BugReporterContext &BRC,
                                             BugReport &BR) {
-  // Collect new constraints
-  addNewConstraints(Constraints, N->getState()->get<ConstraintRange>(),
-                    N->getState()->get_context<ConstraintRange>());
+  const ConstraintRangeTy &Cs = N->getState()->get<ConstraintRange>();
+  ConstraintRangeTy::Factory &CF =
+      N->getState()->get_context<ConstraintRange>();
+
+  // Collect new constraints, if we don't have them yet
+  for (auto const &C : Cs) {
+    const SymbolRef &Sym = C.first;
+    if (!Constraints.contains(Sym)) {
+      Constraints = CF.add(Constraints, Sym, C.second);
+    }
+  }
 
   return nullptr;
 }
Index: lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
@@ -16,26 +16,42 @@
 using namespace ento;
 
 void SMTConstraintManager::addRangeConstraints(ConstraintRangeTy CR) {
-  Solver->reset();
+  AllPathConstraints.push_back(CR);
+}
+
+clang::ento::ConditionTruthVal SMTConstraintManager::areConstraintsFeasible() {
 
-  for (const auto &I : CR) {
-    SymbolRef Sym = I.first;
+  // Will hold all the constraints of all path
+  SMTExprRef AllPathFormula = Solver->fromBoolean(true);
 
-    SMTExprRef Constraints = Solver->fromBoolean(false);
-    for (const auto &Range : I.second) {
-      SMTExprRef SymRange =
-          getRangeExpr(Sym, Range.From(), Range.To(), /*InRange=*/true);
+  for (const auto &CR : AllPathConstraints) {
+    SMTExprRef PathConstraints = Solver->fromBoolean(true);
 
-      // FIXME: the last argument (isSigned) is not used when generating the
-      // or expression, as both arguments are booleans
-      Constraints =
-          Solver->fromBinOp(Constraints, BO_LOr, SymRange, /*IsSigned=*/true);
+    // This loop will add all the constraints of a given path
+    for (const auto &I : CR) {
+      SymbolRef Sym = I.first;
+
+      // Collect all the ranges for a given symbol
+      SMTExprRef SymbolConstraints = Solver->fromBoolean(false);
+      for (const auto &Range : I.second) {
+        SymbolConstraints = Solver->mkOr(
+            SymbolConstraints,
+            getRangeExpr(Sym, Range.From(), Range.To(), /*InRange=*/true));
+      }
+
+      // Collect all the ranges for all symbol
+      PathConstraints = Solver->mkAnd(PathConstraints, SymbolConstraints);
     }
-    Solver->addConstraint(Constraints);
+
+    // At this point, we have all the constraints of a given path in
+    // PathConstraints, so add them to AllPathFormula
+    AllPathFormula = Solver->mkAnd(AllPathFormula, PathConstraints);
   }
-}
 
-clang::ento::ConditionTruthVal SMTConstraintManager::isModelFeasible() {
+  // All now holds all the constraints, of all paths
+  Solver->addConstraint(AllPathFormula);
+
+  // Check for satisfiability
   return Solver->check();
 }