From ab35f2e9941f250ca3a36454487c5a07b38dfbf6 Mon Sep 17 00:00:00 2001
From: Daniel Dunbar <daniel@zuster.org>
Date: Wed, 10 Jun 2009 05:10:00 +0000
Subject: 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
---
 lib/Solver/PCLoggingSolver.cpp | 13 ++++---------
 1 file changed, 4 insertions(+), 9 deletions(-)

(limited to 'lib/Solver/PCLoggingSolver.cpp')

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, 
-- 
cgit 1.4.1