diff --git a/CMakeLists.txt b/CMakeLists.txt
index 4067849a0..77ca26279 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -68,8 +68,7 @@ find_package(Threads REQUIRED)
 
 
 include_directories(
-    ${CMAKE_SOURCE_DIR}/minisat/mtl
-    ${CMAKE_SOURCE_DIR}/minisat/core
+    ${CMAKE_SOURCE_DIR}
     ${CMAKE_SOURCE_DIR}/common
     ${CMAKE_SOURCE_DIR}/sorts
     ${CMAKE_SOURCE_DIR}/symbols
diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt
index 71b95348c..062a72e2c 100644
--- a/src/api/CMakeLists.txt
+++ b/src/api/CMakeLists.txt
@@ -53,7 +53,7 @@ if (BUILD_SHARED_LIBS)
         LIBRARY DESTINATION lib
         ARCHIVE DESTINATION lib
         RUNTIME DESTINATION bin
-        INCLUDES DESTINATION include
+        INCLUDES DESTINATION include ${INSTALL_HEADERS_DIR}
     )
 
     install(EXPORT OpenSMTTargets
diff --git a/src/cnfizers/TermMapper.h b/src/cnfizers/TermMapper.h
index 59967c3b5..03ce49b89 100644
--- a/src/cnfizers/TermMapper.h
+++ b/src/cnfizers/TermMapper.h
@@ -26,8 +26,8 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 #ifndef TERMMAPPER_H
 #define TERMMAPPER_H
 #include "Logic.h"
-#include "Map.h"
 #include "PTRef.h"
+#include <minisat/mtl/Map.h>
 
 class TermMapper {
 private:
diff --git a/src/common/CMakeLists.txt b/src/common/CMakeLists.txt
index 20447fdc9..5ba51c00e 100644
--- a/src/common/CMakeLists.txt
+++ b/src/common/CMakeLists.txt
@@ -1,11 +1,11 @@
-add_library(common OBJECT "FastRational.cc" Real.h)
+add_library(common OBJECT "")
 
 target_sources(common
-    PUBLIC "${CMAKE_CURRENT_LIST_DIR}/FastRational.h"
-    PUBLIC "${CMAKE_CURRENT_LIST_DIR}/FlaPartitionMap.cc"
+    PUBLIC
+        "${CMAKE_CURRENT_LIST_DIR}/FastRational.cc"
+        "${CMAKE_CURRENT_LIST_DIR}/FlaPartitionMap.cc"
+        "${CMAKE_CURRENT_LIST_DIR}/Real.h"
     PRIVATE
-    "${CMAKE_CURRENT_LIST_DIR}/Alloc.h"
-    "${CMAKE_CURRENT_LIST_DIR}/XAlloc.h"
     "${CMAKE_CURRENT_LIST_DIR}/SystemQueries.h"
     "${CMAKE_CURRENT_LIST_DIR}/Integer.h"
     "${CMAKE_CURRENT_LIST_DIR}/Number.h"
@@ -22,7 +22,7 @@ target_sources(common
 )
 
 install(FILES
-        Integer.h Number.h FastRational.h XAlloc.h Alloc.h StringMap.h Timer.h osmtinttypes.h
+        Integer.h Number.h FastRational.h StringMap.h Timer.h osmtinttypes.h
         TreeOps.h Real.h FlaPartitionMap.h PartitionInfo.h OsmtApiException.h TypeUtils.h
         NumberUtils.h NatSet.h ScopedVector.h
 DESTINATION ${INSTALL_HEADERS_DIR})
diff --git a/src/common/FastRational.h b/src/common/FastRational.h
index a69606fbd..4c2984566 100644
--- a/src/common/FastRational.h
+++ b/src/common/FastRational.h
@@ -6,14 +6,14 @@ Copyright (c) 2008, 2009 Centre national de la recherche scientifique (CNRS)
  */
 #ifndef FAST_RATIONALS_H
 #define FAST_RATIONALS_H
-#include <string>
 #include <gmpxx.h>
 #include <cassert>
 #include <climits>
-#include "Vec.h"
+#include <cstdint>
+#include <optional>
 #include <stack>
+#include <string>
 #include <vector>
-#include <optional>
 
 typedef int32_t  word;
 typedef uint32_t uword;
diff --git a/src/common/PartitionInfo.h b/src/common/PartitionInfo.h
index 36be79af1..06459449a 100644
--- a/src/common/PartitionInfo.h
+++ b/src/common/PartitionInfo.h
@@ -10,8 +10,8 @@
 #include "InterpolationUtils.h"
 #include "PTRef.h"
 #include "SymRef.h"
-#include "SolverTypes.h"
 #include "FlaPartitionMap.h"
+#include <minisat/core/SolverTypes.h>
 
 
 class PartitionInfo {
diff --git a/src/common/StringMap.h b/src/common/StringMap.h
index d7946cfd5..c224afd82 100644
--- a/src/common/StringMap.h
+++ b/src/common/StringMap.h
@@ -27,7 +27,7 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 #ifndef STRINGMAP_H
 #define STRINGMAP_H
 
-#include "Map.h"
+#include <minisat/mtl/Map.h>
 
 //===================================================================================================
 // Specializations for string hashing (Map from mtl)
diff --git a/src/common/TreeOps.h b/src/common/TreeOps.h
index 2350aa048..bace4a7f7 100644
--- a/src/common/TreeOps.h
+++ b/src/common/TreeOps.h
@@ -13,7 +13,7 @@
 #include "Logic.h"
 #include "NatSet.h"
 #include "Pterm.h"
-#include "Vec.h"
+#include <minisat/mtl/Vec.h>
 
 #include <unordered_set>
 
diff --git a/src/itehandler/CMakeLists.txt b/src/itehandler/CMakeLists.txt
index d06694cac..20e4633cd 100644
--- a/src/itehandler/CMakeLists.txt
+++ b/src/itehandler/CMakeLists.txt
@@ -1,3 +1,5 @@
+
+
 add_library(itehandler OBJECT IteToSwitch.cc IteToSwitchMisc.cc IteHandler.cc)
-install(FILES IteToSwitch.h IteHandler.h DESTINATION ${INSTALL_HEADERS_DIR})
+
 
diff --git a/src/logics/Logic.h b/src/logics/Logic.h
index f3f1d18a7..4639a1d02 100644
--- a/src/logics/Logic.h
+++ b/src/logics/Logic.h
@@ -14,11 +14,11 @@
 #include "SStore.h"
 #include "CgTypes.h"
 #include "LogicFactory.h"
-#include "MapWithKeys.h"
 #include "OsmtApiException.h"
 #include "FunctionTools.h"
 #include "TypeUtils.h"
 #include "NatSet.h"
+#include <minisat/mtl/MapWithKeys.h>
 
 #include <cassert>
 #include <cstring>
diff --git a/src/logics/SubstLoopBreaker.h b/src/logics/SubstLoopBreaker.h
index cd3bc00e2..5497812a9 100644
--- a/src/logics/SubstLoopBreaker.h
+++ b/src/logics/SubstLoopBreaker.h
@@ -4,13 +4,14 @@
 
 #ifndef OPENSMT_SUBSTLOOPBREAKER_H
 #define OPENSMT_SUBSTLOOPBREAKER_H
-#include <stdint.h>
+
 #include <PTRef.h>
-#include <Sort.h>
-#include <Alloc.h>
-#include <assert.h>
 #include <PtStructs.h>
 #include <Logic.h>
+#include <minisat/mtl/Sort.h>
+
+#include <cassert>
+#include <cstdint>
 
 // For breaking substitution loops
 enum class NStatus { inStack, complete, unseen };
diff --git a/src/logics/Theory.h b/src/logics/Theory.h
index 3d52f526f..2be77712b 100644
--- a/src/logics/Theory.h
+++ b/src/logics/Theory.h
@@ -26,15 +26,12 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 #ifndef THEORY_H
 #define THEORY_H
 
-#include <memory>
-
-#include "Logic.h"
 #include "BVLogic.h"
-
+#include "Logic.h"
+#include "PartitionManager.h"
 #include "UFTHandler.h"
-#include "Alloc.h"
 
-#include "PartitionManager.h"
+#include <memory>
 
 struct PreprocessingContext {
     std::size_t frameCount {0};
diff --git a/src/minisat/CMakeLists.txt b/src/minisat/CMakeLists.txt
index 10ce1fb20..4b2ecb0d5 100644
--- a/src/minisat/CMakeLists.txt
+++ b/src/minisat/CMakeLists.txt
@@ -1,12 +1,20 @@
 add_library(minisat INTERFACE)
 
-target_include_directories(minisat
-    INTERFACE ${CMAKE_CURRENT_LIST_DIR}/mtl
-    INTERFACE ${CMAKE_CURRENT_LIST_DIR}/core
-    )
+install(FILES 
+        mtl/Heap.h
+        mtl/Map.h
+        mtl/Vec.h
+        mtl/Alg.h
+        mtl/Sort.h
+        mtl/Queue.h
+        mtl/MapWithKeys.h
+        DESTINATION ${INSTALL_HEADERS_DIR}/minisat/mtl
+)
 
+install(FILES
+        core/SolverTypes.h
+        core/Alloc.h
+        core/XAlloc.h
+        DESTINATION ${INSTALL_HEADERS_DIR}/minisat/core)
 
-install(FILES 
-mtl/Heap.h mtl/Map.h mtl/Vec.h mtl/Alg.h mtl/Sort.h mtl/Queue.h core/SolverTypes.h mtl/MapWithKeys.h
- DESTINATION ${INSTALL_HEADERS_DIR})
 
diff --git a/src/common/Alloc.h b/src/minisat/core/Alloc.h
similarity index 99%
rename from src/common/Alloc.h
rename to src/minisat/core/Alloc.h
index f63591ebf..9c4c131d2 100644
--- a/src/common/Alloc.h
+++ b/src/minisat/core/Alloc.h
@@ -20,9 +20,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #ifndef Minisat_Alloc_h
 #define Minisat_Alloc_h
-#include "osmtinttypes.h"
+
 #include "XAlloc.h"
-#include "Vec.h"
+#include <minisat/mtl/Vec.h>
 
 //=================================================================================================
 // Simple Region-based memory allocator:
diff --git a/src/minisat/core/SolverTypes.h b/src/minisat/core/SolverTypes.h
index 32648b3d5..4a0105167 100644
--- a/src/minisat/core/SolverTypes.h
+++ b/src/minisat/core/SolverTypes.h
@@ -22,9 +22,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_SolverTypes_h
 #define Minisat_SolverTypes_h
 
-#include "Alg.h"
-#include "Vec.h"
-#include "Map.h"
+#include <minisat/mtl/Alg.h>
+#include <minisat/mtl/Vec.h>
+#include <minisat/mtl/Map.h>
 #include "Alloc.h"
 
 #include <cassert>
diff --git a/src/common/XAlloc.h b/src/minisat/core/XAlloc.h
similarity index 97%
rename from src/common/XAlloc.h
rename to src/minisat/core/XAlloc.h
index 66f6aed85..00772886a 100644
--- a/src/common/XAlloc.h
+++ b/src/minisat/core/XAlloc.h
@@ -21,8 +21,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_XAlloc_h
 #define Minisat_XAlloc_h
 
-#include <errno.h>
-#include <stdlib.h>
+#include <cerrno>
+#include <cstdlib>
 
 
 //=================================================================================================
diff --git a/src/minisat/mtl/Heap.h b/src/minisat/mtl/Heap.h
index da7c9258f..036eeb4f5 100644
--- a/src/minisat/mtl/Heap.h
+++ b/src/minisat/mtl/Heap.h
@@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #define Minisat_Heap_h
 
 #include "Vec.h"
-#include "stdio.h"
+#include <cstdio>
 
 //=================================================================================================
 // A heap implementation with support for decrease/increase key.
diff --git a/src/minisat/mtl/Map.h b/src/minisat/mtl/Map.h
index b9e77887c..f96f276f9 100644
--- a/src/minisat/mtl/Map.h
+++ b/src/minisat/mtl/Map.h
@@ -20,7 +20,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_Map_h
 #define Minisat_Map_h
 
-#include "osmtinttypes.h"
 #include "Vec.h"
 #include <vector>
 
diff --git a/src/minisat/mtl/Vec.h b/src/minisat/mtl/Vec.h
index 1e6593df8..6ee25fdcf 100644
--- a/src/minisat/mtl/Vec.h
+++ b/src/minisat/mtl/Vec.h
@@ -22,13 +22,15 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_Vec_h
 #define Minisat_Vec_h
 
+#include <minisat/core/XAlloc.h>
+
 #include <cassert>
-#include <new>
+#include <climits>
+#include <cstdint>
 #include <initializer_list>
-#include <vector>
+#include <new>
 #include <utility>
-#include "osmtinttypes.h"
-#include "XAlloc.h"
+#include <vector>
 
 //=================================================================================================
 // Automatically resizable arrays
diff --git a/src/options/SMTConfig.cc b/src/options/SMTConfig.cc
index bb9401667..b938446bf 100644
--- a/src/options/SMTConfig.cc
+++ b/src/options/SMTConfig.cc
@@ -541,7 +541,6 @@ void
 SMTConfig::initializeConfig( )
 {
   // Set Global Default configuration
-  status                        = l_Undef;
   insertOption(o_produce_stats, new SMTOption(0));
 //  produce_stats                 = 0;
 //  produce_models                = 0;
diff --git a/src/options/SMTConfig.h b/src/options/SMTConfig.h
index e799c7924..b986d2e50 100644
--- a/src/options/SMTConfig.h
+++ b/src/options/SMTConfig.h
@@ -27,10 +27,11 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 #ifndef SMTCONFIG_H
 #define SMTCONFIG_H
 
-#include "SolverTypes.h"
 #include "StringMap.h"
 #include "smt2tokens.h"
 
+#include <minisat/mtl/Vec.h>
+
 #include <cstring>
 #include <libgen.h>
 #include <iostream>
@@ -503,7 +504,6 @@ struct SMTConfig
     }
   }
 
-  lbool        status;                       // Status of the benchmark
 //  int          incremental;                  // Incremental solving
   int           isIncremental() const
      { return optionTable.has(o_incremental) ?
diff --git a/src/parallel/SplitData.h b/src/parallel/SplitData.h
index 370f00b75..9260b6ca0 100644
--- a/src/parallel/SplitData.h
+++ b/src/parallel/SplitData.h
@@ -8,8 +8,8 @@
 #ifndef PARALLEL_SPLITDATA_H
 #define PARALLEL_SPLITDATA_H
 
-#include "SolverTypes.h"
 #include "THandler.h"
+#include <minisat/core/SolverTypes.h>
 
 // -----------------------------------------------------------------------------------------
 // The splits
diff --git a/src/pterms/PtStructs.h b/src/pterms/PtStructs.h
index bde0229ef..475c1dfbf 100644
--- a/src/pterms/PtStructs.h
+++ b/src/pterms/PtStructs.h
@@ -8,8 +8,8 @@
 #ifndef OPENSMT_PTHELPERSTRUCTS_H
 #define OPENSMT_PTHELPERSTRUCTS_H
 
-#include "SolverTypes.h"
 #include "PTRef.h"
+#include <minisat/core/SolverTypes.h>
 
 class PtAsgn {
 public:
diff --git a/src/pterms/Pterm.h b/src/pterms/Pterm.h
index 2c4be2692..547b92e70 100644
--- a/src/pterms/Pterm.h
+++ b/src/pterms/Pterm.h
@@ -28,9 +28,9 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 #ifndef PTERM_H
 #define PTERM_H
 
-#include "Vec.h"
-#include "Sort.h"
-#include "SolverTypes.h"
+#include <minisat/mtl/Vec.h>
+#include <minisat/core/SolverTypes.h>
+#include <minisat/mtl/Sort.h>
 #include "SymRef.h"
 #include "PtStructs.h"
 
diff --git a/src/smtsolvers/CMakeLists.txt b/src/smtsolvers/CMakeLists.txt
index 69a79101c..8fce3533c 100644
--- a/src/smtsolvers/CMakeLists.txt
+++ b/src/smtsolvers/CMakeLists.txt
@@ -1,6 +1,5 @@
 add_library(smtsolvers OBJECT "")
 
-
 list(APPEND PRIVATE_SOURCES_TO_ADD
 		"${CMAKE_CURRENT_SOURCE_DIR}/SimpSMTSolver.cc"
 		"${CMAKE_CURRENT_SOURCE_DIR}/CoreSMTSolver.cc"
@@ -37,9 +36,5 @@ target_sources(proof
 	PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/ResolutionProof.h"
 	PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/ResolutionProof.cc")
 
-install(FILES TheoryInterpolator.h
-	 DESTINATION ${INSTALL_HEADERS_DIR})
-
-
-install(FILES SimpSMTSolver.h CoreSMTSolver.h
-		DESTINATION ${INSTALL_HEADERS_DIR})
+install(FILES TheoryInterpolator.h SimpSMTSolver.h CoreSMTSolver.h
+	 DESTINATION ${INSTALL_HEADERS_DIR})
\ No newline at end of file
diff --git a/src/smtsolvers/CoreSMTSolver.cc b/src/smtsolvers/CoreSMTSolver.cc
index 82b94f9a9..e9d9be97e 100644
--- a/src/smtsolvers/CoreSMTSolver.cc
+++ b/src/smtsolvers/CoreSMTSolver.cc
@@ -48,19 +48,16 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "ModelBuilder.h"
 #include "OsmtInternalException.h"
-#include "Sort.h"
+#include "Random.h"
+#include "ReportUtils.h"
+#include "ResolutionProof.h"
+#include "SystemQueries.h"
 
 #include <cmath>
 #include <iostream>
 #include <iomanip>
 #include <algorithm>
 
-#include "ResolutionProof.h"
-#include "SystemQueries.h"
-#include "ReportUtils.h"
-
-#include "Random.h"
-
 namespace opensmt {
     extern bool stop;
 }
diff --git a/src/smtsolvers/CoreSMTSolver.h b/src/smtsolvers/CoreSMTSolver.h
index 1061614cb..d795aaf93 100644
--- a/src/smtsolvers/CoreSMTSolver.h
+++ b/src/smtsolvers/CoreSMTSolver.h
@@ -55,11 +55,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include <vector>
 
-#include "Vec.h"
-#include "Heap.h"
-#include "Alg.h"
+#include <minisat/mtl/Vec.h>
+#include <minisat/mtl/Heap.h>
+#include <minisat/mtl/Alg.h>
 
-#include "SolverTypes.h"
+#include <minisat/core/SolverTypes.h>
 
 #include "Timer.h"
 
diff --git a/src/smtsolvers/LAScore.h b/src/smtsolvers/LAScore.h
index 74a0a96e9..18250ac05 100644
--- a/src/smtsolvers/LAScore.h
+++ b/src/smtsolvers/LAScore.h
@@ -5,7 +5,7 @@
 #ifndef OPENSMT_LASCORE_H
 #define OPENSMT_LASCORE_H
 
-#include <SolverTypes.h>
+#include <minisat/core/SolverTypes.h>
 #include <SMTConfig.h>
 #include <TypeUtils.h>
 
diff --git a/src/smtsolvers/ResolutionProof.h b/src/smtsolvers/ResolutionProof.h
index 4e90831b5..d1a994a09 100644
--- a/src/smtsolvers/ResolutionProof.h
+++ b/src/smtsolvers/ResolutionProof.h
@@ -26,7 +26,7 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 #ifndef PROOF2_H
 #define PROOF2_H
 
-#include "SolverTypes.h"
+#include <minisat/core/SolverTypes.h>
 #include <vector>
 #include <unordered_map>
 #include <iosfwd>
diff --git a/src/smtsolvers/SimpSMTSolver.cc b/src/smtsolvers/SimpSMTSolver.cc
index b51ad6b8e..a87a6f144 100644
--- a/src/smtsolvers/SimpSMTSolver.cc
+++ b/src/smtsolvers/SimpSMTSolver.cc
@@ -47,7 +47,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "SimpSMTSolver.h"
 
 #include "ReportUtils.h"
-#include "Sort.h"
 
 //=================================================================================================
 // Constructor/Destructor:
diff --git a/src/smtsolvers/SimpSMTSolver.h b/src/smtsolvers/SimpSMTSolver.h
index 51563bccc..5c2c5782b 100644
--- a/src/smtsolvers/SimpSMTSolver.h
+++ b/src/smtsolvers/SimpSMTSolver.h
@@ -46,8 +46,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef SIMP_SMT_SOLVER_H
 #define SIMP_SMT_SOLVER_H
 
-#include "Queue.h"
 #include "CoreSMTSolver.h"
+#include <minisat/mtl/Queue.h>
 
 class SimpSMTSolver : public CoreSMTSolver
 {
diff --git a/src/sorts/SSort.h b/src/sorts/SSort.h
index 14922397a..3a7ef8286 100644
--- a/src/sorts/SSort.h
+++ b/src/sorts/SSort.h
@@ -27,8 +27,8 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 #ifndef SORT_H
 #define SORT_H
 
-#include "Vec.h"
-#include "Alloc.h"
+#include <minisat/mtl/Vec.h>
+#include <minisat/core/Alloc.h>
 
 #include <string>
 
diff --git a/src/sorts/SStore.h b/src/sorts/SStore.h
index 683305081..11e738144 100644
--- a/src/sorts/SStore.h
+++ b/src/sorts/SStore.h
@@ -28,8 +28,8 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 #define SSTORE_H
 
 #include "SSort.h"
-#include "Alloc.h"
 #include "TypeUtils.h"
+#include <minisat/core/Alloc.h>
 
 
 #include <unordered_map>
diff --git a/src/symbols/CMakeLists.txt b/src/symbols/CMakeLists.txt
index 5634eaa6c..1b0fe61bd 100644
--- a/src/symbols/CMakeLists.txt
+++ b/src/symbols/CMakeLists.txt
@@ -7,7 +7,5 @@ PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/SymStore.h"
 PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/SymStore.cc"
 )
 
-#target_link_libraries(symbols sorts)
-
 install(FILES Symbol.h SymStore.h SymRef.h DESTINATION ${INSTALL_HEADERS_DIR})
 
diff --git a/src/symbols/SymRef.h b/src/symbols/SymRef.h
index d70758cb8..3dd399db4 100644
--- a/src/symbols/SymRef.h
+++ b/src/symbols/SymRef.h
@@ -26,7 +26,7 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 #ifndef OPENSMT_SYMREF_H
 #define OPENSMT_SYMREF_H
 
-#include "Map.h"
+#include <minisat/mtl/Map.h>
 
 struct SymRef {
     uint32_t x;
diff --git a/src/symbols/Symbol.h b/src/symbols/Symbol.h
index 4b6f6018e..b4d90b763 100644
--- a/src/symbols/Symbol.h
+++ b/src/symbols/Symbol.h
@@ -28,8 +28,8 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 #ifndef SYMBOL_H
 #define SYMBOL_H
 
-#include "Vec.h"
-#include "Alloc.h"
+#include <minisat/mtl/Vec.h>
+#include <minisat/core/Alloc.h>
 #include "SSort.h"
 
 #include "SymRef.h"
diff --git a/src/tsolvers/Deductions.h b/src/tsolvers/Deductions.h
index 14b77de63..9c5b2696f 100644
--- a/src/tsolvers/Deductions.h
+++ b/src/tsolvers/Deductions.h
@@ -27,7 +27,7 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 #ifndef DEDUCTIONS_H
 #define DEDUCTIONS_H
 
-#include "SolverTypes.h"
+#include <minisat/core/SolverTypes.h>
 
 struct SolverId {
     uint32_t id;
diff --git a/src/tsolvers/TSolver.h b/src/tsolvers/TSolver.h
index a2106a53e..23f57c92d 100644
--- a/src/tsolvers/TSolver.h
+++ b/src/tsolvers/TSolver.h
@@ -30,9 +30,9 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 #include "PtStructs.h"
 #include "SMTConfig.h"
 #include "Deductions.h"
-#include "SolverTypes.h"
 #include "TResult.h"
-#include "MapWithKeys.h"
+#include <minisat/core/SolverTypes.h>
+#include <minisat/mtl/MapWithKeys.h>
 
 #include <unordered_set>
 
diff --git a/src/tsolvers/bvsolver/Bvector.h b/src/tsolvers/bvsolver/Bvector.h
index d4fb006ec..a454e2c1b 100644
--- a/src/tsolvers/bvsolver/Bvector.h
+++ b/src/tsolvers/bvsolver/Bvector.h
@@ -25,11 +25,12 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 
 #ifndef BVECTOR_H
 #define BVECTOR_H
-#include "Vec.h"
-#include "Alloc.h"
+
 #include "PTRef.h"
 
-#include "Map.h"
+#include <minisat/core/Alloc.h>
+#include <minisat/mtl/Map.h>
+#include <minisat/mtl/Vec.h>
 
 struct BVRef {
     uint32_t x;
diff --git a/src/tsolvers/egraph/Enode.h b/src/tsolvers/egraph/Enode.h
index f934e94ed..8c08fad80 100644
--- a/src/tsolvers/egraph/Enode.h
+++ b/src/tsolvers/egraph/Enode.h
@@ -27,13 +27,11 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 #ifndef ENODE_H
 #define ENODE_H
 
-#include "Vec.h"
-#include "Alloc.h"
-
 #include "PtStructs.h"
 #include "SymRef.h"
 #include "TypeUtils.h"
 #include "CgTypes.h"
+#include <minisat/mtl/Vec.h>
 
 struct ERef {
     uint32_t x;
diff --git a/src/tsolvers/lasolver/LABounds.cc b/src/tsolvers/lasolver/LABounds.cc
index 9ccc1ecf2..587fbf67e 100644
--- a/src/tsolvers/lasolver/LABounds.cc
+++ b/src/tsolvers/lasolver/LABounds.cc
@@ -1,6 +1,6 @@
 #include "LABounds.h"
-#include "Map.h"
-#include "Sort.h"
+#include <minisat/mtl/Map.h>
+#include <minisat/mtl/Sort.h>
 
 LABound::LABound(BoundT type, LVRef var, Delta && delta, int id)
     : type(type.t)
diff --git a/src/tsolvers/lasolver/LABounds.h b/src/tsolvers/lasolver/LABounds.h
index 4b5cfd02e..68adde8f8 100644
--- a/src/tsolvers/lasolver/LABounds.h
+++ b/src/tsolvers/lasolver/LABounds.h
@@ -4,7 +4,8 @@
 #include "Delta.h"
 #include "LARefs.h"
 #include "LAVar.h"
-#include "Alloc.h"
+#include <minisat/core/Alloc.h>
+#include <minisat/mtl/Vec.h>
 
 //
 // Bound index type.  The bounds are ordered in a list, and indexed using a number in the list.
diff --git a/src/tsolvers/lasolver/LAVarMapper.h b/src/tsolvers/lasolver/LAVarMapper.h
index 8ebddeec4..bc12985b6 100644
--- a/src/tsolvers/lasolver/LAVarMapper.h
+++ b/src/tsolvers/lasolver/LAVarMapper.h
@@ -10,7 +10,7 @@
 
 #include "LARefs.h"
 #include "Pterm.h"
-#include "Vec.h"
+#include <minisat/mtl/Vec.h>
 
 class ArithLogic;
 
diff --git a/src/tsolvers/lasolver/LRAModel.h b/src/tsolvers/lasolver/LRAModel.h
index e469b85c5..273ba6bbc 100644
--- a/src/tsolvers/lasolver/LRAModel.h
+++ b/src/tsolvers/lasolver/LRAModel.h
@@ -5,13 +5,14 @@
 #ifndef OPENSMT_LRAMODEL_H
 #define OPENSMT_LRAMODEL_H
 
-#include <cstdint>
 #include "Delta.h"
 #include "LABounds.h"
-#include "Vec.h"
 #include "LARefs.h"
 #include "LAVarMapper.h"
 #include "NatSet.h"
+#include <minisat/mtl/Vec.h>
+
+#include <cstdint>
 
 //
 // Class for maintaining the model of a variable
diff --git a/src/tsolvers/stpsolver/STPStore.h b/src/tsolvers/stpsolver/STPStore.h
index de6bbe12c..8105b21f2 100644
--- a/src/tsolvers/stpsolver/STPStore.h
+++ b/src/tsolvers/stpsolver/STPStore.h
@@ -1,11 +1,11 @@
 #ifndef OPENSMT_STPSTORE_H
 #define OPENSMT_STPSTORE_H
 
-#include <cstdint>
-#include <vector>
 #include <Number.h>
-#include <SolverTypes.h>
 #include <PtStructs.h>
+
+#include <cstdint>
+#include <vector>
 // implementations of template functions #included below class definitions
 
 struct VertexRef {
diff --git a/test/unit/test_LIACutSolver.cpp b/test/unit/test_LIACutSolver.cpp
index 2842b0c1e..081081901 100644
--- a/test/unit/test_LIACutSolver.cpp
+++ b/test/unit/test_LIACutSolver.cpp
@@ -1,11 +1,7 @@
 #include <gtest/gtest.h>
 #include <Real.h>
-#include <stdlib.h>
-#include <Vec.h>
-#include <Sort.h>
 #include <SMTConfig.h>
 #include <lasolver/Simplex.h>
-#include <lasolver/LASolver.h>
 
 using Polynomial = PolynomialT<LVRef>;
 
@@ -64,62 +60,4 @@ TEST(LIACutSolver_test, test_computeEqualityBasis)
 
     Simplex::Explanation explanation = s->checkSimplex();
     ASSERT_EQ(explanation.size(), 0); //this property has to be failed as the system is UNSAT then explanation size has to be >0
-
 }
-
-
-/*
- *
-vec<PtAsgn> ex;
-ex.clear();
-bool complete;
-ex = s->check_simplex(complete);
-ASSERT_EQ(ex.size(), 0);
-
-Real d = s->computeDelta();
-Delta x_val = s.getValuation(x);
-cout << x_val.R() + x_val.D() * d << endl;
-
-Delta y_val = s.getValuation(y);
-cout << y_val.R() + y_val.D() * d << endl;
-
-Delta sum = s.getValuation(y_minus_x);
-cout << sum.R() + sum.D() * d << endl;
-
-//call initialize function and check delta part to see if initilize did its job
-
-///up to now we created vars, polynomial, checked simplex on them and if simplex not UNSAT then compute equal basis
-
-std::unique_ptr<LRAModel> eqBasisModel = model.copyFlat(); // copy the model as a snapshot of the most recent values
-auto eqBasisSimplex = std::unique_ptr<Simplex>(new Simplex(config, *eqBasisModel, boundStore));
-eqBasisSimplex->initFromSimplex(s);  // Initialize the new simplex (mostly tableau) from the old simplex
-
-//removes all bounds that cannot produce equalities and turns Ax<=b to Ax<b
-initialize(*eqBasisSimplex, *eqBasisModel);
-
-//if delta part is zero it means <=, otherwise <. Hence call simplex to solve it
-
-std::vector<LABoundRef> explanationBounds;
-eqBasisSimplex->checkSimplex(explanationBounds, explanationCoefficients);
-
-//size of explanation now has to increase, should not be zero
-
-d = eqBasisSimplex->computeDelta();
-Delta x_val = eqBasisSimplex.getValuation(x);
-cout << x_val.R() + x_val.D() * d << endl;
-cout << x_val.D() << endl;
-
-Delta y_val = eqBasisSimplex.getValuation(y);
-cout << y_val.R() + y_val.D() * d << endl;
-cout << y_val.D() << endl;
-
-Delta sum = eqBasisSimplex.getValuation(y_minus_x);
-cout << sum.R() + sum.D() * d << endl;
-cout << sum.D() << endl;
-
-//1. give an example of inequallity system that implies equality
-//2. give it bounds
-//3. initialize removes all bounds that cannot produce equalities and turns Ax<=b to Ax<b
-//4. ckeck simplex on Ax<b if Ax<b is UNSAT then AX<=b implies equality
-*/
-
diff --git a/test/unit/test_LIAStrengthening.cc b/test/unit/test_LIAStrengthening.cc
index b6d7423f0..1ab85621e 100644
--- a/test/unit/test_LIAStrengthening.cc
+++ b/test/unit/test_LIAStrengthening.cc
@@ -3,10 +3,6 @@
 //
 #include <gtest/gtest.h>
 #include <Real.h>
-#include <stdlib.h>
-#include <Vec.h>
-#include <Sort.h>
-#include <SMTConfig.h>
 #include <ArithLogic.h>
 
 class LIAStrengthening: public ::testing::Test {
diff --git a/test/unit/test_Proof.cc b/test/unit/test_Proof.cc
index da9f7bc24..9f535ffc6 100644
--- a/test/unit/test_Proof.cc
+++ b/test/unit/test_Proof.cc
@@ -151,8 +151,8 @@ TEST_F(ReductionTest, test_recyclePivots) {
         proof.newOriginalClause(cr);
     }
     // Learnt clauses
-    CRef a_c = ca.alloc(vec<Lit>{a,c}, {true, 0});
-    CRef nd = ca.alloc(vec<Lit>{~d}, {true, 0});
+    CRef a_c = ca.alloc(vec<Lit>{a,c}, true, 0);
+    CRef nd = ca.alloc(vec<Lit>{~d}, true, 0);
 
     proof.beginChain(a_b);
     proof.addResolutionStep(nb_c, var(b));
@@ -201,19 +201,19 @@ TEST_F(ReductionTest, test_recyclePivots_IdenticalAntecedents) {
         proof.newOriginalClause(cr);
     }
     // Learnt clauses
-    CRef a_b = ca.alloc(vec<Lit>{a,b}, {true, 0});
+    CRef a_b = ca.alloc(vec<Lit>{a,b}, true, 0);
 
     proof.beginChain(a_d);
     proof.addResolutionStep(b_nd, var(d));
     proof.endChain(a_b);
 
-    CRef b_c = ca.alloc(vec<Lit>{b,c}, {true, 0});
+    CRef b_c = ca.alloc(vec<Lit>{b,c}, true, 0);
 
     proof.beginChain(na_c);
     proof.addResolutionStep(a_b, var(a));
     proof.endChain(b_c);
 
-    CRef ne = ca.alloc(vec<Lit>{~e}, {true, 0});
+    CRef ne = ca.alloc(vec<Lit>{~e}, true, 0);
 
     proof.beginChain(b_nc_nd_ne);
     proof.addResolutionStep(b_c, var(c));
@@ -261,19 +261,19 @@ TEST_F(ReductionTest, test_recyclePivots_IdenticalAntecedents_AfterPhaseOneRepla
         proof.newOriginalClause(cr);
     }
     // Learnt clauses
-    CRef a_b = ca.alloc(vec<Lit>{a,b}, {true, 0});
+    CRef a_b = ca.alloc(vec<Lit>{a,b}, true, 0);
 
     proof.beginChain(a_d);
     proof.addResolutionStep(b_nd, var(d));
     proof.endChain(a_b);
 
-    CRef b_c = ca.alloc(vec<Lit>{b,c}, {true, 0});
+    CRef b_c = ca.alloc(vec<Lit>{b,c}, true, 0);
 
     proof.beginChain(na_c);
     proof.addResolutionStep(a_b, var(a));
     proof.endChain(b_c);
 
-    CRef ne = ca.alloc(vec<Lit>{~e}, {true, 0});
+    CRef ne = ca.alloc(vec<Lit>{~e}, true, 0);
 
     proof.beginChain(b_nc_nd_ne);
     proof.addResolutionStep(b_c, var(c));
@@ -319,7 +319,7 @@ TEST_F(ReductionTest, test_proofTransformAndRestructure) {
         proof.newOriginalClause(cr);
     }
     // Learnt clauses
-    CRef a_d = ca.alloc(vec<Lit>{a,d}, {true, 0});
+    CRef a_d = ca.alloc(vec<Lit>{a,d}, true, 0);
 
     proof.beginChain(a_e);
     proof.addResolutionStep(d_ne, var(e));
@@ -381,13 +381,13 @@ TEST_F(ReductionTest, test_proofTransformAndRestructure_IdenticalAntecedents) {
     }
 
     // learnt clauses
-    CRef na_c_d = ca.alloc(vec<Lit>{~a,c,d}, {true, 0});
+    CRef na_c_d = ca.alloc(vec<Lit>{~a,c,d}, true, 0);
     proof.beginChain(a_b);
     proof.addResolutionStep(na_c, var(a));
     proof.addResolutionStep(na_nb_d,var(b));
     proof.endChain(na_c_d);
 
-    CRef na_c_e = ca.alloc(vec<Lit>{~a,c,e}, {true, 0});
+    CRef na_c_e = ca.alloc(vec<Lit>{~a,c,e}, true, 0);
     proof.beginChain(nd_e);
     proof.addResolutionStep(na_c_d, var(d));
     proof.endChain(na_c_e);
diff --git a/test/unit/test_Rationals.cpp b/test/unit/test_Rationals.cpp
index 8890b8255..efa89726c 100644
--- a/test/unit/test_Rationals.cpp
+++ b/test/unit/test_Rationals.cpp
@@ -1,8 +1,7 @@
 #include <gtest/gtest.h>
 #include <Real.h>
-#include <stdlib.h>
-#include <Vec.h>
-#include <Sort.h>
+
+#include <vector>
 
 using Real = opensmt::Real;
 
@@ -35,15 +34,15 @@ TEST(Rationals_test, test_normalized)
 
 TEST(Rationals_test, test_hash_function)
 {
-    vec<uint32_t> hashes;
+    std::vector<uint32_t> hashes;
     opensmt::NumberHash hasher;
     for (int i = 0; i < 10; i++) {
         Real r((int)random());
-        hashes.push(hasher(r));
+        hashes.push_back(hasher(r));
     }
     for (int i = 0; i < 10; i++) {
         Real r(i);
-        hashes.push(hasher(r));
+        hashes.push_back(hasher(r));
     }
     for (int i = 0; i < 10; i++) {
         char* str;
@@ -51,7 +50,7 @@ TEST(Rationals_test, test_hash_function)
         assert(written != -1); (void)written;
         Real r(str);
         free(str);
-        hashes.push(hasher(r));
+        hashes.push_back(hasher(r));
     }
 
     for (int i = 0; i < 10; i++) {
@@ -70,7 +69,7 @@ TEST(Rationals_test, test_hash_function)
         assert(written != -1); (void)written;
         Real r(str);
         free(str);
-        hashes.push(hasher(r));
+        hashes.push_back(hasher(r));
     }
 
     for (int k = 0; k < 10; k++) {
@@ -87,12 +86,12 @@ TEST(Rationals_test, test_hash_function)
             assert(written != -1); (void)written;
             Real r(str);
             free(str);
-            hashes.push(hasher(r));
+            hashes.push_back(hasher(r));
         }
     }
-    sort(hashes);
+    std::sort(hashes.begin(), hashes.end());
     int prev = hashes[0];
-    for (int i = 1; i < hashes.size(); i++) {
+    for (std::size_t i = 1; i < hashes.size(); i++) {
         ASSERT_NE(prev, hashes[i]);
         prev = hashes[i];
     }
diff --git a/test/unit/test_SATSolverTypes.cc b/test/unit/test_SATSolverTypes.cc
index a94df4321..0e4117433 100644
--- a/test/unit/test_SATSolverTypes.cc
+++ b/test/unit/test_SATSolverTypes.cc
@@ -5,7 +5,7 @@
  */
 
 #include <gtest/gtest.h>
-#include "SolverTypes.h"
+#include <minisat/core/SolverTypes.h>
 #include <numeric>
 
 class SATSolverTypesTest : public ::testing::Test {
diff --git a/test/unit/test_SubstitutionBreaker.cpp b/test/unit/test_SubstitutionBreaker.cpp
index 8ce7e7d30..e5d28193c 100644
--- a/test/unit/test_SubstitutionBreaker.cpp
+++ b/test/unit/test_SubstitutionBreaker.cpp
@@ -3,10 +3,8 @@
 //
 #include <gtest/gtest.h>
 #include <Logic.h>
-#include <Map.h>
 #include <SubstLoopBreaker.h>
 
-typedef Map<PTRef,PtAsgn,PTRefHash>::Pair spair;
 
 class SubstitutionBreaker : public ::testing::Test {
 public: