Consolidated Expr-related include files into a single include/klee/Expr directory. This improves the organization of the code, and also makes it easier to reuse Expr outside KLEE.

79 files changed, 206 insertions, 201 deletions

diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h
index e2c6bffe..891e6f06 100644
--- a/include/klee/ExecutionState.h
+++ b/include/klee/ExecutionState.h
@@ -10,8 +10,8 @@
 #ifndef KLEE_EXECUTIONSTATE_H
 #define KLEE_EXECUTIONSTATE_H
 
-#include "klee/Constraints.h"
-#include "klee/Expr.h"
+#include "klee/Expr/Constraints.h"
+#include "klee/Expr/Expr.h"
 #include "klee/Internal/ADT/TreeStream.h"
 #include "klee/Internal/System/Time.h"
 #include "klee/MergeHandler.h"
diff --git a/include/klee/util/ArrayCache.h b/include/klee/Expr/ArrayCache.h
index bec6e15a..09eddf49 100644
--- a/include/klee/util/ArrayCache.h
+++ b/include/klee/Expr/ArrayCache.h
@@ -10,8 +10,8 @@
 #ifndef KLEE_ARRAYCACHE_H
 #define KLEE_ARRAYCACHE_H
 
-#include "klee/Expr.h"
-#include "klee/util/ArrayExprHash.h" // For klee::ArrayHashFn
+#include "klee/Expr/Expr.h"
+#include "klee/Expr/ArrayExprHash.h" // For klee::ArrayHashFn
 
 // FIXME: Remove this hack when we switch to C++11
 #ifdef _LIBCPP_VERSION
diff --git a/include/klee/util/ArrayExprHash.h b/include/klee/Expr/ArrayExprHash.h
index 05cb8692..04660fe0 100644
--- a/include/klee/util/ArrayExprHash.h
+++ b/include/klee/Expr/ArrayExprHash.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_ARRAYEXPRHASH_H
 #define KLEE_ARRAYEXPRHASH_H
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 #include "klee/TimerStatIncrementer.h"
 #include "klee/SolverStats.h"
 
diff --git a/include/klee/util/Assignment.h b/include/klee/Expr/Assignment.h
index 8d082791..ead459a9 100644
--- a/include/klee/util/Assignment.h
+++ b/include/klee/Expr/Assignment.h
@@ -10,11 +10,9 @@
 #ifndef KLEE_ASSIGNMENT_H
 #define KLEE_ASSIGNMENT_H
 
-#include <map>
-
-#include "klee/util/ExprEvaluator.h"
+#include "klee/Expr/ExprEvaluator.h"
 
-// FIXME: Rename?
+#include <map>
 
 namespace klee {
   class Array;
diff --git a/include/klee/Constraints.h b/include/klee/Expr/Constraints.h
index 08077293..b9bf3464 100644
--- a/include/klee/Constraints.h
+++ b/include/klee/Expr/Constraints.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_CONSTRAINTS_H
 #define KLEE_CONSTRAINTS_H
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 
 // FIXME: Currently we use ConstraintManager for two things: to pass
 // sets of constraints around, and to optimize constraints. We should
diff --git a/include/klee/Expr.h b/include/klee/Expr/Expr.h
index d4e4f7fa..d4e4f7fa 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr/Expr.h
diff --git a/include/klee/ExprBuilder.h b/include/klee/Expr/ExprBuilder.h
index 4a2c5cf4..4a2c5cf4 100644
--- a/include/klee/ExprBuilder.h
+++ b/include/klee/Expr/ExprBuilder.h
diff --git a/include/klee/util/ExprEvaluator.h b/include/klee/Expr/ExprEvaluator.h
index ed366f77..e0368203 100644
--- a/include/klee/util/ExprEvaluator.h
+++ b/include/klee/Expr/ExprEvaluator.h
@@ -10,8 +10,8 @@
 #ifndef KLEE_EXPREVALUATOR_H
 #define KLEE_EXPREVALUATOR_H
 
-#include "klee/Expr.h"
-#include "klee/util/ExprVisitor.h"
+#include "klee/Expr/Expr.h"
+#include "klee/Expr/ExprVisitor.h"
 
 namespace klee {
   class ExprEvaluator : public ExprVisitor {
diff --git a/include/klee/util/ExprHashMap.h b/include/klee/Expr/ExprHashMap.h
index 6477b7c9..2b0b3bda 100644
--- a/include/klee/util/ExprHashMap.h
+++ b/include/klee/Expr/ExprHashMap.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_EXPRHASHMAP_H
 #define KLEE_EXPRHASHMAP_H
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 
 #include <ciso646>
 #ifdef _LIBCPP_VERSION
diff --git a/include/klee/util/ExprPPrinter.h b/include/klee/Expr/ExprPPrinter.h
index f2537750..7541c132 100644
--- a/include/klee/util/ExprPPrinter.h
+++ b/include/klee/Expr/ExprPPrinter.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_EXPRPPRINTER_H
 #define KLEE_EXPRPPRINTER_H
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 
 namespace llvm {
   class raw_ostream;
diff --git a/include/klee/util/ExprRangeEvaluator.h b/include/klee/Expr/ExprRangeEvaluator.h
index b3011827..4d212764 100644
--- a/include/klee/util/ExprRangeEvaluator.h
+++ b/include/klee/Expr/ExprRangeEvaluator.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_EXPRRANGEEVALUATOR_H
 #define KLEE_EXPRRANGEEVALUATOR_H
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 #include "klee/util/Bits.h"
 
 namespace klee {
diff --git a/include/klee/util/ExprSMTLIBPrinter.h b/include/klee/Expr/ExprSMTLIBPrinter.h
index cf5df1c5..b042bfeb 100644
--- a/include/klee/util/ExprSMTLIBPrinter.h
+++ b/include/klee/Expr/ExprSMTLIBPrinter.h
@@ -11,13 +11,14 @@
 #ifndef KLEE_EXPRSMTLIBPRINTER_H
 #define KLEE_EXPRSMTLIBPRINTER_H
 
-#include <string>
-#include <set>
-#include <map>
-#include <klee/Constraints.h>
-#include <klee/Expr.h>
-#include <klee/util/PrintContext.h>
+#include <klee/Expr/Constraints.h>
+#include <klee/Expr/Expr.h>
 #include <klee/Solver.h>
+#include <klee/util/PrintContext.h>
+
+#include <map>
+#include <set>
+#include <string>
 
 namespace llvm {
 class raw_ostream;
diff --git a/include/klee/util/ExprUtil.h b/include/klee/Expr/ExprUtil.h
index 88db15f0..c6b2c2d7 100644
--- a/include/klee/util/ExprUtil.h
+++ b/include/klee/Expr/ExprUtil.h
@@ -10,7 +10,8 @@
 #ifndef KLEE_EXPRUTIL_H
 #define KLEE_EXPRUTIL_H
 
-#include "klee/util/ExprVisitor.h"
+#include "klee/Expr/ExprVisitor.h"
+
 #include <vector>
 
 namespace klee {
diff --git a/include/klee/util/ExprVisitor.h b/include/klee/Expr/ExprVisitor.h
index 03d4d77d..03d4d77d 100644
--- a/include/klee/util/ExprVisitor.h
+++ b/include/klee/Expr/ExprVisitor.h
diff --git a/include/expr/Lexer.h b/include/klee/Expr/Parser/Lexer.h
index 14ae7f85..14ae7f85 100644
--- a/include/expr/Lexer.h
+++ b/include/klee/Expr/Parser/Lexer.h
diff --git a/include/expr/Parser.h b/include/klee/Expr/Parser/Parser.h
index 6a34b8d0..c1888e26 100644
--- a/include/expr/Parser.h
+++ b/include/klee/Expr/Parser/Parser.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_PARSER_H
 #define KLEE_PARSER_H
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 
 #include <vector>
 #include <string>
diff --git a/include/klee/Internal/Module/Cell.h b/include/klee/Internal/Module/Cell.h
index 691c1c89..abdce3f6 100644
--- a/include/klee/Internal/Module/Cell.h
+++ b/include/klee/Internal/Module/Cell.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_CELL_H
 #define KLEE_CELL_H
 
-#include <klee/Expr.h>
+#include <klee/Expr/Expr.h>
 
 namespace klee {
   class MemoryObject;
diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index 476fb732..f320a5b6 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_SOLVER_H
 #define KLEE_SOLVER_H
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 #include "klee/SolverCmdLine.h"
 #include "klee/Internal/System/Time.h"
 
diff --git a/include/klee/util/PrintContext.h b/include/klee/util/PrintContext.h
index 9deaa207..de9094da 100644
--- a/include/klee/util/PrintContext.h
+++ b/include/klee/util/PrintContext.h
@@ -10,8 +10,10 @@
 #ifndef KLEE_PRINTCONTEXT_H
 #define KLEE_PRINTCONTEXT_H
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
+
 #include "llvm/Support/raw_ostream.h"
+
 #include <sstream>
 #include <string>
 #include <stack>
diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp
index fdf9c905..1a88e4ec 100644
--- a/lib/Core/AddressSpace.cpp
+++ b/lib/Core/AddressSpace.cpp
@@ -12,7 +12,7 @@
 #include "Memory.h"
 #include "TimingSolver.h"
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 #include "klee/TimerStatIncrementer.h"
 
 using namespace klee;
diff --git a/lib/Core/AddressSpace.h b/lib/Core/AddressSpace.h
index d8ba6f36..9e7e414a 100644
--- a/lib/Core/AddressSpace.h
+++ b/lib/Core/AddressSpace.h
@@ -12,7 +12,7 @@
 
 #include "ObjectHolder.h"
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 #include "klee/Internal/ADT/ImmutableMap.h"
 #include "klee/Internal/System/Time.h"
 
diff --git a/lib/Core/Context.cpp b/lib/Core/Context.cpp
index 8246e631..a74d5446 100644
--- a/lib/Core/Context.cpp
+++ b/lib/Core/Context.cpp
@@ -9,7 +9,7 @@
 
 #include "Context.h"
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 
 #include "llvm/IR/Type.h"
 #include "llvm/IR/DerivedTypes.h"
diff --git a/lib/Core/Context.h b/lib/Core/Context.h
index b2ea83f1..ecef646e 100644
--- a/lib/Core/Context.h
+++ b/lib/Core/Context.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_CONTEXT_H
 #define KLEE_CONTEXT_H
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 
 namespace klee {
 
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 3bce274c..15003b0e 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -11,7 +11,7 @@
 
 #include "klee/ExecutionState.h"
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 #include "klee/Internal/Module/Cell.h"
 #include "klee/Internal/Module/InstructionInfoTable.h"
 #include "klee/Internal/Module/KInstruction.h"
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 330665c0..5590af41 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -28,7 +28,11 @@
 #include "klee/Common.h"
 #include "klee/Config/Version.h"
 #include "klee/ExecutionState.h"
-#include "klee/Expr.h"
+#include "klee/Expr/Assignment.h"
+#include "klee/Expr/Expr.h"
+#include "klee/Expr/ExprPPrinter.h"
+#include "klee/Expr/ExprSMTLIBPrinter.h"
+#include "klee/Expr/ExprUtil.h"
 #include "klee/Internal/ADT/KTest.h"
 #include "klee/Internal/ADT/RNG.h"
 #include "klee/Internal/Module/Cell.h"
@@ -46,10 +50,6 @@
 #include "klee/SolverCmdLine.h"
 #include "klee/SolverStats.h"
 #include "klee/TimerStatIncrementer.h"
-#include "klee/util/Assignment.h"
-#include "klee/util/ExprPPrinter.h"
-#include "klee/util/ExprSMTLIBPrinter.h"
-#include "klee/util/ExprUtil.h"
 #include "klee/util/GetElementPtrTypeIterator.h"
 
 #include "llvm/ADT/SmallPtrSet.h"
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index eafdc2f7..e2aab56c 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -16,17 +16,18 @@
 #define KLEE_EXECUTOR_H
 
 #include "klee/ExecutionState.h"
-#include "klee/Interpreter.h"
+#include "klee/Expr/ArrayCache.h"
 #include "klee/Internal/Module/Cell.h"
 #include "klee/Internal/Module/KInstruction.h"
 #include "klee/Internal/Module/KModule.h"
 #include "klee/Internal/System/Time.h"
-#include "klee/util/ArrayCache.h"
-#include "llvm/Support/raw_ostream.h"
+#include "klee/Interpreter.h"
 
 #include "llvm/ADT/Twine.h"
+#include "llvm/Support/raw_ostream.h"
 
 #include "../Expr/ArrayExprOptimizer.h"
+
 #include <map>
 #include <memory>
 #include <set>
diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index 7b227eba..15125fe1 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -11,14 +11,12 @@
 
 #include "Context.h"
 
-#include "klee/Expr.h"
-#include "klee/Interpreter.h"
-#include "klee/Solver.h"
-
 #include "klee/Config/Version.h"
+#include "klee/Expr/Expr.h"
 #include "klee/Internal/Module/KModule.h"
-
 #include "klee/Internal/Support/ErrorHandling.h"
+#include "klee/Interpreter.h"
+#include "klee/Solver.h"
 
 #include "llvm/IR/Constants.h"
 #include "llvm/IR/DataLayout.h"
diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp
index 90000683..cc001660 100644
--- a/lib/Core/ImpliedValue.cpp
+++ b/lib/Core/ImpliedValue.cpp
@@ -10,13 +10,12 @@
 #include "ImpliedValue.h"
 
 #include "Context.h"
-#include "klee/Constraints.h"
-#include "klee/Expr.h"
-#include "klee/Solver.h"
-// FIXME: Use APInt.
-#include "klee/Internal/Support/IntEvaluation.h"
 
-#include "klee/util/ExprUtil.h"
+#include "klee/Expr/Constraints.h"
+#include "klee/Expr/Expr.h"
+#include "klee/Expr/ExprUtil.h"
+#include "klee/Internal/Support/IntEvaluation.h" // FIXME: Use APInt
+#include "klee/Solver.h"
 
 #include <map>
 #include <set>
diff --git a/lib/Core/ImpliedValue.h b/lib/Core/ImpliedValue.h
index 2b323c01..5943e41f 100644
--- a/lib/Core/ImpliedValue.h
+++ b/lib/Core/ImpliedValue.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_IMPLIEDVALUE_H
 #define KLEE_IMPLIEDVALUE_H
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 
 #include <vector>
 
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index 9348105e..93be1f44 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -12,11 +12,12 @@
 #include "Context.h"
 #include "MemoryManager.h"
 #include "ObjectHolder.h"
-#include "klee/Expr.h"
+
+#include "klee/Expr/ArrayCache.h"
+#include "klee/Expr/Expr.h"
 #include "klee/Internal/Support/ErrorHandling.h"
 #include "klee/OptionCategories.h"
 #include "klee/Solver.h"
-#include "klee/util/ArrayCache.h"
 #include "klee/util/BitArray.h"
 
 #include "llvm/IR/Function.h"
diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
index 3558c96c..dfda433c 100644
--- a/lib/Core/Memory.h
+++ b/lib/Core/Memory.h
@@ -12,12 +12,13 @@
 
 #include "Context.h"
 #include "TimingSolver.h"
-#include "klee/Expr.h"
+
+#include "klee/Expr/Expr.h"
 
 #include "llvm/ADT/StringExtras.h"
 
-#include <vector>
 #include <string>
+#include <vector>
 
 namespace llvm {
   class Value;
diff --git a/lib/Core/MemoryManager.cpp b/lib/Core/MemoryManager.cpp
index dba90f8d..af3a2f26 100644
--- a/lib/Core/MemoryManager.cpp
+++ b/lib/Core/MemoryManager.cpp
@@ -7,11 +7,12 @@
 //
 //===----------------------------------------------------------------------===//
 
+#include "MemoryManager.h"
+
 #include "CoreStats.h"
 #include "Memory.h"
-#include "MemoryManager.h"
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 #include "klee/Internal/Support/ErrorHandling.h"
 
 #include "llvm/Support/CommandLine.h"
diff --git a/lib/Core/PTree.cpp b/lib/Core/PTree.cpp
index e3e38868..732dc817 100644
--- a/lib/Core/PTree.cpp
+++ b/lib/Core/PTree.cpp
@@ -9,15 +9,13 @@
 
 #include "PTree.h"
 
-#include <klee/Expr.h>
-#include <klee/util/ExprPPrinter.h>
+#include <klee/Expr/Expr.h>
+#include <klee/Expr/ExprPPrinter.h>
 
 #include <vector>
 
 using namespace klee;
 
-  /* *** */
-
 PTree::PTree(const data_type &root) : root(new Node(nullptr, root)) {}
 
 std::pair<PTreeNode*, PTreeNode*>
diff --git a/lib/Core/PTree.h b/lib/Core/PTree.h
index b13b1d67..3185203f 100644
--- a/lib/Core/PTree.h
+++ b/lib/Core/PTree.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_PTREE_H
 #define KLEE_PTREE_H
 
-#include <klee/Expr.h>
+#include <klee/Expr/Expr.h>
 
 namespace klee {
   class ExecutionState;
diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp
index 90de17ff..a896197b 100644
--- a/lib/Core/SeedInfo.cpp
+++ b/lib/Core/SeedInfo.cpp
@@ -12,8 +12,8 @@
 #include "TimingSolver.h"
 
 #include "klee/ExecutionState.h"
-#include "klee/Expr.h"
-#include "klee/util/ExprUtil.h"
+#include "klee/Expr/Expr.h"
+#include "klee/Expr/ExprUtil.h"
 #include "klee/Internal/ADT/KTest.h"
 #include "klee/Internal/Support/ErrorHandling.h"
 
diff --git a/lib/Core/SeedInfo.h b/lib/Core/SeedInfo.h
index 0d2b6ae0..fb2d025d 100644
--- a/lib/Core/SeedInfo.h
+++ b/lib/Core/SeedInfo.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_SEEDINFO_H
 #define KLEE_SEEDINFO_H
 
-#include "klee/util/Assignment.h"
+#include "klee/Expr/Assignment.h"
 
 extern "C" {
   struct KTest;
diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h
index 6951a3ad..b08073ab 100644
--- a/lib/Core/TimingSolver.h
+++ b/lib/Core/TimingSolver.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_TIMINGSOLVER_H
 #define KLEE_TIMINGSOLVER_H
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 #include "klee/Solver.h"
 #include "klee/Internal/System/Time.h"
 
diff --git a/lib/Expr/ArrayCache.cpp b/lib/Expr/ArrayCache.cpp
index b669f237..d4e8ee8f 100644
--- a/lib/Expr/ArrayCache.cpp
+++ b/lib/Expr/ArrayCache.cpp
@@ -1,4 +1,4 @@
-#include "klee/util/ArrayCache.h"
+#include "klee/Expr/ArrayCache.h"
 
 namespace klee {
 
diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp
index 43b289e2..1a48adfe 100644
--- a/lib/Expr/ArrayExprOptimizer.cpp
+++ b/lib/Expr/ArrayExprOptimizer.cpp
@@ -13,10 +13,10 @@
 #include "AssignmentGenerator.h"
 
 #include "klee/Config/Version.h"
-#include "klee/ExprBuilder.h"
+#include "klee/Expr/Assignment.h"
+#include "klee/Expr/ExprBuilder.h"
 #include "klee/Internal/Support/ErrorHandling.h"
 #include "klee/OptionCategories.h"
-#include "klee/util/Assignment.h"
 #include "klee/util/BitArray.h"
 
 #include <llvm/ADT/APInt.h>
diff --git a/lib/Expr/ArrayExprOptimizer.h b/lib/Expr/ArrayExprOptimizer.h
index 8f6472a4..ca90931d 100644
--- a/lib/Expr/ArrayExprOptimizer.h
+++ b/lib/Expr/ArrayExprOptimizer.h
@@ -17,7 +17,7 @@
 #include <utility>
 #include <vector>
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 #include "klee/util/Ref.h"
 
 namespace klee {
diff --git a/lib/Expr/ArrayExprRewriter.h b/lib/Expr/ArrayExprRewriter.h
index a0ee9f1d..098cb0a6 100644
--- a/lib/Expr/ArrayExprRewriter.h
+++ b/lib/Expr/ArrayExprRewriter.h
@@ -14,7 +14,7 @@
 #include <map>
 #include <vector>
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 #include "klee/util/Ref.h"
 
 namespace klee {
diff --git a/lib/Expr/ArrayExprVisitor.h b/lib/Expr/ArrayExprVisitor.h
index bfa75478..a6d9ae46 100644
--- a/lib/Expr/ArrayExprVisitor.h
+++ b/lib/Expr/ArrayExprVisitor.h
@@ -10,9 +10,9 @@
 #ifndef KLEE_ARRAYEXPRVISITOR_H
 #define KLEE_ARRAYEXPRVISITOR_H
 
-#include "klee/ExprBuilder.h"
+#include "klee/Expr/ExprBuilder.h"
+#include "klee/Expr/ExprVisitor.h"
 #include "klee/SolverCmdLine.h"
-#include "klee/util/ExprVisitor.h"
 
 #include <unordered_map>
 #include <unordered_set>
diff --git a/lib/Expr/Assigment.cpp b/lib/Expr/Assigment.cpp
index d788785a..2fc569cc 100644
--- a/lib/Expr/Assigment.cpp
+++ b/lib/Expr/Assigment.cpp
@@ -6,7 +6,9 @@
 // License. See LICENSE.TXT for details.
 //
 //===----------------------------------------------------------------------===//
-#include "klee/util/Assignment.h"
+
+#include "klee/Expr/Assignment.h"
+
 namespace klee {
 
 void Assignment::dump() {
diff --git a/lib/Expr/AssignmentGenerator.cpp b/lib/Expr/AssignmentGenerator.cpp
index dc744ba0..acb2dc13 100644
--- a/lib/Expr/AssignmentGenerator.cpp
+++ b/lib/Expr/AssignmentGenerator.cpp
@@ -9,21 +9,22 @@
 
 #include "AssignmentGenerator.h"
 
-#include <cassert>
-#include <cstdint>
+#include "klee/Expr/Assignment.h"
+#include "klee/Internal/Support/ErrorHandling.h"
+#include "klee/klee.h"
+
 #include <llvm/ADT/APInt.h>
 #include <llvm/Support/Casting.h>
 #include <llvm/Support/raw_ostream.h>
+
+#include <cassert>
+#include <cstdint>
 #include <map>
 #include <set>
 #include <stddef.h>
 #include <string>
 #include <utility>
 
-#include "klee/Internal/Support/ErrorHandling.h"
-#include "klee/klee.h"
-#include "klee/util/Assignment.h"
-
 using namespace klee;
 
 bool AssignmentGenerator::generatePartialAssignment(const ref<Expr> &e,
diff --git a/lib/Expr/AssignmentGenerator.h b/lib/Expr/AssignmentGenerator.h
index 3bd940e7..173b863e 100644
--- a/lib/Expr/AssignmentGenerator.h
+++ b/lib/Expr/AssignmentGenerator.h
@@ -10,11 +10,11 @@
 #ifndef KLEE_ASSIGNMENTGENERATOR_H
 #define KLEE_ASSIGNMENTGENERATOR_H
 
-#include <vector>
-
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 #include "klee/util/Ref.h"
 
+#include <vector>
+
 namespace klee {
 class Assignment;
 } /* namespace klee */
diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp
index e033333b..2b5adc4c 100644
--- a/lib/Expr/Constraints.cpp
+++ b/lib/Expr/Constraints.cpp
@@ -7,12 +7,12 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "klee/Constraints.h"
+#include "klee/Expr/Constraints.h"
 
+#include "klee/Expr/ExprPPrinter.h"
+#include "klee/Expr/ExprVisitor.h"
 #include "klee/Internal/Module/KModule.h"
 #include "klee/OptionCategories.h"
-#include "klee/util/ExprPPrinter.h"
-#include "klee/util/ExprVisitor.h"
 
 #include "llvm/IR/Function.h"
 #include "llvm/Support/CommandLine.h"
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index 060595d6..6b8dc95f 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -7,14 +7,14 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 
 #include "klee/Config/Version.h"
+#include "klee/Expr/ExprPPrinter.h"
 // FIXME: We shouldn't need this once fast constant support moves into
 // Core. If we need to do arithmetic, we probably want to use APInt.
 #include "klee/Internal/Support/IntEvaluation.h"
 #include "klee/OptionCategories.h"
-#include "klee/util/ExprPPrinter.h"
 
 #include "llvm/ADT/Hashing.h"
 #include "llvm/Support/CommandLine.h"
diff --git a/lib/Expr/ExprBuilder.cpp b/lib/Expr/ExprBuilder.cpp
index d9e20e45..e1cfa2d2 100644
--- a/lib/Expr/ExprBuilder.cpp
+++ b/lib/Expr/ExprBuilder.cpp
@@ -7,7 +7,7 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "klee/ExprBuilder.h"
+#include "klee/Expr/ExprBuilder.h"
 
 using namespace klee;
 
diff --git a/lib/Expr/ExprEvaluator.cpp b/lib/Expr/ExprEvaluator.cpp
index 6b84cd6f..f03d7669 100644
--- a/lib/Expr/ExprEvaluator.cpp
+++ b/lib/Expr/ExprEvaluator.cpp
@@ -7,7 +7,7 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "klee/util/ExprEvaluator.h"
+#include "klee/Expr/ExprEvaluator.h"
 
 using namespace klee;
 
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index 114c46b4..2ccd7262 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -7,9 +7,9 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "klee/util/ExprPPrinter.h"
+#include "klee/Expr/ExprPPrinter.h"
 
-#include "klee/Constraints.h"
+#include "klee/Expr/Constraints.h"
 #include "klee/OptionCategories.h"
 #include "klee/util/PrintContext.h"
 
diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp
index 06186db2..b83a6af4 100644
--- a/lib/Expr/ExprSMTLIBPrinter.cpp
+++ b/lib/Expr/ExprSMTLIBPrinter.cpp
@@ -7,7 +7,7 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "klee/util/ExprSMTLIBPrinter.h"
+#include "klee/Expr/ExprSMTLIBPrinter.h"
 
 #include "llvm/Support/Casting.h"
 #include "llvm/Support/CommandLine.h"
diff --git a/lib/Expr/ExprUtil.cpp b/lib/Expr/ExprUtil.cpp
index 2106b226..911366f3 100644
--- a/lib/Expr/ExprUtil.cpp
+++ b/lib/Expr/ExprUtil.cpp
@@ -7,12 +7,10 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "klee/util/ExprUtil.h"
-#include "klee/util/ExprHashMap.h"
-
-#include "klee/Expr.h"
-
-#include "klee/util/ExprVisitor.h"
+#include "klee/Expr/ExprUtil.h"
+#include "klee/Expr/Expr.h"
+#include "klee/Expr/ExprHashMap.h"
+#include "klee/Expr/ExprVisitor.h"
 
 #include <set>
 
diff --git a/lib/Expr/ExprVisitor.cpp b/lib/Expr/ExprVisitor.cpp
index b99cc7e7..a3fa41d8 100644
--- a/lib/Expr/ExprVisitor.cpp
+++ b/lib/Expr/ExprVisitor.cpp
@@ -7,9 +7,10 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "klee/util/ExprVisitor.h"
+#include "klee/Expr/ExprVisitor.h"
+
+#include "klee/Expr/Expr.h"
 
-#include "klee/Expr.h"
 #include "llvm/Support/CommandLine.h"
 
 namespace {
diff --git a/lib/Expr/Lexer.cpp b/lib/Expr/Lexer.cpp
index e250a968..784764bb 100644
--- a/lib/Expr/Lexer.cpp
+++ b/lib/Expr/Lexer.cpp
@@ -7,7 +7,7 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "expr/Lexer.h"
+#include "klee/Expr/Parser/Lexer.h"
 
 #include "llvm/Support/MemoryBuffer.h"
 #include "llvm/Support/raw_ostream.h"
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index 479ff6c2..c365002d 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -7,16 +7,14 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "expr/Parser.h"
-
-#include "expr/Lexer.h"
-
 #include "klee/Config/Version.h"
-#include "klee/Constraints.h"
-#include "klee/ExprBuilder.h"
+#include "klee/Expr/Constraints.h"
+#include "klee/Expr/ArrayCache.h"
+#include "klee/Expr/ExprBuilder.h"
+#include "klee/Expr/ExprPPrinter.h"
+#include "klee/Expr/Parser/Lexer.h"
+#include "klee/Expr/Parser/Parser.h"
 #include "klee/Solver.h"
-#include "klee/util/ExprPPrinter.h"
-#include "klee/util/ArrayCache.h"
 
 #include "llvm/ADT/APInt.h"
 #include "llvm/Support/MemoryBuffer.h"
diff --git a/lib/Expr/Updates.cpp b/lib/Expr/Updates.cpp
index d58a3642..7264ca89 100644
--- a/lib/Expr/Updates.cpp
+++ b/lib/Expr/Updates.cpp
@@ -7,14 +7,12 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 
 #include <cassert>
 
 using namespace klee;
 
-///
-
 UpdateNode::UpdateNode(const UpdateNode *_next, 
                        const ref<Expr> &_index, 
                        const ref<Expr> &_value) 
diff --git a/lib/Solver/AssignmentValidatingSolver.cpp b/lib/Solver/AssignmentValidatingSolver.cpp
index 82702dbf..b75f982a 100644
--- a/lib/Solver/AssignmentValidatingSolver.cpp
+++ b/lib/Solver/AssignmentValidatingSolver.cpp
@@ -6,10 +6,12 @@
 // License. See LICENSE.TXT for details.
 //
 //===----------------------------------------------------------------------===//
-#include "klee/util/Assignment.h"
-#include "klee/Constraints.h"
+
+#include "klee/Expr/Constraints.h"
+#include "klee/Expr/Assignment.h"
 #include "klee/Solver.h"
 #include "klee/SolverImpl.h"
+
 #include <vector>
 
 namespace klee {
diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp
index a6ca93ac..2eedc616 100644
--- a/lib/Solver/CachingSolver.cpp
+++ b/lib/Solver/CachingSolver.cpp
@@ -10,8 +10,8 @@
 
 #include "klee/Solver.h"
 
-#include "klee/Constraints.h"
-#include "klee/Expr.h"
+#include "klee/Expr/Constraints.h"
+#include "klee/Expr/Expr.h"
 #include "klee/IncompleteSolver.h"
 #include "klee/SolverImpl.h"
 
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index d2e080d9..5c181dc3 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -9,17 +9,17 @@
 
 #include "klee/Solver.h"
 
-#include "klee/Constraints.h"
-#include "klee/Expr.h"
+#include "klee/Expr/Assignment.h"
+#include "klee/Expr/Constraints.h"
+#include "klee/Expr/Expr.h"
+#include "klee/Expr/ExprUtil.h"
+#include "klee/Expr/ExprVisitor.h"
 #include "klee/Internal/ADT/MapOfSets.h"
 #include "klee/Internal/Support/ErrorHandling.h"
 #include "klee/OptionCategories.h"
 #include "klee/SolverImpl.h"
 #include "klee/SolverStats.h"
 #include "klee/TimerStatIncrementer.h"
-#include "klee/util/Assignment.h"
-#include "klee/util/ExprUtil.h"
-#include "klee/util/ExprVisitor.h"
 
 #include "llvm/Support/CommandLine.h"
 
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index 5ea6c1d4..9f493cd1 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -10,27 +10,25 @@
 #define DEBUG_TYPE "cex-solver"
 #include "klee/Solver.h"
 
-#include "klee/Constraints.h"
-#include "klee/Expr.h"
+#include "klee/Expr/Constraints.h"
+#include "klee/Expr/Expr.h"
+#include "klee/Expr/ExprEvaluator.h"
+#include "klee/Expr/ExprRangeEvaluator.h"
+#include "klee/Expr/ExprVisitor.h"
 #include "klee/IncompleteSolver.h"
-#include "klee/util/ExprEvaluator.h"
-#include "klee/util/ExprRangeEvaluator.h"
-#include "klee/util/ExprVisitor.h"
-// FIXME: Use APInt.
 #include "klee/Internal/Support/Debug.h"
-#include "klee/Internal/Support/IntEvaluation.h"
+#include "klee/Internal/Support/IntEvaluation.h" // FIXME: Use APInt
 
 #include "llvm/Support/raw_ostream.h"
-#include <sstream>
+
 #include <cassert>
 #include <map>
+#include <sstream>
 #include <vector>
 
 using namespace klee;
 
-/***/
-
-      // Hacker's Delight, pgs 58-63
+// Hacker's Delight, pgs 58-63
 static uint64_t minOR(uint64_t a, uint64_t b,
                       uint64_t c, uint64_t d) {
   uint64_t temp, m = ((uint64_t) 1)<<63;
diff --git a/lib/Solver/IncompleteSolver.cpp b/lib/Solver/IncompleteSolver.cpp
index 72fe2a95..e19a71e1 100644
--- a/lib/Solver/IncompleteSolver.cpp
+++ b/lib/Solver/IncompleteSolver.cpp
@@ -9,7 +9,7 @@
 
 #include "klee/IncompleteSolver.h"
 
-#include "klee/Constraints.h"
+#include "klee/Expr/Constraints.h"
 
 using namespace klee;
 using namespace llvm;
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index 447e5575..12017e5c 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -10,19 +10,19 @@
 #define DEBUG_TYPE "independent-solver"
 #include "klee/Solver.h"
 
-#include "klee/Expr.h"
-#include "klee/Constraints.h"
-#include "klee/SolverImpl.h"
+#include "klee/Expr/Assignment.h"
+#include "klee/Expr/Constraints.h"
+#include "klee/Expr/Expr.h"
+#include "klee/Expr/ExprUtil.h"
 #include "klee/Internal/Support/Debug.h"
-
-#include "klee/util/ExprUtil.h"
-#include "klee/util/Assignment.h"
+#include "klee/SolverImpl.h"
 
 #include "llvm/Support/raw_ostream.h"
+
+#include <list>
 #include <map>
-#include <vector>
 #include <ostream>
-#include <list>
+#include <vector>
 
 using namespace klee;
 using namespace llvm;
diff --git a/lib/Solver/KQueryLoggingSolver.cpp b/lib/Solver/KQueryLoggingSolver.cpp
index 0c2ac6dd..27e8ad0b 100644
--- a/lib/Solver/KQueryLoggingSolver.cpp
+++ b/lib/Solver/KQueryLoggingSolver.cpp
@@ -9,14 +9,12 @@
 
 #include "QueryLoggingSolver.h"
 
-#include "klee/Expr.h"
-#include "klee/util/ExprPPrinter.h"
+#include "klee/Expr/Expr.h"
+#include "klee/Expr/ExprPPrinter.h"
 #include "klee/Internal/System/Time.h"
 
 using namespace klee;
 
-///
-
 class KQueryLoggingSolver : public QueryLoggingSolver {
 
 private :
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h
index ffe4608d..3112495d 100644
--- a/lib/Solver/MetaSMTBuilder.h
+++ b/lib/Solver/MetaSMTBuilder.h
@@ -7,23 +7,17 @@
 //
 //===----------------------------------------------------------------------===//
 
-/*
- * MetaSMTBuilder.h
- *
- *  Created on: 8 Aug 2012
- *      Author: hpalikar
- */
-
 #ifndef KLEE_METASMTBUILDER_H
 #define KLEE_METASMTBUILDER_H
 
-#include "klee/Config/config.h"
-#include "klee/Expr.h"
-#include "klee/util/ExprPPrinter.h"
-#include "klee/util/ArrayExprHash.h"
-#include "klee/util/ExprHashMap.h"
 #include "ConstantDivision.h"
 
+#include "klee/Config/config.h"
+#include "klee/Expr/ArrayExprHash.h"
+#include "klee/Expr/Expr.h"
+#include "klee/Expr/ExprHashMap.h"
+#include "klee/Expr/ExprPPrinter.h"
+
 #ifdef ENABLE_METASMT
 
 #include "llvm/Support/CommandLine.h"
diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp
index dfa78e42..c4ff1f13 100644
--- a/lib/Solver/MetaSMTSolver.cpp
+++ b/lib/Solver/MetaSMTSolver.cpp
@@ -7,16 +7,17 @@
 //
 //===----------------------------------------------------------------------===//
 #include "klee/Config/config.h"
-#ifdef ENABLE_METASMT
 
+#ifdef ENABLE_METASMT
 #include "MetaSMTSolver.h"
 #include "MetaSMTBuilder.h"
-#include "klee/Constraints.h"
+
+#include "klee/Expr/Assignment.h"
+#include "klee/Expr/Constraints.h"
+#include "klee/Expr/ExprUtil.h"
 #include "klee/Internal/Support/ErrorHandling.h"
 #include "klee/Solver.h"
 #include "klee/SolverImpl.h"
-#include "klee/util/Assignment.h"
-#include "klee/util/ExprUtil.h"
 
 #include "llvm/Support/ErrorHandling.h"
 
@@ -51,11 +52,11 @@
 #endif
 
 #include <errno.h>
-#include <unistd.h>
 #include <signal.h>
-#include <sys/wait.h>
 #include <sys/ipc.h>
 #include <sys/shm.h>
+#include <sys/wait.h>
+#include <unistd.h>
 
 static unsigned char *shared_memory_ptr;
 static int shared_memory_id = 0;
diff --git a/lib/Solver/SMTLIBLoggingSolver.cpp b/lib/Solver/SMTLIBLoggingSolver.cpp
index f734ac38..bfea5c1b 100644
--- a/lib/Solver/SMTLIBLoggingSolver.cpp
+++ b/lib/Solver/SMTLIBLoggingSolver.cpp
@@ -8,7 +8,8 @@
 //===----------------------------------------------------------------------===//
 
 #include "QueryLoggingSolver.h"
-#include "klee/util/ExprSMTLIBPrinter.h"
+
+#include "klee/Expr/ExprSMTLIBPrinter.h"
 
 using namespace klee;
 
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 0bd5084a..645c8989 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -10,10 +10,10 @@
 #ifdef ENABLE_STP
 #include "STPBuilder.h"
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 #include "klee/Solver.h"
-#include "klee/util/Bits.h"
 #include "klee/SolverStats.h"
+#include "klee/util/Bits.h"
 
 #include "ConstantDivision.h"
 
diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h
index cb163384..814046fa 100644
--- a/lib/Solver/STPBuilder.h
+++ b/lib/Solver/STPBuilder.h
@@ -10,9 +10,9 @@
 #ifndef KLEE_STPBUILDER_H
 #define KLEE_STPBUILDER_H
 
-#include "klee/util/ExprHashMap.h"
-#include "klee/util/ArrayExprHash.h"
 #include "klee/Config/config.h"
+#include "klee/Expr/ArrayExprHash.h"
+#include "klee/Expr/ExprHashMap.h"
 
 #include <vector>
 
diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp
index e8b9222f..eb46b6db 100644
--- a/lib/Solver/STPSolver.cpp
+++ b/lib/Solver/STPSolver.cpp
@@ -9,23 +9,25 @@
 #include "klee/Config/config.h"
 
 #ifdef ENABLE_STP
+
 #include "STPBuilder.h"
 #include "STPSolver.h"
-#include "klee/Constraints.h"
+
+#include "klee/Expr/Assignment.h"
+#include "klee/Expr/Constraints.h"
+#include "klee/Expr/ExprUtil.h"
+#include "klee/Internal/Support/ErrorHandling.h"
 #include "klee/OptionCategories.h"
 #include "klee/SolverImpl.h"
-#include "klee/Internal/Support/ErrorHandling.h"
-#include "klee/util/Assignment.h"
-#include "klee/util/ExprUtil.h"
 
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/Errno.h"
 
 #include <csignal>
-#include <unistd.h>
 #include <sys/ipc.h>
 #include <sys/shm.h>
 #include <sys/wait.h>
+#include <unistd.h>
 
 namespace {
 
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 4f7458c5..6c7361dc 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -8,8 +8,9 @@
 //===----------------------------------------------------------------------===//
 
 #include "klee/Solver.h"
+
+#include "klee/Expr/Constraints.h"
 #include "klee/SolverImpl.h"
-#include "klee/Constraints.h"
 
 using namespace klee;
 
diff --git a/lib/Solver/ValidatingSolver.cpp b/lib/Solver/ValidatingSolver.cpp
index 40a7c9e0..71e6834e 100644
--- a/lib/Solver/ValidatingSolver.cpp
+++ b/lib/Solver/ValidatingSolver.cpp
@@ -6,9 +6,11 @@
 // License. See LICENSE.TXT for details.
 //
 //===----------------------------------------------------------------------===//
-#include "klee/Constraints.h"
+
+#include "klee/Expr/Constraints.h"
 #include "klee/Solver.h"
 #include "klee/SolverImpl.h"
+
 #include <vector>
 
 namespace klee {
diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp
index 06b995ae..07a7b681 100644
--- a/lib/Solver/Z3Builder.cpp
+++ b/lib/Solver/Z3Builder.cpp
@@ -10,7 +10,7 @@
 #ifdef ENABLE_Z3
 #include "Z3Builder.h"
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 #include "klee/Internal/Support/ErrorHandling.h"
 #include "klee/Solver.h"
 #include "klee/SolverStats.h"
diff --git a/lib/Solver/Z3Builder.h b/lib/Solver/Z3Builder.h
index efbf4f9a..4501ecbd 100644
--- a/lib/Solver/Z3Builder.h
+++ b/lib/Solver/Z3Builder.h
@@ -11,8 +11,9 @@
 #define KLEE_Z3BUILDER_H
 
 #include "klee/Config/config.h"
-#include "klee/util/ArrayExprHash.h"
-#include "klee/util/ExprHashMap.h"
+#include "klee/Expr/ArrayExprHash.h"
+#include "klee/Expr/ExprHashMap.h"
+
 #include <unordered_map>
 #include <z3.h>
 
diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp
index 74fee290..cfcb77e7 100644
--- a/lib/Solver/Z3Solver.cpp
+++ b/lib/Solver/Z3Solver.cpp
@@ -6,19 +6,22 @@
 // License. See LICENSE.TXT for details.
 //
 //===----------------------------------------------------------------------===//
+
 #include "klee/Config/config.h"
 #include "klee/Internal/Support/ErrorHandling.h"
 #include "klee/Internal/Support/FileHandling.h"
 #include "klee/OptionCategories.h"
 
 #ifdef ENABLE_Z3
+
 #include "Z3Solver.h"
 #include "Z3Builder.h"
-#include "klee/Constraints.h"
+
+#include "klee/Expr/Constraints.h"
+#include "klee/Expr/Assignment.h"
+#include "klee/Expr/ExprUtil.h"
 #include "klee/Solver.h"
 #include "klee/SolverImpl.h"
-#include "klee/util/Assignment.h"
-#include "klee/util/ExprUtil.h"
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/raw_ostream.h"
 
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index 9033a2b4..cc292d10 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -7,23 +7,22 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "expr/Lexer.h"
-#include "expr/Parser.h"
-
 #include "klee/Common.h"
 #include "klee/Config/Version.h"
-#include "klee/Constraints.h"
-#include "klee/Expr.h"
-#include "klee/ExprBuilder.h"
+#include "klee/Expr/Constraints.h"
+#include "klee/Expr/Expr.h"
+#include "klee/Expr/ExprBuilder.h"
+#include "klee/Expr/ExprPPrinter.h"
+#include "klee/Expr/ExprSMTLIBPrinter.h"
+#include "klee/Expr/ExprVisitor.h"
+#include "klee/Expr/Parser/Lexer.h"
+#include "klee/Expr/Parser/Parser.h"
 #include "klee/Internal/Support/PrintVersion.h"
 #include "klee/OptionCategories.h"
 #include "klee/Solver.h"
 #include "klee/SolverCmdLine.h"
 #include "klee/SolverImpl.h"
 #include "klee/Statistics.h"
-#include "klee/util/ExprPPrinter.h"
-#include "klee/util/ExprSMTLIBPrinter.h"
-#include "klee/util/ExprVisitor.h"
 
 #include "llvm/ADT/StringExtras.h"
 #include "llvm/Support/CommandLine.h"
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 99a9bf2a..8235c261 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -11,7 +11,7 @@
 
 #include "klee/Config/Version.h"
 #include "klee/ExecutionState.h"
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 #include "klee/Internal/ADT/KTest.h"
 #include "klee/Internal/ADT/TreeStream.h"
 #include "klee/Internal/Support/Debug.h"
diff --git a/unittests/Assignment/AssignmentTest.cpp b/unittests/Assignment/AssignmentTest.cpp
index 0eaa28f1..872d3301 100644
--- a/unittests/Assignment/AssignmentTest.cpp
+++ b/unittests/Assignment/AssignmentTest.cpp
@@ -1,6 +1,8 @@
-#include "klee/util/ArrayCache.h"
-#include "klee/util/Assignment.h"
 #include "gtest/gtest.h"
+
+#include "klee/Expr/ArrayCache.h"
+#include "klee/Expr/Assignment.h"
+
 #include <iostream>
 #include <vector>
 
diff --git a/unittests/Expr/ExprTest.cpp b/unittests/Expr/ExprTest.cpp
index fba15535..3a7541e9 100644
--- a/unittests/Expr/ExprTest.cpp
+++ b/unittests/Expr/ExprTest.cpp
@@ -10,8 +10,8 @@
 #include <iostream>
 #include "gtest/gtest.h"
 
-#include "klee/Expr.h"
-#include "klee/util/ArrayCache.h"
+#include "klee/Expr/ArrayCache.h"
+#include "klee/Expr/Expr.h"
 
 using namespace klee;
 
diff --git a/unittests/Solver/SolverTest.cpp b/unittests/Solver/SolverTest.cpp
index b178ced3..b15fd64b 100644
--- a/unittests/Solver/SolverTest.cpp
+++ b/unittests/Solver/SolverTest.cpp
@@ -7,16 +7,18 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include <iostream>
 #include "gtest/gtest.h"
 
-#include "klee/SolverCmdLine.h"
-#include "klee/Constraints.h"
-#include "klee/Expr.h"
+#include "klee/Expr/ArrayCache.h"
+#include "klee/Expr/Constraints.h"
+#include "klee/Expr/Expr.h"
 #include "klee/Solver.h"
-#include "klee/util/ArrayCache.h"
+#include "klee/SolverCmdLine.h"
+
 #include "llvm/ADT/StringExtras.h"
 
+#include <iostream>
+
 using namespace klee;
 
 namespace {