about summary refs log tree commit diff homepage
path: root/lib/Solver/MetaSMTBuilder.h
diff options
context:
space:
mode:
authorHoang M. Le <hle@informatik.uni-bremen.de>2016-05-24 17:14:35 +0200
committerHoang M. Le <hle@informatik.uni-bremen.de>2016-06-10 10:24:00 +0200
commitb097c8d29ccefee7aa799b0ca870cc4e8ec39812 (patch)
treebe9bb97f2adaf0ebab349aa87809b39f19f66031 /lib/Solver/MetaSMTBuilder.h
parent96ed13583a464538cab900c851bcc7338150772a (diff)
downloadklee-b097c8d29ccefee7aa799b0ca870cc4e8ec39812.tar.gz
clean up metaSMT includes
Diffstat (limited to 'lib/Solver/MetaSMTBuilder.h')
-rw-r--r--lib/Solver/MetaSMTBuilder.h11
1 files changed, 0 insertions, 11 deletions
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h
index 9e1f9a62..9aca9f83 100644
--- a/lib/Solver/MetaSMTBuilder.h
+++ b/lib/Solver/MetaSMTBuilder.h
@@ -32,17 +32,6 @@
 #include <metaSMT/frontend/Logic.hpp>
 #include <metaSMT/frontend/QF_BV.hpp>
 #include <metaSMT/frontend/Array.hpp>
-#include <metaSMT/support/default_visitation_unrolling_limit.hpp>
-#include <metaSMT/support/run_algorithm.hpp>
-
-#define Expr VCExpr
-#define STP STP_Backend
-#include <metaSMT/backend/STP.hpp>
-#undef Expr
-#undef STP
- 
-#include <boost/mpl/vector.hpp>
-#include <boost/format.hpp>
 
 using namespace metaSMT;
 using namespace metaSMT::logic::QF_BV;