Index: lib/StaticAnalyzer/Core/BugReporter.cpp
===================================================================
--- lib/StaticAnalyzer/Core/BugReporter.cpp
+++ lib/StaticAnalyzer/Core/BugReporter.cpp
@@ -2594,10 +2594,12 @@
   AnalyzerOptions &Opts,
   GRBugReporter &Reporter) {
 
+  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;
@@ -2605,8 +2607,6 @@
     // Register refutation visitors first, if they mark the bug invalid no
     // further analysis is required
     R->addVisitor(llvm::make_unique<LikelyFalsePositiveSuppressionBRVisitor>());
-    if (Opts.shouldCrosscheckWithZ3())
-      R->addVisitor(llvm::make_unique<FalsePositiveRefutationBRVisitor>());
 
     // Register additional node visitors.
     R->addVisitor(llvm::make_unique<NilReceiverBRVisitor>());
@@ -2616,12 +2616,22 @@
     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()) {
+    R->clearVisitors();
+    R->addVisitor(llvm::make_unique<FalsePositiveRefutationBRVisitor>());
+    BugReporterContext BRC(Reporter, ErrorGraph.BackMap);
+    visitorNotes = generateVisitorsDiagnostics(R, ErrorGraph.ErrorNode, BRC);
+  }
+
+  if (R->isValid())
+    return std::make_pair(R, std::move(visitorNotes));
+
   return std::make_pair(nullptr, llvm::make_unique<VisitorsDiagnosticsTy>());
 }