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/SMTExpr.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 previous unsat core's assumptions
+  std::vector<SMTExprRef> &UnsatCore;
+
 public:
-  FalsePositiveRefutationBRVisitor();
+  FalsePositiveRefutationBRVisitor(std::vector<SMTExprRef> &UC);
 
   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
@@ -62,6 +62,12 @@
   /// Checks if the added constraints are satisfiable
   clang::ento::ConditionTruthVal isModelFeasible();
 
+  /// Return the unsat core from the solver
+  std::vector<SMTExprRef> getUnsatCore() { return Solver->getUnsatCore(); }
+
+  /// Add constraints from an unsat core
+  void addConstraintFromUnsatCore(std::vector<SMTExprRef> &UC);
+
   /// Dumps SMT formula
   LLVM_DUMP_METHOD void dump() const { Solver->dump(); }
 
Index: include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
===================================================================
--- include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
+++ include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
@@ -527,6 +527,9 @@
   /// Check if the constraints are satisfiable
   virtual ConditionTruthVal check() const = 0;
 
+  /// Get the unsat core from the solver
+  virtual std::vector<SMTExprRef> getUnsatCore() = 0;
+
   /// Push the current solver state
   virtual void push() = 0;
 
Index: lib/StaticAnalyzer/Core/BugReporter.cpp
===================================================================
--- lib/StaticAnalyzer/Core/BugReporter.cpp
+++ lib/StaticAnalyzer/Core/BugReporter.cpp
@@ -2594,6 +2594,7 @@
   AnalyzerOptions &Opts,
   GRBugReporter &Reporter) {
 
+  std::vector<SMTExprRef> UnsatCore;
   while (TrimG.popNextReportGraph(ErrorGraph)) {
     // Find the BugReport with the original location.
     assert(ErrorGraph.Index < bugReports.size());
@@ -2606,7 +2607,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>(UnsatCore));
 
     // Register additional node visitors.
     R->addVisitor(llvm::make_unique<NilReceiverBRVisitor>());
Index: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
===================================================================
--- lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
+++ lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
@@ -2370,8 +2370,15 @@
   return std::make_shared<PathDiagnosticEventPiece>(L, "Taint originated here");
 }
 
-static bool areConstraintsUnfeasible(BugReporterContext &BRC,
-                                     const ConstraintRangeTy &Cs) {
+FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor(
+    std::vector<SMTExprRef> &UC)
+    : Constraints(ConstraintRangeTy::Factory().getEmptyMap()), UnsatCore(UC) {}
+
+void FalsePositiveRefutationBRVisitor::finalizeVisitor(
+    BugReporterContext &BRC, const ExplodedNode *EndPathNode, BugReport &BR) {
+  // Collect new constraints
+  VisitNode(EndPathNode, nullptr, BRC, BR);
+
   // Create a refutation manager
   std::unique_ptr<ConstraintManager> RefutationMgr = CreateZ3ConstraintManager(
       BRC.getStateManager(), BRC.getStateManager().getOwningEngine());
@@ -2380,35 +2387,22 @@
       static_cast<SMTConstraintManager *>(RefutationMgr.get());
 
   // Add constraints to the solver
-  SMTRefutationMgr->addRangeConstraints(Cs);
-
-  // And check for satisfiability
-  return SMTRefutationMgr->isModelFeasible().isConstrainedFalse();
-}
+  SMTRefutationMgr->addRangeConstraints(Constraints);
 
-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);
-    }
-  }
-}
+  // Add constraints from the unsat core
+  SMTRefutationMgr->addConstraintFromUnsatCore(UnsatCore);
 
-FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor()
-    : Constraints(ConstraintRangeTy::Factory().getEmptyMap()) {}
+  // And check for satisfiability
+  if (SMTRefutationMgr->isModelFeasible().isConstrainedFalse()) {
+    // Mark the bug as invalid
+    BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext());
 
-void FalsePositiveRefutationBRVisitor::finalizeVisitor(
-    BugReporterContext &BRC, const ExplodedNode *EndPathNode, BugReport &BR) {
-  // Collect new constraints
-  VisitNode(EndPathNode, nullptr, BRC, BR);
+    // And save the unsat core
+    std::vector<SMTExprRef> NewUnsatCore = SMTRefutationMgr->getUnsatCore();
 
-  // Create a new refutation manager and check feasibility
-  if (areConstraintsUnfeasible(BRC, Constraints))
-    BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext());
+    UnsatCore.insert(UnsatCore.begin(), NewUnsatCore.begin(),
+                     NewUnsatCore.end());
+  }
 }
 
 std::shared_ptr<PathDiagnosticPiece>
@@ -2416,9 +2410,17 @@
                                             const ExplodedNode *PrevN,
                                             BugReporterContext &BRC,
                                             BugReport &BR) {
+  const ConstraintRangeTy &Cs = N->getState()->get<ConstraintRange>();
+  ConstraintRangeTy::Factory &CF = N->getState()->get_context<ConstraintRange>();
+
   // Collect new constraints
-  addNewConstraints(Constraints, N->getState()->get<ConstraintRange>(),
-                    N->getState()->get_context<ConstraintRange>());
+  // Add 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
@@ -15,6 +15,13 @@
 using namespace clang;
 using namespace ento;
 
+void SMTConstraintManager::addConstraintFromUnsatCore(
+    std::vector<SMTExprRef> &UC) {
+  for (const auto &E : UC) {
+    Solver->addConstraint(E);
+  }
+}
+
 void SMTConstraintManager::addRangeConstraints(ConstraintRangeTy CR) {
   Solver->reset();
 
Index: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -62,6 +62,8 @@
     Z3_set_param_value(Config, "proof", "false");
     // Set timeout to 15000ms = 15s
     Z3_set_param_value(Config, "timeout", "15000");
+    // Enable unsat core generation
+    Z3_set_param_value(Config, "unsat_core", "true");
   }
 
   ~Z3Config() { Z3_del_config(Config); }
@@ -925,6 +927,19 @@
     return ConditionTruthVal();
   }
 
+  std::vector<SMTExprRef> getUnsatCore() override {
+    Z3_ast_vector Core = Z3_solver_get_unsat_core(Context.Context, Solver);
+    unsigned Size = Z3_ast_vector_size(Context.Context, Core);
+
+    std::vector<SMTExprRef> UnsatCore;
+    for (unsigned i = 0; i < Size; i++) {
+      UnsatCore.push_back(std::make_shared<Z3Expr>(
+          Context, Z3_ast_vector_get(Context.Context, Core, i)));
+    }
+
+    return UnsatCore;
+  }
+
   /// Push the current solver state
   void push() override { return Z3_solver_push(Context.Context, Solver); }