diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index dff6fc644..530798cfb 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -51,7 +51,8 @@ def init_project_def():
     add_lib('mbp', ['model', 'simplex'], 'qe/mbp')
     add_lib('qe_lite', ['tactic', 'mbp'], 'qe/lite')
     add_lib('bigfix',['util'], 'math/bigfix')
-    add_lib('polysat', ['bigfix','util','dd','simplex','interval'],'math/polysat')
+    add_lib('polysat_univariate_solver', ['util', 'solver'], 'math/polysat/univariate')
+    add_lib('polysat', ['bigfix','util','dd','simplex','interval','polysat_univariate_solver'], 'math/polysat')
     add_lib('solver_assertions', ['pattern','smt_params','cmd_context','qe_lite'], 'solver/assertions')
     add_lib('sat_smt', ['sat', 'euf', 'tactic', 'solver', 'smt_params', 'bit_blaster', 'fpa', 'mbp', 'normal_forms', 'lp', 'pattern', 'qe_lite', 'polysat'], 'sat/smt')
     add_lib('sat_tactic', ['tactic', 'sat', 'solver', 'sat_smt'], 'sat/tactic')
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 97f4f945e..e6a9a9879 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -41,8 +41,6 @@ add_subdirectory(math/hilbert)
 add_subdirectory(math/simplex)
 add_subdirectory(math/interval)
 add_subdirectory(math/bigfix)
-add_subdirectory(math/polysat)
-add_subdirectory(math/polysat/univariate)
 add_subdirectory(math/automata)
 add_subdirectory(math/realclosure)
 add_subdirectory(math/subpaving)
@@ -65,6 +63,8 @@ add_subdirectory(math/subpaving/tactic)
 add_subdirectory(tactic/aig)
 add_subdirectory(tactic/arith)
 add_subdirectory(solver)
+add_subdirectory(math/polysat/univariate)
+add_subdirectory(math/polysat)
 add_subdirectory(cmd_context)
 add_subdirectory(cmd_context/extra_cmds)
 add_subdirectory(parsers/smt2)
diff --git a/src/math/polysat/CMakeLists.txt b/src/math/polysat/CMakeLists.txt
index 0f184c7aa..341e3eaa7 100644
--- a/src/math/polysat/CMakeLists.txt
+++ b/src/math/polysat/CMakeLists.txt
@@ -30,6 +30,7 @@ z3_add_component(polysat
     simplex
     interval
     bigfix
+    polysat_univariate_solver
   PYG_FILES
     polysat_params.pyg
 )
diff --git a/src/math/polysat/univariate/CMakeLists.txt b/src/math/polysat/univariate/CMakeLists.txt
index 29f25f2c6..80de20416 100644
--- a/src/math/polysat/univariate/CMakeLists.txt
+++ b/src/math/polysat/univariate/CMakeLists.txt
@@ -1,4 +1,7 @@
 z3_add_component(polysat_univariate_solver
   SOURCES
     univariate_solver.cpp
+  COMPONENT_DEPENDENCIES
+    util
+    solver
 )
diff --git a/src/math/polysat/univariate/univariate_solver.cpp b/src/math/polysat/univariate/univariate_solver.cpp
index f17d4a735..f9091fa1e 100644
--- a/src/math/polysat/univariate/univariate_solver.cpp
+++ b/src/math/polysat/univariate/univariate_solver.cpp
@@ -17,8 +17,6 @@ Author:
 --*/
 
 #include "math/polysat/univariate/univariate_solver.h"
-#include "math/polysat/log.h"
-#include "sat/sat_solver/inc_sat_solver.h"
 #include "solver/solver.h"
 #include "util/util.h"
 #include "ast/ast.h"
@@ -55,9 +53,7 @@ namespace polysat {
         ~univariate_bitblast_solver() override = default;
 
         void push() override {
-            // LOG("univariate push...");
             s->push();
-            // LOG("univariate push done");
         }
 
         void pop(unsigned n) override {