Refactor MetaSMTSolver and MetaSMTSolverImpl out of Solver.cpp into

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

This might not be a NFC (non functional change) as there's a good chance this
has broken the MetaSMT build of KLEE. I don't have a build of MetaSMT to hand
and there is no TravisCI build.  At this point because there is no maintainer
for this code I think we should consider removing it as it is going bitrot.

2 files changed, 466 insertions, 462 deletions

diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp
new file mode 100644
index 00000000..8394bbf3
--- /dev/null
+++ b/lib/Solver/MetaSMTSolver.cpp
@@ -0,0 +1,466 @@
+//===-- MetaSMTSolver.cpp -------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifdef SUPPORT_METASMT
+
+#include "MetaSMTBuilder.h"
+#include "klee/Constraints.h"
+#include "klee/Solver.h"
+#include "klee/SolverImpl.h"
+#include "klee/util/Assignment.h"
+#include "klee/util/ExprUtil.h"
+
+#include <metaSMT/DirectSolver_Context.hpp>
+#include <metaSMT/backend/Z3_Backend.hpp>
+#include <metaSMT/backend/Boolector.hpp>
+#include <metaSMT/backend/MiniSAT.hpp>
+#include <metaSMT/support/run_algorithm.hpp>
+#include <metaSMT/API/Stack.hpp>
+#include <metaSMT/API/Group.hpp>
+
+#include <errno.h>
+#include <unistd.h>
+#include <signal.h>
+#include <sys/wait.h>
+#include <sys/ipc.h>
+#include <sys/shm.h>
+
+
+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
+
+namespace klee {
+
+template <typename SolverContext> class MetaSMTSolverImpl : public SolverImpl {
+private:
+  SolverContext _meta_solver;
+  MetaSMTSolver<SolverContext> *_solver;
+  MetaSMTBuilder<SolverContext> *_builder;
+  double _timeout;
+  bool _useForked;
+  SolverRunStatus _runStatusCode;
+
+public:
+  MetaSMTSolverImpl(MetaSMTSolver<SolverContext> *solver, bool useForked,
+                    bool optimizeDivides);
+  virtual ~MetaSMTSolverImpl();
+
+  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 &query,
+                            const std::vector<const Array *> &objects,
+                            std::vector<std::vector<unsigned char> > &values,
+                            bool &hasSolution);
+
+  SolverImpl::SolverRunStatus
+  runAndGetCex(ref<Expr> query_expr, const std::vector<const Array *> &objects,
+               std::vector<std::vector<unsigned char> > &values,
+               bool &hasSolution);
+
+  SolverImpl::SolverRunStatus
+  runAndGetCexForked(const Query &query,
+                     const std::vector<const Array *> &objects,
+                     std::vector<std::vector<unsigned char> > &values,
+                     bool &hasSolution, double timeout);
+
+  SolverRunStatus getOperationStatusCode();
+
+  SolverContext &get_meta_solver() { return (_meta_solver); };
+};
+
+template <typename SolverContext>
+MetaSMTSolverImpl<SolverContext>::MetaSMTSolverImpl(
+    MetaSMTSolver<SolverContext> *solver, bool useForked, bool optimizeDivides)
+    : _solver(solver), _builder(new MetaSMTBuilder<SolverContext>(
+                           _meta_solver, optimizeDivides)),
+      _timeout(0.0), _useForked(useForked) {
+  assert(_solver && "unable to create MetaSMTSolver");
+  assert(_builder && "unable to create MetaSMTBuilder");
+
+  if (_useForked) {
+    shared_memory_id =
+        shmget(IPC_PRIVATE, shared_memory_size, IPC_CREAT | 0700);
+    assert(shared_memory_id >= 0 && "shmget failed");
+    shared_memory_ptr = (unsigned char *)shmat(shared_memory_id, NULL, 0);
+    assert(shared_memory_ptr != (void *)-1 && "shmat failed");
+    shmctl(shared_memory_id, IPC_RMID, NULL);
+  }
+}
+
+template <typename SolverContext>
+MetaSMTSolverImpl<SolverContext>::~MetaSMTSolverImpl() {}
+
+template <typename SolverContext>
+char *MetaSMTSolverImpl<SolverContext>::getConstraintLog(const Query &) {
+  const char *msg = "Not supported";
+  char *buf = new char[strlen(msg) + 1];
+  strcpy(buf, msg);
+  return (buf);
+}
+
+template <typename SolverContext>
+bool MetaSMTSolverImpl<SolverContext>::computeTruth(const Query &query,
+                                                    bool &isValid) {
+
+  bool success = false;
+  std::vector<const Array *> objects;
+  std::vector<std::vector<unsigned char> > values;
+  bool hasSolution;
+
+  if (computeInitialValues(query, objects, values, hasSolution)) {
+    // query.expr is valid iff !query.expr is not satisfiable
+    isValid = !hasSolution;
+    success = true;
+  }
+
+  return (success);
+}
+
+template <typename SolverContext>
+bool MetaSMTSolverImpl<SolverContext>::computeValue(const Query &query,
+                                                    ref<Expr> &result) {
+
+  bool success = false;
+  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)) {
+    assert(hasSolution && "state has invalid constraint set");
+    // Evaluate the expression with the computed assignment.
+    Assignment a(objects, values);
+    result = a.evaluate(query.expr);
+    success = true;
+  }
+
+  return (success);
+}
+
+template <typename SolverContext>
+bool MetaSMTSolverImpl<SolverContext>::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);
+  assert(_builder);
+
+  /*
+   * FIXME push() and pop() work for Z3 but not for Boolector.
+   * If using Z3, use push() and pop() and assert constraints.
+   * If using Boolector, assume constrainsts instead of asserting them.
+   */
+  // push(_meta_solver);
+
+  if (!_useForked) {
+    for (ConstraintManager::const_iterator it = query.constraints.begin(),
+                                           ie = query.constraints.end();
+         it != ie; ++it) {
+      // assertion(_meta_solver, _builder->construct(*it));
+      assumption(_meta_solver, _builder->construct(*it));
+    }
+  }
+
+  ++stats::queries;
+  ++stats::queryCounterexamples;
+
+  bool success = true;
+  if (_useForked) {
+    _runStatusCode =
+        runAndGetCexForked(query, objects, values, hasSolution, _timeout);
+    success = ((SOLVER_RUN_STATUS_SUCCESS_SOLVABLE == _runStatusCode) ||
+               (SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE == _runStatusCode));
+  } else {
+    _runStatusCode = runAndGetCex(query.expr, objects, values, hasSolution);
+    success = true;
+  }
+
+  if (success) {
+    if (hasSolution) {
+      ++stats::queriesInvalid;
+    } else {
+      ++stats::queriesValid;
+    }
+  }
+
+  // pop(_meta_solver);
+
+  return (success);
+}
+
+template <typename SolverContext>
+SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::runAndGetCex(
+    ref<Expr> query_expr, const std::vector<const Array *> &objects,
+    std::vector<std::vector<unsigned char> > &values, bool &hasSolution) {
+
+  // assume the negation of the query
+  assumption(_meta_solver, _builder->construct(Expr::createIsZero(query_expr)));
+  hasSolution = solve(_meta_solver);
+
+  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;
+      assert(array);
+      typename SolverContext::result_type array_exp =
+          _builder->getInitialArray(array);
+
+      std::vector<unsigned char> data;
+      data.reserve(array->size);
+
+      for (unsigned offset = 0; offset < array->size; offset++) {
+        typename SolverContext::result_type elem_exp = evaluate(
+            _meta_solver, metaSMT::logic::Array::select(
+                              array_exp, bvuint(offset, array->getDomain())));
+        unsigned char elem_value = metaSMT::read_value(_meta_solver, elem_exp);
+        data.push_back(elem_value);
+      }
+
+      values.push_back(data);
+    }
+  }
+
+  if (true == hasSolution) {
+    return (SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE);
+  } else {
+    return (SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE);
+  }
+}
+
+static void metaSMTTimeoutHandler(int x) { _exit(52); }
+
+template <typename SolverContext>
+SolverImpl::SolverRunStatus
+MetaSMTSolverImpl<SolverContext>::runAndGetCexForked(
+    const Query &query, 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;
+  }
+  // sum += sizeof(uint64_t);
+  sum += sizeof(stats::queryConstructs);
+  assert(sum < shared_memory_size &&
+         "not enough shared memory for counterexample");
+
+  fflush(stdout);
+  fflush(stderr);
+  int pid = fork();
+  if (pid == -1) {
+    fprintf(stderr, "error: fork failed (for metaSMT)");
+    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, metaSMTTimeoutHandler);
+      ::alarm(std::max(1, (int)timeout));
+    }
+
+    for (ConstraintManager::const_iterator it = query.constraints.begin(),
+                                           ie = query.constraints.end();
+         it != ie; ++it) {
+      assertion(_meta_solver, _builder->construct(*it));
+      // assumption(_meta_solver, _builder->construct(*it));
+    }
+
+    std::vector<std::vector<typename SolverContext::result_type> >
+        aux_arr_exprs;
+    if (UseMetaSMT == METASMT_BACKEND_BOOLECTOR) {
+      for (std::vector<const Array *>::const_iterator it = objects.begin(),
+                                                      ie = objects.end();
+           it != ie; ++it) {
+
+        std::vector<typename SolverContext::result_type> aux_arr;
+        const Array *array = *it;
+        assert(array);
+        typename SolverContext::result_type array_exp =
+            _builder->getInitialArray(array);
+
+        for (unsigned offset = 0; offset < array->size; offset++) {
+          typename SolverContext::result_type elem_exp = evaluate(
+              _meta_solver, metaSMT::logic::Array::select(
+                                array_exp, bvuint(offset, array->getDomain())));
+          aux_arr.push_back(elem_exp);
+        }
+        aux_arr_exprs.push_back(aux_arr);
+      }
+      assert(aux_arr_exprs.size() == objects.size());
+    }
+
+    // assume the negation of the query
+    // can be also asserted instead of assumed as we are in a child process
+    assumption(_meta_solver,
+               _builder->construct(Expr::createIsZero(query.expr)));
+    unsigned res = solve(_meta_solver);
+
+    if (res) {
+
+      if (UseMetaSMT != METASMT_BACKEND_BOOLECTOR) {
+
+        for (std::vector<const Array *>::const_iterator it = objects.begin(),
+                                                        ie = objects.end();
+             it != ie; ++it) {
+
+          const Array *array = *it;
+          assert(array);
+          typename SolverContext::result_type array_exp =
+              _builder->getInitialArray(array);
+
+          for (unsigned offset = 0; offset < array->size; offset++) {
+
+            typename SolverContext::result_type elem_exp =
+                evaluate(_meta_solver,
+                         metaSMT::logic::Array::select(
+                             array_exp, bvuint(offset, array->getDomain())));
+            unsigned char elem_value =
+                metaSMT::read_value(_meta_solver, elem_exp);
+            *pos++ = elem_value;
+          }
+        }
+      } else {
+        typename std::vector<
+            std::vector<typename SolverContext::result_type> >::const_iterator
+            eit = aux_arr_exprs.begin(),
+            eie = aux_arr_exprs.end();
+        for (std::vector<const Array *>::const_iterator it = objects.begin(),
+                                                        ie = objects.end();
+             it != ie, eit != eie; ++it, ++eit) {
+          const Array *array = *it;
+          const std::vector<typename SolverContext::result_type> &arr_exp =
+              *eit;
+          assert(array);
+          assert(array->size == arr_exp.size());
+
+          for (unsigned offset = 0; offset < array->size; offset++) {
+            unsigned char elem_value =
+                metaSMT::read_value(_meta_solver, arr_exp[offset]);
+            *pos++ = elem_value;
+          }
+        }
+      }
+    }
+    assert((uint64_t *)pos);
+    *((uint64_t *)pos) = stats::queryConstructs;
+
+    _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 metaSMT failed");
+      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: metaSMT did not return successfully (status = %d) \n",
+              WTERMSIG(status));
+      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: metaSMT timed out");
+      return (SolverImpl::SOLVER_RUN_STATUS_TIMEOUT);
+    } else {
+      fprintf(stderr, "error: metaSMT did not return a recognized code");
+      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;
+        assert(array);
+        std::vector<unsigned char> &data = values[i++];
+        data.insert(data.begin(), pos, pos + array->size);
+        pos += array->size;
+      }
+    }
+    stats::queryConstructs += (*((uint64_t *)pos) - stats::queryConstructs);
+
+    if (true == hasSolution) {
+      return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE;
+    } else {
+      return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE;
+    }
+  }
+}
+
+template <typename SolverContext>
+SolverImpl::SolverRunStatus
+MetaSMTSolverImpl<SolverContext>::getOperationStatusCode() {
+  return _runStatusCode;
+}
+
+template class MetaSMTSolver<DirectSolver_Context<Boolector> >;
+template class MetaSMTSolver<DirectSolver_Context<Z3_Backend> >;
+template class MetaSMTSolver<DirectSolver_Context<STP_Backend> >;
+
+template <typename SolverContext>
+MetaSMTSolver<SolverContext>::MetaSMTSolver(bool useForked,
+                                            bool optimizeDivides)
+    : Solver(new MetaSMTSolverImpl<SolverContext>(this, useForked,
+                                                  optimizeDivides)) {}
+
+template <typename SolverContext>
+MetaSMTSolver<SolverContext>::~MetaSMTSolver() {}
+
+template <typename SolverContext>
+char *MetaSMTSolver<SolverContext>::getConstraintLog(const Query &query) {
+  return (impl->getConstraintLog(query));
+}
+
+template <typename SolverContext>
+void MetaSMTSolver<SolverContext>::setCoreSolverTimeout(double timeout) {
+  impl->setCoreSolverTimeout(timeout);
+}
+}
+#endif // SUPPORT_METASMT
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index a391ada4..bb4bef69 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -10,7 +10,6 @@
 #include "klee/Solver.h"
 #include "klee/SolverImpl.h"
 
-#include "MetaSMTBuilder.h"
 
 #include "klee/Constraints.h"
 #include "klee/Expr.h"
@@ -29,34 +28,11 @@
 #include <map>
 #include <vector>
 
-#include <errno.h>
-#include <unistd.h>
-#include <signal.h>
-#include <sys/wait.h>
-#include <sys/ipc.h>
-#include <sys/shm.h>
-
 #include "llvm/Support/ErrorHandling.h"
 
 
 using namespace klee;
 
-
-#ifdef SUPPORT_METASMT
-
-#include <metaSMT/DirectSolver_Context.hpp>
-#include <metaSMT/backend/Z3_Backend.hpp>
-#include <metaSMT/backend/Boolector.hpp>
-#include <metaSMT/backend/MiniSAT.hpp>
-#include <metaSMT/support/run_algorithm.hpp>
-#include <metaSMT/API/Stack.hpp>
-#include <metaSMT/API/Group.hpp>
-
-using namespace metaSMT;
-using namespace metaSMT::solver;
-
-#endif /* SUPPORT_METASMT */
-
 const char *Solver::validity_to_str(Validity v) {
   switch (v) {
   default:    return "Unknown";
@@ -264,444 +240,6 @@ std::pair< ref<Expr>, ref<Expr> > Solver::getRange(const Query& query) {
                         ConstantExpr::create(max, width));
 }
 
-/***/
-
-#ifdef SUPPORT_METASMT
-
-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
-
-// ------------------------------------- MetaSMTSolverImpl class declaration ------------------------------
-
-template<typename SolverContext>
-class MetaSMTSolverImpl : public SolverImpl {
-private:
-
-  SolverContext _meta_solver;
-  MetaSMTSolver<SolverContext>  *_solver;  
-  MetaSMTBuilder<SolverContext> *_builder;
-  double _timeout;
-  bool   _useForked;
-  SolverRunStatus _runStatusCode;
-
-public:
-  MetaSMTSolverImpl(MetaSMTSolver<SolverContext> *solver, bool useForked, bool optimizeDivides);  
-  virtual ~MetaSMTSolverImpl();
-  
-  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 &query,
-                            const std::vector<const Array*> &objects,
-                            std::vector< std::vector<unsigned char> > &values,
-                            bool &hasSolution);
-    
-  SolverImpl::SolverRunStatus runAndGetCex(ref<Expr> query_expr,
-                                           const std::vector<const Array*> &objects,
-                                           std::vector< std::vector<unsigned char> > &values,
-                                           bool &hasSolution);
-  
-  SolverImpl::SolverRunStatus runAndGetCexForked(const Query &query,
-                                                 const std::vector<const Array*> &objects,
-                                                 std::vector< std::vector<unsigned char> > &values,
-                                                 bool &hasSolution,
-                                                 double timeout);
-  
-  SolverRunStatus getOperationStatusCode();
-  
-  SolverContext& get_meta_solver() { return(_meta_solver); };
-  
-};
-
-
-// ------------------------------------- MetaSMTSolver methods --------------------------------------------
-
-
-template<typename SolverContext>
-MetaSMTSolver<SolverContext>::MetaSMTSolver(bool useForked, bool optimizeDivides) 
-  : Solver(new MetaSMTSolverImpl<SolverContext>(this, useForked, optimizeDivides))
-{
-   
-}
-
-template<typename SolverContext>
-MetaSMTSolver<SolverContext>::~MetaSMTSolver()
-{
-  
-}
-
-template<typename SolverContext>
-char *MetaSMTSolver<SolverContext>::getConstraintLog(const Query& query) {
-  return(impl->getConstraintLog(query));
-}
-
-template<typename SolverContext>
-void MetaSMTSolver<SolverContext>::setCoreSolverTimeout(double timeout) {
-  impl->setCoreSolverTimeout(timeout);
-}
-
-
-// ------------------------------------- MetaSMTSolverImpl methods ----------------------------------------
-
-
-
-template<typename SolverContext>
-MetaSMTSolverImpl<SolverContext>::MetaSMTSolverImpl(MetaSMTSolver<SolverContext> *solver, bool useForked, bool optimizeDivides)
-  : _solver(solver),    
-    _builder(new MetaSMTBuilder<SolverContext>(_meta_solver, optimizeDivides)),
-    _timeout(0.0),
-    _useForked(useForked)
-{  
-  assert(_solver && "unable to create MetaSMTSolver");
-  assert(_builder && "unable to create MetaSMTBuilder");
-  
-  if (_useForked) {
-      shared_memory_id = shmget(IPC_PRIVATE, shared_memory_size, IPC_CREAT | 0700);
-      assert(shared_memory_id >= 0 && "shmget failed");
-      shared_memory_ptr = (unsigned char*) shmat(shared_memory_id, NULL, 0);
-      assert(shared_memory_ptr != (void*) -1 && "shmat failed");
-      shmctl(shared_memory_id, IPC_RMID, NULL);
-  }
-}
-
-template<typename SolverContext>
-MetaSMTSolverImpl<SolverContext>::~MetaSMTSolverImpl() {
-
-}
-
-template<typename SolverContext>
-char *MetaSMTSolverImpl<SolverContext>::getConstraintLog(const Query&) {
-  const char* msg = "Not supported";
-  char *buf = new char[strlen(msg) + 1];
-  strcpy(buf, msg);
-  return(buf);
-}
-
-template<typename SolverContext>
-bool MetaSMTSolverImpl<SolverContext>::computeTruth(const Query& query, bool &isValid) {  
-
-  bool success = false;
-  std::vector<const Array*> objects;
-  std::vector< std::vector<unsigned char> > values;
-  bool hasSolution;
-
-  if (computeInitialValues(query, objects, values, hasSolution)) {
-      // query.expr is valid iff !query.expr is not satisfiable
-      isValid = !hasSolution;
-      success = true;
-  }
-
-  return(success);
-}
-
-template<typename SolverContext>
-bool MetaSMTSolverImpl<SolverContext>::computeValue(const Query& query, ref<Expr> &result) {
-  
-  bool success = false;
-  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)) {  
-      assert(hasSolution && "state has invalid constraint set");
-      // Evaluate the expression with the computed assignment.
-      Assignment a(objects, values);
-      result = a.evaluate(query.expr);
-      success = true;
-  }
-
-  return(success);
-}
-
-
-template<typename SolverContext>
-bool MetaSMTSolverImpl<SolverContext>::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);
-  assert(_builder);
-
-  /*
-   * FIXME push() and pop() work for Z3 but not for Boolector.
-   * If using Z3, use push() and pop() and assert constraints.
-   * If using Boolector, assume constrainsts instead of asserting them.
-   */
-  //push(_meta_solver);
-
-  if (!_useForked) {
-      for (ConstraintManager::const_iterator it = query.constraints.begin(), ie = query.constraints.end(); it != ie; ++it) {
-          //assertion(_meta_solver, _builder->construct(*it));
-          assumption(_meta_solver, _builder->construct(*it));  
-      }  
-  }  
-    
-  ++stats::queries;
-  ++stats::queryCounterexamples;  
- 
-  bool success = true;
-  if (_useForked) {
-      _runStatusCode = runAndGetCexForked(query, objects, values, hasSolution, _timeout);
-      success = ((SOLVER_RUN_STATUS_SUCCESS_SOLVABLE == _runStatusCode) || (SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE == _runStatusCode));
-  }
-  else {
-      _runStatusCode = runAndGetCex(query.expr, objects, values, hasSolution);
-      success = true;
-  } 
-    
-  if (success) {
-      if (hasSolution) {
-          ++stats::queriesInvalid;
-      }
-      else {
-          ++stats::queriesValid;
-      }
-  }  
-   
-  //pop(_meta_solver); 
-  
-  return(success);
-}
-
-template<typename SolverContext>
-SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::runAndGetCex(ref<Expr> query_expr,
-                                             const std::vector<const Array*> &objects,
-                                             std::vector< std::vector<unsigned char> > &values,
-                                             bool &hasSolution)
-{
-
-  // assume the negation of the query  
-  assumption(_meta_solver, _builder->construct(Expr::createIsZero(query_expr)));  
-  hasSolution = solve(_meta_solver);  
-  
-  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;
-          assert(array);
-          typename SolverContext::result_type array_exp = _builder->getInitialArray(array);
-           
-          std::vector<unsigned char> data;      
-          data.reserve(array->size);       
-           
-          for (unsigned offset = 0; offset < array->size; offset++) {
-              typename SolverContext::result_type elem_exp = evaluate(
-                       _meta_solver,
-                       metaSMT::logic::Array::select(array_exp, bvuint(offset, array->getDomain())));
-              unsigned char elem_value = metaSMT::read_value(_meta_solver, elem_exp);
-              data.push_back(elem_value);
-          }
-                   
-          values.push_back(data);
-      }
-  }
-  
-  if (true == hasSolution) {
-      return(SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE);
-  }
-  else {
-      return(SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE);  
-  }
-}
-
-static void metaSMTTimeoutHandler(int x) {
-  _exit(52);
-}
-
-template<typename SolverContext>
-SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::runAndGetCexForked(const Query &query,
-                                                          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;    
-  }
-  // sum += sizeof(uint64_t);
-  sum += sizeof(stats::queryConstructs);
-  assert(sum < shared_memory_size && "not enough shared memory for counterexample");
-
-  fflush(stdout);
-  fflush(stderr);
-  int pid = fork();
-  if (pid == -1) {
-      fprintf(stderr, "error: fork failed (for metaSMT)");
-      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, metaSMTTimeoutHandler);
-          ::alarm(std::max(1, (int) timeout));
-      }     
-      
-      for (ConstraintManager::const_iterator it = query.constraints.begin(), ie = query.constraints.end(); it != ie; ++it) {      
-          assertion(_meta_solver, _builder->construct(*it));
-          //assumption(_meta_solver, _builder->construct(*it));  
-      } 
-      
-      
-      std::vector< std::vector<typename SolverContext::result_type> > aux_arr_exprs;
-      if (UseMetaSMT == METASMT_BACKEND_BOOLECTOR) {
-          for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) {
-            
-              std::vector<typename SolverContext::result_type> aux_arr;          
-              const Array *array = *it;
-              assert(array);
-              typename SolverContext::result_type array_exp = _builder->getInitialArray(array);
-              
-              for (unsigned offset = 0; offset < array->size; offset++) {
-                  typename SolverContext::result_type elem_exp = evaluate(
-                      _meta_solver,
-                      metaSMT::logic::Array::select(array_exp, bvuint(offset, array->getDomain())));
-                  aux_arr.push_back(elem_exp);
-              }
-              aux_arr_exprs.push_back(aux_arr);
-          }
-          assert(aux_arr_exprs.size() == objects.size());
-      }
-      
-           
-      // assume the negation of the query
-      // can be also asserted instead of assumed as we are in a child process
-      assumption(_meta_solver, _builder->construct(Expr::createIsZero(query.expr)));        
-      unsigned res = solve(_meta_solver);
-
-      if (res) {
-
-          if (UseMetaSMT != METASMT_BACKEND_BOOLECTOR) {
-
-              for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) {
-
-                  const Array *array = *it;
-                  assert(array);
-                  typename SolverContext::result_type array_exp = _builder->getInitialArray(array);      
-
-                  for (unsigned offset = 0; offset < array->size; offset++) {
-
-                      typename SolverContext::result_type elem_exp = evaluate(
-                          _meta_solver,
-                          metaSMT::logic::Array::select(array_exp, bvuint(offset, array->getDomain())));
-                      unsigned char elem_value = metaSMT::read_value(_meta_solver, elem_exp);
-                      *pos++ = elem_value;
-                  }
-              }
-          }
-          else {
-              typename std::vector< std::vector<typename SolverContext::result_type> >::const_iterator eit = aux_arr_exprs.begin(), eie = aux_arr_exprs.end();
-              for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie, eit != eie; ++it, ++eit) {
-                  const Array *array = *it;
-                  const std::vector<typename SolverContext::result_type>& arr_exp = *eit;
-                  assert(array);
-                  assert(array->size == arr_exp.size());
-
-                  for (unsigned offset = 0; offset < array->size; offset++) {
-                      unsigned char elem_value = metaSMT::read_value(_meta_solver, arr_exp[offset]);
-                       *pos++ = elem_value;
-                  }
-              }
-          }
-      }
-      assert((uint64_t*) pos);
-      *((uint64_t*) pos) = stats::queryConstructs;      
-      
-      _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 metaSMT failed");
-          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: metaSMT did not return successfully (status = %d) \n", WTERMSIG(status));
-           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: metaSMT timed out");
-          return(SolverImpl::SOLVER_RUN_STATUS_TIMEOUT);
-      }
-      else {
-          fprintf(stderr, "error: metaSMT did not return a recognized code");
-          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;
-              assert(array);
-              std::vector<unsigned char> &data = values[i++];
-              data.insert(data.begin(), pos, pos + array->size);
-              pos += array->size;
-          }
-      }
-      stats::queryConstructs += (*((uint64_t*) pos) - stats::queryConstructs);      
-
-      if (true == hasSolution) {
-          return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE;
-      }
-      else {
-          return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE;
-      }
-  }
-}
-
-template<typename SolverContext>
-SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::getOperationStatusCode() {
-   return _runStatusCode;
-}
-
-template class MetaSMTSolver< DirectSolver_Context < Boolector> >;
-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();