diff --git a/mk_make.py b/mk_make.py
index 35c06b4c5..92b0cf4a0 100644
--- a/mk_make.py
+++ b/mk_make.py
@@ -158,4 +158,5 @@ def add_lib(name, deps):
 
 add_lib('util', [])
 add_lib('polynomial', ['util'])
+add_lib('sat', ['util'])
 add_lib('ast', ['util', 'polynomial'])
diff --git a/lib/luby.cpp b/src/sat/luby.cpp
similarity index 100%
rename from lib/luby.cpp
rename to src/sat/luby.cpp
diff --git a/lib/luby.h b/src/sat/luby.h
similarity index 100%
rename from lib/luby.h
rename to src/sat/luby.h
diff --git a/lib/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp
similarity index 100%
rename from lib/sat_asymm_branch.cpp
rename to src/sat/sat_asymm_branch.cpp
diff --git a/lib/sat_asymm_branch.h b/src/sat/sat_asymm_branch.h
similarity index 100%
rename from lib/sat_asymm_branch.h
rename to src/sat/sat_asymm_branch.h
diff --git a/lib/sat_clause.cpp b/src/sat/sat_clause.cpp
similarity index 100%
rename from lib/sat_clause.cpp
rename to src/sat/sat_clause.cpp
diff --git a/lib/sat_clause.h b/src/sat/sat_clause.h
similarity index 100%
rename from lib/sat_clause.h
rename to src/sat/sat_clause.h
diff --git a/lib/sat_clause_set.cpp b/src/sat/sat_clause_set.cpp
similarity index 100%
rename from lib/sat_clause_set.cpp
rename to src/sat/sat_clause_set.cpp
diff --git a/lib/sat_clause_set.h b/src/sat/sat_clause_set.h
similarity index 100%
rename from lib/sat_clause_set.h
rename to src/sat/sat_clause_set.h
diff --git a/lib/sat_clause_use_list.cpp b/src/sat/sat_clause_use_list.cpp
similarity index 100%
rename from lib/sat_clause_use_list.cpp
rename to src/sat/sat_clause_use_list.cpp
diff --git a/lib/sat_clause_use_list.h b/src/sat/sat_clause_use_list.h
similarity index 100%
rename from lib/sat_clause_use_list.h
rename to src/sat/sat_clause_use_list.h
diff --git a/lib/sat_cleaner.cpp b/src/sat/sat_cleaner.cpp
similarity index 100%
rename from lib/sat_cleaner.cpp
rename to src/sat/sat_cleaner.cpp
diff --git a/lib/sat_cleaner.h b/src/sat/sat_cleaner.h
similarity index 100%
rename from lib/sat_cleaner.h
rename to src/sat/sat_cleaner.h
diff --git a/lib/sat_config.cpp b/src/sat/sat_config.cpp
similarity index 100%
rename from lib/sat_config.cpp
rename to src/sat/sat_config.cpp
diff --git a/lib/sat_config.h b/src/sat/sat_config.h
similarity index 100%
rename from lib/sat_config.h
rename to src/sat/sat_config.h
diff --git a/lib/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp
similarity index 100%
rename from lib/sat_elim_eqs.cpp
rename to src/sat/sat_elim_eqs.cpp
diff --git a/lib/sat_elim_eqs.h b/src/sat/sat_elim_eqs.h
similarity index 100%
rename from lib/sat_elim_eqs.h
rename to src/sat/sat_elim_eqs.h
diff --git a/lib/sat_extension.h b/src/sat/sat_extension.h
similarity index 100%
rename from lib/sat_extension.h
rename to src/sat/sat_extension.h
diff --git a/lib/sat_iff3_finder.cpp b/src/sat/sat_iff3_finder.cpp
similarity index 100%
rename from lib/sat_iff3_finder.cpp
rename to src/sat/sat_iff3_finder.cpp
diff --git a/lib/sat_iff3_finder.h b/src/sat/sat_iff3_finder.h
similarity index 100%
rename from lib/sat_iff3_finder.h
rename to src/sat/sat_iff3_finder.h
diff --git a/lib/sat_integrity_checker.cpp b/src/sat/sat_integrity_checker.cpp
similarity index 100%
rename from lib/sat_integrity_checker.cpp
rename to src/sat/sat_integrity_checker.cpp
diff --git a/lib/sat_integrity_checker.h b/src/sat/sat_integrity_checker.h
similarity index 100%
rename from lib/sat_integrity_checker.h
rename to src/sat/sat_integrity_checker.h
diff --git a/lib/sat_justification.h b/src/sat/sat_justification.h
similarity index 100%
rename from lib/sat_justification.h
rename to src/sat/sat_justification.h
diff --git a/lib/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp
similarity index 100%
rename from lib/sat_model_converter.cpp
rename to src/sat/sat_model_converter.cpp
diff --git a/lib/sat_model_converter.h b/src/sat/sat_model_converter.h
similarity index 100%
rename from lib/sat_model_converter.h
rename to src/sat/sat_model_converter.h
diff --git a/lib/sat_probing.cpp b/src/sat/sat_probing.cpp
similarity index 100%
rename from lib/sat_probing.cpp
rename to src/sat/sat_probing.cpp
diff --git a/lib/sat_probing.h b/src/sat/sat_probing.h
similarity index 100%
rename from lib/sat_probing.h
rename to src/sat/sat_probing.h
diff --git a/lib/sat_scc.cpp b/src/sat/sat_scc.cpp
similarity index 100%
rename from lib/sat_scc.cpp
rename to src/sat/sat_scc.cpp
diff --git a/lib/sat_scc.h b/src/sat/sat_scc.h
similarity index 100%
rename from lib/sat_scc.h
rename to src/sat/sat_scc.h
diff --git a/lib/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
similarity index 100%
rename from lib/sat_simplifier.cpp
rename to src/sat/sat_simplifier.cpp
diff --git a/lib/sat_simplifier.h b/src/sat/sat_simplifier.h
similarity index 100%
rename from lib/sat_simplifier.h
rename to src/sat/sat_simplifier.h
diff --git a/lib/sat_solver.cpp b/src/sat/sat_solver.cpp
similarity index 99%
rename from lib/sat_solver.cpp
rename to src/sat/sat_solver.cpp
index 3ca32a499..0322e80c5 100644
--- a/lib/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -17,7 +17,6 @@ Revision History:
 
 --*/
 #include"sat_solver.h"
-#include"strategy_exception.h"
 #include"sat_integrity_checker.h"
 #include"luby.h"
 #include"trace.h"
diff --git a/lib/sat_solver.h b/src/sat/sat_solver.h
similarity index 100%
rename from lib/sat_solver.h
rename to src/sat/sat_solver.h
diff --git a/lib/sat_types.h b/src/sat/sat_types.h
similarity index 100%
rename from lib/sat_types.h
rename to src/sat/sat_types.h
diff --git a/lib/sat_var_queue.h b/src/sat/sat_var_queue.h
similarity index 100%
rename from lib/sat_var_queue.h
rename to src/sat/sat_var_queue.h
diff --git a/lib/sat_watched.cpp b/src/sat/sat_watched.cpp
similarity index 100%
rename from lib/sat_watched.cpp
rename to src/sat/sat_watched.cpp
diff --git a/lib/sat_watched.h b/src/sat/sat_watched.h
similarity index 100%
rename from lib/sat_watched.h
rename to src/sat/sat_watched.h
diff --git a/lib/tactic_exception.cpp b/src/util/tactic_exception.cpp
similarity index 100%
rename from lib/tactic_exception.cpp
rename to src/util/tactic_exception.cpp
diff --git a/lib/tactic_exception.h b/src/util/tactic_exception.h
similarity index 100%
rename from lib/tactic_exception.h
rename to src/util/tactic_exception.h