[NFC] Refactor STPSolver and STPSolverImpl out of Solver.cpp into their

own file ``STPSolver.cpp``. Whilst I'm here also clang-format the
modified code.

2 files changed, 385 insertions, 353 deletions

diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp
new file mode 100644
index 00000000..cb15a23c
--- /dev/null
+++ b/lib/Solver/STPSolver.cpp
@@ -0,0 +1,384 @@
+//===-- STPSolver.cpp -----------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "STPBuilder.h"
+#include "klee/Solver.h"
+#include "klee/SolverImpl.h"
+#include "klee/Constraints.h"
+#include "klee/Internal/Support/ErrorHandling.h"
+#include "klee/util/Assignment.h"
+#include "klee/util/ExprUtil.h"
+
+#include "llvm/Support/CommandLine.h"
+#include "llvm/Support/ErrorHandling.h"
+
+#include <errno.h>
+#include <unistd.h>
+#include <signal.h>
+#include <sys/wait.h>
+#include <sys/ipc.h>
+#include <sys/shm.h>
+
+namespace {
+
+llvm::cl::opt<bool> DebugDumpSTPQueries(
+    "debug-dump-stp-queries", llvm::cl::init(false),
+    llvm::cl::desc("Dump every STP query to stderr (default=off)"));
+
+llvm::cl::opt<bool> IgnoreSolverFailures(
+    "ignore-solver-failures", llvm::cl::init(false),
+    llvm::cl::desc("Ignore any solver failures (default=off)"));
+}
+
+#define vc_bvBoolExtract IAMTHESPAWNOFSATAN
+
+static unsigned char *shared_memory_ptr;
+static int shared_memory_id = 0;
+// Darwin by default has a very small limit on the maximum amount of shared
+// memory, which will quickly be exhausted by KLEE running its tests in
+// parallel. For now, we work around this by just requesting a smaller size --
+// in practice users hitting this limit on counterexample sizes probably already
+// are hitting more serious scalability issues.
+#ifdef __APPLE__
+static const unsigned shared_memory_size = 1 << 16;
+#else
+static const unsigned shared_memory_size = 1 << 20;
+#endif
+
+static void stp_error_handler(const char *err_msg) {
+  fprintf(stderr, "error: STP Error: %s\n", err_msg);
+  abort();
+}
+
+namespace klee {
+
+class STPSolverImpl : public SolverImpl {
+private:
+  VC vc;
+  STPBuilder *builder;
+  double timeout;
+  bool useForkedSTP;
+  SolverRunStatus runStatusCode;
+
+public:
+  STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides = true);
+  ~STPSolverImpl();
+
+  char *getConstraintLog(const Query &);
+  void setCoreSolverTimeout(double _timeout) { timeout = _timeout; }
+
+  bool computeTruth(const Query &, bool &isValid);
+  bool computeValue(const Query &, ref<Expr> &result);
+  bool computeInitialValues(const Query &,
+                            const std::vector<const Array *> &objects,
+                            std::vector<std::vector<unsigned char> > &values,
+                            bool &hasSolution);
+  SolverRunStatus getOperationStatusCode();
+};
+
+STPSolverImpl::STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides)
+    : vc(vc_createValidityChecker()),
+      builder(new STPBuilder(vc, _optimizeDivides)), timeout(0.0),
+      useForkedSTP(_useForkedSTP), runStatusCode(SOLVER_RUN_STATUS_FAILURE) {
+  assert(vc && "unable to create validity checker");
+  assert(builder && "unable to create STPBuilder");
+
+  // In newer versions of STP, a memory management mechanism has been
+  // introduced that automatically invalidates certain C interface
+  // pointers at vc_Destroy time.  This caused double-free errors
+  // due to the ExprHandle destructor also attempting to invalidate
+  // the pointers using vc_DeleteExpr.  By setting EXPRDELETE to 0
+  // we restore the old behaviour.
+  vc_setInterfaceFlags(vc, EXPRDELETE, 0);
+
+  vc_registerErrorHandler(::stp_error_handler);
+
+  if (useForkedSTP) {
+    assert(shared_memory_id == 0 && "shared memory id already allocated");
+    shared_memory_id =
+        shmget(IPC_PRIVATE, shared_memory_size, IPC_CREAT | 0700);
+    if (shared_memory_id < 0)
+      llvm::report_fatal_error("unable to allocate shared memory region");
+    shared_memory_ptr = (unsigned char *)shmat(shared_memory_id, NULL, 0);
+    if (shared_memory_ptr == (void *)-1)
+      llvm::report_fatal_error("unable to attach shared memory region");
+    shmctl(shared_memory_id, IPC_RMID, NULL);
+  }
+}
+
+STPSolverImpl::~STPSolverImpl() {
+  // Detach the memory region.
+  shmdt(shared_memory_ptr);
+  shared_memory_ptr = 0;
+  shared_memory_id = 0;
+
+  delete builder;
+
+  vc_Destroy(vc);
+}
+
+/***/
+
+char *STPSolverImpl::getConstraintLog(const Query &query) {
+  vc_push(vc);
+  for (std::vector<ref<Expr> >::const_iterator it = query.constraints.begin(),
+                                               ie = query.constraints.end();
+       it != ie; ++it)
+    vc_assertFormula(vc, builder->construct(*it));
+  assert(query.expr == ConstantExpr::alloc(0, Expr::Bool) &&
+         "Unexpected expression in query!");
+
+  char *buffer;
+  unsigned long length;
+  vc_printQueryStateToBuffer(vc, builder->getFalse(), &buffer, &length, false);
+  vc_pop(vc);
+
+  return buffer;
+}
+
+bool STPSolverImpl::computeTruth(const Query &query, bool &isValid) {
+  std::vector<const Array *> objects;
+  std::vector<std::vector<unsigned char> > values;
+  bool hasSolution;
+
+  if (!computeInitialValues(query, objects, values, hasSolution))
+    return false;
+
+  isValid = !hasSolution;
+  return true;
+}
+
+bool STPSolverImpl::computeValue(const Query &query, ref<Expr> &result) {
+  std::vector<const Array *> objects;
+  std::vector<std::vector<unsigned char> > values;
+  bool hasSolution;
+
+  // Find the object used in the expression, and compute an assignment
+  // for them.
+  findSymbolicObjects(query.expr, objects);
+  if (!computeInitialValues(query.withFalse(), objects, values, hasSolution))
+    return false;
+  assert(hasSolution && "state has invalid constraint set");
+
+  // Evaluate the expression with the computed assignment.
+  Assignment a(objects, values);
+  result = a.evaluate(query.expr);
+
+  return true;
+}
+
+static SolverImpl::SolverRunStatus
+runAndGetCex(::VC vc, STPBuilder *builder, ::VCExpr q,
+             const std::vector<const Array *> &objects,
+             std::vector<std::vector<unsigned char> > &values,
+             bool &hasSolution) {
+  // XXX I want to be able to timeout here, safely
+  hasSolution = !vc_query(vc, q);
+
+  if (hasSolution) {
+    values.reserve(objects.size());
+    for (std::vector<const Array *>::const_iterator it = objects.begin(),
+                                                    ie = objects.end();
+         it != ie; ++it) {
+      const Array *array = *it;
+      std::vector<unsigned char> data;
+
+      data.reserve(array->size);
+      for (unsigned offset = 0; offset < array->size; offset++) {
+        ExprHandle counter =
+            vc_getCounterExample(vc, builder->getInitialRead(array, offset));
+        unsigned char val = getBVUnsigned(counter);
+        data.push_back(val);
+      }
+
+      values.push_back(data);
+    }
+  }
+
+  if (true == hasSolution) {
+    return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE;
+  } else {
+    return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE;
+  }
+}
+
+static void stpTimeoutHandler(int x) { _exit(52); }
+
+static SolverImpl::SolverRunStatus
+runAndGetCexForked(::VC vc, STPBuilder *builder, ::VCExpr q,
+                   const std::vector<const Array *> &objects,
+                   std::vector<std::vector<unsigned char> > &values,
+                   bool &hasSolution, double timeout) {
+  unsigned char *pos = shared_memory_ptr;
+  unsigned sum = 0;
+  for (std::vector<const Array *>::const_iterator it = objects.begin(),
+                                                  ie = objects.end();
+       it != ie; ++it)
+    sum += (*it)->size;
+  if (sum >= shared_memory_size)
+    llvm::report_fatal_error("not enough shared memory for counterexample");
+
+  fflush(stdout);
+  fflush(stderr);
+  int pid = fork();
+  if (pid == -1) {
+    fprintf(stderr, "ERROR: fork failed (for STP)");
+    if (!IgnoreSolverFailures)
+      exit(1);
+    return SolverImpl::SOLVER_RUN_STATUS_FORK_FAILED;
+  }
+
+  if (pid == 0) {
+    if (timeout) {
+      ::alarm(0); /* Turn off alarm so we can safely set signal handler */
+      ::signal(SIGALRM, stpTimeoutHandler);
+      ::alarm(std::max(1, (int)timeout));
+    }
+    unsigned res = vc_query(vc, q);
+    if (!res) {
+      for (std::vector<const Array *>::const_iterator it = objects.begin(),
+                                                      ie = objects.end();
+           it != ie; ++it) {
+        const Array *array = *it;
+        for (unsigned offset = 0; offset < array->size; offset++) {
+          ExprHandle counter =
+              vc_getCounterExample(vc, builder->getInitialRead(array, offset));
+          *pos++ = getBVUnsigned(counter);
+        }
+      }
+    }
+    _exit(res);
+  } else {
+    int status;
+    pid_t res;
+
+    do {
+      res = waitpid(pid, &status, 0);
+    } while (res < 0 && errno == EINTR);
+
+    if (res < 0) {
+      fprintf(stderr, "ERROR: waitpid() for STP failed");
+      if (!IgnoreSolverFailures)
+        exit(1);
+      return SolverImpl::SOLVER_RUN_STATUS_WAITPID_FAILED;
+    }
+
+    // From timed_run.py: It appears that linux at least will on
+    // "occasion" return a status when the process was terminated by a
+    // signal, so test signal first.
+    if (WIFSIGNALED(status) || !WIFEXITED(status)) {
+      fprintf(stderr, "ERROR: STP did not return successfully.  Most likely "
+                      "you forgot to run 'ulimit -s unlimited'\n");
+      if (!IgnoreSolverFailures) {
+        exit(1);
+      }
+      return SolverImpl::SOLVER_RUN_STATUS_INTERRUPTED;
+    }
+
+    int exitcode = WEXITSTATUS(status);
+    if (exitcode == 0) {
+      hasSolution = true;
+    } else if (exitcode == 1) {
+      hasSolution = false;
+    } else if (exitcode == 52) {
+      fprintf(stderr, "error: STP timed out");
+      // mark that a timeout occurred
+      return SolverImpl::SOLVER_RUN_STATUS_TIMEOUT;
+    } else {
+      fprintf(stderr, "error: STP did not return a recognized code");
+      if (!IgnoreSolverFailures)
+        exit(1);
+      return SolverImpl::SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE;
+    }
+
+    if (hasSolution) {
+      values = std::vector<std::vector<unsigned char> >(objects.size());
+      unsigned i = 0;
+      for (std::vector<const Array *>::const_iterator it = objects.begin(),
+                                                      ie = objects.end();
+           it != ie; ++it) {
+        const Array *array = *it;
+        std::vector<unsigned char> &data = values[i++];
+        data.insert(data.begin(), pos, pos + array->size);
+        pos += array->size;
+      }
+    }
+
+    if (true == hasSolution) {
+      return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE;
+    } else {
+      return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE;
+    }
+  }
+}
+bool STPSolverImpl::computeInitialValues(
+    const Query &query, const std::vector<const Array *> &objects,
+    std::vector<std::vector<unsigned char> > &values, bool &hasSolution) {
+  runStatusCode = SOLVER_RUN_STATUS_FAILURE;
+
+  TimerStatIncrementer t(stats::queryTime);
+
+  vc_push(vc);
+
+  for (ConstraintManager::const_iterator it = query.constraints.begin(),
+                                         ie = query.constraints.end();
+       it != ie; ++it)
+    vc_assertFormula(vc, builder->construct(*it));
+
+  ++stats::queries;
+  ++stats::queryCounterexamples;
+
+  ExprHandle stp_e = builder->construct(query.expr);
+
+  if (DebugDumpSTPQueries) {
+    char *buf;
+    unsigned long len;
+    vc_printQueryStateToBuffer(vc, stp_e, &buf, &len, false);
+    klee_warning("STP query:\n%.*s\n", (unsigned)len, buf);
+  }
+
+  bool success;
+  if (useForkedSTP) {
+    runStatusCode = runAndGetCexForked(vc, builder, stp_e, objects, values,
+                                       hasSolution, timeout);
+    success = ((SOLVER_RUN_STATUS_SUCCESS_SOLVABLE == runStatusCode) ||
+               (SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE == runStatusCode));
+  } else {
+    runStatusCode =
+        runAndGetCex(vc, builder, stp_e, objects, values, hasSolution);
+    success = true;
+  }
+
+  if (success) {
+    if (hasSolution)
+      ++stats::queriesInvalid;
+    else
+      ++stats::queriesValid;
+  }
+
+  vc_pop(vc);
+
+  return success;
+}
+
+SolverImpl::SolverRunStatus STPSolverImpl::getOperationStatusCode() {
+  return runStatusCode;
+}
+
+STPSolver::STPSolver(bool useForkedSTP, bool optimizeDivides)
+    : Solver(new STPSolverImpl(useForkedSTP, optimizeDivides)) {}
+
+char *STPSolver::getConstraintLog(const Query &query) {
+  return impl->getConstraintLog(query);
+}
+
+void STPSolver::setCoreSolverTimeout(double timeout) {
+  impl->setCoreSolverTimeout(timeout);
+}
+}
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 07e8b8a0..a391ada4 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -10,7 +10,6 @@
 #include "klee/Solver.h"
 #include "klee/SolverImpl.h"
 
-#include "STPBuilder.h"
 #include "MetaSMTBuilder.h"
 
 #include "klee/Constraints.h"
@@ -24,7 +23,6 @@
 #include "klee/CommandLine.h"
 #include "klee/SolverStats.h"
 
-#define vc_bvBoolExtract IAMTHESPAWNOFSATAN
 
 #include <cassert>
 #include <cstdio>
@@ -38,18 +36,8 @@
 #include <sys/ipc.h>
 #include <sys/shm.h>
 
-#include "llvm/Support/CommandLine.h"
 #include "llvm/Support/ErrorHandling.h"
 
-llvm::cl::opt<bool>
-IgnoreSolverFailures("ignore-solver-failures",
-                     llvm::cl::init(false),
-                     llvm::cl::desc("Ignore any solver failures (default=off)"));
-
-llvm::cl::opt<bool>
-DebugDumpSTPQueries("debug-dump-stp-queries",
-                     llvm::cl::init(false),
-                     llvm::cl::desc("Dump every STP query to stderr (default=off)"));
 
 using namespace klee;
 
@@ -278,29 +266,7 @@ std::pair< ref<Expr>, ref<Expr> > Solver::getRange(const Query& query) {
 
 /***/
 
-class STPSolverImpl : public SolverImpl {
-private:
-  VC vc;
-  STPBuilder *builder;
-  double timeout;
-  bool useForkedSTP;
-  SolverRunStatus runStatusCode;
-
-public:
-  STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides = true);
-  ~STPSolverImpl();
-  
-  char *getConstraintLog(const Query&);
-  void setCoreSolverTimeout(double _timeout) { timeout = _timeout; }
-
-  bool computeTruth(const Query&, bool &isValid);
-  bool computeValue(const Query&, ref<Expr> &result);
-  bool computeInitialValues(const Query&,
-                            const std::vector<const Array*> &objects,
-                            std::vector< std::vector<unsigned char> > &values,
-                            bool &hasSolution);
-  SolverRunStatus getOperationStatusCode();
-};
+#ifdef SUPPORT_METASMT
 
 static unsigned char *shared_memory_ptr;
 static int shared_memory_id = 0;
@@ -315,324 +281,6 @@ static const unsigned shared_memory_size = 1<<16;
 static const unsigned shared_memory_size = 1<<20;
 #endif
 
-static void stp_error_handler(const char* err_msg) {
-  fprintf(stderr, "error: STP Error: %s\n", err_msg);
-  abort();
-}
-
-STPSolverImpl::STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides)
-  : vc(vc_createValidityChecker()),
-    builder(new STPBuilder(vc, _optimizeDivides)),
-    timeout(0.0),
-    useForkedSTP(_useForkedSTP),
-    runStatusCode(SOLVER_RUN_STATUS_FAILURE)
-{
-  assert(vc && "unable to create validity checker");
-  assert(builder && "unable to create STPBuilder");
-
-  // In newer versions of STP, a memory management mechanism has been
-  // introduced that automatically invalidates certain C interface
-  // pointers at vc_Destroy time.  This caused double-free errors
-  // due to the ExprHandle destructor also attempting to invalidate
-  // the pointers using vc_DeleteExpr.  By setting EXPRDELETE to 0
-  // we restore the old behaviour.
-  vc_setInterfaceFlags(vc, EXPRDELETE, 0);
-
-  vc_registerErrorHandler(::stp_error_handler);
-
-  if (useForkedSTP) {
-    assert(shared_memory_id == 0 && "shared memory id already allocated");
-    shared_memory_id = shmget(IPC_PRIVATE, shared_memory_size, IPC_CREAT | 0700);
-    if (shared_memory_id < 0)
-      llvm::report_fatal_error("unable to allocate shared memory region");
-    shared_memory_ptr = (unsigned char*) shmat(shared_memory_id, NULL, 0);
-    if (shared_memory_ptr == (void*)-1)
-      llvm::report_fatal_error("unable to attach shared memory region");
-    shmctl(shared_memory_id, IPC_RMID, NULL);
-  }
-}
-
-STPSolverImpl::~STPSolverImpl() {
-  // Detach the memory region.
-  shmdt(shared_memory_ptr);
-  shared_memory_ptr = 0;
-  shared_memory_id = 0;
-
-  delete builder;
-
-  vc_Destroy(vc);
-}
-
-/***/
-
-STPSolver::STPSolver(bool useForkedSTP, bool optimizeDivides)
-  : Solver(new STPSolverImpl(useForkedSTP, optimizeDivides))
-{
-}
-
-char *STPSolver::getConstraintLog(const Query &query) {
-  return impl->getConstraintLog(query);  
-}
-
-void STPSolver::setCoreSolverTimeout(double timeout) {
-    impl->setCoreSolverTimeout(timeout);
-}
-
-/***/
-
-char *STPSolverImpl::getConstraintLog(const Query &query) {
-  vc_push(vc);
-  for (std::vector< ref<Expr> >::const_iterator it = query.constraints.begin(), 
-         ie = query.constraints.end(); it != ie; ++it)
-    vc_assertFormula(vc, builder->construct(*it));
-  assert(query.expr == ConstantExpr::alloc(0, Expr::Bool) &&
-         "Unexpected expression in query!");
-
-  char *buffer;
-  unsigned long length;
-  vc_printQueryStateToBuffer(vc, builder->getFalse(), 
-                             &buffer, &length, false);
-  vc_pop(vc);
-
-  return buffer;
-}
-
-bool STPSolverImpl::computeTruth(const Query& query,
-                                 bool &isValid) {
-  std::vector<const Array*> objects;
-  std::vector< std::vector<unsigned char> > values;
-  bool hasSolution;
-
-  if (!computeInitialValues(query, objects, values, hasSolution))
-    return false;
-
-  isValid = !hasSolution;
-  return true;
-}
-
-bool STPSolverImpl::computeValue(const Query& query,
-                                 ref<Expr> &result) {
-  std::vector<const Array*> objects;
-  std::vector< std::vector<unsigned char> > values;
-  bool hasSolution;
-
-  // Find the object used in the expression, and compute an assignment
-  // for them.
-  findSymbolicObjects(query.expr, objects);
-  if (!computeInitialValues(query.withFalse(), objects, values, hasSolution))
-    return false;
-  assert(hasSolution && "state has invalid constraint set");
-  
-  // Evaluate the expression with the computed assignment.
-  Assignment a(objects, values);
-  result = a.evaluate(query.expr);
-
-  return true;
-}
-
-static SolverImpl::SolverRunStatus runAndGetCex(::VC vc, STPBuilder *builder, ::VCExpr q,
-                                                const std::vector<const Array*> &objects,
-                                                std::vector< std::vector<unsigned char> > &values,
-                                                bool &hasSolution) {
-  // XXX I want to be able to timeout here, safely
-  hasSolution = !vc_query(vc, q);
-
-  if (hasSolution) {
-    values.reserve(objects.size());
-    for (std::vector<const Array*>::const_iterator
-           it = objects.begin(), ie = objects.end(); it != ie; ++it) {
-      const Array *array = *it;
-      std::vector<unsigned char> data;
-      
-      data.reserve(array->size);
-      for (unsigned offset = 0; offset < array->size; offset++) {
-        ExprHandle counter = 
-          vc_getCounterExample(vc, builder->getInitialRead(array, offset));
-        unsigned char val = getBVUnsigned(counter);
-        data.push_back(val);
-      }
-      
-      values.push_back(data);
-    }
-  }
-  
-  if (true == hasSolution) {
-    return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE;
-  }
-  else {
-    return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE;  
-  }
-}
-
-static void stpTimeoutHandler(int x) {
-  _exit(52);
-}
-
-static SolverImpl::SolverRunStatus runAndGetCexForked(::VC vc, 
-                                                      STPBuilder *builder,
-                                                      ::VCExpr q,
-                                                      const std::vector<const Array*> &objects,
-                                                      std::vector< std::vector<unsigned char> >
-                                                      &values,
-                                                      bool &hasSolution,
-                                                      double timeout) {
-  unsigned char *pos = shared_memory_ptr;
-  unsigned sum = 0;
-  for (std::vector<const Array*>::const_iterator
-         it = objects.begin(), ie = objects.end(); it != ie; ++it)
-    sum += (*it)->size;
-  if (sum >= shared_memory_size)
-    llvm::report_fatal_error("not enough shared memory for counterexample");
-
-  fflush(stdout);
-  fflush(stderr);
-  int pid = fork();
-  if (pid==-1) {
-    fprintf(stderr, "ERROR: fork failed (for STP)");
-    if (!IgnoreSolverFailures) 
-      exit(1);
-    return SolverImpl::SOLVER_RUN_STATUS_FORK_FAILED;
-  }
-
-  if (pid == 0) {
-    if (timeout) {      
-      ::alarm(0); /* Turn off alarm so we can safely set signal handler */
-      ::signal(SIGALRM, stpTimeoutHandler);
-      ::alarm(std::max(1, (int)timeout));
-    }    
-    unsigned res = vc_query(vc, q);
-    if (!res) {
-      for (std::vector<const Array*>::const_iterator
-             it = objects.begin(), ie = objects.end(); it != ie; ++it) {
-        const Array *array = *it;
-        for (unsigned offset = 0; offset < array->size; offset++) {
-          ExprHandle counter = 
-            vc_getCounterExample(vc, builder->getInitialRead(array, offset));
-          *pos++ = getBVUnsigned(counter);
-        }
-      }
-    }
-    _exit(res);
-  } else {
-    int status;
-    pid_t res;
-
-    do {
-      res = waitpid(pid, &status, 0);
-    } while (res < 0 && errno == EINTR);
-    
-    if (res < 0) {
-      fprintf(stderr, "ERROR: waitpid() for STP failed");
-      if (!IgnoreSolverFailures) 
-	exit(1);
-      return SolverImpl::SOLVER_RUN_STATUS_WAITPID_FAILED;
-    }
-    
-    // From timed_run.py: It appears that linux at least will on
-    // "occasion" return a status when the process was terminated by a
-    // signal, so test signal first.
-    if (WIFSIGNALED(status) || !WIFEXITED(status)) {
-      fprintf(stderr, "ERROR: STP did not return successfully.  Most likely you forgot to run 'ulimit -s unlimited'\n");
-      if (!IgnoreSolverFailures)  {
-	exit(1);
-      }
-      return SolverImpl::SOLVER_RUN_STATUS_INTERRUPTED;
-    }
-
-    int exitcode = WEXITSTATUS(status);
-    if (exitcode==0) {
-      hasSolution = true;
-    } else if (exitcode==1) {
-      hasSolution = false;
-    } else if (exitcode==52) {
-      fprintf(stderr, "error: STP timed out");
-      // mark that a timeout occurred
-      return SolverImpl::SOLVER_RUN_STATUS_TIMEOUT;
-    } else {
-      fprintf(stderr, "error: STP did not return a recognized code");
-      if (!IgnoreSolverFailures) 
-	exit(1);
-      return SolverImpl::SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE;
-    }
-    
-    if (hasSolution) {
-      values = std::vector< std::vector<unsigned char> >(objects.size());
-      unsigned i=0;
-      for (std::vector<const Array*>::const_iterator
-             it = objects.begin(), ie = objects.end(); it != ie; ++it) {
-        const Array *array = *it;
-        std::vector<unsigned char> &data = values[i++];
-        data.insert(data.begin(), pos, pos + array->size);
-        pos += array->size;
-      }
-    }
-    
-    if (true == hasSolution) {
-      return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE;
-    }
-    else {        
-      return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE;
-    }
-  }
-}
-bool
-STPSolverImpl::computeInitialValues(const Query &query,
-                                    const std::vector<const Array*> 
-                                      &objects,
-                                    std::vector< std::vector<unsigned char> > 
-                                      &values,
-                                    bool &hasSolution) {
-  runStatusCode =  SOLVER_RUN_STATUS_FAILURE; 
-    
-  TimerStatIncrementer t(stats::queryTime);
-
-  vc_push(vc);
-
-  for (ConstraintManager::const_iterator it = query.constraints.begin(), 
-         ie = query.constraints.end(); it != ie; ++it)
-    vc_assertFormula(vc, builder->construct(*it));
-  
-  ++stats::queries;
-  ++stats::queryCounterexamples;
-
-  ExprHandle stp_e = builder->construct(query.expr);
-     
-  if (DebugDumpSTPQueries) {
-    char *buf;
-    unsigned long len;
-    vc_printQueryStateToBuffer(vc, stp_e, &buf, &len, false);
-    klee_warning("STP query:\n%.*s\n", (unsigned) len, buf);
-  }
-
-  bool success;
-  if (useForkedSTP) {
-    runStatusCode = runAndGetCexForked(vc, builder, stp_e, objects, values, 
-                                       hasSolution, timeout);
-    success = ((SOLVER_RUN_STATUS_SUCCESS_SOLVABLE == runStatusCode) ||
-               (SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE == runStatusCode));    
-  } else {
-    runStatusCode = runAndGetCex(vc, builder, stp_e, objects, values, hasSolution);    
-    success = true;
-  }
-  
-  if (success) {
-    if (hasSolution)
-      ++stats::queriesInvalid;
-    else
-      ++stats::queriesValid;
-  }
-  
-  vc_pop(vc);
-  
-  return success;
-}
-
-SolverImpl::SolverRunStatus STPSolverImpl::getOperationStatusCode() {
-   return runStatusCode;
-}
-
-#ifdef SUPPORT_METASMT
-
 // ------------------------------------- MetaSMTSolverImpl class declaration ------------------------------
 
 template<typename SolverContext>