about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
-rw-r--r--.clang-format4
-rw-r--r--.dockerignore3
-rw-r--r--.gitattributes5
-rwxr-xr-x.travis/klee.sh2
-rwxr-xr-x.travis/stp.sh12
-rw-r--r--Dockerfile128
-rw-r--r--Makefile.common7
-rw-r--r--Makefile.config.in4
-rw-r--r--Makefile.rules4
-rw-r--r--autoconf/configure.ac22
-rwxr-xr-xconfigure1136
-rw-r--r--include/klee/ExecutionState.h107
-rw-r--r--include/klee/Internal/Module/KInstruction.h2
-rw-r--r--include/klee/Internal/Module/KModule.h2
-rw-r--r--include/klee/Internal/System/Time.h9
-rw-r--r--include/klee/klee.h77
-rw-r--r--include/klee/util/ExprSMTLIBPrinter.h1
-rw-r--r--lib/Core/ExecutionState.cpp33
-rw-r--r--lib/Core/Executor.cpp4
-rw-r--r--lib/Core/Memory.cpp4
-rw-r--r--lib/Core/TimingSolver.cpp23
-rw-r--r--lib/Expr/Constraints.cpp31
-rw-r--r--lib/Expr/ExprSMTLIBPrinter.cpp73
-rw-r--r--lib/Module/RaiseAsm.cpp10
-rw-r--r--lib/Solver/STPBuilder.cpp26
-rw-r--r--lib/Support/Time.cpp10
-rw-r--r--lib/Support/Timer.cpp10
-rw-r--r--runtime/Intrinsic/klee_int.c2
-rw-r--r--runtime/klee-libc/__cxa_atexit.c4
-rw-r--r--runtime/klee-libc/abort.c4
-rw-r--r--runtime/klee-libc/atexit.c4
-rw-r--r--runtime/klee-libc/calloc.c15
-rw-r--r--runtime/klee-libc/htonl.c6
-rw-r--r--runtime/klee-libc/klee-choose.c6
-rw-r--r--runtime/klee-libc/memcpy.c4
-rw-r--r--runtime/klee-libc/memmove.c4
-rw-r--r--runtime/klee-libc/mempcpy.c4
-rw-r--r--runtime/klee-libc/memset.c4
-rw-r--r--runtime/klee-libc/putchar.c6
-rw-r--r--runtime/klee-libc/strchr.c4
-rw-r--r--runtime/klee-libc/strcmp.c4
-rw-r--r--runtime/klee-libc/strcoll.c6
-rw-r--r--runtime/klee-libc/strcpy.c4
-rw-r--r--runtime/klee-libc/strlen.c4
-rw-r--r--runtime/klee-libc/strrchr.c4
-rw-r--r--runtime/klee-libc/tolower.c4
-rw-r--r--runtime/klee-libc/toupper.c4
-rw-r--r--test/Feature/arithmetic-right-overshift-sym-conc.c25
-rw-r--r--test/Programs/pcregrep.c4
-rw-r--r--test/Runtime/Uclibc/2007-10-08-optimization-calls-wrong-libc-functions.c4
-rw-r--r--test/Solver/AShr_to_smtlib.kquery16
-rw-r--r--test/Solver/AShr_to_smtlib.kquery.good.smt27
-rw-r--r--tools/kleaver/Makefile2
-rw-r--r--tools/klee/Makefile2
-rw-r--r--tools/klee/main.cpp6
-rw-r--r--unittests/Expr/Makefile2
-rw-r--r--unittests/Ref/Makefile2
-rw-r--r--unittests/Solver/Makefile2
-rw-r--r--utils/hacks/TreeGraphs/Graphics/Canvas/__init__.py410
-rw-r--r--utils/hacks/TreeGraphs/Graphics/Geometry/Intersect2D.py118
-rw-r--r--utils/hacks/TreeGraphs/Graphics/Geometry/mat2.py40
-rw-r--r--utils/hacks/TreeGraphs/Graphics/Geometry/mat3.py80
-rw-r--r--utils/hacks/TreeGraphs/Graphics/Geometry/mat4.py304
-rw-r--r--utils/hacks/TreeGraphs/Graphics/Geometry/quat.py214
-rw-r--r--utils/hacks/TreeGraphs/Graphics/Geometry/vec2.py158
-rw-r--r--utils/hacks/TreeGraphs/Graphics/Geometry/vec3.py110
-rw-r--r--utils/hacks/TreeGraphs/Graphics/Geometry/vec4.py92
-rw-r--r--utils/hacks/TreeGraphs/Graphics/__init__.py2
68 files changed, 1833 insertions, 1613 deletions
diff --git a/.clang-format b/.clang-format
new file mode 100644
index 00000000..4f679309
--- /dev/null
+++ b/.clang-format
@@ -0,0 +1,4 @@
+---
+Language: Cpp
+BasedOnStyle:  LLVM
+...
diff --git a/.dockerignore b/.dockerignore
new file mode 100644
index 00000000..b3d5b5a0
--- /dev/null
+++ b/.dockerignore
@@ -0,0 +1,3 @@
+.git
+autom4te.cache
+.*.swp
diff --git a/.gitattributes b/.gitattributes
new file mode 100644
index 00000000..2098a079
--- /dev/null
+++ b/.gitattributes
@@ -0,0 +1,5 @@
+* text=auto
+
+*.h text
+*.c text
+*.cpp text
diff --git a/.travis/klee.sh b/.travis/klee.sh
index faf3f5f5..3106dca9 100755
--- a/.travis/klee.sh
+++ b/.travis/klee.sh
@@ -33,7 +33,7 @@ if [ "${KLEE_UCLIBC}" -eq 1 ]; then
     cd klee-uclibc
     ./configure --make-llvm-lib --with-cc "${KLEE_CC}" --with-llvm-config /usr/bin/llvm-config-${LLVM_VERSION}
     make
-    KLEE_UCLIBC_CONFIGURE_OPTION="--with-uclibc=$(pwd) --with-posix-runtime"
+    KLEE_UCLIBC_CONFIGURE_OPTION="--with-uclibc=$(pwd) --enable-posix-runtime"
     cd ../
 else
     KLEE_UCLIBC_CONFIGURE_OPTION=""
diff --git a/.travis/stp.sh b/.travis/stp.sh
index abc4e566..89d89909 100755
--- a/.travis/stp.sh
+++ b/.travis/stp.sh
@@ -6,6 +6,18 @@ set -e
 STP_LOG="$(pwd)/stp-build.log"
 
 if [ "${STP_VERSION}" == "UPSTREAM" ]; then
+    # Build minisat
+    git clone https://github.com/stp/minisat
+    cd minisat
+    mkdir build
+    cd build
+    MINISAT_DIR=`pwd`
+    cmake -DCMAKE_INSTALL_PREFIX=/usr ..
+    make
+    sudo make install
+    cd ../../
+
+    # Build STP
     git clone --depth 1 git://github.com/stp/stp.git src
     mkdir build
     cd build
diff --git a/Dockerfile b/Dockerfile
new file mode 100644
index 00000000..07f1bb48
--- /dev/null
+++ b/Dockerfile
@@ -0,0 +1,128 @@
+FROM ubuntu:14.04
+MAINTAINER Dan Liew <daniel.liew@imperial.ac.uk>
+
+# FIXME: Docker doesn't currently offer a way to
+# squash the layers from within a Dockerfile so
+# the resulting image is unnecessarily large!
+
+ENV LLVM_VERSION=3.4 \
+    STP_VERSION=UPSTREAM \
+    DISABLE_ASSERTIONS=0 \
+    ENABLE_OPTIMIZED=1 \
+    KLEE_UCLIBC=1 \
+    KLEE_SRC=/home/klee/klee_src \
+    BUILD_DIR=/home/klee/klee_build
+
+RUN apt-get update && \
+    apt-get -y --no-install-recommends install \
+        clang-${LLVM_VERSION} \
+        llvm-${LLVM_VERSION} \
+        llvm-${LLVM_VERSION}-dev \
+        llvm-${LLVM_VERSION}-runtime \
+        llvm \
+        libcap-dev \
+        git \
+        subversion \
+        cmake \
+        make \
+        libboost-program-options-dev \
+        python3 \
+        python3-dev \
+        python3-pip \
+        perl \
+        flex \
+        bison \
+        libncurses-dev \
+        zlib1g-dev \
+        patch \
+        wget \
+        unzip \
+        binutils && \
+    pip3 install -U lit tabulate && \
+    update-alternatives --install /usr/bin/python python /usr/bin/python3 50
+
+# Create ``klee`` user for container with password ``klee``.
+# and give it password-less sudo access (temporarily so we can use the TravisCI scripts)
+RUN useradd -m klee && \
+    echo klee:klee | chpasswd && \
+    cp /etc/sudoers /etc/sudoers.bak && \
+    echo 'klee  ALL=(root) NOPASSWD: ALL' >> /etc/sudoers
+USER klee
+WORKDIR /home/klee
+
+# Copy across source files needed for build
+RUN mkdir ${KLEE_SRC}
+ADD configure \
+    LICENSE.TXT \
+    Makefile \
+    Makefile.* \
+    README.md \
+    TODO.txt \
+    ${KLEE_SRC}/
+ADD .travis ${KLEE_SRC}/.travis/
+ADD autoconf ${KLEE_SRC}/autoconf/
+ADD docs ${KLEE_SRC}/docs/
+ADD include ${KLEE_SRC}/include/
+ADD lib ${KLEE_SRC}/lib/
+ADD runtime ${KLEE_SRC}/runtime/
+ADD scripts ${KLEE_SRC}/scripts/
+ADD test ${KLEE_SRC}/test/
+ADD tools ${KLEE_SRC}/tools/
+ADD unittests ${KLEE_SRC}/unittests/
+ADD utils ${KLEE_SRC}/utils/
+
+# Set klee user to be owner
+RUN sudo chown --recursive klee: ${KLEE_SRC}
+
+# Create build directory
+RUN mkdir -p ${BUILD_DIR}
+
+# Build STP (use TravisCI script)
+RUN cd ${BUILD_DIR} && mkdir stp && cd stp && ${KLEE_SRC}/.travis/stp.sh
+
+# Install testing utils (use TravisCI script)
+RUN cd ${BUILD_DIR} && mkdir testing-utils && cd testing-utils && \
+    ${KLEE_SRC}/.travis/testing-utils.sh
+
+# FIXME: This is a nasty hack so KLEE's configure and build finds
+# LLVM's headers file, libraries and tools
+RUN sudo mkdir -p /usr/lib/llvm-${LLVM_VERSION}/build/Release/bin && \
+    sudo ln -s /usr/bin/llvm-config /usr/lib/llvm-${LLVM_VERSION}/build/Release/bin/llvm-config && \
+    sudo ln -s /usr/bin/llvm-dis /usr/lib/llvm-${LLVM_VERSION}/build/Release/bin/llvm-dis && \
+    sudo ln -s /usr/bin/llvm-as /usr/lib/llvm-${LLVM_VERSION}/build/Release/bin/llvm-as && \
+    sudo ln -s /usr/bin/llvm-link /usr/lib/llvm-${LLVM_VERSION}/build/Release/bin/llvm-link && \
+    sudo ln -s /usr/bin/llvm-ar /usr/lib/llvm-${LLVM_VERSION}/build/Release/bin/llvm-ar && \
+    sudo ln -s /usr/bin/opt /usr/lib/llvm-${LLVM_VERSION}/build/Release/bin/opt && \
+    sudo ln -s /usr/bin/lli /usr/lib/llvm-${LLVM_VERSION}/build/Release/bin/lli && \
+    sudo mkdir -p /usr/lib/llvm-${LLVM_VERSION}/build/include && \
+    sudo ln -s /usr/include/llvm-${LLVM_VERSION}/llvm /usr/lib/llvm-${LLVM_VERSION}/build/include/llvm && \
+    sudo ln -s /usr/include/llvm-c-${LLVM_VERSION}/llvm-c /usr/lib/llvm-${LLVM_VERSION}/build/include/llvm-c && \
+    for static_lib in /usr/lib/llvm-3.4/lib/*.a ; do sudo ln -s ${static_lib} /usr/lib/`basename ${static_lib}`; done
+
+# FIXME: This is **really gross**. The Official Ubuntu LLVM packages don't ship
+# with ``FileCheck`` or the ``not`` tools so we have to hack building these
+# into KLEE's build system in order for the tests to pass
+RUN cd ${KLEE_SRC}/tools && \
+    for tool in FileCheck not; do \
+        svn export \
+        http://llvm.org/svn/llvm-project/llvm/branches/release_34/utils/${tool} ${tool} ; \
+        sed -i 's/^USEDLIBS.*$/LINK_COMPONENTS = support/' ${tool}/Makefile; \
+    done && \
+    sed -i '0,/^PARALLEL_DIRS/a PARALLEL_DIRS += FileCheck not' Makefile
+
+# FIXME: The current TravisCI script expects clang-${LLVM_VERSION} to exist
+RUN sudo ln -s /usr/bin/clang /usr/bin/clang-${LLVM_VERSION} && \
+    sudo ln -s /usr/bin/clang++ /usr/bin/clang++-${LLVM_VERSION}
+
+# Build KLEE (use TravisCI script)
+RUN cd ${BUILD_DIR} && ${KLEE_SRC}/.travis/klee.sh
+
+# Revoke password-less sudo and Set up sudo access for the ``klee`` user so it
+# requires a password
+USER root
+RUN mv /etc/sudoers.bak /etc/sudoers && \
+    echo 'klee  ALL=(root) ALL' >> /etc/sudoers
+USER klee
+
+# Add KLEE binary directory to PATH
+RUN echo 'export PATH=$PATH:'${BUILD_DIR}'/klee/Release+Asserts/bin' >> /home/klee/.bashrc
diff --git a/Makefile.common b/Makefile.common
index 92f5118b..80e6e8a1 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -27,6 +27,12 @@ LLVMCC := $(LLVMGCC)
 LLVMCXX := $(LLVMGXX)
 endif
 
+# Deliberately override the host compiler
+# so that we use what was detected when KLEE was configured
+# and not LLVM.
+CC := $(KLEE_HOST_C_COMPILER)
+CXX := $(KLEE_HOST_CXX_COMPILER)
+
 # Needed to build runtime library using clang (gnu89 is the gcc default)
 C.Flags += -std=gnu89
 
@@ -38,7 +44,6 @@ endif
 # This is filename that KLEE will look for when trying to load klee-uclibc
 KLEE_UCLIBC_BCA_NAME="klee-uclibc.bca"
 
-LD.Flags += $(STP_LDFLAGS)
 CXX.Flags += $(STP_CFLAGS)
 CXX.Flags += -DKLEE_DIR=\"$(PROJ_OBJ_ROOT)\" -DKLEE_INSTALL_BIN_DIR=\"$(PROJ_bindir)\"
 CXX.Flags += -DKLEE_INSTALL_LIB_DIR=\"$(PROJ_libdir)\"
diff --git a/Makefile.config.in b/Makefile.config.in
index ee95c4e5..fb8dbdb2 100644
--- a/Makefile.config.in
+++ b/Makefile.config.in
@@ -53,6 +53,10 @@ RUNTIME_ENABLE_PROFILING :=
 KLEE_BITCODE_C_COMPILER := @KLEE_BITCODE_C_COMPILER@
 KLEE_BITCODE_CXX_COMPILER := @KLEE_BITCODE_CXX_COMPILER@
 
+# Host compiler
+KLEE_HOST_C_COMPILER := @KLEE_HOST_C_COMPILER@
+KLEE_HOST_CXX_COMPILER := @KLEE_HOST_CXX_COMPILER@
+
 # A list of "features" which tests can check for in XFAIL:
 TEST_FEATURE_LIST :=
 
diff --git a/Makefile.rules b/Makefile.rules
index 5e954adf..20e19e26 100644
--- a/Makefile.rules
+++ b/Makefile.rules
@@ -486,9 +486,9 @@ endif
 ifeq ($(HOST_OS),Darwin)
   DARWIN_VERSION := `sw_vers -productVersion`
   # Strip a number like 10.4.7 to 10.4
-  DARWIN_VERSION := $(shell echo $(DARWIN_VERSION)| sed -E 's/(10.[0-9]).*/\1/')
+  DARWIN_VERSION := $(shell echo $(DARWIN_VERSION)| sed -E 's/(10.[0-9]+).*/\1/')
   # Get "4" out of 10.4 for later pieces in the makefile.
-  DARWIN_MAJVERS := $(shell echo $(DARWIN_VERSION)| sed -E 's/10.([0-9]).*/\1/')
+  DARWIN_MAJVERS := $(shell echo $(DARWIN_VERSION)| sed -E 's/10.([0-9]+).*/\1/')
 
   SharedLinkOptions=-Wl,-flat_namespace -Wl,-undefined,suppress \
                     -dynamiclib
diff --git a/autoconf/configure.ac b/autoconf/configure.ac
index 5b9c4e58..747f6544 100644
--- a/autoconf/configure.ac
+++ b/autoconf/configure.ac
@@ -34,8 +34,11 @@ AH_BOTTOM([#endif])
 
 dnl We need to check for the compiler up here to avoid anything else
 dnl starting with a different one.
+AC_PROG_CC(gcc clang)
 AC_PROG_CXX(g++ clang++ )
 AC_LANG([C++])
+AC_SUBST(KLEE_HOST_C_COMPILER,$CC)
+AC_SUBST(KLEE_HOST_CXX_COMPILER,$CXX)
 
 dnl **************************************************************************
 dnl Find the host
@@ -576,10 +579,27 @@ AC_CHECK_HEADER(stp/c_interface.h,,
     ])
 CPPFLAGS="$old_CPPFLAGS"
 
+STP_NEEDS_MINISAT=0
 AC_CHECK_LIB(stp, vc_setInterfaceFlags,, [
-       AC_MSG_ERROR([Could not link with libstp])
+       STP_NEEDS_MINISAT=1; AC_MSG_RESULT([Could not link with libstp])
 ], "$STP_LDFLAGS")
 
+dnl Try linking again with minisat if necessary
+if test "X$STP_NEEDS_MINISAT" != X0 ; then
+  # Need to clear cached result
+  unset ac_cv_lib_stp_vc_setInterfaceFlags
+
+  AC_CHECK_LIB(stp,
+	       vc_setInterfaceFlags,, [
+	       AC_MSG_ERROR([Unable to link with libstp. Check config.log to see what went wrong])
+  ], "$STP_LDFLAGS" "-lminisat" )
+
+  STP_LDFLAGS="${STP_LDFLAGS} -lstp -lminisat"
+else
+  STP_LDFLAGS="${STP_LDFLAGS} -lstp"
+fi
+
+
 AC_SUBST(STP_CFLAGS)
 AC_SUBST(STP_LDFLAGS)
 
diff --git a/configure b/configure
index 82657008..e4f8ffb6 100755
--- a/configure
+++ b/configure
@@ -633,9 +633,6 @@ HAVE_SELINUX
 EGREP
 GREP
 CPP
-ac_ct_CC
-CFLAGS
-CC
 RUNTIME_CONFIGURATION
 RUNTIME_DEBUG_SYMBOLS
 RUNTIME_DISABLE_ASSERTIONS
@@ -667,13 +664,18 @@ build_os
 build_vendor
 build_cpu
 build
+KLEE_HOST_CXX_COMPILER
+KLEE_HOST_C_COMPILER
+ac_ct_CXX
+CXXFLAGS
+CXX
 OBJEXT
 EXEEXT
-ac_ct_CXX
+ac_ct_CC
 CPPFLAGS
 LDFLAGS
-CXXFLAGS
-CXX
+CFLAGS
+CC
 LLVM_OBJ
 LLVM_SRC
 target_alias
@@ -733,14 +735,14 @@ with_metasmt
       ac_precious_vars='build_alias
 host_alias
 target_alias
-CXX
-CXXFLAGS
+CC
+CFLAGS
 LDFLAGS
 LIBS
 CPPFLAGS
+CXX
+CXXFLAGS
 CCC
-CC
-CFLAGS
 CPP
 CXXCPP'
 
@@ -1382,15 +1384,15 @@ Optional Packages:
   --with-metasmt          Location of metaSMT installation directory
 
 Some influential environment variables:
-  CXX         C++ compiler command
-  CXXFLAGS    C++ compiler flags
+  CC          C compiler command
+  CFLAGS      C compiler flags
   LDFLAGS     linker flags, e.g. -L<lib dir> if you have libraries in a
               nonstandard directory <lib dir>
   LIBS        libraries to pass to the linker, e.g. -l<library>
   CPPFLAGS    (Objective) C/C++ preprocessor flags, e.g. -I<include dir> if
               you have headers in a nonstandard directory <include dir>
-  CC          C compiler command
-  CFLAGS      C compiler flags
+  CXX         C++ compiler command
+  CXXFLAGS    C++ compiler flags
   CPP         C preprocessor
   CXXCPP      C++ preprocessor
 
@@ -1474,10 +1476,10 @@ fi
 ## Autoconf initialization. ##
 ## ------------------------ ##
 
-# ac_fn_cxx_try_compile LINENO
-# ----------------------------
+# ac_fn_c_try_compile LINENO
+# --------------------------
 # Try to compile conftest.$ac_ext, and return whether this succeeded.
-ac_fn_cxx_try_compile ()
+ac_fn_c_try_compile ()
 {
   as_lineno=${as_lineno-"$1"} as_lineno_stack=as_lineno_stack=$as_lineno_stack
   rm -f conftest.$ac_objext
@@ -1497,7 +1499,7 @@ $as_echo "$ac_try_echo"; } >&5
   fi
   $as_echo "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5
   test $ac_status = 0; } && {
-	 test -z "$ac_cxx_werror_flag" ||
+	 test -z "$ac_c_werror_flag" ||
 	 test ! -s conftest.err
        } && test -s conftest.$ac_objext; then :
   ac_retval=0
@@ -1510,23 +1512,23 @@ fi
   eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno
   as_fn_set_status $ac_retval
 
-} # ac_fn_cxx_try_compile
+} # ac_fn_c_try_compile
 
-# ac_fn_cxx_try_link LINENO
-# -------------------------
-# Try to link conftest.$ac_ext, and return whether this succeeded.
-ac_fn_cxx_try_link ()
+# ac_fn_cxx_try_compile LINENO
+# ----------------------------
+# Try to compile conftest.$ac_ext, and return whether this succeeded.
+ac_fn_cxx_try_compile ()
 {
   as_lineno=${as_lineno-"$1"} as_lineno_stack=as_lineno_stack=$as_lineno_stack
-  rm -f conftest.$ac_objext conftest$ac_exeext
-  if { { ac_try="$ac_link"
+  rm -f conftest.$ac_objext
+  if { { ac_try="$ac_compile"
 case "(($ac_try" in
   *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
   *) ac_try_echo=$ac_try;;
 esac
 eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\""
 $as_echo "$ac_try_echo"; } >&5
-  (eval "$ac_link") 2>conftest.err
+  (eval "$ac_compile") 2>conftest.err
   ac_status=$?
   if test -s conftest.err; then
     grep -v '^ *+' conftest.err >conftest.er1
@@ -1537,10 +1539,7 @@ $as_echo "$ac_try_echo"; } >&5
   test $ac_status = 0; } && {
 	 test -z "$ac_cxx_werror_flag" ||
 	 test ! -s conftest.err
-       } && test -s conftest$ac_exeext && {
-	 test "$cross_compiling" = yes ||
-	 test -x conftest$ac_exeext
-       }; then :
+       } && test -s conftest.$ac_objext; then :
   ac_retval=0
 else
   $as_echo "$as_me: failed program was:" >&5
@@ -1548,31 +1547,26 @@ sed 's/^/| /' conftest.$ac_ext >&5
 
 	ac_retval=1
 fi
-  # Delete the IPA/IPO (Inter Procedural Analysis/Optimization) information
-  # created by the PGI compiler (conftest_ipa8_conftest.oo), as it would
-  # interfere with the next link command; also delete a directory that is
-  # left behind by Apple's compiler.  We do this before executing the actions.
-  rm -rf conftest.dSYM conftest_ipa8_conftest.oo
   eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno
   as_fn_set_status $ac_retval
 
-} # ac_fn_cxx_try_link
+} # ac_fn_cxx_try_compile
 
-# ac_fn_c_try_compile LINENO
-# --------------------------
-# Try to compile conftest.$ac_ext, and return whether this succeeded.
-ac_fn_c_try_compile ()
+# ac_fn_cxx_try_link LINENO
+# -------------------------
+# Try to link conftest.$ac_ext, and return whether this succeeded.
+ac_fn_cxx_try_link ()
 {
   as_lineno=${as_lineno-"$1"} as_lineno_stack=as_lineno_stack=$as_lineno_stack
-  rm -f conftest.$ac_objext
-  if { { ac_try="$ac_compile"
+  rm -f conftest.$ac_objext conftest$ac_exeext
+  if { { ac_try="$ac_link"
 case "(($ac_try" in
   *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
   *) ac_try_echo=$ac_try;;
 esac
 eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\""
 $as_echo "$ac_try_echo"; } >&5
-  (eval "$ac_compile") 2>conftest.err
+  (eval "$ac_link") 2>conftest.err
   ac_status=$?
   if test -s conftest.err; then
     grep -v '^ *+' conftest.err >conftest.er1
@@ -1581,9 +1575,12 @@ $as_echo "$ac_try_echo"; } >&5
   fi
   $as_echo "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5
   test $ac_status = 0; } && {
-	 test -z "$ac_c_werror_flag" ||
+	 test -z "$ac_cxx_werror_flag" ||
 	 test ! -s conftest.err
-       } && test -s conftest.$ac_objext; then :
+       } && test -s conftest$ac_exeext && {
+	 test "$cross_compiling" = yes ||
+	 test -x conftest$ac_exeext
+       }; then :
   ac_retval=0
 else
   $as_echo "$as_me: failed program was:" >&5
@@ -1591,10 +1588,15 @@ sed 's/^/| /' conftest.$ac_ext >&5
 
 	ac_retval=1
 fi
+  # Delete the IPA/IPO (Inter Procedural Analysis/Optimization) information
+  # created by the PGI compiler (conftest_ipa8_conftest.oo), as it would
+  # interfere with the next link command; also delete a directory that is
+  # left behind by Apple's compiler.  We do this before executing the actions.
+  rm -rf conftest.dSYM conftest_ipa8_conftest.oo
   eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno
   as_fn_set_status $ac_retval
 
-} # ac_fn_c_try_compile
+} # ac_fn_cxx_try_link
 
 # ac_fn_c_try_cpp LINENO
 # ----------------------
@@ -2460,27 +2462,23 @@ ac_config_headers="$ac_config_headers include/klee/Config/config.h"
 
 
 
-ac_ext=cpp
-ac_cpp='$CXXCPP $CPPFLAGS'
-ac_compile='$CXX -c $CXXFLAGS $CPPFLAGS conftest.$ac_ext >&5'
-ac_link='$CXX -o conftest$ac_exeext $CXXFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS >&5'
-ac_compiler_gnu=$ac_cv_cxx_compiler_gnu
-if test -z "$CXX"; then
-  if test -n "$CCC"; then
-    CXX=$CCC
-  else
-    if test -n "$ac_tool_prefix"; then
-  for ac_prog in g++ clang++
+ac_ext=c
+ac_cpp='$CPP $CPPFLAGS'
+ac_compile='$CC -c $CFLAGS $CPPFLAGS conftest.$ac_ext >&5'
+ac_link='$CC -o conftest$ac_exeext $CFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS >&5'
+ac_compiler_gnu=$ac_cv_c_compiler_gnu
+if test -n "$ac_tool_prefix"; then
+  for ac_prog in gcc clang
   do
     # Extract the first word of "$ac_tool_prefix$ac_prog", so it can be a program name with args.
 set dummy $ac_tool_prefix$ac_prog; ac_word=$2
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
 $as_echo_n "checking for $ac_word... " >&6; }
-if ${ac_cv_prog_CXX+:} false; then :
+if ${ac_cv_prog_CC+:} false; then :
   $as_echo_n "(cached) " >&6
 else
-  if test -n "$CXX"; then
-  ac_cv_prog_CXX="$CXX" # Let the user override the test.
+  if test -n "$CC"; then
+  ac_cv_prog_CC="$CC" # Let the user override the test.
 else
 as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
 for as_dir in $PATH
@@ -2489,7 +2487,7 @@ do
   test -z "$as_dir" && as_dir=.
     for ac_exec_ext in '' $ac_executable_extensions; do
   if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
-    ac_cv_prog_CXX="$ac_tool_prefix$ac_prog"
+    ac_cv_prog_CC="$ac_tool_prefix$ac_prog"
     $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
     break 2
   fi
@@ -2499,32 +2497,32 @@ IFS=$as_save_IFS
 
 fi
 fi
-CXX=$ac_cv_prog_CXX
-if test -n "$CXX"; then
-  { $as_echo "$as_me:${as_lineno-$LINENO}: result: $CXX" >&5
-$as_echo "$CXX" >&6; }
+CC=$ac_cv_prog_CC
+if test -n "$CC"; then
+  { $as_echo "$as_me:${as_lineno-$LINENO}: result: $CC" >&5
+$as_echo "$CC" >&6; }
 else
   { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
 $as_echo "no" >&6; }
 fi
 
 
-    test -n "$CXX" && break
+    test -n "$CC" && break
   done
 fi
-if test -z "$CXX"; then
-  ac_ct_CXX=$CXX
-  for ac_prog in g++ clang++
+if test -z "$CC"; then
+  ac_ct_CC=$CC
+  for ac_prog in gcc clang
 do
   # Extract the first word of "$ac_prog", so it can be a program name with args.
 set dummy $ac_prog; ac_word=$2
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
 $as_echo_n "checking for $ac_word... " >&6; }
-if ${ac_cv_prog_ac_ct_CXX+:} false; then :
+if ${ac_cv_prog_ac_ct_CC+:} false; then :
   $as_echo_n "(cached) " >&6
 else
-  if test -n "$ac_ct_CXX"; then
-  ac_cv_prog_ac_ct_CXX="$ac_ct_CXX" # Let the user override the test.
+  if test -n "$ac_ct_CC"; then
+  ac_cv_prog_ac_ct_CC="$ac_ct_CC" # Let the user override the test.
 else
 as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
 for as_dir in $PATH
@@ -2533,7 +2531,7 @@ do
   test -z "$as_dir" && as_dir=.
     for ac_exec_ext in '' $ac_executable_extensions; do
   if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
-    ac_cv_prog_ac_ct_CXX="$ac_prog"
+    ac_cv_prog_ac_ct_CC="$ac_prog"
     $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
     break 2
   fi
@@ -2543,21 +2541,21 @@ IFS=$as_save_IFS
 
 fi
 fi
-ac_ct_CXX=$ac_cv_prog_ac_ct_CXX
-if test -n "$ac_ct_CXX"; then
-  { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_ct_CXX" >&5
-$as_echo "$ac_ct_CXX" >&6; }
+ac_ct_CC=$ac_cv_prog_ac_ct_CC
+if test -n "$ac_ct_CC"; then
+  { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_ct_CC" >&5
+$as_echo "$ac_ct_CC" >&6; }
 else
   { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
 $as_echo "no" >&6; }
 fi
 
 
-  test -n "$ac_ct_CXX" && break
+  test -n "$ac_ct_CC" && break
 done
 
-  if test "x$ac_ct_CXX" = x; then
-    CXX="g++"
+  if test "x$ac_ct_CC" = x; then
+    CC=""
   else
     case $cross_compiling:$ac_tool_warned in
 yes:)
@@ -2565,14 +2563,18 @@ yes:)
 $as_echo "$as_me: WARNING: using cross tools not prefixed with host triplet" >&2;}
 ac_tool_warned=yes ;;
 esac
-    CXX=$ac_ct_CXX
+    CC=$ac_ct_CC
   fi
 fi
 
-  fi
-fi
+
+test -z "$CC" && { { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5
+$as_echo "$as_me: error: in \`$ac_pwd':" >&2;}
+as_fn_error $? "no acceptable C compiler found in \$PATH
+See \`config.log' for more details" "$LINENO" 5; }
+
 # Provide some information about the compiler.
-$as_echo "$as_me:${as_lineno-$LINENO}: checking for C++ compiler version" >&5
+$as_echo "$as_me:${as_lineno-$LINENO}: checking for C compiler version" >&5
 set X $ac_compile
 ac_compiler=$2
 for ac_option in --version -v -V -qversion; do
@@ -2612,8 +2614,8 @@ ac_clean_files="$ac_clean_files a.out a.out.dSYM a.exe b.out"
 # Try to create an executable without -o first, disregard a.out.
 # It will help us diagnose broken compilers, and finding out an intuition
 # of exeext.
-{ $as_echo "$as_me:${as_lineno-$LINENO}: checking whether the C++ compiler works" >&5
-$as_echo_n "checking whether the C++ compiler works... " >&6; }
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking whether the C compiler works" >&5
+$as_echo_n "checking whether the C compiler works... " >&6; }
 ac_link_default=`$as_echo "$ac_link" | sed 's/ -o *conftest[^ ]*//'`
 
 # The possible output files:
@@ -2683,14 +2685,14 @@ sed 's/^/| /' conftest.$ac_ext >&5
 
 { { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5
 $as_echo "$as_me: error: in \`$ac_pwd':" >&2;}
-as_fn_error 77 "C++ compiler cannot create executables
+as_fn_error 77 "C compiler cannot create executables
 See \`config.log' for more details" "$LINENO" 5; }
 else
   { $as_echo "$as_me:${as_lineno-$LINENO}: result: yes" >&5
 $as_echo "yes" >&6; }
 fi
-{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for C++ compiler default output file name" >&5
-$as_echo_n "checking for C++ compiler default output file name... " >&6; }
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for C compiler default output file name" >&5
+$as_echo_n "checking for C compiler default output file name... " >&6; }
 { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_file" >&5
 $as_echo "$ac_file" >&6; }
 ac_exeext=$ac_cv_exeext
@@ -2784,7 +2786,7 @@ $as_echo "$ac_try_echo"; } >&5
     else
 	{ { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5
 $as_echo "$as_me: error: in \`$ac_pwd':" >&2;}
-as_fn_error $? "cannot run C++ compiled programs.
+as_fn_error $? "cannot run C compiled programs.
 If you meant to cross compile, use \`--host'.
 See \`config.log' for more details" "$LINENO" 5; }
     fi
@@ -2846,6 +2848,353 @@ fi
 $as_echo "$ac_cv_objext" >&6; }
 OBJEXT=$ac_cv_objext
 ac_objext=$OBJEXT
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking whether we are using the GNU C compiler" >&5
+$as_echo_n "checking whether we are using the GNU C compiler... " >&6; }
+if ${ac_cv_c_compiler_gnu+:} false; then :
+  $as_echo_n "(cached) " >&6
+else
+  cat confdefs.h - <<_ACEOF >conftest.$ac_ext
+/* end confdefs.h.  */
+
+int
+main ()
+{
+#ifndef __GNUC__
+       choke me
+#endif
+
+  ;
+  return 0;
+}
+_ACEOF
+if ac_fn_c_try_compile "$LINENO"; then :
+  ac_compiler_gnu=yes
+else
+  ac_compiler_gnu=no
+fi
+rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext
+ac_cv_c_compiler_gnu=$ac_compiler_gnu
+
+fi
+{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_c_compiler_gnu" >&5
+$as_echo "$ac_cv_c_compiler_gnu" >&6; }
+if test $ac_compiler_gnu = yes; then
+  GCC=yes
+else
+  GCC=
+fi
+ac_test_CFLAGS=${CFLAGS+set}
+ac_save_CFLAGS=$CFLAGS
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking whether $CC accepts -g" >&5
+$as_echo_n "checking whether $CC accepts -g... " >&6; }
+if ${ac_cv_prog_cc_g+:} false; then :
+  $as_echo_n "(cached) " >&6
+else
+  ac_save_c_werror_flag=$ac_c_werror_flag
+   ac_c_werror_flag=yes
+   ac_cv_prog_cc_g=no
+   CFLAGS="-g"
+   cat confdefs.h - <<_ACEOF >conftest.$ac_ext
+/* end confdefs.h.  */
+
+int
+main ()
+{
+
+  ;
+  return 0;
+}
+_ACEOF
+if ac_fn_c_try_compile "$LINENO"; then :
+  ac_cv_prog_cc_g=yes
+else
+  CFLAGS=""
+      cat confdefs.h - <<_ACEOF >conftest.$ac_ext
+/* end confdefs.h.  */
+
+int
+main ()
+{
+
+  ;
+  return 0;
+}
+_ACEOF
+if ac_fn_c_try_compile "$LINENO"; then :
+
+else
+  ac_c_werror_flag=$ac_save_c_werror_flag
+	 CFLAGS="-g"
+	 cat confdefs.h - <<_ACEOF >conftest.$ac_ext
+/* end confdefs.h.  */
+
+int
+main ()
+{
+
+  ;
+  return 0;
+}
+_ACEOF
+if ac_fn_c_try_compile "$LINENO"; then :
+  ac_cv_prog_cc_g=yes
+fi
+rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext
+fi
+rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext
+fi
+rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext
+   ac_c_werror_flag=$ac_save_c_werror_flag
+fi
+{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_prog_cc_g" >&5
+$as_echo "$ac_cv_prog_cc_g" >&6; }
+if test "$ac_test_CFLAGS" = set; then
+  CFLAGS=$ac_save_CFLAGS
+elif test $ac_cv_prog_cc_g = yes; then
+  if test "$GCC" = yes; then
+    CFLAGS="-g -O2"
+  else
+    CFLAGS="-g"
+  fi
+else
+  if test "$GCC" = yes; then
+    CFLAGS="-O2"
+  else
+    CFLAGS=
+  fi
+fi
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $CC option to accept ISO C89" >&5
+$as_echo_n "checking for $CC option to accept ISO C89... " >&6; }
+if ${ac_cv_prog_cc_c89+:} false; then :
+  $as_echo_n "(cached) " >&6
+else
+  ac_cv_prog_cc_c89=no
+ac_save_CC=$CC
+cat confdefs.h - <<_ACEOF >conftest.$ac_ext
+/* end confdefs.h.  */
+#include <stdarg.h>
+#include <stdio.h>
+struct stat;
+/* Most of the following tests are stolen from RCS 5.7's src/conf.sh.  */
+struct buf { int x; };
+FILE * (*rcsopen) (struct buf *, struct stat *, int);
+static char *e (p, i)
+     char **p;
+     int i;
+{
+  return p[i];
+}
+static char *f (char * (*g) (char **, int), char **p, ...)
+{
+  char *s;
+  va_list v;
+  va_start (v,p);
+  s = g (p, va_arg (v,int));
+  va_end (v);
+  return s;
+}
+
+/* OSF 4.0 Compaq cc is some sort of almost-ANSI by default.  It has
+   function prototypes and stuff, but not '\xHH' hex character constants.
+   These don't provoke an error unfortunately, instead are silently treated
+   as 'x'.  The following induces an error, until -std is added to get
+   proper ANSI mode.  Curiously '\x00'!='x' always comes out true, for an
+   array size at least.  It's necessary to write '\x00'==0 to get something
+   that's true only with -std.  */
+int osf4_cc_array ['\x00' == 0 ? 1 : -1];
+
+/* IBM C 6 for AIX is almost-ANSI by default, but it replaces macro parameters
+   inside strings and character constants.  */
+#define FOO(x) 'x'
+int xlc6_cc_array[FOO(a) == 'x' ? 1 : -1];
+
+int test (int i, double x);
+struct s1 {int (*f) (int a);};
+struct s2 {int (*f) (double a);};
+int pairnames (int, char **, FILE *(*)(struct buf *, struct stat *, int), int, int);
+int argc;
+char **argv;
+int
+main ()
+{
+return f (e, argv, 0) != argv[0]  ||  f (e, argv, 1) != argv[1];
+  ;
+  return 0;
+}
+_ACEOF
+for ac_arg in '' -qlanglvl=extc89 -qlanglvl=ansi -std \
+	-Ae "-Aa -D_HPUX_SOURCE" "-Xc -D__EXTENSIONS__"
+do
+  CC="$ac_save_CC $ac_arg"
+  if ac_fn_c_try_compile "$LINENO"; then :
+  ac_cv_prog_cc_c89=$ac_arg
+fi
+rm -f core conftest.err conftest.$ac_objext
+  test "x$ac_cv_prog_cc_c89" != "xno" && break
+done
+rm -f conftest.$ac_ext
+CC=$ac_save_CC
+
+fi
+# AC_CACHE_VAL
+case "x$ac_cv_prog_cc_c89" in
+  x)
+    { $as_echo "$as_me:${as_lineno-$LINENO}: result: none needed" >&5
+$as_echo "none needed" >&6; } ;;
+  xno)
+    { $as_echo "$as_me:${as_lineno-$LINENO}: result: unsupported" >&5
+$as_echo "unsupported" >&6; } ;;
+  *)
+    CC="$CC $ac_cv_prog_cc_c89"
+    { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_prog_cc_c89" >&5
+$as_echo "$ac_cv_prog_cc_c89" >&6; } ;;
+esac
+if test "x$ac_cv_prog_cc_c89" != xno; then :
+
+fi
+
+ac_ext=c
+ac_cpp='$CPP $CPPFLAGS'
+ac_compile='$CC -c $CFLAGS $CPPFLAGS conftest.$ac_ext >&5'
+ac_link='$CC -o conftest$ac_exeext $CFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS >&5'
+ac_compiler_gnu=$ac_cv_c_compiler_gnu
+
+ac_ext=cpp
+ac_cpp='$CXXCPP $CPPFLAGS'
+ac_compile='$CXX -c $CXXFLAGS $CPPFLAGS conftest.$ac_ext >&5'
+ac_link='$CXX -o conftest$ac_exeext $CXXFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS >&5'
+ac_compiler_gnu=$ac_cv_cxx_compiler_gnu
+if test -z "$CXX"; then
+  if test -n "$CCC"; then
+    CXX=$CCC
+  else
+    if test -n "$ac_tool_prefix"; then
+  for ac_prog in g++ clang++
+  do
+    # Extract the first word of "$ac_tool_prefix$ac_prog", so it can be a program name with args.
+set dummy $ac_tool_prefix$ac_prog; ac_word=$2
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
+$as_echo_n "checking for $ac_word... " >&6; }
+if ${ac_cv_prog_CXX+:} false; then :
+  $as_echo_n "(cached) " >&6
+else
+  if test -n "$CXX"; then
+  ac_cv_prog_CXX="$CXX" # Let the user override the test.
+else
+as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
+for as_dir in $PATH
+do
+  IFS=$as_save_IFS
+  test -z "$as_dir" && as_dir=.
+    for ac_exec_ext in '' $ac_executable_extensions; do
+  if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
+    ac_cv_prog_CXX="$ac_tool_prefix$ac_prog"
+    $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
+    break 2
+  fi
+done
+  done
+IFS=$as_save_IFS
+
+fi
+fi
+CXX=$ac_cv_prog_CXX
+if test -n "$CXX"; then
+  { $as_echo "$as_me:${as_lineno-$LINENO}: result: $CXX" >&5
+$as_echo "$CXX" >&6; }
+else
+  { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
+$as_echo "no" >&6; }
+fi
+
+
+    test -n "$CXX" && break
+  done
+fi
+if test -z "$CXX"; then
+  ac_ct_CXX=$CXX
+  for ac_prog in g++ clang++
+do
+  # Extract the first word of "$ac_prog", so it can be a program name with args.
+set dummy $ac_prog; ac_word=$2
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
+$as_echo_n "checking for $ac_word... " >&6; }
+if ${ac_cv_prog_ac_ct_CXX+:} false; then :
+  $as_echo_n "(cached) " >&6
+else
+  if test -n "$ac_ct_CXX"; then
+  ac_cv_prog_ac_ct_CXX="$ac_ct_CXX" # Let the user override the test.
+else
+as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
+for as_dir in $PATH
+do
+  IFS=$as_save_IFS
+  test -z "$as_dir" && as_dir=.
+    for ac_exec_ext in '' $ac_executable_extensions; do
+  if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
+    ac_cv_prog_ac_ct_CXX="$ac_prog"
+    $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
+    break 2
+  fi
+done
+  done
+IFS=$as_save_IFS
+
+fi
+fi
+ac_ct_CXX=$ac_cv_prog_ac_ct_CXX
+if test -n "$ac_ct_CXX"; then
+  { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_ct_CXX" >&5
+$as_echo "$ac_ct_CXX" >&6; }
+else
+  { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
+$as_echo "no" >&6; }
+fi
+
+
+  test -n "$ac_ct_CXX" && break
+done
+
+  if test "x$ac_ct_CXX" = x; then
+    CXX="g++"
+  else
+    case $cross_compiling:$ac_tool_warned in
+yes:)
+{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: using cross tools not prefixed with host triplet" >&5
+$as_echo "$as_me: WARNING: using cross tools not prefixed with host triplet" >&2;}
+ac_tool_warned=yes ;;
+esac
+    CXX=$ac_ct_CXX
+  fi
+fi
+
+  fi
+fi
+# Provide some information about the compiler.
+$as_echo "$as_me:${as_lineno-$LINENO}: checking for C++ compiler version" >&5
+set X $ac_compile
+ac_compiler=$2
+for ac_option in --version -v -V -qversion; do
+  { { ac_try="$ac_compiler $ac_option >&5"
+case "(($ac_try" in
+  *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+  *) ac_try_echo=$ac_try;;
+esac
+eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\""
+$as_echo "$ac_try_echo"; } >&5
+  (eval "$ac_compiler $ac_option >&5") 2>conftest.err
+  ac_status=$?
+  if test -s conftest.err; then
+    sed '10a\
+... rest of stderr output deleted ...
+         10q' conftest.err >conftest.er1
+    cat conftest.er1 >&5
+  fi
+  rm -f conftest.er1 conftest.err
+  $as_echo "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5
+  test $ac_status = 0; }
+done
+
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking whether we are using the GNU C++ compiler" >&5
 $as_echo_n "checking whether we are using the GNU C++ compiler... " >&6; }
 if ${ac_cv_cxx_compiler_gnu+:} false; then :
@@ -2973,6 +3322,10 @@ ac_compile='$CXX -c $CXXFLAGS $CPPFLAGS conftest.$ac_ext >&5'
 ac_link='$CXX -o conftest$ac_exeext $CXXFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS >&5'
 ac_compiler_gnu=$ac_cv_cxx_compiler_gnu
 
+KLEE_HOST_C_COMPILER=$CC
+
+KLEE_HOST_CXX_COMPILER=$CXX
+
 
 
 # Make sure we can run config.sub.
@@ -3793,545 +4146,6 @@ ac_link='$CC -o conftest$ac_exeext $CFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $
 ac_compiler_gnu=$ac_cv_c_compiler_gnu
 
 
-ac_ext=c
-ac_cpp='$CPP $CPPFLAGS'
-ac_compile='$CC -c $CFLAGS $CPPFLAGS conftest.$ac_ext >&5'
-ac_link='$CC -o conftest$ac_exeext $CFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS >&5'
-ac_compiler_gnu=$ac_cv_c_compiler_gnu
-if test -n "$ac_tool_prefix"; then
-  # Extract the first word of "${ac_tool_prefix}gcc", so it can be a program name with args.
-set dummy ${ac_tool_prefix}gcc; ac_word=$2
-{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
-$as_echo_n "checking for $ac_word... " >&6; }
-if ${ac_cv_prog_CC+:} false; then :
-  $as_echo_n "(cached) " >&6
-else
-  if test -n "$CC"; then
-  ac_cv_prog_CC="$CC" # Let the user override the test.
-else
-as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
-for as_dir in $PATH
-do
-  IFS=$as_save_IFS
-  test -z "$as_dir" && as_dir=.
-    for ac_exec_ext in '' $ac_executable_extensions; do
-  if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
-    ac_cv_prog_CC="${ac_tool_prefix}gcc"
-    $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
-    break 2
-  fi
-done
-  done
-IFS=$as_save_IFS
-
-fi
-fi
-CC=$ac_cv_prog_CC
-if test -n "$CC"; then
-  { $as_echo "$as_me:${as_lineno-$LINENO}: result: $CC" >&5
-$as_echo "$CC" >&6; }
-else
-  { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
-$as_echo "no" >&6; }
-fi
-
-
-fi
-if test -z "$ac_cv_prog_CC"; then
-  ac_ct_CC=$CC
-  # Extract the first word of "gcc", so it can be a program name with args.
-set dummy gcc; ac_word=$2
-{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
-$as_echo_n "checking for $ac_word... " >&6; }
-if ${ac_cv_prog_ac_ct_CC+:} false; then :
-  $as_echo_n "(cached) " >&6
-else
-  if test -n "$ac_ct_CC"; then
-  ac_cv_prog_ac_ct_CC="$ac_ct_CC" # Let the user override the test.
-else
-as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
-for as_dir in $PATH
-do
-  IFS=$as_save_IFS
-  test -z "$as_dir" && as_dir=.
-    for ac_exec_ext in '' $ac_executable_extensions; do
-  if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
-    ac_cv_prog_ac_ct_CC="gcc"
-    $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
-    break 2
-  fi
-done
-  done
-IFS=$as_save_IFS
-
-fi
-fi
-ac_ct_CC=$ac_cv_prog_ac_ct_CC
-if test -n "$ac_ct_CC"; then
-  { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_ct_CC" >&5
-$as_echo "$ac_ct_CC" >&6; }
-else
-  { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
-$as_echo "no" >&6; }
-fi
-
-  if test "x$ac_ct_CC" = x; then
-    CC=""
-  else
-    case $cross_compiling:$ac_tool_warned in
-yes:)
-{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: using cross tools not prefixed with host triplet" >&5
-$as_echo "$as_me: WARNING: using cross tools not prefixed with host triplet" >&2;}
-ac_tool_warned=yes ;;
-esac
-    CC=$ac_ct_CC
-  fi
-else
-  CC="$ac_cv_prog_CC"
-fi
-
-if test -z "$CC"; then
-          if test -n "$ac_tool_prefix"; then
-    # Extract the first word of "${ac_tool_prefix}cc", so it can be a program name with args.
-set dummy ${ac_tool_prefix}cc; ac_word=$2
-{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
-$as_echo_n "checking for $ac_word... " >&6; }
-if ${ac_cv_prog_CC+:} false; then :
-  $as_echo_n "(cached) " >&6
-else
-  if test -n "$CC"; then
-  ac_cv_prog_CC="$CC" # Let the user override the test.
-else
-as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
-for as_dir in $PATH
-do
-  IFS=$as_save_IFS
-  test -z "$as_dir" && as_dir=.
-    for ac_exec_ext in '' $ac_executable_extensions; do
-  if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
-    ac_cv_prog_CC="${ac_tool_prefix}cc"
-    $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
-    break 2
-  fi
-done
-  done
-IFS=$as_save_IFS
-
-fi
-fi
-CC=$ac_cv_prog_CC
-if test -n "$CC"; then
-  { $as_echo "$as_me:${as_lineno-$LINENO}: result: $CC" >&5
-$as_echo "$CC" >&6; }
-else
-  { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
-$as_echo "no" >&6; }
-fi
-
-
-  fi
-fi
-if test -z "$CC"; then
-  # Extract the first word of "cc", so it can be a program name with args.
-set dummy cc; ac_word=$2
-{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
-$as_echo_n "checking for $ac_word... " >&6; }
-if ${ac_cv_prog_CC+:} false; then :
-  $as_echo_n "(cached) " >&6
-else
-  if test -n "$CC"; then
-  ac_cv_prog_CC="$CC" # Let the user override the test.
-else
-  ac_prog_rejected=no
-as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
-for as_dir in $PATH
-do
-  IFS=$as_save_IFS
-  test -z "$as_dir" && as_dir=.
-    for ac_exec_ext in '' $ac_executable_extensions; do
-  if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
-    if test "$as_dir/$ac_word$ac_exec_ext" = "/usr/ucb/cc"; then
-       ac_prog_rejected=yes
-       continue
-     fi
-    ac_cv_prog_CC="cc"
-    $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
-    break 2
-  fi
-done
-  done
-IFS=$as_save_IFS
-
-if test $ac_prog_rejected = yes; then
-  # We found a bogon in the path, so make sure we never use it.
-  set dummy $ac_cv_prog_CC
-  shift
-  if test $# != 0; then
-    # We chose a different compiler from the bogus one.
-    # However, it has the same basename, so the bogon will be chosen
-    # first if we set CC to just the basename; use the full file name.
-    shift
-    ac_cv_prog_CC="$as_dir/$ac_word${1+' '}$@"
-  fi
-fi
-fi
-fi
-CC=$ac_cv_prog_CC
-if test -n "$CC"; then
-  { $as_echo "$as_me:${as_lineno-$LINENO}: result: $CC" >&5
-$as_echo "$CC" >&6; }
-else
-  { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
-$as_echo "no" >&6; }
-fi
-
-
-fi
-if test -z "$CC"; then
-  if test -n "$ac_tool_prefix"; then
-  for ac_prog in cl.exe
-  do
-    # Extract the first word of "$ac_tool_prefix$ac_prog", so it can be a program name with args.
-set dummy $ac_tool_prefix$ac_prog; ac_word=$2
-{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
-$as_echo_n "checking for $ac_word... " >&6; }
-if ${ac_cv_prog_CC+:} false; then :
-  $as_echo_n "(cached) " >&6
-else
-  if test -n "$CC"; then
-  ac_cv_prog_CC="$CC" # Let the user override the test.
-else
-as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
-for as_dir in $PATH
-do
-  IFS=$as_save_IFS
-  test -z "$as_dir" && as_dir=.
-    for ac_exec_ext in '' $ac_executable_extensions; do
-  if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
-    ac_cv_prog_CC="$ac_tool_prefix$ac_prog"
-    $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
-    break 2
-  fi
-done
-  done
-IFS=$as_save_IFS
-
-fi
-fi
-CC=$ac_cv_prog_CC
-if test -n "$CC"; then
-  { $as_echo "$as_me:${as_lineno-$LINENO}: result: $CC" >&5
-$as_echo "$CC" >&6; }
-else
-  { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
-$as_echo "no" >&6; }
-fi
-
-
-    test -n "$CC" && break
-  done
-fi
-if test -z "$CC"; then
-  ac_ct_CC=$CC
-  for ac_prog in cl.exe
-do
-  # Extract the first word of "$ac_prog", so it can be a program name with args.
-set dummy $ac_prog; ac_word=$2
-{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
-$as_echo_n "checking for $ac_word... " >&6; }
-if ${ac_cv_prog_ac_ct_CC+:} false; then :
-  $as_echo_n "(cached) " >&6
-else
-  if test -n "$ac_ct_CC"; then
-  ac_cv_prog_ac_ct_CC="$ac_ct_CC" # Let the user override the test.
-else
-as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
-for as_dir in $PATH
-do
-  IFS=$as_save_IFS
-  test -z "$as_dir" && as_dir=.
-    for ac_exec_ext in '' $ac_executable_extensions; do
-  if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
-    ac_cv_prog_ac_ct_CC="$ac_prog"
-    $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
-    break 2
-  fi
-done
-  done
-IFS=$as_save_IFS
-
-fi
-fi
-ac_ct_CC=$ac_cv_prog_ac_ct_CC
-if test -n "$ac_ct_CC"; then
-  { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_ct_CC" >&5
-$as_echo "$ac_ct_CC" >&6; }
-else
-  { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
-$as_echo "no" >&6; }
-fi
-
-
-  test -n "$ac_ct_CC" && break
-done
-
-  if test "x$ac_ct_CC" = x; then
-    CC=""
-  else
-    case $cross_compiling:$ac_tool_warned in
-yes:)
-{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: using cross tools not prefixed with host triplet" >&5
-$as_echo "$as_me: WARNING: using cross tools not prefixed with host triplet" >&2;}
-ac_tool_warned=yes ;;
-esac
-    CC=$ac_ct_CC
-  fi
-fi
-
-fi
-
-
-test -z "$CC" && { { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5
-$as_echo "$as_me: error: in \`$ac_pwd':" >&2;}
-as_fn_error $? "no acceptable C compiler found in \$PATH
-See \`config.log' for more details" "$LINENO" 5; }
-
-# Provide some information about the compiler.
-$as_echo "$as_me:${as_lineno-$LINENO}: checking for C compiler version" >&5
-set X $ac_compile
-ac_compiler=$2
-for ac_option in --version -v -V -qversion; do
-  { { ac_try="$ac_compiler $ac_option >&5"
-case "(($ac_try" in
-  *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
-  *) ac_try_echo=$ac_try;;
-esac
-eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\""
-$as_echo "$ac_try_echo"; } >&5
-  (eval "$ac_compiler $ac_option >&5") 2>conftest.err
-  ac_status=$?
-  if test -s conftest.err; then
-    sed '10a\
-... rest of stderr output deleted ...
-         10q' conftest.err >conftest.er1
-    cat conftest.er1 >&5
-  fi
-  rm -f conftest.er1 conftest.err
-  $as_echo "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5
-  test $ac_status = 0; }
-done
-
-{ $as_echo "$as_me:${as_lineno-$LINENO}: checking whether we are using the GNU C compiler" >&5
-$as_echo_n "checking whether we are using the GNU C compiler... " >&6; }
-if ${ac_cv_c_compiler_gnu+:} false; then :
-  $as_echo_n "(cached) " >&6
-else
-  cat confdefs.h - <<_ACEOF >conftest.$ac_ext
-/* end confdefs.h.  */
-
-int
-main ()
-{
-#ifndef __GNUC__
-       choke me
-#endif
-
-  ;
-  return 0;
-}
-_ACEOF
-if ac_fn_c_try_compile "$LINENO"; then :
-  ac_compiler_gnu=yes
-else
-  ac_compiler_gnu=no
-fi
-rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext
-ac_cv_c_compiler_gnu=$ac_compiler_gnu
-
-fi
-{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_c_compiler_gnu" >&5
-$as_echo "$ac_cv_c_compiler_gnu" >&6; }
-if test $ac_compiler_gnu = yes; then
-  GCC=yes
-else
-  GCC=
-fi
-ac_test_CFLAGS=${CFLAGS+set}
-ac_save_CFLAGS=$CFLAGS
-{ $as_echo "$as_me:${as_lineno-$LINENO}: checking whether $CC accepts -g" >&5
-$as_echo_n "checking whether $CC accepts -g... " >&6; }
-if ${ac_cv_prog_cc_g+:} false; then :
-  $as_echo_n "(cached) " >&6
-else
-  ac_save_c_werror_flag=$ac_c_werror_flag
-   ac_c_werror_flag=yes
-   ac_cv_prog_cc_g=no
-   CFLAGS="-g"
-   cat confdefs.h - <<_ACEOF >conftest.$ac_ext
-/* end confdefs.h.  */
-
-int
-main ()
-{
-
-  ;
-  return 0;
-}
-_ACEOF
-if ac_fn_c_try_compile "$LINENO"; then :
-  ac_cv_prog_cc_g=yes
-else
-  CFLAGS=""
-      cat confdefs.h - <<_ACEOF >conftest.$ac_ext
-/* end confdefs.h.  */
-
-int
-main ()
-{
-
-  ;
-  return 0;
-}
-_ACEOF
-if ac_fn_c_try_compile "$LINENO"; then :
-
-else
-  ac_c_werror_flag=$ac_save_c_werror_flag
-	 CFLAGS="-g"
-	 cat confdefs.h - <<_ACEOF >conftest.$ac_ext
-/* end confdefs.h.  */
-
-int
-main ()
-{
-
-  ;
-  return 0;
-}
-_ACEOF
-if ac_fn_c_try_compile "$LINENO"; then :
-  ac_cv_prog_cc_g=yes
-fi
-rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext
-fi
-rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext
-fi
-rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext
-   ac_c_werror_flag=$ac_save_c_werror_flag
-fi
-{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_prog_cc_g" >&5
-$as_echo "$ac_cv_prog_cc_g" >&6; }
-if test "$ac_test_CFLAGS" = set; then
-  CFLAGS=$ac_save_CFLAGS
-elif test $ac_cv_prog_cc_g = yes; then
-  if test "$GCC" = yes; then
-    CFLAGS="-g -O2"
-  else
-    CFLAGS="-g"
-  fi
-else
-  if test "$GCC" = yes; then
-    CFLAGS="-O2"
-  else
-    CFLAGS=
-  fi
-fi
-{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $CC option to accept ISO C89" >&5
-$as_echo_n "checking for $CC option to accept ISO C89... " >&6; }
-if ${ac_cv_prog_cc_c89+:} false; then :
-  $as_echo_n "(cached) " >&6
-else
-  ac_cv_prog_cc_c89=no
-ac_save_CC=$CC
-cat confdefs.h - <<_ACEOF >conftest.$ac_ext
-/* end confdefs.h.  */
-#include <stdarg.h>
-#include <stdio.h>
-struct stat;
-/* Most of the following tests are stolen from RCS 5.7's src/conf.sh.  */
-struct buf { int x; };
-FILE * (*rcsopen) (struct buf *, struct stat *, int);
-static char *e (p, i)
-     char **p;
-     int i;
-{
-  return p[i];
-}
-static char *f (char * (*g) (char **, int), char **p, ...)
-{
-  char *s;
-  va_list v;
-  va_start (v,p);
-  s = g (p, va_arg (v,int));
-  va_end (v);
-  return s;
-}
-
-/* OSF 4.0 Compaq cc is some sort of almost-ANSI by default.  It has
-   function prototypes and stuff, but not '\xHH' hex character constants.
-   These don't provoke an error unfortunately, instead are silently treated
-   as 'x'.  The following induces an error, until -std is added to get
-   proper ANSI mode.  Curiously '\x00'!='x' always comes out true, for an
-   array size at least.  It's necessary to write '\x00'==0 to get something
-   that's true only with -std.  */
-int osf4_cc_array ['\x00' == 0 ? 1 : -1];
-
-/* IBM C 6 for AIX is almost-ANSI by default, but it replaces macro parameters
-   inside strings and character constants.  */
-#define FOO(x) 'x'
-int xlc6_cc_array[FOO(a) == 'x' ? 1 : -1];
-
-int test (int i, double x);
-struct s1 {int (*f) (int a);};
-struct s2 {int (*f) (double a);};
-int pairnames (int, char **, FILE *(*)(struct buf *, struct stat *, int), int, int);
-int argc;
-char **argv;
-int
-main ()
-{
-return f (e, argv, 0) != argv[0]  ||  f (e, argv, 1) != argv[1];
-  ;
-  return 0;
-}
-_ACEOF
-for ac_arg in '' -qlanglvl=extc89 -qlanglvl=ansi -std \
-	-Ae "-Aa -D_HPUX_SOURCE" "-Xc -D__EXTENSIONS__"
-do
-  CC="$ac_save_CC $ac_arg"
-  if ac_fn_c_try_compile "$LINENO"; then :
-  ac_cv_prog_cc_c89=$ac_arg
-fi
-rm -f core conftest.err conftest.$ac_objext
-  test "x$ac_cv_prog_cc_c89" != "xno" && break
-done
-rm -f conftest.$ac_ext
-CC=$ac_save_CC
-
-fi
-# AC_CACHE_VAL
-case "x$ac_cv_prog_cc_c89" in
-  x)
-    { $as_echo "$as_me:${as_lineno-$LINENO}: result: none needed" >&5
-$as_echo "none needed" >&6; } ;;
-  xno)
-    { $as_echo "$as_me:${as_lineno-$LINENO}: result: unsupported" >&5
-$as_echo "unsupported" >&6; } ;;
-  *)
-    CC="$CC $ac_cv_prog_cc_c89"
-    { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_prog_cc_c89" >&5
-$as_echo "$ac_cv_prog_cc_c89" >&6; } ;;
-esac
-if test "x$ac_cv_prog_cc_c89" != xno; then :
-
-fi
-
-ac_ext=c
-ac_cpp='$CPP $CPPFLAGS'
-ac_compile='$CC -c $CFLAGS $CPPFLAGS conftest.$ac_ext >&5'
-ac_link='$CC -o conftest$ac_exeext $CFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS >&5'
-ac_compiler_gnu=$ac_cv_c_compiler_gnu
-
 
 ac_ext=c
 ac_cpp='$CPP $CPPFLAGS'
@@ -5085,6 +4899,7 @@ fi
 
 CPPFLAGS="$old_CPPFLAGS"
 
+STP_NEEDS_MINISAT=0
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking for vc_setInterfaceFlags in -lstp" >&5
 $as_echo_n "checking for vc_setInterfaceFlags in -lstp... " >&6; }
 if ${ac_cv_lib_stp_vc_setInterfaceFlags+:} false; then :
@@ -5130,8 +4945,69 @@ _ACEOF
 
 else
 
-       as_fn_error $? "Could not link with libstp" "$LINENO" 5
+       STP_NEEDS_MINISAT=1; { $as_echo "$as_me:${as_lineno-$LINENO}: result: Could not link with libstp" >&5
+$as_echo "Could not link with libstp" >&6; }
+
+fi
+
+
+if test "X$STP_NEEDS_MINISAT" != X0 ; then
+  # Need to clear cached result
+  unset ac_cv_lib_stp_vc_setInterfaceFlags
 
+  { $as_echo "$as_me:${as_lineno-$LINENO}: checking for vc_setInterfaceFlags in -lstp" >&5
+$as_echo_n "checking for vc_setInterfaceFlags in -lstp... " >&6; }
+if ${ac_cv_lib_stp_vc_setInterfaceFlags+:} false; then :
+  $as_echo_n "(cached) " >&6
+else
+  ac_check_lib_save_LIBS=$LIBS
+LIBS="-lstp "$STP_LDFLAGS" "-lminisat"  $LIBS"
+cat confdefs.h - <<_ACEOF >conftest.$ac_ext
+/* end confdefs.h.  */
+
+/* Override any GCC internal prototype to avoid an error.
+   Use char because int might match the return type of a GCC
+   builtin and then its argument prototype would still apply.  */
+#ifdef __cplusplus
+extern "C"
+#endif
+char vc_setInterfaceFlags ();
+int
+main ()
+{
+return vc_setInterfaceFlags ();
+  ;
+  return 0;
+}
+_ACEOF
+if ac_fn_cxx_try_link "$LINENO"; then :
+  ac_cv_lib_stp_vc_setInterfaceFlags=yes
+else
+  ac_cv_lib_stp_vc_setInterfaceFlags=no
+fi
+rm -f core conftest.err conftest.$ac_objext \
+    conftest$ac_exeext conftest.$ac_ext
+LIBS=$ac_check_lib_save_LIBS
+fi
+{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_lib_stp_vc_setInterfaceFlags" >&5
+$as_echo "$ac_cv_lib_stp_vc_setInterfaceFlags" >&6; }
+if test "x$ac_cv_lib_stp_vc_setInterfaceFlags" = xyes; then :
+  cat >>confdefs.h <<_ACEOF
+#define HAVE_LIBSTP 1
+_ACEOF
+
+  LIBS="-lstp $LIBS"
+
+else
+
+	       as_fn_error $? "Unable to link with libstp. Check config.log to see what went wrong" "$LINENO" 5
+
+fi
+
+
+  STP_LDFLAGS="${STP_LDFLAGS} -lstp -lminisat"
+else
+  STP_LDFLAGS="${STP_LDFLAGS} -lstp"
 fi
 
 
diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h
index 97b700c1..32f840f6 100644
--- a/include/klee/ExecutionState.h
+++ b/include/klee/ExecutionState.h
@@ -23,14 +23,14 @@
 #include <vector>
 
 namespace klee {
-  class Array;
-  class CallPathNode;
-  struct Cell;
-  struct KFunction;
-  struct KInstruction;
-  class MemoryObject;
-  class PTreeNode;
-  struct InstructionInfo;
+class Array;
+class CallPathNode;
+struct Cell;
+struct KFunction;
+struct KInstruction;
+class MemoryObject;
+class PTreeNode;
+struct InstructionInfo;
 
 llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const MemoryMap &mm);
 
@@ -39,7 +39,7 @@ struct StackFrame {
   KFunction *kf;
   CallPathNode *callPathNode;
 
-  std::vector<const MemoryObject*> allocas;
+  std::vector<const MemoryObject *> allocas;
   Cell *locals;
 
   /// Minimum distance to an uncovered instruction once the function
@@ -61,56 +61,92 @@ struct StackFrame {
   ~StackFrame();
 };
 
+/// @brief ExecutionState representing a path under exploration
 class ExecutionState {
 public:
   typedef std::vector<StackFrame> stack_ty;
 
 private:
   // unsupported, use copy constructor
-  ExecutionState &operator=(const ExecutionState&); 
-  std::map< std::string, std::string > fnAliases;
+  ExecutionState &operator=(const ExecutionState &);
+
+  std::map<std::string, std::string> fnAliases;
 
 public:
-  bool fakeState;
-  unsigned depth;
-  
-  // pc - pointer to current instruction stream
-  KInstIterator pc, prevPC;
+  // Execution - Control Flow specific
+
+  /// @brief Pointer to instruction to be executed after the current
+  /// instruction
+  KInstIterator pc;
+
+  /// @brief Pointer to instruction which is currently executed
+  KInstIterator prevPC;
+
+  /// @brief Stack representing the current instruction stream
   stack_ty stack;
+
+  /// @brief Remember from which Basic Block control flow arrived
+  /// (i.e. to select the right phi values)
+  unsigned incomingBBIndex;
+
+  // Overall state of the state - Data specific
+
+  /// @brief Address space used by this state (e.g. Global and Heap)
+  AddressSpace addressSpace;
+
+  /// @brief Constraints collected so far
   ConstraintManager constraints;
+
+  /// Statistics and information
+
+  /// @brief Costs for all queries issued for this state, in seconds
   mutable double queryCost;
+
+  /// @brief Weight assigned for importance of this state.  Can be
+  /// used for searchers to decide what paths to explore
   double weight;
-  AddressSpace addressSpace;
-  TreeOStream pathOS, symPathOS;
+
+  /// @brief Exploration depth, i.e., number of times KLEE branched for this state
+  unsigned depth;
+
+  /// @brief History of complete path: represents branches taken to
+  /// reach/create this state (both concrete and symbolic)
+  TreeOStream pathOS;
+
+  /// @brief History of symbolic path: represents symbolic branches
+  /// taken to reach/create this state
+  TreeOStream symPathOS;
+
+  /// @brief Counts how many instructions were executed since the last new
+  /// instruction was covered.
   unsigned instsSinceCovNew;
+
+  /// @brief Whether a new instruction was covered in this state
   bool coveredNew;
 
-  /// Disables forking, set by user code.
+  /// @brief Disables forking for this state. Set by user code
   bool forkDisabled;
 
-  std::map<const std::string*, std::set<unsigned> > coveredLines;
+  /// @brief Set containing which lines in which files are covered by this state
+  std::map<const std::string *, std::set<unsigned> > coveredLines;
+
+  /// @brief Pointer to the process tree of the current state
   PTreeNode *ptreeNode;
 
-  /// ordered list of symbolics: used to generate test cases. 
+  /// @brief Ordered list of symbolics: used to generate test cases.
   //
   // FIXME: Move to a shared list structure (not critical).
-  std::vector< std::pair<const MemoryObject*, const Array*> > symbolics;
+  std::vector<std::pair<const MemoryObject *, const Array *> > symbolics;
 
-  /// Set of used array names.  Used to avoid collisions.
+  /// @brief Set of used array names for this state.  Used to avoid collisions.
   std::set<std::string> arrayNames;
 
-  // Used by the checkpoint/rollback methods for fake objects.
-  // FIXME: not freeing things on branch deletion.
-  MemoryMap shadowObjects;
-
-  unsigned incomingBBIndex;
-
   std::string getFnAlias(std::string fn);
   void addFnAlias(std::string old_fn, std::string new_fn);
   void removeFnAlias(std::string fn);
-  
+
 private:
-  ExecutionState() : fakeState(false), ptreeNode(0) {}
+  ExecutionState() : ptreeNode(0) {}
 
 public:
   ExecutionState(KFunction *kf);
@@ -119,24 +155,21 @@ public:
   // use on structure
   ExecutionState(const std::vector<ref<Expr> > &assumptions);
 
-  ExecutionState(const ExecutionState& state);
+  ExecutionState(const ExecutionState &state);
 
   ~ExecutionState();
-  
+
   ExecutionState *branch();
 
   void pushFrame(KInstIterator caller, KFunction *kf);
   void popFrame();
 
   void addSymbolic(const MemoryObject *mo, const Array *array);
-  void addConstraint(ref<Expr> e) { 
-    constraints.addConstraint(e); 
-  }
+  void addConstraint(ref<Expr> e) { constraints.addConstraint(e); }
 
   bool merge(const ExecutionState &b);
   void dumpStack(llvm::raw_ostream &out) const;
 };
-
 }
 
 #endif
diff --git a/include/klee/Internal/Module/KInstruction.h b/include/klee/Internal/Module/KInstruction.h
index fc86070b..62f514ff 100644
--- a/include/klee/Internal/Module/KInstruction.h
+++ b/include/klee/Internal/Module/KInstruction.h
@@ -50,7 +50,7 @@ namespace klee {
     std::vector< std::pair<unsigned, uint64_t> > indices;
 
     /// offset - A constant offset to add to the pointer operand to execute the
-    /// insturction.
+    /// instruction.
     uint64_t offset;
   };
 }
diff --git a/include/klee/Internal/Module/KModule.h b/include/klee/Internal/Module/KModule.h
index 80672b5e..76db4694 100644
--- a/include/klee/Internal/Module/KModule.h
+++ b/include/klee/Internal/Module/KModule.h
@@ -92,7 +92,7 @@ namespace klee {
 #endif
     
     // Some useful functions to know the address of
-    llvm::Function *dbgStopPointFn, *kleeMergeFn;
+    llvm::Function *kleeMergeFn;
 
     // Our shadow versions of LLVM structures.
     std::vector<KFunction*> functions;
diff --git a/include/klee/Internal/System/Time.h b/include/klee/Internal/System/Time.h
index 5229c8c9..14d23536 100644
--- a/include/klee/Internal/System/Time.h
+++ b/include/klee/Internal/System/Time.h
@@ -10,10 +10,19 @@
 #ifndef KLEE_UTIL_TIME_H
 #define KLEE_UTIL_TIME_H
 
+#include <llvm/Support/TimeValue.h>
+
 namespace klee {
   namespace util {
+
+    /// Seconds spent by this process in user mode.
     double getUserTime();
+
+    /// Wall time in seconds.
     double getWallTime();
+
+    /// Wall time as TimeValue object.
+    llvm::sys::TimeValue getWallTimeVal();
   }
 }
 
diff --git a/include/klee/klee.h b/include/klee/klee.h
index ce92ba37..032e5243 100644
--- a/include/klee/klee.h
+++ b/include/klee/klee.h
@@ -1,11 +1,11 @@
-//===-- klee.h --------------------------------------------------*- C++ -*-===//
+/*===-- klee.h --------------------------------------------------*- C++ -*-===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
-//===----------------------------------------------------------------------===//
+//===----------------------------------------------------------------------===*/
 
 #ifndef __KLEE_H__
 #define __KLEE_H__
@@ -18,51 +18,57 @@ extern "C" {
 #endif
   
   /* Add an accesible memory object at a user specified location. It
-     is the users responsibility to make sure that these memory
-     objects do not overlap. These memory objects will also
-     (obviously) not correctly interact with external function
-     calls. */
+   * is the users responsibility to make sure that these memory
+   * objects do not overlap. These memory objects will also
+   * (obviously) not correctly interact with external function
+   * calls.
+   */
   void klee_define_fixed_object(void *addr, size_t nbytes);
 
-  /// klee_make_symbolic - Make the contents of the object pointer to by \arg
-  /// addr symbolic. 
-  ///
-  /// \arg addr - The start of the object.
-  /// \arg nbytes - The number of bytes to make symbolic; currently this *must*
-  /// be the entire contents of the object.
-  /// \arg name - An optional name, used for identifying the object in messages,
-  /// output files, etc.
+  /* klee_make_symbolic - Make the contents of the object pointer to by \arg
+   * addr symbolic.
+   *
+   * \arg addr - The start of the object.
+   * \arg nbytes - The number of bytes to make symbolic; currently this *must*
+   * be the entire contents of the object.
+   * \arg name - An optional name, used for identifying the object in messages,
+   * output files, etc.
+   */
   void klee_make_symbolic(void *addr, size_t nbytes, const char *name);
 
-  /// klee_range - Construct a symbolic value in the signed interval
-  /// [begin,end).
-  ///
-  /// \arg name - An optional name, used for identifying the object in messages,
-  /// output files, etc.
+  /* klee_range - Construct a symbolic value in the signed interval
+   * [begin,end).
+   *
+   * \arg name - An optional name, used for identifying the object in messages,
+   * output files, etc.
+   */
   int klee_range(int begin, int end, const char *name);
 
-  /// klee_int - Construct an unconstrained symbolic integer.
-  ///
-  /// \arg name - An optional name, used for identifying the object in messages,
-  /// output files, etc.
+  /*  klee_int - Construct an unconstrained symbolic integer.
+   *
+   * \arg name - An optional name, used for identifying the object in messages,
+   * output files, etc.
+   */
   int klee_int(const char *name);
 
-  /// klee_silent_exit - Terminate the current KLEE process without generating a
-  /// test file.
+  /* klee_silent_exit - Terminate the current KLEE process without generating a
+   * test file.
+   */
   __attribute__((noreturn))
   void klee_silent_exit(int status);
 
-  /// klee_abort - Abort the current KLEE process.
+  /* klee_abort - Abort the current KLEE process. */
   __attribute__((noreturn))
   void klee_abort(void);  
 
-  /// klee_report_error - Report a user defined error and terminate the current
-  /// KLEE process.
-  ///
-  /// \arg file - The filename to report in the error message.
-  /// \arg line - The line number to report in the error message.
-  /// \arg message - A string to include in the error message.
-  /// \arg suffix - The suffix to use for error files.
+  /* klee_report_error - Report a user defined error and terminate the current
+   * KLEE process.
+   *
+   * \arg file - The filename to report in the error message.
+   * \arg line - The line number to report in the error message.
+   * \arg message - A string to include in the error message.
+   * \arg suffix - The suffix to use for error files.
+   */
   __attribute__((noreturn))
   void klee_report_error(const char *file, 
 			 int line, 
@@ -142,6 +148,11 @@ extern "C" {
   /* Print stack trace. */
   void klee_stack_trace(void);
 
+  /* Print range for given argument and tagged with name */
+  void klee_print_range(const char * name, int arg );
+
+  /* Merge current states together if possible */
+  void klee_merge();
 #ifdef __cplusplus
 }
 #endif
diff --git a/include/klee/util/ExprSMTLIBPrinter.h b/include/klee/util/ExprSMTLIBPrinter.h
index 6b0d260a..e90a49f1 100644
--- a/include/klee/util/ExprSMTLIBPrinter.h
+++ b/include/klee/util/ExprSMTLIBPrinter.h
@@ -319,6 +319,7 @@ protected:
   void printNotEqualExpr(const ref<NeExpr> &e);
   void printSelectExpr(const ref<SelectExpr> &e,
                                ExprSMTLIBPrinter::SMTLIB_SORT s);
+  void printAShrExpr(const ref<AShrExpr> &e);
 
   // For the set of operators that take sort "s" arguments
   void printSortArgsExpr(const ref<Expr> &e,
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 5d32c936..6aeaa833 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -66,13 +66,14 @@ StackFrame::~StackFrame() {
 
 /***/
 
-ExecutionState::ExecutionState(KFunction *kf) 
-  : fakeState(false),
-    depth(0),
+ExecutionState::ExecutionState(KFunction *kf) :
     pc(kf->instructions),
     prevPC(pc),
+
     queryCost(0.), 
     weight(1),
+    depth(0),
+
     instsSinceCovNew(0),
     coveredNew(false),
     forkDisabled(false),
@@ -80,12 +81,8 @@ ExecutionState::ExecutionState(KFunction *kf)
   pushFrame(0, kf);
 }
 
-ExecutionState::ExecutionState(const std::vector<ref<Expr> > &assumptions) 
-  : fakeState(true),
-    constraints(assumptions),
-    queryCost(0.),
-    ptreeNode(0) {
-}
+ExecutionState::ExecutionState(const std::vector<ref<Expr> > &assumptions)
+    : constraints(assumptions), queryCost(0.), ptreeNode(0) {}
 
 ExecutionState::~ExecutionState() {
   for (unsigned int i=0; i<symbolics.size(); i++)
@@ -100,28 +97,30 @@ ExecutionState::~ExecutionState() {
   while (!stack.empty()) popFrame();
 }
 
-ExecutionState::ExecutionState(const ExecutionState& state)
-  : fnAliases(state.fnAliases),
-    fakeState(state.fakeState),
-    depth(state.depth),
+ExecutionState::ExecutionState(const ExecutionState& state):
+    fnAliases(state.fnAliases),
     pc(state.pc),
     prevPC(state.prevPC),
     stack(state.stack),
+    incomingBBIndex(state.incomingBBIndex),
+
+    addressSpace(state.addressSpace),
     constraints(state.constraints),
+
     queryCost(state.queryCost),
     weight(state.weight),
-    addressSpace(state.addressSpace),
+    depth(state.depth),
+
     pathOS(state.pathOS),
     symPathOS(state.symPathOS),
+
     instsSinceCovNew(state.instsSinceCovNew),
     coveredNew(state.coveredNew),
     forkDisabled(state.forkDisabled),
     coveredLines(state.coveredLines),
     ptreeNode(state.ptreeNode),
     symbolics(state.symbolics),
-    arrayNames(state.arrayNames),
-    shadowObjects(state.shadowObjects),
-    incomingBBIndex(state.incomingBBIndex)
+    arrayNames(state.arrayNames)
 {
   for (unsigned int i=0; i<symbolics.size(); i++)
     symbolics[i].first->refCount++;
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index c78c9f8a..45876659 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -2592,9 +2592,7 @@ void Executor::run(ExecutionState &initialState) {
             unsigned numStates = states.size();
             unsigned toKill = std::max(1U, numStates - numStates*MaxMemory/mbs);
 
-            if (MaxMemoryInhibit)
-              klee_warning("killing %d states (over memory cap)",
-                           toKill);
+            klee_warning("killing %d states (over memory cap)", toKill);
 
             std::vector<ExecutionState*> arr(states.begin(), states.end());
             for (unsigned i=0,N=arr.size(); N && i<toKill; ++i,--N) {
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index 1dd1e1fd..07c292a0 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -468,7 +468,7 @@ ref<Expr> ObjectState::read(ref<Expr> offset, Expr::Width width) const {
 
   // Otherwise, follow the slow general case.
   unsigned NumBytes = width / 8;
-  assert(width == NumBytes * 8 && "Invalid write size!");
+  assert(width == NumBytes * 8 && "Invalid read size!");
   ref<Expr> Res(0);
   for (unsigned i = 0; i != NumBytes; ++i) {
     unsigned idx = Context::get().isLittleEndian() ? i : (NumBytes - i - 1);
@@ -488,7 +488,7 @@ ref<Expr> ObjectState::read(unsigned offset, Expr::Width width) const {
 
   // Otherwise, follow the slow general case.
   unsigned NumBytes = width / 8;
-  assert(width == NumBytes * 8 && "Invalid write size!");
+  assert(width == NumBytes * 8 && "Invalid width for read size!");
   ref<Expr> Res(0);
   for (unsigned i = 0; i != NumBytes; ++i) {
     unsigned idx = Context::get().isLittleEndian() ? i : (NumBytes - i - 1);
diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp
index 037b23f3..b70bcbef 100644
--- a/lib/Core/TimingSolver.cpp
+++ b/lib/Core/TimingSolver.cpp
@@ -13,10 +13,11 @@
 #include "klee/ExecutionState.h"
 #include "klee/Solver.h"
 #include "klee/Statistics.h"
+#include "klee/Internal/System/Time.h"
 
 #include "CoreStats.h"
 
-#include "llvm/Support/Process.h"
+#include "llvm/Support/TimeValue.h"
 
 using namespace klee;
 using namespace llvm;
@@ -31,15 +32,14 @@ bool TimingSolver::evaluate(const ExecutionState& state, ref<Expr> expr,
     return true;
   }
 
-  sys::TimeValue now(0,0),user(0,0),delta(0,0),sys(0,0);
-  sys::Process::GetTimeUsage(now,user,sys);
+  sys::TimeValue now = util::getWallTimeVal();
 
   if (simplifyExprs)
     expr = state.constraints.simplifyExpr(expr);
 
   bool success = solver->evaluate(Query(state.constraints, expr), result);
 
-  sys::Process::GetTimeUsage(delta,user,sys);
+  sys::TimeValue delta = util::getWallTimeVal();
   delta -= now;
   stats::solverTime += delta.usec();
   state.queryCost += delta.usec()/1000000.;
@@ -55,15 +55,14 @@ bool TimingSolver::mustBeTrue(const ExecutionState& state, ref<Expr> expr,
     return true;
   }
 
-  sys::TimeValue now(0,0),user(0,0),delta(0,0),sys(0,0);
-  sys::Process::GetTimeUsage(now,user,sys);
+  sys::TimeValue now = util::getWallTimeVal();
 
   if (simplifyExprs)
     expr = state.constraints.simplifyExpr(expr);
 
   bool success = solver->mustBeTrue(Query(state.constraints, expr), result);
 
-  sys::Process::GetTimeUsage(delta,user,sys);
+  sys::TimeValue delta = util::getWallTimeVal();
   delta -= now;
   stats::solverTime += delta.usec();
   state.queryCost += delta.usec()/1000000.;
@@ -102,15 +101,14 @@ bool TimingSolver::getValue(const ExecutionState& state, ref<Expr> expr,
     return true;
   }
   
-  sys::TimeValue now(0,0),user(0,0),delta(0,0),sys(0,0);
-  sys::Process::GetTimeUsage(now,user,sys);
+  sys::TimeValue now = util::getWallTimeVal();
 
   if (simplifyExprs)
     expr = state.constraints.simplifyExpr(expr);
 
   bool success = solver->getValue(Query(state.constraints, expr), result);
 
-  sys::Process::GetTimeUsage(delta,user,sys);
+  sys::TimeValue delta = util::getWallTimeVal();
   delta -= now;
   stats::solverTime += delta.usec();
   state.queryCost += delta.usec()/1000000.;
@@ -127,14 +125,13 @@ TimingSolver::getInitialValues(const ExecutionState& state,
   if (objects.empty())
     return true;
 
-  sys::TimeValue now(0,0),user(0,0),delta(0,0),sys(0,0);
-  sys::Process::GetTimeUsage(now,user,sys);
+  sys::TimeValue now = util::getWallTimeVal();
 
   bool success = solver->getInitialValues(Query(state.constraints,
                                                 ConstantExpr::alloc(0, Expr::Bool)), 
                                           objects, result);
   
-  sys::Process::GetTimeUsage(delta,user,sys);
+  sys::TimeValue delta = util::getWallTimeVal();
   delta -= now;
   stats::solverTime += delta.usec();
   state.queryCost += delta.usec()/1000000.;
diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp
index ae4563f4..dbdfd999 100644
--- a/lib/Expr/Constraints.cpp
+++ b/lib/Expr/Constraints.cpp
@@ -23,6 +23,14 @@
 
 using namespace klee;
 
+namespace {
+  llvm::cl::opt<bool>
+  RewriteEqualities("rewrite-equalities",
+		    llvm::cl::init(true),
+		    llvm::cl::desc("Rewrite existing constraints when an equality with a constant is added (default=on)"));
+}
+
+
 class ExprReplaceVisitor : public ExprVisitor {
 private:
   ref<Expr> src, dst;
@@ -118,13 +126,7 @@ ref<Expr> ConstraintManager::simplifyExpr(ref<Expr> e) const {
 }
 
 void ConstraintManager::addConstraintInternal(ref<Expr> e) {
-  // rewrite any known equalities 
-
-  // XXX should profile the effects of this and the overhead.
-  // traversing the constraints looking for equalities is hardly the
-  // slowest thing we do, but it is probably nicer to have a
-  // ConstraintSet ADT which efficiently remembers obvious patterns
-  // (byte-constant comparison).
+  // rewrite any known equalities and split Ands into different conjuncts
 
   switch (e->getKind()) {
   case Expr::Constant:
@@ -141,10 +143,17 @@ void ConstraintManager::addConstraintInternal(ref<Expr> e) {
   }
 
   case Expr::Eq: {
-    BinaryExpr *be = cast<BinaryExpr>(e);
-    if (isa<ConstantExpr>(be->left)) {
-      ExprReplaceVisitor visitor(be->right, be->left);
-      rewriteConstraints(visitor);
+    if (RewriteEqualities) {
+      // XXX: should profile the effects of this and the overhead.
+      // traversing the constraints looking for equalities is hardly the
+      // slowest thing we do, but it is probably nicer to have a
+      // ConstraintSet ADT which efficiently remembers obvious patterns
+      // (byte-constant comparison).
+      BinaryExpr *be = cast<BinaryExpr>(e);
+      if (isa<ConstantExpr>(be->left)) {
+	ExprReplaceVisitor visitor(be->right, be->left);
+	rewriteConstraints(visitor);
+      }
     }
     constraints.push_back(e);
     break;
diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp
index c780ae90..e8e9a253 100644
--- a/lib/Expr/ExprSMTLIBPrinter.cpp
+++ b/lib/Expr/ExprSMTLIBPrinter.cpp
@@ -255,7 +255,10 @@ void ExprSMTLIBPrinter::printFullExpression(
      * type T.
      */
     printLogicalOrBitVectorExpr(e, expectedSort);
+    return;
 
+  case Expr::AShr:
+    printAShrExpr(cast<AShrExpr>(e));
     return;
 
   default:
@@ -334,6 +337,73 @@ void ExprSMTLIBPrinter::printCastExpr(const ref<CastExpr> &e) {
   *p << ")";
 }
 
+void ExprSMTLIBPrinter::printAShrExpr(const ref<AShrExpr> &e) {
+  // There is a difference between AShr and SMT-LIBv2's
+  // bvashr function when the shift amount is >= the bit width
+  // so we need to treat it specially here.
+  //
+  // Technically this is undefined behaviour for LLVM's ashr operator
+  // but currently llvm::APInt:ashr(...) will emit 0 if the shift amount
+  // is >= the bit width but this does not match how SMT-LIBv2's bvashr
+  // behaves as demonstrates by the following query
+  //
+  // (declare-fun x () (_ BitVec 32))
+  // (declare-fun y () (_ BitVec 32))
+  // (declare-fun result () (_ BitVec 32))
+  // (assert (bvuge y (_ bv32 32)))
+  // (assert (= result (bvashr x y)))
+  // (assert (distinct (_ bv0 32) result))
+  // (check-sat)
+  // sat
+  //
+  // Our solution is to instead emit
+  //
+  // (ite (bvuge shift_amount bit_width)
+  //      (_ bv0 bitwidth)
+  //      (bvashr value_to_shift shift_amount)
+  // )
+  //
+
+  Expr::Width bitWidth = e->getKid(0)->getWidth();
+  assert(bitWidth > 0 && "Invalid bit width");
+  ref<Expr> bitWidthExpr = ConstantExpr::create(bitWidth, bitWidth);
+  ref<Expr> zeroExpr = ConstantExpr::create(0, bitWidth);
+
+  // FIXME: we print e->getKid(1) twice and it might not get
+  // abbreviated
+  *p << "(ite";
+  p->pushIndent();
+  printSeperator();
+
+  *p << "(bvuge";
+  p->pushIndent();
+  printSeperator();
+  printExpression(e->getKid(1), SORT_BITVECTOR);
+  printSeperator();
+  printExpression(bitWidthExpr, SORT_BITVECTOR);
+  p->popIndent();
+  printSeperator();
+  *p << ")";
+
+  printSeperator();
+  printExpression(zeroExpr, SORT_BITVECTOR);
+  printSeperator();
+
+  *p << "(bvashr";
+  p->pushIndent();
+  printSeperator();
+  printExpression(e->getKid(0), SORT_BITVECTOR);
+  printSeperator();
+  printExpression(e->getKid(1), SORT_BITVECTOR);
+  p->popIndent();
+  printSeperator();
+  *p << ")";
+
+  p->popIndent();
+  printSeperator();
+  *p << ")";
+}
+
 const char *ExprSMTLIBPrinter::getSMTLIBKeyword(const ref<Expr> &e) {
 
   switch (e->getKind()) {
@@ -373,8 +443,7 @@ const char *ExprSMTLIBPrinter::getSMTLIBKeyword(const ref<Expr> &e) {
     return "bvshl";
   case Expr::LShr:
     return "bvlshr";
-  case Expr::AShr:
-    return "bvashr";
+  // AShr is not supported here. See printAShrExpr()
 
   case Expr::Eq:
     return "=";
diff --git a/lib/Module/RaiseAsm.cpp b/lib/Module/RaiseAsm.cpp
index d9145a1e..12e5479b 100644
--- a/lib/Module/RaiseAsm.cpp
+++ b/lib/Module/RaiseAsm.cpp
@@ -66,17 +66,18 @@ bool RaiseAsmPass::runOnModule(Module &M) {
   std::string HostTriple = llvm::sys::getHostTriple();
 #endif
   const Target *NativeTarget = TargetRegistry::lookupTarget(HostTriple, Err);
+  TargetMachine * TM = 0;
   if (NativeTarget == 0) {
     llvm::errs() << "Warning: unable to select native target: " << Err << "\n";
     TLI = 0;
   } else {
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1)
-    TargetMachine *TM = NativeTarget->createTargetMachine(HostTriple, "", "",
+    TM = NativeTarget->createTargetMachine(HostTriple, "", "",
                                                           TargetOptions());
 #elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 0)
-    TargetMachine *TM = NativeTarget->createTargetMachine(HostTriple, "", "");
+    TM = NativeTarget->createTargetMachine(HostTriple, "", "");
 #else
-    TargetMachine *TM = NativeTarget->createTargetMachine(HostTriple, "");
+    TM = NativeTarget->createTargetMachine(HostTriple, "");
 #endif
     TLI = TM->getTargetLowering();
   }
@@ -91,5 +92,8 @@ bool RaiseAsmPass::runOnModule(Module &M) {
     }
   }
 
+  if (TM)
+    delete TM;
+
   return changed;
 }
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 6d7dd8b7..a5e4c5ad 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -51,11 +51,6 @@ namespace {
 
 
 STPArrayExprHash::~STPArrayExprHash() {
-  
-  // Design decision: STPArrayExprHash is destroyed from the destructor of STPBuilder at the end of the KLEE run;
-  // Therefore, freeing memory allocated for STP::VCExpr's is currently disabled.
-  
-   /*
   for (ArrayHashIter it = _array_hash.begin(); it != _array_hash.end(); ++it) {
     ::VCExpr array_expr = it->second;
     if (array_expr) {
@@ -63,16 +58,16 @@ STPArrayExprHash::~STPArrayExprHash() {
       array_expr = 0;
     }
   }
-  
-  
-  for (UpdateNodeHashConstIter it = _update_node_hash.begin(); it != _update_node_hash.end(); ++it) {
+
+
+  for (UpdateNodeHashConstIter it = _update_node_hash.begin();
+      it != _update_node_hash.end(); ++it) {
     ::VCExpr un_expr = it->second;
     if (un_expr) {
       ::vc_DeleteExpr(un_expr);
       un_expr = 0;
     }
   }
-  */
 }
 
 /***/
@@ -218,10 +213,9 @@ ExprHandle STPBuilder::bvVarLeftShift(ExprHandle expr, ExprHandle shift) {
   }
 
   // If overshifting, shift to zero
-  res = vc_iteExpr(vc,
-                   vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)),
-                   res,
-                   bvZero(width));
+  ExprHandle ex = vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width));
+
+  res = vc_iteExpr(vc, ex, res, bvZero(width));
   return res;
 }
 
@@ -239,8 +233,9 @@ ExprHandle STPBuilder::bvVarRightShift(ExprHandle expr, ExprHandle shift) {
   }
 
   // If overshifting, shift to zero
+  ExprHandle ex = vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width));
   res = vc_iteExpr(vc,
-                   vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)),
+                   ex,
                    res,
                    bvZero(width));
   return res;
@@ -269,8 +264,9 @@ ExprHandle STPBuilder::bvVarArithRightShift(ExprHandle expr, ExprHandle shift) {
   }
 
   // If overshifting, shift to zero
+  ExprHandle ex = vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width));
   res = vc_iteExpr(vc,
-                   vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)),
+                   ex,
                    res,
                    bvZero(width));
   return res;
diff --git a/lib/Support/Time.cpp b/lib/Support/Time.cpp
index 909e07da..be5eaf18 100644
--- a/lib/Support/Time.cpp
+++ b/lib/Support/Time.cpp
@@ -10,6 +10,7 @@
 #include "klee/Config/Version.h"
 #include "klee/Internal/System/Time.h"
 
+#include "llvm/Support/TimeValue.h"
 #include "llvm/Support/Process.h"
 
 using namespace llvm;
@@ -22,7 +23,10 @@ double util::getUserTime() {
 }
 
 double util::getWallTime() {
-  sys::TimeValue now(0,0),user(0,0),sys(0,0);
-  sys::Process::GetTimeUsage(now,user,sys);
-  return (now.seconds() + (double) now.nanoseconds() * 1e-9);
+  sys::TimeValue now = getWallTimeVal();
+  return (now.seconds() + ((double) now.nanoseconds() * 1e-9));
+}
+
+sys::TimeValue util::getWallTimeVal() {
+  return sys::TimeValue::now();
 }
diff --git a/lib/Support/Timer.cpp b/lib/Support/Timer.cpp
index c61a90a3..da969810 100644
--- a/lib/Support/Timer.cpp
+++ b/lib/Support/Timer.cpp
@@ -10,19 +10,15 @@
 #include "klee/Config/Version.h"
 #include "klee/Internal/Support/Timer.h"
 
-#include "llvm/Support/Process.h"
+#include "klee/Internal/System/Time.h"
 
 using namespace klee;
 using namespace llvm;
 
 WallTimer::WallTimer() {
-  sys::TimeValue now(0,0),user(0,0),sys(0,0);
-  sys::Process::GetTimeUsage(now,user,sys);
-  startMicroseconds = now.usec();
+  startMicroseconds = util::getWallTimeVal().usec();
 }
 
 uint64_t WallTimer::check() {
-  sys::TimeValue now(0,0),user(0,0),sys(0,0);
-  sys::Process::GetTimeUsage(now,user,sys);
-  return now.usec() - startMicroseconds;
+  return util::getWallTimeVal().usec() - startMicroseconds;
 }
diff --git a/runtime/Intrinsic/klee_int.c b/runtime/Intrinsic/klee_int.c
index 56f0f9dc..6ea1e02e 100644
--- a/runtime/Intrinsic/klee_int.c
+++ b/runtime/Intrinsic/klee_int.c
@@ -8,7 +8,7 @@
 //===----------------------------------------------------------------------===//
 
 #include <assert.h>
-#include <klee/klee.h>
+#include "klee/klee.h"
 
 int klee_int(const char *name) {
   int x;
diff --git a/runtime/klee-libc/__cxa_atexit.c b/runtime/klee-libc/__cxa_atexit.c
index e7982848..990b645d 100644
--- a/runtime/klee-libc/__cxa_atexit.c
+++ b/runtime/klee-libc/__cxa_atexit.c
@@ -1,11 +1,11 @@
-//===-- __cxa_atexit.c ----------------------------------------------------===//
+/*===-- __cxa_atexit.c ----------------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
-//===----------------------------------------------------------------------===//
+//===----------------------------------------------------------------------===*/
 
 #include "klee/klee.h"
 
diff --git a/runtime/klee-libc/abort.c b/runtime/klee-libc/abort.c
index 0332d095..741bcf82 100644
--- a/runtime/klee-libc/abort.c
+++ b/runtime/klee-libc/abort.c
@@ -1,11 +1,11 @@
-//===-- abort.c -----------------------------------------------------------===//
+/*===-- abort.c -----------------------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
-//===----------------------------------------------------------------------===//
+//===----------------------------------------------------------------------===*/
 
 #include <stdlib.h>
 
diff --git a/runtime/klee-libc/atexit.c b/runtime/klee-libc/atexit.c
index c71b2cd6..7b3b53b5 100644
--- a/runtime/klee-libc/atexit.c
+++ b/runtime/klee-libc/atexit.c
@@ -1,11 +1,11 @@
-//===-- atexit.c ----------------------------------------------------------===//
+/*==-- atexit.c ----------------------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
-//===----------------------------------------------------------------------===//
+//===----------------------------------------------------------------------===*/
 
 int __cxa_atexit(void (*fn)(void*),
                  void *arg,
diff --git a/runtime/klee-libc/calloc.c b/runtime/klee-libc/calloc.c
index 30b88b30..1466fc07 100644
--- a/runtime/klee-libc/calloc.c
+++ b/runtime/klee-libc/calloc.c
@@ -1,16 +1,16 @@
-//===-- calloc.c ----------------------------------------------------------===//
+/*===-- calloc.c ----------------------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
-//===----------------------------------------------------------------------===//
+//===----------------------------------------------------------------------===*/
 
 #include <stdlib.h>
 #include <string.h>
 
-// DWD - I prefer to be internal
+/* DWD - I prefer to be internal */
 #if 0
 void *calloc(size_t nmemb, size_t size) {
 	unsigned nbytes = nmemb * size;
@@ -19,7 +19,8 @@ void *calloc(size_t nmemb, size_t size) {
 		memset(addr, 0, nbytes);
 	return addr;
 }
-// Always reallocate.
+
+/* Always reallocate. */
 void *realloc(void *ptr, size_t nbytes) {
 	if(!ptr)
 		return malloc(nbytes);
@@ -30,14 +31,14 @@ void *realloc(void *ptr, size_t nbytes) {
 	}
 
         unsigned copy_nbytes = klee_get_obj_size(ptr);
-	//printf("REALLOC: current object = %d bytes!\n", copy_nbytes);
+	/* printf("REALLOC: current object = %d bytes!\n", copy_nbytes); */
 
 	void *addr = malloc(nbytes);
 	if(addr) {
-		// shrinking
+	        /* shrinking */
 		if(copy_nbytes > nbytes)
 			copy_nbytes = nbytes;
-		//printf("REALLOC: copying = %d bytes!\n", copy_nbytes);
+		/* printf("REALLOC: copying = %d bytes!\n", copy_nbytes); */
 		memcpy(addr, ptr, copy_nbytes);
 		free(ptr);
 	} 
diff --git a/runtime/klee-libc/htonl.c b/runtime/klee-libc/htonl.c
index 521ef5d6..777ecf94 100644
--- a/runtime/klee-libc/htonl.c
+++ b/runtime/klee-libc/htonl.c
@@ -1,11 +1,11 @@
-//===-- htonl.c -----------------------------------------------------------===//
+/*===-- htonl.c -----------------------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
-//===----------------------------------------------------------------------===//
+//===----------------------------------------------------------------------===*/
 
 #include <sys/types.h>
 #include <sys/param.h>
@@ -16,7 +16,7 @@
 #undef ntohs
 #undef ntohl
 
-// Make sure we can recognize the endianness.
+/* Make sure we can recognize the endianness. */
 #if (!defined(BYTE_ORDER) || !defined(BIG_ENDIAN) || !defined(LITTLE_ENDIAN))
 #error "Unknown platform endianness!"
 #endif
diff --git a/runtime/klee-libc/klee-choose.c b/runtime/klee-libc/klee-choose.c
index 181aedaa..44e5cea2 100644
--- a/runtime/klee-libc/klee-choose.c
+++ b/runtime/klee-libc/klee-choose.c
@@ -1,11 +1,11 @@
-//===-- klee-choose.c -----------------------------------------------------===//
+/*===-- klee-choose.c -----------------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
-//===----------------------------------------------------------------------===//
+//===----------------------------------------------------------------------===*/
 
 #include "klee/klee.h"
 
@@ -13,7 +13,7 @@ uintptr_t klee_choose(uintptr_t n) {
   uintptr_t x;
   klee_make_symbolic(&x, sizeof x, "klee_choose");
 
-  // NB: this will *not* work if they don't compare to n values.
+  /* NB: this will *not* work if they don't compare to n values. */
   if(x >= n)
     klee_silent_exit(0);
   return x;
diff --git a/runtime/klee-libc/memcpy.c b/runtime/klee-libc/memcpy.c
index 7f7f133d..c7c6e6d3 100644
--- a/runtime/klee-libc/memcpy.c
+++ b/runtime/klee-libc/memcpy.c
@@ -1,11 +1,11 @@
-//===-- memcpy.c ----------------------------------------------------------===//
+/*===-- memcpy.c ----------------------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
-//===----------------------------------------------------------------------===//
+//===----------------------------------------------------------------------===*/
 
 #include <stdlib.h>
 
diff --git a/runtime/klee-libc/memmove.c b/runtime/klee-libc/memmove.c
index c6e1ada9..3e86de02 100644
--- a/runtime/klee-libc/memmove.c
+++ b/runtime/klee-libc/memmove.c
@@ -1,11 +1,11 @@
-//===-- memmove.c ---------------------------------------------------------===//
+/*===-- memmove.c ---------------------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
-//===----------------------------------------------------------------------===//
+//===----------------------------------------------------------------------===*/
 
 #include <stdlib.h>
 
diff --git a/runtime/klee-libc/mempcpy.c b/runtime/klee-libc/mempcpy.c
index 31e142d9..31712251 100644
--- a/runtime/klee-libc/mempcpy.c
+++ b/runtime/klee-libc/mempcpy.c
@@ -1,11 +1,11 @@
-//===-- mempcpy.c ---------------------------------------------------------===//
+/*===-- mempcpy.c ---------------------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
-//===----------------------------------------------------------------------===//
+//===----------------------------------------------------------------------===*/
 
 #include <stdlib.h>
 
diff --git a/runtime/klee-libc/memset.c b/runtime/klee-libc/memset.c
index ee9ecb87..81025d32 100644
--- a/runtime/klee-libc/memset.c
+++ b/runtime/klee-libc/memset.c
@@ -1,11 +1,11 @@
-//===-- memset.c ----------------------------------------------------------===//
+/*===-- memset.c ----------------------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
-//===----------------------------------------------------------------------===//
+//===----------------------------------------------------------------------===*/
 
 #include <stdlib.h>
 
diff --git a/runtime/klee-libc/putchar.c b/runtime/klee-libc/putchar.c
index 497402a6..bee2d2d7 100644
--- a/runtime/klee-libc/putchar.c
+++ b/runtime/klee-libc/putchar.c
@@ -1,16 +1,16 @@
-//===-- putchar.c ---------------------------------------------------------===//
+/*===-- putchar.c ---------------------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
-//===----------------------------------------------------------------------===//
+//===----------------------------------------------------------------------===*/
 
 #include <stdio.h>
 #include <unistd.h>
 
-// Some header may #define putchar.
+/* Some header may #define putchar. */
 #undef putchar
 
 int putchar(int c) {
diff --git a/runtime/klee-libc/strchr.c b/runtime/klee-libc/strchr.c
index 33f97bea..50f1b9f4 100644
--- a/runtime/klee-libc/strchr.c
+++ b/runtime/klee-libc/strchr.c
@@ -1,11 +1,11 @@
-//===-- strchr.c ----------------------------------------------------------===//
+/*===-- strchr.c ----------------------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
-//===----------------------------------------------------------------------===//
+//===----------------------------------------------------------------------===*/
 
 char *strchr(const char *p, int ch) {
   char c;
diff --git a/runtime/klee-libc/strcmp.c b/runtime/klee-libc/strcmp.c
index 6b8c4e85..cdb002c7 100644
--- a/runtime/klee-libc/strcmp.c
+++ b/runtime/klee-libc/strcmp.c
@@ -1,11 +1,11 @@
-//===-- strcmp.c ----------------------------------------------------------===//
+/*===-- strcmp.c ----------------------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
-//===----------------------------------------------------------------------===//
+//===----------------------------------------------------------------------===*/
 
 int strcmp(const char *a, const char *b) {
   while (*a && *a == *b)
diff --git a/runtime/klee-libc/strcoll.c b/runtime/klee-libc/strcoll.c
index 73d59f89..8f78b0b3 100644
--- a/runtime/klee-libc/strcoll.c
+++ b/runtime/klee-libc/strcoll.c
@@ -1,15 +1,15 @@
-//===-- strcoll.c ---------------------------------------------------------===//
+/*===-- strcoll.c ---------------------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
-//===----------------------------------------------------------------------===//
+//===----------------------------------------------------------------------===*/
 
 #include <string.h>
 
-// according to the manpage, this is equiv in the POSIX/C locale.
+/* according to the manpage, this is equiv in the POSIX/C locale. */
 int strcoll(const char *s1, const char *s2) {
   return strcmp(s1,s2);
 }
diff --git a/runtime/klee-libc/strcpy.c b/runtime/klee-libc/strcpy.c
index 0fbaf9a7..d1ec67b8 100644
--- a/runtime/klee-libc/strcpy.c
+++ b/runtime/klee-libc/strcpy.c
@@ -1,11 +1,11 @@
-//===-- strcpy.c ----------------------------------------------------------===//
+/*===-- strcpy.c ----------------------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
-//===----------------------------------------------------------------------===//
+//===----------------------------------------------------------------------===*/
 
 char *strcpy(char *to, const char *from) {
   char *start = to;
diff --git a/runtime/klee-libc/strlen.c b/runtime/klee-libc/strlen.c
index e298410c..33846134 100644
--- a/runtime/klee-libc/strlen.c
+++ b/runtime/klee-libc/strlen.c
@@ -1,11 +1,11 @@
-//===-- strlen.c ----------------------------------------------------------===//
+/*===-- strlen.c ----------------------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
-//===----------------------------------------------------------------------===//
+//===----------------------------------------------------------------------===*/
 
 #include <string.h>
 
diff --git a/runtime/klee-libc/strrchr.c b/runtime/klee-libc/strrchr.c
index 01128b48..4d51769b 100644
--- a/runtime/klee-libc/strrchr.c
+++ b/runtime/klee-libc/strrchr.c
@@ -1,11 +1,11 @@
-//===-- strrchr.c ---------------------------------------------------------===//
+/*===-- strrchr.c ---------------------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
-//===----------------------------------------------------------------------===//
+//===----------------------------------------------------------------------===*/
 
 #include <string.h>
 
diff --git a/runtime/klee-libc/tolower.c b/runtime/klee-libc/tolower.c
index 265f5deb..a311f2010 100644
--- a/runtime/klee-libc/tolower.c
+++ b/runtime/klee-libc/tolower.c
@@ -1,11 +1,11 @@
-//===-- tolower.c ---------------------------------------------------------===//
+/*===-- tolower.c ---------------------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
-//===----------------------------------------------------------------------===//
+//===----------------------------------------------------------------------===*/
 
 int tolower(int ch) {
   if ( (unsigned int)(ch - 'A') < 26u )
diff --git a/runtime/klee-libc/toupper.c b/runtime/klee-libc/toupper.c
index 37e5f9d6..5030b5cc 100644
--- a/runtime/klee-libc/toupper.c
+++ b/runtime/klee-libc/toupper.c
@@ -1,11 +1,11 @@
-//===-- toupper.c ---------------------------------------------------------===//
+/*===-- toupper.c ---------------------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
-//===----------------------------------------------------------------------===//
+//===----------------------------------------------------------------------===*/
 
 int toupper(int ch) {
   if ( (unsigned int)(ch - 'a') < 26u )
diff --git a/test/Feature/arithmetic-right-overshift-sym-conc.c b/test/Feature/arithmetic-right-overshift-sym-conc.c
index a771bc75..7af6f9d7 100644
--- a/test/Feature/arithmetic-right-overshift-sym-conc.c
+++ b/test/Feature/arithmetic-right-overshift-sym-conc.c
@@ -15,11 +15,13 @@ typedef enum
 
 // We're using signed ints so should be doing
 // arithmetic right shift.
-int overshift(volatile unsigned int y, const char * type)
+// lhs should be a constant
+int overshift(signed int lhs, volatile unsigned int y, const char * type)
 {
     overshift_t ret;
-    volatile signed int x=15;
+    volatile signed int x = lhs;
     unsigned int limit = sizeof(x)*8;
+    assert(!klee_is_symbolic(x));
 
     volatile signed int result;
     result = x >> y; // Potential overshift
@@ -45,10 +47,13 @@ int overshift(volatile unsigned int y, const char * type)
 
 int main(int argc, char** argv)
 {
-    // Concrete overshift
     volatile unsigned int y = sizeof(unsigned int)*8;
-    overshift_t conc = overshift(y, "Concrete");
-    assert( conc == TO_ZERO);
+    // Try with +ve lhs
+    overshift_t conc = overshift(15, y, "Concrete");
+    assert(conc == TO_ZERO);
+    // Try with -ve lhs
+    conc = overshift(-1, y, "Concrete");
+    assert(conc == TO_ZERO);
 
     // Symbolic overshift
     volatile unsigned int y2;
@@ -56,11 +61,15 @@ int main(int argc, char** argv)
     // Add constraints so only one value possible
     klee_assume(y2 > (y-1));
     klee_assume(y2 < (y+1));
-    overshift_t sym = overshift(y2, "Symbolic");
-    assert( sym == TO_ZERO);
+    // Try with +ve lhs
+    overshift_t sym = overshift(15, y2, "Symbolic");
+    assert(sym == TO_ZERO);
+    // Try with -ve lhs
+    sym = overshift(-1, y2, "Symbolic");
+    assert(sym == TO_ZERO);
 
     // Concrete and symbolic behaviour should be the same
-    assert( conc == sym);
+    assert(conc == sym);
 
     return 0;
 }
diff --git a/test/Programs/pcregrep.c b/test/Programs/pcregrep.c
index fb99ef87..5ed8f4fa 100644
--- a/test/Programs/pcregrep.c
+++ b/test/Programs/pcregrep.c
@@ -211,7 +211,7 @@ struct l_struct_2E_pcre {
 /* Function Declarations */
 double fmod(double, double);
 float fmodf(float, float);
-unsigned int main(unsigned int llvm_cbe_argc, unsigned char **llvm_cbe_argv);
+int main(int llvm_cbe_argc, char **llvm_cbe_argv);
 unsigned int fprintf(struct l_struct_2E__IO_FILE *, unsigned char *, ...);
 unsigned int __strtol_internal(unsigned char *, unsigned char **, unsigned int , unsigned int );
 unsigned int printf(unsigned char *, ...);
@@ -319,7 +319,7 @@ static inline int llvm_fcmp_ogt(double X, double Y) { return X >  Y ; }
 static inline int llvm_fcmp_ole(double X, double Y) { return X <= Y ; }
 static inline int llvm_fcmp_oge(double X, double Y) { return X >= Y ; }
 
-unsigned int main(unsigned int llvm_cbe_argc, unsigned char **llvm_cbe_argv) {
+int main(int llvm_cbe_argc, char **llvm_cbe_argv) {
   unsigned int llvm_cbe_length_i_i;    /* Address-exposed local */
   unsigned int llvm_cbe_firstbyte_i_i;    /* Address-exposed local */
   unsigned int llvm_cbe_reqbyte_i_i;    /* Address-exposed local */
diff --git a/test/Runtime/Uclibc/2007-10-08-optimization-calls-wrong-libc-functions.c b/test/Runtime/Uclibc/2007-10-08-optimization-calls-wrong-libc-functions.c
index 71f6d07a..d82f0eb9 100644
--- a/test/Runtime/Uclibc/2007-10-08-optimization-calls-wrong-libc-functions.c
+++ b/test/Runtime/Uclibc/2007-10-08-optimization-calls-wrong-libc-functions.c
@@ -5,10 +5,12 @@
 #include <string.h>
 #include <assert.h>
 
+#include "klee/klee.h"
+
 int main() {
   int a;
 
-  klee_make_symbolic(&a, sizeof a);
+  klee_make_symbolic(&a, sizeof a, "a");
 
   memset(&a, 0, sizeof a);
 
diff --git a/test/Solver/AShr_to_smtlib.kquery b/test/Solver/AShr_to_smtlib.kquery
new file mode 100644
index 00000000..774c46d9
--- /dev/null
+++ b/test/Solver/AShr_to_smtlib.kquery
@@ -0,0 +1,16 @@
+# RUN: %kleaver -print-smtlib -smtlib-abbreviation-mode=none %s > %t
+# RUN: diff -u %t %s.good.smt2
+
+# This test tries to check that the SMT-LIBv2 we generate when a AShrExpr is
+# used is correct.
+#
+# FIXME: We should really pass the generated query to an SMT solver that supports
+# SMT-LIBv2 and check it gives the correct answer ``unsat``. An older version of
+# KLEE where AShrExpr wasn't handled correctly would give ``sat`` for this query.
+#
+# We could fix this if we required STP to be in the user's PATH and made available
+# as a substitution in llvm-lit
+
+array value[1] : w32 -> w8 = symbolic
+array shift[1] : w32 -> w8 = symbolic
+(query [(Ule 8 (Read w8 0 shift))] (Eq 0 (AShr w8 (Read w8 0 value) (Read w8 0 shift))) )
diff --git a/test/Solver/AShr_to_smtlib.kquery.good.smt2 b/test/Solver/AShr_to_smtlib.kquery.good.smt2
new file mode 100644
index 00000000..e9478da6
--- /dev/null
+++ b/test/Solver/AShr_to_smtlib.kquery.good.smt2
@@ -0,0 +1,7 @@
+;SMTLIBv2 Query 0
+(set-logic QF_AUFBV )
+(declare-fun shift () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun value () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(assert (and  (=  false (=  (_ bv0 8) (ite (bvuge (select  shift (_ bv0 32) ) (_ bv8 8) ) (_ bv0 8) (bvashr (select  value (_ bv0 32) ) (select  shift (_ bv0 32) ) ) ) ) ) (bvule  (_ bv8 8) (select  shift (_ bv0 32) ) ) ) )
+(check-sat)
+(exit)
diff --git a/tools/kleaver/Makefile b/tools/kleaver/Makefile
index f66d0598..10b19a20 100644
--- a/tools/kleaver/Makefile
+++ b/tools/kleaver/Makefile
@@ -19,7 +19,7 @@ LINK_COMPONENTS = support
 
 include $(LEVEL)/Makefile.common
 
-LIBS += -lstp
+LIBS += $(STP_LDFLAGS)
 
 ifeq ($(ENABLE_METASMT),1)
   include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile
diff --git a/tools/klee/Makefile b/tools/klee/Makefile
index b9506b47..eb80d845 100644
--- a/tools/klee/Makefile
+++ b/tools/klee/Makefile
@@ -20,7 +20,7 @@ LINK_COMPONENTS += irreader
 endif
 include $(LEVEL)/Makefile.common
 
-LIBS += -lstp
+LIBS += $(STP_LDFLAGS)
 
 ifeq ($(ENABLE_METASMT),1)
   include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 8a246685..dc9cacc1 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -636,9 +636,9 @@ static std::string strip(std::string &in) {
 static void parseArguments(int argc, char **argv) {
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 2)
   // This version always reads response files
-  cl::ParseCommandLineOptions(argc, (const char**) argv, " klee\n");
+  cl::ParseCommandLineOptions(argc, argv, " klee\n");
 #else
-  cl::ParseCommandLineOptions(argc, (char**) argv, " klee\n", /*ReadResponseFiles=*/ true);
+  cl::ParseCommandLineOptions(argc, argv, " klee\n", /*ReadResponseFiles=*/ true);
 #endif
 }
 
@@ -1092,6 +1092,8 @@ static llvm::Module *linkWithUclibc(llvm::Module *mainModule, StringRef libDir)
   replaceOrRenameFunction(mainModule, "__libc_open", "open");
   replaceOrRenameFunction(mainModule, "__libc_fcntl", "fcntl");
 
+  // Take care of fortified functions
+  replaceOrRenameFunction(mainModule, "__fprintf_chk", "fprintf");
 
   // XXX we need to rearchitect so this can also be used with
   // programs externally linked with uclibc.
diff --git a/unittests/Expr/Makefile b/unittests/Expr/Makefile
index a9bfeda1..e52aea31 100644
--- a/unittests/Expr/Makefile
+++ b/unittests/Expr/Makefile
@@ -10,4 +10,4 @@ LINK_COMPONENTS := support
 include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest
 
 CXXFLAGS += -DLLVM_29_UNITTEST
-LIBS += -lstp
+LIBS += $(STP_LDFLAGS)
diff --git a/unittests/Ref/Makefile b/unittests/Ref/Makefile
index 94bbb83c..14dcc8bd 100644
--- a/unittests/Ref/Makefile
+++ b/unittests/Ref/Makefile
@@ -9,4 +9,4 @@ LINK_COMPONENTS := support
 
 include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest
 
-LIBS += -lstp
+LIBS += $(STP_LDFLAGS)
diff --git a/unittests/Solver/Makefile b/unittests/Solver/Makefile
index 00713691..aeac34ac 100644
--- a/unittests/Solver/Makefile
+++ b/unittests/Solver/Makefile
@@ -9,4 +9,4 @@ LINK_COMPONENTS := support
 
 include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest
 
-LIBS += -lstp
+LIBS += $(STP_LDFLAGS)
diff --git a/utils/hacks/TreeGraphs/Graphics/Canvas/__init__.py b/utils/hacks/TreeGraphs/Graphics/Canvas/__init__.py
index be03cc2f..048540ab 100644
--- a/utils/hacks/TreeGraphs/Graphics/Canvas/__init__.py
+++ b/utils/hacks/TreeGraphs/Graphics/Canvas/__init__.py
@@ -1,205 +1,205 @@
-from __future__ import division

-

-###

-

-import math, os, random

-

-from Graphics.Geometry import vec2

-

-from reportlab.pdfgen import canvas

-#from reportlab.graphics import shapes

-from reportlab.pdfbase import pdfmetrics

-

-"""

-class Canvas:

-	def startDrawing(self, (w,h)):

-	def endDrawing(self):

-		

-	def getAspect(self):

-		

-	def setColor(self, r, g, b):

-	def setLineWidth(self, width):

-	def drawOutlineBox(self, x0, y0, x1, y1):

-	def drawFilledBox(self, x0, y0, x1, y1):

-	def drawFilledPolygon(self, pts):

-	def drawOutlineCircle(self, x, y, r):

-	def startDrawPoints(self):

-	def endDrawPoints(self):

-	def drawPoint(self, x, y):

-	def setPointSize(self, size):

-

-	def drawLine(self, a, b):

-	def drawLines(self, ptPairs):

-	def drawLineStrip(self, pts):

-

-	def pushTransform(self):

-	def popTransform(self):

-	def translate(self, x, y):

-	def scale(self, x, y):

-	def setFontSize(self, size):

-	def drawString(self, (x, y), text):

-"""

-

-class BaseCanvas:

-	def drawPoints(self, pts):

-		self.startDrawPoints()

-		for pt in pts:

-			self.drawPoint(pt)

-		self.endDrawPoints()

-		

-	def drawStringCentered(self, boxLL, boxUR, text):

-		ll,ur = self.getStringBBox(text)

-		stringSize = vec2.sub(ur,ll)

-		boxSize = vec2.sub(boxUR,boxLL)

-		deltaSize = vec2.sub(boxSize, stringSize)

-		halfDeltaSize = vec2.mulN(deltaSize, .5)

-		

-		self.drawString(vec2.add(boxLL,halfDeltaSize), text)

-

-	def getStringSize(self, string):

-		ll,ur = self.getStringBBox(string)

-		return vec2.sub(ur,ll)

-	

-class PdfCanvas(BaseCanvas):

-	def __init__(self, name, basePos=(300,400), baseScale=(250,250), pageSize=None):

-		self._font = 'Times-Roman'

-		self.c = canvas.Canvas(name, pagesize=pageSize)

-		self.pointSize = 1

-		self.scaleX = self.scaleY = 1

-		self.state = []

-		self.basePos = tuple(basePos)

-		self.baseScale = tuple(baseScale)

-		self.lastFontSizeSet = None

-		

-		self.kLineScaleFactor = 1.95

-		

-	def getAspect(self):

-		return 1.0,1.0

-		

-	def startDrawing(self):

-		self.pointSize = 1

-		self.scaleX = self.scaleY = 1

-		

-		self.translate((self.basePos[0] + self.baseScale[0], self.basePos[1] + self.baseScale[1]))

-		self.scale(self.baseScale)

-

-		self.setColor(0,0,0)

-		self.setLineWidth(1)

-		self.setPointSize(1)

-

-	def finishPage(self):

-		self.c.showPage()

-

-		self.pointSize = 1

-		self.scaleX = self.scaleY = 1

-		

-		self.translate((self.basePos[0] + self.baseScale[0], self.basePos[1] + self.baseScale[1]))

-		self.scale(self.baseScale)

-

-		self.setColor(0,0,0)

-		self.setLineWidth(1)

-		self.setPointSize(1)

-		

-		if self.lastFontSizeSet is not None:

-			self.setFontSize(self.lastFontSizeSet)

-			

-	def endDrawing(self):

-		self.c.showPage()

-		self.c.save()

-		

-	def setColor(self, r, g, b):

-		self.c.setStrokeColorRGB(r,g,b)

-		self.c.setFillColorRGB(r,g,b)

-	def setLineWidth(self, width):

-		avgScale = (self.scaleX+self.scaleY)/2

-		self.c.setLineWidth(width/(self.kLineScaleFactor*avgScale))

-	def setPointSize(self, size):

-		avgScale = (self.scaleX+self.scaleY)/2

-		self.pointSize = size/(4*avgScale)

-

-	def drawOutlineBox(self, (x0, y0), (x1, y1)):

-		self.c.rect(x0, y0, x1-x0, y1-y0, stroke=1, fill=0)

-	def drawFilledBox(self, (x0, y0), (x1, y1)):

-		self.c.rect(x0, y0, x1-x0, y1-y0, stroke=0, fill=1)

-	def drawOutlineCircle(self, (x, y), r):

-		self.c.circle(x, y, r, stroke=1, fill=0)

-	def drawFilledCircle(self, (x, y), r):

-		self.c.circle(x, y, r, stroke=0, fill=1)

-	def drawFilledPolygon(self, pts):

-		p = self.c.beginPath()

-		p.moveTo(*pts[-1])

-		for x,y in pts:

-			p.lineTo(x,y)

-		self.c.drawPath(p, fill=1, stroke=0)

-	def drawOutlinePolygon(self, pts):

-		p = self.c.beginPath()

-		p.moveTo(* pts[0])

-		for x,y in pts[1:]:

-			p.lineTo(x,y)

-		p.close()

-		self.c.drawPath(p, fill=0, stroke=1)

-	def startDrawPoints(self):

-		pass

-	def endDrawPoints(self):

-		pass

-	def drawPoint(self, (x, y)):

-		self.c.circle(x, y, self.pointSize, stroke=0, fill=1)

-

-	def drawLine(self, a, b):

-		self.drawLines([(a,b)])

-	def drawLines(self, ptPairs):

-		p = self.c.beginPath()

-		for a,b in ptPairs:

-			p.moveTo(a[0],a[1])

-			p.lineTo(b[0],b[1])

-		self.c.drawPath(p)

-	def drawLineStrip(self, pts):

-		p = self.c.beginPath()

-		p.moveTo(pts[0][0],pts[0][1])

-		for pt in pts[1:]:

-			p.lineTo(pt[0],pt[1])

-		self.c.drawPath(p)

-	def drawBezier(self, (p0,p1,p2,p3)):

-		self.c.bezier(*(p0+p1+p2+p3))

-		

-	def pushTransform(self):

-		self.state.append( (self.scaleX,self.scaleY) )

-		self.c.saveState()

-	def popTransform(self):

-		self.c.restoreState()

-		self.scaleX,self.scaleY = self.state.pop()

-	def translate(self, (x, y)):

-		self.c.translate(x, y)

-	def rotate(self, angle):

-		self.c.rotate(angle*180/math.pi)

-	def scale(self, (x, y)):

-		self.scaleX *= x

-		self.scaleY *= y

-		self.c.scale(x, y)

-

-	def setFont(self, fontName):

-		self._font = {"Symbol":"Symbol",

-					 "Times":"Times-Roman"}.get(fontName,fontName)

-	def setFontSize(self, size):

-		self.lastFontSizeSet = size

-		avgScale = (self.scaleX+self.scaleY)/2

-		self.fontSize = size/(2*avgScale)

-		self.c.setFont(self._font, self.fontSize)

-#		self.c.setFont("Times-Roman", size/(2*avgScale))

-	def drawString(self, (x, y), text):

-		self.c.drawString(x, y, text)

-		

-	def drawOutlineString(self, (x,y), text):

-		t = self.c.beginText(x, y)

-		t.setTextRenderMode(1)

-		t.textLine(text)

-		t.setTextRenderMode(0)

-		self.c.drawText(t)

-

-	def getStringBBox(self, text):

-		font = pdfmetrics.getFont(self._font)

-		width = pdfmetrics.stringWidth(text, self._font, self.fontSize)

-		ll = (0,0)

-		ur = (width, (1.0 - font.face.ascent/2048.)*self.fontSize)

-		ur = (width, (1.0 - font.face.ascent/2048.)*self.fontSize)

-		return ll,ur

+from __future__ import division
+
+###
+
+import math, os, random
+
+from Graphics.Geometry import vec2
+
+from reportlab.pdfgen import canvas
+#from reportlab.graphics import shapes
+from reportlab.pdfbase import pdfmetrics
+
+"""
+class Canvas:
+	def startDrawing(self, (w,h)):
+	def endDrawing(self):
+		
+	def getAspect(self):
+		
+	def setColor(self, r, g, b):
+	def setLineWidth(self, width):
+	def drawOutlineBox(self, x0, y0, x1, y1):
+	def drawFilledBox(self, x0, y0, x1, y1):
+	def drawFilledPolygon(self, pts):
+	def drawOutlineCircle(self, x, y, r):
+	def startDrawPoints(self):
+	def endDrawPoints(self):
+	def drawPoint(self, x, y):
+	def setPointSize(self, size):
+
+	def drawLine(self, a, b):
+	def drawLines(self, ptPairs):
+	def drawLineStrip(self, pts):
+
+	def pushTransform(self):
+	def popTransform(self):
+	def translate(self, x, y):
+	def scale(self, x, y):
+	def setFontSize(self, size):
+	def drawString(self, (x, y), text):
+"""
+
+class BaseCanvas:
+	def drawPoints(self, pts):
+		self.startDrawPoints()
+		for pt in pts:
+			self.drawPoint(pt)
+		self.endDrawPoints()
+		
+	def drawStringCentered(self, boxLL, boxUR, text):
+		ll,ur = self.getStringBBox(text)
+		stringSize = vec2.sub(ur,ll)
+		boxSize = vec2.sub(boxUR,boxLL)
+		deltaSize = vec2.sub(boxSize, stringSize)
+		halfDeltaSize = vec2.mulN(deltaSize, .5)
+		
+		self.drawString(vec2.add(boxLL,halfDeltaSize), text)
+
+	def getStringSize(self, string):
+		ll,ur = self.getStringBBox(string)
+		return vec2.sub(ur,ll)
+	
+class PdfCanvas(BaseCanvas):
+	def __init__(self, name, basePos=(300,400), baseScale=(250,250), pageSize=None):
+		self._font = 'Times-Roman'
+		self.c = canvas.Canvas(name, pagesize=pageSize)
+		self.pointSize = 1
+		self.scaleX = self.scaleY = 1
+		self.state = []
+		self.basePos = tuple(basePos)
+		self.baseScale = tuple(baseScale)
+		self.lastFontSizeSet = None
+		
+		self.kLineScaleFactor = 1.95
+		
+	def getAspect(self):
+		return 1.0,1.0
+		
+	def startDrawing(self):
+		self.pointSize = 1
+		self.scaleX = self.scaleY = 1
+		
+		self.translate((self.basePos[0] + self.baseScale[0], self.basePos[1] + self.baseScale[1]))
+		self.scale(self.baseScale)
+
+		self.setColor(0,0,0)
+		self.setLineWidth(1)
+		self.setPointSize(1)
+
+	def finishPage(self):
+		self.c.showPage()
+
+		self.pointSize = 1
+		self.scaleX = self.scaleY = 1
+		
+		self.translate((self.basePos[0] + self.baseScale[0], self.basePos[1] + self.baseScale[1]))
+		self.scale(self.baseScale)
+
+		self.setColor(0,0,0)
+		self.setLineWidth(1)
+		self.setPointSize(1)
+		
+		if self.lastFontSizeSet is not None:
+			self.setFontSize(self.lastFontSizeSet)
+			
+	def endDrawing(self):
+		self.c.showPage()
+		self.c.save()
+		
+	def setColor(self, r, g, b):
+		self.c.setStrokeColorRGB(r,g,b)
+		self.c.setFillColorRGB(r,g,b)
+	def setLineWidth(self, width):
+		avgScale = (self.scaleX+self.scaleY)/2
+		self.c.setLineWidth(width/(self.kLineScaleFactor*avgScale))
+	def setPointSize(self, size):
+		avgScale = (self.scaleX+self.scaleY)/2
+		self.pointSize = size/(4*avgScale)
+
+	def drawOutlineBox(self, (x0, y0), (x1, y1)):
+		self.c.rect(x0, y0, x1-x0, y1-y0, stroke=1, fill=0)
+	def drawFilledBox(self, (x0, y0), (x1, y1)):
+		self.c.rect(x0, y0, x1-x0, y1-y0, stroke=0, fill=1)
+	def drawOutlineCircle(self, (x, y), r):
+		self.c.circle(x, y, r, stroke=1, fill=0)
+	def drawFilledCircle(self, (x, y), r):
+		self.c.circle(x, y, r, stroke=0, fill=1)
+	def drawFilledPolygon(self, pts):
+		p = self.c.beginPath()
+		p.moveTo(*pts[-1])
+		for x,y in pts:
+			p.lineTo(x,y)
+		self.c.drawPath(p, fill=1, stroke=0)
+	def drawOutlinePolygon(self, pts):
+		p = self.c.beginPath()
+		p.moveTo(* pts[0])
+		for x,y in pts[1:]:
+			p.lineTo(x,y)
+		p.close()
+		self.c.drawPath(p, fill=0, stroke=1)
+	def startDrawPoints(self):
+		pass
+	def endDrawPoints(self):
+		pass
+	def drawPoint(self, (x, y)):
+		self.c.circle(x, y, self.pointSize, stroke=0, fill=1)
+
+	def drawLine(self, a, b):
+		self.drawLines([(a,b)])
+	def drawLines(self, ptPairs):
+		p = self.c.beginPath()
+		for a,b in ptPairs:
+			p.moveTo(a[0],a[1])
+			p.lineTo(b[0],b[1])
+		self.c.drawPath(p)
+	def drawLineStrip(self, pts):
+		p = self.c.beginPath()
+		p.moveTo(pts[0][0],pts[0][1])
+		for pt in pts[1:]:
+			p.lineTo(pt[0],pt[1])
+		self.c.drawPath(p)
+	def drawBezier(self, (p0,p1,p2,p3)):
+		self.c.bezier(*(p0+p1+p2+p3))
+		
+	def pushTransform(self):
+		self.state.append( (self.scaleX,self.scaleY) )
+		self.c.saveState()
+	def popTransform(self):
+		self.c.restoreState()
+		self.scaleX,self.scaleY = self.state.pop()
+	def translate(self, (x, y)):
+		self.c.translate(x, y)
+	def rotate(self, angle):
+		self.c.rotate(angle*180/math.pi)
+	def scale(self, (x, y)):
+		self.scaleX *= x
+		self.scaleY *= y
+		self.c.scale(x, y)
+
+	def setFont(self, fontName):
+		self._font = {"Symbol":"Symbol",
+					 "Times":"Times-Roman"}.get(fontName,fontName)
+	def setFontSize(self, size):
+		self.lastFontSizeSet = size
+		avgScale = (self.scaleX+self.scaleY)/2
+		self.fontSize = size/(2*avgScale)
+		self.c.setFont(self._font, self.fontSize)
+#		self.c.setFont("Times-Roman", size/(2*avgScale))
+	def drawString(self, (x, y), text):
+		self.c.drawString(x, y, text)
+		
+	def drawOutlineString(self, (x,y), text):
+		t = self.c.beginText(x, y)
+		t.setTextRenderMode(1)
+		t.textLine(text)
+		t.setTextRenderMode(0)
+		self.c.drawText(t)
+
+	def getStringBBox(self, text):
+		font = pdfmetrics.getFont(self._font)
+		width = pdfmetrics.stringWidth(text, self._font, self.fontSize)
+		ll = (0,0)
+		ur = (width, (1.0 - font.face.ascent/2048.)*self.fontSize)
+		ur = (width, (1.0 - font.face.ascent/2048.)*self.fontSize)
+		return ll,ur
diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/Intersect2D.py b/utils/hacks/TreeGraphs/Graphics/Geometry/Intersect2D.py
index a600a64f..d310c20a 100644
--- a/utils/hacks/TreeGraphs/Graphics/Geometry/Intersect2D.py
+++ b/utils/hacks/TreeGraphs/Graphics/Geometry/Intersect2D.py
@@ -1,59 +1,59 @@
-import vec2, math

-

-def intersectLineCircle((p, no), (C, r)):

-	x = vec2.sub(p,C)

-	b = 2.*vec2.dot(no, x)

-	c = vec2.sqr(x) - r*r

-	dist = b*b - 4*c

-	

-	if dist<0:

-		return None

-	else:

-		d = math.sqrt(dist)

-		t0 = (-b - d)*.5

-		t1 = (-b + d)*.5

-		return (t0,t1)

-	

-#def intersectLineCircle((lineP,lineN),(circleP,circleR)):

-#	dx,dy = vec2.sub(lineP,circleP)

-#	nx,ny = lineN

-#

-#	a =   (nx*nx + ny*ny)

-#	b = 2*(dx*nx + dy*ny)

-#	c =   (dx*dx + dy*dy) - circleR*circleR

-#	

-#	k = b*b - 4*a*c

-#	if k<0:

-#		return None

-#	else:

-#		d = math.sqrt(k)

-#		t1 = (-b - d)/2*a

-#		t0 = (-b + d)/2*a

-#		return t0,t1

-	

-def intersectCircleCircle(c0P, c0R, c1P, c1R):

-	v = vec2.sub(c1P, c0P)

-	d = vec2.length(v)

-	

-	R = c0R

-	r = c1R

-

-	try:	

-		x = (d*d - r*r + R*R)/(2*d)

-	except ZeroDivisionError:

-		if R<r:

-			return 'inside',()

-		elif r>R:

-			return 'outside',()

-		else:

-			return 'coincident',()

-	

-	k = R*R - x*x

-	if k<0:

-		if x<0:

-			return 'inside',()

-		else:

-			return 'outside',()

-	else:

-		y = math.sqrt(k)

-		return 'intersect',(vec2.toangle(v),vec2.toangle((x,y)))

+import vec2, math
+
+def intersectLineCircle((p, no), (C, r)):
+	x = vec2.sub(p,C)
+	b = 2.*vec2.dot(no, x)
+	c = vec2.sqr(x) - r*r
+	dist = b*b - 4*c
+	
+	if dist<0:
+		return None
+	else:
+		d = math.sqrt(dist)
+		t0 = (-b - d)*.5
+		t1 = (-b + d)*.5
+		return (t0,t1)
+	
+#def intersectLineCircle((lineP,lineN),(circleP,circleR)):
+#	dx,dy = vec2.sub(lineP,circleP)
+#	nx,ny = lineN
+#
+#	a =   (nx*nx + ny*ny)
+#	b = 2*(dx*nx + dy*ny)
+#	c =   (dx*dx + dy*dy) - circleR*circleR
+#	
+#	k = b*b - 4*a*c
+#	if k<0:
+#		return None
+#	else:
+#		d = math.sqrt(k)
+#		t1 = (-b - d)/2*a
+#		t0 = (-b + d)/2*a
+#		return t0,t1
+	
+def intersectCircleCircle(c0P, c0R, c1P, c1R):
+	v = vec2.sub(c1P, c0P)
+	d = vec2.length(v)
+	
+	R = c0R
+	r = c1R
+
+	try:	
+		x = (d*d - r*r + R*R)/(2*d)
+	except ZeroDivisionError:
+		if R<r:
+			return 'inside',()
+		elif r>R:
+			return 'outside',()
+		else:
+			return 'coincident',()
+	
+	k = R*R - x*x
+	if k<0:
+		if x<0:
+			return 'inside',()
+		else:
+			return 'outside',()
+	else:
+		y = math.sqrt(k)
+		return 'intersect',(vec2.toangle(v),vec2.toangle((x,y)))
diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/mat2.py b/utils/hacks/TreeGraphs/Graphics/Geometry/mat2.py
index 05320d5e..5a09be62 100644
--- a/utils/hacks/TreeGraphs/Graphics/Geometry/mat2.py
+++ b/utils/hacks/TreeGraphs/Graphics/Geometry/mat2.py
@@ -1,20 +1,20 @@
-import vec2

-

-def det(m):

-	((m00,m01),(m10,m11))= m

-	

-	return m00*m11 - m01*m10

-

-def mul(a,b):

-	b_trans= zip(* b)

-	return tuple([transmulvec2(b_trans, a_r) for a_r in a])

-

-	# multiple vector v by a transposed matrix

-def transmulvec2(m_trans,v):

-	return tuple([vec2.dot(v, m_c) for m_c in m_trans])

-

-def mulvec2(m,v):

-	return transmulvec2(zip(* m), v)

-

-def mulN(m,N):

-	return tuple([vec2.mulN(v,N) for v in m])

+import vec2
+
+def det(m):
+	((m00,m01),(m10,m11))= m
+	
+	return m00*m11 - m01*m10
+
+def mul(a,b):
+	b_trans= zip(* b)
+	return tuple([transmulvec2(b_trans, a_r) for a_r in a])
+
+	# multiple vector v by a transposed matrix
+def transmulvec2(m_trans,v):
+	return tuple([vec2.dot(v, m_c) for m_c in m_trans])
+
+def mulvec2(m,v):
+	return transmulvec2(zip(* m), v)
+
+def mulN(m,N):
+	return tuple([vec2.mulN(v,N) for v in m])
diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/mat3.py b/utils/hacks/TreeGraphs/Graphics/Geometry/mat3.py
index b8705a32..c25d7e50 100644
--- a/utils/hacks/TreeGraphs/Graphics/Geometry/mat3.py
+++ b/utils/hacks/TreeGraphs/Graphics/Geometry/mat3.py
@@ -1,40 +1,40 @@
-import vec3,mat2

-

-def identity():

-	return ((1.0, 0.0, 0.0),

-			(0.0, 1.0, 0.0),

-			(0.0, 0.0, 1.0))

-

-def fromscale(scale):

-	x,y,z= scale

-	x,y,z= float(x),float(y),float(z)

-	return ((  x, 0.0, 0.0),

-			(0.0,   y, 0.0),

-			(0.0, 0.0,   z))

-def fromscaleN(n):

-	return fromscale((n,n,n))

-

-def mul(a,b):

-	b_trans= zip(* b)

-	return tuple([transmulvec3(b_trans, a_r) for a_r in a])

-

-	# multiple vector v by a transposed matrix

-def transmulvec3(m_trans,v):

-	return tuple([vec3.dot(v, m_c) for m_c in m_trans])

-

-def mulvec3(m,v):

-	return transmulvec3(zip(* m), v)

-

-def mulN(m,N):

-	return tuple([vec3.mulN(v,N) for v in m])

-

-def det(m):

-	((m00,m01,m02),

-	 (m10,m11,m12),

-	 (m20,m21,m22))= m

-

-	a= m00 * mat2.det( ((m11, m12), (m21, m22)) );

-	b= m10 * mat2.det( ((m01, m02), (m21, m22)) );

-	c= m20 * mat2.det( ((m01, m02), (m11, m12)) );

-	

-	return a-b+c

+import vec3,mat2
+
+def identity():
+	return ((1.0, 0.0, 0.0),
+			(0.0, 1.0, 0.0),
+			(0.0, 0.0, 1.0))
+
+def fromscale(scale):
+	x,y,z= scale
+	x,y,z= float(x),float(y),float(z)
+	return ((  x, 0.0, 0.0),
+			(0.0,   y, 0.0),
+			(0.0, 0.0,   z))
+def fromscaleN(n):
+	return fromscale((n,n,n))
+
+def mul(a,b):
+	b_trans= zip(* b)
+	return tuple([transmulvec3(b_trans, a_r) for a_r in a])
+
+	# multiple vector v by a transposed matrix
+def transmulvec3(m_trans,v):
+	return tuple([vec3.dot(v, m_c) for m_c in m_trans])
+
+def mulvec3(m,v):
+	return transmulvec3(zip(* m), v)
+
+def mulN(m,N):
+	return tuple([vec3.mulN(v,N) for v in m])
+
+def det(m):
+	((m00,m01,m02),
+	 (m10,m11,m12),
+	 (m20,m21,m22))= m
+
+	a= m00 * mat2.det( ((m11, m12), (m21, m22)) );
+	b= m10 * mat2.det( ((m01, m02), (m21, m22)) );
+	c= m20 * mat2.det( ((m01, m02), (m11, m12)) );
+	
+	return a-b+c
diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/mat4.py b/utils/hacks/TreeGraphs/Graphics/Geometry/mat4.py
index 8dc7d35c..e927c936 100644
--- a/utils/hacks/TreeGraphs/Graphics/Geometry/mat4.py
+++ b/utils/hacks/TreeGraphs/Graphics/Geometry/mat4.py
@@ -1,153 +1,153 @@
-import vec4,mat3

-

-def identity():

-	return ((1.0, 0.0, 0.0, 0.0),

-			(0.0, 1.0, 0.0, 0.0),

-			(0.0, 0.0, 1.0, 0.0),

-			(0.0, 0.0, 0.0, 1.0))

-

-def fromtrans(trans):

-	return ((1.0, 0.0, 0.0, 0.0),

-			(0.0, 1.0, 0.0, 0.0),

-			(0.0, 0.0, 1.0, 0.0),

-			(trans[0], trans[1], trans[2], 1.0))

-

-def fromscale(scale):

-	x,y,z= scale

-	x,y,z= float(x),float(y),float(z)

-	return ((  x, 0.0, 0.0, 0.0),

-			(0.0,   y, 0.0, 0.0),

-			(0.0, 0.0,   z, 0.0),

-			(0.0, 0.0, 0.0, 1.0))

-def fromscaleN(n):

-	return fromscale((n,n,n))

-

-def fromortho(left,right,bottom,top,znear,zfar):

-	m0= ( 2.0/(right-left), 0.0, 0.0, 0.0)

-	m1= (0.0,  2.0/(top-bottom), 0.0, 0.0)

-	m2= (0.0, 0.0, -2.0/(zfar-znear), 0.0)

-	m3= (	-((right+left)/(right-left)),

-			-((top+bottom)/(top-bottom)),

-			-((zfar+znear)/(zfar-znear)),

-			1.0)

-	return (m0,m1,m2,m3)

-

-def mulN(m,N):

-	return tuple([vec4.mulN(v,N) for v in m])

-	

-def mul(a,b):

-	b_trans= zip(* b)

-	return tuple([transmulvec4(b_trans, a_r) for a_r in a])

-

-	# multiple vector v by a transposed matrix

-def transmulvec4(m_trans,v):

-	return tuple([vec4.dot(v, m_c) for m_c in m_trans])

-

-def mulvec4(m,v):

-	return transmulvec4(zip(* m), v)

-	

-def trans(m):

-	((m00,m01,m02,m03),	

-	 (m10,m11,m12,m13),	

-	 (m20,m21,m22,m23),	

-	 (m30,m31,m32,m33))= m

-	 

-	return (	(m00,m10,m20,m30),	

-				(m01,m11,m21,m31),	

-				(m02,m12,m22,m32),	

-				(m03,m13,m23,m33))

-

-def det(m):

-	((m00,m01,m02,m03),	

-	 (m10,m11,m12,m13),	

-	 (m20,m21,m22,m23),	

-	 (m30,m31,m32,m33))= m

-	 

-	a= m00 * mat3.det(	((m11, m12, m13), 

-						 (m21, m22, m23), 

-						 (m31, m32, m33)) );

-	b= m10 * mat3.det(	((m01, m02, m03), 

-						 (m21, m22, m23), 

-						 (m31, m32, m33)) );

-	c= m20 * mat3.det(  ((m01, m02, m03), 

-						 (m11, m12, m13), 

-						 (m31, m32, m33)) );

-	d= m30 * mat3.det(	((m01, m02, m03), 

-						 (m11, m12, m13), 

-						 (m21, m22, m23)) );

-	

-	return a-b+c-d;

-

-def adj(m):

-	((m00,m01,m02,m03),	

-	 (m10,m11,m12,m13),	

-	 (m20,m21,m22,m23),	

-	 (m30,m31,m32,m33))= m

-	 

-	t00=  mat3.det( ((m11, m12, m13), 

-					 (m21, m22, m23),

-					 (m31, m32, m33)) )

-	t01= -mat3.det( ((m10, m12, m13), 

-					 (m20, m22, m23),

-					 (m30, m32, m33)) )

-	t02=  mat3.det( ((m10, m11, m13), 

-					 (m20, m21, m23),

-					 (m30, m31, m33)) )

-	t03= -mat3.det( ((m10, m11, m12), 

-					 (m20, m21, m22),

-					 (m30, m31, m32)) )

-

-

-	t10= -mat3.det( ((m01, m02, m03), 

-					 (m21, m22, m23),

-					 (m31, m32, m33)) )

-	t11=  mat3.det( ((m00, m02, m03), 

-					 (m20, m22, m23),

-					 (m30, m32, m33)) )

-	t12= -mat3.det( ((m00, m01, m03), 

-					 (m20, m21, m23),

-					 (m30, m31, m33)) )

-	t13=  mat3.det( ((m00, m01, m02), 

-					 (m20, m21, m22),

-					 (m30, m31, m32)) )

-

-	t20=  mat3.det( ((m01, m02, m03), 

-					 (m11, m12, m13),

-					 (m31, m32, m33)) )

-	t21= -mat3.det( ((m00, m02, m03), 

-					 (m10, m12, m13),

-					 (m30, m32, m33)) )

-	t22=  mat3.det( ((m00, m01, m03), 

-					 (m10, m11, m13),

-					 (m30, m31, m33)) )

-	t23= -mat3.det( ((m00, m01, m02), 

-					 (m10, m11, m12),

-					 (m30, m31, m32)) )

-

-	t30= -mat3.det( ((m01, m02, m03), 

-					 (m11, m12, m13),

-					 (m21, m22, m23)) )

-	t31=  mat3.det( ((m00, m02, m03), 

-					 (m10, m12, m13),

-					 (m20, m22, m23)) )

-	t32= -mat3.det( ((m00, m01, m03), 

-					 (m10, m11, m13),

-					 (m20, m21, m23)) )

-	t33=  mat3.det( ((m00, m01, m02), 

-					 (m10, m11, m12),

-					 (m20, m21, m22)) )

-					

-	return ((t00,t01,t02,t03),

-			(t10,t11,t12,t13),

-			(t20,t21,t22,t23),

-			(t30,t31,t32,t33))

-	

-def inv(m):

-	d= det(m)

-	t= trans(adj(m))

-	v= 1.0/d

-	return tuple([(a*v,b*v,c*v,d*v) for a,b,c,d in t])

-	

-def toGL(m):

-	m0,m1,m2,m3= m

+import vec4,mat3
+
+def identity():
+	return ((1.0, 0.0, 0.0, 0.0),
+			(0.0, 1.0, 0.0, 0.0),
+			(0.0, 0.0, 1.0, 0.0),
+			(0.0, 0.0, 0.0, 1.0))
+
+def fromtrans(trans):
+	return ((1.0, 0.0, 0.0, 0.0),
+			(0.0, 1.0, 0.0, 0.0),
+			(0.0, 0.0, 1.0, 0.0),
+			(trans[0], trans[1], trans[2], 1.0))
+
+def fromscale(scale):
+	x,y,z= scale
+	x,y,z= float(x),float(y),float(z)
+	return ((  x, 0.0, 0.0, 0.0),
+			(0.0,   y, 0.0, 0.0),
+			(0.0, 0.0,   z, 0.0),
+			(0.0, 0.0, 0.0, 1.0))
+def fromscaleN(n):
+	return fromscale((n,n,n))
+
+def fromortho(left,right,bottom,top,znear,zfar):
+	m0= ( 2.0/(right-left), 0.0, 0.0, 0.0)
+	m1= (0.0,  2.0/(top-bottom), 0.0, 0.0)
+	m2= (0.0, 0.0, -2.0/(zfar-znear), 0.0)
+	m3= (	-((right+left)/(right-left)),
+			-((top+bottom)/(top-bottom)),
+			-((zfar+znear)/(zfar-znear)),
+			1.0)
+	return (m0,m1,m2,m3)
+
+def mulN(m,N):
+	return tuple([vec4.mulN(v,N) for v in m])
+	
+def mul(a,b):
+	b_trans= zip(* b)
+	return tuple([transmulvec4(b_trans, a_r) for a_r in a])
+
+	# multiple vector v by a transposed matrix
+def transmulvec4(m_trans,v):
+	return tuple([vec4.dot(v, m_c) for m_c in m_trans])
+
+def mulvec4(m,v):
+	return transmulvec4(zip(* m), v)
+	
+def trans(m):
+	((m00,m01,m02,m03),	
+	 (m10,m11,m12,m13),	
+	 (m20,m21,m22,m23),	
+	 (m30,m31,m32,m33))= m
+	 
+	return (	(m00,m10,m20,m30),	
+				(m01,m11,m21,m31),	
+				(m02,m12,m22,m32),	
+				(m03,m13,m23,m33))
+
+def det(m):
+	((m00,m01,m02,m03),	
+	 (m10,m11,m12,m13),	
+	 (m20,m21,m22,m23),	
+	 (m30,m31,m32,m33))= m
+	 
+	a= m00 * mat3.det(	((m11, m12, m13), 
+						 (m21, m22, m23), 
+						 (m31, m32, m33)) );
+	b= m10 * mat3.det(	((m01, m02, m03), 
+						 (m21, m22, m23), 
+						 (m31, m32, m33)) );
+	c= m20 * mat3.det(  ((m01, m02, m03), 
+						 (m11, m12, m13), 
+						 (m31, m32, m33)) );
+	d= m30 * mat3.det(	((m01, m02, m03), 
+						 (m11, m12, m13), 
+						 (m21, m22, m23)) );
+	
+	return a-b+c-d;
+
+def adj(m):
+	((m00,m01,m02,m03),	
+	 (m10,m11,m12,m13),	
+	 (m20,m21,m22,m23),	
+	 (m30,m31,m32,m33))= m
+	 
+	t00=  mat3.det( ((m11, m12, m13), 
+					 (m21, m22, m23),
+					 (m31, m32, m33)) )
+	t01= -mat3.det( ((m10, m12, m13), 
+					 (m20, m22, m23),
+					 (m30, m32, m33)) )
+	t02=  mat3.det( ((m10, m11, m13), 
+					 (m20, m21, m23),
+					 (m30, m31, m33)) )
+	t03= -mat3.det( ((m10, m11, m12), 
+					 (m20, m21, m22),
+					 (m30, m31, m32)) )
+
+
+	t10= -mat3.det( ((m01, m02, m03), 
+					 (m21, m22, m23),
+					 (m31, m32, m33)) )
+	t11=  mat3.det( ((m00, m02, m03), 
+					 (m20, m22, m23),
+					 (m30, m32, m33)) )
+	t12= -mat3.det( ((m00, m01, m03), 
+					 (m20, m21, m23),
+					 (m30, m31, m33)) )
+	t13=  mat3.det( ((m00, m01, m02), 
+					 (m20, m21, m22),
+					 (m30, m31, m32)) )
+
+	t20=  mat3.det( ((m01, m02, m03), 
+					 (m11, m12, m13),
+					 (m31, m32, m33)) )
+	t21= -mat3.det( ((m00, m02, m03), 
+					 (m10, m12, m13),
+					 (m30, m32, m33)) )
+	t22=  mat3.det( ((m00, m01, m03), 
+					 (m10, m11, m13),
+					 (m30, m31, m33)) )
+	t23= -mat3.det( ((m00, m01, m02), 
+					 (m10, m11, m12),
+					 (m30, m31, m32)) )
+
+	t30= -mat3.det( ((m01, m02, m03), 
+					 (m11, m12, m13),
+					 (m21, m22, m23)) )
+	t31=  mat3.det( ((m00, m02, m03), 
+					 (m10, m12, m13),
+					 (m20, m22, m23)) )
+	t32= -mat3.det( ((m00, m01, m03), 
+					 (m10, m11, m13),
+					 (m20, m21, m23)) )
+	t33=  mat3.det( ((m00, m01, m02), 
+					 (m10, m11, m12),
+					 (m20, m21, m22)) )
+					
+	return ((t00,t01,t02,t03),
+			(t10,t11,t12,t13),
+			(t20,t21,t22,t23),
+			(t30,t31,t32,t33))
+	
+def inv(m):
+	d= det(m)
+	t= trans(adj(m))
+	v= 1.0/d
+	return tuple([(a*v,b*v,c*v,d*v) for a,b,c,d in t])
+	
+def toGL(m):
+	m0,m1,m2,m3= m
 	return m0+m1+m2+m3
\ No newline at end of file
diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/quat.py b/utils/hacks/TreeGraphs/Graphics/Geometry/quat.py
index f7837891..663d3d8c 100644
--- a/utils/hacks/TreeGraphs/Graphics/Geometry/quat.py
+++ b/utils/hacks/TreeGraphs/Graphics/Geometry/quat.py
@@ -1,107 +1,107 @@
-from __future__ import division

-

-import math

-import vec3, vec4

-

-def identity():

-	return (0.0,0.0,0.0,1.0)

-

-def fromaxisangle(axisangle):

-	axis,angle= axisangle

-	ang_2= angle/2.0

-	s_ang= math.sin(ang_2)

-	c_ang= math.cos(ang_2)

-	

-	q= vec3.mulN(axis, s_ang) + (c_ang,)

-	return normalize(q)

-

-def fromnormals(n1,n2):

-	axis,angle= vec3.normalize(vec3.cross(n1, n2)), math.acos(vec3.dot(n1, n2))

-	return fromaxisangle((axis,angle))

-

-	# avoid trigonmetry

-def fromnormals_faster(n1,n2):

-	axis= vec3.normalize(vec3.cross(n1, n2))

-

-	half_n= vec3.normalize(vec3.add(n1, n2))

-	cos_half_angle= vec3.dot(n1, half_n)

-	sin_half_angle= 1.0 - cos_half_angle**2

-	

-	return vec3.mulN(axis, sin_half_angle) + (cos_half_angle,)

-

-def fromvectors(v1,v2):

-	return fromnormals(vec3.normalize(v1), vec3.normalize(v2))

-

-def magnitude(q):

-	return vec4.length(q)

-

-def normalize(q):

-	return vec4.divN(q, magnitude(q))

-

-def conjugate(q):

-	x,y,z,w= q

-	return (-x, -y, -z, w)

-

-def mulvec3(q, v):

-	t= mul(q, v+(0.0,))

-	t= mul(t, conjugate(q))

-	return t[:3]

-

-def mul(a, b):

-	ax,ay,az,aw= a

-	bx,by,bz,bw= b

-

-	x= aw*bx + ax*bw + ay*bz - az*by

-	y= aw*by + ay*bw + az*bx - ax*bz

-	z= aw*bz + az*bw + ax*by - ay*bx 

-	w= aw*bw - ax*bx - ay*by - az*bz

-

-	return (x,y,z,w)

-

-def toaxisangle(q):

-	tw= math.acos(q[3])

-	scale= math.sin(tw)

-	angle= tw*2.0

-

-	try:

-		axis= vec3.divN(q[:3], scale)

-	except ZeroDivisionError:

-		axis= (1.0,0.0,0.0)

-

-	return axis,angle

-

-def tomat3x3(q):

-	x,y,z,w= q

-

-	m0= (	1.0 -	2.0 * ( y*y + z*z ),

-					2.0 * ( x*y - z*w ),

-					2.0 * ( x*z + y*w ))

-	m1=	(			2.0 * ( x*y + z*w ),

-			1.0 -	2.0 * ( x*x + z*z ),

-					2.0 * ( y*z - x*w )) 

-	m2=	(			2.0 * ( x*z - y*w ),

-					2.0 * ( y*z + x*w ),

-			1.0 -	2.0 * ( x*x + y*y ))

-

-	return m0,m1,m2

-

-def tomat4x4(q):

-	m0,m1,m2= tomat3x3(q)

-	return (m0 + (0.0,),

-			m1 + (0.0,),

-			m2 + (0.0,),

-			(0.0, 0.0, 0.0, 1.0))

-

-def slerp(a, b, t):

-	raise NotImplementedError

-

-	cos_omega= vec4.dot(a, b)

-	

-	if (cos_omega<0.0):

-		cos_omega= -cos_omega

-		b= vec4.neg(b)

-

-	imega= math.acos(cos_omega)

-	t= sin(t*omega)/sin(omega)

-

-	return vec4.lerp(a, b, t)

+from __future__ import division
+
+import math
+import vec3, vec4
+
+def identity():
+	return (0.0,0.0,0.0,1.0)
+
+def fromaxisangle(axisangle):
+	axis,angle= axisangle
+	ang_2= angle/2.0
+	s_ang= math.sin(ang_2)
+	c_ang= math.cos(ang_2)
+	
+	q= vec3.mulN(axis, s_ang) + (c_ang,)
+	return normalize(q)
+
+def fromnormals(n1,n2):
+	axis,angle= vec3.normalize(vec3.cross(n1, n2)), math.acos(vec3.dot(n1, n2))
+	return fromaxisangle((axis,angle))
+
+	# avoid trigonmetry
+def fromnormals_faster(n1,n2):
+	axis= vec3.normalize(vec3.cross(n1, n2))
+
+	half_n= vec3.normalize(vec3.add(n1, n2))
+	cos_half_angle= vec3.dot(n1, half_n)
+	sin_half_angle= 1.0 - cos_half_angle**2
+	
+	return vec3.mulN(axis, sin_half_angle) + (cos_half_angle,)
+
+def fromvectors(v1,v2):
+	return fromnormals(vec3.normalize(v1), vec3.normalize(v2))
+
+def magnitude(q):
+	return vec4.length(q)
+
+def normalize(q):
+	return vec4.divN(q, magnitude(q))
+
+def conjugate(q):
+	x,y,z,w= q
+	return (-x, -y, -z, w)
+
+def mulvec3(q, v):
+	t= mul(q, v+(0.0,))
+	t= mul(t, conjugate(q))
+	return t[:3]
+
+def mul(a, b):
+	ax,ay,az,aw= a
+	bx,by,bz,bw= b
+
+	x= aw*bx + ax*bw + ay*bz - az*by
+	y= aw*by + ay*bw + az*bx - ax*bz
+	z= aw*bz + az*bw + ax*by - ay*bx 
+	w= aw*bw - ax*bx - ay*by - az*bz
+
+	return (x,y,z,w)
+
+def toaxisangle(q):
+	tw= math.acos(q[3])
+	scale= math.sin(tw)
+	angle= tw*2.0
+
+	try:
+		axis= vec3.divN(q[:3], scale)
+	except ZeroDivisionError:
+		axis= (1.0,0.0,0.0)
+
+	return axis,angle
+
+def tomat3x3(q):
+	x,y,z,w= q
+
+	m0= (	1.0 -	2.0 * ( y*y + z*z ),
+					2.0 * ( x*y - z*w ),
+					2.0 * ( x*z + y*w ))
+	m1=	(			2.0 * ( x*y + z*w ),
+			1.0 -	2.0 * ( x*x + z*z ),
+					2.0 * ( y*z - x*w )) 
+	m2=	(			2.0 * ( x*z - y*w ),
+					2.0 * ( y*z + x*w ),
+			1.0 -	2.0 * ( x*x + y*y ))
+
+	return m0,m1,m2
+
+def tomat4x4(q):
+	m0,m1,m2= tomat3x3(q)
+	return (m0 + (0.0,),
+			m1 + (0.0,),
+			m2 + (0.0,),
+			(0.0, 0.0, 0.0, 1.0))
+
+def slerp(a, b, t):
+	raise NotImplementedError
+
+	cos_omega= vec4.dot(a, b)
+	
+	if (cos_omega<0.0):
+		cos_omega= -cos_omega
+		b= vec4.neg(b)
+
+	imega= math.acos(cos_omega)
+	t= sin(t*omega)/sin(omega)
+
+	return vec4.lerp(a, b, t)
diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/vec2.py b/utils/hacks/TreeGraphs/Graphics/Geometry/vec2.py
index 80159043..73bc5717 100644
--- a/utils/hacks/TreeGraphs/Graphics/Geometry/vec2.py
+++ b/utils/hacks/TreeGraphs/Graphics/Geometry/vec2.py
@@ -1,79 +1,79 @@
-from __future__ import division

-from math import ceil,floor,sqrt,atan2,pi,cos,sin

-import random

-_abs,_min,_max= abs,min,max

-

-def random(rng=random):

-	return (rng.random()*2-1,rng.random()*2-1)

-

-def getangle(a):

-	x,y= a

-	if y>=0:

-		return atan2(y,x)

-	else:

-		return pi*2 + atan2(y,x)

-toangle = getangle

-

-def topolar(pt):

-	return getangle(pt),length(pt)

-def fromangle(angle,radius=1.):

-	return (cos(angle)*radius, sin(angle)*radius)

-frompolar = fromangle

-

-def rotate((x,y),angle):

-	c_a,s_a = cos(angle),sin(angle)

-	return (c_a*x - s_a*y, s_a*x + c_a*y)

-

-def rotate90((x,y)):

-	return (-y,x)

-	

-def abs(a): return (_abs(a[0]),_abs(a[1]))	

-def inv(a):	return (-a[0], -a[1])

-

-def add(a,b):	return (a[0]+b[0], a[1]+b[1])

-def sub(a,b):	return (a[0]-b[0], a[1]-b[1])

-def mul(a,b):	return (a[0]*b[0], a[1]*b[1])

-def div(a,b):	return (a[0]/b[0], a[1]/b[1])

-def mod(a,b):	return (a[0]%b[0], a[1]%b[1])

-def dot(a,b):	return (a[0]*b[0]+ a[1]*b[1])

-

-def addN(a,n):	return (a[0]+n, a[1]+n)

-def subN(a,n):	return (a[0]-n, a[1]-n)

-def mulN(a,n):	return (a[0]*n, a[1]*n)

-def modN(a,n):	return (a[0]%n, a[1]%n)

-def divN(a,n):	return (a[0]/n, a[1]/n)

-

-def sqr(a):			return dot(a,a)

-def length(a):		return sqrt(sqr(a))

-def avg(a,b):		return mulN(add(a,b),0.5)

-def distance(a,b):	return length(sub(a,b))

-

-def normalize(a):

-	return mulN(a, 1.0/length(a))

-

-def normalizeOrZero(a):

-	try:

-		return mulN(a, 1.0/length(a))

-	except ZeroDivisionError:

-		return (0.0,0.0)

-	

-def min((a0,a1),(b0,b1)):

-	return (_min(a0,b0),_min(a1,b1))

-def max((a0,a1),(b0,b1)):

-	return (_max(a0,b0),_max(a1,b1))

-

-def lerp(a,b,t):

-	return add(mulN(a,1.0-t), mulN(b, t))

-

-def toint(a):

-	return (int(a[0]), int(a[1]))

-def tofloor(a):

-	return (floor(a[0]), floor(a[1]))

-def toceil(a):

-	return (ceil(a[0]), ceil(a[1]))

-

-def sumlist(l):

-	return reduce(add, l)

-def avglist(l):

-	return mulN(sumlist(l), 1.0/len(l))

-

+from __future__ import division
+from math import ceil,floor,sqrt,atan2,pi,cos,sin
+import random
+_abs,_min,_max= abs,min,max
+
+def random(rng=random):
+	return (rng.random()*2-1,rng.random()*2-1)
+
+def getangle(a):
+	x,y= a
+	if y>=0:
+		return atan2(y,x)
+	else:
+		return pi*2 + atan2(y,x)
+toangle = getangle
+
+def topolar(pt):
+	return getangle(pt),length(pt)
+def fromangle(angle,radius=1.):
+	return (cos(angle)*radius, sin(angle)*radius)
+frompolar = fromangle
+
+def rotate((x,y),angle):
+	c_a,s_a = cos(angle),sin(angle)
+	return (c_a*x - s_a*y, s_a*x + c_a*y)
+
+def rotate90((x,y)):
+	return (-y,x)
+	
+def abs(a): return (_abs(a[0]),_abs(a[1]))	
+def inv(a):	return (-a[0], -a[1])
+
+def add(a,b):	return (a[0]+b[0], a[1]+b[1])
+def sub(a,b):	return (a[0]-b[0], a[1]-b[1])
+def mul(a,b):	return (a[0]*b[0], a[1]*b[1])
+def div(a,b):	return (a[0]/b[0], a[1]/b[1])
+def mod(a,b):	return (a[0]%b[0], a[1]%b[1])
+def dot(a,b):	return (a[0]*b[0]+ a[1]*b[1])
+
+def addN(a,n):	return (a[0]+n, a[1]+n)
+def subN(a,n):	return (a[0]-n, a[1]-n)
+def mulN(a,n):	return (a[0]*n, a[1]*n)
+def modN(a,n):	return (a[0]%n, a[1]%n)
+def divN(a,n):	return (a[0]/n, a[1]/n)
+
+def sqr(a):			return dot(a,a)
+def length(a):		return sqrt(sqr(a))
+def avg(a,b):		return mulN(add(a,b),0.5)
+def distance(a,b):	return length(sub(a,b))
+
+def normalize(a):
+	return mulN(a, 1.0/length(a))
+
+def normalizeOrZero(a):
+	try:
+		return mulN(a, 1.0/length(a))
+	except ZeroDivisionError:
+		return (0.0,0.0)
+	
+def min((a0,a1),(b0,b1)):
+	return (_min(a0,b0),_min(a1,b1))
+def max((a0,a1),(b0,b1)):
+	return (_max(a0,b0),_max(a1,b1))
+
+def lerp(a,b,t):
+	return add(mulN(a,1.0-t), mulN(b, t))
+
+def toint(a):
+	return (int(a[0]), int(a[1]))
+def tofloor(a):
+	return (floor(a[0]), floor(a[1]))
+def toceil(a):
+	return (ceil(a[0]), ceil(a[1]))
+
+def sumlist(l):
+	return reduce(add, l)
+def avglist(l):
+	return mulN(sumlist(l), 1.0/len(l))
+
diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/vec3.py b/utils/hacks/TreeGraphs/Graphics/Geometry/vec3.py
index ed4d8114..48ebf129 100644
--- a/utils/hacks/TreeGraphs/Graphics/Geometry/vec3.py
+++ b/utils/hacks/TreeGraphs/Graphics/Geometry/vec3.py
@@ -1,55 +1,55 @@
-from __future__ import division

-from math import ceil,floor,sqrt

-from random import random as _random

-_min,_max= min,max

-

-def random():

-	return (_random()*2-1,_random()*2-1,_random()*2-1)

-

-def inv(a):	return (-a[0],-a[1],-a[2])

-

-def add(a,b):	return (a[0]+b[0], a[1]+b[1], a[2]+b[2])

-def sub(a,b):	return (a[0]-b[0], a[1]-b[1], a[2]-b[2])

-def mul(a,b):	return (a[0]*b[0], a[1]*b[1], a[2]*b[2])

-def div(a,b):	return (a[0]/b[0], a[1]/b[1], a[2]/b[2])

-def mod(a,b):	return (a[0]%b[0], a[1]%b[1], a[2]%b[2])

-def dot(a,b):	return (a[0]*b[0]+ a[1]*b[1]+ a[2]*b[2])

-

-def addN(a,n):	return (a[0]+n, a[1]+n, a[2]+n)

-def subN(a,n):	return (a[0]-n, a[1]-n, a[2]-n)

-def mulN(a,n):	return (a[0]*n, a[1]*n, a[2]*n)

-def modN(a,n):	return (a[0]%n, a[1]%n, a[2]%n)

-def divN(a,n):	return (a[0]/n, a[1]/n, a[2]/n)

-

-def sqr(a):			return dot(a,a)

-def length(a):		return sqrt(sqr(a))

-def normalize(a):	return mulN(a, 1.0/length(a))

-def avg(a,b):		return mulN(add(a,b),0.5)

-def distance(a,b):	return length(sub(a,b))

-

-def cross(a, b):

-	return (a[1]*b[2] - a[2]*b[1],

-			a[2]*b[0] - a[0]*b[2],

-			a[0]*b[1] - a[1]*b[0])

-def reflect(a, b):

-	return sub(mulN(b, dot(a, b)*2), a)

-

-def lerp(a,b,t):

-	return add(mulN(a,1.0-t), mulN(b, t))

-

-def min((a0,a1,a2),(b0,b1,b2)):

-	return (_min(a0,b0),_min(a1,b1),_min(a2,b2))

-def max((a0,a1,a2),(b0,b1,b2)):

-	return (_max(a0,b0),_max(a1,b1),_max(a2,b2))

-

-def toint(a):

-	return (int(a[0]), int(a[1]), int(a[2]))

-def tofloor(a):

-	return (floor(a[0]), floor(a[1]), floor(a[2]))

-def toceil(a):

-	return (ceil(a[0]), ceil(a[1]), ceil(a[2]))

-

-def sumlist(l):

-	return reduce(add, l)

-def avglist(l):

-	return mulN(sumlist(l), 1.0/len(l))

+from __future__ import division
+from math import ceil,floor,sqrt
+from random import random as _random
+_min,_max= min,max
+
+def random():
+	return (_random()*2-1,_random()*2-1,_random()*2-1)
+
+def inv(a):	return (-a[0],-a[1],-a[2])
+
+def add(a,b):	return (a[0]+b[0], a[1]+b[1], a[2]+b[2])
+def sub(a,b):	return (a[0]-b[0], a[1]-b[1], a[2]-b[2])
+def mul(a,b):	return (a[0]*b[0], a[1]*b[1], a[2]*b[2])
+def div(a,b):	return (a[0]/b[0], a[1]/b[1], a[2]/b[2])
+def mod(a,b):	return (a[0]%b[0], a[1]%b[1], a[2]%b[2])
+def dot(a,b):	return (a[0]*b[0]+ a[1]*b[1]+ a[2]*b[2])
+
+def addN(a,n):	return (a[0]+n, a[1]+n, a[2]+n)
+def subN(a,n):	return (a[0]-n, a[1]-n, a[2]-n)
+def mulN(a,n):	return (a[0]*n, a[1]*n, a[2]*n)
+def modN(a,n):	return (a[0]%n, a[1]%n, a[2]%n)
+def divN(a,n):	return (a[0]/n, a[1]/n, a[2]/n)
+
+def sqr(a):			return dot(a,a)
+def length(a):		return sqrt(sqr(a))
+def normalize(a):	return mulN(a, 1.0/length(a))
+def avg(a,b):		return mulN(add(a,b),0.5)
+def distance(a,b):	return length(sub(a,b))
+
+def cross(a, b):
+	return (a[1]*b[2] - a[2]*b[1],
+			a[2]*b[0] - a[0]*b[2],
+			a[0]*b[1] - a[1]*b[0])
+def reflect(a, b):
+	return sub(mulN(b, dot(a, b)*2), a)
+
+def lerp(a,b,t):
+	return add(mulN(a,1.0-t), mulN(b, t))
+
+def min((a0,a1,a2),(b0,b1,b2)):
+	return (_min(a0,b0),_min(a1,b1),_min(a2,b2))
+def max((a0,a1,a2),(b0,b1,b2)):
+	return (_max(a0,b0),_max(a1,b1),_max(a2,b2))
+
+def toint(a):
+	return (int(a[0]), int(a[1]), int(a[2]))
+def tofloor(a):
+	return (floor(a[0]), floor(a[1]), floor(a[2]))
+def toceil(a):
+	return (ceil(a[0]), ceil(a[1]), ceil(a[2]))
+
+def sumlist(l):
+	return reduce(add, l)
+def avglist(l):
+	return mulN(sumlist(l), 1.0/len(l))
diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/vec4.py b/utils/hacks/TreeGraphs/Graphics/Geometry/vec4.py
index 3a542272..c0741bb3 100644
--- a/utils/hacks/TreeGraphs/Graphics/Geometry/vec4.py
+++ b/utils/hacks/TreeGraphs/Graphics/Geometry/vec4.py
@@ -1,46 +1,46 @@
-from __future__ import division

-from math import ceil,floor,sqrt

-import vec3

-_min,_max= min,max

-

-def inv(a):	return (-a[0], -a[1], -a[2], -a[3])

-

-def add(a,b):	return (a[0]+b[0], a[1]+b[1], a[2]+b[2], a[3]+b[3])

-def sub(a,b):	return (a[0]-b[0], a[1]-b[1], a[2]-b[2], a[3]-b[3])

-def mul(a,b):	return (a[0]*b[0], a[1]*b[1], a[2]*b[2], a[3]*b[3])

-def div(a,b):	return (a[0]/b[0], a[1]/b[1], a[2]/b[2], a[3]/b[3])

-def mod(a,b):	return (a[0]%b[0], a[1]%b[1], a[2]%b[2], a[3]%b[3])

-def dot(a,b):	return (a[0]*b[0]+ a[1]*b[1]+ a[2]*b[2]+ a[3]*b[3])

-

-def addN(a,n):	return (a[0]+n, a[1]+n, a[2]+n, a[3]+n)

-def subN(a,n):	return (a[0]-n, a[1]-n, a[2]-n, a[3]-n)

-def mulN(a,n):	return (a[0]*n, a[1]*n, a[2]*n, a[3]*n)

-def modN(a,n):	return (a[0]%n, a[1]%n, a[2]%n, a[3]%n)

-def divN(a,n):	return (a[0]/n, a[1]/n, a[2]/n, a[3]/n)

-

-def sqr(a):		return dot(a,a)

-def length(a):	return sqrt(sqr(a))

-def avg(a,b):	return mulN(add(a,b),0.5)

-def normalize(a):	return mulN(a, 1.0/length(a))

-

-def lerp(a,b,t):

-	return add(mulN(a,1.0-t), mulN(b, t))

-

-def min((a0,a1,a2,a3),(b0,b1,b2,b3)):

-	return (_min(a0,b0),_min(a1,b1),_min(a2,b2),_min(a3,b3))

-def max((a0,a1,a2,a3),(b0,b1,b2,b3)):

-	return (_max(a0,b0),_max(a1,b1),_max(a2,b2),_max(a3,b3))

-

-def toint(a):

-	return (int(a[0]), int(a[1]), int(a[2]), int(a[3]))

-def tofloor(a):

-	return (floor(a[0]), floor(a[1]), floor(a[2]), floor(a[3]))

-def toceil(a):

-	return (ceil(a[0]), ceil(a[1]), ceil(a[2]), ceil(a[3]))

-def tovec3(a):

-	return vec3.divN(a, a[3])

-

-def sumlist(l):

-	return reduce(add, l)

-def avglist(l):

-	return mulN(sumlist(l), 1.0/len(l))

+from __future__ import division
+from math import ceil,floor,sqrt
+import vec3
+_min,_max= min,max
+
+def inv(a):	return (-a[0], -a[1], -a[2], -a[3])
+
+def add(a,b):	return (a[0]+b[0], a[1]+b[1], a[2]+b[2], a[3]+b[3])
+def sub(a,b):	return (a[0]-b[0], a[1]-b[1], a[2]-b[2], a[3]-b[3])
+def mul(a,b):	return (a[0]*b[0], a[1]*b[1], a[2]*b[2], a[3]*b[3])
+def div(a,b):	return (a[0]/b[0], a[1]/b[1], a[2]/b[2], a[3]/b[3])
+def mod(a,b):	return (a[0]%b[0], a[1]%b[1], a[2]%b[2], a[3]%b[3])
+def dot(a,b):	return (a[0]*b[0]+ a[1]*b[1]+ a[2]*b[2]+ a[3]*b[3])
+
+def addN(a,n):	return (a[0]+n, a[1]+n, a[2]+n, a[3]+n)
+def subN(a,n):	return (a[0]-n, a[1]-n, a[2]-n, a[3]-n)
+def mulN(a,n):	return (a[0]*n, a[1]*n, a[2]*n, a[3]*n)
+def modN(a,n):	return (a[0]%n, a[1]%n, a[2]%n, a[3]%n)
+def divN(a,n):	return (a[0]/n, a[1]/n, a[2]/n, a[3]/n)
+
+def sqr(a):		return dot(a,a)
+def length(a):	return sqrt(sqr(a))
+def avg(a,b):	return mulN(add(a,b),0.5)
+def normalize(a):	return mulN(a, 1.0/length(a))
+
+def lerp(a,b,t):
+	return add(mulN(a,1.0-t), mulN(b, t))
+
+def min((a0,a1,a2,a3),(b0,b1,b2,b3)):
+	return (_min(a0,b0),_min(a1,b1),_min(a2,b2),_min(a3,b3))
+def max((a0,a1,a2,a3),(b0,b1,b2,b3)):
+	return (_max(a0,b0),_max(a1,b1),_max(a2,b2),_max(a3,b3))
+
+def toint(a):
+	return (int(a[0]), int(a[1]), int(a[2]), int(a[3]))
+def tofloor(a):
+	return (floor(a[0]), floor(a[1]), floor(a[2]), floor(a[3]))
+def toceil(a):
+	return (ceil(a[0]), ceil(a[1]), ceil(a[2]), ceil(a[3]))
+def tovec3(a):
+	return vec3.divN(a, a[3])
+
+def sumlist(l):
+	return reduce(add, l)
+def avglist(l):
+	return mulN(sumlist(l), 1.0/len(l))
diff --git a/utils/hacks/TreeGraphs/Graphics/__init__.py b/utils/hacks/TreeGraphs/Graphics/__init__.py
index 4055b3ef..645cf234 100644
--- a/utils/hacks/TreeGraphs/Graphics/__init__.py
+++ b/utils/hacks/TreeGraphs/Graphics/__init__.py
@@ -1 +1 @@
-__all__= ['Formats', 'SubSurf', 'Geometry', 'AqsisInterface', 'TwoD', 'ThreeD', 'Apps']

+__all__= ['Formats', 'SubSurf', 'Geometry', 'AqsisInterface', 'TwoD', 'ThreeD', 'Apps']