Patch by Tomasz Kuchta adding more detailed information on query failures.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171391 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 11 insertions, 4 deletions

diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index 16a0ea42..1a4663a1 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -8,6 +8,7 @@
 #include "klee/Expr.h"
 #include "klee/ExprBuilder.h"
 #include "klee/Solver.h"
+#include "klee/SolverImpl.h"
 #include "klee/Statistics.h"
 #include "klee/util/ExprPPrinter.h"
 #include "klee/util/ExprVisitor.h"
@@ -93,7 +94,7 @@ namespace {
   UseFastCexSolver("use-fast-cex-solver",
 		   cl::init(false));
   
-  // FIXME: Command line argument duplicated in Executor.cpp of Klee. Different
+  // FIXME: Command line argument modified in Executor.cpp of Klee. Different
   // output file name used.
   cl::opt<bool>
   UseSTPQueryPCLog("use-stp-query-pc-log",
@@ -220,7 +221,9 @@ static bool EvaluateInputAST(const char *Filename,
                           result)) {
           std::cout << (result ? "VALID" : "INVALID");
         } else {
-          std::cout << "FAIL";
+          std::cout << "FAIL (reason: " 
+                    << SolverImpl::getOperationStatusString(S->impl->getOperationStatusCode())
+                    << ")";
         }
       } else if (!QC->Values.empty()) {
         assert(QC->Objects.empty() && 
@@ -236,7 +239,9 @@ static bool EvaluateInputAST(const char *Filename,
           std::cout << "INVALID\n";
           std::cout << "\tExpr 0:\t" << result;
         } else {
-          std::cout << "FAIL";
+          std::cout << "FAIL (reason: " 
+                    << SolverImpl::getOperationStatusString(S->impl->getOperationStatusCode())
+                    << ")";
         }
       } else {
         std::vector< std::vector<unsigned char> > result;
@@ -260,7 +265,9 @@ static bool EvaluateInputAST(const char *Filename,
               std::cout << "\n";
           }
         } else {
-          std::cout << "FAIL";
+          std::cout << "FAIL (reason: " 
+                    << SolverImpl::getOperationStatusString(S->impl->getOperationStatusCode())
+                    << ")";
         }
       }