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,15 @@
                            bool IsArg = false,
                            bool EnableNullFPSuppression = true);
 
+/// \return visitor which marks line participating in the trace
+/// with the diagnostic defined in \c diagnosticMarkingRelevantLines.
+std::unique_ptr<BugReporterVisitor> getRelevantLinesVisitor();
+
+/// \return diagnostic string which is emitted for lines marked relevant.
+StringRef diagnosticMarkingRelevantLines() {
+  return "LineNumHint";
+}
+
 const Expr *getDerefExpr(const Stmt *S);
 const Stmt *GetDenomExpr(const ExplodedNode *N);
 const Stmt *GetRetValExpr(const ExplodedNode *N);
Index: include/clang/StaticAnalyzer/Core/BugReporter/PathDiagnostic.h
===================================================================
--- include/clang/StaticAnalyzer/Core/BugReporter/PathDiagnostic.h
+++ include/clang/StaticAnalyzer/Core/BugReporter/PathDiagnostic.h
@@ -101,7 +101,13 @@
 
   void HandlePathDiagnostic(std::unique_ptr<PathDiagnostic> D);
 
-  enum PathGenerationScheme { None, Minimal, Extensive, AlternateExtensive };
+  enum PathGenerationScheme {
+    None, Minimal, Extensive, AlternateExtensive,
+    
+    /// Emits all the diagnostic prescribed by the \p Minimal scheme,
+    /// as well as marking all lines participating in the trace.
+    RelevantLines
+  };
   virtual PathGenerationScheme getGenerationScheme() const { return Minimal; }
   virtual bool supportsLogicalOpControlFlow() const { return false; }
   
Index: lib/Rewrite/HTMLRewrite.cpp
===================================================================
--- lib/Rewrite/HTMLRewrite.cpp
+++ lib/Rewrite/HTMLRewrite.cpp
@@ -210,7 +210,8 @@
   SmallString<256> Str;
   llvm::raw_svector_ostream OS(Str);
 
-  OS << "<tr><td class=\"num\" id=\"LN"
+  OS << "<tr class=\"codeline\" data-linenumber=\""
+     << LineNo << "\">" << "<td class=\"num\" id=\"LN"
      << LineNo << "\">"
      << LineNo << "</td><td class=\"line\">";
 
@@ -263,7 +264,11 @@
   }
 
   // Add one big table tag that surrounds all of the code.
-  RB.InsertTextBefore(0, "<table class=\"code\">\n");
+  std::string s;
+  llvm::raw_string_ostream os(s);
+  os << "<table class=\"code\" id=\"CodeTable" << FID.getHashValue();
+  os << "\">\n";
+  RB.InsertTextBefore(0, os.str());
   RB.InsertTextAfter(FileEnd - FileBeg, "</table>");
 }
 
Index: lib/StaticAnalyzer/Core/BugReporter.cpp
===================================================================
--- lib/StaticAnalyzer/Core/BugReporter.cpp
+++ lib/StaticAnalyzer/Core/BugReporter.cpp
@@ -527,6 +527,29 @@
   return R->isValid();
 }
 
+/// Runs \c RelevantLinesVisitor on the diagnostics.
+/// Does not run any other visitors.
+static bool GenerateRelevantLinesDiagnostic(PathDiagnostic &PD,
+                                   PathDiagnosticBuilder &PDB,
+                                   const ExplodedNode *N) {
+
+  N = N->getFirstPred();
+  if (!N)
+    return true;
+
+  BugReport *R = PDB.getBugReport();
+  auto V = bugreporter::getRelevantLinesVisitor();
+
+  while (const ExplodedNode *Pred = N->getFirstPred()) {
+
+    // Add the generated diagnostics to the path.
+    if (auto p =  V->VisitNode(N, Pred, PDB, *R))
+      PD.getActivePath().push_front(std::move(p));
+    N = Pred;
+  }
+  return R->isValid();
+}
+
 //===----------------------------------------------------------------------===//
 // "Minimal" path diagnostic generation algorithm.
 //===----------------------------------------------------------------------===//
@@ -3180,6 +3203,10 @@
       case PathDiagnosticConsumer::None:
         GenerateVisitorsOnlyPathDiagnostic(PD, PDB, N, visitors);
         break;
+      case PathDiagnosticConsumer::RelevantLines:
+        GenerateMinimalPathDiagnostic(PD, PDB, N, LCM, visitors);
+        GenerateRelevantLinesDiagnostic(PD, PDB, N);
+        break;
       }
 
       // Clean up the visitors we used.
Index: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
===================================================================
--- lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
+++ lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
@@ -25,6 +25,8 @@
 #include "llvm/ADT/SmallString.h"
 #include "llvm/ADT/StringExtras.h"
 #include "llvm/Support/raw_ostream.h"
+#include <unordered_map>
+#include <unordered_set>
 
 using namespace clang;
 using namespace ento;
@@ -1878,3 +1880,64 @@
 
   return std::move(Piece);
 }
+
+/// Mark the lines participating in the counterexample
+class PrinterVisitor final : public BugReporterVisitorImpl<PrinterVisitor> {
+
+  /// File ID followed by a line number.
+  std::unordered_map<unsigned, std::unordered_set<unsigned>> ExecutedLines;
+
+  /// State machine variable.
+  mutable bool DonePrinting = false;
+
+public:
+  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.
+
+      DonePrinting = true;
+      return nullptr;
+    } else if (const Stmt *S = PathDiagnosticLocation::getStmt(N)) {
+
+      // Statement location with an associated SourceLocation object.
+      SourceLocation Loc = S->getSourceRange().getBegin();
+
+      auto p = ExecutedLines.insert(
+          {SM.getFileID(Loc).getHashValue(), std::unordered_set<unsigned>()});
+
+      bool Inserted =
+          p.first->second.insert(SM.getSpellingLineNumber(Loc)).second;
+      if (Inserted)
+        return createDiagnostic(SM, N->getLocationContext(), S);
+    }
+    return nullptr;
+  }
+
+private:
+  /// \return Diagnostic piece related to the statement \p S.
+  std::shared_ptr<PathDiagnosticEventPiece> createDiagnostic(
+      SourceManager &SM, const LocationContext *LC, const Stmt* S) {
+
+    auto L = PathDiagnosticLocation::createBegin(S, SM, LC);
+
+    auto Piece = std::make_shared<PathDiagnosticEventPiece>(L,
+        diagnosticMarkingRelevantLines());
+    Piece->addRange(S->getSourceRange());
+    return Piece;
+  }
+};
+
+std::unique_ptr<BugReporterVisitor> bugreporter::getRelevantLinesVisitor() {
+  return llvm::make_unique<PrinterVisitor>();
+}
Index: lib/StaticAnalyzer/Core/HTMLDiagnostics.cpp
===================================================================
--- lib/StaticAnalyzer/Core/HTMLDiagnostics.cpp
+++ lib/StaticAnalyzer/Core/HTMLDiagnostics.cpp
@@ -19,6 +19,7 @@
 #include "clang/Lex/Preprocessor.h"
 #include "clang/Rewrite/Core/HTMLRewrite.h"
 #include "clang/Rewrite/Core/Rewriter.h"
+#include "clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h"
 #include "clang/StaticAnalyzer/Core/BugReporter/PathDiagnostic.h"
 #include "clang/StaticAnalyzer/Core/CheckerManager.h"
 #include "clang/StaticAnalyzer/Core/IssueHash.h"
@@ -29,6 +30,8 @@
 #include "llvm/Support/Path.h"
 #include "llvm/Support/raw_ostream.h"
 #include <sstream>
+#include <unordered_map>
+#include <unordered_set>
 
 using namespace clang;
 using namespace ento;
@@ -45,6 +48,10 @@
   const Preprocessor &PP;
   AnalyzerOptions &AnalyzerOpts;
   const bool SupportsCrossFileDiagnostics;
+
+  /// Mapping from FileID to a set of contained line numbers.
+  /// Contains all numbers which get considered by the analyzer.
+  std::unordered_map<unsigned, std::unordered_set<unsigned>> ExecutedLines;
 public:
   HTMLDiagnostics(AnalyzerOptions &AnalyzerOpts,
                   const std::string& prefix,
@@ -64,6 +71,10 @@
     return SupportsCrossFileDiagnostics;
   }
 
+  PathGenerationScheme getGenerationScheme() const override {
+    return CounterexampleDump;
+  }
+
   unsigned ProcessMacroPiece(raw_ostream &os,
                              const PathDiagnosticMacroPiece& P,
                              unsigned num);
@@ -91,6 +102,13 @@
   // Rewrite the file specified by FID with HTML formatting.
   void RewriteFile(Rewriter &R, const SourceManager& SMgr,
                    const PathPieces& path, FileID FID);
+
+private:
+  /// \return JavaScript for an option to only show relevant lines.
+  std::string showRelevantLinesJavascript();
+
+  /// \return JSON representation of \c ExecutedLines.
+  std::string serializeExecutedLines();
 };
 
 } // end anonymous namespace
@@ -320,6 +338,13 @@
   return os.str();
 }
 
+static unsigned getNumberOfLineHints(const PathPieces& path) {
+  return std::count_if(path.begin(), path.end(),
+      [](const std::shared_ptr<PathDiagnosticPiece> &p) {
+        return p->getString() == "LineNumHint";
+      });
+}
+
 void HTMLDiagnostics::FinalizeHTML(const PathDiagnostic& D, Rewriter &R,
     const SourceManager& SMgr, const PathPieces& path, FileID FID,
     const FileEntry *Entry, const char *declName) {
@@ -337,6 +362,10 @@
   int LineNumber = path.back()->getLocation().asLocation().getExpansionLineNumber();
   int ColumnNumber = path.back()->getLocation().asLocation().getExpansionColumnNumber();
 
+  // Checkbox to filter the output to the counterexample.
+  R.InsertTextBefore(SMgr.getLocForStartOfFile(FID),
+      showRelevantLinesJavascript());
+
   // Add the name of the file as an <h1> tag.
   {
     std::string s;
@@ -426,7 +455,8 @@
       << ColumnNumber
       << " -->\n";
 
-    os << "\n<!-- BUGPATHLENGTH " << path.size() << " -->\n";
+    os << "\n<!-- BUGPATHLENGTH " << (path.size() - getNumberOfLineHints(path))
+       << " -->\n";
 
     // Mark the end of the tags.
     os << "\n<!-- BUGMETAEND -->\n";
@@ -435,25 +465,107 @@
     R.InsertTextBefore(SMgr.getLocForStartOfFile(FID), os.str());
   }
 
+
   html::AddHeaderFooterInternalBuiltinCSS(R, FID, Entry->getName());
 }
 
+std::string HTMLDiagnostics::showRelevantLinesJavascript() {
+  std::string s;
+  llvm::raw_string_ostream os(s);
+  os << "<script type='text/javascript'>\n";
+  os << serializeExecutedLines();
+
+  os << R"<<<(
+
+var filterCounterexample = function (hide) {
+  for (var file_id in allowed_lines) {
+    var table = document.getElementById("CodeTable" + file_id);
+    if (!table) {
+      continue;
+    }
+    var lines_in_fid = allowed_lines[file_id];
+    var lines = table.getElementsByClassName("codeline");
+    var line;
+    for (var i=0; i<lines.length; i++) {
+        var el = lines[i];
+        var lineNo = el.getAttribute("data-linenumber");
+        if (!lines_in_fid[lineNo]) {
+          if (hide) {
+            el.setAttribute("hidden", "");
+          } else {
+            el.removeAttribute("hidden");
+          }
+        }
+    }
+  }
+}
+
+document.onreadystatechange = function() {
+    document.querySelector('input[name="showCounterexample"]').onchange=
+        function (event) {
+      filterCounterexample(this.checked);
+    };
+};
+</script>
+
+<form>
+    <input type="checkbox" name="showCounterexample" />
+    <label for="showCounterexample">Show only relevant lines</label>
+</form>
+)<<<";
+
+  return os.str();
+}
+
+std::string HTMLDiagnostics::serializeExecutedLines() {
+  std::string s;
+  llvm::raw_string_ostream os(s);
+  os << "var allowed_lines = {";
+
+  for (auto p : ExecutedLines) {
+    os << "\"" << p.first << "\": {";
+    for (unsigned LineNo : p.second) {
+      os << "\"" << LineNo << "\": \"1\"" << ", ";
+    }
+    os << "},\n";
+  }
+
+  os << "};";
+  return os.str();
+}
+
 void HTMLDiagnostics::RewriteFile(Rewriter &R, const SourceManager& SMgr,
     const PathPieces& path, FileID FID) {
   // Process the path.
   // Maintain the counts of extra note pieces separately.
   unsigned TotalPieces = path.size();
+
   unsigned TotalNotePieces =
       std::count_if(path.begin(), path.end(),
                     [](const std::shared_ptr<PathDiagnosticPiece> &p) {
                       return isa<PathDiagnosticNotePiece>(*p);
                     });
+  unsigned TotalLineNoNotes = getNumberOfLineHints(path);
 
-  unsigned TotalRegularPieces = TotalPieces - TotalNotePieces;
+  unsigned TotalRegularPieces = TotalPieces - TotalNotePieces - TotalLineNoNotes;
   unsigned NumRegularPieces = TotalRegularPieces;
   unsigned NumNotePieces = TotalNotePieces;
 
   for (auto I = path.rbegin(), E = path.rend(); I != E; ++I) {
+
+    if ((*I)->getString() == bugreporter::diagnosticMarkingRelevantLines()) {
+
+      // Add marked lines to ExecutedLines dictionary.
+      for (SourceRange Rng : (*I)->getRanges()) {
+        FileID FID = SMgr.getFileID(Rng.getBegin());
+        auto p = ExecutedLines.insert(
+            {FID.getHashValue(), std::unordered_set<unsigned>()});
+        p.first->second.insert(SMgr.getSpellingLineNumber(Rng.getBegin()));
+      }
+      --NumRegularPieces;
+      continue;
+    }
+
     if (isa<PathDiagnosticNotePiece>(I->get())) {
       // This adds diagnostic bubbles, but not navigation.
       // Navigation through note pieces would be added later,