Initial KLEE checkin.

 - Lots more tweaks, documentation, and web page content is needed,
   but this should compile & work on OS X & Linux.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8

46 files changed, 6215 insertions, 0 deletions

diff --git a/include/expr/Lexer.h b/include/expr/Lexer.h
new file mode 100644
index 00000000..4ae760a0
--- /dev/null
+++ b/include/expr/Lexer.h
@@ -0,0 +1,114 @@
+//===-- Lexer.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_EXPR_LEXER_H
+#define KLEE_EXPR_LEXER_H
+
+#include <string>
+
+namespace llvm {
+  class MemoryBuffer;
+}
+
+namespace klee {
+namespace expr {
+  struct Token {
+    enum Kind {
+      At,                       /// '@'
+      Arrow,                    /// '->'
+      Colon,                    /// ':'
+      Comma,                    /// ','
+      Comment,                  /// #[^\n]+
+      EndOfFile,                /// <end of file>
+      Equals,                   /// ' = '
+      Identifier,               /// [a-zA-Z_][a-zA-Z0-9._]*
+      KWFalse,                  /// 'false'
+      KWQuery,                  /// 'query'
+      KWReserved,               /// fp[0-9]+([.].*)?, i[0-9]+
+      KWTrue,                   /// 'true'
+      KWWidth,                  /// w[0-9]+
+      LBrace,                   /// '{'
+      LParen,                   /// '('
+      LSquare,                  /// '['
+      Number,                   /// [+-]?[0-9][a-zA-Z0-9_]+
+      RBrace,                   /// '}'
+      RParen,                   /// ')'
+      RSquare,                  /// ']'
+      Semicolon,                /// ';'
+      Unknown                   /// <other>
+    };
+
+    Kind        kind;           /// The token kind.
+    const char *start;          /// The beginning of the token string. 
+    unsigned    length;         /// The length of the token.
+    unsigned    line;           /// The line number of the start of this token.
+    unsigned    column;         /// The column number at the start of
+                                /// this token.
+
+    /// getKindName - The name of this token's kind.
+    const char *getKindName() const;
+
+    /// getString - The string spanned by this token. This is not
+    /// particularly efficient, use start and length when reasonable.
+    std::string getString() const { return std::string(start, length); }
+
+    /// isKeyword - True if this token is a keyword.
+    bool isKeyword() const { 
+      return kind >= KWFalse && kind <= KWTrue; 
+    }
+
+    // dump - Dump the token to stderr.
+    void dump();
+  };
+
+  /// Lexer - Interface for lexing tokens from a .pc language file.
+  class Lexer {
+    const char *BufferPos;      /// The current lexer position.
+    const char *BufferEnd;      /// The buffer end position.
+    unsigned    LineNumber;     /// The current line.
+    unsigned    ColumnNumber;   /// The current column.
+
+    /// GetNextChar - Eat a character or -1 from the stream.
+    int GetNextChar();
+
+    /// PeekNextChar - Return the next character without consuming it
+    /// from the stream. This does not perform newline
+    /// canonicalization.
+    int PeekNextChar();
+
+    /// SetTokenKind - Set the token kind and length (using the
+    /// token's start pointer, which must have been initialized).
+    Token &SetTokenKind(Token &Result, Token::Kind k);
+
+    /// SetTokenKind - Set an identifiers token kind. This has the
+    /// same requirements as SetTokenKind and additionally takes care
+    /// of keyword recognition.
+    Token &SetIdentifierTokenKind(Token &Result);
+  
+    void SkipToEndOfLine();
+
+    /// LexNumber - Lex a number which does not have a base specifier.
+    Token &LexNumber(Token &Result);
+
+    /// LexIdentifier - Lex an identifier.
+    Token &LexIdentifier(Token &Result);
+
+  public:
+    explicit Lexer(const llvm::MemoryBuffer *_buf);
+    ~Lexer();
+
+    /// Lex - Return the next token from the file or EOF continually
+    /// when the end of the file is reached. The input argument is
+    /// used as the result, for convenience.
+    Token &Lex(Token &Result);
+  };
+}
+}
+
+#endif
diff --git a/include/expr/Parser.h b/include/expr/Parser.h
new file mode 100644
index 00000000..7634d66a
--- /dev/null
+++ b/include/expr/Parser.h
@@ -0,0 +1,178 @@
+//===-- Parser.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_EXPR_PARSER_H
+#define KLEE_EXPR_PARSER_H
+
+#include "klee/Expr.h"
+
+#include <vector>
+#include <string>
+
+namespace llvm {
+  class MemoryBuffer;
+}
+
+namespace klee {
+namespace expr {
+  // These are the language types we manipulate.
+  typedef ref<Expr> ExprHandle;
+  typedef UpdateList VersionHandle;
+  
+  /// Identifier - Wrapper for a uniqued string.
+  struct Identifier {
+    const std::string Name;
+
+  public:
+    Identifier(const std::string _Name) : Name(_Name) {}
+  };
+
+  // FIXME: Do we have a use for tracking source locations?
+
+  /// Decl - Base class for top level declarations.
+  class Decl {
+  public:
+    Decl();
+    virtual ~Decl() {}
+
+    /// dump - Dump the AST node to stderr.
+    virtual void dump() = 0;
+  };
+
+  /// ArrayDecl - Array declarations.
+  ///
+  /// For example:
+  ///   array obj : 32 -> 8 = symbolic
+  ///   array obj[32] : 32 -> 8 = { ... }
+  class ArrayDecl : public Decl {
+  public:
+    /// Name - The name of this array.
+    const Identifier *Name;
+
+    /// Size - The maximum array size (or 0 if unspecified). Concrete
+    /// arrays always are specified with a size.
+    const unsigned Size;
+
+    /// Domain - The width of indices.
+    const unsigned Domain;
+
+    /// Range - The width of array contents.
+    const unsigned Range;
+    
+    /// Contents - The initial contents of the array. The array is
+    /// symbolic if no contents are specified. The contained
+    /// expressions are guaranteed to be constants.
+    const std::vector<ExprHandle> Contents;
+
+  public:
+    template<typename InputIterator>
+    ArrayDecl(const Identifier *_Name, unsigned _Size, 
+              unsigned _Domain, unsigned _Range,
+              InputIterator ContentsBegin=InputIterator(), 
+              InputIterator ContentsEnd=InputIterator()) 
+      : Name(_Name), Size(_Size), Domain(_Domain), Range(_Range),
+        Contents(ContentsBegin, ContentsEnd) {}
+  };
+
+  /// VarDecl - Variable declarations, used to associate names to
+  /// expressions or array versions outside of expressions.
+  /// 
+  /// For example:
+  // FIXME: What syntax are we going to use for this? We need it.
+  class VarDecl : public Decl {
+  public:
+    const Identifier *Name;    
+  };
+
+  /// ExprVarDecl - Expression variable declarations.
+  class ExprVarDecl : public VarDecl {
+  public:
+    ExprHandle Value;
+  };
+
+  /// VersionVarDecl - Array version variable declarations.
+  class VersionVarDecl : public VarDecl {
+  public:
+    VersionHandle Value;
+  };
+
+  /// CommandDecl - Base class for language commands.
+  class CommandDecl : public Decl {
+  public:
+    const Identifier *Name;
+  };
+
+  /// QueryCommand - Query commands.
+  ///
+  /// (query [ ... constraints ... ] expression)
+  /// (query [ ... constraints ... ] expression values)
+  /// (query [ ... constraints ... ] expression values objects)
+  class QueryCommand : public CommandDecl {
+  public:
+    // FIXME: One issue with STP... should we require the FE to
+    // guarantee that these are consistent? That is a cornerstone of
+    // being able to do independence. We may want this as a flag, if
+    // we are to interface with things like SMT.
+
+    /// Constraints - The list of constraints to assume for this
+    /// expression.
+    const std::vector<ExprHandle> Constraints;
+    
+    /// Query - The expression being queried.
+    ExprHandle Query;
+
+    /// Values - The expressions for which counterexamples should be
+    /// given if the query is invalid.
+    const std::vector<ExprHandle> Values;
+
+    /// Objects - Symbolic arrays whose initial contents should be
+    /// given if the query is invalid.
+    const std::vector<ArrayDecl> Objects;
+
+  public:
+    template<typename InputIterator>
+    QueryCommand(InputIterator ConstraintsBegin, 
+                 InputIterator ConstraintsEnd,
+                 ExprHandle _Query)
+      : Constraints(ConstraintsBegin, ConstraintsEnd),
+        Query(_Query) {}
+
+    virtual void dump();
+  };
+  
+  /// Parser - Public interface for parsing a .pc language file.
+  class Parser {
+  protected:
+    Parser();
+  public:
+    virtual ~Parser();
+
+    /// SetMaxErrors - Suppress anything beyond the first N errors.
+    virtual void SetMaxErrors(unsigned N) = 0;
+    
+    /// GetNumErrors - Return the number of encountered errors.
+    virtual unsigned GetNumErrors() const = 0;
+
+    /// ParseTopLevelDecl - Parse and return a top level declaration,
+    /// which the caller assumes ownership of.
+    ///
+    /// \return NULL indicates the end of the file has been reached.
+    virtual Decl *ParseTopLevelDecl() = 0;
+
+    /// CreateParser - Create a parser implementation for the given
+    /// MemoryBuffer.
+    ///
+    /// \arg Name - The name to use in diagnostic messages.
+    static Parser *Create(const std::string Name,
+                          const llvm::MemoryBuffer *MB);
+  };
+}
+}
+
+#endif
diff --git a/include/klee/Config/config.h.in b/include/klee/Config/config.h.in
new file mode 100644
index 00000000..ef41d786
--- /dev/null
+++ b/include/klee/Config/config.h.in
@@ -0,0 +1,64 @@
+/* include/klee/Config/config.h.in.  Generated from autoconf/configure.tmp.ac by autoheader.  */
+
+/* Define if stplog enabled */
+#undef ENABLE_STPLOG
+
+/* Does the platform use __ctype_b_loc, etc. */
+#undef HAVE_CTYPE_EXTERNALS
+
+/* Define to 1 if you have the <inttypes.h> header file. */
+#undef HAVE_INTTYPES_H
+
+/* Define to 1 if you have the <memory.h> header file. */
+#undef HAVE_MEMORY_H
+
+/* Define to 1 if you have the <selinux/selinux.h> header file. */
+#undef HAVE_SELINUX_SELINUX_H
+
+/* Define to 1 if you have the <stdint.h> header file. */
+#undef HAVE_STDINT_H
+
+/* Define to 1 if you have the <stdlib.h> header file. */
+#undef HAVE_STDLIB_H
+
+/* Define to 1 if you have the <strings.h> header file. */
+#undef HAVE_STRINGS_H
+
+/* Define to 1 if you have the <string.h> header file. */
+#undef HAVE_STRING_H
+
+/* Define to 1 if you have the <sys/acl.h> header file. */
+#undef HAVE_SYS_ACL_H
+
+/* Define to 1 if you have the <sys/stat.h> header file. */
+#undef HAVE_SYS_STAT_H
+
+/* Define to 1 if you have the <sys/types.h> header file. */
+#undef HAVE_SYS_TYPES_H
+
+/* Define to 1 if you have the <unistd.h> header file. */
+#undef HAVE_UNISTD_H
+
+/* Path to KLEE's uClibc */
+#undef KLEE_UCLIBC
+
+/* Define to the address where bug reports for this package should be sent. */
+#undef PACKAGE_BUGREPORT
+
+/* Define to the full name of this package. */
+#undef PACKAGE_NAME
+
+/* Define to the full name and version of this package. */
+#undef PACKAGE_STRING
+
+/* Define to the one symbol short name of this package. */
+#undef PACKAGE_TARNAME
+
+/* Define to the version of this package. */
+#undef PACKAGE_VERSION
+
+/* Configuration for runtime libraries */
+#undef RUNTIME_CONFIGURATION
+
+/* Define to 1 if you have the ANSI C header files. */
+#undef STDC_HEADERS
diff --git a/include/klee/Constraints.h b/include/klee/Constraints.h
new file mode 100644
index 00000000..87069f89
--- /dev/null
+++ b/include/klee/Constraints.h
@@ -0,0 +1,79 @@
+//===-- Constraints.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_CONSTRAINTS_H
+#define KLEE_CONSTRAINTS_H
+
+#include "klee/Expr.h"
+
+// FIXME: Currently we use ConstraintManager for two things: to pass
+// sets of constraints around, and to optimize constraints. We should
+// move the first usage into a separate data structure
+// (ConstraintSet?) which ConstraintManager could embed if it likes.
+namespace klee {
+
+class ExprVisitor;
+  
+class ConstraintManager {
+public:
+  typedef std::vector< ref<Expr> > constraints_ty;
+  typedef constraints_ty::iterator iterator;
+  typedef constraints_ty::const_iterator const_iterator;
+
+  ConstraintManager() {}
+
+  // create from constraints with no optimization
+  explicit
+  ConstraintManager(const std::vector< ref<Expr> > &_constraints) :
+    constraints(_constraints) {}
+
+  ConstraintManager(const ConstraintManager &cs) : constraints(cs.constraints) {}
+
+  typedef std::vector< ref<Expr> >::const_iterator constraint_iterator;
+
+  // given a constraint which is known to be valid, attempt to 
+  // simplify the existing constraint set
+  void simplifyForValidConstraint(ref<Expr> e);
+
+  ref<Expr> simplifyExpr(ref<Expr> e) const;
+
+  void addConstraint(ref<Expr> e);
+  
+  bool empty() const {
+    return constraints.empty();
+  }
+  ref<Expr> back() const {
+    return constraints.back();
+  }
+  constraint_iterator begin() const {
+    return constraints.begin();
+  }
+  constraint_iterator end() const {
+    return constraints.end();
+  }
+  size_t size() const {
+    return constraints.size();
+  }
+
+  bool operator==(const ConstraintManager &other) const {
+    return constraints == other.constraints;
+  }
+  
+private:
+  std::vector< ref<Expr> > constraints;
+
+  // returns true iff the constraints were modified
+  bool rewriteConstraints(ExprVisitor &visitor);
+
+  void addConstraintInternal(ref<Expr> e);
+};
+
+}
+
+#endif /* KLEE_CONSTRAINTS_H */
diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h
new file mode 100644
index 00000000..09ce2a4b
--- /dev/null
+++ b/include/klee/ExecutionState.h
@@ -0,0 +1,250 @@
+//===-- ExecutionState.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_EXECUTIONSTATE_H
+#define KLEE_EXECUTIONSTATE_H
+
+#include "klee/Constraints.h"
+#include "klee/Expr.h"
+#include "klee/Internal/ADT/TreeStream.h"
+
+// FIXME: We do not want to be exposing these? :(
+#include "../../lib/Core/AddressSpace.h"
+#include "klee/Internal/Module/KInstIterator.h"
+
+#include <map>
+#include <set>
+#include <vector>
+
+namespace klee {
+  class CallPathNode;
+  class Cell;
+  class KFunction;
+  class KInstruction;
+  class MemoryObject;
+  class PTreeNode;
+  class InstructionInfo;
+  class ExecutionTraceEvent;
+
+std::ostream &operator<<(std::ostream &os, const MemoryMap &mm);
+
+struct StackFrame {
+  KInstIterator caller;
+  KFunction *kf;
+  CallPathNode *callPathNode;
+
+  std::vector<const MemoryObject*> allocas;
+  Cell *locals;
+
+  /// Minimum distance to an uncovered instruction once the function
+  /// returns. This is not a good place for this but is used to
+  /// quickly compute the context sensitive minimum distance to an
+  /// uncovered instruction. This value is updated by the StatsTracker
+  /// periodically.
+  unsigned minDistToUncoveredOnReturn;
+
+  // For vararg functions: arguments not passed via parameter are
+  // stored (packed tightly) in a local (alloca) memory object. This
+  // is setup to match the way the front-end generates vaarg code (it
+  // does not pass vaarg through as expected). VACopy is lowered inside
+  // of intrinsic lowering.
+  MemoryObject *varargs;
+
+  StackFrame(KInstIterator caller, KFunction *kf);
+  StackFrame(const StackFrame &s);
+  ~StackFrame();
+};
+
+// FIXME: Redo execution trace stuff to use a TreeStream, there is no
+// need to keep this stuff in memory as far as I can tell.
+
+// each state should have only one of these guys ...
+class ExecutionTraceManager {
+public:
+  ExecutionTraceManager() : hasSeenUserMain(false) {}
+
+  void addEvent(ExecutionTraceEvent* evt);
+  void printAllEvents(std::ostream &os) const;
+
+private:
+  // have we seen a call to __user_main() yet?
+  // don't bother tracing anything until we see this,
+  // or else we'll get junky prologue shit
+  bool hasSeenUserMain;
+
+  // ugh C++ only supports polymorphic calls thru pointers
+  //
+  // WARNING: these are NEVER FREED, because they are shared
+  // across different states (when states fork), so we have 
+  // an *intentional* memory leak, but oh wellz ;)
+  std::vector<ExecutionTraceEvent*> events;
+};
+
+
+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;
+
+public:
+  bool fakeState;
+  // Are we currently underconstrained?  Hack: value is size to make fake
+  // objects.
+  unsigned underConstrained;
+  unsigned depth;
+  
+  // pc - pointer to current instruction stream
+  KInstIterator pc, prevPC;
+  stack_ty stack;
+  ConstraintManager constraints;
+  mutable double queryCost;
+  double weight;
+  AddressSpace addressSpace;
+  TreeOStream pathOS, symPathOS;
+  unsigned instsSinceCovNew;
+  bool coveredNew;
+
+  // for printing execution traces when this state terminates
+  ExecutionTraceManager exeTraceMgr;
+
+  /// Disables forking, set by user code.
+  bool forkDisabled;
+
+  std::map<const std::string*, std::set<unsigned> > coveredLines;
+  PTreeNode *ptreeNode;
+
+  /// ordered list of symbolics: used to generate test cases. 
+  //
+  // FIXME: Move to a shared list structure (not critical).
+  std::vector<const MemoryObject*> symbolics;
+
+  // 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), underConstrained(0), ptreeNode(0) {};
+
+public:
+  ExecutionState(KFunction *kf);
+
+  // XXX total hack, just used to make a state so solver can
+  // use on structure
+  ExecutionState(const std::vector<ref<Expr> > &assumptions);
+
+  ~ExecutionState();
+  
+  ExecutionState *branch();
+
+  void pushFrame(KInstIterator caller, KFunction *kf);
+  void popFrame();
+
+  void addSymbolic(const MemoryObject *mo) { 
+    symbolics.push_back(mo);
+  }
+  void addConstraint(ref<Expr> e) { 
+    constraints.addConstraint(e); 
+  }
+
+  // Used for checkpoint/rollback of fake objects created during tainting.
+  ObjectState *cloneObject(ObjectState *os, MemoryObject *mo);
+
+  //
+
+  bool merge(const ExecutionState &b);
+};
+
+
+// for producing abbreviated execution traces to help visualize
+// paths and diagnose bugs
+
+class ExecutionTraceEvent {
+public:
+  // the location of the instruction:
+  std::string file;
+  unsigned line;
+  std::string funcName;
+  unsigned stackDepth;
+
+  unsigned consecutiveCount; // init to 1, increase for CONSECUTIVE
+                             // repetitions of the SAME event
+
+  ExecutionTraceEvent()
+    : file("global"), line(0), funcName("global_def"),
+      consecutiveCount(1) {}
+
+  ExecutionTraceEvent(ExecutionState& state, KInstruction* ki);
+
+  virtual ~ExecutionTraceEvent() {}
+
+  void print(std::ostream &os) const;
+
+  // return true if it shouldn't be added to ExecutionTraceManager
+  //
+  virtual bool ignoreMe() const;
+
+private:
+  virtual void printDetails(std::ostream &os) const = 0;
+};
+
+
+class FunctionCallTraceEvent : public ExecutionTraceEvent {
+public:
+  std::string calleeFuncName;
+
+  FunctionCallTraceEvent(ExecutionState& state, KInstruction* ki,
+                         const std::string& _calleeFuncName)
+    : ExecutionTraceEvent(state, ki), calleeFuncName(_calleeFuncName) {}
+
+private:
+  virtual void printDetails(std::ostream &os) const {
+    os << "CALL " << calleeFuncName;
+  }
+
+};
+
+class FunctionReturnTraceEvent : public ExecutionTraceEvent {
+public:
+  FunctionReturnTraceEvent(ExecutionState& state, KInstruction* ki)
+    : ExecutionTraceEvent(state, ki) {}
+
+private:
+  virtual void printDetails(std::ostream &os) const {
+    os << "RETURN";
+  }
+};
+
+class BranchTraceEvent : public ExecutionTraceEvent {
+public:
+  bool trueTaken;         // which side taken?
+  bool canForkGoBothWays;
+
+  BranchTraceEvent(ExecutionState& state, KInstruction* ki,
+                   bool _trueTaken, bool _isTwoWay)
+    : ExecutionTraceEvent(state, ki),
+      trueTaken(_trueTaken),
+      canForkGoBothWays(_isTwoWay) {}
+
+private:
+  virtual void printDetails(std::ostream &os) const;
+};
+
+}
+
+#endif
diff --git a/include/klee/Expr.h b/include/klee/Expr.h
new file mode 100644
index 00000000..d16a09bf
--- /dev/null
+++ b/include/klee/Expr.h
@@ -0,0 +1,808 @@
+//===-- Expr.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_EXPR_H
+#define KLEE_EXPR_H
+
+#include "Machine.h"
+#include "klee/util/Bits.h"
+
+#include "llvm/Support/Streams.h"
+#include "llvm/ADT/SmallVector.h"
+
+#include <set>
+#include <vector>
+
+namespace llvm {
+  class Type;
+}
+
+namespace klee {
+
+class Array;
+class ConstantExpr;
+class ObjectState;
+class MemoryObject;
+
+template<class T> class ref;
+
+
+/// Class representing symbolic expressions.
+/**
+
+<b>Expression canonicalization</b>: we define certain rules for
+canonicalization rules for Exprs in order to simplify code that
+pattern matches Exprs (since the number of forms are reduced), to open
+up further chances for optimization, and to increase similarity for
+caching and other purposes.
+
+The general rules are:
+<ol>
+<li> No Expr has all constant arguments.</li>
+
+<li> Booleans:
+    <ol type="a">
+    <li> Boolean not is written as <tt>(false == ?)</tt> </li>
+     <li> \c Ne, \c Ugt, \c Uge, \c Sgt, \c Sge are not used </li>
+     <li> The only acceptable operations with boolean arguments are \c And, 
+          \c Or, \c Xor, \c Eq, as well as \c SExt, \c ZExt,
+          \c Select and \c NotOptimized. </li>
+     <li> The only boolean operation which may involve a constant is boolean not (<tt>== false</tt>). </li>
+     </ol>
+</li>
+
+<li> Linear Formulas: 
+   <ol type="a">
+   <li> For any subtree representing a linear formula, a constant
+   term must be on the LHS of the root node of the subtree.  In particular, 
+   in a BinaryExpr a constant must always be on the LHS.  For example, subtraction 
+   by a constant c is written as <tt>add(-c, ?)</tt>.  </li>
+    </ol>
+</li>
+
+
+<li> Chains are unbalanced to the right </li>
+
+</ol>
+
+
+<b>Steps required for adding an expr</b>:
+   -# Add case to printKind
+   -# Add to ExprVisitor
+   -# Add to IVC (implied value concretization) if possible
+
+Todo: Shouldn't bool \c Xor just be written as not equal?
+
+*/
+
+class Expr {
+public:
+  static unsigned count;
+  static const unsigned MAGIC_HASH_CONSTANT = 39;
+
+  /// The type of an expression is simply its width, in bits. 
+  typedef unsigned Width; 
+  
+  static const Width InvalidWidth = 0;
+  static const Width Bool = 1;
+  static const Width Int8 = 8;
+  static const Width Int16 = 16;
+  static const Width Int32 = 32;
+  static const Width Int64 = 64;
+  
+
+  enum Kind {
+    InvalidKind = -1,
+
+    // Primitive
+
+    Constant = 0,
+
+    // Special
+
+    /// Prevents optimization below the given expression.  Used for
+    /// testing: make equality constraints that KLEE will not use to
+    /// optimize to concretes.
+    NotOptimized,
+
+    //// Skip old varexpr, just for deserialization, purge at some point
+    Read=NotOptimized+2, 
+    Select,
+    Concat,
+    Extract,
+
+    // Casting,
+    
+    ZExt,
+    SExt,
+
+    // Arithmetic
+    Add,
+    Sub,
+    Mul,
+    UDiv,
+    SDiv,
+    URem,
+    SRem,
+
+    // Bit
+    And,
+    Or,
+    Xor,
+    Shl,
+    LShr,
+    AShr,
+    
+    // Compare
+    Eq,
+    Ne,  /// Not used in canonical form
+    Ult,
+    Ule,
+    Ugt, /// Not used in canonical form
+    Uge, /// Not used in canonical form
+    Slt,
+    Sle,
+    Sgt, /// Not used in canonical form
+    Sge, /// Not used in canonical form
+
+    LastKind=Sge
+  };
+
+  unsigned refCount;
+
+protected:  
+  unsigned hashValue;
+  
+public:
+  Expr() : refCount(0) { Expr::count++; }
+  virtual ~Expr() { Expr::count--; } 
+
+  virtual Kind getKind() const = 0;
+  virtual Width getWidth() const = 0;
+  
+  virtual unsigned getNumKids() const = 0;
+  virtual ref<Expr> getKid(unsigned i) const = 0;
+    
+  virtual void print(std::ostream &os) const;
+
+  /// Returns the pre-computed hash of the current expression
+  virtual unsigned hash() const { return hashValue; }
+
+  /// (Re)computes the hash of the current expression.
+  /// Returns the hash value. 
+  virtual unsigned computeHash();
+  
+  static unsigned hashConstant(uint64_t val, Width w) {
+    return val ^ (w * MAGIC_HASH_CONSTANT);
+  }
+  
+  /// Returns 0 iff b is structuraly equivalent to *this
+  int compare(const Expr &b) const;
+  virtual int compareContents(const Expr &b) const { return 0; }
+
+  // Given an array of new kids return a copy of the expression
+  // but using those children. 
+  virtual ref<Expr> rebuild(ref<Expr> kids[/* getNumKids() */]) const = 0;
+
+  ///
+
+  uint64_t getConstantValue() const;
+
+  /* Static utility methods */
+
+  static void printKind(std::ostream &os, Kind k);
+  static void printWidth(std::ostream &os, Expr::Width w);
+  static Width getWidthForLLVMType(const llvm::Type *type);
+
+  /// returns the smallest number of bytes in which the given width fits
+  static inline unsigned getMinBytesForWidth(Width w) {
+      return (w + 7) / 8;
+  }
+
+  /* Kind utilities */
+
+  /* Utility creation functions */
+  static ref<Expr> createCoerceToPointerType(ref<Expr> e);
+  static ref<Expr> createNot(ref<Expr> e);
+  static ref<Expr> createImplies(ref<Expr> hyp, ref<Expr> conc);
+  static ref<Expr> createIsZero(ref<Expr> e);
+
+  /// Create a little endian read of the given type at offset 0 of the
+  /// given object.
+  static ref<Expr> createTempRead(const Array *array, Expr::Width w);
+  
+  static ref<Expr> createPointer(uint64_t v);
+
+  // do not use
+  static Expr *createConstant(uint64_t val, Width w);
+  
+  struct CreateArg;
+  static ref<Expr> createFromKind(Kind k, std::vector<CreateArg> args);
+
+  static bool isValidKidWidth(unsigned kid, Width w) { return true; }
+  static bool needsResultType() { return false; }
+};
+// END class Expr
+
+
+
+#include "klee/util/Ref.h"
+
+struct Expr::CreateArg {
+  ref<Expr> expr;
+  Width width;
+  
+  CreateArg(Width w = Bool) : expr(0, Expr::Bool), width(w) {}
+  CreateArg(ref<Expr> e) : expr(e), width(Expr::InvalidWidth) {}
+  
+  bool isExpr() { return !isWidth(); }
+  bool isWidth() { return width != Expr::InvalidWidth; }
+};
+
+// Comparison operators
+
+inline bool operator==(const Expr &lhs, const Expr &rhs) {
+  return lhs.compare(rhs) == 0;
+}
+
+inline bool operator<(const Expr &lhs, const Expr &rhs) {
+  return lhs.compare(rhs) < 0;
+}
+
+inline bool operator!=(const Expr &lhs, const Expr &rhs) {
+  return !(lhs == rhs);
+}
+
+inline bool operator>(const Expr &lhs, const Expr &rhs) {
+  return rhs < lhs;
+}
+
+inline bool operator<=(const Expr &lhs, const Expr &rhs) {
+  return !(lhs > rhs);
+}
+
+inline bool operator>=(const Expr &lhs, const Expr &rhs) {
+  return !(lhs < rhs);
+}
+
+// Printing operators
+
+inline std::ostream &operator<<(std::ostream &os, const Expr &e) {
+  e.print(os);
+  return os;
+}
+
+inline std::ostream &operator<<(std::ostream &os, const Expr::Kind kind) {
+  Expr::printKind(os, kind);
+  return os;
+}
+
+// Terminal Exprs
+
+class ConstantExpr : public Expr {
+public:
+  static const Kind kind = Constant;
+  static const unsigned numKids = 0;
+  
+public:
+  union {
+    uint64_t asUInt64;
+  };
+  Width width;
+
+public:
+  ~ConstantExpr() {};
+  // should change the code to make this private
+  ConstantExpr(uint64_t v, Width w) : asUInt64(v), width(w) {}
+  
+  Width getWidth() const { return width; }
+  Kind getKind() const { return Constant; }
+
+  unsigned getNumKids() const { return 0; }
+  ref<Expr> getKid(unsigned i) const { return 0; }
+
+  int compareContents(const Expr &b) const { 
+    const ConstantExpr &cb = static_cast<const ConstantExpr&>(b);
+    if (width != cb.width) return width < cb.width ? -1 : 1;
+    if (asUInt64 < cb.asUInt64) {
+      return -1;
+    } else if (asUInt64 > cb.asUInt64) {
+      return 1;
+    } else {
+      return 0;
+    }
+  }
+
+  virtual ref<Expr> rebuild(ref<Expr> kids[]) const { 
+    assert(0 && "rebuild() on ConstantExpr"); 
+  }
+
+  virtual unsigned computeHash();
+  
+  static ref<ConstantExpr> fromMemory(void *address, Width w);
+  void toMemory(void *address);
+
+  static ref<ConstantExpr> alloc(uint64_t v, Width w) {
+    // constructs an "optimized" ConstantExpr
+    return ref<ConstantExpr>(v, w);
+  }
+  
+  static ref<ConstantExpr> create(uint64_t v, Width w) {
+    assert(v == bits64::truncateToNBits(v, w) &&
+           "invalid constant");
+    return alloc(v, w);
+  }
+};
+
+  
+// Utility classes
+
+class BinaryExpr : public Expr {
+public:
+  ref<Expr> left, right;
+
+public:
+  unsigned getNumKids() const { return 2; }
+  ref<Expr> getKid(unsigned i) const { 
+    if(i == 0)
+      return left;
+    if(i == 1)
+      return right;
+    return 0;
+  }
+ 
+protected:
+  BinaryExpr(const ref<Expr> &l, const ref<Expr> &r) : left(l), right(r) {}
+};
+
+
+class CmpExpr : public BinaryExpr {
+
+protected:
+  CmpExpr(ref<Expr> l, ref<Expr> r) : BinaryExpr(l,r) {}
+  
+public:                                                       
+  Width getWidth() const { return Bool; }
+};
+
+// Special
+
+class NotOptimizedExpr : public Expr {
+public:
+  static const Kind kind = NotOptimized;
+  static const unsigned numKids = 1;
+  ref<Expr> src;
+
+  static ref<Expr> alloc(const ref<Expr> &src) {
+    ref<Expr> r(new NotOptimizedExpr(src));
+    r.computeHash();
+    return r;
+  }
+  
+  static ref<Expr> create(ref<Expr> src);
+  
+  Width getWidth() const { return src.getWidth(); }
+  Kind getKind() const { return NotOptimized; }
+
+  unsigned getNumKids() const { return 1; }
+  ref<Expr> getKid(unsigned i) const { return src; }
+
+  virtual ref<Expr> rebuild(ref<Expr> kids[]) const { return create(kids[0]); }
+
+private:
+  NotOptimizedExpr(const ref<Expr> &_src) : src(_src) {}
+};
+
+
+/// Class representing a byte update of an array.
+class UpdateNode {
+  friend class UpdateList;
+  friend class STPBuilder; // for setting STPArray
+
+  mutable unsigned refCount;
+  // gross
+  mutable void *stpArray;
+  // cache instead of recalc
+  unsigned hashValue;
+
+public:
+  const UpdateNode *next;
+  ref<Expr> index, value;
+  
+private:
+  /// size of this update sequence, including this update
+  unsigned size;
+  
+public:
+  UpdateNode(const UpdateNode *_next, 
+             const ref<Expr> &_index, 
+             const ref<Expr> &_value);
+
+  unsigned getSize() const { return size; }
+
+  int compare(const UpdateNode &b) const;  
+  unsigned hash() const { return hashValue; }
+
+private:
+  UpdateNode() : refCount(0), stpArray(0) {}
+  ~UpdateNode();
+
+  unsigned computeHash();
+};
+
+class Array {
+public:
+  const MemoryObject *object;
+  unsigned id;
+  unsigned size;
+
+  // FIXME: This does not belong here.
+  mutable void *stpInitialArray;
+
+public:
+  // NOTE: id's ***MUST*** be unique to ensure sanity w.r.t. STP,
+  // which hashes different arrays with the same id to the same
+  // object! We should probably use the pointer for talking to STP, as
+  // long as we can guarantee that it won't be a "stale" reference
+  // once we have freed it.
+  Array(const MemoryObject *_object, unsigned _id, uint64_t _size) 
+    : object(_object), id(_id), size(_size), stpInitialArray(0) {}
+  ~Array() {
+    // FIXME: This relies on caller to delete the STP array.
+    assert(!stpInitialArray && "Array must be deleted by caller!");
+  }
+};
+
+/// Class representing a complete list of updates into an array. 
+/** The main trick is the isRooted bit, which enables important optimizations. 
+    ...
+ */
+class UpdateList { 
+  friend class ReadExpr; // for default constructor
+
+public:
+  const Array *root;
+  
+  /// pointer to the most recent update node
+  const UpdateNode *head;
+  
+  // shouldn't this be part of the ReadExpr? 
+  bool isRooted;
+
+public:
+  UpdateList(const Array *_root, bool isRooted, const UpdateNode *_head);
+  UpdateList(const UpdateList &b);
+  ~UpdateList();
+  
+  UpdateList &operator=(const UpdateList &b);
+
+  /// size of this update list
+  unsigned getSize() const { return (head ? head->getSize() : 0); }
+  
+  void extend(const ref<Expr> &index, const ref<Expr> &value);
+
+  int compare(const UpdateList &b) const;
+  unsigned hash() const;
+};
+
+/// Class representing a one byte read from an array. 
+class ReadExpr : public Expr {
+public:
+  static const Kind kind = Read;
+  static const unsigned numKids = 1;
+  
+public:
+  UpdateList updates;
+  ref<Expr> index;
+
+public:
+  static ref<Expr> alloc(const UpdateList &updates, const ref<Expr> &index) {
+    ref<Expr> r(new ReadExpr(updates, index));
+    r.computeHash();
+    return r;
+  }
+  
+  static ref<Expr> create(const UpdateList &updates, ref<Expr> i);
+  
+  Width getWidth() const { return Expr::Int8; }
+  Kind getKind() const { return Read; }
+  
+  unsigned getNumKids() const { return numKids; }
+  ref<Expr> getKid(unsigned i) const { return !i ? index : 0; }  
+  
+  int compareContents(const Expr &b) const;
+
+  virtual ref<Expr> rebuild(ref<Expr> kids[]) const { 
+    return create(updates, kids[0]);
+  }
+
+  virtual unsigned computeHash();
+
+private:
+  ReadExpr(const UpdateList &_updates, const ref<Expr> &_index) : 
+    updates(_updates), index(_index) {}
+};
+
+
+/// Class representing an if-then-else expression.
+class SelectExpr : public Expr {
+public:
+  static const Kind kind = Select;
+  static const unsigned numKids = 3;
+  
+public:
+  ref<Expr> cond, trueExpr, falseExpr;
+
+public:
+  static ref<Expr> alloc(const ref<Expr> &c, const ref<Expr> &t, const ref<Expr> &f) {
+    ref<Expr> r(new SelectExpr(c, t, f));
+    r.computeHash();
+    return r;
+  }
+  
+  static ref<Expr> create(ref<Expr> c, ref<Expr> t, ref<Expr> f);
+
+  Width getWidth() const { return trueExpr.getWidth(); }
+  Kind getKind() const { return Select; }
+
+  unsigned getNumKids() const { return numKids; }
+  ref<Expr> getKid(unsigned i) const { 
+        switch(i) {
+        case 0: return cond;
+        case 1: return trueExpr;
+        case 2: return falseExpr;
+        default: return 0;
+        }
+   }
+
+  static bool isValidKidWidth(unsigned kid, Width w) {
+    if (kid == 0)
+      return w == Bool;
+    else
+      return true;
+  }
+    
+  virtual ref<Expr> rebuild(ref<Expr> kids[]) const { 
+    return create(kids[0], kids[1], kids[2]);
+  }
+
+private:
+  SelectExpr(const ref<Expr> &c, const ref<Expr> &t, const ref<Expr> &f) 
+    : cond(c), trueExpr(t), falseExpr(f) {}
+};
+
+
+/** Children of a concat expression can have arbitrary widths.  
+    Kid 0 is the left kid, kid 1 is the right kid.
+*/
+class ConcatExpr : public Expr { 
+public: 
+  static const Kind kind = Concat;
+  static const unsigned numKids = 2;
+
+private:
+  Width width;
+  ref<Expr> left, right;  
+
+public:
+  static ref<Expr> alloc(const ref<Expr> &l, const ref<Expr> &r) {
+    ref<Expr> c(new ConcatExpr(l, r));
+    c.computeHash();
+    return c;
+  }
+  
+  static ref<Expr> create(const ref<Expr> &l, const ref<Expr> &r);
+
+  Width getWidth() const { return width; }
+  Kind getKind() const { return kind; }
+  ref<Expr> getLeft() const { return left; }
+  ref<Expr> getRight() const { return right; }
+
+  unsigned getNumKids() const { return numKids; }
+  ref<Expr> getKid(unsigned i) const { 
+    if (i == 0) return left; 
+    else if (i == 1) return right;
+    else return NULL;
+  }
+
+  /// Shortcuts to create larger concats.  The chain returned is unbalanced to the right
+  static ref<Expr> createN(unsigned nKids, const ref<Expr> kids[]);
+  static ref<Expr> create4(const ref<Expr> &kid1, const ref<Expr> &kid2,
+			   const ref<Expr> &kid3, const ref<Expr> &kid4);
+  static ref<Expr> create8(const ref<Expr> &kid1, const ref<Expr> &kid2,
+			   const ref<Expr> &kid3, const ref<Expr> &kid4,
+			   const ref<Expr> &kid5, const ref<Expr> &kid6,
+			   const ref<Expr> &kid7, const ref<Expr> &kid8);
+  
+  virtual ref<Expr> rebuild(ref<Expr> kids[]) const { return create(kids[0], kids[1]); }
+
+
+  /* These will be eliminated */
+  bool is2ByteConcat() const { return false; }
+  bool is4ByteConcat() const { return false; }
+  bool is8ByteConcat() const { return false; }
+  
+private:
+  ConcatExpr(const ref<Expr> &l, const ref<Expr> &r) : left(l), right(r) {
+    width = l.getWidth() + r.getWidth();
+  }
+};
+
+
+/** This class represents an extract from expression {\tt expr}, at
+    bit offset {\tt offset} of width {\tt width}.  Bit 0 is the right most 
+    bit of the expression.
+ */
+class ExtractExpr : public Expr { 
+public:
+  static const Kind kind = Extract;
+  static const unsigned numKids = 1;
+  
+public:
+  ref<Expr> expr;
+  unsigned offset;
+  Width width;
+
+public:  
+  static ref<Expr> alloc(const ref<Expr> &e, unsigned o, Width w) {
+    ref<Expr> r(new ExtractExpr(e, o, w));
+    r.computeHash();
+    return r;
+  }
+  
+  /// Creates an ExtractExpr with the given bit offset and width
+  static ref<Expr> create(ref<Expr> e, unsigned bitOff, Width w);
+
+  /// Creates an ExtractExpr with the given byte offset and width
+  static ref<Expr> createByteOff(ref<Expr> e, unsigned byteOff, Width w=Expr::Int8);
+
+  Width getWidth() const { return width; }
+  Kind getKind() const { return Extract; }
+
+  unsigned getNumKids() const { return numKids; }
+  ref<Expr> getKid(unsigned i) const { return expr; }
+
+  int compareContents(const Expr &b) const {
+    const ExtractExpr &eb = static_cast<const ExtractExpr&>(b);
+    if (offset != eb.offset) return offset < eb.offset ? -1 : 1;
+    if (width != eb.width) return width < eb.width ? -1 : 1;
+    return 0;
+  }
+
+  virtual ref<Expr> rebuild(ref<Expr> kids[]) const { 
+    return create(kids[0], offset, width);
+  }
+
+  virtual unsigned computeHash();
+
+private:
+  ExtractExpr(const ref<Expr> &e, unsigned b, Width w) 
+    : expr(e),offset(b),width(w) {}
+};
+
+
+// Casting
+
+class CastExpr : public Expr {
+public:
+  ref<Expr> src;
+  Width width;
+
+public:
+  CastExpr(const ref<Expr> &e, Width w) : src(e), width(w) {}
+
+  Width getWidth() const { return width; }
+
+  unsigned getNumKids() const { return 1; }
+  ref<Expr> getKid(unsigned i) const { return (i==0) ? src : 0; }
+  
+  static bool needsResultType() { return true; }
+  
+  int compareContents(const Expr &b) const {
+    const CastExpr &eb = static_cast<const CastExpr&>(b);
+    if (width != eb.width) return width < eb.width ? -1 : 1;
+    return 0;
+  }
+
+  virtual unsigned computeHash();
+};
+
+#define CAST_EXPR_CLASS(_class_kind)                        \
+class _class_kind ## Expr : public CastExpr {               \
+public:                                                     \
+  static const Kind kind = _class_kind;                     \
+  static const unsigned numKids = 1;                        \
+public:                                                     \
+    _class_kind ## Expr(ref<Expr> e, Width w) : CastExpr(e,w) {} \
+    static ref<Expr> alloc(const ref<Expr> &e, Width w) {                   \
+      ref<Expr> r(new _class_kind ## Expr(e, w));                     \
+      r.computeHash();                                                    \
+      return r;                                                       \
+    }                                                       \
+    static ref<Expr> create(const ref<Expr> &e, Width w);                   \
+    Kind getKind() const { return _class_kind; }            \
+    virtual ref<Expr> rebuild(ref<Expr> kids[]) const { \
+      return create(kids[0], width); \
+    } \
+};                                                          \
+
+CAST_EXPR_CLASS(SExt)
+CAST_EXPR_CLASS(ZExt)
+
+// Arithmetic/Bit Exprs
+
+#define ARITHMETIC_EXPR_CLASS(_class_kind)                      \
+class _class_kind ## Expr : public BinaryExpr {                 \
+public:                                                         \
+  static const Kind kind = _class_kind;                         \
+  static const unsigned numKids = 2;                            \
+public:                                                         \
+    _class_kind ## Expr(const ref<Expr> &l, const ref<Expr> &r) : BinaryExpr(l,r) {}  \
+    static ref<Expr> alloc(const ref<Expr> &l, const ref<Expr> &r) {          \
+      ref<Expr> res(new _class_kind ## Expr (l, r));                      \
+      res.computeHash();                                                      \
+      return res;                                                         \
+    }                                                           \
+    static ref<Expr> create(const ref<Expr> &l, const ref<Expr> &r);                      \
+    Width getWidth() const { return left.getWidth(); }            \
+    Kind getKind() const { return _class_kind; }                \
+    virtual ref<Expr> rebuild(ref<Expr> kids[]) const { \
+      return create(kids[0], kids[1]); \
+    } \
+};                                                              \
+
+ARITHMETIC_EXPR_CLASS(Add)
+ARITHMETIC_EXPR_CLASS(Sub)
+ARITHMETIC_EXPR_CLASS(Mul)
+ARITHMETIC_EXPR_CLASS(UDiv)
+ARITHMETIC_EXPR_CLASS(SDiv)
+ARITHMETIC_EXPR_CLASS(URem)
+ARITHMETIC_EXPR_CLASS(SRem)
+ARITHMETIC_EXPR_CLASS(And)
+ARITHMETIC_EXPR_CLASS(Or)
+ARITHMETIC_EXPR_CLASS(Xor)
+ARITHMETIC_EXPR_CLASS(Shl)
+ARITHMETIC_EXPR_CLASS(LShr)
+ARITHMETIC_EXPR_CLASS(AShr)
+
+// Comparison Exprs
+
+#define COMPARISON_EXPR_CLASS(_class_kind)                  \
+class _class_kind ## Expr : public CmpExpr {                \
+public:                                                     \
+  static const Kind kind = _class_kind;                     \
+  static const unsigned numKids = 2;                        \
+public:                                                     \
+    _class_kind ## Expr(const ref<Expr> &l, const ref<Expr> &r) : CmpExpr(l,r) {} \
+    static ref<Expr> alloc(const ref<Expr> &l, const ref<Expr> &r) {                  \
+      ref<Expr> res(new _class_kind ## Expr (l, r));                    \
+      res.computeHash();                                                    \
+      return res;                                                       \
+    }                                                       \
+    static ref<Expr> create(const ref<Expr> &l, const ref<Expr> &r);                  \
+    Kind getKind() const { return _class_kind; }            \
+    virtual ref<Expr> rebuild(ref<Expr> kids[]) const { \
+      return create(kids[0], kids[1]); \
+    } \
+};                                                          \
+
+COMPARISON_EXPR_CLASS(Eq)
+COMPARISON_EXPR_CLASS(Ne)
+COMPARISON_EXPR_CLASS(Ult)
+COMPARISON_EXPR_CLASS(Ule)
+COMPARISON_EXPR_CLASS(Ugt)
+COMPARISON_EXPR_CLASS(Uge)
+COMPARISON_EXPR_CLASS(Slt)
+COMPARISON_EXPR_CLASS(Sle)
+COMPARISON_EXPR_CLASS(Sgt)
+COMPARISON_EXPR_CLASS(Sge)
+
+} // End klee namespace
+
+#endif
diff --git a/include/klee/IncompleteSolver.h b/include/klee/IncompleteSolver.h
new file mode 100644
index 00000000..f72607b5
--- /dev/null
+++ b/include/klee/IncompleteSolver.h
@@ -0,0 +1,108 @@
+//===-- IncompleteSolver.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_INCOMPLETESOLVER_H
+#define KLEE_INCOMPLETESOLVER_H
+
+#include "klee/Solver.h"
+#include "klee/SolverImpl.h"
+
+namespace klee {
+
+/// IncompleteSolver - Base class for incomplete solver
+/// implementations.
+///
+/// Incomplete solvers are useful for implementing optimizations which
+/// may quickly compute an answer, but cannot always compute the
+/// correct answer. They can be used with the StagedSolver to provide
+/// a complete Solver implementation.
+class IncompleteSolver {
+public:
+  /// PartialValidity - Represent a possibility incomplete query
+  /// validity.
+  enum PartialValidity {
+    /// The query is provably true.
+    MustBeTrue = 1,
+
+    /// The query is provably false.
+    MustBeFalse = -1,
+
+    /// The query is not provably false (a true assignment is known to
+    /// exist).
+    MayBeTrue = 2,
+
+    /// The query is not provably true (a false assignment is known to
+    /// exist).
+    MayBeFalse = -2,
+
+    /// The query is known to have both true and false assignments.
+    TrueOrFalse = 0,
+
+    /// The validity of the query is unknown.
+    None = 3
+  };
+
+  static PartialValidity negatePartialValidity(PartialValidity pv);
+
+public:
+  IncompleteSolver() {};
+  virtual ~IncompleteSolver() {};
+
+  /// computeValidity - Compute a partial validity for the given query.
+  ///
+  /// The passed expression is non-constant with bool type.
+  ///
+  /// The IncompleteSolver class provides an implementation of
+  /// computeValidity using computeTruth. Sub-classes may override
+  /// this if a more efficient implementation is available.
+  virtual IncompleteSolver::PartialValidity computeValidity(const Query&);
+
+  /// computeValidity - Compute a partial validity for the given query.
+  ///
+  /// The passed expression is non-constant with bool type.
+  virtual IncompleteSolver::PartialValidity computeTruth(const Query&) = 0;
+  
+  /// computeValue - Attempt to compute a value for the given expression.
+  virtual bool computeValue(const Query&, ref<Expr> &result) = 0;
+
+  /// computeInitialValues - Attempt to compute the constant values
+  /// for the initial state of each given object. If a correct result
+  /// is not found, then the values array must be unmodified.
+  virtual bool computeInitialValues(const Query&,
+                                    const std::vector<const Array*> 
+                                      &objects,
+                                    std::vector< std::vector<unsigned char> > 
+                                      &values,
+                                    bool &hasSolution) = 0;
+};
+
+/// StagedSolver - Adapter class for staging an incomplete solver with
+/// a complete secondary solver, to form an (optimized) complete
+/// solver.
+class StagedSolverImpl : public SolverImpl {
+private:
+  IncompleteSolver *primary;
+  Solver *secondary;
+  
+public:
+  StagedSolverImpl(IncompleteSolver *_primary, Solver *_secondary);
+  ~StagedSolverImpl();
+    
+  bool computeTruth(const Query&, bool &isValid);
+  bool computeValidity(const Query&, Solver::Validity &result);
+  bool computeValue(const Query&, ref<Expr> &result);
+  bool computeInitialValues(const Query&,
+                            const std::vector<const Array*> &objects,
+                            std::vector< std::vector<unsigned char> > &values,
+                            bool &hasSolution);
+};
+
+}
+
+#endif
diff --git a/include/klee/Internal/ADT/BOut.h b/include/klee/Internal/ADT/BOut.h
new file mode 100644
index 00000000..14aeb714
--- /dev/null
+++ b/include/klee/Internal/ADT/BOut.h
@@ -0,0 +1,62 @@
+//===-- BOut.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 __COMMON_BOUT_H__
+#define __COMMON_BOUT_H__
+
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+  typedef struct BOutObject BOutObject;
+  struct BOutObject {
+    char *name;
+    unsigned numBytes;
+    unsigned char *bytes;
+  };
+  
+  typedef struct BOut BOut;
+  struct BOut {
+    /* file format version */
+    unsigned version; 
+    
+    unsigned numArgs;
+    char **args;
+
+    unsigned symArgvs;
+    unsigned symArgvLen;
+
+    unsigned numObjects;
+    BOutObject *objects;
+  };
+
+  
+  /* returns the current .bout file format version */
+  unsigned bOut_getCurrentVersion();
+  
+  /* return true iff file at path matches BOut header */
+  int   bOut_isBOutFile(const char *path);
+
+  /* returns NULL on (unspecified) error */
+  BOut* bOut_fromFile(const char *path);
+
+  /* returns 1 on success, 0 on (unspecified) error */
+  int   bOut_toFile(BOut *, const char *path);
+  
+  /* returns total number of object bytes */
+  unsigned bOut_numBytes(BOut *);
+
+  void  bOut_free(BOut *);
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
diff --git a/include/klee/Internal/ADT/DiscretePDF.h b/include/klee/Internal/ADT/DiscretePDF.h
new file mode 100644
index 00000000..bda851fa
--- /dev/null
+++ b/include/klee/Internal/ADT/DiscretePDF.h
@@ -0,0 +1,47 @@
+//===-- DiscretePDF.h -------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+namespace klee {
+  template <class T>
+  class DiscretePDF {
+    // not perfectly parameterized, but float/double/int should work ok,
+    // although it would be better to have choose argument range from 0
+    // to queryable max.
+    typedef double weight_type;
+
+  public:
+    DiscretePDF();
+    ~DiscretePDF();
+
+    bool empty() const;
+    void insert(T item, weight_type weight);
+    void update(T item, weight_type newWeight);
+    void remove(T item);
+    bool inTree(T item);
+    weight_type getWeight(T item);
+	
+    /* pick a tree element according to its
+     * weight. p should be in [0,1).
+     */
+    T choose(double p);
+    
+  private:
+    class Node;
+    Node *m_root;
+    
+    Node **lookup(T item, Node **parent_out);
+    void split(Node *node);
+    void rotate(Node *node);
+    void lengthen(Node *node);
+    void propogateSumsUp(Node *n);
+  };
+
+}
+
+#include "DiscretePDF.inc"
diff --git a/include/klee/Internal/ADT/DiscretePDF.inc b/include/klee/Internal/ADT/DiscretePDF.inc
new file mode 100644
index 00000000..1eb23629
--- /dev/null
+++ b/include/klee/Internal/ADT/DiscretePDF.inc
@@ -0,0 +1,342 @@
+//===- DiscretePDF.inc - --*- C++ -*-===//
+
+//
+
+namespace klee {
+
+template <class T>
+class DiscretePDF<T>::Node
+{
+private:
+  bool m_mark;
+
+public:
+  Node *parent, *left, *right;
+  T key;
+  weight_type weight, sumWeights;
+
+public:
+  Node(T key_, weight_type weight_, Node *parent_);
+  ~Node();
+
+  Node *sibling() { return this==parent->left?parent->right:parent->left; }
+
+  void markRed() { m_mark = true; }
+  void markBlack() { m_mark = false; }
+  bool isBlack() { return !m_mark; }
+  bool leftIsBlack() { return !left || left->isBlack(); }
+  bool rightIsBlack() { return !right || right->isBlack(); }
+  void setSum() { 
+    sumWeights = weight;
+    if (left) sumWeights += left->sumWeights;
+    if (right) sumWeights += right->sumWeights;
+  }
+};
+
+  ///
+
+template <class T>
+DiscretePDF<T>::Node::Node(T key_, weight_type weight_, Node *parent_) {
+  m_mark = false;
+
+  key = key_;
+  weight = weight_;
+  sumWeights = 0;
+  left = right = 0;
+  parent = parent_;
+}
+
+template <class T>
+DiscretePDF<T>::Node::~Node() {
+  if (left) delete left;
+  if (right) delete right;
+}
+
+//
+
+template <class T>
+DiscretePDF<T>::DiscretePDF() {
+  m_root = 0;
+}
+
+template <class T>
+DiscretePDF<T>::~DiscretePDF() {
+  if (m_root) delete m_root;
+}
+
+template <class T>
+bool DiscretePDF<T>::empty() const {
+  return m_root == 0;
+}
+
+template <class T>
+void DiscretePDF<T>::insert(T item, weight_type weight) {
+  Node *p=0, *n=m_root;
+
+  while (n) {
+    if (!n->leftIsBlack() && !n->rightIsBlack())
+      split(n);
+
+    p = n;
+    if (n->key==item) {
+      assert(0 && "insert: argument(item) already in tree");
+    } else {
+      n = (item<n->key)?n->left:n->right;
+    }
+  }
+
+  n = new Node(item, weight, p);
+
+  if (!p) {
+    m_root = n;
+  } else {
+    if (item<p->key) {
+      p->left = n;
+    } else {
+      p->right = n;
+    }
+
+    split(n);
+  }
+
+  propogateSumsUp(n);
+}
+
+template <class T>
+void DiscretePDF<T>::remove(T item) {
+  Node **np = lookup(item, 0);
+  Node *child, *n = *np;
+
+  if (!n) {
+    assert(0 && "remove: argument(item) not in tree");
+  } else {
+    if (n->left) {
+      Node **leftMaxp = &n->left;
+
+      while ((*leftMaxp)->right)
+        leftMaxp = &(*leftMaxp)->right;
+
+      n->key = (*leftMaxp)->key;
+      n->weight = (*leftMaxp)->weight;
+
+      np = leftMaxp;
+      n = *np;
+    }
+
+    // node now has at most one child
+
+    child = n->left?n->left:n->right;
+    *np = child;
+
+    if (child) {
+      child->parent = n->parent;
+
+      if (n->isBlack()) {
+        lengthen(child);
+      }
+    }
+
+    propogateSumsUp(n->parent);
+
+    n->left = n->right = 0;
+    delete n;
+  }
+}
+
+template <class T>
+void DiscretePDF<T>::update(T item, weight_type weight) {
+  Node *n = *lookup(item, 0);
+
+  if (!n) {
+    assert(0 && "update: argument(item) not in tree");
+  } else {
+    n->weight = weight;
+    propogateSumsUp(n);
+  }
+}
+
+template <class T>
+T DiscretePDF<T>::choose(double p) {
+  if (p<0.0 || p>=1.0) {
+    assert(0 && "choose: argument(p) outside valid range");
+  } else if (!m_root) {
+    assert(0 && "choose: choose() called on empty tree");
+  } else {
+    weight_type w = (weight_type) (m_root->sumWeights * p);
+    Node *n = m_root;
+
+    while (1) {
+      if (n->left) {
+        if (w<n->left->sumWeights) {
+          n = n->left;
+          continue;
+        } else {
+          w -= n->left->sumWeights;
+        }
+      }
+      if (w<n->weight || !n->right) {
+        break; // !n->right condition shouldn't be necessary, just sanity check
+      }
+      w -= n->weight;
+      n = n->right;
+    }
+
+    return n->key;
+  }
+}
+
+template <class T>
+bool DiscretePDF<T>::inTree(T item) {
+  Node *n = *lookup(item, 0);
+
+  return !!n;
+}
+
+template <class T>
+typename DiscretePDF<T>::weight_type DiscretePDF<T>::getWeight(T item) {
+  Node *n = *lookup(item, 0);
+  assert(n);
+  return n->weight;
+}
+
+//
+
+template <class T>
+typename DiscretePDF<T>::Node **
+DiscretePDF<T>::lookup(T item, Node **parent_out) {
+  Node *n, *p=0, **np=&m_root;
+
+  while ((n = *np)) {
+    if (n->key==item) {
+      break;
+    } else {
+      p = n;
+      if (item<n->key) {
+        np = &n->left;
+      } else {
+        np = &n->right;
+      }
+    }
+  }
+
+  if (parent_out)
+    *parent_out = p;
+  return np;
+}
+
+template <class T>
+void DiscretePDF<T>::split(Node *n) {
+  if (n->left) n->left->markBlack();
+  if (n->right) n->right->markBlack();
+
+  if (n->parent) {
+    Node *p = n->parent;
+
+    n->markRed();
+
+    if (!p->isBlack()) {
+      p->parent->markRed();
+
+      // not same direction
+      if (!((n==p->left && p==p->parent->left) || 
+            (n==p->right && p==p->parent->right))) {
+        rotate(n);
+        p = n;
+      }
+
+      rotate(p);
+      p->markBlack();
+    }
+  }
+}
+
+template <class T>
+void DiscretePDF<T>::rotate(Node *n) {
+  Node *p=n->parent, *pp=p->parent;
+
+  n->parent = pp;
+  p->parent = n;
+
+  if (n==p->left) {
+    p->left = n->right;
+    n->right = p;
+    if (p->left) p->left->parent = p;
+  } else {
+    p->right = n->left;
+    n->left = p;
+    if (p->right) p->right->parent = p;
+  }
+
+  n->setSum();
+  p->setSum();
+	
+  if (!pp) {
+    m_root = n;
+  } else {
+    if (p==pp->left) {
+      pp->left = n;
+    } else {
+      pp->right = n;
+    }
+  }
+}
+
+template <class T>
+void DiscretePDF<T>::lengthen(Node *n) {
+  if (!n->isBlack()) {
+    n->markBlack();
+  } else if (n->parent) {
+    Node *sibling = n->sibling();
+
+    if (sibling && !sibling->isBlack()) {
+      n->parent->markRed();
+      sibling->markBlack();
+
+      rotate(sibling); // node sibling is now old sibling child, must be black
+      sibling = n->sibling();
+    }
+
+    // sibling is black
+
+    if (!sibling) {
+      lengthen(n->parent);
+    } else if (sibling->leftIsBlack() && sibling->rightIsBlack()) {
+      if (n->parent->isBlack()) {
+        sibling->markRed();
+        lengthen(n->parent);
+      } else {
+        sibling->markRed();
+        n->parent->markBlack();
+      }
+    } else {
+      if (n==n->parent->left && sibling->rightIsBlack()) {
+        rotate(sibling->left); // sibling->left must be red
+        sibling->markRed();
+        sibling->parent->markBlack();
+        sibling = sibling->parent;
+      } else if (n==n->parent->right && sibling->leftIsBlack()) {
+        rotate(sibling->right); // sibling->right must be red
+        sibling->markRed();
+        sibling->parent->markBlack();
+        sibling = sibling->parent;
+      }
+
+      // sibling is black, and sibling's far child is red
+
+      rotate(sibling);
+      if (!n->parent->isBlack()) 
+        sibling->markRed();
+      sibling->left->markBlack();
+      sibling->right->markBlack();
+    }
+  }
+}
+
+template <class T>
+void DiscretePDF<T>::propogateSumsUp(Node *n) {
+  for (; n; n=n->parent)
+    n->setSum();
+}
+
+}
+
diff --git a/include/klee/Internal/ADT/ImmutableMap.h b/include/klee/Internal/ADT/ImmutableMap.h
new file mode 100644
index 00000000..c7af3786
--- /dev/null
+++ b/include/klee/Internal/ADT/ImmutableMap.h
@@ -0,0 +1,104 @@
+//===-- ImmutableMap.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 __UTIL_IMMUTABLEMAP_H__
+#define __UTIL_IMMUTABLEMAP_H__
+
+#include <functional>
+
+#include "ImmutableTree.h"
+
+namespace klee {
+  template<class V, class D>
+  struct _Select1st {
+    D &operator()(V &a) const { return a.first; }
+    const D &operator()(const V &a) const { return a.first; }
+  };
+  
+  template<class K, class D, class CMP=std::less<K> >
+  class ImmutableMap {
+  public:
+    typedef K key_type;
+    typedef std::pair<K,D> value_type;
+
+    typedef ImmutableTree<K, value_type, _Select1st<value_type,key_type>, CMP> Tree;
+    typedef typename Tree::iterator iterator;
+
+  private:
+    Tree elts;
+
+    ImmutableMap(const Tree &b): elts(b) {}
+
+  public:
+    ImmutableMap() {}
+    ImmutableMap(const ImmutableMap &b) : elts(b.elts) {}
+    ~ImmutableMap() {}
+
+    ImmutableMap &operator=(const ImmutableMap &b) { elts = b.elts; return *this; }
+    
+    bool empty() const { 
+      return elts.empty(); 
+    }
+    unsigned count(const key_type &key) const { 
+      return elts.count(key); 
+    }
+    const value_type *lookup(const key_type &key) const { 
+      return elts.lookup(key); 
+    }
+    const value_type *lookup_previous(const key_type &key) const { 
+      return elts.lookup_previous(key); 
+    }
+    const value_type &min() const { 
+      return elts.min(); 
+    }
+    const value_type &max() const { 
+      return elts.max(); 
+    }
+    unsigned size() const { 
+      return elts.size(); 
+    }
+
+    ImmutableMap insert(const value_type &value) const { 
+      return elts.insert(value); 
+    }
+    ImmutableMap replace(const value_type &value) const { 
+      return elts.replace(value); 
+    }
+    ImmutableMap remove(const key_type &key) const { 
+      return elts.remove(key); 
+    }
+    ImmutableMap popMin(const value_type &valueOut) const { 
+      return elts.popMin(valueOut); 
+    }
+    ImmutableMap popMax(const value_type &valueOut) const { 
+      return elts.popMax(valueOut); 
+    }
+
+    iterator begin() const { 
+      return elts.begin(); 
+    }
+    iterator end() const { 
+      return elts.end(); 
+    }
+    iterator find(const key_type &key) const { 
+      return elts.find(key); 
+    }
+    iterator lower_bound(const key_type &key) const { 
+      return elts.lower_bound(key); 
+    }
+    iterator upper_bound(const key_type &key) const { 
+      return elts.upper_bound(key); 
+    }
+
+    static unsigned getAllocated() { return Tree::allocated; }
+  };
+
+}
+
+#endif
diff --git a/include/klee/Internal/ADT/ImmutableSet.h b/include/klee/Internal/ADT/ImmutableSet.h
new file mode 100644
index 00000000..0c79eb9c
--- /dev/null
+++ b/include/klee/Internal/ADT/ImmutableSet.h
@@ -0,0 +1,101 @@
+//===-- ImmutableSet.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 __UTIL_IMMUTABLESET_H__
+#define __UTIL_IMMUTABLESET_H__
+
+#include <functional>
+
+#include "ImmutableTree.h"
+
+namespace klee {
+  template<class T>
+  struct _Identity {
+    T &operator()(T &a) const { return a; }
+    const T &operator()(const T &a) const { return a; }
+  };
+  
+  template<class T, class CMP=std::less<T> >
+  class ImmutableSet {
+  public:
+    typedef T key_type;
+    typedef T value_type;
+
+    typedef ImmutableTree<T, T, _Identity<T>, CMP> Tree;
+    typedef typename Tree::iterator iterator;
+
+  private:
+    Tree elts;
+
+    ImmutableSet(const Tree &b): elts(b) {}
+
+  public:
+    ImmutableSet() {}
+    ImmutableSet(const ImmutableSet &b) : elts(b.elts) {}
+    ~ImmutableSet() {}
+
+    ImmutableSet &operator=(const ImmutableSet &b) { elts = b.elts; return *this; }
+    
+    bool empty() const { 
+      return elts.empty(); 
+    }
+    unsigned count(const key_type &key) const { 
+      return elts.count(key); 
+    }
+    const value_type *lookup(const key_type &key) const { 
+      return elts.lookup(key); 
+    }
+    const value_type &min() const { 
+      return elts.min(); 
+    }
+    const value_type &max() const { 
+      return elts.max(); 
+    }
+    unsigned size() { 
+      return elts.size(); 
+    }
+
+    ImmutableSet insert(const value_type &value) const {
+      return elts.insert(value); 
+    }
+    ImmutableSet replace(const value_type &value) const {
+      return elts.replace(value); 
+    }
+    ImmutableSet remove(const key_type &key) const { 
+      return elts.remove(key); 
+    }
+    ImmutableSet popMin(const value_type &valueOut) const { 
+      return elts.popMin(valueOut); 
+    }
+    ImmutableSet popMax(const value_type &valueOut) const { 
+      return elts.popMax(valueOut); 
+    }
+
+    iterator begin() const { 
+      return elts.begin(); 
+    }
+    iterator end() const { 
+      return elts.end(); 
+    }
+    iterator find(const key_type &key) const { 
+      return elts.find(key); 
+    }
+    iterator lower_bound(const key_type &key) const { 
+      return elts.lower_bound(key); 
+    }
+    iterator upper_bound(const key_type &key) const { 
+      return elts.upper_bound(key); 
+    }
+
+    static unsigned getAllocated() { return Tree::allocated; }
+  };
+
+}
+
+#endif
diff --git a/include/klee/Internal/ADT/ImmutableTree.h b/include/klee/Internal/ADT/ImmutableTree.h
new file mode 100644
index 00000000..2f294077
--- /dev/null
+++ b/include/klee/Internal/ADT/ImmutableTree.h
@@ -0,0 +1,619 @@
+//===-- ImmutableTree.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 __UTIL_IMMUTABLETREE_H__
+#define __UTIL_IMMUTABLETREE_H__
+
+#include <cassert>
+#include <vector>
+
+namespace klee {
+  template<class K, class V, class KOV, class CMP>
+  class ImmutableTree {
+  public:
+    static unsigned allocated;
+    class iterator;
+
+    typedef K key_type;
+    typedef V value_type;
+    typedef KOV key_of_value;
+    typedef CMP key_compare;
+
+  public:
+    ImmutableTree();
+    ImmutableTree(const ImmutableTree &s);
+    ~ImmutableTree();
+
+    ImmutableTree &operator=(const ImmutableTree &s);
+
+    bool empty() const;
+
+    unsigned count(const key_type &key) const; // always 0 or 1
+    const value_type *lookup(const key_type &key) const;
+
+    // find the last value less than or equal to key, or null if
+    // no such value exists
+    const value_type *lookup_previous(const key_type &key) const;
+
+    const value_type &min() const;
+    const value_type &max() const;
+    unsigned size() const;
+
+    ImmutableTree insert(const value_type &value) const;
+    ImmutableTree replace(const value_type &value) const;
+    ImmutableTree remove(const key_type &key) const;
+    ImmutableTree popMin(value_type &valueOut) const;
+    ImmutableTree popMax(value_type &valueOut) const;
+
+    iterator begin() const;
+    iterator end() const;
+    iterator find(const key_type &key) const;
+    iterator lower_bound(const key_type &key) const;
+    iterator upper_bound(const key_type &key) const;
+
+    static unsigned getAllocated() { return allocated; }
+
+  private:
+    class Node;
+
+    Node *node;
+    ImmutableTree(Node *_node);
+  };
+
+  /***/
+
+  template<class K, class V, class KOV, class CMP>
+  class ImmutableTree<K,V,KOV,CMP>::Node {
+  public:
+    static Node terminator;
+    Node *left, *right;
+    value_type value;
+    unsigned height, references;
+
+  protected:
+    Node(); // solely for creating the terminator node
+    static Node *balance(Node *left, const value_type &value, Node *right);
+
+  public:
+
+    Node(Node *_left, Node *_right, const value_type &_value);
+    ~Node();
+
+    void decref();
+    Node *incref();
+
+    bool isTerminator();
+
+    unsigned size();
+    Node *popMin(value_type &valueOut);
+    Node *popMax(value_type &valueOut);
+    Node *insert(const value_type &v);
+    Node *replace(const value_type &v);
+    Node *remove(const key_type &k);
+  };
+
+  // Should live somewhere else, this is a simple stack with maximum size.
+  template<typename T>
+  class FixedStack {
+    unsigned pos, max;
+    T *elts;
+
+  public:
+    FixedStack(unsigned _max) : pos(0),
+                                max(_max),
+                                elts(new T[max]) {}
+    FixedStack(const FixedStack &b) : pos(b.pos),
+                                      max(b.max),
+                                      elts(new T[b.max]) {
+      std::copy(b.elts, b.elts+pos, elts);
+    }
+    ~FixedStack() { delete[] elts; }
+
+    void push_back(const T &elt) { elts[pos++] = elt; }
+    void pop_back() { --pos; }
+    bool empty() { return pos==0; }
+    T &back() { return elts[pos-1]; }
+
+
+    FixedStack &operator=(const FixedStack &b) {
+      assert(max == b.max); 
+      pos = b.pos;
+      std::copy(b.elts, b.elts+pos, elts);
+      return *this;
+    }
+
+    bool operator==(const FixedStack &b) {
+      return (pos == b.pos &&
+              std::equal(elts, elts+pos, b.elts));
+    }
+    bool operator!=(const FixedStack &b) { return !(*this==b); }
+  };
+
+  template<class K, class V, class KOV, class CMP>
+  class ImmutableTree<K,V,KOV,CMP>::iterator {
+    friend class ImmutableTree<K,V,KOV,CMP>;
+  private:
+    Node *root; // so can back up from end
+    FixedStack<Node*> stack;
+    
+  public:
+    iterator(Node *_root, bool atBeginning) : root(_root->incref()),
+                                              stack(root->height) {
+      if (atBeginning) {
+        for (Node *n=root; !n->isTerminator(); n=n->left)
+          stack.push_back(n);
+      }
+    }
+    iterator(const iterator &i) : root(i.root->incref()),
+                                  stack(i.stack) {
+    }
+    ~iterator() {
+      root->decref();
+    }
+
+    iterator &operator=(const iterator &b) {
+      b.root->incref();
+      root->decref();
+      root = b.root;
+      stack = b.stack;
+      return *this;
+    }
+
+    const value_type &operator*() {
+      Node *n = stack.back();
+      return n->value;
+    }
+
+    const value_type *operator->() {
+      Node *n = stack.back();
+      return &n->value;
+    }
+
+    bool operator==(const iterator &b) {
+      return stack==b.stack;
+    }
+    bool operator!=(const iterator &b) {
+      return stack!=b.stack;
+    }
+    
+    iterator &operator--() {
+      if (stack.empty()) {
+        for (Node *n=root; !n->isTerminator(); n=n->right)
+          stack.push_back(n);
+      } else {
+        Node *n = stack.back();
+        if (n->left->isTerminator()) {
+          for (;;) {
+            Node *prev = n;
+            stack.pop_back();
+            if (stack.empty()) {
+              break;
+            } else {
+              n = stack.back();
+              if (prev==n->right)
+                break;
+            }
+          }
+        } else {
+          stack.push_back(n->left);
+          for (n=n->left->right; !n->isTerminator(); n=n->right)
+            stack.push_back(n);
+        }
+      }
+      return *this;
+    }
+
+    iterator &operator++() {
+      assert(!stack.empty());
+      Node *n = stack.back();
+      if (n->right->isTerminator()) {
+        for (;;) {
+          Node *prev = n;
+          stack.pop_back();
+          if (stack.empty()) {
+            break;
+          } else {
+            n = stack.back();
+            if (prev==n->left)
+              break;
+          }
+        }
+      } else {
+        stack.push_back(n->right);
+        for (n=n->right->left; !n->isTerminator(); n=n->left)
+          stack.push_back(n);
+      }
+      return *this;
+    }
+  };
+
+  /***/
+
+  template<class K, class V, class KOV, class CMP> 
+  typename ImmutableTree<K,V,KOV,CMP>::Node 
+  ImmutableTree<K,V,KOV,CMP>::Node::terminator;
+
+  template<class K, class V, class KOV, class CMP> 
+  unsigned ImmutableTree<K,V,KOV,CMP>::allocated = 0;
+
+  template<class K, class V, class KOV, class CMP>
+  ImmutableTree<K,V,KOV,CMP>::Node::Node() 
+    : left(&terminator), 
+      right(&terminator), 
+      height(0), 
+      references(3) { 
+    assert(this==&terminator);
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  ImmutableTree<K,V,KOV,CMP>::Node::Node(Node *_left, Node *_right, const value_type &_value)
+    : left(_left), 
+      right(_right), 
+      value(_value), 
+      height(std::max(left->height, right->height) + 1),
+      references(1) 
+  {
+    ++allocated;
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  ImmutableTree<K,V,KOV,CMP>::Node::~Node() {
+    left->decref();
+    right->decref();
+    --allocated;
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  inline void ImmutableTree<K,V,KOV,CMP>::Node::decref() {
+    --references;
+    if (references==0) delete this;
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  inline typename ImmutableTree<K,V,KOV,CMP>::Node *ImmutableTree<K,V,KOV,CMP>::Node::incref() {
+    ++references;
+    return this;
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  inline bool ImmutableTree<K,V,KOV,CMP>::Node::isTerminator() {
+    return this==&terminator;
+  }
+
+  /***/
+
+  template<class K, class V, class KOV, class CMP>
+  typename ImmutableTree<K,V,KOV,CMP>::Node *
+  ImmutableTree<K,V,KOV,CMP>::Node::balance(Node *left, const value_type &value, Node *right) {
+    if (left->height > right->height + 2) {
+      Node *ll = left->left;
+      Node *lr = left->right;
+      if (ll->height >= lr->height) {
+        Node *nlr = new Node(lr->incref(), right, value);
+        Node *res = new Node(ll->incref(), nlr, left->value);
+        left->decref();
+        return res;
+      } else {
+        Node *lrl = lr->left;
+        Node *lrr = lr->right;
+        Node *nll = new Node(ll->incref(), lrl->incref(), left->value);
+        Node *nlr = new Node(lrr->incref(), right, value);
+        Node *res = new Node(nll, nlr, lr->value);
+        left->decref();
+        return res;
+      }
+    } else if (right->height > left->height + 2) {
+      Node *rl = right->left;
+      Node *rr = right->right;
+      if (rr->height >= rl->height) {
+        Node *nrl = new Node(left, rl->incref(), value);
+        Node *res = new Node(nrl, rr->incref(), right->value);
+        right->decref();
+        return res;
+      } else {
+        Node *rll = rl->left;
+        Node *rlr = rl->right;
+        Node *nrl = new Node(left, rll->incref(), value);
+        Node *nrr = new Node(rlr->incref(), rr->incref(), right->value);
+        Node *res = new Node(nrl, nrr, rl->value);
+        right->decref();
+        return res;
+      }
+    } else {
+      return new Node(left, right, value);
+    }
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  unsigned ImmutableTree<K,V,KOV,CMP>::Node::size() {
+    if (isTerminator()) {
+      return 0;
+    } else {
+      return left->size() + 1 + right->size();
+    }
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  typename ImmutableTree<K,V,KOV,CMP>::Node *
+  ImmutableTree<K,V,KOV,CMP>::Node::popMin(value_type &valueOut) {
+    if (left->isTerminator()) {
+      valueOut = value;
+      return right->incref();
+    } else {
+      return balance(left->popMin(valueOut), value, right->incref());
+    }
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  typename ImmutableTree<K,V,KOV,CMP>::Node *
+  ImmutableTree<K,V,KOV,CMP>::Node::popMax(value_type &valueOut) {
+    if (right->isTerminator()) {
+      valueOut = value;
+      return left->incref();
+    } else {
+      return balance(left->incref(), value, right->popMax(valueOut));
+    }
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  typename ImmutableTree<K,V,KOV,CMP>::Node *
+  ImmutableTree<K,V,KOV,CMP>::Node::insert(const value_type &v) {
+    if (isTerminator()) {
+      return new Node(terminator.incref(), terminator.incref(), v);
+    } else {
+      if (key_compare()(key_of_value()(v), key_of_value()(value))) {
+        return balance(left->insert(v), value, right->incref());
+      } else if (key_compare()(key_of_value()(value), key_of_value()(v))) {
+        return balance(left->incref(), value, right->insert(v));
+      } else {
+        return incref();
+      }
+    }
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  typename ImmutableTree<K,V,KOV,CMP>::Node *
+  ImmutableTree<K,V,KOV,CMP>::Node::replace(const value_type &v) {
+    if (isTerminator()) {
+      return new Node(terminator.incref(), terminator.incref(), v);
+    } else {
+      if (key_compare()(key_of_value()(v), key_of_value()(value))) {
+        return balance(left->replace(v), value, right->incref());
+      } else if (key_compare()(key_of_value()(value), key_of_value()(v))) {
+        return balance(left->incref(), value, right->replace(v));
+      } else {
+        return new Node(left->incref(), right->incref(), v);
+      }
+    }
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  typename ImmutableTree<K,V,KOV,CMP>::Node *
+  ImmutableTree<K,V,KOV,CMP>::Node::remove(const key_type &k) {
+    if (isTerminator()) {
+      return incref();
+    } else {
+      if (key_compare()(k, key_of_value()(value))) {
+        return balance(left->remove(k), value, right->incref());
+      } else if (key_compare()(key_of_value()(value), k)) {
+        return balance(left->incref(), value, right->remove(k));
+      } else {
+        if (left->isTerminator()) {
+          return right->incref();
+        } else if (right->isTerminator()) {
+          return left->incref();
+        } else {
+          value_type min;
+          Node *nr = right->popMin(min);
+          return balance(left->incref(), min, nr);
+        }
+      }
+    }
+  }
+
+  /***/
+
+  template<class K, class V, class KOV, class CMP>
+  ImmutableTree<K,V,KOV,CMP>::ImmutableTree() 
+    : node(Node::terminator.incref()) {
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  ImmutableTree<K,V,KOV,CMP>::ImmutableTree(Node *_node) 
+    : node(_node) {
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  ImmutableTree<K,V,KOV,CMP>::ImmutableTree(const ImmutableTree &s) 
+    : node(s.node->incref()) {
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  ImmutableTree<K,V,KOV,CMP>::~ImmutableTree() {
+    node->decref(); 
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  ImmutableTree<K,V,KOV,CMP> &ImmutableTree<K,V,KOV,CMP>::operator=(const ImmutableTree &s) {
+    Node *n = s.node->incref();
+    node->decref();
+    node = n;
+    return *this;
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  bool ImmutableTree<K,V,KOV,CMP>::empty() const {
+    return node->isTerminator();
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  unsigned ImmutableTree<K,V,KOV,CMP>::count(const key_type &k) const {
+    Node *n = node;
+    while (!n->isTerminator()) {
+      key_type key = key_of_value()(n->value);
+      if (key_compare()(k, key)) {
+        n = n->left;
+      } else if (key_compare()(key, k)) {
+        n = n->right;
+      } else {
+        return 1;
+      }
+    }
+    return 0;
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  const typename ImmutableTree<K,V,KOV,CMP>::value_type *
+  ImmutableTree<K,V,KOV,CMP>::lookup(const key_type &k) const {
+    Node *n = node;
+    while (!n->isTerminator()) {
+      key_type key = key_of_value()(n->value);
+      if (key_compare()(k, key)) {
+        n = n->left;
+      } else if (key_compare()(key, k)) {
+        n = n->right;
+      } else {
+        return &n->value;
+      }
+    }
+    return 0;
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  const typename ImmutableTree<K,V,KOV,CMP>::value_type *
+  ImmutableTree<K,V,KOV,CMP>::lookup_previous(const key_type &k) const {
+    Node *n = node;
+    Node *result = 0;
+    while (!n->isTerminator()) {
+      key_type key = key_of_value()(n->value);
+      if (key_compare()(k, key)) {
+        n = n->left;
+      } else if (key_compare()(key, k)) {
+        result = n;
+        n = n->right;
+      } else {
+        return &n->value;
+      }
+    }
+    return result ? &result->value : 0;
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  const typename ImmutableTree<K,V,KOV,CMP>::value_type &
+  ImmutableTree<K,V,KOV,CMP>::min() const { 
+    Node *n = node;
+    assert(!n->isTerminator());
+    while (!n->left->isTerminator()) n = n->left;
+    return n->value;
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  const typename ImmutableTree<K,V,KOV,CMP>::value_type &
+  ImmutableTree<K,V,KOV,CMP>::max() const {
+    Node *n = node;
+    assert(!n->isTerminator());
+    while (!n->right->isTerminator()) n = n->right;
+    return n->value;
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  unsigned ImmutableTree<K,V,KOV,CMP>::size() const {
+    return node->size();
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  ImmutableTree<K,V,KOV,CMP> 
+  ImmutableTree<K,V,KOV,CMP>::insert(const value_type &value) const { 
+    return ImmutableTree(node->insert(value)); 
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  ImmutableTree<K,V,KOV,CMP> 
+  ImmutableTree<K,V,KOV,CMP>::replace(const value_type &value) const { 
+    return ImmutableTree(node->replace(value)); 
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  ImmutableTree<K,V,KOV,CMP> 
+  ImmutableTree<K,V,KOV,CMP>::remove(const key_type &key) const { 
+    return ImmutableTree(node->remove(key)); 
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  ImmutableTree<K,V,KOV,CMP> 
+  ImmutableTree<K,V,KOV,CMP>::popMin(value_type &valueOut) const { 
+    return ImmutableTree(node->popMin(valueOut)); 
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  ImmutableTree<K,V,KOV,CMP> 
+  ImmutableTree<K,V,KOV,CMP>::popMax(value_type &valueOut) const { 
+    return ImmutableTree(node->popMax(valueOut)); 
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  inline typename ImmutableTree<K,V,KOV,CMP>::iterator 
+  ImmutableTree<K,V,KOV,CMP>::begin() const {
+    return iterator(node, true);
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  inline typename ImmutableTree<K,V,KOV,CMP>::iterator 
+  ImmutableTree<K,V,KOV,CMP>::end() const {
+    return iterator(node, false);
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  inline typename ImmutableTree<K,V,KOV,CMP>::iterator 
+  ImmutableTree<K,V,KOV,CMP>::find(const key_type &key) const {
+    iterator end(node,false), it = lower_bound(key);
+    if (it==end || key_compare()(key,key_of_value()(*it))) {
+      return end;
+    } else {
+      return it;
+    }
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  inline typename ImmutableTree<K,V,KOV,CMP>::iterator 
+  ImmutableTree<K,V,KOV,CMP>::lower_bound(const key_type &k) const {
+    // XXX ugh this doesn't have to be so ugly does it?
+    iterator it(node,false);
+    for (Node *root=node; !root->isTerminator();) {
+      it.stack.push_back(root);
+      if (key_compare()(k, key_of_value()(root->value))) {
+        root = root->left;
+      } else if (key_compare()(key_of_value()(root->value), k)) {
+        root = root->right;
+      } else {
+        return it;
+      }
+    }
+    // it is now beginning or first element < k
+    if (!it.stack.empty()) {
+      Node *last = it.stack.back();
+      if (key_compare()(key_of_value()(last->value), k))
+        ++it;
+    }
+    return it;
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  typename ImmutableTree<K,V,KOV,CMP>::iterator 
+  ImmutableTree<K,V,KOV,CMP>::upper_bound(const key_type &key) const {
+    iterator end(node,false),it = lower_bound(key);
+    if (it!=end && 
+        !key_compare()(key,key_of_value()(*it))) // no need to loop, no duplicates
+      ++it;
+    return it;
+  }
+
+}
+
+#endif
diff --git a/include/klee/Internal/ADT/MapOfSets.h b/include/klee/Internal/ADT/MapOfSets.h
new file mode 100644
index 00000000..25c5e2b9
--- /dev/null
+++ b/include/klee/Internal/ADT/MapOfSets.h
@@ -0,0 +1,385 @@
+//===-- MapOfSets.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 __UTIL_MAPOFSETS_H__
+#define __UTIL_MAPOFSETS_H__
+
+#include <cassert>
+#include <vector>
+#include <set>
+#include <map>
+
+// This should really be broken down into TreeOfSets on top of which
+// SetOfSets and MapOfSets are easily implemeted. It should also be
+// parameterized on the underlying set type. Neither are hard to do,
+// just not worth it at the moment.
+//
+// I also broke some STLish conventions because I was bored.
+
+namespace klee {
+
+  /** This implements the UBTree data structure (see Hoffmann and
+      Koehler, "A New Method to Index and Query Sets", IJCAI 1999) */
+  template<class K, class V>
+  class MapOfSets {
+  public:
+    class iterator;
+
+  public:
+    MapOfSets();
+
+    void clear();
+
+    void insert(const std::set<K> &set, const V &value);
+
+    V *lookup(const std::set<K> &set);
+
+    iterator begin();
+    iterator end();
+
+    void subsets(const std::set<K> &set, 
+                 std::vector< std::pair<std::set<K>, V> > &resultOut);
+    void supersets(const std::set<K> &set, 
+                   std::vector< std::pair<std::set<K>, V> > &resultOut);
+    
+    template<class Predicate>
+    V *findSuperset(const std::set<K> &set, const Predicate &p);
+    template<class Predicate>
+    V *findSubset(const std::set<K> &set, const Predicate &p);
+
+  private:
+    class Node;
+
+    Node root;
+
+    template<class Iterator, class Vector>
+    void findSubsets(Node *n, 
+                     const std::set<K> &accum,
+                     Iterator begin, 
+                     Iterator end,
+                     Vector &resultsOut);
+    template<class Iterator, class Vector>
+    void findSupersets(Node *n, 
+                       const std::set<K> &accum,
+                       Iterator begin, 
+                       Iterator end,
+                       Vector &resultsOut);
+    template<class Predicate>
+    V *findSuperset(Node *n, 
+                    typename std::set<K>::iterator begin, 
+                    typename std::set<K>::iterator end,
+                    const Predicate &p);
+    template<class Predicate>
+    V *findSubset(Node *n, 
+                  typename std::set<K>::iterator begin, 
+                  typename std::set<K>::iterator end,
+                  const Predicate &p);
+  };
+
+  /***/
+
+  template<class K, class V>
+  class MapOfSets<K,V>::Node {
+    friend class MapOfSets<K,V>;
+    friend class MapOfSets<K,V>::iterator;
+
+  public:
+    typedef std::map<K, Node> children_ty;
+
+    V value;
+
+  private:
+    bool isEndOfSet;
+    std::map<K, Node> children;
+    
+  public:
+    Node() : isEndOfSet(false) {}
+  };
+  
+  template<class K, class V>
+  class MapOfSets<K,V>::iterator {
+    typedef std::vector< typename std::map<K, Node>::iterator > stack_ty;
+    friend class MapOfSets<K,V>;
+  private:
+    Node *root;
+    bool onEntry;
+    stack_ty stack;
+
+    void step() {
+      if (onEntry) {
+        onEntry = false;
+        Node *n = stack.empty() ? root : &stack.back()->second;
+        while (!n->children.empty()) {
+          stack.push_back(n->children.begin());
+          n = &stack.back()->second;
+          if (n->isEndOfSet) {
+            onEntry = true;
+            return;
+          }
+        } 
+      }
+
+      while (!stack.empty()) {
+        unsigned size = stack.size();
+        Node *at = size==1 ? root : &stack[size-2]->second;
+        typename std::map<K,Node>::iterator &cur = stack.back();
+        ++cur;
+        if (cur==at->children.end()) {
+          stack.pop_back();
+        } else {
+          Node *n = &cur->second;
+
+          while (!n->isEndOfSet) {
+            assert(!n->children.empty());
+            stack.push_back(n->children.begin());
+            n = &stack.back()->second;
+          }
+
+          onEntry = true;
+          break;
+        }
+      } 
+    }
+
+  public:
+    // end()
+    iterator() : onEntry(false) {} 
+    // begin()
+    iterator(Node *_n) : root(_n), onEntry(true) {
+      if (!root->isEndOfSet)
+        step();
+    }
+
+    const std::pair<const std::set<K>, const V> operator*() {
+      assert(onEntry || !stack.empty());
+      std::set<K> s;
+      for (typename stack_ty::iterator it = stack.begin(), ie = stack.end();
+           it != ie; ++it)
+        s.insert((*it)->first);
+      Node *n = stack.empty() ? root : &stack.back()->second;
+      return std::make_pair(s, n->value);
+    }
+
+    bool operator==(const iterator &b) {
+      return onEntry==b.onEntry && stack==b.stack;
+    }
+    bool operator!=(const iterator &b) {
+      return !(*this==b);
+    }
+
+    iterator &operator++() {
+      step();
+      return *this;
+    }
+  };
+
+  /***/
+
+  template<class K, class V>
+  MapOfSets<K,V>::MapOfSets() {}  
+
+  template<class K, class V>
+  void MapOfSets<K,V>::insert(const std::set<K> &set, const V &value) {
+    Node *n = &root;
+    for (typename std::set<K>::const_iterator it = set.begin(), ie = set.end();
+         it != ie; ++it)
+      n = &n->children.insert(std::make_pair(*it, Node())).first->second;
+    n->isEndOfSet = true;
+    n->value = value;
+  }
+
+  template<class K, class V>
+  V *MapOfSets<K,V>::lookup(const std::set<K> &set) {
+    Node *n = &root;
+    for (typename std::set<K>::const_iterator it = set.begin(), ie = set.end();
+         it != ie; ++it) {
+      typename Node::children_ty::iterator kit = n->children.find(*it);
+      if (kit==n->children.end()) {
+        return 0;
+      } else {
+        n = &kit->second;
+      }
+    }
+    if (n->isEndOfSet) {
+      return &n->value;
+    } else {
+      return 0;
+    }
+  }
+
+  template<class K, class V>
+  typename MapOfSets<K,V>::iterator 
+  MapOfSets<K,V>::begin() { return iterator(&root); }
+  
+  template<class K, class V>
+  typename MapOfSets<K,V>::iterator 
+  MapOfSets<K,V>::end() { return iterator(); }
+
+  template<class K, class V>
+  template<class Iterator, class Vector>
+  void MapOfSets<K,V>::findSubsets(Node *n, 
+                                  const std::set<K> &accum,
+                                  Iterator begin, 
+                                  Iterator end,
+                                  Vector &resultsOut) {
+    if (n->isEndOfSet) {
+      resultsOut.push_back(std::make_pair(accum, n->value));
+    }
+    
+    for (Iterator it=begin; it!=end;) {
+      K elt = *it;
+      typename Node::children_ty::iterator kit = n->children.find(elt);
+      it++;
+      if (kit!=n->children.end()) {
+        std::set<K> nacc = accum;
+        nacc.insert(elt);
+        findSubsets(&kit->second, nacc, it, end, resultsOut);
+      }
+    }
+  }
+
+  template<class K, class V>
+  void MapOfSets<K,V>::subsets(const std::set<K> &set,
+                               std::vector< std::pair<std::set<K>, 
+                                                      V> > &resultOut) {
+    findSubsets(&root, std::set<K>(), set.begin(), set.end(), resultOut);
+  }
+
+  template<class K, class V>
+  template<class Iterator, class Vector>
+  void MapOfSets<K,V>::findSupersets(Node *n, 
+                                     const std::set<K> &accum,
+                                     Iterator begin, 
+                                     Iterator end,
+                                     Vector &resultsOut) {
+    if (begin==end) {
+      if (n->isEndOfSet)
+        resultsOut.push_back(std::make_pair(accum, n->value));
+      for (typename Node::children_ty::iterator it = n->children.begin(),
+             ie = n->children.end(); it != ie; ++it) {
+        std::set<K> nacc = accum;
+        nacc.insert(it->first);
+        findSupersets(&it->second, nacc, begin, end, resultsOut);
+      }
+    } else {
+      K elt = *begin;
+      Iterator next = begin;
+      ++next;
+      for (typename Node::children_ty::iterator it = n->children.begin(),
+             ie = n->children.end(); it != ie; ++it) {
+        std::set<K> nacc = accum;
+        nacc.insert(it->first);
+        if (elt==it->first) {
+          findSupersets(&it->second, nacc, next, end, resultsOut);
+        } else if (it->first<elt) {
+          findSupersets(&it->second, nacc, begin, end, resultsOut);
+        } else {
+          break;
+        }
+      }
+    }
+  }
+
+  template<class K, class V>
+  void MapOfSets<K,V>::supersets(const std::set<K> &set,
+                               std::vector< std::pair<std::set<K>, V> > &resultOut) {
+    findSupersets(&root, std::set<K>(), set.begin(), set.end(), resultOut);
+  }
+
+  template<class K, class V>
+  template<class Predicate>
+  V *MapOfSets<K,V>::findSubset(Node *n, 
+                                typename std::set<K>::iterator begin, 
+                                typename std::set<K>::iterator end,
+                                const Predicate &p) {   
+    if (n->isEndOfSet && p(n->value)) {
+      return &n->value;
+    } else if (begin==end) {
+      return 0;
+    } else {
+      typename Node::children_ty::iterator kend = n->children.end();
+      typename Node::children_ty::iterator 
+        kbegin = n->children.lower_bound(*begin);
+      typename std::set<K>::iterator it = begin;
+      if (kbegin==kend)
+        return 0;
+      for (;;) { // kbegin!=kend && *it <= kbegin->first
+        while (*it < kbegin->first) {
+          ++it;
+          if (it==end)
+            return 0;
+        }
+        if (*it == kbegin->first) {
+          ++it;
+          V *res = findSubset(&kbegin->second, it, end, p);
+          if (res || it==end)
+            return res;
+        }
+        while (kbegin->first < *it) {
+          ++kbegin;
+          if (kbegin==kend)
+            return 0;
+        }
+      }
+    }
+  }
+  
+  template<class K, class V>
+  template<class Predicate>
+  V *MapOfSets<K,V>::findSuperset(Node *n, 
+                                  typename std::set<K>::iterator begin, 
+                                  typename std::set<K>::iterator end,
+                                  const Predicate &p) {   
+    if (begin==end) {
+      if (n->isEndOfSet && p(n->value))
+        return &n->value;
+      for (typename Node::children_ty::iterator it = n->children.begin(),
+             ie = n->children.end(); it != ie; ++it) {
+        V *res = findSuperset(&it->second, begin, end, p);
+        if (res) return res;
+      }
+    } else {
+      typename Node::children_ty::iterator kbegin = n->children.begin();
+      typename Node::children_ty::iterator kmid = 
+        n->children.lower_bound(*begin);
+      for (typename Node::children_ty::iterator it = n->children.begin(),
+             ie = n->children.end(); it != ie; ++it) {
+        V *res = findSuperset(&it->second, begin, end, p);
+        if (res) return res;
+      }
+      if (kmid!=n->children.end() && *begin==kmid->first) {
+        V *res = findSuperset(&kmid->second, ++begin, end, p);
+        if (res) return res;
+      }
+    }
+    return 0;
+  }
+
+  template<class K, class V>
+  template<class Predicate>
+  V *MapOfSets<K,V>::findSuperset(const std::set<K> &set, const Predicate &p) {    
+    return findSuperset(&root, set.begin(), set.end(), p);
+  }
+
+  template<class K, class V>
+  template<class Predicate>
+  V *MapOfSets<K,V>::findSubset(const std::set<K> &set, const Predicate &p) {    
+    return findSubset(&root, set.begin(), set.end(), p);
+  }
+
+  template<class K, class V>
+  void MapOfSets<K,V>::clear() {
+    root.isEndOfSet = false;
+    root.value = V();
+    root.children.clear();
+  }
+
+}
+
+#endif
diff --git a/include/klee/Internal/ADT/RNG.h b/include/klee/Internal/ADT/RNG.h
new file mode 100644
index 00000000..b7f4906b
--- /dev/null
+++ b/include/klee/Internal/ADT/RNG.h
@@ -0,0 +1,50 @@
+//===-- RNG.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_UTIL_RNG_H
+#define KLEE_UTIL_RNG_H
+
+namespace klee {
+  class RNG {
+  private:
+    /* Period parameters */  
+    static const int N = 624;
+    static const int M = 397;
+    static const unsigned int MATRIX_A = 0x9908b0dfUL;   /* constant vector a */
+    static const unsigned int UPPER_MASK = 0x80000000UL; /* most significant w-r bits */
+    static const unsigned int LOWER_MASK = 0x7fffffffUL; /* least significant r bits */
+      
+  private:
+    unsigned int mt[N]; /* the array for the state vector  */
+    int mti;
+    
+  public:
+    RNG(unsigned int seed=5489UL);
+  
+    void seed(unsigned int seed);
+    
+    /* generates a random number on [0,0xffffffff]-interval */
+    unsigned int getInt32();
+    /* generates a random number on [0,0x7fffffff]-interval */
+    int getInt31();
+    /* generates a random number on [0,1]-real-interval */
+    double getDoubleLR();
+    float getFloatLR();
+    /* generates a random number on [0,1)-real-interval */
+    double getDoubleL();
+    float getFloatL();
+    /* generates a random number on (0,1)-real-interval */
+    double getDouble();
+    float getFloat();
+    /* generators a random flop */
+    bool getBool();
+  };
+}
+
+#endif
diff --git a/include/klee/Internal/ADT/TreeStream.h b/include/klee/Internal/ADT/TreeStream.h
new file mode 100644
index 00000000..63e49dbb
--- /dev/null
+++ b/include/klee/Internal/ADT/TreeStream.h
@@ -0,0 +1,77 @@
+//===-- TreeStream.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 __UTIL_TREESTREAM_H__
+#define __UTIL_TREESTREAM_H__
+
+#include <string>
+#include <iostream>
+#include <vector>
+
+namespace klee {
+
+  typedef unsigned TreeStreamID;
+  class TreeOStream;
+
+  class TreeStreamWriter {
+    static const unsigned bufferSize = 4*4096;
+
+    friend class TreeOStream;
+
+  private:
+    char buffer[bufferSize];
+    unsigned lastID, bufferCount;
+
+    std::string path;
+    std::ofstream *output;
+    unsigned ids;
+
+    void write(TreeOStream &os, const char *s, unsigned size);
+    void flushBuffer();
+
+  public:
+    TreeStreamWriter(const std::string &_path);
+    ~TreeStreamWriter();
+
+    bool good();
+
+    TreeOStream open();
+    TreeOStream open(const TreeOStream &node);
+
+    void flush();
+
+    // hack, to be replace by proper stream capabilities
+    void readStream(TreeStreamID id,
+                    std::vector<unsigned char> &out);
+  };
+
+  class TreeOStream {
+    friend class TreeStreamWriter;
+
+  private:
+    TreeStreamWriter *writer;
+    unsigned id;
+    
+    TreeOStream(TreeStreamWriter &_writer, unsigned _id);
+
+  public:
+    TreeOStream();
+    ~TreeOStream();
+
+    unsigned getID() const;
+
+    void write(const char *buffer, unsigned size);
+
+    TreeOStream &operator<<(const std::string &s);
+
+    void flush();
+  };
+}
+
+#endif
diff --git a/include/klee/Internal/Module/Cell.h b/include/klee/Internal/Module/Cell.h
new file mode 100644
index 00000000..f54cd6eb
--- /dev/null
+++ b/include/klee/Internal/Module/Cell.h
@@ -0,0 +1,23 @@
+//===-- Cell.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_CELL_H
+#define KLEE_CELL_H
+
+#include <klee/Expr.h>
+
+namespace klee {
+  class MemoryObject;
+
+  struct Cell {
+    ref<Expr> value;
+  };
+}
+
+#endif
diff --git a/include/klee/Internal/Module/InstructionInfoTable.h b/include/klee/Internal/Module/InstructionInfoTable.h
new file mode 100644
index 00000000..c93f5ddb
--- /dev/null
+++ b/include/klee/Internal/Module/InstructionInfoTable.h
@@ -0,0 +1,70 @@
+//===-- InstructionInfoTable.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_LIB_INSTRUCTIONINFOTABLE_H
+#define KLEE_LIB_INSTRUCTIONINFOTABLE_H
+
+#include <map>
+#include <string>
+#include <set>
+
+namespace llvm {
+  class Function;
+  class Instruction;
+  class Module; 
+}
+
+namespace klee {
+
+  /* Stores debug information for a KInstruction */
+  struct InstructionInfo {
+    unsigned id;
+    const std::string &file;
+    unsigned line;
+    unsigned assemblyLine;
+
+  public:
+    InstructionInfo(unsigned _id,
+                    const std::string &_file,
+                    unsigned _line,
+                    unsigned _assemblyLine)
+      : id(_id), 
+        file(_file),
+        line(_line),
+        assemblyLine(_assemblyLine) {
+    }
+  };
+
+  class InstructionInfoTable {
+    struct ltstr { 
+      bool operator()(const std::string *a, const std::string *b) const {
+        return *a<*b;
+      }
+    };
+
+    std::string dummyString;
+    InstructionInfo dummyInfo;
+    std::map<const llvm::Instruction*, InstructionInfo> infos;
+    std::set<const std::string *, ltstr> internedStrings;
+
+  private:
+    const std::string *internString(std::string s);
+
+  public:
+    InstructionInfoTable(llvm::Module *m);
+    ~InstructionInfoTable();
+
+    unsigned getMaxID() const;
+    const InstructionInfo &getInfo(const llvm::Instruction*) const;
+    const InstructionInfo &getFunctionInfo(const llvm::Function*) const;
+  };
+
+}
+
+#endif
diff --git a/include/klee/Internal/Module/KInstIterator.h b/include/klee/Internal/Module/KInstIterator.h
new file mode 100644
index 00000000..3890cc65
--- /dev/null
+++ b/include/klee/Internal/Module/KInstIterator.h
@@ -0,0 +1,49 @@
+//===-- KInstIterator.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_KINSTITERATOR_H
+#define KLEE_KINSTITERATOR_H
+
+namespace klee {
+  class KInstruction;
+
+  class KInstIterator {
+    KInstruction **it;
+
+  public:
+    KInstIterator() : it(0) {}
+    KInstIterator(KInstruction **_it) : it(_it) {}
+    KInstIterator(const KInstIterator &b) : it(b.it) {}
+    ~KInstIterator() {}
+
+    KInstIterator &operator=(const KInstIterator &b) {
+      it = b.it;
+      return *this;
+    }
+
+    bool operator==(const KInstIterator &b) const {
+      return it==b.it;
+    }
+    bool operator!=(const KInstIterator &b) const {
+      return !(*this == b);
+    }
+
+    KInstIterator &operator++() {
+      ++it;
+      return *this;
+    }
+
+    operator KInstruction*() const { return it ? *it : 0;}
+    operator bool() const { return it != 0; }
+
+    KInstruction *operator ->() const { return *it; }
+  };
+} // End klee namespace
+
+#endif
diff --git a/include/klee/Internal/Module/KInstruction.h b/include/klee/Internal/Module/KInstruction.h
new file mode 100644
index 00000000..c91d37ab
--- /dev/null
+++ b/include/klee/Internal/Module/KInstruction.h
@@ -0,0 +1,50 @@
+//===-- KInstruction.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_KINSTRUCTION_H
+#define KLEE_KINSTRUCTION_H
+
+#include <vector>
+
+namespace llvm {
+  class Instruction;
+}
+
+namespace klee {
+  class Executor;
+  struct InstructionInfo;
+  class KModule;
+
+
+  /// KInstruction - Intermediate instruction representation used
+  /// during execution.
+  struct KInstruction {
+    llvm::Instruction *inst;    
+    const InstructionInfo *info;
+
+    /// Value numbers for each operand. -1 is an invalid value,
+    /// otherwise negative numbers are indices (negated and offset by
+    /// 2) into the module constant table and positive numbers are
+    /// register indices.
+    int *operands;
+    /// Destination register index.
+    unsigned dest;
+
+  public:
+    virtual ~KInstruction(); 
+  };
+
+  struct KGEPInstruction : KInstruction {
+    std::vector< std::pair<unsigned, unsigned> > indices;
+    unsigned offset;
+  };
+}
+
+#endif
+
diff --git a/include/klee/Internal/Module/KModule.h b/include/klee/Internal/Module/KModule.h
new file mode 100644
index 00000000..690f079d
--- /dev/null
+++ b/include/klee/Internal/Module/KModule.h
@@ -0,0 +1,119 @@
+//===-- KModule.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_KMODULE_H
+#define KLEE_KMODULE_H
+
+#include "klee/Interpreter.h"
+
+#include <map>
+#include <set>
+#include <vector>
+
+namespace llvm {
+  class BasicBlock;
+  class Constant;
+  class Function;
+  class Instruction;
+  class Module;
+  class TargetData;
+}
+
+namespace klee {
+  class Cell;
+  class Executor;
+  class Expr;
+  class InterpreterHandler;
+  class InstructionInfoTable;
+  class KInstruction;
+  class KModule;
+  template<class T> class ref;
+
+  struct KFunction {
+    llvm::Function *function;
+
+    unsigned numArgs, numRegisters;
+
+    unsigned numInstructions;
+    KInstruction **instructions;
+
+    std::map<llvm::BasicBlock*, unsigned> basicBlockEntry;
+
+    /// Whether instructions in this function should count as
+    /// "coverable" for statistics and search heuristics.
+    bool trackCoverage;
+
+  private:
+    KFunction(const KFunction&);
+    KFunction &operator=(const KFunction&);
+
+  public:
+    explicit KFunction(llvm::Function*, KModule *);
+    ~KFunction();
+
+    unsigned getArgRegister(unsigned index) { return index; }
+  };
+
+
+  class KConstant {
+  public:
+    /// Actual LLVM constant this represents.
+    llvm::Constant* ct;
+
+    /// The constant ID.
+    unsigned id;
+
+    /// First instruction where this constant was encountered, or NULL
+    /// if not applicable/unavailable.
+    KInstruction *ki;
+
+    KConstant(llvm::Constant*, unsigned, KInstruction*);
+  };
+
+
+  class KModule {
+  public:
+    llvm::Module *module;
+    llvm::TargetData *targetData;
+    
+    // Some useful functions to know the address of
+    llvm::Function *dbgStopPointFn, *kleeMergeFn;
+
+    // Our shadow versions of LLVM structures.
+    std::vector<KFunction*> functions;
+    std::map<llvm::Function*, KFunction*> functionMap;
+
+    // Functions which escape (may be called indirectly)
+    // XXX change to KFunction
+    std::set<llvm::Function*> escapingFunctions;
+
+    InstructionInfoTable *infos;
+
+    std::vector<llvm::Constant*> constants;
+    std::map<llvm::Constant*, KConstant*> constantMap;
+    KConstant* getKConstant(llvm::Constant *c);
+
+    Cell *constantTable;
+
+  public:
+    KModule(llvm::Module *_module);
+    ~KModule();
+
+    /// Initialize local data structures.
+    //
+    // FIXME: ihandler should not be here
+    void prepare(const Interpreter::ModuleOptions &opts, 
+                 InterpreterHandler *ihandler);
+
+    /// Return an id for the given constant, creating a new one if necessary.
+    unsigned getConstantID(llvm::Constant *c, KInstruction* ki);
+  };
+} // End klee namespace
+
+#endif
diff --git a/include/klee/Internal/README.txt b/include/klee/Internal/README.txt
new file mode 100644
index 00000000..9cedb653
--- /dev/null
+++ b/include/klee/Internal/README.txt
@@ -0,0 +1,3 @@
+This directory holds header files for things which are exposed as part
+of the internal API of a library, but shouldn't be exposed to
+externally.
diff --git a/include/klee/Internal/Support/FloatEvaluation.h b/include/klee/Internal/Support/FloatEvaluation.h
new file mode 100644
index 00000000..1d305374
--- /dev/null
+++ b/include/klee/Internal/Support/FloatEvaluation.h
@@ -0,0 +1,258 @@
+//===-- FloatEvaluation.h ---------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+// FIXME: Ditch this and use APFloat.
+
+#ifndef KLEE_UTIL_FLOATS_H
+#define KLEE_UTIL_FLOATS_H
+
+#include "klee/util/Bits.h"     //bits64::truncateToNBits
+#include "IntEvaluation.h" //ints::sext
+
+#include "llvm/Support/MathExtras.h"
+
+namespace klee {
+namespace floats {
+
+// ********************************** //
+// *** Pack uint64_t into FP types ** //
+// ********************************** //
+
+// interpret the 64 bits as a double instead of a uint64_t
+inline double UInt64AsDouble( uint64_t bits ) {
+  double ret;
+  assert( sizeof(bits) == sizeof(ret) );
+  memcpy( &ret, &bits, sizeof bits );
+  return ret;
+}
+
+// interpret the first 32 bits as a float instead of a uint64_t
+inline float UInt64AsFloat( uint64_t bits ) {
+  uint32_t tmp = bits; // ensure that we read correct bytes
+  float ret;
+  assert( sizeof(tmp) == sizeof(ret) );
+  memcpy( &ret, &tmp, sizeof tmp );
+  return ret;
+}
+
+
+// ********************************** //
+// *** Pack FP types into uint64_t ** //
+// ********************************** //
+
+// interpret the 64 bits as a uint64_t instead of a double
+inline uint64_t DoubleAsUInt64( double d ) {
+  uint64_t ret;
+  assert( sizeof(d) == sizeof(ret) );
+  memcpy( &ret, &d, sizeof d );
+  return ret;
+}
+
+// interpret the 32 bits as a uint64_t instead of as a float (add 32 0s)
+inline uint64_t FloatAsUInt64( float f ) {
+  uint32_t tmp;
+  assert( sizeof(tmp) == sizeof(f) );
+  memcpy( &tmp, &f, sizeof f );
+  return (uint64_t)tmp;
+}
+
+
+// ********************************** //
+// ************ Constants *********** //
+// ********************************** //
+
+const unsigned FLT_BITS = 32;
+const unsigned DBL_BITS = 64;
+
+
+
+// ********************************** //
+// ***** LLVM Binary Operations ***** //
+// ********************************** //
+
+// add of l and r
+inline uint64_t add(uint64_t l, uint64_t r, unsigned inWidth) {
+  switch( inWidth ) {
+  case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l)  + UInt64AsFloat(r)),  FLT_BITS);
+  case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) + UInt64AsDouble(r)), DBL_BITS);
+  default: assert(0 && "invalid floating point width");
+  }
+}
+
+// difference of l and r
+inline uint64_t sub(uint64_t l, uint64_t r, unsigned inWidth) {
+  switch( inWidth ) {
+  case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l)  - UInt64AsFloat(r)),  FLT_BITS);
+  case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) - UInt64AsDouble(r)), DBL_BITS);
+  default: assert(0 && "invalid floating point width");
+  }
+}
+
+// product of l and r
+inline uint64_t mul(uint64_t l, uint64_t r, unsigned inWidth) {
+  switch( inWidth ) {
+  case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l)  * UInt64AsFloat(r)),  FLT_BITS);
+  case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) * UInt64AsDouble(r)), DBL_BITS);
+  default: assert(0 && "invalid floating point width");
+  }
+}
+
+// signed divide of l by r
+inline uint64_t div(uint64_t l, uint64_t r, unsigned inWidth) {
+  switch( inWidth ) {
+  case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l)  / UInt64AsFloat(r)),  FLT_BITS);
+  case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) / UInt64AsDouble(r)), DBL_BITS);
+  default: assert(0 && "invalid floating point width");
+  }
+}
+
+// signed modulo of l by r
+inline uint64_t mod(uint64_t l, uint64_t r, unsigned inWidth) {
+  switch( inWidth ) {
+  case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64( fmod(UInt64AsFloat(l),  UInt64AsFloat(r)) ), FLT_BITS);
+  case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64( fmod(UInt64AsDouble(l), UInt64AsDouble(r)) ), DBL_BITS);
+  default: assert(0 && "invalid floating point width");
+  }
+}
+
+
+// ********************************** //
+// *** LLVM Comparison Operations *** //
+// ********************************** //
+
+// determine if l represents NaN
+inline bool isNaN(uint64_t l, unsigned inWidth) {
+  switch( inWidth ) {
+  case FLT_BITS: return llvm::IsNAN( UInt64AsFloat(l) );
+  case DBL_BITS: return llvm::IsNAN( UInt64AsDouble(l) );
+  default: assert(0 && "invalid floating point width");
+  }
+}
+
+inline uint64_t eq(uint64_t l, uint64_t r, unsigned inWidth) {
+  switch( inWidth ) {
+  case FLT_BITS: return UInt64AsFloat(l)  == UInt64AsFloat(r);
+  case DBL_BITS: return UInt64AsDouble(l) == UInt64AsDouble(r);
+  default: assert(0 && "invalid floating point width");
+  }
+}
+
+inline uint64_t ne(uint64_t l, uint64_t r, unsigned inWidth) {
+  switch( inWidth ) {
+  case FLT_BITS: return UInt64AsFloat(l)  != UInt64AsFloat(r);
+  case DBL_BITS: return UInt64AsDouble(l) != UInt64AsDouble(r);
+  default: assert(0 && "invalid floating point width");
+  }
+}
+
+inline uint64_t lt(uint64_t l, uint64_t r, unsigned inWidth) {
+  switch( inWidth ) {
+  case FLT_BITS: return UInt64AsFloat(l)  < UInt64AsFloat(r);
+  case DBL_BITS: return UInt64AsDouble(l) < UInt64AsDouble(r);
+  default: assert(0 && "invalid floating point width");
+  }
+}
+
+inline uint64_t le(uint64_t l, uint64_t r, unsigned inWidth) {
+  switch( inWidth ) {
+  case FLT_BITS: return UInt64AsFloat(l)  <= UInt64AsFloat(r);
+  case DBL_BITS: return UInt64AsDouble(l) <= UInt64AsDouble(r);
+  default: assert(0 && "invalid floating point width");
+  }
+}
+
+inline uint64_t gt(uint64_t l, uint64_t r, unsigned inWidth) {
+  switch( inWidth ) {
+  case FLT_BITS: return UInt64AsFloat(l)  > UInt64AsFloat(r);
+  case DBL_BITS: return UInt64AsDouble(l) > UInt64AsDouble(r);
+  default: assert(0 && "invalid floating point width");
+  }
+}
+
+inline uint64_t ge(uint64_t l, uint64_t r, unsigned inWidth) {
+  switch( inWidth ) {
+  case FLT_BITS: return UInt64AsFloat(l)  >= UInt64AsFloat(r);
+  case DBL_BITS: return UInt64AsDouble(l) >= UInt64AsDouble(r);
+  default: assert(0 && "invalid floating point width");
+  }
+}
+
+
+// ********************************** //
+// *** LLVM Conversion Operations *** //
+// ********************************** //
+
+// truncation of l (which must be a double) to float (casts a double to a float)
+inline uint64_t trunc(uint64_t l, unsigned outWidth, unsigned inWidth) {
+  // FIXME: Investigate this, should this not happen? Was a quick
+  // patch for busybox.
+  if (inWidth==64 && outWidth==64) {
+    return l;
+  } else {
+    assert(inWidth==64 && "can only truncate from a 64-bit double");
+    assert(outWidth==32 && "can only truncate to a 32-bit float");
+    float trunc = (float)UInt64AsDouble(l);
+    return bits64::truncateToNBits(FloatAsUInt64(trunc), outWidth);
+  }
+}
+
+// extension of l (which must be a float) to double (casts a float to a double)
+inline uint64_t ext(uint64_t l, unsigned outWidth, unsigned inWidth) {
+  // FIXME: Investigate this, should this not happen? Was a quick
+  // patch for busybox.
+  if (inWidth==64 && outWidth==64) {
+    return l;
+  } else {
+    assert(inWidth==32 && "can only extend from a 32-bit float");
+    assert(outWidth==64 && "can only extend to a 64-bit double");
+    double ext = (double)UInt64AsFloat(l);
+    return bits64::truncateToNBits(DoubleAsUInt64(ext), outWidth);
+  }
+}
+
+// conversion of l to an unsigned integer, rounding towards zero
+inline uint64_t toUnsignedInt( uint64_t l, unsigned outWidth, unsigned inWidth ) {
+  switch( inWidth ) {
+  case FLT_BITS: return bits64::truncateToNBits((uint64_t)UInt64AsFloat(l),  outWidth );
+  case DBL_BITS: return bits64::truncateToNBits((uint64_t)UInt64AsDouble(l), outWidth );
+  default: assert(0 && "invalid floating point width");
+  }
+}
+
+// conversion of l to a signed integer, rounding towards zero
+inline uint64_t toSignedInt( uint64_t l, unsigned outWidth, unsigned inWidth ) {
+  switch( inWidth ) {
+  case FLT_BITS: return bits64::truncateToNBits((int64_t)UInt64AsFloat(l),  outWidth);
+  case DBL_BITS: return bits64::truncateToNBits((int64_t)UInt64AsDouble(l), outWidth);
+  default: assert(0 && "invalid floating point width");
+  }
+}
+
+// conversion of l, interpreted as an unsigned int, to a floating point number
+inline uint64_t UnsignedIntToFP( uint64_t l, unsigned outWidth ) {
+  switch( outWidth ) {
+  case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64((float)l),  outWidth);
+  case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64((double)l), outWidth);
+  default: assert(0 && "invalid floating point width");
+  }
+}
+
+// conversion of l, interpreted as a signed int, to a floating point number
+inline uint64_t SignedIntToFP( uint64_t l, unsigned outWidth, unsigned inWidth ) {
+  switch( outWidth ) {
+  case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64((float)(int64_t)ints::sext(l, 64, inWidth)), outWidth);
+  case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64((double)(int64_t)ints::sext(l,64, inWidth)), outWidth);
+  default: assert(0 && "invalid floating point width");
+  }
+}
+
+} // end namespace ints
+} // end namespace klee
+
+#endif //KLEE_UTIL_FLOATS_H
diff --git a/include/klee/Internal/Support/IntEvaluation.h b/include/klee/Internal/Support/IntEvaluation.h
new file mode 100644
index 00000000..ed3ffc23
--- /dev/null
+++ b/include/klee/Internal/Support/IntEvaluation.h
@@ -0,0 +1,164 @@
+//===-- IntEvaluation.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_UTIL_INTEVALUATION_H
+#define KLEE_UTIL_INTEVALUATION_H
+
+#include "klee/util/Bits.h"
+
+#define MAX_BITS (sizeof(uint64_t) * 8)
+
+// ASSUMPTION: invalid bits in each uint64_t are 0. the trade-off here is
+// between making trunc/zext/sext fast and making operations that depend
+// on the invalid bits being 0 fast. 
+
+namespace klee {
+namespace ints {
+
+// add of l and r
+inline uint64_t add(uint64_t l, uint64_t r, unsigned inWidth) {
+  return bits64::truncateToNBits(l + r, inWidth);
+}
+
+// difference of l and r
+inline uint64_t sub(uint64_t l, uint64_t r, unsigned inWidth) {
+  return bits64::truncateToNBits(l - r, inWidth);
+}
+
+// product of l and r
+inline uint64_t mul(uint64_t l, uint64_t r, unsigned inWidth) {
+  return bits64::truncateToNBits(l * r, inWidth);
+}
+
+// truncation of l to outWidth bits
+inline uint64_t trunc(uint64_t l, unsigned outWidth, unsigned inWidth) {
+  return bits64::truncateToNBits(l, outWidth);
+}
+
+// zero-extension of l from inWidth to outWidth bits
+inline uint64_t zext(uint64_t l, unsigned outWidth, unsigned inWidth) {
+  return l;
+}
+
+// sign-extension of l from inWidth to outWidth bits
+inline uint64_t sext(uint64_t l, unsigned outWidth, unsigned inWidth) {
+  uint32_t numInvalidBits = MAX_BITS - inWidth;
+  return bits64::truncateToNBits(((int64_t)(l << numInvalidBits)) >> numInvalidBits, outWidth);
+}
+
+// unsigned divide of l by r
+inline uint64_t udiv(uint64_t l, uint64_t r, unsigned inWidth) {
+  return bits64::truncateToNBits(l / r, inWidth);
+}
+
+// unsigned mod of l by r
+inline uint64_t urem(uint64_t l, uint64_t r, unsigned inWidth) {
+  return bits64::truncateToNBits(l % r, inWidth);
+}
+
+// signed divide of l by r
+inline uint64_t sdiv(uint64_t l, uint64_t r, unsigned inWidth) {
+  // sign extend operands so that signed operation on 64-bits works correctly
+  int64_t sl = sext(l, MAX_BITS, inWidth);
+  int64_t sr = sext(r, MAX_BITS, inWidth);
+  return bits64::truncateToNBits(sl / sr, inWidth);
+}
+
+// signed mod of l by r
+inline uint64_t srem(uint64_t l, uint64_t r, unsigned inWidth) {
+  // sign extend operands so that signed operation on 64-bits works correctly
+  int64_t sl = sext(l, MAX_BITS, inWidth);
+  int64_t sr = sext(r, MAX_BITS, inWidth);
+  return bits64::truncateToNBits(sl % sr, inWidth);
+}
+
+// arithmetic shift right of l by r bits
+inline uint64_t ashr(uint64_t l, uint64_t shift, unsigned inWidth) {
+  int64_t sl = sext(l, MAX_BITS, inWidth);
+  return bits64::truncateToNBits(sl >> shift, inWidth);
+}
+
+// logical shift right of l by r bits
+inline uint64_t lshr(uint64_t l, uint64_t shift, unsigned inWidth) {
+  return l >> shift;
+}
+
+// shift left of l by r bits
+inline uint64_t shl(uint64_t l, uint64_t shift, unsigned inWidth) {
+  return bits64::truncateToNBits(l << shift, inWidth);
+}
+
+// logical AND of l and r
+inline uint64_t land(uint64_t l, uint64_t r, unsigned inWidth) {
+  return l & r;
+}
+
+// logical OR of l and r
+inline uint64_t lor(uint64_t l, uint64_t r, unsigned inWidth) {
+  return l | r;
+}
+
+// logical XOR of l and r
+inline uint64_t lxor(uint64_t l, uint64_t r, unsigned inWidth) {
+  return l ^ r;
+}
+
+// comparison operations
+inline uint64_t eq(uint64_t l, uint64_t r, unsigned inWidth) {
+  return l == r;
+}
+
+inline uint64_t ne(uint64_t l, uint64_t r, unsigned inWidth) {
+  return l != r;
+}
+
+inline uint64_t ult(uint64_t l, uint64_t r, unsigned inWidth) {
+  return l < r;
+}
+
+inline uint64_t ule(uint64_t l, uint64_t r, unsigned inWidth) {
+  return l <= r;
+}
+
+inline uint64_t ugt(uint64_t l, uint64_t r, unsigned inWidth) {
+  return l > r;
+}
+
+inline uint64_t uge(uint64_t l, uint64_t r, unsigned inWidth) {
+  return l >= r;
+}
+
+inline uint64_t slt(uint64_t l, uint64_t r, unsigned inWidth) {
+  int64_t sl = sext(l, MAX_BITS, inWidth);
+  int64_t sr = sext(r, MAX_BITS, inWidth);
+  return sl < sr;
+}
+
+inline uint64_t sle(uint64_t l, uint64_t r, unsigned inWidth) {
+  int64_t sl = sext(l, MAX_BITS, inWidth);
+  int64_t sr = sext(r, MAX_BITS, inWidth);
+  return sl <= sr;
+}
+
+inline uint64_t sgt(uint64_t l, uint64_t r, unsigned inWidth) {
+  int64_t sl = sext(l, MAX_BITS, inWidth);
+  int64_t sr = sext(r, MAX_BITS, inWidth);
+  return sl > sr;
+}
+
+inline uint64_t sge(uint64_t l, uint64_t r, unsigned inWidth) {
+  int64_t sl = sext(l, MAX_BITS, inWidth);
+  int64_t sr = sext(r, MAX_BITS, inWidth);
+  return sl >= sr;
+}
+
+} // end namespace ints
+} // end namespace klee
+
+#endif 
diff --git a/include/klee/Internal/Support/ModuleUtil.h b/include/klee/Internal/Support/ModuleUtil.h
new file mode 100644
index 00000000..6cf5fbee
--- /dev/null
+++ b/include/klee/Internal/Support/ModuleUtil.h
@@ -0,0 +1,40 @@
+//===-- ModuleUtil.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_TRANSFORM_UTIL_H
+#define KLEE_TRANSFORM_UTIL_H
+
+#include <string>
+
+namespace llvm {
+  class Function;
+  class Instruction;
+  class Module; 
+}
+
+namespace klee {
+ 
+  /// Link a module with a specified bitcode archive.
+  llvm::Module *linkWithLibrary(llvm::Module *module, 
+                                const std::string &libraryName);
+
+  /// Return the Function* target of a Call or Invoke instruction, or
+  /// null if it cannot be determined (should be only for indirect
+  /// calls, although complicated constant expressions might be
+  /// another possibility).
+  llvm::Function *getDirectCallTarget(const llvm::Instruction*);
+
+  /// Return true iff the given Function value is used in something
+  /// other than a direct call (or a constant expression that
+  /// terminates in a direct call).
+  bool functionEscapes(const llvm::Function *f);
+
+}
+
+#endif
diff --git a/include/klee/Internal/Support/QueryLog.h b/include/klee/Internal/Support/QueryLog.h
new file mode 100644
index 00000000..b090d2d9
--- /dev/null
+++ b/include/klee/Internal/Support/QueryLog.h
@@ -0,0 +1,63 @@
+//===-- QueryLog.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_OPT_LOGGINGSOLVER_H
+#define KLEE_OPT_LOGGINGSOLVER_H
+
+#include "klee/Expr.h"
+
+#include <vector>
+
+namespace klee {
+  struct Query;
+
+  class QueryLogEntry {
+  public:
+    enum Type {
+      Validity,
+      Truth,
+      Value,
+      Cex
+    };
+    
+    typedef std::vector< ref<Expr> > exprs_ty;
+    exprs_ty exprs;
+
+    Type type;
+    ref<Expr> query;
+    unsigned instruction;
+    std::vector<const Array*> objects;
+    
+  public:
+    QueryLogEntry() : query(0,Expr::Bool) {}
+    QueryLogEntry(const QueryLogEntry &b);
+    QueryLogEntry(const Query &_query, 
+                  Type _type,
+                  const std::vector<const Array*> *objects = 0);
+  };
+
+  class QueryLogResult {
+  public:
+    uint64_t result;
+    double time;
+
+  public:
+    QueryLogResult() {}
+    QueryLogResult(bool _success, uint64_t _result, double _time) 
+      : result(_result), time(_time) {
+      if (!_success) { // la la la
+        result = 0;
+        time = -1;
+      }
+    }
+  };
+  
+}
+
+#endif
diff --git a/include/klee/Internal/Support/Timer.h b/include/klee/Internal/Support/Timer.h
new file mode 100644
index 00000000..a422abd0
--- /dev/null
+++ b/include/klee/Internal/Support/Timer.h
@@ -0,0 +1,28 @@
+//===-- Timer.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_TIMER_H
+#define KLEE_TIMER_H
+
+#include <stdint.h>
+
+namespace klee {
+  class WallTimer {
+    uint64_t startMicroseconds;
+    
+  public:
+    WallTimer();
+
+    /// check - Return the delta since the timer was created, in microseconds.
+    uint64_t check();
+  };
+}
+
+#endif
+
diff --git a/include/klee/Internal/System/Time.h b/include/klee/Internal/System/Time.h
new file mode 100644
index 00000000..5229c8c9
--- /dev/null
+++ b/include/klee/Internal/System/Time.h
@@ -0,0 +1,20 @@
+//===-- Time.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_UTIL_TIME_H
+#define KLEE_UTIL_TIME_H
+
+namespace klee {
+  namespace util {
+    double getUserTime();
+    double getWallTime();
+  }
+}
+
+#endif
diff --git a/include/klee/Interpreter.h b/include/klee/Interpreter.h
new file mode 100644
index 00000000..eca6e59e
--- /dev/null
+++ b/include/klee/Interpreter.h
@@ -0,0 +1,149 @@
+//===-- Interpreter.h - Abstract Execution Engine Interface -----*- 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_INTERPRETER_H
+#define KLEE_INTERPRETER_H
+
+#include <vector>
+#include <string>
+#include <map>
+#include <set>
+
+struct BOut;
+
+namespace llvm {
+class Function;
+class Module;
+}
+
+namespace klee {
+class ExecutionState;
+class Interpreter;
+class TreeStreamWriter;
+
+class InterpreterHandler {
+public:
+  InterpreterHandler() {}
+  virtual ~InterpreterHandler() {};
+
+  virtual std::ostream &getInfoStream() const = 0;
+
+  virtual std::string getOutputFilename(const std::string &filename) = 0;
+  virtual std::ostream *openOutputFile(const std::string &filename) = 0;
+
+  virtual void incPathsExplored() = 0;
+
+  virtual void processTestCase(const ExecutionState &state,
+                               const char *err, 
+                               const char *suffix) = 0;
+};
+
+class Interpreter {
+public:
+  /// ModuleOptions - Module level options which can be set when
+  /// registering a module with the interpreter.
+  struct ModuleOptions {
+    std::string LibraryDir;
+    bool Optimize;
+    bool CheckDivZero;
+
+    ModuleOptions(const std::string& _LibraryDir, 
+                  bool _Optimize, bool _CheckDivZero)
+      : LibraryDir(_LibraryDir), Optimize(_Optimize), 
+        CheckDivZero(_CheckDivZero) {}
+  };
+
+  /// InterpreterOptions - Options varying the runtime behavior during
+  /// interpretation.
+  struct InterpreterOptions {
+    /// A frequency at which to make concrete reads return constrained
+    /// symbolic values. This is used to test the correctness of the
+    /// symbolic execution on concrete programs.
+    unsigned MakeConcreteSymbolic;
+
+    InterpreterOptions()
+      : MakeConcreteSymbolic(false)
+    {}
+  };
+
+protected:
+  const InterpreterOptions interpreterOpts;
+
+  Interpreter(const InterpreterOptions &_interpreterOpts)
+    : interpreterOpts(_interpreterOpts)
+  {};
+
+public:
+  virtual ~Interpreter() {};
+
+  static Interpreter *create(const InterpreterOptions &_interpreterOpts,
+                             InterpreterHandler *ih);
+
+  /// Register the module to be executed.  
+  ///
+  /// \return The final module after it has been optimized, checks
+  /// inserted, and modified for interpretation.
+  virtual const llvm::Module * 
+  setModule(llvm::Module *module, 
+            const ModuleOptions &opts) = 0;
+
+  // supply a tree stream writer which the interpreter will use
+  // to record the concrete path (as a stream of '0' and '1' bytes).
+  virtual void setPathWriter(TreeStreamWriter *tsw) = 0;
+
+  // supply a tree stream writer which the interpreter will use
+  // to record the symbolic path (as a stream of '0' and '1' bytes).
+  virtual void setSymbolicPathWriter(TreeStreamWriter *tsw) = 0;
+
+  // supply a test case to replay from. this can be used to drive the
+  // interpretation down a user specified path. use null to reset.
+  virtual void setReplayOut(const struct BOut *out) = 0;
+
+  // supply a list of branch decisions specifying which direction to
+  // take on forks. this can be used to drive the interpretation down
+  // a user specified path. use null to reset.
+  virtual void setReplayPath(const std::vector<bool> *path) = 0;
+
+  // supply a set of symbolic bindings that will be used as "seeds"
+  // for the search. use null to reset.
+  virtual void useSeeds(const std::vector<struct BOut *> *seeds) = 0;
+
+  virtual void runFunctionAsMain(llvm::Function *f,
+                                 int argc,
+                                 char **argv,
+                                 char **envp) = 0;
+
+  /*** Runtime options ***/
+
+  virtual void setHaltExecution(bool value) = 0;
+
+  virtual void setInhibitForking(bool value) = 0;
+
+  /*** State accessor methods ***/
+
+  virtual unsigned getPathStreamID(const ExecutionState &state) = 0;
+
+  virtual unsigned getSymbolicPathStreamID(const ExecutionState &state) = 0;
+  
+  virtual void getConstraintLog(const ExecutionState &state,
+                                std::string &res,
+                                bool asCVC = false) = 0;
+
+  virtual bool getSymbolicSolution(const ExecutionState &state, 
+                                   std::vector< 
+                                   std::pair<std::string,
+                                   std::vector<unsigned char> > >
+                                   &res) = 0;
+
+  virtual void getCoveredLines(const ExecutionState &state,
+                               std::map<const std::string*, std::set<unsigned> > &res) = 0;
+};
+
+} // End klee namespace
+
+#endif
diff --git a/include/klee/Machine.h b/include/klee/Machine.h
new file mode 100644
index 00000000..b8a9e9ac
--- /dev/null
+++ b/include/klee/Machine.h
@@ -0,0 +1,28 @@
+//===-- Machine.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_MACHINE_H__
+#define __KLEE_MACHINE_H__
+
+#include "klee/Expr.h"
+
+namespace klee {
+  namespace machine {
+    enum ByteOrder {
+      LSB = 0,
+      MSB = 1
+    };
+  }
+}
+
+#define kMachineByteOrder      klee::machine::LSB
+#define kMachinePointerType    Expr::Int32
+#define kMachinePointerSize    4
+
+#endif /* __KLEE_MACHINE_H__ */
diff --git a/include/klee/Solver.h b/include/klee/Solver.h
new file mode 100644
index 00000000..2d4fa044
--- /dev/null
+++ b/include/klee/Solver.h
@@ -0,0 +1,216 @@
+//===-- Solver.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_SOLVER_H
+#define KLEE_SOLVER_H
+
+#include "klee/Expr.h"
+
+#include <vector>
+
+namespace klee {
+  class ConstraintManager;
+  class Expr;
+  class SolverImpl;
+
+  struct Query {
+  public:
+    const ConstraintManager &constraints;
+    ref<Expr> expr;
+
+    Query(const ConstraintManager& _constraints, ref<Expr> _expr)
+      : constraints(_constraints), expr(_expr) {
+    }
+
+    /// withExpr - Return a copy of the query with the given expression.
+    Query withExpr(ref<Expr> _expr) const {
+      return Query(constraints, _expr);
+    }
+
+    /// withFalse - Return a copy of the query with a false expression.
+    Query withFalse() const {
+      return Query(constraints, ref<Expr>(0, Expr::Bool));
+    }
+
+    /// negateExpr - Return a copy of the query with the expression negated.
+    Query negateExpr() const {
+      return withExpr(Expr::createNot(expr));
+    }
+  };
+
+  class Solver {
+    // DO NOT IMPLEMENT.
+    Solver(const Solver&);
+    void operator=(const Solver&);
+
+  public:
+    enum Validity {
+      True = 1,
+      False = -1,
+      Unknown = 0
+    };
+  
+  public:
+    /// validity_to_str - Return the name of given Validity enum value.
+    static const char *validity_to_str(Validity v);
+
+  public:
+    SolverImpl *impl;
+
+  public:
+    Solver(SolverImpl *_impl) : impl(_impl) {};
+    ~Solver();
+
+    /// evaluate - Determine the full validity of an expression in particular
+    /// state.
+    ////
+    /// \param [out] result - The validity of the given expression (provably
+    /// true, provably false, or neither).
+    ///
+    /// \return True on success.
+    bool evaluate(const Query&, Validity &result);
+  
+    /// mustBeTrue - Determine if the expression is provably true.
+    ///
+    /// \param [out] result - On success, true iff the expresssion is provably
+    /// false.
+    ///
+    /// \return True on success.
+    bool mustBeTrue(const Query&, bool &result);
+
+    /// mustBeFalse - Determine if the expression is provably false.
+    ///
+    /// \param [out] result - On success, true iff the expresssion is provably
+    /// false.
+    ///
+    /// \return True on success.
+    bool mustBeFalse(const Query&, bool &result);
+
+    /// mayBeTrue - Determine if there is a valid assignment for the given state
+    /// in which the expression evaluates to false.
+    ///
+    /// \param [out] result - On success, true iff the expresssion is true for
+    /// some satisfying assignment.
+    ///
+    /// \return True on success.
+    bool mayBeTrue(const Query&, bool &result);
+
+    /// mayBeFalse - Determine if there is a valid assignment for the given
+    /// state in which the expression evaluates to false.
+    ///
+    /// \param [out] result - On success, true iff the expresssion is false for
+    /// some satisfying assignment.
+    ///
+    /// \return True on success.
+    bool mayBeFalse(const Query&, bool &result);
+
+    /// getValue - Compute one possible value for the given expression.
+    ///
+    /// \param [out] result - On success, a value for the expression in some
+    /// satisying assignment.
+    ///
+    /// \return True on success.
+    bool getValue(const Query&, ref<Expr> &result);
+
+    /// getInitialValues - Compute the initial values for a list of objects.
+    ///
+    /// \param [out] result - On success, this vector will be filled in with an
+    /// array of bytes for each given object (with length matching the object
+    /// size). The bytes correspond to the initial values for the objects for
+    /// some satisying assignment.
+    ///
+    /// \return True on success.
+    ///
+    /// NOTE: This function returns failure if there is no satisfying
+    /// assignment.
+    //
+    // FIXME: This API is lame. We should probably just provide an API which
+    // returns an Assignment object, then clients can get out whatever values
+    // they want. This also allows us to optimize the representation.
+    bool getInitialValues(const Query&, 
+                          const std::vector<const Array*> &objects,
+                          std::vector< std::vector<unsigned char> > &result);
+
+    /// getRange - Compute a tight range of possible values for a given
+    /// expression.
+    ///
+    /// \return - A pair with (min, max) values for the expression.
+    ///
+    /// \post(mustBeTrue(min <= e <= max) && 
+    ///       mayBeTrue(min == e) &&
+    ///       mayBeTrue(max == e))
+    //
+    // FIXME: This should go into a helper class, and should handle failure.
+    virtual std::pair< ref<Expr>, ref<Expr> > getRange(const Query&);
+  };
+
+  /// STPSolver - A complete solver based on STP.
+  class STPSolver : public Solver {
+  public:
+    /// STPSolver - Construct a new STPSolver.
+    ///
+    /// \param useForkedSTP - Whether STP should be run in a separate process
+    /// (required for using timeouts).
+    STPSolver(bool useForkedSTP);
+    
+    /// getConstraintLog - Return the constraint log for the given state in CVC
+    /// format.
+    char *getConstraintLog(const Query&);
+    
+    /// setTimeout - Set constraint solver timeout delay to the given value; 0
+    /// is off.
+    void setTimeout(double timeout);
+  };
+
+  /* *** */
+
+  /// createValidatingSolver - Create a solver which will validate all query
+  /// results against an oracle, used for testing that an optimized solver has
+  /// the same results as an unoptimized one. This solver will assert on any
+  /// mismatches.
+  ///
+  /// \param s - The primary underlying solver to use.
+  /// \param oracle - The solver to check query results against.
+  Solver *createValidatingSolver(Solver *s, Solver *oracle);
+
+  /// createCachingSolver - Create a solver which will cache the queries in
+  /// memory (without eviction).
+  ///
+  /// \param s - The underlying solver to use.
+  Solver *createCachingSolver(Solver *s);
+
+  /// createCexCachingSolver - Create a counterexample caching solver. This is a
+  /// more sophisticated cache which records counterexamples for a constraint
+  /// set and uses subset/superset relations among constraints to try and
+  /// quickly find satisfying assignments.
+  ///
+  /// \param s - The underlying solver to use.
+  Solver *createCexCachingSolver(Solver *s);
+
+  /// createFastCexSolver - Create a "fast counterexample solver", which tries
+  /// to quickly compute a satisfying assignment for a constraint set using
+  /// value propogation and range analysis.
+  ///
+  /// \param s - The underlying solver to use.
+  Solver *createFastCexSolver(Solver *s);
+
+  /// createIndependentSolver - Create a solver which will eliminate any
+  /// unnecessary constraints before propogating the query to the underlying
+  /// solver.
+  ///
+  /// \param s - The underlying solver to use.
+  Solver *createIndependentSolver(Solver *s);
+  
+  /// createPCLoggingSolver - Create a solver which will forward all queries
+  /// after writing them to the given path in .pc format.
+  Solver *createPCLoggingSolver(Solver *s, std::string path);
+
+}
+
+#endif
diff --git a/include/klee/SolverImpl.h b/include/klee/SolverImpl.h
new file mode 100644
index 00000000..29c356be
--- /dev/null
+++ b/include/klee/SolverImpl.h
@@ -0,0 +1,63 @@
+//===-- SolverImpl.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_SOLVERIMPL_H
+#define KLEE_SOLVERIMPL_H
+
+#include <vector>
+
+namespace klee {
+  class Array;
+  class ExecutionState;
+  class Expr;
+  struct Query;
+
+  /// SolverImpl - Abstract base clase for solver implementations.
+  class SolverImpl {
+    // DO NOT IMPLEMENT.
+    SolverImpl(const SolverImpl&);
+    void operator=(const SolverImpl&);
+    
+  public:
+    SolverImpl() {}
+    virtual ~SolverImpl();
+
+    /// computeValidity - Compute a full validity result for the
+    /// query.
+    ///
+    /// The query expression is guaranteed to be non-constant and have
+    /// bool type.
+    ///
+    /// SolverImpl provides a default implementation which uses
+    /// computeTruth. Clients should override this if a more efficient
+    /// implementation is available.
+    virtual bool computeValidity(const Query& query, Solver::Validity &result);
+    
+    /// computeTruth - Determine whether the given query is provable.
+    ///
+    /// The query expression is guaranteed to be non-constant and have
+    /// bool type.
+    virtual bool computeTruth(const Query& query, bool &isValid) = 0;
+
+    /// computeValue - Compute a feasible value for the expression.
+    ///
+    /// The query expression is guaranteed to be non-constant.
+    virtual bool computeValue(const Query& query, ref<Expr> &result) = 0;
+    
+    virtual bool computeInitialValues(const Query& query,
+                                      const std::vector<const Array*> 
+                                        &objects,
+                                      std::vector< std::vector<unsigned char> > 
+                                        &values,
+                                      bool &hasSolution) = 0;  
+};
+
+}
+
+#endif
diff --git a/include/klee/Statistic.h b/include/klee/Statistic.h
new file mode 100644
index 00000000..e5aef6b1
--- /dev/null
+++ b/include/klee/Statistic.h
@@ -0,0 +1,65 @@
+//===-- Statistic.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_STATISTIC_H
+#define KLEE_STATISTIC_H
+
+#include <string>
+
+namespace klee {
+  class Statistic;
+  class StatisticManager;
+  class StatisticRecord;
+
+  /// Statistic - A named statistic instance.
+  ///
+  /// The Statistic class holds information about the statistic, but
+  /// not the actual values. Values are managed by the global
+  /// StatisticManager to enable transparent support for instruction
+  /// level and call path level statistics.
+  class Statistic {
+    friend class StatisticManager;
+    friend class StatisticRecord;
+
+  private:
+    unsigned id;
+    const std::string name;
+    const std::string shortName;
+
+  public:
+    Statistic(const std::string &_name, 
+              const std::string &_shortName);
+    ~Statistic();
+
+    /// getID - Get the unique statistic ID.
+    unsigned getID() { return id; }
+
+    /// getName - Get the statistic name.
+    const std::string &getName() const { return name; }
+
+    /// getShortName - Get the "short" statistic name, used in
+    /// callgrind output for example.
+    const std::string &getShortName() const { return shortName; }
+
+    /// getValue - Get the current primary statistic value.
+    uint64_t getValue() const;
+
+    /// operator uint64_t - Get the current primary statistic value.
+    operator uint64_t () const { return getValue(); }
+
+    /// operator++ - Increment the statistic by 1.
+    Statistic &operator ++() { return (*this += 1); }
+
+    /// operator+= - Increment the statistic by \arg addend.
+    Statistic &operator +=(const uint64_t addend);
+  };
+}
+
+#endif
+
diff --git a/include/klee/Statistics.h b/include/klee/Statistics.h
new file mode 100644
index 00000000..20ab2528
--- /dev/null
+++ b/include/klee/Statistics.h
@@ -0,0 +1,154 @@
+//===-- Statistics.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_STATISTICS_H
+#define KLEE_STATISTICS_H
+
+#include "Statistic.h"
+
+#include <vector>
+#include <string>
+#include <string.h>
+
+namespace klee {
+  class Statistic;
+  class StatisticRecord {
+    friend class StatisticManager;
+
+  private:
+    uint64_t *data;
+
+  public:    
+    StatisticRecord();
+    StatisticRecord(const StatisticRecord &s);
+    ~StatisticRecord() { delete[] data; }
+    
+    void zero();
+
+    uint64_t getValue(const Statistic &s) const; 
+    void incrementValue(const Statistic &s, uint64_t addend) const;
+    StatisticRecord &operator =(const StatisticRecord &s);
+    StatisticRecord &operator +=(const StatisticRecord &sr);
+  };
+
+  class StatisticManager {
+  private:
+    bool enabled;
+    std::vector<Statistic*> stats;
+    uint64_t *globalStats;
+    uint64_t *indexedStats;
+    StatisticRecord *contextStats;
+    unsigned index;
+
+  public:
+    StatisticManager();
+    ~StatisticManager();
+
+    void useIndexedStats(unsigned totalIndices);
+
+    StatisticRecord *getContext();
+    void setContext(StatisticRecord *sr); /* null to reset */
+
+    void setIndex(unsigned i) { index = i; }
+    unsigned getIndex() { return index; }
+    unsigned getNumStatistics() { return stats.size(); }
+    Statistic &getStatistic(unsigned i) { return *stats[i]; }
+    
+    void registerStatistic(Statistic &s);
+    void incrementStatistic(Statistic &s, uint64_t addend);
+    uint64_t getValue(const Statistic &s) const;
+    void incrementIndexedValue(const Statistic &s, unsigned index, 
+                               uint64_t addend) const;
+    uint64_t getIndexedValue(const Statistic &s, unsigned index) const;
+    void setIndexedValue(const Statistic &s, unsigned index, uint64_t value);
+    int getStatisticID(const std::string &name) const;
+    Statistic *getStatisticByName(const std::string &name) const;
+  };
+
+  extern StatisticManager *theStatisticManager;
+
+  inline void StatisticManager::incrementStatistic(Statistic &s, 
+                                                   uint64_t addend) {
+    if (enabled) {
+      globalStats[s.id] += addend;
+      if (indexedStats) {
+        indexedStats[index*stats.size() + s.id] += addend;
+        if (contextStats)
+          contextStats->data[s.id] += addend;
+      }
+    }
+  }
+
+  inline StatisticRecord *StatisticManager::getContext() {
+    return contextStats;
+  }
+  inline void StatisticManager::setContext(StatisticRecord *sr) {
+    contextStats = sr;
+  }
+
+  inline void StatisticRecord::zero() {
+    ::memset(data, 0, sizeof(*data)*theStatisticManager->getNumStatistics());
+  }
+
+  inline StatisticRecord::StatisticRecord() 
+    : data(new uint64_t[theStatisticManager->getNumStatistics()]) {
+    zero();
+  }
+
+  inline StatisticRecord::StatisticRecord(const StatisticRecord &s) 
+    : data(new uint64_t[theStatisticManager->getNumStatistics()]) {
+    ::memcpy(data, s.data, 
+             sizeof(*data)*theStatisticManager->getNumStatistics());
+  }
+
+  inline StatisticRecord &StatisticRecord::operator=(const StatisticRecord &s) {
+    ::memcpy(data, s.data, 
+             sizeof(*data)*theStatisticManager->getNumStatistics());
+    return *this;
+  }
+
+  inline void StatisticRecord::incrementValue(const Statistic &s, 
+                                              uint64_t addend) const {
+    data[s.id] += addend;
+  }
+  inline uint64_t StatisticRecord::getValue(const Statistic &s) const { 
+    return data[s.id]; 
+  }
+
+  inline StatisticRecord &
+  StatisticRecord::operator +=(const StatisticRecord &sr) {
+    unsigned nStats = theStatisticManager->getNumStatistics();
+    for (unsigned i=0; i<nStats; i++)
+      data[i] += sr.data[i];
+    return *this;
+  }
+
+  inline uint64_t StatisticManager::getValue(const Statistic &s) const {
+    return globalStats[s.id];
+  }
+
+  inline void StatisticManager::incrementIndexedValue(const Statistic &s, 
+                                                      unsigned index,
+                                                      uint64_t addend) const {
+    indexedStats[index*stats.size() + s.id] += addend;
+  }
+
+  inline uint64_t StatisticManager::getIndexedValue(const Statistic &s, 
+                                                    unsigned index) const {
+    return indexedStats[index*stats.size() + s.id];
+  }
+
+  inline void StatisticManager::setIndexedValue(const Statistic &s, 
+                                                unsigned index,
+                                                uint64_t value) {
+    indexedStats[index*stats.size() + s.id] = value;
+  }
+}
+
+#endif
diff --git a/include/klee/TimerStatIncrementer.h b/include/klee/TimerStatIncrementer.h
new file mode 100644
index 00000000..35495d8b
--- /dev/null
+++ b/include/klee/TimerStatIncrementer.h
@@ -0,0 +1,32 @@
+//===-- TimerStatIncrementer.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_TIMERSTATINCREMENTER_H
+#define KLEE_TIMERSTATINCREMENTER_H
+
+#include "klee/Statistics.h"
+#include "klee/Internal/Support/Timer.h"
+
+namespace klee {
+  class TimerStatIncrementer {
+  private:
+    WallTimer timer;
+    Statistic &statistic;
+
+  public:
+    TimerStatIncrementer(Statistic &_statistic) : statistic(_statistic) {}
+    ~TimerStatIncrementer() {
+      statistic += timer.check(); 
+    };
+
+    uint64_t check() { return timer.check(); }
+  };
+}
+
+#endif
diff --git a/include/klee/klee.h b/include/klee/klee.h
new file mode 100644
index 00000000..698a61c4
--- /dev/null
+++ b/include/klee/klee.h
@@ -0,0 +1,120 @@
+//===-- 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__
+
+#ifdef __cplusplus
+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. */
+  void klee_define_fixed_object(void *addr, unsigned nbytes);
+
+  /* make the contents of the object pointed to by addr symbolic. addr
+   * should always be the start of the object and nbytes must be its
+   * entire size. name is an optional name (can be the empty string)
+   */
+  void klee_make_symbolic_name(void *addr, unsigned nbytes, 
+			       const char *name);
+
+  void klee_make_symbolic(void *addr, unsigned nbytes);  
+  
+  /* Return symbolic value in the (signed) interval [begin,end) */
+  int klee_range(int begin, int end, const char *name);
+
+  /* Return a symbolic integer */
+  int klee_int(const char *name);
+
+  void *klee_malloc_n(unsigned nelems, unsigned size, unsigned alignment);
+
+  /* terminate the state without generating a test file */
+  __attribute__((noreturn))
+  void klee_silent_exit(int status);
+  
+  __attribute__((noreturn))
+  void klee_abort(void);  
+
+  /** Report an error and terminate the state. */
+  __attribute__((noreturn))
+  void klee_report_error(const char *file, 
+			 int line, 
+			 const char *message, 
+			 const char *suffix);
+  
+  /* called by checking code to get size of memory. */
+  unsigned klee_get_obj_size(void *ptr);
+  
+  /* print the tree associated w/ a given expression. */
+  void klee_print_expr(const char *msg, ...);
+  
+  /* NB: this *does not* fork n times and return [0,n) in children.
+   * It makes n be symbolic and returns: caller must compare N times.
+   */
+  unsigned klee_choose(unsigned n);
+  
+  /* special klee assert macro. this assert should be used when path consistency
+   * across platforms is desired (e.g., in tests).
+   * NB: __assert_fail is a klee "special" function
+   */
+# define klee_assert(expr)                                              \
+  ((expr)                                                               \
+   ? (void) (0)                                                         \
+   : __assert_fail (#expr, __FILE__, __LINE__, __PRETTY_FUNCTION__))    \
+
+  /* Return true if the given value is symbolic (represented by an
+   * expression) in the current state. This is primarily for debugging
+   * and writing tests but can also be used to enable prints in replay
+   * mode.
+   */
+  unsigned klee_is_symbolic(unsigned n);
+
+
+  /* The following intrinsics are primarily intended for internal use
+     and may have peculiar semantics. */
+
+  void klee_assume(unsigned condition);
+  void klee_warning(const char *message);
+  void klee_warning_once(const char *message);
+  void klee_prefer_cex(void *object, unsigned condition);
+  void klee_mark_global(void *object);
+
+  /* Return a possible constant value for the input expression. This
+     allows programs to forcibly concretize values on their own. */
+  unsigned klee_get_value(unsigned expr);
+
+  /* Ensure that memory in the range [address, address+size) is
+     accessible to the program. If some byte in the range is not
+     accessible an error will be generated and the state
+     terminated. 
+  
+     The current implementation requires both address and size to be
+     constants and that the range lie within a single object. */
+  void klee_check_memory_access(const void *address, unsigned size);
+
+  /* Enable/disable forking. */
+  void klee_set_forking(unsigned enable);
+
+  /* klee_alias_function("foo", "bar") will replace, at runtime (on
+     the current path and all paths spawned on the current path), all
+     calls to foo() by calls to bar().  foo() and bar() have to exist
+     and have identical types.  Use klee_alias_function("foo", "foo")
+     to undo.  Be aware that some special functions, such as exit(),
+     may not always work. */
+  void klee_alias_function(const char* fn_name, const char* new_fn_name);
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif /* __KLEE_H__ */
diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h
new file mode 100644
index 00000000..19f89a03
--- /dev/null
+++ b/include/klee/util/Assignment.h
@@ -0,0 +1,100 @@
+//===-- Assignment.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_UTIL_ASSIGNMENT_H
+#define KLEE_UTIL_ASSIGNMENT_H
+
+#include <map>
+
+#include "klee/util/ExprEvaluator.h"
+
+// FIXME: Rename?
+
+namespace klee {
+  class Array;
+
+  class Assignment {
+  public:
+    typedef std::map<const Array*, std::vector<unsigned char> > bindings_ty;
+
+    bool allowFreeValues;
+    bindings_ty bindings;
+    
+  public:
+    Assignment(bool _allowFreeValues=false) 
+      : allowFreeValues(_allowFreeValues) {}
+    Assignment(std::vector<const Array*> &objects, 
+               std::vector< std::vector<unsigned char> > &values,
+               bool _allowFreeValues=false) 
+      : allowFreeValues(_allowFreeValues){
+      std::vector< std::vector<unsigned char> >::iterator valIt = 
+        values.begin();
+      for (std::vector<const Array*>::iterator it = objects.begin(),
+             ie = objects.end(); it != ie; ++it) {
+        const Array *os = *it;
+        std::vector<unsigned char> &arr = *valIt;
+        bindings.insert(std::make_pair(os, arr));
+        ++valIt;
+      }
+    }
+    
+    ref<Expr> evaluate(const Array *mo, unsigned index) const;
+    ref<Expr> evaluate(ref<Expr> e);
+
+    template<typename InputIterator>
+    bool satisfies(InputIterator begin, InputIterator end);
+  };
+  
+  class AssignmentEvaluator : public ExprEvaluator {
+    const Assignment &a;
+
+  protected:
+    ref<Expr> getInitialValue(const Array &mo, unsigned index) {
+      return a.evaluate(&mo, index);
+    }
+    
+  public:
+    AssignmentEvaluator(const Assignment &_a) : a(_a) {}    
+  };
+
+  /***/
+
+  inline ref<Expr> Assignment::evaluate(const Array *array, 
+                                        unsigned index) const {
+    bindings_ty::const_iterator it = bindings.find(array);
+    if (it!=bindings.end() && index<it->second.size()) {
+      return ref<Expr>(it->second[index], Expr::Int8);
+    } else {
+      if (allowFreeValues) {
+        return ReadExpr::create(UpdateList(array, true, 0), 
+                                ref<Expr>(index, Expr::Int32));
+      } else {
+        return ref<Expr>(0, Expr::Int8);
+      }
+    }
+  }
+
+  inline ref<Expr> Assignment::evaluate(ref<Expr> e) { 
+    AssignmentEvaluator v(*this);
+    return v.visit(e); 
+  }
+
+  template<typename InputIterator>
+  inline bool Assignment::satisfies(InputIterator begin, InputIterator end) {
+    AssignmentEvaluator v(*this);
+    for (; begin!=end; ++begin) {
+      ref<Expr> res = v.visit(*begin);
+      if (!res.isConstant() || !res.getConstantValue())
+        return false;
+    }
+    return true;
+  }
+}
+
+#endif
diff --git a/include/klee/util/BitArray.h b/include/klee/util/BitArray.h
new file mode 100644
index 00000000..6f887600
--- /dev/null
+++ b/include/klee/util/BitArray.h
@@ -0,0 +1,42 @@
+//===-- BitArray.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_UTIL_BITARRAY_H
+#define KLEE_UTIL_BITARRAY_H
+
+namespace klee {
+
+  // XXX would be nice not to have
+  // two allocations here for allocated
+  // BitArrays
+class BitArray {
+private:
+  uint32_t *bits;
+  
+protected:
+  static uint32_t length(unsigned size) { return (size+31)/32; }
+
+public:
+  BitArray(unsigned size, bool value = false) : bits(new uint32_t[length(size)]) {
+    memset(bits, value?0xFF:0, sizeof(*bits)*length(size));
+  }
+  BitArray(const BitArray &b, unsigned size) : bits(new uint32_t[length(size)]) {
+    memcpy(bits, b.bits, sizeof(*bits)*length(size));
+  }
+  ~BitArray() { delete[] bits; }
+
+  bool get(unsigned idx) { return (bool) ((bits[idx/32]>>(idx&0x1F))&1); }
+  void set(unsigned idx) { bits[idx/32] |= 1<<(idx&0x1F); }
+  void unset(unsigned idx) { bits[idx/32] &= ~(1<<(idx&0x1F)); }
+  void set(unsigned idx, bool value) { if (value) set(idx); else unset(idx); }
+};
+
+} // End klee namespace
+
+#endif
diff --git a/include/klee/util/Bits.h b/include/klee/util/Bits.h
new file mode 100644
index 00000000..ffbda09e
--- /dev/null
+++ b/include/klee/util/Bits.h
@@ -0,0 +1,102 @@
+//===-- Bits.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_UTIL_BITS_H
+#define KLEE_UTIL_BITS_H
+
+#include "llvm/Support/DataTypes.h"
+
+namespace klee {
+  namespace bits32 {
+    // @pre(0 <= N <= 32)
+    // @post(retval = max([truncateToNBits(i,N) for i in naturals()]))
+    inline unsigned maxValueOfNBits(unsigned N) {
+      if (N==0)
+        return 0;
+      return ((unsigned) -1) >> (32 - N);
+    }
+
+    // @pre(0 < N <= 32)
+    inline unsigned truncateToNBits(unsigned x, unsigned N) {
+      return x&(((unsigned) -1) >> (32 - N));
+    }
+
+    inline unsigned withoutRightmostBit(unsigned x) {
+      return x&(x-1);
+    }
+
+    inline unsigned isolateRightmostBit(unsigned x) {
+      return x&-x;
+    }
+
+    inline unsigned isPowerOfTwo(unsigned x) {
+      if (x==0) return 0;
+      return !(x&(x-1));
+    }
+
+    // @pre(withoutRightmostBit(x) == 0)
+    // @post((1 << retval) == x)
+    inline unsigned indexOfSingleBit(unsigned x) {
+      unsigned res = 0;
+      if (x&0xFFFF0000) res += 16;
+      if (x&0xFF00FF00) res += 8;
+      if (x&0xF0F0F0F0) res += 4;
+      if (x&0xCCCCCCCC) res += 2;
+      if (x&0xAAAAAAAA) res += 1;
+      return res;
+    } 
+
+    inline unsigned indexOfRightmostBit(unsigned x) {
+      return indexOfSingleBit(isolateRightmostBit(x));
+    }
+  }
+
+  namespace bits64 {
+    // @pre(0 <= N <= 32)
+    // @post(retval = max([truncateToNBits(i,N) for i in naturals()]))
+    inline uint64_t maxValueOfNBits(unsigned N) {
+      if (N==0)
+        return 0;
+      return ((uint64_t) (int64_t) -1) >> (64 - N);
+    }
+    
+    // @pre(0 < N <= 64)
+    inline uint64_t truncateToNBits(uint64_t x, unsigned N) {
+      return x&(((uint64_t) (int64_t) -1) >> (64 - N));
+    }
+
+    inline uint64_t withoutRightmostBit(uint64_t x) {
+      return x&(x-1);
+    }
+
+    inline uint64_t isolateRightmostBit(uint64_t x) {
+      return x&-x;
+    }
+
+    inline uint64_t isPowerOfTwo(uint64_t x) {
+      if (x==0) return 0;
+      return !(x&(x-1));
+    }
+
+    // @pre((x&(x-1)) == 0)
+    // @post((1 << retval) == x)
+    inline unsigned indexOfSingleBit(uint64_t x) {
+      unsigned res = bits32::indexOfSingleBit((unsigned) (x | (x>>32)));
+      if (x&((uint64_t) 0xFFFFFFFF << 32))
+	  res += 32;
+      return res;
+    } 
+
+    inline uint64_t indexOfRightmostBit(uint64_t x) {
+      return indexOfSingleBit(isolateRightmostBit(x));
+    }
+  }
+} // End klee namespace
+
+#endif
diff --git a/include/klee/util/ExprEvaluator.h b/include/klee/util/ExprEvaluator.h
new file mode 100644
index 00000000..be98942d
--- /dev/null
+++ b/include/klee/util/ExprEvaluator.h
@@ -0,0 +1,39 @@
+//===-- ExprEvaluator.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_EXPREVALUATOR_H
+#define KLEE_EXPREVALUATOR_H
+
+#include "klee/Expr.h"
+#include "klee/util/ExprVisitor.h"
+
+namespace klee {
+  class ExprEvaluator : public ExprVisitor {
+  protected:
+    Action evalRead(const UpdateList &ul, unsigned index);
+    Action visitRead(const ReadExpr &re);
+      
+    Action protectedDivOperation(const BinaryExpr &e);
+    Action visitUDiv(const UDivExpr &e);
+    Action visitSDiv(const SDivExpr &e);
+    Action visitURem(const URemExpr &e);
+    Action visitSRem(const SRemExpr &e);
+      
+  public:
+    ExprEvaluator() {}
+
+    // override to implement evaluation, this function is called to
+    // get the initial value for a symbolic byte. if the value is
+    // unknown then the user can simply return a ReadExpr at version 0
+    // of this MemoryObject.
+    virtual ref<Expr> getInitialValue(const Array& os, unsigned index) = 0;
+  };
+}
+
+#endif
diff --git a/include/klee/util/ExprHashMap.h b/include/klee/util/ExprHashMap.h
new file mode 100644
index 00000000..d9f95bff
--- /dev/null
+++ b/include/klee/util/ExprHashMap.h
@@ -0,0 +1,48 @@
+//===-- ExprHashMap.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_EXPRHASHMAP_H
+#define KLEE_EXPRHASHMAP_H
+
+#include "klee/Expr.h"
+#include <tr1/unordered_map>
+#include <tr1/unordered_set>
+
+namespace klee {
+
+  namespace util {
+    struct ExprHash  {
+      unsigned operator()(const ref<Expr> e) const {
+        return e.hash();
+      }
+    };
+    
+    struct ExprCmp {
+      bool operator()(const ref<Expr> &a, const ref<Expr> &b) const {
+        return a==b;
+      }
+    };
+  }
+  
+  template<class T> 
+  class ExprHashMap : 
+
+    public std::tr1::unordered_map<ref<Expr>,
+				   T,
+				   klee::util::ExprHash,
+				   klee::util::ExprCmp> {
+  };
+  
+  typedef std::tr1::unordered_set<ref<Expr>,
+				  klee::util::ExprHash,
+				  klee::util::ExprCmp> ExprHashSet;
+
+}
+
+#endif
diff --git a/include/klee/util/ExprPPrinter.h b/include/klee/util/ExprPPrinter.h
new file mode 100644
index 00000000..a1961e2b
--- /dev/null
+++ b/include/klee/util/ExprPPrinter.h
@@ -0,0 +1,58 @@
+//===-- ExprPPrinter.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_EXPRPPRINTER_H
+#define KLEE_EXPRPPRINTER_H
+
+#include "klee/Expr.h"
+
+namespace klee {
+  class ConstraintManager;
+
+  class ExprPPrinter {
+  protected:
+    ExprPPrinter() {}
+    
+  public:
+    static ExprPPrinter *create(std::ostream &os);
+
+    virtual ~ExprPPrinter() {}
+
+    virtual void setNewline(const std::string &newline) = 0;
+    virtual void reset() = 0;
+    virtual void scan(const ref<Expr> &e) = 0;
+    virtual void print(const ref<Expr> &e, unsigned indent=0) = 0;
+
+    // utility methods
+
+    template<class Container>
+    void scan(Container c) {
+      scan(c.begin(), c.end());
+    }
+
+    template<class InputIterator>
+    void scan(InputIterator it, InputIterator end) {
+      for (; it!=end; ++it)
+        scan(*it);
+    }
+
+    static void printOne(std::ostream &os, const char *message, 
+                         const ref<Expr> &e);
+
+    static void printConstraints(std::ostream &os,
+                                 const ConstraintManager &constraints);
+
+    static void printQuery(std::ostream &os,
+                           const ConstraintManager &constraints,
+                           const ref<Expr> &q);
+  };
+
+}
+
+#endif
diff --git a/include/klee/util/ExprRangeEvaluator.h b/include/klee/util/ExprRangeEvaluator.h
new file mode 100644
index 00000000..3729b5c2
--- /dev/null
+++ b/include/klee/util/ExprRangeEvaluator.h
@@ -0,0 +1,283 @@
+//===-- ExprRangeEvaluator.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_EXPRRANGEEVALUATOR_H
+#define KLEE_EXPRRANGEEVALUATOR_H
+
+#include "klee/Expr.h"
+#include "klee/util/Bits.h"
+
+namespace klee {
+
+/*
+class ValueType {
+public:
+  ValueType(); // empty range
+  ValueType(uint64_t value);
+  ValueType(uint64_t min, uint64_t max);
+  
+  bool mustEqual(const uint64_t b);
+  bool mustEqual(const ValueType &b);
+  bool mayEqual(const uint64_t b);  
+  bool mayEqual(const ValueType &b);
+
+  bool isFullRange(unsigned width);
+
+  ValueType set_union(ValueType &);
+  ValueType set_intersection(ValueType &);
+  ValueType set_difference(ValueType &);
+
+  ValueType binaryAnd(ValueType &);
+  ValueType binaryOr(ValueType &);
+  ValueType binaryXor(ValueType &);
+  ValueType concat(ValueType &, unsigned width);
+  ValueType add(ValueType &, unsigned width);
+  ValueType sub(ValueType &, unsigned width);
+  ValueType mul(ValueType &, unsigned width);
+  ValueType udiv(ValueType &, unsigned width);
+  ValueType sdiv(ValueType &, unsigned width);
+  ValueType urem(ValueType &, unsigned width);
+  ValueType srem(ValueType &, unsigned width);
+
+  uint64_t min();
+  uint64_t max();
+  int64_t minSigned(unsigned width);
+  int64_t maxSigned(unsigned width);
+}
+*/
+
+template<class T>
+class ExprRangeEvaluator {
+protected:
+  virtual T getInitialReadRange(const Array &os, T index) = 0;
+
+  T evalRead(const UpdateList &ul, T index);
+
+public:
+  ExprRangeEvaluator() {}
+  virtual ~ExprRangeEvaluator() {}
+
+  T evaluate(const ref<Expr> &e);
+};
+
+template<class T>
+T ExprRangeEvaluator<T>::evalRead(const UpdateList &ul,
+                                  T index) {
+  T res;
+
+  for (const UpdateNode *un=ul.head; un; un=un->next) {
+    T ui = evaluate(un->index);
+
+    if (ui.mustEqual(index)) {
+      return res.set_union(evaluate(un->value));
+    } else if (ui.mayEqual(index)) {
+      res = res.set_union(evaluate(un->value));
+      if (res.isFullRange(8)) {
+        return res;
+      } 
+    }
+  }
+
+  return res.set_union(getInitialReadRange(*ul.root, index));
+}
+
+template<class T>
+T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
+  switch (e.getKind()) {
+  case Expr::Constant:
+    return T(e.getConstantValue());
+
+  case Expr::NotOptimized: 
+    break;
+
+  case Expr::Read: {
+    const ReadExpr *re = static_ref_cast<const ReadExpr>(e);
+    T index = evaluate(re->index);
+
+    assert(re->getWidth()==Expr::Int8 && "unexpected multibyte read");
+
+    return evalRead(re->updates, index);
+  }
+
+  case Expr::Select: {
+    const SelectExpr *se = static_ref_cast<const SelectExpr>(e);
+    T cond = evaluate(se->cond);
+      
+    if (cond.mustEqual(1)) {
+      return evaluate(se->trueExpr);
+    } else if (cond.mustEqual(0)) {
+      return evaluate(se->falseExpr);
+    } else {
+      return evaluate(se->trueExpr).set_union(evaluate(se->falseExpr));
+    }
+  }
+
+    // XXX these should be unrolled to ensure nice inline
+  case Expr::Concat: {
+    const Expr *ep = e.get();
+    T res(0);
+    for (unsigned i=0; i<ep->getNumKids(); i++)
+      res = res.concat(evaluate(ep->getKid(i)),8);
+    return res;
+  }
+
+    // Arithmetic
+
+  case Expr::Add: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    unsigned width = be->left.getWidth();
+    return evaluate(be->left).add(evaluate(be->right), width);
+  }
+  case Expr::Sub: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    unsigned width = be->left.getWidth();
+    return evaluate(be->left).sub(evaluate(be->right), width);
+  }
+  case Expr::Mul: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    unsigned width = be->left.getWidth();
+    return evaluate(be->left).mul(evaluate(be->right), width);
+  }
+  case Expr::UDiv: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    unsigned width = be->left.getWidth();
+    return evaluate(be->left).udiv(evaluate(be->right), width);
+  }
+  case Expr::SDiv: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    unsigned width = be->left.getWidth();
+    return evaluate(be->left).sdiv(evaluate(be->right), width);
+  }
+  case Expr::URem: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    unsigned width = be->left.getWidth();
+    return evaluate(be->left).urem(evaluate(be->right), width);
+  }
+  case Expr::SRem: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    unsigned width = be->left.getWidth();
+    return evaluate(be->left).srem(evaluate(be->right), width);
+  }
+
+    // Binary
+
+  case Expr::And: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    return evaluate(be->left).binaryAnd(evaluate(be->right));
+  }
+  case Expr::Or: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    return evaluate(be->left).binaryOr(evaluate(be->right));
+  }
+  case Expr::Xor: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    return evaluate(be->left).binaryXor(evaluate(be->right));
+  }
+  case Expr::Shl: {
+    //    BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+    //    unsigned width = be->left.getWidth();
+    //    return evaluate(be->left).shl(evaluate(be->right), width);
+    break;
+  }
+  case Expr::LShr: {
+    //    BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+    //    unsigned width = be->left.getWidth();
+    //    return evaluate(be->left).lshr(evaluate(be->right), width);
+    break;
+  }
+  case Expr::AShr: {
+    //    BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+    //    unsigned width = be->left.getWidth();
+    //    return evaluate(be->left).ashr(evaluate(be->right), width);
+    break;
+  }
+
+    // Comparison
+
+  case Expr::Eq: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    T left = evaluate(be->left);
+    T right = evaluate(be->right);
+      
+    if (left.mustEqual(right)) {
+      return T(1);
+    } else if (!left.mayEqual(right)) {
+      return T(0);
+    }
+    break;
+  }
+
+  case Expr::Ult: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    T left = evaluate(be->left);
+    T right = evaluate(be->right);
+      
+    if (left.max() < right.min()) {
+      return T(1);
+    } else if (left.min() >= right.max()) {
+      return T(0);
+    }
+    break;
+  }
+  case Expr::Ule: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    T left = evaluate(be->left);
+    T right = evaluate(be->right);
+      
+    if (left.max() <= right.min()) {
+      return T(1);
+    } else if (left.min() > right.max()) {
+      return T(0);
+    }
+    break;
+  }
+  case Expr::Slt: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    T left = evaluate(be->left);
+    T right = evaluate(be->right);
+    unsigned bits = be->left.getWidth();
+
+    if (left.maxSigned(bits) < right.minSigned(bits)) {
+      return T(1);
+    } else if (left.minSigned(bits) >= right.maxSigned(bits)) {
+      return T(0);
+    }
+    break;
+  }
+  case Expr::Sle: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    T left = evaluate(be->left);
+    T right = evaluate(be->right);
+    unsigned bits = be->left.getWidth();
+      
+    if (left.maxSigned(bits) <= right.minSigned(bits)) {
+      return T(1);
+    } else if (left.minSigned(bits) > right.maxSigned(bits)) {
+      return T(0);
+    }
+    break;
+  }
+
+  case Expr::Ne:
+  case Expr::Ugt:
+  case Expr::Uge:
+  case Expr::Sgt:
+  case Expr::Sge:
+    assert(0 && "invalid expressions (uncanonicalized)");
+
+  default:
+    break;
+  }
+
+  return T(0, bits64::maxValueOfNBits(e.getWidth()));
+}
+
+}
+
+#endif
diff --git a/include/klee/util/ExprUtil.h b/include/klee/util/ExprUtil.h
new file mode 100644
index 00000000..a81c299f
--- /dev/null
+++ b/include/klee/util/ExprUtil.h
@@ -0,0 +1,43 @@
+//===-- ExprUtil.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_EXPRUTIL_H
+#define KLEE_EXPRUTIL_H
+
+#include <vector>
+
+namespace klee {
+  class Array;
+  class Expr;
+  class ReadExpr;
+  template<typename T> class ref;
+
+  /// Find all ReadExprs used in the expression DAG. If visitUpdates
+  /// is true then this will including those reachable by traversing
+  /// update lists. Note that this may be slow and return a large
+  /// number of results.
+  void findReads(ref<Expr> e, 
+                 bool visitUpdates,
+                 std::vector< ref<ReadExpr> > &result);
+  
+  /// Return a list of all unique symbolic objects referenced by the given
+  /// expression.
+  void findSymbolicObjects(ref<Expr> e,
+                           std::vector<const Array*> &results);
+
+  /// Return a list of all unique symbolic objects referenced by the
+  /// given expression range.
+  template<typename InputIterator>
+  void findSymbolicObjects(InputIterator begin, 
+                           InputIterator end,
+                           std::vector<const Array*> &results);
+
+}
+
+#endif
diff --git a/include/klee/util/ExprVisitor.h b/include/klee/util/ExprVisitor.h
new file mode 100644
index 00000000..8f8617e3
--- /dev/null
+++ b/include/klee/util/ExprVisitor.h
@@ -0,0 +1,95 @@
+//===-- ExprVisitor.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_EXPRVISITOR_H
+#define KLEE_EXPRVISITOR_H
+
+#include "ExprHashMap.h"
+
+namespace klee {
+  class ExprVisitor {
+  protected:
+    // typed variant, but non-virtual for efficiency
+    class Action {
+    public:
+      enum Kind { SkipChildren, DoChildren, ChangeTo };
+
+    private:
+      //      Action() {}
+      Action(Kind _kind) 
+        : kind(_kind), argument(0,Expr::Bool) {}
+      Action(Kind _kind, const ref<Expr> &_argument) 
+        : kind(_kind), argument(_argument) {}
+
+      friend class ExprVisitor;
+
+    public:
+      Kind kind;
+      ref<Expr> argument;
+
+      static Action changeTo(const ref<Expr> &expr) { return Action(ChangeTo,expr); }
+      static Action doChildren() { return Action(DoChildren); }
+      static Action skipChildren() { return Action(SkipChildren); }
+    };
+
+  protected:
+    explicit
+    ExprVisitor(bool _recursive=false) : recursive(_recursive) {}
+    virtual ~ExprVisitor() {}
+
+    virtual Action visitExpr(const Expr&);
+    virtual Action visitExprPost(const Expr&);
+
+    virtual Action visitNotOptimized(const NotOptimizedExpr&);
+    virtual Action visitRead(const ReadExpr&);
+    virtual Action visitSelect(const SelectExpr&);
+    virtual Action visitConcat(const ConcatExpr&);
+    virtual Action visitExtract(const ExtractExpr&);
+    virtual Action visitZExt(const ZExtExpr&);
+    virtual Action visitSExt(const SExtExpr&);
+    virtual Action visitAdd(const AddExpr&);
+    virtual Action visitSub(const SubExpr&);
+    virtual Action visitMul(const MulExpr&);
+    virtual Action visitUDiv(const UDivExpr&);
+    virtual Action visitSDiv(const SDivExpr&);
+    virtual Action visitURem(const URemExpr&);
+    virtual Action visitSRem(const SRemExpr&);
+    virtual Action visitAnd(const AndExpr&);
+    virtual Action visitOr(const OrExpr&);
+    virtual Action visitXor(const XorExpr&);
+    virtual Action visitShl(const ShlExpr&);
+    virtual Action visitLShr(const LShrExpr&);
+    virtual Action visitAShr(const AShrExpr&);
+    virtual Action visitEq(const EqExpr&);
+    virtual Action visitNe(const NeExpr&);
+    virtual Action visitUlt(const UltExpr&);
+    virtual Action visitUle(const UleExpr&);
+    virtual Action visitUgt(const UgtExpr&);
+    virtual Action visitUge(const UgeExpr&);
+    virtual Action visitSlt(const SltExpr&);
+    virtual Action visitSle(const SleExpr&);
+    virtual Action visitSgt(const SgtExpr&);
+    virtual Action visitSge(const SgeExpr&);
+
+  private:
+    typedef ExprHashMap< ref<Expr> > visited_ty;
+    visited_ty visited;
+    bool recursive;
+
+    ref<Expr> visitActual(const ref<Expr> &e);
+    
+  public:
+    // apply the visitor to the expression and return a possibly
+    // modified new expression.
+    ref<Expr> visit(const ref<Expr> &e);
+  };
+
+}
+
+#endif
diff --git a/include/klee/util/Ref.h b/include/klee/util/Ref.h
new file mode 100644
index 00000000..a70b09cf
--- /dev/null
+++ b/include/klee/util/Ref.h
@@ -0,0 +1,303 @@
+//===-- Ref.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_REF_H
+#define KLEE_REF_H
+
+#include <assert.h>
+
+class Expr;
+class BinaryExpr;
+class CastExpr;
+class CmpExpr;
+
+class ConstantExpr;
+class ReadExpr;
+class UpdateNode;
+class NotOptimizedExpr;
+class ReadExpr;
+class SelectExpr;
+class ConcatExpr;
+class ExtractExpr;
+class ZExtExpr;
+class SExtExpr;
+class AddExpr;
+class SubExpr;
+class MulExpr;
+class UDivExpr;
+class SDivExpr;
+class URemExpr;
+class SRemExpr;
+class AndExpr;
+class OrExpr;
+class XorExpr;
+class ShlExpr;
+class LShrExpr;
+class AShrExpr;
+class EqExpr;
+class NeExpr;
+class UltExpr;
+class UleExpr;
+class UgtExpr;
+class UgeExpr;
+class SltExpr;
+class SleExpr;
+class SgtExpr;
+class SgeExpr;
+class KModule;
+
+  class ExprVisitor;
+  class StackFrame;
+  class ObjectState;
+
+template<class T>
+class ref {
+public:
+  // default constructor: create a NULL reference
+  ref() : constantWidth(Expr::InvalidWidth) {
+    contents.ptr = 0;
+  }
+
+private:
+  // if NotConstant, not this ref is not a constant.
+  // otherwise, it's the width of the constant.
+  Expr::Width constantWidth;
+  static const Expr::Width NotConstant = (Expr::Width) 0;
+  
+  union {
+    T *ptr;
+    uint64_t val;
+  } contents;
+  
+  void inc() {
+    if (constantWidth == NotConstant &&
+        contents.ptr) {
+      contents.ptr->refCount++;
+    }
+  }
+  
+  void dec() {
+    if (constantWidth == NotConstant &&
+        contents.ptr &&
+        --contents.ptr->refCount == 0) {
+      delete contents.ptr;
+    }
+  }  
+
+  friend class ExprVisitor;
+  friend class Cell;
+  friend class ObjectState;
+  friend class KModule;
+
+public:
+  template<class U> friend class ref;
+  template<class U> friend U* dyn_ref_cast(ref &src);
+  template<class U> friend const U* dyn_ref_cast(const ref &src);
+  template<class U> friend U* static_ref_cast(ref &src);
+  template<class U> friend const U* static_ref_cast(const ref &src);
+
+  // constructor from pointer
+  ref(T *p) : constantWidth(NotConstant) {
+    contents.ptr = p;
+    inc();
+  }
+
+  // construct from constant
+  ref(uint64_t val, Expr::Width w) : constantWidth(w) {
+    contents.val = val;
+  }
+  
+  // normal copy constructor
+  ref (const ref<T> &r)
+    : constantWidth(r.constantWidth), contents(r.contents) {
+    inc();
+  }
+  
+  // conversion constructor
+  template<class U>
+  ref (const ref<U> &r) {
+    constantWidth = r.constantWidth;
+    contents.val = r.contents.val;
+    inc();
+  }
+  
+  // pointer operations
+  T *get () {
+    // demand(constantWidth == NotConstant, "deref of constant");
+
+    // allocate 
+    if (constantWidth != NotConstant) {
+      contents.ptr = dynamic_cast<T*>(Expr::createConstant(contents.val, constantWidth));
+      assert(contents.ptr && "error with lazy constant initialization");
+      constantWidth = NotConstant;
+      
+      inc();
+    }
+    return contents.ptr;
+  }
+
+  T *get () const {
+    assert(constantWidth == NotConstant && "deref of constant");
+    return contents.ptr;
+  }
+
+  // method calls for the constant optimization
+  bool isConstant() const {
+    if (constantWidth != NotConstant) {
+      return true;
+    } else if (contents.ptr) {
+      return contents.ptr->getKind() == Expr::Constant;
+    } else {
+      return false; // should never happen, but nice check
+    }
+  }
+
+  uint64_t getConstantValue() const {
+    if (constantWidth) {
+      return contents.val;
+    } else {
+      return contents.ptr->getConstantValue();
+    }
+  }
+
+  unsigned hash() const {
+    if (constantWidth) {
+      return Expr::hashConstant(contents.val, constantWidth);
+    } else {
+      return contents.ptr->hash();
+    }
+  }
+
+  unsigned computeHash() const {
+    if (isConstant()) {
+      return Expr::hashConstant(contents.val, constantWidth);
+    } else {
+      return contents.ptr->computeHash();
+    }
+  }
+
+  void rehash() const {
+    if (!isConstant())
+      contents.ptr->computeHash();
+  }
+  
+  Expr::Width getWidth() const {
+    if (constantWidth != NotConstant)
+      return constantWidth;
+    return contents.ptr->getWidth();
+  }
+
+  Expr::Kind getKind() const {
+    if (constantWidth != NotConstant)
+      return Expr::Constant;
+    return contents.ptr->getKind();
+  }
+
+  unsigned getNumKids() const {
+    if (constantWidth != NotConstant)
+      return 0;
+    return contents.ptr->getNumKids();
+  }
+
+  ref<Expr> getKid(unsigned k) {
+    if (constantWidth != NotConstant)
+      return 0;
+    return contents.ptr->getKid(k);
+  }
+
+  ~ref () { dec (); }
+
+  /* The copy assignment operator must also explicitly be defined,
+   * despite a redundant template. */
+  ref<T> &operator= (const ref<T> &r) {
+    dec();
+    constantWidth = r.constantWidth;
+    contents.val = r.contents.val;
+    inc();
+    
+    return *this;
+  }
+  
+  template<class U> ref<T> &operator= (const ref<U> &r) {
+    dec();
+    constantWidth = r.constantWidth;
+    contents.val = r.contents.val;
+    inc();
+    
+    return *this;
+  }
+
+  bool isNull() const { return !constantWidth && !contents.ptr; }
+
+  // assumes non-null arguments
+  int compare(const ref &rhs) const {
+    Expr::Kind ak = getKind(), bk = rhs.getKind();
+    if (ak!=bk) 
+      return (ak < bk) ? -1 : 1;
+    if (ak==Expr::Constant) {
+      Expr::Width at = getWidth(), bt = rhs.getWidth();
+      if (at!=bt) 
+        return (at < bt) ? -1 : 1;
+      uint64_t av = getConstantValue(), bv = rhs.getConstantValue();
+      if (av<bv) {
+        return -1;
+      } else if (av>bv) {
+        return 1;
+      } else {
+        return 0;
+      }
+    } else {
+      return get()->compare(*rhs.get());
+    }
+  }
+
+  // assumes non-null arguments
+  bool operator<(const ref &rhs) const { return compare(rhs)<0; }
+  bool operator==(const ref &rhs) const { return compare(rhs)==0; }
+  bool operator!=(const ref &rhs) const { return compare(rhs)!=0; }
+};
+
+
+template<class T>
+inline std::ostream &operator<<(std::ostream &os, const ref<T> &e) {
+  if (e.isConstant()) {
+    os << e.getConstantValue();
+  } else {
+    os << *e.get();
+  }
+  return os;
+}
+
+template<class U>
+U* dyn_ref_cast(ref<Expr> &src) {
+  if (src.constantWidth != ref<Expr>::NotConstant)
+    return 0;
+    
+  return dynamic_cast<U*>(src.contents.ptr);
+}
+
+template<class U>
+const U* dyn_ref_cast(const ref<Expr> &src) {
+  if (src.constantWidth != ref<Expr>::NotConstant)
+    return 0;
+    
+  return dynamic_cast<const U*>(src.contents.ptr);
+}
+
+template<class U>
+U* static_ref_cast(ref<Expr> &src) {
+  return static_cast<U*>(src.contents.ptr);
+}
+
+template<class U>
+const U* static_ref_cast(const ref<Expr> &src) {
+  return static_cast<const U*>(src.contents.ptr);
+}
+
+#endif /* KLEE_REF_H */