From e4d747935909c34b3f8d20938af7c01b7812db74 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Thu, 14 Jan 2016 10:07:35 +0000
Subject: MetaSMT build fixes.

---
 lib/Solver/CoreSolver.cpp    |  3 ++-
 lib/Solver/MetaSMTSolver.cpp | 11 ++++++-----
 2 files changed, 8 insertions(+), 6 deletions(-)

(limited to 'lib/Solver')

diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp
index 0d451f27..9248f3d3 100644
--- a/lib/Solver/CoreSolver.cpp
+++ b/lib/Solver/CoreSolver.cpp
@@ -32,10 +32,11 @@
 #undef Type
 #undef STP
 
+using namespace klee;
 using namespace metaSMT;
 using namespace metaSMT::solver;
 
-static Solver *handleMetaSMT() {
+static klee::Solver *handleMetaSMT() {
   Solver *coreSolver = NULL;
   std::string backend;
   switch (MetaSMTBackend) {
diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp
index 971ef371..c4f6a5d0 100644
--- a/lib/Solver/MetaSMTSolver.cpp
+++ b/lib/Solver/MetaSMTSolver.cpp
@@ -297,7 +297,7 @@ MetaSMTSolverImpl<SolverContext>::runAndGetCexForked(
 
     std::vector<std::vector<typename SolverContext::result_type> >
         aux_arr_exprs;
-    if (UseMetaSMT == METASMT_BACKEND_BOOLECTOR) {
+    if (MetaSMTBackend == METASMT_BACKEND_BOOLECTOR) {
       for (std::vector<const Array *>::const_iterator it = objects.begin(),
                                                       ie = objects.end();
            it != ie; ++it) {
@@ -327,7 +327,7 @@ MetaSMTSolverImpl<SolverContext>::runAndGetCexForked(
 
     if (res) {
 
-      if (UseMetaSMT != METASMT_BACKEND_BOOLECTOR) {
+      if (MetaSMTBackend != METASMT_BACKEND_BOOLECTOR) {
 
         for (std::vector<const Array *>::const_iterator it = objects.begin(),
                                                         ie = objects.end();
@@ -440,9 +440,6 @@ 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,
@@ -462,5 +459,9 @@ template <typename SolverContext>
 void MetaSMTSolver<SolverContext>::setCoreSolverTimeout(double timeout) {
   impl->setCoreSolverTimeout(timeout);
 }
+
+template class MetaSMTSolver<DirectSolver_Context<metaSMT::solver::Boolector> >;
+template class MetaSMTSolver<DirectSolver_Context<metaSMT::solver::Z3_Backend> >;
+template class MetaSMTSolver<DirectSolver_Context<metaSMT::solver::STP_Backend> >;
 }
 #endif // ENABLE_METASMT
-- 
cgit 1.4.1