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/StaticAnalyzer/Core/PathSensitive/SVals.h"
 #include "llvm/ADT/FoldingSet.h"
+#include "llvm/ADT/StringRef.h"
 
 namespace clang {
 class CFGBlock;
@@ -365,6 +366,13 @@
                            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.
+inline 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,16 @@
 
   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,9 +210,9 @@
   SmallString<256> Str;
   llvm::raw_svector_ostream OS(Str);
 
-  OS << "<tr><td class=\"num\" id=\"LN"
-     << LineNo << "\">"
-     << LineNo << "</td><td class=\"line\">";
+  OS << "<tr class=\"codeline\" data-linenumber=\"" << LineNo << "\">"
+     << "<td class=\"num\" id=\"LN" << LineNo << "\">" << LineNo
+     << "</td><td class=\"line\">";
 
   if (B == E) { // Handle empty lines.
     OS << " </td></tr>";
@@ -263,7 +263,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 << "data-fileid=\"" << FID.getHashValue() << "\">\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,95 @@
 
   return std::move(Piece);
 }
+
+/// Mark the lines participating in the counterexample
+class RelevantLinesVisitor final
+    : public BugReporterVisitorImpl<RelevantLinesVisitor> {
+
+  /// File IDs mapped to sets of line numbers.
+  std::unordered_map<unsigned, std::unordered_set<unsigned>> ExecutedLines;
+
+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();
+    const Stmt *S = PathDiagnosticLocation::getStmt(N);
+
+    if (!S) {
+      // We aim to print the prototype of every function we encounter.
+      // The following trick is used: for every visited node without
+      // an attached statement, we instead use the opportunity to return
+      // the diagnostics associated with the function declaration of the
+      // current context.
+      auto FD = dyn_cast<FunctionDecl>(N->getLocationContext()->getDecl());
+      if (FD && insertedAny(SM, FD))
+        return createDiagnostic(SM, FD);
+      return nullptr;
+    }
+
+    SourceLocation Loc = S->getSourceRange().getBegin();
+    SourceLocation ExpansionLoc = SM.getExpansionLoc(Loc);
+    FileID FID = SM.getFileID(ExpansionLoc);
+    unsigned LineNo = SM.getExpansionLineNumber(ExpansionLoc);
+
+    auto p = ExecutedLines.emplace(FID.getHashValue(), /*bucket_count=*/10);
+    if (p.first->second.insert(LineNo).second)
+      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, bugreporter::diagnosticMarkingRelevantLines());
+    Piece->addRange(
+        S->getSourceRange().getBegin(), S->getSourceRange().getBegin());
+    return Piece;
+  }
+
+  /// \return Diagnostic piece related to declaration \p D.
+  std::shared_ptr<PathDiagnosticEventPiece>
+  createDiagnostic(SourceManager &SM, const FunctionDecl *FD) {
+
+    auto L = PathDiagnosticLocation::createBegin(FD, SM);
+    auto Piece = std::make_shared<PathDiagnosticEventPiece>(
+        L, bugreporter::diagnosticMarkingRelevantLines());
+    Piece->addRange(FD->getSourceRange().getBegin(),
+                    FD->getBody()->getSourceRange().getBegin());
+    return Piece;
+  }
+
+  /// \return Whether inserting any of the lines in the prototype of \p FD
+  /// has changed the content of \c ExecutedLines.
+  bool insertedAny(SourceManager &SM, const FunctionDecl *FD) {
+    bool Inserted = false;
+    SourceLocation Start = FD->getSourceRange().getBegin();
+    SourceLocation End = FD->getBody()->getSourceRange().getBegin();
+    unsigned StartLine = SM.getExpansionLineNumber(Start);
+    unsigned EndLine = SM.getExpansionLineNumber(End);
+
+    FileID FID = SM.getFileID(SM.getExpansionLoc(Start));
+    auto p = ExecutedLines.emplace(FID.getHashValue(), /*bucket_count=*/10);
+    for (unsigned Line=StartLine; Line<=EndLine; Line++) {
+      Inserted = Inserted || p.first->second.insert(Line).second;
+    }
+    return Inserted;
+  }
+};
+
+std::unique_ptr<BugReporterVisitor> bugreporter::getRelevantLinesVisitor() {
+  return llvm::make_unique<RelevantLinesVisitor>();
+}
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,11 @@
   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 +72,10 @@
     return SupportsCrossFileDiagnostics;
   }
 
+  PathGenerationScheme getGenerationScheme() const override {
+    return RelevantLines;
+  }
+
   unsigned ProcessMacroPiece(raw_ostream &os,
                              const PathDiagnosticMacroPiece& P,
                              unsigned num);
@@ -91,6 +103,18 @@
   // 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();
+
+  /// Populate \c ExecutedLines with information from diagnostics in \p P.
+  void populateExecutedLines(
+      const PathDiagnosticPiece *P,
+      const SourceManager &SMgr);
 };
 
 } // end anonymous namespace
@@ -320,6 +344,14 @@
   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() ==
+                                bugreporter::diagnosticMarkingRelevantLines();
+                       });
+}
+
 void HTMLDiagnostics::FinalizeHTML(const PathDiagnostic& D, Rewriter &R,
     const SourceManager& SMgr, const PathPieces& path, FileID FID,
     const FileEntry *Entry, const char *declName) {
@@ -337,6 +369,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 +462,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";
@@ -438,23 +475,113 @@
   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) {
+  var tables = document.getElementsByClassName("code");
+  for (var t=0; t<tables.length; t++) {
+    var table = tables[t];
+    var file_id = table.getAttribute("data-fileid");
+    var lines_in_fid = allowed_lines[file_id];
+    if (!lines_in_fid) {
+      lines_in_fid = {};
+    }
+    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");
+          }
+        }
+    }
+  }
+}
+
+window.addEventListener("keydown", function (event) {
+  if (event.defaultPrevented) {
+    return;
+  }
+  if (event.key == "S") {
+    var checked = document.getElementsByName("showCounterexample")[0].checked;
+    filterCounterexample(!checked);
+    document.getElementsByName("showCounterexample")[0].checked = !checked;
+  } else {
+    return;
+  } 
+  event.preventDefault();
+}, true);
+
+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 (shortcut: Shift+S)
+    </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 TotalLineNumNotes = getNumberOfLineHints(path);
 
-  unsigned TotalRegularPieces = TotalPieces - TotalNotePieces;
+  unsigned TotalRegularPieces =
+      TotalPieces - TotalNotePieces - TotalLineNumNotes;
   unsigned NumRegularPieces = TotalRegularPieces;
   unsigned NumNotePieces = TotalNotePieces;
 
   for (auto I = path.rbegin(), E = path.rend(); I != E; ++I) {
-    if (isa<PathDiagnosticNotePiece>(I->get())) {
+
+    if ((*I)->getString() == bugreporter::diagnosticMarkingRelevantLines()) {
+      populateExecutedLines(I->get(), SMgr);
+    } else if (isa<PathDiagnosticNotePiece>(I->get())) {
       // This adds diagnostic bubbles, but not navigation.
       // Navigation through note pieces would be added later,
       // as a separate pass through the piece list.
@@ -479,6 +606,23 @@
   html::HighlightMacros(R, FID, PP);
 }
 
+void HTMLDiagnostics::populateExecutedLines(
+      const PathDiagnosticPiece *P,
+      const SourceManager &SMgr) {
+
+  for (SourceRange Rng : P->getRanges()) {
+    FileID FID = SMgr.getFileID(SMgr.getExpansionLoc(Rng.getBegin()));
+    unsigned StartLine = SMgr.getExpansionLineNumber(Rng.getBegin());
+    unsigned EndLine = SMgr.getExpansionLineNumber(Rng.getEnd());
+
+    auto p = ExecutedLines.emplace(FID.getHashValue(), /*buckets=*/10);
+    for (unsigned Line=StartLine; Line<=EndLine; Line++) {
+      p.first->second.insert(Line);
+    }
+  }
+
+}
+
 void HTMLDiagnostics::HandlePiece(Rewriter& R, FileID BugFileID,
                                   const PathDiagnosticPiece& P,
                                   unsigned num, unsigned max) {