2 files changed, 15 insertions, 0 deletions
diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index 00e4c962..906309d2 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -42,6 +42,9 @@ namespace klee {
     Query negateExpr() const {
       return withExpr(Expr::createIsZero(expr));
     }
+
+    /// Dump query
+    void dump() const ;
   };
 
   class Solver {
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 3903ab0d..07331fa4 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -1267,4 +1267,16 @@ template class MetaSMTSolver< DirectSolver_Context < Z3_Backend> >;
 template class MetaSMTSolver< DirectSolver_Context < STP_Backend> >;
 
 #endif /* SUPPORT_METASMT */
+///
 
+void Query::dump() const {
+  llvm::errs() << "Constraints [\n";
+  for (ConstraintManager::const_iterator i = constraints.begin();
+      i != constraints.end(); i++) {
+    (*i)->dump();
+  }
+  llvm::errs() << "]\n";
+  llvm::errs() << "Query [\n";
+  expr->dump();
+  llvm::errs() << "]\n";
+}