diff --git a/llvm/include/llvm/Analysis/ConstraintSystem.h b/llvm/include/llvm/Analysis/ConstraintSystem.h
--- a/llvm/include/llvm/Analysis/ConstraintSystem.h
+++ b/llvm/include/llvm/Analysis/ConstraintSystem.h
@@ -10,8 +10,10 @@
 #define LLVM_ANALYSIS_CONSTRAINTSOLVER_H
 
 #include "llvm/ADT/APInt.h"
+#include "llvm/ADT/ArrayRef.h"
 #include "llvm/ADT/SmallVector.h"
 #include <cstdlib>
+#include <string>
 
 namespace llvm {
 
@@ -29,9 +31,15 @@
   // Eliminate constraints from the system using Fourier–Motzkin elimination.
   bool eliminateUsingFM();
 
-  /// Print the constraints in the system.
+  /// Print the constraints in the system, using \p Names as variable names.
+  void dump(ArrayRef<std::string> Names);
+
+  /// Print the constraints in the system, using x0...xn as variable names.
   void dump();
 
+  /// Retuns true if there may be a solution for the constraints in the system.
+  bool mayHaveSolutionImpl();
+
 public:
   void addVariableRow(const SmallVector<int64_t, 8> &R) {
     assert(Constraints.empty() || R.size() == Constraints.back().size());
diff --git a/llvm/lib/Analysis/ConstraintSystem.cpp b/llvm/lib/Analysis/ConstraintSystem.cpp
--- a/llvm/lib/Analysis/ConstraintSystem.cpp
+++ b/llvm/lib/Analysis/ConstraintSystem.cpp
@@ -7,6 +7,8 @@
 //===----------------------------------------------------------------------===//
 
 #include "llvm/Analysis/ConstraintSystem.h"
+#include "llvm/ADT/SmallVector.h"
+#include "llvm/ADT/StringExtras.h"
 #include "llvm/Support/Debug.h"
 
 #include <algorithm>
@@ -15,6 +17,8 @@
 
 using namespace llvm;
 
+#define DEBUG_TYPE "constraint-system"
+
 bool ConstraintSystem::eliminateUsingFM() {
   // Implementation of Fourier–Motzkin elimination, with some tricks from the
   // paper Pugh, William. "The Omega test: a fast and practical integer
@@ -88,7 +92,7 @@
   return true;
 }
 
-bool ConstraintSystem::mayHaveSolution() {
+bool ConstraintSystem::mayHaveSolutionImpl() {
   while (!Constraints.empty() && Constraints[0].size() > 1) {
     if (!eliminateUsingFM())
       return true;
@@ -105,21 +109,41 @@
   return true;
 }
 
-void ConstraintSystem::dump() {
+void ConstraintSystem::dump(ArrayRef<std::string> Names) {
   if (Constraints.empty())
     return;
 
-  std::cout << "c\t";
-  for (unsigned i = 1; i < Constraints[0].size(); i++)
-    std::cout << "x" << i << "\t";
-  std::cout << "\n";
-  for (auto &R : Constraints) {
-    for (auto a : R)
-      std::cout << a << "\t";
-    std::cout << "\n";
+  for (auto &Row : Constraints) {
+    SmallVector<std::string, 16> Parts;
+    for (unsigned i = 1; i < Row.size(); ++i) {
+      if (Row[i] == 0)
+        continue;
+      std::string Coefficient = "";
+      if (Row[i] != 1)
+        Coefficient = std::to_string(Row[i]) + " * ";
+      Parts.push_back(Coefficient + Names[i - 1]);
+    }
+    assert(!Parts.empty());
+    LLVM_DEBUG(dbgs() << join(Parts, std::string(" + "))
+                      << " <= " << std::to_string(Row[0]) << "\n");
   }
 }
 
+void ConstraintSystem::dump() {
+  SmallVector<std::string, 16> Names;
+  for (unsigned i = 1; i < Constraints.back().size(); ++i)
+    Names.push_back("x" + std::to_string(i));
+  LLVM_DEBUG(dbgs() << "---\n");
+  dump(Names);
+}
+
+bool ConstraintSystem::mayHaveSolution() {
+  dump();
+  bool HasSolution = mayHaveSolutionImpl();
+  LLVM_DEBUG(dbgs() << (HasSolution ? "sat" : "unsat") << "\n");
+  return HasSolution;
+}
+
 bool ConstraintSystem::isConditionImplied(SmallVector<int64_t, 8> R) {
   // If there is no solution with the negation of R added to the system, the
   // condition must hold based on the exsisting constraints.
diff --git a/llvm/utils/convert-constraint-log-to-z3.py b/llvm/utils/convert-constraint-log-to-z3.py
new file mode 100755
--- /dev/null
+++ b/llvm/utils/convert-constraint-log-to-z3.py
@@ -0,0 +1,69 @@
+#!/usr/bin/env python
+
+"""
+Helper script to convert the log generated by '-debug-only=constraint-system'
+to a Python script that uses Z3 to verify the decisions using Z3's Python API.
+
+Example usage:
+
+> cat path/to/file.log
+---
+x6 + -1 * x7 <= -1
+x6 + -1 * x7 <= -2
+sat
+
+> ./convert-constraint-log-to-z3.py path/to/file.log > check.py && python ./check.py
+
+> cat check.py
+    from z3 import *
+x3 = Int("x3")
+x1 = Int("x1")
+x2 = Int("x2")
+s = Solver()
+s.add(x1 + -1 * x2 <= 0)
+s.add(x2 + -1 * x3 <= 0)
+s.add(-1 * x1 + x3 <= -1)
+assert(s.check() == unsat)
+print('all checks passed')
+"""
+
+
+import argparse
+import re
+
+
+def main():
+    parser = argparse.ArgumentParser(
+        description='Convert constraint log to script to verify using Z3.')
+    parser.add_argument('log_file', metavar='log', type=str,
+                        help='constraint-system log file')
+    args = parser.parse_args()
+
+    content = ''
+    with open(args.log_file, 'rt') as f:
+        content = f.read()
+
+    groups = content.split('---')
+    var_re = re.compile('x\d+')
+
+    print('from z3 import *')
+    for group in groups:
+        constraints = [g.strip() for g in group.split('\n') if g.strip() != '']
+        variables = set()
+        for c in constraints[:-1]:
+            for m in var_re.finditer(c):
+                variables.add(m.group())
+        if len(variables) == 0:
+            continue
+        for v in variables:
+            print('{} = Int("{}")'.format(v, v))
+        print('s = Solver()')
+        for c in constraints[:-1]:
+            print('s.add({})'.format(c))
+        expected = constraints[-1].strip()
+        print('assert(s.check() == {})'.format(expected))
+    print('print("all checks passed")')
+
+
+if __name__ == '__main__':
+    main()