diff --git a/mk_make.py b/mk_make.py
index 92b0cf4a0..0bf3ecb80 100644
--- a/mk_make.py
+++ b/mk_make.py
@@ -158,5 +158,6 @@ def add_lib(name, deps):
 
 add_lib('util', [])
 add_lib('polynomial', ['util'])
-add_lib('sat', ['util'])
+add_lib('sat', ['util', 'sat_core'])
+add_lib('nlsat', ['util', 'sat_core', 'polynomial'])
 add_lib('ast', ['util', 'polynomial'])
diff --git a/lib/for_each_ast.cpp b/src/ast/for_each_ast.cpp
similarity index 100%
rename from lib/for_each_ast.cpp
rename to src/ast/for_each_ast.cpp
diff --git a/lib/for_each_expr.cpp b/src/ast/for_each_expr.cpp
similarity index 100%
rename from lib/for_each_expr.cpp
rename to src/ast/for_each_expr.cpp
diff --git a/lib/for_each_expr.h b/src/ast/for_each_expr.h
similarity index 100%
rename from lib/for_each_expr.h
rename to src/ast/for_each_expr.h
diff --git a/lib/well_sorted.cpp b/src/ast/well_sorted.cpp
similarity index 100%
rename from lib/well_sorted.cpp
rename to src/ast/well_sorted.cpp
diff --git a/lib/well_sorted.h b/src/ast/well_sorted.h
similarity index 100%
rename from lib/well_sorted.h
rename to src/ast/well_sorted.h
diff --git a/lib/nlsat_assignment.h b/src/nlsat/nlsat_assignment.h
similarity index 100%
rename from lib/nlsat_assignment.h
rename to src/nlsat/nlsat_assignment.h
diff --git a/lib/nlsat_clause.cpp b/src/nlsat/nlsat_clause.cpp
similarity index 100%
rename from lib/nlsat_clause.cpp
rename to src/nlsat/nlsat_clause.cpp
diff --git a/lib/nlsat_clause.h b/src/nlsat/nlsat_clause.h
similarity index 100%
rename from lib/nlsat_clause.h
rename to src/nlsat/nlsat_clause.h
diff --git a/lib/nlsat_evaluator.cpp b/src/nlsat/nlsat_evaluator.cpp
similarity index 100%
rename from lib/nlsat_evaluator.cpp
rename to src/nlsat/nlsat_evaluator.cpp
diff --git a/lib/nlsat_evaluator.h b/src/nlsat/nlsat_evaluator.h
similarity index 100%
rename from lib/nlsat_evaluator.h
rename to src/nlsat/nlsat_evaluator.h
diff --git a/lib/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
similarity index 100%
rename from lib/nlsat_explain.cpp
rename to src/nlsat/nlsat_explain.cpp
diff --git a/lib/nlsat_explain.h b/src/nlsat/nlsat_explain.h
similarity index 100%
rename from lib/nlsat_explain.h
rename to src/nlsat/nlsat_explain.h
diff --git a/lib/nlsat_interval_set.cpp b/src/nlsat/nlsat_interval_set.cpp
similarity index 100%
rename from lib/nlsat_interval_set.cpp
rename to src/nlsat/nlsat_interval_set.cpp
diff --git a/lib/nlsat_interval_set.h b/src/nlsat/nlsat_interval_set.h
similarity index 100%
rename from lib/nlsat_interval_set.h
rename to src/nlsat/nlsat_interval_set.h
diff --git a/lib/nlsat_justification.h b/src/nlsat/nlsat_justification.h
similarity index 100%
rename from lib/nlsat_justification.h
rename to src/nlsat/nlsat_justification.h
diff --git a/lib/nlsat_scoped_literal_vector.h b/src/nlsat/nlsat_scoped_literal_vector.h
similarity index 100%
rename from lib/nlsat_scoped_literal_vector.h
rename to src/nlsat/nlsat_scoped_literal_vector.h
diff --git a/lib/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
similarity index 99%
rename from lib/nlsat_solver.cpp
rename to src/nlsat/nlsat_solver.cpp
index 79ae334e3..b55a0a000 100644
--- a/lib/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -25,7 +25,7 @@ Revision History:
 #include"nlsat_evaluator.h"
 #include"nlsat_explain.h"
 #include"algebraic_numbers.h"
-#include"tactic.h"
+#include"tactic_exception.h"
 #include"chashtable.h"
 #include"id_gen.h"
 #include"dependency.h"
diff --git a/lib/nlsat_solver.h b/src/nlsat/nlsat_solver.h
similarity index 100%
rename from lib/nlsat_solver.h
rename to src/nlsat/nlsat_solver.h
diff --git a/lib/nlsat_types.cpp b/src/nlsat/nlsat_types.cpp
similarity index 100%
rename from lib/nlsat_types.cpp
rename to src/nlsat/nlsat_types.cpp
diff --git a/lib/nlsat_types.h b/src/nlsat/nlsat_types.h
similarity index 100%
rename from lib/nlsat_types.h
rename to src/nlsat/nlsat_types.h
diff --git a/src/sat/sat_types.h b/src/sat_core/sat_types.h
similarity index 100%
rename from src/sat/sat_types.h
rename to src/sat_core/sat_types.h