diff --git a/src/math/polysat/CMakeLists.txt b/src/math/polysat/CMakeLists.txt
index cf0e36479..2986cb94e 100644
--- a/src/math/polysat/CMakeLists.txt
+++ b/src/math/polysat/CMakeLists.txt
@@ -32,7 +32,6 @@ z3_add_component(polysat
     viable.cpp
     viable_fallback.cpp
   COMPONENT_DEPENDENCIES
-    bigfix
     dd
     euf
     interval
diff --git a/src/math/polysat/clause.h b/src/math/polysat/clause.h
index c1c3170bb..b951be24d 100644
--- a/src/math/polysat/clause.h
+++ b/src/math/polysat/clause.h
@@ -24,7 +24,7 @@ namespace polysat {
     // NB code review:
     // right, ref-count is unlikely the right mechanism.
     // In the SAT solver all clauses are managed in one arena (auxiliarary and redundant)
-    // and deleted when they exist the arena.
+    // and deleted when they exit the arena.
     //
     class clause {
     public: