Merge pull request #409 from hoangmle/fix_metaSMT

Add metaSMT to Travis CI, fix metaSMTBuilder to pass all tests

14 files changed, 1205 insertions, 1031 deletions

diff --git a/.travis.yml b/.travis.yml
index 158f8f76..42072095 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -19,14 +19,22 @@ env:
 
     # Check the matrix of:
     #   LLVM  : {2.9, 3.4}
-    #   SOLVERS : {Z3, STP, STP:Z3}
+    #   SOLVERS : {Z3, STP, STP:Z3, metaSMT}
     #   STP_VERSION   : {2.1.0, master}
+    #   METASMT_DEFAULT : {btor, stp, z3}
     #   UCLIBC: {0, klee_uclibc_v1.0.0, klee_0_9_29} // Note ``0`` means disabled
     # with Asserts enabled.
 
     # COVERAGE set indicated that coverage data should be uplaoded to the server, only ONE job should have COVERAGE set
 
     matrix:
+    # Test experimental metaSMT support
+    - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_DEFAULT=btor KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
+    - LLVM_VERSION=2.9 SOLVERS=metaSMT METASMT_DEFAULT=btor KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
+    - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_DEFAULT=stp  KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
+    - LLVM_VERSION=2.9 SOLVERS=metaSMT METASMT_DEFAULT=stp  KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
+    - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_DEFAULT=z3   KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
+    - LLVM_VERSION=2.9 SOLVERS=metaSMT METASMT_DEFAULT=z3   KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
     # Test experimental Z3 support
     - LLVM_VERSION=3.4 SOLVERS=Z3 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
     - LLVM_VERSION=2.9 SOLVERS=Z3 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
@@ -65,6 +73,8 @@ before_install:
     # Set up the locations to get various packages from
     # We assume the Travis image uses Ubuntu 12.04 LTS
     ###########################################################################
+    # Needed for Boost
+    - sudo add-apt-repository -y ppa:boost-latest
     # Needed for CMake
     - sudo add-apt-repository -y ppa:kalakris/cmake
     # Needed for LLVM
@@ -105,4 +115,4 @@ script:
     - ${KLEE_SRC}/.travis/testing-utils.sh
     - cd ../
     # Build KLEE
-    - ${KLEE_SRC}/.travis/klee.sh
+    - travis_wait 30 ${KLEE_SRC}/.travis/klee.sh
diff --git a/.travis/klee.sh b/.travis/klee.sh
index 296e1c83..98dbbc0d 100755
--- a/.travis/klee.sh
+++ b/.travis/klee.sh
@@ -51,6 +51,7 @@ fi
 ###############################################################################
 KLEE_Z3_CONFIGURE_OPTION=""
 KLEE_STP_CONFIGURE_OPTION=""
+KLEE_METASMT_CONFIGURE_OPTION=""
 SOLVER_LIST=$(echo "${SOLVERS}" | sed 's/:/ /')
 
 for solver in ${SOLVER_LIST}; do
@@ -63,6 +64,10 @@ for solver in ${SOLVER_LIST}; do
     echo "Z3"
     KLEE_Z3_CONFIGURE_OPTION="--with-z3=/usr"
     ;;
+  metaSMT)
+    echo "metaSMT"
+    KLEE_METASMT_CONFIGURE_OPTION="--with-metasmt=${BUILD_DIR}/metaSMT/build/root --with-metasmt-default-backend=${METASMT_DEFAULT}"
+    ;;
   *)
     echo "Unknown solver ${solver}"
     exit 1
@@ -87,6 +92,7 @@ ${KLEE_SRC}/configure --with-llvmsrc=/usr/lib/llvm-${LLVM_VERSION}/build \
             --with-llvmcxx=${KLEE_CXX} \
             ${KLEE_STP_CONFIGURE_OPTION} \
             ${KLEE_Z3_CONFIGURE_OPTION} \
+            ${KLEE_METASMT_CONFIGURE_OPTION} \
             ${KLEE_UCLIBC_CONFIGURE_OPTION} \
             ${TCMALLOC_OPTION} \
             CXXFLAGS="${COVERAGE_FLAGS}" \
diff --git a/.travis/metaSMT.sh b/.travis/metaSMT.sh
new file mode 100755
index 00000000..7a0d1eef
--- /dev/null
+++ b/.travis/metaSMT.sh
@@ -0,0 +1,20 @@
+#!/bin/bash -x
+
+# Get Boost, Z3, libgmp
+sudo apt-get -y install libboost1.55-dev libz3 libz3-dev libgmp-dev
+
+# Clone
+git clone git://github.com/hoangmle/metaSMT.git
+cd metaSMT
+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/     #
+
+# Build
+make -C build install
diff --git a/.travis/solvers.sh b/.travis/solvers.sh
index db717f2d..d64c1077 100755
--- a/.travis/solvers.sh
+++ b/.travis/solvers.sh
@@ -20,6 +20,10 @@ for solver in ${SOLVER_LIST}; do
     # Should we install libz3-dbg too?
     sudo apt-get -y install libz3 libz3-dev
     ;;
+  metaSMT)
+    echo "metaSMT"
+    ${KLEE_SRC}/.travis/metaSMT.sh
+    ;;
   *)
     echo "Unknown solver ${solver}"
     exit 1
diff --git a/Makefile.common b/Makefile.common
index 9bc850ba..cf7bdcf7 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -78,11 +78,5 @@ ifeq ($(ENABLE_UCLIBC),1)
 endif
 
 # For metaSMT
-ifeq ($(ENABLE_METASMT),1)
-  include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile
-  LD.Flags += -L$(METASMT_ROOT)/lib
-  CXX.Flags += -DBOOST_HAS_GCC_TR1 -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS
-  CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags))
-  CXX.Flags += $(metaSMT_INCLUDES)
-endif
+include $(PROJ_SRC_ROOT)/MetaSMT.mk
 
diff --git a/Makefile.config.in b/Makefile.config.in
index 7d3c05f6..1b0b7ba8 100644
--- a/Makefile.config.in
+++ b/Makefile.config.in
@@ -35,6 +35,7 @@ STP_LDFLAGS := @STP_LDFLAGS@
 
 ENABLE_METASMT := @ENABLE_METASMT@
 METASMT_ROOT := @METASMT_ROOT@
+METASMT_DEFAULT_BACKEND := @METASMT_DEFAULT_BACKEND@
 
 ENABLE_Z3 := @ENABLE_Z3@
 Z3_CFLAGS := @Z3_CFLAGS@
diff --git a/MetaSMT.mk b/MetaSMT.mk
index 94dd398a..817fa663 100644
--- a/MetaSMT.mk
+++ b/MetaSMT.mk
@@ -1,17 +1,13 @@
 # This file contains common code for linking against MetaSMT
 #
-# FIXME: This is a horribly fragile hack.
-# Instead the detection of what solvers the build of MetaSMT supports should be
-# done by the configure script and then the appropriate compiler flags should
-# be emitted to Makefile.config for consumption here.
+# Consume flags generated by metaSMT here.
 ifeq ($(ENABLE_METASMT),1)
   include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile
-  LD.Flags += -L$(METASMT_ROOT)/../../deps/Z3-4.1/lib \
-              -L$(METASMT_ROOT)/../../deps/boolector-1.5.118/lib \
-              -L$(METASMT_ROOT)/../../deps/minisat-git/lib/ \
-              -L$(METASMT_ROOT)/../../deps/boost-1_52_0/lib \
-              -L$(METASMT_ROOT)/../../deps/stp-svn/lib
-  CXX.Flags += -DBOOST_HAS_GCC_TR1
+  LD.Flags += $(metaSMT_LDFLAGS)
+  CXX.Flags += -DMETASMT_DEFAULT_BACKEND_IS_$(METASMT_DEFAULT_BACKEND)
+  CXX.Flags += $(metaSMT_CXXFLAGS)
+  CXX.Flags += $(metaSMT_INCLUDES)
   CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags))
-  LIBS += -lgomp -lboost_iostreams -lboost_thread -lboost_system -lmetaSMT -lz3 -lstp -lrt -lboolector -lminisat_core
+  CXX.Flags := $(filter-out -fno-rtti,$(CXX.Flags))
+  LIBS += $(metaSMT_LDLIBS)
 endif
diff --git a/autoconf/configure.ac b/autoconf/configure.ac
index 2be02321..a08e190e 100644
--- a/autoconf/configure.ac
+++ b/autoconf/configure.ac
@@ -742,7 +742,6 @@ dnl **************************************************************************
 AC_ARG_WITH(metasmt,
   AS_HELP_STRING([--with-metasmt],
     [Location of metaSMT installation directory]),,)
-
 if test X$with_metasmt = X ; then
   ENABLE_METASMT=0
   AC_MSG_NOTICE([Not using MetaSMT solver backend])
@@ -769,13 +768,51 @@ else
 
   AC_DEFINE(ENABLE_METASMT, 1, [Enable metaSMT API])
   AC_SUBST(METASMT_ROOT,$metasmt_root)
-  AC_SUBST(REQUIRES_RTTI,[[1]])
   ENABLE_METASMT=1
   AC_MSG_NOTICE([Using MetaSMT solver backend])
 fi
 
 AC_SUBST(ENABLE_METASMT)
 
+
+dnl **************************************************************************
+dnl User option to specify the default backend of metaSMT
+dnl **************************************************************************
+
+AC_ARG_WITH(metasmt-default-backend,
+  AS_HELP_STRING([--with-metasmt-default-backend],
+    [Default backend of metaSMT (btor|stp|z3, stp if unspecified)]),,)
+
+if test "X$with_metasmt_default_backend" != X ; then
+  if test "X$ENABLE_METASMT" != X1 ; then
+    AC_MSG_ERROR([--with-metasmt-default-backend requires metaSMT to be enabled])
+  fi
+  if test "$with_metasmt_default_backend" == "btor" ; then
+    METASMT_DEFAULT_BACKEND=BTOR
+    AC_MSG_NOTICE([metaSMT uses Boolector as default backend])
+  fi
+  if test "$with_metasmt_default_backend" == "z3" ; then
+    METASMT_DEFAULT_BACKEND=Z3
+    AC_MSG_NOTICE([metaSMT uses Z3 as default backend])
+  fi
+  if test "$with_metasmt_default_backend" == "stp" ; then
+    METASMT_DEFAULT_BACKEND=STP
+    AC_MSG_NOTICE([metaSMT uses STP as default backend])
+  fi
+  if test "X$METASMT_DEFAULT_BACKEND" == X ; then
+    METASMT_DEFAULT_BACKEND=STP
+    AC_MSG_NOTICE([$with_metasmt_default_backend unsupported, metaSMT uses STP as default backend])
+  fi
+else
+  if test "X$ENABLE_METASMT" == X1 ; then
+    METASMT_DEFAULT_BACKEND=STP
+    AC_MSG_NOTICE([No solver specified, metaSMT uses STP as default backend])
+  fi  
+fi
+
+AC_SUBST(METASMT_DEFAULT_BACKEND)
+
+
 dnl **************************************************************************
 dnl Check at least one solver backend is enabled
 dnl **************************************************************************
diff --git a/configure b/configure
index 33893680..7f1839c0 100755
--- a/configure
+++ b/configure
@@ -624,6 +624,7 @@ ac_includes_default="\
 
 ac_subst_vars='LTLIBOBJS
 LIBOBJS
+METASMT_DEFAULT_BACKEND
 ENABLE_METASMT
 METASMT_ROOT
 Z3_LDFLAGS
@@ -739,6 +740,7 @@ with_tcmalloc
 with_stp
 with_z3
 with_metasmt
+with_metasmt_default_backend
 '
       ac_precious_vars='build_alias
 host_alias
@@ -1393,6 +1395,9 @@ Optional Packages:
   --with-stp              Location of STP installation directory
   --with-z3               Location of Z3 installation directory
   --with-metasmt          Location of metaSMT installation directory
+  --with-metasmt-default-backend
+                          Default backend of metaSMT (btor|stp|z3, stp if
+                          unspecified)
 
 Some influential environment variables:
   CC          C compiler command
@@ -5324,7 +5329,6 @@ if test "${with_metasmt+set}" = set; then :
   withval=$with_metasmt;
 fi
 
-
 if test X$with_metasmt = X ; then
   ENABLE_METASMT=0
   { $as_echo "$as_me:${as_lineno-$LINENO}: Not using MetaSMT solver backend" >&5
@@ -5384,8 +5388,6 @@ $as_echo "#define ENABLE_METASMT 1" >>confdefs.h
 
   METASMT_ROOT=$metasmt_root
 
-  REQUIRES_RTTI=1
-
   ENABLE_METASMT=1
   { $as_echo "$as_me:${as_lineno-$LINENO}: Using MetaSMT solver backend" >&5
 $as_echo "$as_me: Using MetaSMT solver backend" >&6;}
@@ -5394,6 +5396,50 @@ fi
 
 
 
+
+
+# Check whether --with-metasmt-default-backend was given.
+if test "${with_metasmt_default_backend+set}" = set; then :
+  withval=$with_metasmt_default_backend;
+fi
+
+
+if test "X$with_metasmt_default_backend" != X ; then
+  if test "X$ENABLE_METASMT" != X1 ; then
+    as_fn_error $? "--with-metasmt-default-backend requires metaSMT to be enabled" "$LINENO" 5
+  fi
+  if test "$with_metasmt_default_backend" == "btor" ; then
+    METASMT_DEFAULT_BACKEND=BTOR
+    { $as_echo "$as_me:${as_lineno-$LINENO}: metaSMT uses Boolector as default backend" >&5
+$as_echo "$as_me: metaSMT uses Boolector as default backend" >&6;}
+  fi
+  if test "$with_metasmt_default_backend" == "z3" ; then
+    METASMT_DEFAULT_BACKEND=Z3
+    { $as_echo "$as_me:${as_lineno-$LINENO}: metaSMT uses Z3 as default backend" >&5
+$as_echo "$as_me: metaSMT uses Z3 as default backend" >&6;}
+  fi
+  if test "$with_metasmt_default_backend" == "stp" ; then
+    METASMT_DEFAULT_BACKEND=STP
+    { $as_echo "$as_me:${as_lineno-$LINENO}: metaSMT uses STP as default backend" >&5
+$as_echo "$as_me: metaSMT uses STP as default backend" >&6;}
+  fi
+  if test "X$METASMT_DEFAULT_BACKEND" == X ; then
+    METASMT_DEFAULT_BACKEND=STP
+    { $as_echo "$as_me:${as_lineno-$LINENO}: $with_metasmt_default_backend unsupported, metaSMT uses STP as default backend" >&5
+$as_echo "$as_me: $with_metasmt_default_backend unsupported, metaSMT uses STP as default backend" >&6;}
+  fi
+else
+  if test "X$ENABLE_METASMT" == X1 ; then
+    METASMT_DEFAULT_BACKEND=STP
+    { $as_echo "$as_me:${as_lineno-$LINENO}: No solver specified, metaSMT uses STP as default backend" >&5
+$as_echo "$as_me: No solver specified, metaSMT uses STP as default backend" >&6;}
+  fi
+fi
+
+
+
+
+
 if test "X$ENABLE_STP$ENABLE_Z3$ENABLE_METASMT" == X000 ; then
     as_fn_error $? "At least one solver backend must be enabled, try using --with-stp, --with-z3 or --with-metasmt" "$LINENO" 5
 fi
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index a0fbda03..20c190a5 100644
--- a/lib/Basic/CmdLineOptions.cpp
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -84,16 +84,30 @@ llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions(
 
 #ifdef ENABLE_METASMT
 
+#ifdef METASMT_DEFAULT_BACKEND_IS_BTOR
+#define METASMT_DEFAULT_BACKEND_STR "(default = btor)."
+#define METASMT_DEFAULT_BACKEND METASMT_BACKEND_BOOLECTOR
+#elif METASMT_DEFAULT_BACKEND_IS_Z3
+#define METASMT_DEFAULT_BACKEND_STR "(default = z3)."
+#define METASMT_DEFAULT_BACKEND METASMT_BACKEND_Z3
+#else
+#define METASMT_DEFAULT_BACKEND_STR "(default = stp)."
+#define METASMT_DEFAULT_BACKEND METASMT_BACKEND_STP
+#endif
+
 llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend(
     "metasmt-backend",
-    llvm::cl::desc("Specify the MetaSMT solver backend type (default=STP)."),
+    llvm::cl::desc("Specify the MetaSMT solver backend type " METASMT_DEFAULT_BACKEND_STR),
     llvm::cl::values(
         clEnumValN(METASMT_BACKEND_STP, "stp", "Use metaSMT with STP"),
         clEnumValN(METASMT_BACKEND_Z3, "z3", "Use metaSMT with Z3"),
         clEnumValN(METASMT_BACKEND_BOOLECTOR, "btor",
                    "Use metaSMT with Boolector"),
         clEnumValEnd),
-    llvm::cl::init(METASMT_BACKEND_STP));
+    llvm::cl::init(METASMT_DEFAULT_BACKEND));
+
+#undef METASMT_DEFAULT_BACKEND
+#undef METASMT_DEFAULT_BACKEND_STR
 
 #endif /* ENABLE_METASMT */
 
diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp
index 94bb3a5e..66328f30 100644
--- a/lib/Solver/CoreSolver.cpp
+++ b/lib/Solver/CoreSolver.cpp
@@ -15,14 +15,9 @@
 
 #ifdef ENABLE_METASMT
 
-#include <metaSMT/frontend/Array.hpp>
+#include <metaSMT/DirectSolver_Context.hpp>
 #include <metaSMT/backend/Z3_Backend.hpp>
 #include <metaSMT/backend/Boolector.hpp>
-#include <metaSMT/backend/MiniSAT.hpp>
-#include <metaSMT/DirectSolver_Context.hpp>
-#include <metaSMT/support/run_algorithm.hpp>
-#include <metaSMT/API/Stack.hpp>
-#include <metaSMT/API/Group.hpp>
 
 #define Expr VCExpr
 #define Type VCType
diff --git a/lib/Solver/Makefile b/lib/Solver/Makefile
index a44b4f6e..715f4b2d 100755
--- a/lib/Solver/Makefile
+++ b/lib/Solver/Makefile
@@ -16,11 +16,5 @@ NO_INSTALL=1
 
 include $(LEVEL)/Makefile.common
 
-ifeq ($(ENABLE_METASMT),1)
-  include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile
-  CXX.Flags += -DBOOST_HAS_GCC_TR1
-  CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags))
-  CXX.Flags := $(filter-out -fno-rtti,$(CXX.Flags))
-  CXX.Flags += $(metaSMT_CXXFLAGS)
-  CXX.Flags += $(metaSMT_INCLUDES)
-endif
+include $(PROJ_SRC_ROOT)/MetaSMT.mk
+
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h
index 9e1f9a62..ba7ea03b 100644
--- a/lib/Solver/MetaSMTBuilder.h
+++ b/lib/Solver/MetaSMTBuilder.h
@@ -7,7 +7,6 @@
 //
 //===----------------------------------------------------------------------===//
 
-
 /*
  * MetaSMTBuilder.h
  *
@@ -32,336 +31,357 @@
 #include <metaSMT/frontend/Logic.hpp>
 #include <metaSMT/frontend/QF_BV.hpp>
 #include <metaSMT/frontend/Array.hpp>
-#include <metaSMT/support/default_visitation_unrolling_limit.hpp>
-#include <metaSMT/support/run_algorithm.hpp>
-
-#define Expr VCExpr
-#define STP STP_Backend
-#include <metaSMT/backend/STP.hpp>
-#undef Expr
-#undef STP
- 
-#include <boost/mpl/vector.hpp>
-#include <boost/format.hpp>
 
 using namespace metaSMT;
 using namespace metaSMT::logic::QF_BV;
 
-
 #define DIRECT_CONTEXT
 
 namespace {
-  llvm::cl::opt<bool>
-  UseConstructHashMetaSMT("use-construct-hash-metasmt", 
-                   llvm::cl::desc("Use hash-consing during metaSMT query construction."),
-                   llvm::cl::init(true));
+llvm::cl::opt<bool> UseConstructHashMetaSMT(
+    "use-construct-hash-metasmt",
+    llvm::cl::desc("Use hash-consing during metaSMT query construction."),
+    llvm::cl::init(true));
 }
 
-
 namespace klee {
 
-typedef metaSMT::logic::Predicate<proto::terminal<metaSMT::logic::tag::true_tag>::type  > const MetaSMTConstTrue;
-typedef metaSMT::logic::Predicate<proto::terminal<metaSMT::logic::tag::false_tag>::type  > const MetaSMTConstFalse;
+typedef metaSMT::logic::Predicate<proto::terminal<
+    metaSMT::logic::tag::true_tag>::type> const MetaSMTConstTrue;
+typedef metaSMT::logic::Predicate<proto::terminal<
+    metaSMT::logic::tag::false_tag>::type> const MetaSMTConstFalse;
 typedef metaSMT::logic::Array::array MetaSMTArray;
 
-template<typename SolverContext>
-class MetaSMTBuilder;
+template <typename SolverContext> class MetaSMTBuilder;
+
+template <typename SolverContext>
+class MetaSMTArrayExprHash
+    : public ArrayExprHash<typename SolverContext::result_type> {
+
+  friend class MetaSMTBuilder<SolverContext>;
 
-template<typename SolverContext>
-class MetaSMTArrayExprHash : public ArrayExprHash< typename SolverContext::result_type > {
-    
-    friend class MetaSMTBuilder<SolverContext>;
-    
 public:
-    MetaSMTArrayExprHash() {};
-    virtual ~MetaSMTArrayExprHash() {};
+  MetaSMTArrayExprHash(){};
+  virtual ~MetaSMTArrayExprHash(){};
 };
 
 static const bool mimic_stp = true;
 
-
-template<typename SolverContext>
-class MetaSMTBuilder {
+template <typename SolverContext> class MetaSMTBuilder {
 public:
+  MetaSMTBuilder(SolverContext &solver, bool optimizeDivides)
+      : _solver(solver), _optimizeDivides(optimizeDivides){};
+  virtual ~MetaSMTBuilder(){};
+
+  typename SolverContext::result_type construct(ref<Expr> e);
+
+  typename SolverContext::result_type getInitialRead(const Array *root,
+                                                     unsigned index);
+
+  typename SolverContext::result_type getTrue() {
+    return (evaluate(_solver, metaSMT::logic::True));
+  }
+
+  typename SolverContext::result_type getFalse() {
+    return (evaluate(_solver, metaSMT::logic::False));
+  }
+
+  typename SolverContext::result_type bvOne(unsigned width) {
+    return bvZExtConst(width, 1);
+  }
+
+  typename SolverContext::result_type bvZero(unsigned width) {
+    return bvZExtConst(width, 0);
+  }
+
+  typename SolverContext::result_type bvMinusOne(unsigned width) {
+    return bvSExtConst(width, (int64_t)-1);
+  }
+
+  typename SolverContext::result_type bvConst32(unsigned width,
+                                                uint32_t value) {
+    return (evaluate(_solver, bvuint(value, width)));
+  }
+
+  typename SolverContext::result_type bvConst64(unsigned width,
+                                                uint64_t value) {
+    return (evaluate(_solver, bvuint(value, width)));
+  }
+
+  typename SolverContext::result_type bvZExtConst(unsigned width,
+                                                  uint64_t value);
+  typename SolverContext::result_type bvSExtConst(unsigned width,
+                                                  uint64_t value);
+
+  // logical left and right shift (not arithmetic)
+  typename SolverContext::result_type
+  bvLeftShift(typename SolverContext::result_type expr, unsigned width,
+              unsigned shift);
+  typename SolverContext::result_type
+  bvRightShift(typename SolverContext::result_type expr, unsigned width,
+               unsigned shift);
+  typename SolverContext::result_type
+  bvVarLeftShift(typename SolverContext::result_type expr,
+                 typename SolverContext::result_type shift, unsigned width);
+  typename SolverContext::result_type
+  bvVarRightShift(typename SolverContext::result_type expr,
+                  typename SolverContext::result_type shift, unsigned width);
+  typename SolverContext::result_type
+  bvVarArithRightShift(typename SolverContext::result_type expr,
+                       typename SolverContext::result_type shift,
+                       unsigned width);
+
+  typename SolverContext::result_type getArrayForUpdate(const Array *root,
+                                                        const UpdateNode *un);
+  typename SolverContext::result_type getInitialArray(const Array *root);
+  MetaSMTArray buildArray(unsigned elem_width, unsigned index_width);
 
-    MetaSMTBuilder(SolverContext& solver, bool optimizeDivides) : _solver(solver), _optimizeDivides(optimizeDivides) { };
-    virtual ~MetaSMTBuilder() {};
-    
-    typename SolverContext::result_type construct(ref<Expr> e);
-    
-    typename SolverContext::result_type getInitialRead(const Array *root, unsigned index);
-    
-    typename SolverContext::result_type getTrue() {
-        return(evaluate(_solver, metaSMT::logic::True));        
-    }
-    
-    typename SolverContext::result_type getFalse() {        
-        return(evaluate(_solver, metaSMT::logic::False));        
-    }
-    
-    typename SolverContext::result_type bvOne(unsigned width) {
-        return bvZExtConst(width, 1);
-    }
-    
-    typename SolverContext::result_type bvZero(unsigned width) {
-        return bvZExtConst(width, 0);
-    }
-    
-    typename SolverContext::result_type bvMinusOne(unsigned width) {
-        return bvSExtConst(width, (int64_t) -1);
-    }
-    
-    typename SolverContext::result_type bvConst32(unsigned width, uint32_t value) {
-        return(evaluate(_solver, bvuint(value, width)));
-    }
-    
-    typename SolverContext::result_type bvConst64(unsigned width, uint64_t value) {
-         return(evaluate(_solver, bvuint(value, width)));
-    }
-       
-    typename SolverContext::result_type bvZExtConst(unsigned width, uint64_t value);    
-    typename SolverContext::result_type bvSExtConst(unsigned width, uint64_t value);
-    
-    //logical left and right shift (not arithmetic)
-    typename SolverContext::result_type bvLeftShift(typename SolverContext::result_type expr, unsigned width, unsigned shift, unsigned shiftBits);
-    typename SolverContext::result_type bvRightShift(typename SolverContext::result_type expr, unsigned width, unsigned amount, unsigned shiftBits);
-    typename SolverContext::result_type bvVarLeftShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width);
-    typename SolverContext::result_type bvVarRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width);
-    typename SolverContext::result_type bvVarArithRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width);
-    
-    
-    typename SolverContext::result_type getArrayForUpdate(const Array *root, const UpdateNode *un);
-    typename SolverContext::result_type getInitialArray(const Array *root);
-    MetaSMTArray buildArray(unsigned elem_width, unsigned index_width);
-        
 private:
-    typedef ExprHashMap< std::pair<typename SolverContext::result_type, unsigned> >  MetaSMTExprHashMap;
-    typedef typename MetaSMTExprHashMap::iterator MetaSMTExprHashMapIter;
-    typedef typename MetaSMTExprHashMap::const_iterator MetaSMTExprHashMapConstIter;    
-
-    SolverContext&  _solver;
-    bool _optimizeDivides;
-    MetaSMTArrayExprHash<SolverContext>  _arr_hash;
-    MetaSMTExprHashMap                   _constructed;
-    
-    typename SolverContext::result_type constructActual(ref<Expr> e, int *width_out);
-    typename SolverContext::result_type construct(ref<Expr> e, int *width_out);
-    
-    typename SolverContext::result_type bvBoolExtract(typename SolverContext::result_type expr, int bit);
-    typename SolverContext::result_type bvExtract(typename SolverContext::result_type expr, unsigned top, unsigned bottom);
-    typename SolverContext::result_type eqExpr(typename SolverContext::result_type a, typename SolverContext::result_type b);
-    
-    typename SolverContext::result_type constructAShrByConstant(typename SolverContext::result_type expr, unsigned width, unsigned shift, 
-                                                                typename SolverContext::result_type isSigned, unsigned shiftBits);
-    typename SolverContext::result_type constructMulByConstant(typename SolverContext::result_type expr, unsigned width, uint64_t x);
-    typename SolverContext::result_type constructUDivByConstant(typename SolverContext::result_type expr_n, unsigned width, uint64_t d);
-    typename SolverContext::result_type constructSDivByConstant(typename SolverContext::result_type expr_n, unsigned width, uint64_t d);
-    
-    unsigned getShiftBits(unsigned amount) {
-        unsigned bits = 1;
-        amount--;
-        while (amount >>= 1) {
-            bits++;
-        }
-        return(bits);
-    }
+  typedef ExprHashMap<std::pair<typename SolverContext::result_type, unsigned> >
+      MetaSMTExprHashMap;
+  typedef typename MetaSMTExprHashMap::iterator MetaSMTExprHashMapIter;
+  typedef typename MetaSMTExprHashMap::const_iterator
+      MetaSMTExprHashMapConstIter;
+
+  SolverContext &_solver;
+  bool _optimizeDivides;
+  MetaSMTArrayExprHash<SolverContext> _arr_hash;
+  MetaSMTExprHashMap _constructed;
+
+  typename SolverContext::result_type constructActual(ref<Expr> e,
+                                                      int *width_out);
+  typename SolverContext::result_type construct(ref<Expr> e, int *width_out);
+
+  typename SolverContext::result_type
+  bvBoolExtract(typename SolverContext::result_type expr, int bit);
+  typename SolverContext::result_type
+  bvExtract(typename SolverContext::result_type expr, unsigned top,
+            unsigned bottom);
+  typename SolverContext::result_type
+  eqExpr(typename SolverContext::result_type a,
+         typename SolverContext::result_type b);
+
+  typename SolverContext::result_type
+  constructAShrByConstant(typename SolverContext::result_type expr,
+                          unsigned width, unsigned shift,
+                          typename SolverContext::result_type isSigned);
+  typename SolverContext::result_type
+  constructMulByConstant(typename SolverContext::result_type expr,
+                         unsigned width, uint64_t x);
+  typename SolverContext::result_type
+  constructUDivByConstant(typename SolverContext::result_type expr_n,
+                          unsigned width, uint64_t d);
+  typename SolverContext::result_type
+  constructSDivByConstant(typename SolverContext::result_type expr_n,
+                          unsigned width, uint64_t d);
 };
 
-template<typename SolverContext>
-typename SolverContext::result_type MetaSMTBuilder<SolverContext>::getArrayForUpdate(const Array *root, const UpdateNode *un) {
-  
-    if (!un) {
-        return(getInitialArray(root));
-    }
-    else {
-        typename SolverContext::result_type un_expr;
-        bool hashed = _arr_hash.lookupUpdateNodeExpr(un, un_expr);
-
-        if (!hashed) {
-            un_expr = evaluate(_solver,
-                               metaSMT::logic::Array::store(getArrayForUpdate(root, un->next),
-                                                            construct(un->index, 0),
-                                                            construct(un->value, 0)));
-            _arr_hash.hashUpdateNodeExpr(un, un_expr);
-        }
-        return(un_expr);
-    }
-}
+template <typename SolverContext>
+typename SolverContext::result_type
+MetaSMTBuilder<SolverContext>::getArrayForUpdate(const Array *root,
+                                                 const UpdateNode *un) {
 
-template<typename SolverContext>
-typename SolverContext::result_type MetaSMTBuilder<SolverContext>::getInitialArray(const Array *root)
-{
-    assert(root);
-    typename SolverContext::result_type array_expr;
-    bool hashed = _arr_hash.lookupArrayExpr(root, array_expr);
+  if (!un) {
+    return (getInitialArray(root));
+  } else {
+    typename SolverContext::result_type un_expr;
+    bool hashed = _arr_hash.lookupUpdateNodeExpr(un, un_expr);
 
     if (!hashed) {
+      un_expr = evaluate(_solver,
+                         metaSMT::logic::Array::store(
+                             getArrayForUpdate(root, un->next),
+                             construct(un->index, 0), construct(un->value, 0)));
+      _arr_hash.hashUpdateNodeExpr(un, un_expr);
+    }
+    return (un_expr);
+  }
+}
 
-        array_expr = evaluate(_solver, buildArray(root->getRange(), root->getDomain()));
-
-        if (root->isConstantArray()) {    
-            for (unsigned i = 0, e = root->size; i != e; ++i) {
-                 typename SolverContext::result_type tmp =
-                            evaluate(_solver, 
-                                     metaSMT::logic::Array::store(array_expr,
-                                                                  construct(ConstantExpr::alloc(i, root->getDomain()), 0),
-                                                                  construct(root->constantValues[i], 0)));
-                array_expr = tmp;
-            }
-        }
-        _arr_hash.hashArrayExpr(root, array_expr);
+template <typename SolverContext>
+typename SolverContext::result_type
+MetaSMTBuilder<SolverContext>::getInitialArray(const Array *root) {
+  assert(root);
+  typename SolverContext::result_type array_expr;
+  bool hashed = _arr_hash.lookupArrayExpr(root, array_expr);
+
+  if (!hashed) {
+
+    array_expr =
+        evaluate(_solver, buildArray(root->getRange(), root->getDomain()));
+
+    if (root->isConstantArray()) {
+      for (unsigned i = 0, e = root->size; i != e; ++i) {
+        typename SolverContext::result_type tmp = evaluate(
+            _solver,
+            metaSMT::logic::Array::store(
+                array_expr,
+                construct(ConstantExpr::alloc(i, root->getDomain()), 0),
+                construct(root->constantValues[i], 0)));
+        array_expr = tmp;
+      }
     }
+    _arr_hash.hashArrayExpr(root, array_expr);
+  }
 
-    return(array_expr);
+  return (array_expr);
 }
 
-template<typename SolverContext>
-MetaSMTArray MetaSMTBuilder<SolverContext>::buildArray(unsigned elem_width, unsigned index_width) {
-    return(metaSMT::logic::Array::new_array(elem_width, index_width));
+template <typename SolverContext>
+MetaSMTArray MetaSMTBuilder<SolverContext>::buildArray(unsigned elem_width,
+                                                       unsigned index_width) {
+  return (metaSMT::logic::Array::new_array(elem_width, index_width));
 }
 
-template<typename SolverContext>
-typename SolverContext::result_type MetaSMTBuilder<SolverContext>::getInitialRead(const Array *root, unsigned index) {
-    assert(root); 
-    assert(false);
-    typename SolverContext::result_type array_exp = getInitialArray(root);
-    typename SolverContext::result_type res = evaluate(
-                        _solver,
-                        metaSMT::logic::Array::select(array_exp, bvuint(index, root->getDomain())));    
-    return(res);
+template <typename SolverContext>
+typename SolverContext::result_type
+MetaSMTBuilder<SolverContext>::getInitialRead(const Array *root,
+                                              unsigned index) {
+  assert(root);
+  assert(false);
+  typename SolverContext::result_type array_exp = getInitialArray(root);
+  typename SolverContext::result_type res =
+      evaluate(_solver, metaSMT::logic::Array::select(
+                            array_exp, bvuint(index, root->getDomain())));
+  return (res);
 }
 
+template <typename SolverContext>
+typename SolverContext::result_type
+MetaSMTBuilder<SolverContext>::bvZExtConst(unsigned width, uint64_t value) {
 
-template<typename SolverContext>  
-typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvZExtConst(unsigned width, uint64_t value) {
-
-    typename SolverContext::result_type res;
+  typename SolverContext::result_type res;
 
-    if (width <= 64) {
-        res = bvConst64(width, value);
-    }
-    else {
-        typename SolverContext::result_type expr = bvConst64(64, value);
-        typename SolverContext::result_type zero = bvConst64(64, 0);
+  if (width <= 64) {
+    res = bvConst64(width, value);
+  } else {
+    typename SolverContext::result_type expr = bvConst64(64, value);
+    typename SolverContext::result_type zero = bvConst64(64, 0);
 
-        for (width -= 64; width > 64; width -= 64) {
-             expr = evaluate(_solver, concat(zero, expr));  
-        }
-        res = evaluate(_solver, concat(bvConst64(width, 0), expr));  
+    for (width -= 64; width > 64; width -= 64) {
+      expr = evaluate(_solver, concat(zero, expr));
     }
+    res = evaluate(_solver, concat(bvConst64(width, 0), expr));
+  }
 
-    return(res); 
+  return (res);
 }
 
-template<typename SolverContext>  
-typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvSExtConst(unsigned width, uint64_t value) {
-  
+template <typename SolverContext>
+typename SolverContext::result_type
+MetaSMTBuilder<SolverContext>::bvSExtConst(unsigned width, uint64_t value) {
+
   typename SolverContext::result_type res;
-  
+
   if (width <= 64) {
-      res = bvConst64(width, value); 
-  }
-  else {            
-      // ToDo Reconsider -- note differences in STP and metaSMT for sign_extend arguments
-      res = evaluate(_solver, sign_extend(width - 64, bvConst64(64, value)));		     
+    res = bvConst64(width, value);
+  } else {
+    // ToDo Reconsider -- note differences in STP and metaSMT for sign_extend
+    // arguments
+    res = evaluate(_solver, sign_extend(width - 64, bvConst64(64, value)));
   }
-  return(res); 
+  return (res);
 }
 
-template<typename SolverContext>
-typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvBoolExtract(typename SolverContext::result_type expr, int bit) {
-    return(evaluate(_solver,
-                    metaSMT::logic::equal(extract(bit, bit, expr),
-                                          bvOne(1))));
+template <typename SolverContext>
+typename SolverContext::result_type
+MetaSMTBuilder<SolverContext>::bvBoolExtract(
+    typename SolverContext::result_type expr, int bit) {
+  return (evaluate(_solver,
+                   metaSMT::logic::equal(extract(bit, bit, expr), bvOne(1))));
 }
 
-template<typename SolverContext>
-typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvExtract(typename SolverContext::result_type expr, unsigned top, unsigned bottom) {    
-    return(evaluate(_solver, extract(top, bottom, expr)));
+template <typename SolverContext>
+typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvExtract(
+    typename SolverContext::result_type expr, unsigned top, unsigned bottom) {
+  return (evaluate(_solver, extract(top, bottom, expr)));
 }
 
-template<typename SolverContext>
-typename SolverContext::result_type MetaSMTBuilder<SolverContext>::eqExpr(typename SolverContext::result_type a, typename SolverContext::result_type b) {    
-    return(evaluate(_solver, metaSMT::logic::equal(a, b)));
+template <typename SolverContext>
+typename SolverContext::result_type
+MetaSMTBuilder<SolverContext>::eqExpr(typename SolverContext::result_type a,
+                                      typename SolverContext::result_type b) {
+  return (evaluate(_solver, metaSMT::logic::equal(a, b)));
 }
 
-template<typename SolverContext>
-typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructAShrByConstant(typename SolverContext::result_type expr, unsigned width, unsigned amount,
-                                                                                           typename SolverContext::result_type isSigned, unsigned shiftBits) {
-    unsigned shift = amount & ((1 << shiftBits) - 1);
-    typename SolverContext::result_type res;
-    
-    if (shift == 0) {
-        res = expr;
-    }
-    else if (shift >= width) {
-        res = evaluate(_solver, metaSMT::logic::Ite(isSigned, bvMinusOne(width), bvZero(width)));
-    }
-    else {
-        res = evaluate(_solver, metaSMT::logic::Ite(isSigned,
-                                                    concat(bvMinusOne(shift), bvExtract(expr, width - 1, shift)),
-                                                    bvRightShift(expr, width, shift, shiftBits)));
-    }
-    
-    return(res);
+template <typename SolverContext>
+typename SolverContext::result_type
+MetaSMTBuilder<SolverContext>::constructAShrByConstant(
+    typename SolverContext::result_type expr, unsigned width, unsigned shift,
+    typename SolverContext::result_type isSigned) {
+  typename SolverContext::result_type res;
+
+  if (shift == 0) {
+    res = expr;
+  } else if (shift >= width) {
+    res = bvZero(width);
+  } else {
+    res = evaluate(
+        _solver,
+        metaSMT::logic::Ite(isSigned, concat(bvMinusOne(shift),
+                                             bvExtract(expr, width - 1, shift)),
+                            bvRightShift(expr, width, shift)));
+  }
+
+  return (res);
 }
 
 // width is the width of expr; x -- number of bits to shift with
-template<typename SolverContext>
-typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructMulByConstant(typename SolverContext::result_type expr, unsigned width, uint64_t x) {
-    
-    unsigned shiftBits = getShiftBits(width);
-    uint64_t add, sub;
-    typename SolverContext::result_type res;
-    bool first = true;
+template <typename SolverContext>
+typename SolverContext::result_type
+MetaSMTBuilder<SolverContext>::constructMulByConstant(
+    typename SolverContext::result_type expr, unsigned width, uint64_t x) {
 
-    // expr*x == expr*(add-sub) == expr*add - expr*sub
-    ComputeMultConstants64(x, add, sub);
+  uint64_t add, sub;
+  typename SolverContext::result_type res;
+  bool first = true;
 
-    // legal, these would overflow completely
-    add = bits64::truncateToNBits(add, width);
-    sub = bits64::truncateToNBits(sub, width);
-    
-    for (int j = 63; j >= 0; j--) {
-        uint64_t bit = 1LL << j;
+  // expr*x == expr*(add-sub) == expr*add - expr*sub
+  ComputeMultConstants64(x, add, sub);
 
-        if ((add & bit) || (sub & bit)) {
-            assert(!((add & bit) && (sub & bit)) && "invalid mult constants");
+  // legal, these would overflow completely
+  add = bits64::truncateToNBits(add, width);
+  sub = bits64::truncateToNBits(sub, width);
 
-            typename SolverContext::result_type op = bvLeftShift(expr, width, j, shiftBits);
+  for (int j = 63; j >= 0; j--) {
+    uint64_t bit = 1LL << j;
 
-            if (add & bit) {
-                if (!first) {
-                    res = evaluate(_solver, bvadd(res, op));
-                } else {
-                    res = op;
-                    first = false;
-                }
-            } else {
-                if (!first) {
-                    res = evaluate(_solver, bvsub(res, op));                    
-                } else {
-                     // To reconsider: vc_bvUMinusExpr in STP
-                    res = evaluate(_solver, bvsub(bvZero(width), op));
-                    first = false;
-                }
-            }
+    if ((add & bit) || (sub & bit)) {
+      assert(!((add & bit) && (sub & bit)) && "invalid mult constants");
+
+      typename SolverContext::result_type op = bvLeftShift(expr, width, j);
+
+      if (add & bit) {
+        if (!first) {
+          res = evaluate(_solver, bvadd(res, op));
+        } else {
+          res = op;
+          first = false;
         }
+      } else {
+        if (!first) {
+          res = evaluate(_solver, bvsub(res, op));
+        } else {
+          // To reconsider: vc_bvUMinusExpr in STP
+          res = evaluate(_solver, bvsub(bvZero(width), op));
+          first = false;
+        }
+      }
     }
-  
-    if (first) { 
-        res = bvZero(width);
-    }
+  }
 
-    return(res);
-}
+  if (first) {
+    res = bvZero(width);
+  }
 
+  return (res);
+}
 
-/* 
- * Compute the 32-bit unsigned integer division of n by a divisor d based on 
+/*
+ * Compute the 32-bit unsigned integer division of n by a divisor d based on
  * the constants derived from the constant divisor d.
  *
- * Returns n/d without doing explicit division.  The cost is 2 adds, 3 shifts, 
+ * Returns n/d without doing explicit division.  The cost is 2 adds, 3 shifts,
  * and a (64-bit) multiply.
  *
  * @param expr_n numerator (dividend) n as an expression
@@ -370,36 +390,46 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructMulB
  *
  * @return n/d without doing explicit division
  */
-template<typename SolverContext>
-typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructUDivByConstant(typename SolverContext::result_type expr_n, unsigned width, uint64_t d) {
-    
-    assert(width == 32 && "can only compute udiv constants for 32-bit division");
-    
-    // Compute the constants needed to compute n/d for constant d without division by d.
-    uint32_t mprime, sh1, sh2;
-    ComputeUDivConstants32(d, mprime, sh1, sh2);
-    typename SolverContext::result_type expr_sh1 = bvConst32(32, sh1);
-    typename SolverContext::result_type expr_sh2 = bvConst32(32, sh2);
-    
-    // t1  = MULUH(mprime, n) = ( (uint64_t)mprime * (uint64_t)n ) >> 32
-    typename SolverContext::result_type expr_n_64 = evaluate(_solver, concat(bvZero(32), expr_n)); //extend to 64 bits
-    typename SolverContext::result_type t1_64bits = constructMulByConstant(expr_n_64, 64, (uint64_t)mprime);
-    typename SolverContext::result_type t1        = bvExtract(t1_64bits, 63, 32); //upper 32 bits
-    
-    // n/d = (((n - t1) >> sh1) + t1) >> sh2;
-    typename SolverContext::result_type n_minus_t1 = evaluate(_solver, bvsub(expr_n, t1));   
-    typename SolverContext::result_type shift_sh1  = bvVarRightShift(n_minus_t1, expr_sh1, 32);
-    typename SolverContext::result_type plus_t1    = evaluate(_solver, bvadd(shift_sh1, t1));    
-    typename SolverContext::result_type res        = bvVarRightShift(plus_t1, expr_sh2, 32);
-    
-    return(res);
+template <typename SolverContext>
+typename SolverContext::result_type
+MetaSMTBuilder<SolverContext>::constructUDivByConstant(
+    typename SolverContext::result_type expr_n, unsigned width, uint64_t d) {
+
+  assert(width == 32 && "can only compute udiv constants for 32-bit division");
+
+  // Compute the constants needed to compute n/d for constant d without division
+  // by d.
+  uint32_t mprime, sh1, sh2;
+  ComputeUDivConstants32(d, mprime, sh1, sh2);
+  typename SolverContext::result_type expr_sh1 = bvConst32(32, sh1);
+  typename SolverContext::result_type expr_sh2 = bvConst32(32, sh2);
+
+  // t1  = MULUH(mprime, n) = ( (uint64_t)mprime * (uint64_t)n ) >> 32
+  typename SolverContext::result_type expr_n_64 =
+      evaluate(_solver, concat(bvZero(32), expr_n)); // extend to 64 bits
+  typename SolverContext::result_type t1_64bits =
+      constructMulByConstant(expr_n_64, 64, (uint64_t)mprime);
+  typename SolverContext::result_type t1 =
+      bvExtract(t1_64bits, 63, 32); // upper 32 bits
+
+  // n/d = (((n - t1) >> sh1) + t1) >> sh2;
+  typename SolverContext::result_type n_minus_t1 =
+      evaluate(_solver, bvsub(expr_n, t1));
+  typename SolverContext::result_type shift_sh1 =
+      bvVarRightShift(n_minus_t1, expr_sh1, 32);
+  typename SolverContext::result_type plus_t1 =
+      evaluate(_solver, bvadd(shift_sh1, t1));
+  typename SolverContext::result_type res =
+      bvVarRightShift(plus_t1, expr_sh2, 32);
+
+  return (res);
 }
 
-/* 
- * Compute the 32-bitnsigned integer division of n by a divisor d based on 
+/*
+ * Compute the 32-bitnsigned integer division of n by a divisor d based on
  * the constants derived from the constant divisor d.
  *
- * Returns n/d without doing explicit division.  The cost is 3 adds, 3 shifts, 
+ * Returns n/d without doing explicit division.  The cost is 3 adds, 3 shifts,
  * a (64-bit) multiply, and an XOR.
  *
  * @param n      numerator (dividend) as an expression
@@ -408,519 +438,540 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructUDiv
  *
  * @return n/d without doing explicit division
  */
-template<typename SolverContext>
-typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructSDivByConstant(typename SolverContext::result_type expr_n, unsigned width, uint64_t d) {
-    
-    assert(width == 32 && "can only compute udiv constants for 32-bit division");
-
-    // Compute the constants needed to compute n/d for constant d w/o division by d.
-    int32_t mprime, dsign, shpost;
-    ComputeSDivConstants32(d, mprime, dsign, shpost);
-    typename SolverContext::result_type expr_dsign  = bvConst32(32, dsign);
-    typename SolverContext::result_type expr_shpost = bvConst32(32, shpost);
-    
-    // q0 = n + MULSH( mprime, n ) = n + (( (int64_t)mprime * (int64_t)n ) >> 32)
-    int64_t mprime_64     = (int64_t)mprime;
-    
-    // ToDo Reconsider -- note differences in STP and metaSMT for sign_extend arguments
-    typename SolverContext::result_type expr_n_64    = evaluate(_solver, sign_extend(64 - width, expr_n));    
-    typename SolverContext::result_type mult_64      = constructMulByConstant(expr_n_64, 64, mprime_64);
-    typename SolverContext::result_type mulsh        = bvExtract(mult_64, 63, 32); //upper 32-bits    
-    typename SolverContext::result_type n_plus_mulsh = evaluate(_solver, bvadd(expr_n, mulsh));
-    
-    // Improved variable arithmetic right shift: sign extend, shift, extract.
-    typename SolverContext::result_type extend_npm   = evaluate(_solver, sign_extend(64 - width, n_plus_mulsh));    
-    typename SolverContext::result_type shift_npm    = bvVarRightShift(extend_npm, expr_shpost, 64);
-    typename SolverContext::result_type shift_shpost = bvExtract(shift_npm, 31, 0); //lower 32-bits
-    
-    /////////////
-    
-    // XSIGN(n) is -1 if n is negative, positive one otherwise
-    typename SolverContext::result_type is_signed    = bvBoolExtract(expr_n, 31);
-    typename SolverContext::result_type neg_one      = bvMinusOne(32);
-    typename SolverContext::result_type xsign_of_n   = evaluate(_solver, metaSMT::logic::Ite(is_signed, neg_one, bvZero(32)));    
-
-    // q0 = (n_plus_mulsh >> shpost) - XSIGN(n)
-    typename SolverContext::result_type q0           = evaluate(_solver, bvsub(shift_shpost, xsign_of_n));    
-  
-    // n/d = (q0 ^ dsign) - dsign
-    typename SolverContext::result_type q0_xor_dsign = evaluate(_solver, bvxor(q0, expr_dsign));    
-    typename SolverContext::result_type res          = evaluate(_solver, bvsub(q0_xor_dsign, expr_dsign));    
-    
-    return(res);
+template <typename SolverContext>
+typename SolverContext::result_type
+MetaSMTBuilder<SolverContext>::constructSDivByConstant(
+    typename SolverContext::result_type expr_n, unsigned width, uint64_t d) {
+
+  assert(width == 32 && "can only compute udiv constants for 32-bit division");
+
+  // Compute the constants needed to compute n/d for constant d w/o division by
+  // d.
+  int32_t mprime, dsign, shpost;
+  ComputeSDivConstants32(d, mprime, dsign, shpost);
+  typename SolverContext::result_type expr_dsign = bvConst32(32, dsign);
+  typename SolverContext::result_type expr_shpost = bvConst32(32, shpost);
+
+  // q0 = n + MULSH( mprime, n ) = n + (( (int64_t)mprime * (int64_t)n ) >> 32)
+  int64_t mprime_64 = (int64_t)mprime;
+
+  // ToDo Reconsider -- note differences in STP and metaSMT for sign_extend
+  // arguments
+  typename SolverContext::result_type expr_n_64 =
+      evaluate(_solver, sign_extend(64 - width, expr_n));
+  typename SolverContext::result_type mult_64 =
+      constructMulByConstant(expr_n_64, 64, mprime_64);
+  typename SolverContext::result_type mulsh =
+      bvExtract(mult_64, 63, 32); // upper 32-bits
+  typename SolverContext::result_type n_plus_mulsh =
+      evaluate(_solver, bvadd(expr_n, mulsh));
+
+  // Improved variable arithmetic right shift: sign extend, shift, extract.
+  typename SolverContext::result_type extend_npm =
+      evaluate(_solver, sign_extend(64 - width, n_plus_mulsh));
+  typename SolverContext::result_type shift_npm =
+      bvVarRightShift(extend_npm, expr_shpost, 64);
+  typename SolverContext::result_type shift_shpost =
+      bvExtract(shift_npm, 31, 0); // lower 32-bits
+
+  /////////////
+
+  // XSIGN(n) is -1 if n is negative, positive one otherwise
+  typename SolverContext::result_type is_signed = bvBoolExtract(expr_n, 31);
+  typename SolverContext::result_type neg_one = bvMinusOne(32);
+  typename SolverContext::result_type xsign_of_n =
+      evaluate(_solver, metaSMT::logic::Ite(is_signed, neg_one, bvZero(32)));
+
+  // q0 = (n_plus_mulsh >> shpost) - XSIGN(n)
+  typename SolverContext::result_type q0 =
+      evaluate(_solver, bvsub(shift_shpost, xsign_of_n));
+
+  // n/d = (q0 ^ dsign) - dsign
+  typename SolverContext::result_type q0_xor_dsign =
+      evaluate(_solver, bvxor(q0, expr_dsign));
+  typename SolverContext::result_type res =
+      evaluate(_solver, bvsub(q0_xor_dsign, expr_dsign));
+
+  return (res);
 }
 
-template<typename SolverContext>
-typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvLeftShift(typename SolverContext::result_type expr, unsigned width, unsigned amount, unsigned shiftBits) {
-    
-    typename SolverContext::result_type res;    
-    unsigned shift = amount & ((1 << shiftBits) - 1);
+template <typename SolverContext>
+typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvLeftShift(
+    typename SolverContext::result_type expr, unsigned width, unsigned shift) {
 
-    if (shift == 0) {
-        res = expr;
-    }
-    else if (shift >= width) {
-        res = bvZero(width);
-    }
-    else {
-        // stp shift does "expr @ [0 x s]" which we then have to extract,
-        // rolling our own gives slightly smaller exprs
-        res = evaluate(_solver, concat(extract(width - shift - 1, 0, expr),
-                                       bvZero(shift)));
-    }
+  typename SolverContext::result_type res;
 
-    return(res);
+  if (shift == 0) {
+    res = expr;
+  } else if (shift >= width) {
+    res = bvZero(width);
+  } else {
+    // stp shift does "expr @ [0 x s]" which we then have to extract,
+    // rolling our own gives slightly smaller exprs
+    res = evaluate(_solver,
+                   concat(extract(width - shift - 1, 0, expr), bvZero(shift)));
+  }
+
+  return (res);
 }
 
-template<typename SolverContext>
-typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvRightShift(typename SolverContext::result_type expr, unsigned width, unsigned amount, unsigned shiftBits) {
-  
-    typename SolverContext::result_type res;    
-    unsigned shift = amount & ((1 << shiftBits) - 1);
-
-    if (shift == 0) {
-        res = expr;
-    } 
-    else if (shift >= width) {
-        res = bvZero(width);
-    }
-    else {
-        res = evaluate(_solver, concat(bvZero(shift),
-                                       extract(width - 1, shift, expr)));        
-    }
+template <typename SolverContext>
+typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvRightShift(
+    typename SolverContext::result_type expr, unsigned width, unsigned shift) {
+
+  typename SolverContext::result_type res;
+
+  if (shift == 0) {
+    res = expr;
+  } else if (shift >= width) {
+    res = bvZero(width);
+  } else {
+    res = evaluate(_solver,
+                   concat(bvZero(shift), extract(width - 1, shift, expr)));
+  }
 
-    return(res);
+  return (res);
 }
 
 // left shift by a variable amount on an expression of the specified width
-template<typename SolverContext>
-typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarLeftShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width) {
-    
-    typename SolverContext::result_type res =  bvZero(width);
-    
-    int shiftBits = getShiftBits(width);
+template <typename SolverContext>
+typename SolverContext::result_type
+MetaSMTBuilder<SolverContext>::bvVarLeftShift(
+    typename SolverContext::result_type expr,
+    typename SolverContext::result_type shift, unsigned width) {
+
+  typename SolverContext::result_type res = bvZero(width);
+
+  // construct a big if-then-elif-elif-... with one case per possible shift
+  // amount
+  for (int i = width - 1; i >= 0; i--) {
+    res = evaluate(_solver,
+                   metaSMT::logic::Ite(eqExpr(shift, bvConst32(width, i)),
+                                       bvLeftShift(expr, width, i), res));
+  }
 
-    //get the shift amount (looking only at the bits appropriate for the given width)
-    typename SolverContext::result_type shift = evaluate(_solver, extract(shiftBits - 1, 0, amount));    
+  // If overshifting, shift to zero
+  res = evaluate(_solver,
+                 metaSMT::logic::Ite(bvult(shift, bvConst32(width, width)), res,
+                                     bvZero(width)));
 
-    //construct a big if-then-elif-elif-... with one case per possible shift amount
-    for(int i = width - 1; i >= 0; i--) {
-        res = evaluate(_solver, metaSMT::logic::Ite(eqExpr(shift, bvConst32(shiftBits, i)),
-                                                    bvLeftShift(expr, width, i, shiftBits),
-                                                    res));
-    }
-    
-    // If overshifting, shift to zero    
-    res = evaluate(_solver, metaSMT::logic::Ite(bvult(shift, bvConst32(shiftBits, width)),
-                                                res,
-                                                bvZero(width)));                                                
-
-    return(res);
+  return (res);
 }
 
-// logical right shift by a variable amount on an expression of the specified width
-template<typename SolverContext>
-typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width) {
-    
-    typename SolverContext::result_type res = bvZero(width);
-    
-    int shiftBits = getShiftBits(width);
-    
-    //get the shift amount (looking only at the bits appropriate for the given width)
-    typename SolverContext::result_type shift = bvExtract(amount, shiftBits - 1, 0);
-    
-    //construct a big if-then-elif-elif-... with one case per possible shift amount
-    for (int i = width - 1; i >= 0; i--) {
-        res = evaluate(_solver, metaSMT::logic::Ite(eqExpr(shift, bvConst32(shiftBits, i)),
-                                                    bvRightShift(expr, width, i, shiftBits),
-                                                    res));
-         // ToDo Reconsider widht to provide to bvRightShift
-    }
-    
-    // If overshifting, shift to zero
-    res = evaluate(_solver, metaSMT::logic::Ite(bvult(shift, bvConst32(shiftBits, width)),
-                                                res,
-                                                bvZero(width)));                                                
+// logical right shift by a variable amount on an expression of the specified
+// width
+template <typename SolverContext>
+typename SolverContext::result_type
+MetaSMTBuilder<SolverContext>::bvVarRightShift(
+    typename SolverContext::result_type expr,
+    typename SolverContext::result_type shift, unsigned width) {
+
+  typename SolverContext::result_type res = bvZero(width);
+
+  // construct a big if-then-elif-elif-... with one case per possible shift
+  // amount
+  for (int i = width - 1; i >= 0; i--) {
+    res = evaluate(_solver,
+                   metaSMT::logic::Ite(eqExpr(shift, bvConst32(width, i)),
+                                       bvRightShift(expr, width, i), res));
+    // ToDo Reconsider widht to provide to bvRightShift
+  }
+
+  // If overshifting, shift to zero
+  res = evaluate(_solver,
+                 metaSMT::logic::Ite(bvult(shift, bvConst32(width, width)), res,
+                                     bvZero(width)));
 
-    return(res);
+  return (res);
 }
 
-// arithmetic right shift by a variable amount on an expression of the specified width
-template<typename SolverContext>
-typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarArithRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width) {
-  
-    int shiftBits = getShiftBits(width);
+// arithmetic right shift by a variable amount on an expression of the specified
+// width
+template <typename SolverContext>
+typename SolverContext::result_type
+MetaSMTBuilder<SolverContext>::bvVarArithRightShift(
+    typename SolverContext::result_type expr,
+    typename SolverContext::result_type shift, unsigned width) {
+
+  // get the sign bit to fill with
+  typename SolverContext::result_type signedBool =
+      bvBoolExtract(expr, width - 1);
+
+  // start with the result if shifting by width-1
+  typename SolverContext::result_type res =
+      constructAShrByConstant(expr, width, width - 1, signedBool);
+
+  // construct a big if-then-elif-elif-... with one case per possible shift
+  // amount
+  // XXX more efficient to move the ite on the sign outside all exprs?
+  // XXX more efficient to sign extend, right shift, then extract lower bits?
+  for (int i = width - 2; i >= 0; i--) {
+    res = evaluate(
+        _solver, metaSMT::logic::Ite(
+                     eqExpr(shift, bvConst32(width, i)),
+                     constructAShrByConstant(expr, width, i, signedBool), res));
+  }
 
-    //get the shift amount (looking only at the bits appropriate for the given width)
-    typename SolverContext::result_type shift = bvExtract(amount, shiftBits - 1, 0);
-    
-    //get the sign bit to fill with
-    typename SolverContext::result_type signedBool = bvBoolExtract(expr, width - 1);
-
-    //start with the result if shifting by width-1
-    typename SolverContext::result_type res =  constructAShrByConstant(expr, width, width - 1, signedBool, shiftBits);
-
-    // construct a big if-then-elif-elif-... with one case per possible shift amount
-    // XXX more efficient to move the ite on the sign outside all exprs?
-    // XXX more efficient to sign extend, right shift, then extract lower bits?
-    for (int i = width - 2; i >= 0; i--) {
-        res = evaluate(_solver, metaSMT::logic::Ite(eqExpr(shift, bvConst32(shiftBits,i)),
-                                                    constructAShrByConstant(expr, width, i, signedBool, shiftBits),
-                                                    res));
-    }
-    
-    // If overshifting, shift to zero
-    res = evaluate(_solver, metaSMT::logic::Ite(bvult(shift, bvConst32(shiftBits, width)),
-                                                res,
-                                                bvZero(width)));      
+  // If overshifting, shift to zero
+  res = evaluate(_solver,
+                 metaSMT::logic::Ite(bvult(shift, bvConst32(width, width)), res,
+                                     bvZero(width)));
 
-    return(res);
+  return (res);
 }
 
-template<typename SolverContext>
-typename SolverContext::result_type MetaSMTBuilder<SolverContext>::construct(ref<Expr> e) {
-    typename SolverContext::result_type res = construct(e, 0);
-    _constructed.clear();
-    return res;
+template <typename SolverContext>
+typename SolverContext::result_type
+MetaSMTBuilder<SolverContext>::construct(ref<Expr> e) {
+  typename SolverContext::result_type res = construct(e, 0);
+  _constructed.clear();
+  return res;
 }
 
-
 /** if *width_out!=1 then result is a bitvector,
     otherwise it is a bool */
-template<typename SolverContext>
-typename SolverContext::result_type MetaSMTBuilder<SolverContext>::construct(ref<Expr> e, int *width_out) {
-  
-    if (!UseConstructHashMetaSMT || isa<ConstantExpr>(e)) {
-        return(constructActual(e, width_out));
+template <typename SolverContext>
+typename SolverContext::result_type
+MetaSMTBuilder<SolverContext>::construct(ref<Expr> e, int *width_out) {
+
+  if (!UseConstructHashMetaSMT || isa<ConstantExpr>(e)) {
+    return (constructActual(e, width_out));
+  } else {
+    MetaSMTExprHashMapIter it = _constructed.find(e);
+    if (it != _constructed.end()) {
+      if (width_out) {
+        *width_out = it->second.second;
+      }
+      return it->second.first;
     } else {
-        MetaSMTExprHashMapIter it = _constructed.find(e);
-        if (it != _constructed.end()) {
-            if (width_out) {
-                *width_out = it->second.second;
-            }
-            return it->second.first;
-        } else {
-            int width = 0;
-            if (!width_out) {
-                 width_out = &width;
-            }
-            typename SolverContext::result_type res = constructActual(e, width_out);
-            _constructed.insert(std::make_pair(e, std::make_pair(res, *width_out)));
-            return res;
-        }
+      int width = 0;
+      if (!width_out) {
+        width_out = &width;
+      }
+      typename SolverContext::result_type res = constructActual(e, width_out);
+      _constructed.insert(std::make_pair(e, std::make_pair(res, *width_out)));
+      return res;
     }
+  }
 }
 
-template<typename SolverContext>
-typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActual(ref<Expr> e, int *width_out)  {
+template <typename SolverContext>
+typename SolverContext::result_type
+MetaSMTBuilder<SolverContext>::constructActual(ref<Expr> e, int *width_out) {
 
-    typename SolverContext::result_type res;
-    
-    int width = 0;
-    if (!width_out) { 
-        // assert(false);
-        width_out = &width;
+  typename SolverContext::result_type res;
+
+  int width = 0;
+  if (!width_out) {
+    // assert(false);
+    width_out = &width;
+  }
+
+  ++stats::queryConstructs;
+
+  //     llvm::errs() << "Constructing expression ";
+  //     ExprPPrinter::printSingleExpr(llvm::errs(), e);
+  //     llvm::errs() << "\n";
+
+  switch (e->getKind()) {
+
+  case Expr::Constant: {
+    ConstantExpr *coe = cast<ConstantExpr>(e);
+    assert(coe);
+    unsigned coe_width = coe->getWidth();
+    *width_out = coe_width;
+
+    // Coerce to bool if necessary.
+    if (coe_width == 1) {
+      res = (coe->isTrue()) ? getTrue() : getFalse();
+    } else if (coe_width <= 32) {
+      res = bvConst32(coe_width, coe->getZExtValue(32));
+    } else if (coe_width <= 64) {
+      res = bvConst64(coe_width, coe->getZExtValue());
+    } else {
+      ref<ConstantExpr> tmp = coe;
+      res = bvConst64(64, tmp->Extract(0, 64)->getZExtValue());
+      while (tmp->getWidth() > 64) {
+        tmp = tmp->Extract(64, tmp->getWidth() - 64);
+        unsigned min_width = std::min(64U, tmp->getWidth());
+        res = evaluate(_solver,
+                       concat(bvConst64(min_width, tmp->Extract(0, min_width)
+                                                       ->getZExtValue()),
+                              res));
+      }
     }
-    
-    ++stats::queryConstructs;
-    
-//     llvm::errs() << "Constructing expression ";
-//     ExprPPrinter::printSingleExpr(llvm::errs(), e);
-//     llvm::errs() << "\n";
-
-    switch (e->getKind()) {
-
-        case Expr::Constant:
-        {
-            ConstantExpr *coe = cast<ConstantExpr>(e);
-            assert(coe);
-            unsigned coe_width = coe->getWidth();
-            *width_out = coe_width;
-
-            // Coerce to bool if necessary.
-            if (coe_width == 1) {
-                res = (coe->isTrue()) ? getTrue() : getFalse();
-            }
-            else if (coe_width <= 32) {
-                 res = bvConst32(coe_width, coe->getZExtValue(32));
-            }
-            else if (coe_width <= 64) {
-                 res = bvConst64(coe_width, coe->getZExtValue());
-            }
-            else {
-                 ref<ConstantExpr> tmp = coe;
-                 res = bvConst64(64, tmp->Extract(0, 64)->getZExtValue());
-                 while (tmp->getWidth() > 64) {
-                     tmp = tmp->Extract(64, tmp->getWidth() -  64);
-                     unsigned min_width = std::min(64U, tmp->getWidth());
-                     res = evaluate(_solver,
-                                    concat(bvConst64(min_width, tmp->Extract(0, min_width)->getZExtValue()),
-                                           res));
-                 }
-            }
-            break;
-        }
+    break;
+  }
 
-        case Expr::NotOptimized:
-        { 
-            NotOptimizedExpr *noe = cast<NotOptimizedExpr>(e);
-            assert(noe);
-            res = construct(noe->src, width_out);
-            break;
-        }
-	
-        case Expr::Select: 
-        {
-            SelectExpr *se = cast<SelectExpr>(e);
-            assert(se);
-            res = evaluate(_solver, 
-                           metaSMT::logic::Ite(construct(se->cond, 0), 
-                                               construct(se->trueExpr, width_out),
-                                               construct(se->falseExpr, width_out)));
-            break;
-        }
+  case Expr::NotOptimized: {
+    NotOptimizedExpr *noe = cast<NotOptimizedExpr>(e);
+    assert(noe);
+    res = construct(noe->src, width_out);
+    break;
+  }
 
-        case Expr::Read:
-        {
-            ReadExpr *re = cast<ReadExpr>(e);
-            assert(re && re->updates.root);
-            *width_out = re->updates.root->getRange();
-            // FixMe call method of Array
-            res = evaluate(_solver, 
-                           metaSMT::logic::Array::select(
-                                  getArrayForUpdate(re->updates.root, re->updates.head),
-                                  construct(re->index, 0)));
-            break;
-        }
+  case Expr::Select: {
+    SelectExpr *se = cast<SelectExpr>(e);
+    assert(se);
+    res = evaluate(_solver,
+                   metaSMT::logic::Ite(construct(se->cond, 0),
+                                       construct(se->trueExpr, width_out),
+                                       construct(se->falseExpr, width_out)));
+    break;
+  }
 
-        case Expr::Concat:
-        {
-            ConcatExpr *ce = cast<ConcatExpr>(e);
-            assert(ce);
-            *width_out = ce->getWidth();
-            unsigned numKids = ce->getNumKids();
-
-            if (numKids > 0) {
-                res = evaluate(_solver, construct(ce->getKid(numKids-1), 0));
-                for (int i = numKids - 2; i >= 0; i--) {
-                    res = evaluate(_solver, concat(construct(ce->getKid(i), 0), res));
-                }
-            }
-            break;
-        }
+  case Expr::Read: {
+    ReadExpr *re = cast<ReadExpr>(e);
+    assert(re && re->updates.root);
+    *width_out = re->updates.root->getRange();
+    // FixMe call method of Array
+    res = evaluate(_solver,
+                   metaSMT::logic::Array::select(
+                       getArrayForUpdate(re->updates.root, re->updates.head),
+                       construct(re->index, 0)));
+    break;
+  }
 
-        case Expr::Extract:
-        {
-            ExtractExpr *ee = cast<ExtractExpr>(e);
-            assert(ee);
-            // ToDo spare evaluate?
-            typename SolverContext::result_type child = evaluate(_solver, construct(ee->expr, width_out));
+  case Expr::Concat: {
+    ConcatExpr *ce = cast<ConcatExpr>(e);
+    assert(ce);
+    *width_out = ce->getWidth();
+    unsigned numKids = ce->getNumKids();
+
+    if (numKids > 0) {
+      res = evaluate(_solver, construct(ce->getKid(numKids - 1), 0));
+      for (int i = numKids - 2; i >= 0; i--) {
+        res = evaluate(_solver, concat(construct(ce->getKid(i), 0), res));
+      }
+    }
+    break;
+  }
 
-            unsigned ee_width = ee->getWidth();
-            *width_out = ee_width;
+  case Expr::Extract: {
+    ExtractExpr *ee = cast<ExtractExpr>(e);
+    assert(ee);
+    // ToDo spare evaluate?
+    typename SolverContext::result_type child =
+        evaluate(_solver, construct(ee->expr, width_out));
 
-            if (ee_width == 1) {
-                res = bvBoolExtract(child, ee->offset);
-            }
-            else {
-                res = evaluate(_solver,
-                               extract(ee->offset + ee_width - 1, ee->offset, child));
-            }
-            break;
-        }
+    unsigned ee_width = ee->getWidth();
+    *width_out = ee_width;
 
-        case Expr::ZExt:
-        {
-            CastExpr *ce = cast<CastExpr>(e);
-            assert(ce);
+    if (ee_width == 1) {
+      res = bvBoolExtract(child, ee->offset);
+    } else {
+      res = evaluate(_solver,
+                     extract(ee->offset + ee_width - 1, ee->offset, child));
+    }
+    break;
+  }
 
-            int child_width = 0;
-            typename SolverContext::result_type child = evaluate(_solver, construct(ce->src, &child_width));
+  case Expr::ZExt: {
+    CastExpr *ce = cast<CastExpr>(e);
+    assert(ce);
 
-            unsigned ce_width = ce->getWidth();
-            *width_out = ce_width;
+    int child_width = 0;
+    typename SolverContext::result_type child =
+        evaluate(_solver, construct(ce->src, &child_width));
 
-            if (child_width == 1) {
-                res = evaluate(_solver, 
-                               metaSMT::logic::Ite(child, bvOne(ce_width), bvZero(ce_width)));			                       
-            }
-            else {
-                res = evaluate(_solver, zero_extend(ce_width - child_width, child));
-            }
+    unsigned ce_width = ce->getWidth();
+    *width_out = ce_width;
 
-            // ToDo calculate how many zeros to add
-            // Note: STP and metaSMT differ in the prototype arguments;
-            // STP requires the width of the resulting bv;
-            // whereas metaSMT (and Z3) require the width of the zero vector that is to be appended
-            // res = evaluate(_solver, zero_extend(ce_width, construct(ce->src)));
-    
-            break;	  
-        }
-  
-        case Expr::SExt:
-        {
-            CastExpr *ce = cast<CastExpr>(e);
-            assert(ce);
-    
-            int child_width = 0;
-            typename SolverContext::result_type child = evaluate(_solver, construct(ce->src, &child_width));
-            
-            unsigned ce_width = ce->getWidth();
-            *width_out = ce_width;
-    
-            if (child_width == 1) {
-                res = evaluate(_solver, 
-                               metaSMT::logic::Ite(child, bvMinusOne(ce_width), bvZero(ce_width)));
-            }
-            else {
-                // ToDo ce_width - child_width? It is only ce_width in STPBuilder
-                res = evaluate(_solver, sign_extend(ce_width - child_width, child));
-            }
+    if (child_width == 1) {
+      res = evaluate(_solver, metaSMT::logic::Ite(child, bvOne(ce_width),
+                                                  bvZero(ce_width)));
+    } else {
+      res = evaluate(_solver, zero_extend(ce_width - child_width, child));
+    }
 
-            break;
-        }
-  
-        case Expr::Add:
-        {
-            AddExpr *ae = cast<AddExpr>(e);
-            assert(ae);	    
-            res = evaluate(_solver, bvadd(construct(ae->left, width_out), construct(ae->right, width_out)));
-            assert(*width_out != 1 && "uncanonicalized add");
-            break;	  
-        }  
-  
-        case Expr::Sub:  
-        {
-            SubExpr *se = cast<SubExpr>(e);
-            assert(se);	    
-            res = evaluate(_solver, bvsub(construct(se->left, width_out), construct(se->right, width_out))); 
-            assert(*width_out != 1 && "uncanonicalized sub");
-            break;	  
-        }  
-   
-        case Expr::Mul:
-        { 
-            MulExpr *me = cast<MulExpr>(e);
-            assert(me);
-    
-            typename SolverContext::result_type right_expr = evaluate(_solver, construct(me->right, width_out));
-            assert(*width_out != 1 && "uncanonicalized mul");
-    
-            ConstantExpr *CE = dyn_cast<ConstantExpr>(me->left);
-            if (CE && (CE->getWidth() <= 64)) {	        		
-                res = constructMulByConstant(right_expr, *width_out, CE->getZExtValue());		
-            }
-            else {
-                res = evaluate(_solver, bvmul(construct(me->left, width_out), right_expr));	     
-            }
-            break;
-        }
+    // ToDo calculate how many zeros to add
+    // Note: STP and metaSMT differ in the prototype arguments;
+    // STP requires the width of the resulting bv;
+    // whereas metaSMT (and Z3) require the width of the zero vector that is to
+    // be appended
+    // res = evaluate(_solver, zero_extend(ce_width, construct(ce->src)));
 
-        case Expr::UDiv:
-        {
-            UDivExpr *de = cast<UDivExpr>(e);
-            assert(de);
-
-            typename SolverContext::result_type left_expr = construct(de->left, width_out);
-            assert(*width_out != 1 && "uncanonicalized udiv");
-            bool construct_both = true;
-
-            ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right);
-            if (CE && (CE->getWidth() <= 64)) {
-                uint64_t divisor = CE->getZExtValue();
-                if (bits64::isPowerOfTwo(divisor)) {
-                    res = bvRightShift(left_expr, *width_out, bits64::indexOfSingleBit(divisor), getShiftBits(*width_out));
-                    construct_both = false;
-                }
-                else if (_optimizeDivides) {
-                    if (*width_out == 32) { //only works for 32-bit division
-                        res = constructUDivByConstant(left_expr, *width_out, (uint32_t) divisor);
-                        construct_both = false;
-                    }
-                }
-            }
+    break;
+  }
 
-            if (construct_both) {	    
-                res = evaluate(_solver, bvudiv(left_expr, construct(de->right, width_out))); 
-            }
-            break;
-        }
+  case Expr::SExt: {
+    CastExpr *ce = cast<CastExpr>(e);
+    assert(ce);
 
-        case Expr::SDiv:
-        {
-            SDivExpr *de = cast<SDivExpr>(e);
-            assert(de);
+    int child_width = 0;
+    typename SolverContext::result_type child =
+        evaluate(_solver, construct(ce->src, &child_width));
 
-            typename SolverContext::result_type left_expr = construct(de->left, width_out);
-            assert(*width_out != 1 && "uncanonicalized sdiv");
+    unsigned ce_width = ce->getWidth();
+    *width_out = ce_width;
 
-            ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right);
-            if (CE && _optimizeDivides && (*width_out == 32)) {
-                res = constructSDivByConstant(left_expr, *width_out, CE->getZExtValue(32));
-            }
-            else {
-                res = evaluate(_solver, bvsdiv(left_expr, construct(de->right, width_out))); 
-            }
-            break;
+    if (child_width == 1) {
+      res = evaluate(_solver, metaSMT::logic::Ite(child, bvMinusOne(ce_width),
+                                                  bvZero(ce_width)));
+    } else {
+      // ToDo ce_width - child_width? It is only ce_width in STPBuilder
+      res = evaluate(_solver, sign_extend(ce_width - child_width, child));
+    }
+
+    break;
+  }
+
+  case Expr::Add: {
+    AddExpr *ae = cast<AddExpr>(e);
+    assert(ae);
+    res = evaluate(_solver, bvadd(construct(ae->left, width_out),
+                                  construct(ae->right, width_out)));
+    assert(*width_out != 1 && "uncanonicalized add");
+    break;
+  }
+
+  case Expr::Sub: {
+    SubExpr *se = cast<SubExpr>(e);
+    assert(se);
+    res = evaluate(_solver, bvsub(construct(se->left, width_out),
+                                  construct(se->right, width_out)));
+    assert(*width_out != 1 && "uncanonicalized sub");
+    break;
+  }
+
+  case Expr::Mul: {
+    MulExpr *me = cast<MulExpr>(e);
+    assert(me);
+
+    typename SolverContext::result_type right_expr =
+        evaluate(_solver, construct(me->right, width_out));
+    assert(*width_out != 1 && "uncanonicalized mul");
+
+    ConstantExpr *CE = dyn_cast<ConstantExpr>(me->left);
+    if (CE && (CE->getWidth() <= 64)) {
+      res = constructMulByConstant(right_expr, *width_out, CE->getZExtValue());
+    } else {
+      res =
+          evaluate(_solver, bvmul(construct(me->left, width_out), right_expr));
+    }
+    break;
+  }
+
+  case Expr::UDiv: {
+    UDivExpr *de = cast<UDivExpr>(e);
+    assert(de);
+
+    typename SolverContext::result_type left_expr =
+        construct(de->left, width_out);
+    assert(*width_out != 1 && "uncanonicalized udiv");
+    bool construct_both = true;
+
+    ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right);
+    if (CE && (CE->getWidth() <= 64)) {
+      uint64_t divisor = CE->getZExtValue();
+      if (bits64::isPowerOfTwo(divisor)) {
+        res = bvRightShift(left_expr, *width_out,
+                           bits64::indexOfSingleBit(divisor));
+        construct_both = false;
+      } else if (_optimizeDivides) {
+        if (*width_out == 32) { // only works for 32-bit division
+          res =
+              constructUDivByConstant(left_expr, *width_out, (uint32_t)divisor);
+          construct_both = false;
         }
+      }
+    }
 
-        case Expr::URem:
-        {
-            URemExpr *de = cast<URemExpr>(e);
-            assert(de);
+    if (construct_both) {
+      res =
+          evaluate(_solver, bvudiv(left_expr, construct(de->right, width_out)));
+    }
+    break;
+  }
 
-            typename SolverContext::result_type left_expr = construct(de->left, width_out);
-            assert(*width_out != 1 && "uncanonicalized urem");
-    
-            bool construct_both = true;
-            ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right);
-            if (CE && (CE->getWidth() <= 64)) {
-      
-                uint64_t divisor = CE->getZExtValue();
-
-                if (bits64::isPowerOfTwo(divisor)) {
-  
-                    unsigned bits = bits64::indexOfSingleBit(divisor);		  
-                    // special case for modding by 1 or else we bvExtract -1:0
-                    if (bits == 0) {
-                        res = bvZero(*width_out);
-                        construct_both = false;
-                    }
-                    else {
-                        res = evaluate(_solver, concat(bvZero(*width_out - bits), 
-                                                       bvExtract(left_expr, bits - 1, 0)));
-                        construct_both = false;
-                    }
-                }
+  case Expr::SDiv: {
+    SDivExpr *de = cast<SDivExpr>(e);
+    assert(de);
+
+    typename SolverContext::result_type left_expr =
+        construct(de->left, width_out);
+    assert(*width_out != 1 && "uncanonicalized sdiv");
+
+    bool optimized = false;
+    ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right);
+    if (CE && _optimizeDivides && (*width_out == 32)) {
+      llvm::APInt divisor = CE->getAPValue();
+      if (divisor != llvm::APInt(CE->getWidth(), 1, false /*unsigned*/) &&
+          divisor != llvm::APInt(CE->getWidth(), -1, true /*signed*/)) {
+        res = constructSDivByConstant(left_expr, *width_out,
+                                      CE->getZExtValue(32));
+        optimized = true;
+      }
+    }
+    if (!optimized) {
+      res =
+          evaluate(_solver, bvsdiv(left_expr, construct(de->right, width_out)));
+    }
+    break;
+  }
 
-                // Use fast division to compute modulo without explicit division for constant divisor.
-       
-                if (_optimizeDivides && *width_out == 32) { //only works for 32-bit division
-                    typename SolverContext::result_type quotient = constructUDivByConstant(left_expr, *width_out, (uint32_t) divisor);
-                    typename SolverContext::result_type quot_times_divisor = constructMulByConstant(quotient, *width_out, divisor);
-                    res = evaluate(_solver, bvsub(left_expr, quot_times_divisor));                    
-                    construct_both = false;
-                }
-            }
-    
-            if (construct_both) {
-                res = evaluate(_solver, bvurem(left_expr, construct(de->right, width_out)));	      
-            }
-            break;  
+  case Expr::URem: {
+    URemExpr *de = cast<URemExpr>(e);
+    assert(de);
+
+    typename SolverContext::result_type left_expr =
+        construct(de->left, width_out);
+    assert(*width_out != 1 && "uncanonicalized urem");
+
+    bool construct_both = true;
+    ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right);
+    if (CE && (CE->getWidth() <= 64)) {
+
+      uint64_t divisor = CE->getZExtValue();
+
+      if (bits64::isPowerOfTwo(divisor)) {
+
+        unsigned bits = bits64::indexOfSingleBit(divisor);
+        // special case for modding by 1 or else we bvExtract -1:0
+        if (bits == 0) {
+          res = bvZero(*width_out);
+          construct_both = false;
+        } else {
+          res = evaluate(_solver, concat(bvZero(*width_out - bits),
+                                         bvExtract(left_expr, bits - 1, 0)));
+          construct_both = false;
         }
+      }
+
+      // Use fast division to compute modulo without explicit division for
+      // constant divisor.
+
+      if (_optimizeDivides &&
+          *width_out == 32) { // only works for 32-bit division
+        typename SolverContext::result_type quotient =
+            constructUDivByConstant(left_expr, *width_out, (uint32_t)divisor);
+        typename SolverContext::result_type quot_times_divisor =
+            constructMulByConstant(quotient, *width_out, divisor);
+        res = evaluate(_solver, bvsub(left_expr, quot_times_divisor));
+        construct_both = false;
+      }
+    }
 
-        case Expr::SRem:
-        {
-            SRemExpr *de = cast<SRemExpr>(e);
-            assert(de);
-    
-            typename SolverContext::result_type left_expr = evaluate(_solver, construct(de->left, width_out));
-            typename SolverContext::result_type right_expr = evaluate(_solver, construct(de->right, width_out));
-            assert(*width_out != 1 && "uncanonicalized srem");
-    
-            bool construct_both = true;
-    
-#if 0 //not faster per first benchmark
+    if (construct_both) {
+      res =
+          evaluate(_solver, bvurem(left_expr, construct(de->right, width_out)));
+    }
+    break;
+  }
+
+  case Expr::SRem: {
+    SRemExpr *de = cast<SRemExpr>(e);
+    assert(de);
+
+    typename SolverContext::result_type left_expr =
+        evaluate(_solver, construct(de->left, width_out));
+    typename SolverContext::result_type right_expr =
+        evaluate(_solver, construct(de->right, width_out));
+    assert(*width_out != 1 && "uncanonicalized srem");
+
+    bool construct_both = true;
+
+#if 0 // not faster per first benchmark
             
             if (_optimizeDivides) {
                 if (ConstantExpr *cre = de->right->asConstant()) {
@@ -935,257 +986,259 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActu
                     }
                 }
             }
-    
+
 #endif
 
-            if (construct_both) {     
-                res = evaluate(_solver, bvsrem(left_expr, right_expr));
-            }
-            break;
-        }
+    if (construct_both) {
+      res = evaluate(_solver, bvsrem(left_expr, right_expr));
+    }
+    break;
+  }
 
-        case Expr::Not:
-        {
-            NotExpr *ne = cast<NotExpr>(e);
-            assert(ne);
-    
-            typename SolverContext::result_type child = evaluate(_solver, construct(ne->expr, width_out));
-            if (*width_out == 1) {
-                res = evaluate(_solver, metaSMT::logic::Not(child));
-            }
-            else {                
-                res = evaluate(_solver, bvnot(child));
-            }    
-            break;	  
-        }
-  
-        case Expr::And:
-        {
-            AndExpr *ae = cast<AndExpr>(e);
-	    assert(ae);
-	    
-	    typename SolverContext::result_type left_expr = evaluate(_solver, construct(ae->left, width_out));
-	    typename SolverContext::result_type right_expr = evaluate(_solver, construct(ae->right, width_out));
-	    
-	    if (*width_out == 1) {
-	        res = evaluate(_solver, metaSMT::logic::And(left_expr, right_expr));
-	    }
-	    else {
-	        res = evaluate(_solver, bvand(left_expr, right_expr));
-	    }
-	    
-	    break;	  
-	}
-	  
-	case Expr::Or:
-	{
-	    OrExpr *oe = cast<OrExpr>(e);
-	    assert(oe);
-	    
-	    typename SolverContext::result_type left_expr = evaluate(_solver, construct(oe->left, width_out));
-	    typename SolverContext::result_type right_expr = evaluate(_solver, construct(oe->right, width_out));
-	    
-	    if (*width_out == 1) {
-	        res = evaluate(_solver, metaSMT::logic::Or(left_expr, right_expr));
-	    }
-	    else {
-	        res = evaluate(_solver, bvor(left_expr, right_expr));
-	    }
-	    
-	    break;	  
-	}
-	  
-	case Expr::Xor:
-	{
-	    XorExpr *xe = cast<XorExpr>(e);
-	    assert(xe);
-	    
-	    typename SolverContext::result_type left_expr = evaluate(_solver, construct(xe->left, width_out));
-	    typename SolverContext::result_type right_expr = evaluate(_solver, construct(xe->right, width_out));
-	    
-	    if (*width_out == 1) {
-	        res = evaluate(_solver, metaSMT::logic::Xor(left_expr, right_expr));
-	    }
-	    else {
-	        res = evaluate(_solver, bvxor(left_expr, right_expr));
-	    }
-	    
-	    break;	  
-	}
-	  
-	case Expr::Shl:  
-	{	    
-	    ShlExpr *se = cast<ShlExpr>(e);
-	    assert(se);
-	    
-	    typename SolverContext::result_type left_expr = evaluate(_solver, construct(se->left, width_out));
-	    assert(*width_out != 1 && "uncanonicalized shl");
-	    
-	    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(se->right)) {
-	        res =  bvLeftShift(left_expr, *width_out, (unsigned) CE->getLimitedValue(), getShiftBits(*width_out));
-            }
-            else {
-                int shiftWidth = 0;
-		typename SolverContext::result_type right_expr = evaluate(_solver, construct(se->right, &shiftWidth));
-		res = mimic_stp ? bvVarLeftShift(left_expr, right_expr, *width_out) : 
-		                  evaluate(_solver, bvshl(left_expr, right_expr));	      
-	    }    
-	    
-	    break;	  
-	}
-	
-	case Expr::LShr:
-	{
-	    LShrExpr *lse = cast<LShrExpr>(e);
-	    assert(lse);
-	    
-	    typename SolverContext::result_type left_expr = evaluate(_solver, construct(lse->left, width_out));	    
-	    assert(*width_out != 1 && "uncanonicalized lshr");
-	    
-	    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(lse->right)) {
-	        res =  bvRightShift(left_expr, *width_out, (unsigned) CE->getLimitedValue(), getShiftBits(*width_out));
-	    }
-	    else {
-                int shiftWidth = 0;
-		typename SolverContext::result_type right_expr = evaluate(_solver, construct(lse->right, &shiftWidth));
-		res = mimic_stp ? bvVarRightShift(left_expr, right_expr, *width_out) :
-				  evaluate(_solver, bvshr(left_expr, right_expr));
-	    }
-	    
-	    break;	  
-	}
-	  
-	case Expr::AShr:  
-	{
-	    AShrExpr *ase = cast<AShrExpr>(e);
-	    assert(ase);
-	    
-	    typename SolverContext::result_type left_expr = evaluate(_solver, construct(ase->left, width_out));	    
-	    assert(*width_out != 1 && "uncanonicalized ashr");
-	    
-	    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ase->right)) {
-	        unsigned shift = (unsigned) CE->getLimitedValue();
-                typename SolverContext::result_type signedBool = bvBoolExtract(left_expr, *width_out - 1);
-		res = constructAShrByConstant(left_expr, *width_out, shift, signedBool, getShiftBits(*width_out));	      
-	    }
-	    else {
-                int shiftWidth = 0;
-		typename SolverContext::result_type right_expr = evaluate(_solver, construct(ase->right, &shiftWidth));
-		res = mimic_stp ? bvVarArithRightShift(left_expr, right_expr, *width_out) :
-		                  evaluate(_solver, bvashr(left_expr, right_expr)); 
-	    }    
-	    
-	    break;	  
-	}
-	  
-	case Expr::Eq: 
-	{
-	     EqExpr *ee = cast<EqExpr>(e);
-	     assert(ee);
-	     
-    	     typename SolverContext::result_type left_expr = evaluate(_solver, construct(ee->left, width_out));
-	     typename SolverContext::result_type right_expr = evaluate(_solver, construct(ee->right, width_out));
-
-	     if (*width_out==1) {
-	         if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ee->left)) {
-		     if (CE->isTrue()) {
-		         res = right_expr;  
-		     }
-		     else {
-		         res = evaluate(_solver, metaSMT::logic::Not(right_expr));
-		     }
-		 }
-		 else {
-		     res = evaluate(_solver, metaSMT::logic::equal(left_expr, right_expr));
-		 }
-	     } // end of *width_out == 1
-	     else {
-	         *width_out = 1;
-	         res = evaluate(_solver, metaSMT::logic::equal(left_expr, right_expr));
-	     }
-	     
-	     break;
-	}
-	
-	case Expr::Ult:
-	{
-	    UltExpr *ue = cast<UltExpr>(e);
-	    assert(ue);
-	    
-	    typename SolverContext::result_type left_expr = evaluate(_solver, construct(ue->left, width_out));
-	    typename SolverContext::result_type right_expr = evaluate(_solver, construct(ue->right, width_out));	    
-	    
-	    assert(*width_out != 1 && "uncanonicalized ult");
-	    *width_out = 1;    
-	    
-	    res = evaluate(_solver, bvult(left_expr, right_expr));
-	    break;	  
-	}
-	  
-	case Expr::Ule:
-	{
-	    UleExpr *ue = cast<UleExpr>(e);
-	    assert(ue);
-	    
-	    typename SolverContext::result_type left_expr = evaluate(_solver, construct(ue->left, width_out));
-	    typename SolverContext::result_type right_expr = evaluate(_solver, construct(ue->right, width_out));	
-	    
-	    assert(*width_out != 1 && "uncanonicalized ule");
-	    *width_out = 1;    
-	    
-	    res = evaluate(_solver, bvule(left_expr, right_expr));
-	    break;	  
-	}
-	  
-	case Expr::Slt:
-	{
-	    SltExpr *se = cast<SltExpr>(e);
-	    assert(se);
-	    
-	    typename SolverContext::result_type left_expr = evaluate(_solver, construct(se->left, width_out));
-	    typename SolverContext::result_type right_expr = evaluate(_solver, construct(se->right, width_out));	
-	    
-	    assert(*width_out != 1 && "uncanonicalized slt");
-	    *width_out = 1;
-	    
-	    res = evaluate(_solver, bvslt(left_expr, right_expr));
-	    break;	  
-	}
-	  
-        case Expr::Sle:
-        {
-            SleExpr *se = cast<SleExpr>(e);
-            assert(se);
-    
-            typename SolverContext::result_type left_expr = evaluate(_solver, construct(se->left, width_out));
-            typename SolverContext::result_type right_expr = evaluate(_solver, construct(se->right, width_out));	
-    
-            assert(*width_out != 1 && "uncanonicalized sle");
-            *width_out = 1;    
-    
-            res = evaluate(_solver, bvsle(left_expr, right_expr));
-            break;	  
+  case Expr::Not: {
+    NotExpr *ne = cast<NotExpr>(e);
+    assert(ne);
+
+    typename SolverContext::result_type child =
+        evaluate(_solver, construct(ne->expr, width_out));
+    if (*width_out == 1) {
+      res = evaluate(_solver, metaSMT::logic::Not(child));
+    } else {
+      res = evaluate(_solver, bvnot(child));
+    }
+    break;
+  }
+
+  case Expr::And: {
+    AndExpr *ae = cast<AndExpr>(e);
+    assert(ae);
+
+    typename SolverContext::result_type left_expr =
+        evaluate(_solver, construct(ae->left, width_out));
+    typename SolverContext::result_type right_expr =
+        evaluate(_solver, construct(ae->right, width_out));
+
+    if (*width_out == 1) {
+      res = evaluate(_solver, metaSMT::logic::And(left_expr, right_expr));
+    } else {
+      res = evaluate(_solver, bvand(left_expr, right_expr));
+    }
+
+    break;
+  }
+
+  case Expr::Or: {
+    OrExpr *oe = cast<OrExpr>(e);
+    assert(oe);
+
+    typename SolverContext::result_type left_expr =
+        evaluate(_solver, construct(oe->left, width_out));
+    typename SolverContext::result_type right_expr =
+        evaluate(_solver, construct(oe->right, width_out));
+
+    if (*width_out == 1) {
+      res = evaluate(_solver, metaSMT::logic::Or(left_expr, right_expr));
+    } else {
+      res = evaluate(_solver, bvor(left_expr, right_expr));
+    }
+
+    break;
+  }
+
+  case Expr::Xor: {
+    XorExpr *xe = cast<XorExpr>(e);
+    assert(xe);
+
+    typename SolverContext::result_type left_expr =
+        evaluate(_solver, construct(xe->left, width_out));
+    typename SolverContext::result_type right_expr =
+        evaluate(_solver, construct(xe->right, width_out));
+
+    if (*width_out == 1) {
+      res = evaluate(_solver, metaSMT::logic::Xor(left_expr, right_expr));
+    } else {
+      res = evaluate(_solver, bvxor(left_expr, right_expr));
+    }
+
+    break;
+  }
+
+  case Expr::Shl: {
+    ShlExpr *se = cast<ShlExpr>(e);
+    assert(se);
+
+    typename SolverContext::result_type left_expr =
+        evaluate(_solver, construct(se->left, width_out));
+    assert(*width_out != 1 && "uncanonicalized shl");
+
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(se->right)) {
+      res = bvLeftShift(left_expr, *width_out, (unsigned)CE->getLimitedValue());
+    } else {
+      int shiftWidth = 0;
+      typename SolverContext::result_type right_expr =
+          evaluate(_solver, construct(se->right, &shiftWidth));
+      res = mimic_stp ? bvVarLeftShift(left_expr, right_expr, *width_out)
+                      : evaluate(_solver, bvshl(left_expr, right_expr));
+    }
+
+    break;
+  }
+
+  case Expr::LShr: {
+    LShrExpr *lse = cast<LShrExpr>(e);
+    assert(lse);
+
+    typename SolverContext::result_type left_expr =
+        evaluate(_solver, construct(lse->left, width_out));
+    assert(*width_out != 1 && "uncanonicalized lshr");
+
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(lse->right)) {
+      res =
+          bvRightShift(left_expr, *width_out, (unsigned)CE->getLimitedValue());
+    } else {
+      int shiftWidth = 0;
+      typename SolverContext::result_type right_expr =
+          evaluate(_solver, construct(lse->right, &shiftWidth));
+      res = mimic_stp ? bvVarRightShift(left_expr, right_expr, *width_out)
+                      : evaluate(_solver, bvshr(left_expr, right_expr));
+    }
+
+    break;
+  }
+
+  case Expr::AShr: {
+    AShrExpr *ase = cast<AShrExpr>(e);
+    assert(ase);
+
+    typename SolverContext::result_type left_expr =
+        evaluate(_solver, construct(ase->left, width_out));
+    assert(*width_out != 1 && "uncanonicalized ashr");
+
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ase->right)) {
+      unsigned shift = (unsigned)CE->getLimitedValue();
+      typename SolverContext::result_type signedBool =
+          bvBoolExtract(left_expr, *width_out - 1);
+      res = constructAShrByConstant(left_expr, *width_out, shift, signedBool);
+    } else {
+      int shiftWidth = 0;
+      typename SolverContext::result_type right_expr =
+          evaluate(_solver, construct(ase->right, &shiftWidth));
+      res = mimic_stp ? bvVarArithRightShift(left_expr, right_expr, *width_out)
+                      : evaluate(_solver, bvashr(left_expr, right_expr));
+    }
+
+    break;
+  }
+
+  case Expr::Eq: {
+    EqExpr *ee = cast<EqExpr>(e);
+    assert(ee);
+
+    typename SolverContext::result_type left_expr =
+        evaluate(_solver, construct(ee->left, width_out));
+    typename SolverContext::result_type right_expr =
+        evaluate(_solver, construct(ee->right, width_out));
+
+    if (*width_out == 1) {
+      if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ee->left)) {
+        if (CE->isTrue()) {
+          res = right_expr;
+        } else {
+          res = evaluate(_solver, metaSMT::logic::Not(right_expr));
         }
-  
-        // unused due to canonicalization
+      } else {
+        res = evaluate(_solver, metaSMT::logic::equal(left_expr, right_expr));
+      }
+    } // end of *width_out == 1
+    else {
+      *width_out = 1;
+      res = evaluate(_solver, metaSMT::logic::equal(left_expr, right_expr));
+    }
+
+    break;
+  }
+
+  case Expr::Ult: {
+    UltExpr *ue = cast<UltExpr>(e);
+    assert(ue);
+
+    typename SolverContext::result_type left_expr =
+        evaluate(_solver, construct(ue->left, width_out));
+    typename SolverContext::result_type right_expr =
+        evaluate(_solver, construct(ue->right, width_out));
+
+    assert(*width_out != 1 && "uncanonicalized ult");
+    *width_out = 1;
+
+    res = evaluate(_solver, bvult(left_expr, right_expr));
+    break;
+  }
+
+  case Expr::Ule: {
+    UleExpr *ue = cast<UleExpr>(e);
+    assert(ue);
+
+    typename SolverContext::result_type left_expr =
+        evaluate(_solver, construct(ue->left, width_out));
+    typename SolverContext::result_type right_expr =
+        evaluate(_solver, construct(ue->right, width_out));
+
+    assert(*width_out != 1 && "uncanonicalized ule");
+    *width_out = 1;
+
+    res = evaluate(_solver, bvule(left_expr, right_expr));
+    break;
+  }
+
+  case Expr::Slt: {
+    SltExpr *se = cast<SltExpr>(e);
+    assert(se);
+
+    typename SolverContext::result_type left_expr =
+        evaluate(_solver, construct(se->left, width_out));
+    typename SolverContext::result_type right_expr =
+        evaluate(_solver, construct(se->right, width_out));
+
+    assert(*width_out != 1 && "uncanonicalized slt");
+    *width_out = 1;
+
+    res = evaluate(_solver, bvslt(left_expr, right_expr));
+    break;
+  }
+
+  case Expr::Sle: {
+    SleExpr *se = cast<SleExpr>(e);
+    assert(se);
+
+    typename SolverContext::result_type left_expr =
+        evaluate(_solver, construct(se->left, width_out));
+    typename SolverContext::result_type right_expr =
+        evaluate(_solver, construct(se->right, width_out));
+
+    assert(*width_out != 1 && "uncanonicalized sle");
+    *width_out = 1;
+
+    res = evaluate(_solver, bvsle(left_expr, right_expr));
+    break;
+  }
+
+// unused due to canonicalization
 #if 0
         case Expr::Ne:
         case Expr::Ugt:
         case Expr::Uge:
         case Expr::Sgt:
         case Expr::Sge:
-#endif  
-     
-        default:
-             assert(false);
-             break;      
-      
-    };
-    return res;
-}
+#endif
 
+  default:
+    assert(false);
+    break;
+  };
+  return res;
+}
 
-}  /* end of namespace klee */
+} /* end of namespace klee */
 
 #endif /* ENABLE_METASMT */
 
diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp
index c4f6a5d0..56964b5d 100644
--- a/lib/Solver/MetaSMTSolver.cpp
+++ b/lib/Solver/MetaSMTSolver.cpp
@@ -19,11 +19,15 @@
 #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>
 
+#define Expr VCExpr
+#define Type VCType
+#define STP STP_Backend
+#include <metaSMT/backend/STP.hpp>
+#undef Expr
+#undef Type
+#undef STP
+  
 #include <errno.h>
 #include <unistd.h>
 #include <signal.h>