Index: include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
===================================================================
--- include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
+++ include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
@@ -523,6 +523,9 @@
   /// in the CFG.
   bool shouldConditionalizeStaticInitializers();
 
+  /// \return true if counterexamples should be dumped to stderr.
+  bool shouldDumpCounterexample();
+
   // Returns the size of the functions (in basic blocks), which should be
   // considered to be small enough to always inline.
   //
Index: include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
===================================================================
--- include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
+++ include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
@@ -365,6 +365,9 @@
                            bool IsArg = false,
                            bool EnableNullFPSuppression = true);
 
+/// Print the counterexample as a C file.
+void printCounterexample(BugReport &report);
+
 const Expr *getDerefExpr(const Stmt *S);
 const Stmt *GetDenomExpr(const ExplodedNode *N);
 const Stmt *GetRetValExpr(const ExplodedNode *N);
Index: lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
===================================================================
--- lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
+++ lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
@@ -368,6 +368,10 @@
   return getBooleanOption("cfg-conditional-static-initializers", true);
 }
 
+bool AnalyzerOptions::shouldDumpCounterexample() {
+  return getBooleanOption("dump-counterexample", false);
+}
+
 bool AnalyzerOptions::shouldInlineLambdas() {
   if (!InlineLambdas.hasValue())
     InlineLambdas = getBooleanOption("inline-lambdas", /*Default=*/true);
Index: lib/StaticAnalyzer/Core/BugReporter.cpp
===================================================================
--- lib/StaticAnalyzer/Core/BugReporter.cpp
+++ lib/StaticAnalyzer/Core/BugReporter.cpp
@@ -3125,6 +3125,9 @@
     R->addVisitor(llvm::make_unique<LikelyFalsePositiveSuppressionBRVisitor>());
     R->addVisitor(llvm::make_unique<CXXSelfAssignmentBRVisitor>());
 
+    if (getAnalyzerOptions().shouldDumpCounterexample())
+      bugreporter::printCounterexample(*R);
+
     BugReport::VisitorList visitors;
     unsigned origReportConfigToken, finalReportConfigToken;
     LocationContextMap LCM;
Index: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
===================================================================
--- lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
+++ lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
@@ -11,6 +11,8 @@
 //  enhance the diagnostics reported for a bug.
 //
 //===----------------------------------------------------------------------===//
+#include <cmath>
+#include <string.h>
 #include "clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h"
 #include "clang/AST/Expr.h"
 #include "clang/AST/ExprObjC.h"
@@ -24,6 +26,7 @@
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "llvm/ADT/SmallString.h"
 #include "llvm/ADT/StringExtras.h"
+#include "llvm/ADT/SetVector.h"
 #include "llvm/Support/raw_ostream.h"
 
 using namespace clang;
@@ -1878,3 +1881,155 @@
 
   return std::move(Piece);
 }
+
+/// Export the counterexample to C.
+class PrinterVisitor final : public BugReporterVisitorImpl<PrinterVisitor> {
+
+  /// File ID followed by a line number.
+  llvm::SetVector<std::pair<FileID, unsigned>> VisitedLines;
+
+  /// Output stream to write into.
+  raw_ostream &Ostream;
+
+  /// State machine variables.
+  mutable bool DonePrinting = false;
+
+  /// Max number of chars used to display the filename.
+  static const unsigned MAX_FILENAME_MARGIN = 80;
+  static const unsigned MARGIN_SEP_LEN = 1; 
+  static constexpr const char * const REPORT_SEPARATOR =
+      "/* ============================================================== */\n";
+
+public:
+  PrinterVisitor(raw_ostream &Ostream) : Ostream(Ostream) {}
+
+  PrinterVisitor() = delete;
+
+  void Profile(llvm::FoldingSetNodeID &ID) const override {
+    static int Tag = 0;
+    ID.AddPointer(&Tag);
+  }
+
+  std::shared_ptr<PathDiagnosticPiece> VisitNode(const ExplodedNode *N,
+                                                 const ExplodedNode *PrevN,
+                                                 BugReporterContext &BRC,
+                                                 BugReport &BR) override {
+    SourceManager &SM = BRC.getSourceManager();
+
+    if (DonePrinting) { // Printing was done, do nothing.
+      return nullptr;
+    } else if (!PrevN->getFirstPred()) { // Finished report, do printing.
+
+      // Went through the entire bug report, now print the lines in reverse
+      // order.
+      bool Status = doPrinting(SM);
+      if (!Status)
+        Ostream << "Error while printing\n";
+      Ostream << REPORT_SEPARATOR;
+      DonePrinting = true;
+      return nullptr;
+    } else if (const Stmt *S = PathDiagnosticLocation::getStmt(N)) {
+
+      // Statement location with an associated SourceLocation object.
+      SourceLocation Loc = S->getSourceRange().getBegin();
+
+      // FIXME: might be necessary to insert the spelling location as well.
+      insertLoc(SM, SM.getExpansionLoc(Loc));
+    }
+    return nullptr;
+  }
+
+private:
+  /// Print locations serialized to \c VisitedLines.
+  bool doPrinting(SourceManager &SM) {
+    unsigned Margin = calculateMargin(SM);
+    for (auto It = VisitedLines.rbegin(),
+        ItEnd = VisitedLines.rend();
+        It != ItEnd; ++It) {
+      FileID FID = It->first;
+      unsigned LineNo = It->second;
+      bool Status = printLine(SM, FID, LineNo, Margin);
+      if (!Status)
+        return false;
+    }
+    return true;
+  }
+
+  /// Print line \p LineNo from file \p FID, with left margin \p Margin.
+  /// \return \c true on success, \c false on failure.
+  bool printLine(SourceManager &SM, FileID FID,
+                 unsigned LineNo, unsigned Margin) {
+    SourceLocation Location = SM.translateLineCol(FID, LineNo, 1);
+    unsigned Offset = SM.getFileOffset(Location);
+
+    // Print location first.
+    int Status = printLocation(SM, Location, Margin);
+    if (!Status)
+      return false;
+
+    bool Invalid = false;
+    const char *BufferStart = SM.getBufferData(FID, &Invalid).data();
+    if (Invalid)
+      return false;
+
+    unsigned FileEndOffset = SM.getFileOffset(SM.getLocForEndOfFile(FID));
+    for (unsigned i=Offset; BufferStart[i] != '\n' && i < FileEndOffset; ++i)
+      Ostream << BufferStart[i];
+
+    Ostream << "\n";
+    return true;
+  }
+
+  /// Print location in left margin.
+  bool printLocation(SourceManager &SM, SourceLocation Loc, unsigned Margin) {
+    Loc = SM.getExpansionLoc(Loc);
+    PresumedLoc PLoc = SM.getPresumedLoc(Loc);
+    if (PLoc.isInvalid())
+      return false;
+
+    uint64_t SavedPos = Ostream.tell();
+    Ostream << PLoc.getFilename() << ":" << PLoc.getLine();
+    uint64_t Delta = Ostream.tell() - SavedPos;
+    assert(Margin >= Delta);
+    for (unsigned i=Delta; i<Margin; i++)
+      Ostream << " ";
+    Ostream << "|";
+
+    return true;
+  }
+
+  /// Serialize source location \p Loc to \c visitedLines.
+  void insertLoc(SourceManager &SM, SourceLocation Loc) {
+    VisitedLines.insert(
+        std::make_pair(SM.getFileID(Loc), SM.getSpellingLineNumber(Loc)));
+  }
+
+  /// \return smallest margin required to fit all filenames present
+  /// in the counterexample.
+  unsigned calculateMargin(SourceManager &SM) {
+    unsigned Out = 0;
+    for (auto Pair : VisitedLines) {
+      FileID FID = Pair.first;
+      unsigned LineNo = Pair.second;
+      SourceLocation Loc = SM.translateLineCol(FID, LineNo, 1);
+      Loc = SM.getExpansionLoc(Loc);
+      PresumedLoc PLoc = SM.getPresumedLoc(Loc);
+      if (PLoc.isInvalid())
+        continue;
+
+      // Take logarithm to figure out number of chars required.
+      long LineMargin = 1 + std::lround(floor(log10(PLoc.getLine())));
+      size_t FilenameMargin = strnlen(PLoc.getFilename(), MAX_FILENAME_MARGIN);
+      assert(LineMargin > 0);
+      unsigned RequiredMargin = FilenameMargin
+          + LineMargin + MARGIN_SEP_LEN;
+      if (RequiredMargin > Out)
+        Out = RequiredMargin;
+    }
+    return Out;
+  }
+};
+
+void bugreporter::printCounterexample(BugReport &report) {
+  report.addVisitor(llvm::make_unique<PrinterVisitor>(llvm::errs()));
+}