about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2019-08-15 22:57:36 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2019-09-03 13:38:23 +0100
commita8abaa43873b8ee49320035817fcdd70a9879bda (patch)
treefc7251d414a9669e70d55b19b9a39ff00da48ede
parente1f055b1785fd7f23fc4d30eeb0276278892ed20 (diff)
downloadklee-a8abaa43873b8ee49320035817fcdd70a9879bda.tar.gz
Moved solver-related header files into a separate klee/Solver/ directory.
-rw-r--r--include/klee/Common.h3
-rw-r--r--include/klee/Expr/ArrayExprHash.h3
-rw-r--r--include/klee/Expr/ExprSMTLIBPrinter.h2
-rw-r--r--include/klee/Solver/IncompleteSolver.h (renamed from include/klee/IncompleteSolver.h)4
-rw-r--r--include/klee/Solver/Solver.h (renamed from include/klee/Solver.h)2
-rw-r--r--include/klee/Solver/SolverCmdLine.h (renamed from include/klee/SolverCmdLine.h)0
-rw-r--r--include/klee/Solver/SolverImpl.h (renamed from include/klee/SolverImpl.h)0
-rw-r--r--include/klee/Solver/SolverStats.h (renamed from include/klee/SolverStats.h)0
-rw-r--r--lib/Core/Executor.cpp4
-rw-r--r--lib/Core/ExecutorUtil.cpp2
-rw-r--r--lib/Core/ImpliedValue.cpp2
-rw-r--r--lib/Core/Memory.cpp2
-rw-r--r--lib/Core/SpecialFunctionHandler.cpp4
-rw-r--r--lib/Core/StatsTracker.cpp2
-rw-r--r--lib/Core/TimingSolver.cpp2
-rw-r--r--lib/Core/TimingSolver.h2
-rw-r--r--lib/Core/UserSearcher.cpp3
-rw-r--r--lib/Expr/ArrayExprVisitor.h2
-rw-r--r--lib/Expr/Parser.cpp2
-rw-r--r--lib/Solver/AssignmentValidatingSolver.cpp4
-rw-r--r--lib/Solver/CachingSolver.cpp9
-rw-r--r--lib/Solver/CexCachingSolver.cpp6
-rw-r--r--lib/Solver/ConstructSolverChain.cpp4
-rw-r--r--lib/Solver/CoreSolver.cpp7
-rw-r--r--lib/Solver/DummySolver.cpp6
-rw-r--r--lib/Solver/FastCexSolver.cpp4
-rw-r--r--lib/Solver/IncompleteSolver.cpp2
-rw-r--r--lib/Solver/IndependentSolver.cpp4
-rw-r--r--lib/Solver/MetaSMTSolver.cpp4
-rw-r--r--lib/Solver/MetaSMTSolver.h2
-rw-r--r--lib/Solver/QueryLoggingSolver.h4
-rw-r--r--lib/Solver/STPBuilder.cpp4
-rw-r--r--lib/Solver/STPSolver.cpp2
-rw-r--r--lib/Solver/STPSolver.h2
-rw-r--r--lib/Solver/Solver.cpp4
-rw-r--r--lib/Solver/SolverCmdLine.cpp3
-rw-r--r--lib/Solver/SolverImpl.cpp4
-rw-r--r--lib/Solver/SolverStats.cpp2
-rw-r--r--lib/Solver/ValidatingSolver.cpp4
-rw-r--r--lib/Solver/Z3Builder.cpp4
-rw-r--r--lib/Solver/Z3Solver.cpp4
-rw-r--r--lib/Solver/Z3Solver.h2
-rw-r--r--tools/kleaver/main.cpp6
-rw-r--r--tools/klee/main.cpp2
-rw-r--r--unittests/Solver/SolverTest.cpp4
45 files changed, 74 insertions, 70 deletions
diff --git a/include/klee/Common.h b/include/klee/Common.h
index 611b137c..7b244158 100644
--- a/include/klee/Common.h
+++ b/include/klee/Common.h
@@ -14,7 +14,8 @@
 #ifndef KLEE_COMMON_H
 #define KLEE_COMMON_H
 
-#include "klee/Solver.h"
+#include "klee/Solver/Solver.h"
+
 #include <string>
 
 namespace klee {
diff --git a/include/klee/Expr/ArrayExprHash.h b/include/klee/Expr/ArrayExprHash.h
index 04660fe0..f8bef491 100644
--- a/include/klee/Expr/ArrayExprHash.h
+++ b/include/klee/Expr/ArrayExprHash.h
@@ -11,11 +11,10 @@
 #define KLEE_ARRAYEXPRHASH_H
 
 #include "klee/Expr/Expr.h"
+#include "klee/Solver/SolverStats.h"
 #include "klee/TimerStatIncrementer.h"
-#include "klee/SolverStats.h"
 
 #include <map>
-
 #include <unordered_map>
 
 namespace klee {
diff --git a/include/klee/Expr/ExprSMTLIBPrinter.h b/include/klee/Expr/ExprSMTLIBPrinter.h
index a7a604e1..38ae2fa1 100644
--- a/include/klee/Expr/ExprSMTLIBPrinter.h
+++ b/include/klee/Expr/ExprSMTLIBPrinter.h
@@ -13,7 +13,7 @@
 
 #include "klee/Expr/Constraints.h"
 #include "klee/Expr/Expr.h"
-#include "klee/Solver.h"
+#include "klee/Solver/Solver.h"
 #include "klee/util/PrintContext.h"
 
 #include <map>
diff --git a/include/klee/IncompleteSolver.h b/include/klee/Solver/IncompleteSolver.h
index 6511584e..3841c38b 100644
--- a/include/klee/IncompleteSolver.h
+++ b/include/klee/Solver/IncompleteSolver.h
@@ -10,8 +10,8 @@
 #ifndef KLEE_INCOMPLETESOLVER_H
 #define KLEE_INCOMPLETESOLVER_H
 
-#include "klee/Solver.h"
-#include "klee/SolverImpl.h"
+#include "klee/Solver/Solver.h"
+#include "klee/Solver/SolverImpl.h"
 
 namespace klee {
 
diff --git a/include/klee/Solver.h b/include/klee/Solver/Solver.h
index f320a5b6..fe4d7e88 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver/Solver.h
@@ -11,8 +11,8 @@
 #define KLEE_SOLVER_H
 
 #include "klee/Expr/Expr.h"
-#include "klee/SolverCmdLine.h"
 #include "klee/Internal/System/Time.h"
+#include "klee/Solver/SolverCmdLine.h"
 
 #include <vector>
 
diff --git a/include/klee/SolverCmdLine.h b/include/klee/Solver/SolverCmdLine.h
index b453d058..b453d058 100644
--- a/include/klee/SolverCmdLine.h
+++ b/include/klee/Solver/SolverCmdLine.h
diff --git a/include/klee/SolverImpl.h b/include/klee/Solver/SolverImpl.h
index 90d5af24..90d5af24 100644
--- a/include/klee/SolverImpl.h
+++ b/include/klee/Solver/SolverImpl.h
diff --git a/include/klee/SolverStats.h b/include/klee/Solver/SolverStats.h
index dd39043a..dd39043a 100644
--- a/include/klee/SolverStats.h
+++ b/include/klee/Solver/SolverStats.h
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 85cb8e8d..56753bb1 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -47,8 +47,8 @@
 #include "klee/Internal/System/Time.h"
 #include "klee/Interpreter.h"
 #include "klee/OptionCategories.h"
-#include "klee/SolverCmdLine.h"
-#include "klee/SolverStats.h"
+#include "klee/Solver/SolverCmdLine.h"
+#include "klee/Solver/SolverStats.h"
 #include "klee/TimerStatIncrementer.h"
 #include "klee/util/GetElementPtrTypeIterator.h"
 
diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index 15125fe1..9cd74355 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -16,7 +16,7 @@
 #include "klee/Internal/Module/KModule.h"
 #include "klee/Internal/Support/ErrorHandling.h"
 #include "klee/Interpreter.h"
-#include "klee/Solver.h"
+#include "klee/Solver/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 cc001660..6a17c870 100644
--- a/lib/Core/ImpliedValue.cpp
+++ b/lib/Core/ImpliedValue.cpp
@@ -15,7 +15,7 @@
 #include "klee/Expr/Expr.h"
 #include "klee/Expr/ExprUtil.h"
 #include "klee/Internal/Support/IntEvaluation.h" // FIXME: Use APInt
-#include "klee/Solver.h"
+#include "klee/Solver/Solver.h"
 
 #include <map>
 #include <set>
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index 93be1f44..c7e7a928 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -17,7 +17,7 @@
 #include "klee/Expr/Expr.h"
 #include "klee/Internal/Support/ErrorHandling.h"
 #include "klee/OptionCategories.h"
-#include "klee/Solver.h"
+#include "klee/Solver/Solver.h"
 #include "klee/util/BitArray.h"
 
 #include "llvm/IR/Function.h"
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 231bd88d..4acf2e36 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -13,15 +13,15 @@
 #include "Memory.h"
 #include "MemoryManager.h"
 #include "TimingSolver.h"
-#include "klee/MergeHandler.h"
 
 #include "klee/ExecutionState.h"
 #include "klee/Internal/Module/KInstruction.h"
 #include "klee/Internal/Module/KModule.h"
 #include "klee/Internal/Support/Debug.h"
 #include "klee/Internal/Support/ErrorHandling.h"
+#include "klee/MergeHandler.h"
 #include "klee/OptionCategories.h"
-#include "klee/SolverCmdLine.h"
+#include "klee/Solver/SolverCmdLine.h"
 
 #include "llvm/ADT/Twine.h"
 #include "llvm/IR/DataLayout.h"
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index 408e4d6d..259a8d98 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -18,7 +18,7 @@
 #include "klee/Internal/Support/ModuleUtil.h"
 #include "klee/Internal/System/MemoryUsage.h"
 #include "klee/Internal/Support/ErrorHandling.h"
-#include "klee/SolverStats.h"
+#include "klee/Solver/SolverStats.h"
 
 #include "CallPathManager.h"
 #include "CoreStats.h"
diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp
index 0f69509a..81ebf098 100644
--- a/lib/Core/TimingSolver.cpp
+++ b/lib/Core/TimingSolver.cpp
@@ -11,7 +11,7 @@
 
 #include "klee/Config/Version.h"
 #include "klee/ExecutionState.h"
-#include "klee/Solver.h"
+#include "klee/Solver/Solver.h"
 #include "klee/Statistics.h"
 #include "klee/TimerStatIncrementer.h"
 
diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h
index b08073ab..d74572b8 100644
--- a/lib/Core/TimingSolver.h
+++ b/lib/Core/TimingSolver.h
@@ -11,7 +11,7 @@
 #define KLEE_TIMINGSOLVER_H
 
 #include "klee/Expr/Expr.h"
-#include "klee/Solver.h"
+#include "klee/Solver/Solver.h"
 #include "klee/Internal/System/Time.h"
 
 #include <vector>
diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
index 7efdb30d..c02c349e 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -13,9 +13,8 @@
 #include "Executor.h"
 
 #include "klee/Internal/Support/ErrorHandling.h"
-#include "klee/SolverCmdLine.h"
 #include "klee/MergeHandler.h"
-
+#include "klee/Solver/SolverCmdLine.h"
 
 #include "llvm/Support/CommandLine.h"
 
diff --git a/lib/Expr/ArrayExprVisitor.h b/lib/Expr/ArrayExprVisitor.h
index a6d9ae46..c5a4691e 100644
--- a/lib/Expr/ArrayExprVisitor.h
+++ b/lib/Expr/ArrayExprVisitor.h
@@ -12,7 +12,7 @@
 
 #include "klee/Expr/ExprBuilder.h"
 #include "klee/Expr/ExprVisitor.h"
-#include "klee/SolverCmdLine.h"
+#include "klee/Solver/SolverCmdLine.h"
 
 #include <unordered_map>
 #include <unordered_set>
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index c365002d..6b29ac3e 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -14,7 +14,7 @@
 #include "klee/Expr/ExprPPrinter.h"
 #include "klee/Expr/Parser/Lexer.h"
 #include "klee/Expr/Parser/Parser.h"
-#include "klee/Solver.h"
+#include "klee/Solver/Solver.h"
 
 #include "llvm/ADT/APInt.h"
 #include "llvm/Support/MemoryBuffer.h"
diff --git a/lib/Solver/AssignmentValidatingSolver.cpp b/lib/Solver/AssignmentValidatingSolver.cpp
index b75f982a..7e1ccd38 100644
--- a/lib/Solver/AssignmentValidatingSolver.cpp
+++ b/lib/Solver/AssignmentValidatingSolver.cpp
@@ -9,8 +9,8 @@
 
 #include "klee/Expr/Constraints.h"
 #include "klee/Expr/Assignment.h"
-#include "klee/Solver.h"
-#include "klee/SolverImpl.h"
+#include "klee/Solver/Solver.h"
+#include "klee/Solver/SolverImpl.h"
 
 #include <vector>
 
diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp
index 2eedc616..2c7371d0 100644
--- a/lib/Solver/CachingSolver.cpp
+++ b/lib/Solver/CachingSolver.cpp
@@ -8,14 +8,13 @@
 //===----------------------------------------------------------------------===//
 
 
-#include "klee/Solver.h"
+#include "klee/Solver/Solver.h"
 
 #include "klee/Expr/Constraints.h"
 #include "klee/Expr/Expr.h"
-#include "klee/IncompleteSolver.h"
-#include "klee/SolverImpl.h"
-
-#include "klee/SolverStats.h"
+#include "klee/Solver/IncompleteSolver.h"
+#include "klee/Solver/SolverImpl.h"
+#include "klee/Solver/SolverStats.h"
 
 #include <ciso646>
 #ifdef _LIBCPP_VERSION
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index 5c181dc3..27a165e1 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -7,7 +7,7 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "klee/Solver.h"
+#include "klee/Solver/Solver.h"
 
 #include "klee/Expr/Assignment.h"
 #include "klee/Expr/Constraints.h"
@@ -17,8 +17,8 @@
 #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/Solver/SolverImpl.h"
+#include "klee/Solver/SolverStats.h"
 #include "klee/TimerStatIncrementer.h"
 
 #include "llvm/Support/CommandLine.h"
diff --git a/lib/Solver/ConstructSolverChain.cpp b/lib/Solver/ConstructSolverChain.cpp
index 39e0e824..ed6a77dd 100644
--- a/lib/Solver/ConstructSolverChain.cpp
+++ b/lib/Solver/ConstructSolverChain.cpp
@@ -10,10 +10,12 @@
 /*
  * This file groups declarations that are common to both KLEE and Kleaver.
  */
+
 #include "klee/Common.h"
-#include "klee/SolverCmdLine.h"
 #include "klee/Internal/Support/ErrorHandling.h"
 #include "klee/Internal/System/Time.h"
+#include "klee/Solver/SolverCmdLine.h"
+
 #include "llvm/Support/raw_ostream.h"
 
 
diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp
index 774f52a7..e22f0471 100644
--- a/lib/Solver/CoreSolver.cpp
+++ b/lib/Solver/CoreSolver.cpp
@@ -10,11 +10,14 @@
 #include "STPSolver.h"
 #include "Z3Solver.h"
 #include "MetaSMTSolver.h"
-#include "klee/SolverCmdLine.h"
+
+#include "klee/Solver/SolverCmdLine.h"
 #include "klee/Internal/Support/ErrorHandling.h"
-#include "klee/Solver.h"
+#include "klee/Solver/Solver.h"
+
 #include "llvm/Support/ErrorHandling.h"
 #include "llvm/Support/raw_ostream.h"
+
 #include <string>
 
 namespace klee {
diff --git a/lib/Solver/DummySolver.cpp b/lib/Solver/DummySolver.cpp
index 39328653..60a4fb51 100644
--- a/lib/Solver/DummySolver.cpp
+++ b/lib/Solver/DummySolver.cpp
@@ -7,9 +7,9 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "klee/Solver.h"
-#include "klee/SolverImpl.h"
-#include "klee/SolverStats.h"
+#include "klee/Solver/Solver.h"
+#include "klee/Solver/SolverImpl.h"
+#include "klee/Solver/SolverStats.h"
 
 namespace klee {
 
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index 9f493cd1..3e1162fd 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -8,14 +8,14 @@
 //===----------------------------------------------------------------------===//
 
 #define DEBUG_TYPE "cex-solver"
-#include "klee/Solver.h"
+#include "klee/Solver/Solver.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/Solver/IncompleteSolver.h"
 #include "klee/Internal/Support/Debug.h"
 #include "klee/Internal/Support/IntEvaluation.h" // FIXME: Use APInt
 
diff --git a/lib/Solver/IncompleteSolver.cpp b/lib/Solver/IncompleteSolver.cpp
index e19a71e1..9b57bc6c 100644
--- a/lib/Solver/IncompleteSolver.cpp
+++ b/lib/Solver/IncompleteSolver.cpp
@@ -7,7 +7,7 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "klee/IncompleteSolver.h"
+#include "klee/Solver/IncompleteSolver.h"
 
 #include "klee/Expr/Constraints.h"
 
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index 12017e5c..7beb1a7c 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -8,14 +8,14 @@
 //===----------------------------------------------------------------------===//
 
 #define DEBUG_TYPE "independent-solver"
-#include "klee/Solver.h"
+#include "klee/Solver/Solver.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/SolverImpl.h"
+#include "klee/Solver/SolverImpl.h"
 
 #include "llvm/Support/raw_ostream.h"
 
diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp
index c4ff1f13..6817c47a 100644
--- a/lib/Solver/MetaSMTSolver.cpp
+++ b/lib/Solver/MetaSMTSolver.cpp
@@ -16,8 +16,8 @@
 #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/Solver/Solver.h"
+#include "klee/Solver/SolverImpl.h"
 
 #include "llvm/Support/ErrorHandling.h"
 
diff --git a/lib/Solver/MetaSMTSolver.h b/lib/Solver/MetaSMTSolver.h
index 9fa93719..89cb7143 100644
--- a/lib/Solver/MetaSMTSolver.h
+++ b/lib/Solver/MetaSMTSolver.h
@@ -11,7 +11,7 @@
 #ifndef KLEE_METASMTSOLVER_H
 #define KLEE_METASMTSOLVER_H
 
-#include "klee/Solver.h"
+#include "klee/Solver/Solver.h"
 
 namespace klee {
 
diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h
index 75faf3a3..3c012cc2 100644
--- a/lib/Solver/QueryLoggingSolver.h
+++ b/lib/Solver/QueryLoggingSolver.h
@@ -11,8 +11,8 @@
 #ifndef KLEE_QUERYLOGGINGSOLVER_H
 #define KLEE_QUERYLOGGINGSOLVER_H
 
-#include "klee/Solver.h"
-#include "klee/SolverImpl.h"
+#include "klee/Solver/Solver.h"
+#include "klee/Solver/SolverImpl.h"
 #include "klee/Internal/System/Time.h"
 
 #include "llvm/Support/raw_ostream.h"
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 645c8989..ef6697ef 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -11,8 +11,8 @@
 #include "STPBuilder.h"
 
 #include "klee/Expr/Expr.h"
-#include "klee/Solver.h"
-#include "klee/SolverStats.h"
+#include "klee/Solver/Solver.h"
+#include "klee/Solver/SolverStats.h"
 #include "klee/util/Bits.h"
 
 #include "ConstantDivision.h"
diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp
index eb46b6db..ebb67254 100644
--- a/lib/Solver/STPSolver.cpp
+++ b/lib/Solver/STPSolver.cpp
@@ -18,7 +18,7 @@
 #include "klee/Expr/ExprUtil.h"
 #include "klee/Internal/Support/ErrorHandling.h"
 #include "klee/OptionCategories.h"
-#include "klee/SolverImpl.h"
+#include "klee/Solver/SolverImpl.h"
 
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/Errno.h"
diff --git a/lib/Solver/STPSolver.h b/lib/Solver/STPSolver.h
index 70b9aa12..494a30db 100644
--- a/lib/Solver/STPSolver.h
+++ b/lib/Solver/STPSolver.h
@@ -11,7 +11,7 @@
 #ifndef KLEE_STPSOLVER_H
 #define KLEE_STPSOLVER_H
 
-#include "klee/Solver.h"
+#include "klee/Solver/Solver.h"
 
 namespace klee {
 /// STPSolver - A complete solver based on STP.
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 6c7361dc..855f7102 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -7,10 +7,10 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "klee/Solver.h"
+#include "klee/Solver/Solver.h"
 
 #include "klee/Expr/Constraints.h"
-#include "klee/SolverImpl.h"
+#include "klee/Solver/SolverImpl.h"
 
 using namespace klee;
 
diff --git a/lib/Solver/SolverCmdLine.cpp b/lib/Solver/SolverCmdLine.cpp
index 9e190840..87b66317 100644
--- a/lib/Solver/SolverCmdLine.cpp
+++ b/lib/Solver/SolverCmdLine.cpp
@@ -12,8 +12,9 @@
  * data that are common to both KLEE and Kleaver.
  */
 
+#include "klee/Solver/SolverCmdLine.h"
+
 #include "klee/Config/Version.h"
-#include "klee/SolverCmdLine.h"
 #include "klee/OptionCategories.h"
 
 #include "llvm/ADT/ArrayRef.h"
diff --git a/lib/Solver/SolverImpl.cpp b/lib/Solver/SolverImpl.cpp
index e8f30c9e..ad5388e5 100644
--- a/lib/Solver/SolverImpl.cpp
+++ b/lib/Solver/SolverImpl.cpp
@@ -7,8 +7,8 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "klee/Solver.h"
-#include "klee/SolverImpl.h"
+#include "klee/Solver/Solver.h"
+#include "klee/Solver/SolverImpl.h"
 
 using namespace klee;
 
diff --git a/lib/Solver/SolverStats.cpp b/lib/Solver/SolverStats.cpp
index efdfe6ed..841bfc60 100644
--- a/lib/Solver/SolverStats.cpp
+++ b/lib/Solver/SolverStats.cpp
@@ -7,7 +7,7 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "klee/SolverStats.h"
+#include "klee/Solver/SolverStats.h"
 
 using namespace klee;
 
diff --git a/lib/Solver/ValidatingSolver.cpp b/lib/Solver/ValidatingSolver.cpp
index 71e6834e..93d743db 100644
--- a/lib/Solver/ValidatingSolver.cpp
+++ b/lib/Solver/ValidatingSolver.cpp
@@ -8,8 +8,8 @@
 //===----------------------------------------------------------------------===//
 
 #include "klee/Expr/Constraints.h"
-#include "klee/Solver.h"
-#include "klee/SolverImpl.h"
+#include "klee/Solver/Solver.h"
+#include "klee/Solver/SolverImpl.h"
 
 #include <vector>
 
diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp
index 07a7b681..43440fa7 100644
--- a/lib/Solver/Z3Builder.cpp
+++ b/lib/Solver/Z3Builder.cpp
@@ -12,8 +12,8 @@
 
 #include "klee/Expr/Expr.h"
 #include "klee/Internal/Support/ErrorHandling.h"
-#include "klee/Solver.h"
-#include "klee/SolverStats.h"
+#include "klee/Solver/Solver.h"
+#include "klee/Solver/SolverStats.h"
 #include "klee/util/Bits.h"
 
 #include "llvm/ADT/StringExtras.h"
diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp
index cfcb77e7..00777a78 100644
--- a/lib/Solver/Z3Solver.cpp
+++ b/lib/Solver/Z3Solver.cpp
@@ -20,8 +20,8 @@
 #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/Solver/Solver.h"
+#include "klee/Solver/SolverImpl.h"
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/raw_ostream.h"
 
diff --git a/lib/Solver/Z3Solver.h b/lib/Solver/Z3Solver.h
index bed74b88..9688ccff 100644
--- a/lib/Solver/Z3Solver.h
+++ b/lib/Solver/Z3Solver.h
@@ -11,7 +11,7 @@
 #ifndef KLEE_Z3SOLVER_H
 #define KLEE_Z3SOLVER_H
 
-#include "klee/Solver.h"
+#include "klee/Solver/Solver.h"
 
 namespace klee {
 /// Z3Solver - A complete solver based on Z3
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index cc292d10..70b51208 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -19,9 +19,9 @@
 #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/Solver/Solver.h"
+#include "klee/Solver/SolverCmdLine.h"
+#include "klee/Solver/SolverImpl.h"
 #include "klee/Statistics.h"
 
 #include "llvm/ADT/StringExtras.h"
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 09b3dea5..de2989f6 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -22,7 +22,7 @@
 #include "klee/Internal/System/Time.h"
 #include "klee/Interpreter.h"
 #include "klee/OptionCategories.h"
-#include "klee/SolverCmdLine.h"
+#include "klee/Solver/SolverCmdLine.h"
 #include "klee/Statistics.h"
 
 #include "llvm/IR/Constants.h"
diff --git a/unittests/Solver/SolverTest.cpp b/unittests/Solver/SolverTest.cpp
index b15fd64b..9c1089e0 100644
--- a/unittests/Solver/SolverTest.cpp
+++ b/unittests/Solver/SolverTest.cpp
@@ -12,8 +12,8 @@
 #include "klee/Expr/ArrayCache.h"
 #include "klee/Expr/Constraints.h"
 #include "klee/Expr/Expr.h"
-#include "klee/Solver.h"
-#include "klee/SolverCmdLine.h"
+#include "klee/Solver/Solver.h"
+#include "klee/Solver/SolverCmdLine.h"
 
 #include "llvm/ADT/StringExtras.h"