From dac2e7ba3f12c839ae7c69aaec6626fcbe05e7e2 Mon Sep 17 00:00:00 2001
From: "Hoang M. Le" <hle@informatik.uni-bremen.de>
Date: Thu, 27 Oct 2016 17:49:47 +0200
Subject: upgrade to boolector-2.2.0 & remove the no longer needed aux array
 vector

---
 .travis/metaSMT.sh           |  9 +++++----
 lib/Solver/MetaSMTSolver.cpp | 48 --------------------------------------------
 2 files changed, 5 insertions(+), 52 deletions(-)

diff --git a/.travis/metaSMT.sh b/.travis/metaSMT.sh
index 7a0d1eef..7195ceb0 100755
--- a/.travis/metaSMT.sh
+++ b/.travis/metaSMT.sh
@@ -11,10 +11,11 @@ git clone git://github.com/agra-uni-bremen/dependencies.git
 # Bootstrap
 export BOOST_ROOT=/usr
 sudo cp dependencies/Z3-2.19/Z3Config.cmake /usr # this is a hack
-./bootstrap.sh -d deps -m RELEASE build -DmetaSMT_ENABLE_TESTS=off --build stp-git-basic --build boolector-1.5.118 --build minisat-git -DZ3_DIR=/usr
-sudo cp deps/boolector-1.5.118/lib/* /usr/lib/ #
-sudo cp deps/minisat-git/lib/* /usr/lib/       # hack
-sudo cp deps/stp-git-basic/lib/* /usr/lib/     #
+./bootstrap.sh -d deps -m RELEASE build -DmetaSMT_ENABLE_TESTS=off --build stp-git-basic --build boolector-2.2.0 --build minisat-git --build lingeling-ayv-86bf266-140429 -DZ3_DIR=/usr
+sudo cp deps/boolector-2.2.0/lib/* /usr/lib/              #
+sudo cp deps/lingeling-ayv-86bf266-140429/lib/* /usr/lib/ #
+sudo cp deps/minisat-git/lib/* /usr/lib/                  # hack
+sudo cp deps/stp-git-basic/lib/* /usr/lib/                #
 
 # Build
 make -C build install
diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp
index 022056fe..2dec1873 100644
--- a/lib/Solver/MetaSMTSolver.cpp
+++ b/lib/Solver/MetaSMTSolver.cpp
@@ -288,30 +288,6 @@ MetaSMTSolverImpl<SolverContext>::runAndGetCexForked(
       // assumption(_meta_solver, _builder->construct(*it));
     }
 
-    std::vector<std::vector<typename SolverContext::result_type> >
-        aux_arr_exprs;
-    if (MetaSMTBackend == 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,
@@ -319,9 +295,6 @@ MetaSMTSolverImpl<SolverContext>::runAndGetCexForked(
     unsigned res = solve(_meta_solver);
 
     if (res) {
-
-      if (MetaSMTBackend != METASMT_BACKEND_BOOLECTOR) {
-
         for (std::vector<const Array *>::const_iterator it = objects.begin(),
                                                         ie = objects.end();
              it != ie; ++it) {
@@ -342,27 +315,6 @@ MetaSMTSolverImpl<SolverContext>::runAndGetCexForked(
             *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;
-- 
cgit 1.4.1