Fix a bug in the logging solver which was printing the expression in a

getInitialValues query in the wrong place.


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

1 files changed, 4 insertions, 9 deletions

diff --git a/lib/Solver/PCLoggingSolver.cpp b/lib/Solver/PCLoggingSolver.cpp
index 03146251..e7128982 100644
--- a/lib/Solver/PCLoggingSolver.cpp
+++ b/lib/Solver/PCLoggingSolver.cpp
@@ -103,17 +103,12 @@ public:
                             const std::vector<const Array*> &objects,
                             std::vector< std::vector<unsigned char> > &values,
                             bool &hasSolution) {
-    const ref<Expr> *evalExprBegin = 0, *evalExprEnd = 0;
-    if (!query.expr->isFalse()) {
-      evalExprBegin = &query.expr;
-      evalExprEnd = evalExprBegin + 1;
-    } 
     if (objects.empty()) {
-      startQuery(query.withFalse(), "InitialValues",
-                 evalExprBegin, evalExprEnd);
+      startQuery(query, "InitialValues",
+                 0, 0);
     } else {
-      startQuery(query.withFalse(), "InitialValues",
-                 evalExprBegin, evalExprEnd,
+      startQuery(query, "InitialValues",
+                 0, 0,
                  &objects[0], &objects[0] + objects.size());
     }
     bool success = solver->impl->computeInitialValues(query, objects,