Index: include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
===================================================================
--- include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -35,6 +35,8 @@
   /// Checks if the added constraints are satisfiable
   virtual clang::ento::ConditionTruthVal isModelFeasible() = 0;
 
+  /// Dumps SMT formula
+  LLVM_DUMP_METHOD virtual void dumpSMTFormula() const = 0;
 }; // end class SMTConstraintManager
 
 } // namespace ento
Index: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -911,6 +911,8 @@
 
   ConditionTruthVal isModelFeasible() override;
 
+  LLVM_DUMP_METHOD void dumpSMTFormula() const override;
+
   //===------------------------------------------------------------------===//
   // Implementation for interface from ConstraintManager.
   //===------------------------------------------------------------------===//
@@ -1299,6 +1301,11 @@
   return ConditionTruthVal();
 }
 
+LLVM_DUMP_METHOD void Z3ConstraintManager::dumpSMTFormula() const
+{
+  Solver.dump();
+}
+
 //===------------------------------------------------------------------===//
 // Internal implementation.
 //===------------------------------------------------------------------===//