diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index 59f9ecda6..6ed647a27 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -1401,6 +1401,7 @@ std::ostream& operator<<(std::ostream& out, sort_ref_vector const&  e) {
 
 
 #ifdef Z3DEBUG
+#include <iostream>
 void pp(expr const * n, ast_manager & m) {
     std::cout << mk_ismt2_pp(const_cast<expr*>(n), m) << std::endl;
 }
diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp
index 9c843d729..ad289cf5e 100644
--- a/src/ast/static_features.cpp
+++ b/src/ast/static_features.cpp
@@ -445,8 +445,6 @@ void static_features::post_process(expr * e, bool form_ctx, bool or_and_ctx, boo
     }
 
     unsigned depth = 0;
-    unsigned form_depth = 0;
-    unsigned or_and_depth = 0;
     unsigned ite_depth = 0;
 
     auto [form_ctx_new, or_and_ctx_new, ite_ctx_new] = new_ctx(e);
@@ -533,8 +531,6 @@ void static_features::process_root(expr * e) {
         if (num_args == 2)
             m_num_bin_clauses++;
         unsigned depth = 0;
-        unsigned form_depth = 0;
-        unsigned or_and_depth = 0;
         for (unsigned i = 0; i < num_args; i++) {
             expr * arg = to_app(e)->get_arg(i);
             if (m.is_not(arg))
diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 3f3a9cc89..68a646f92 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -1883,6 +1883,7 @@ namespace nlsat {
 };
 
 #ifdef Z3DEBUG
+#include <iostream>
 void pp(nlsat::explain::imp & ex, unsigned num, nlsat::literal const * ls) {
     ex.display(std::cout, num, ls);
 }
diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp
index 28cfa5c3e..37924496a 100644
--- a/src/qe/nlqsat.cpp
+++ b/src/qe/nlqsat.cpp
@@ -387,8 +387,7 @@ namespace qe {
             for (unsigned i = vars.size(); i-- > 0;) {
                 new_result.reset();
                 ex.project(vars[i], result.size(), result.data(), new_result);
-                TRACE("qe", display_project(tout, vars[i], result, new_result););                
-                TRACE("qe", display_project(std::cout, vars[i], result, new_result););
+                TRACE("qe", display_project(tout, vars[i], result, new_result););
                 result.swap(new_result);
             }
             negate_clause(result);
diff --git a/src/solver/assertions/asserted_formulas.cpp b/src/solver/assertions/asserted_formulas.cpp
index d283a4b13..c6a8093ff 100644
--- a/src/solver/assertions/asserted_formulas.cpp
+++ b/src/solver/assertions/asserted_formulas.cpp
@@ -726,6 +726,7 @@ unsigned asserted_formulas::get_total_size() const {
 
 
 #ifdef Z3DEBUG
+#include <iostream>
 void pp(asserted_formulas & f) {
     f.display(std::cout);
 }
diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp
index 32f9df9af..18b97d116 100644
--- a/src/tactic/fd_solver/smtfd_solver.cpp
+++ b/src/tactic/fd_solver/smtfd_solver.cpp
@@ -1756,14 +1756,14 @@ namespace smtfd {
                     expr_ref val0 = (*m_model)(a);
                     expr_ref val1 = (*m_model)(abs(a));
                     if (is_ground(a) && val0 != val1 && val0->get_sort() == val1->get_sort()) {
-                        std::cout << mk_bounded_pp(a, m, 2) << " := " << val0 << " " << val1 << "\n";
+                        //std::cout << mk_bounded_pp(a, m, 2) << " := " << val0 << " " << val1 << "\n";
                         found_bad = true;
                     }
                 }
                 if (found_bad) {
-                    std::cout << "core: " << core << "\n";
-                    std::cout << *m_model.get() << "\n";
-                    exit(0);
+                    //std::cout << "core: " << core << "\n";
+                    //std::cout << *m_model.get() << "\n";
+                    UNREACHABLE();
                 });
 
             if (!has_q) {
diff --git a/src/util/params.cpp b/src/util/params.cpp
index 1745e56fd..04c70b71e 100644
--- a/src/util/params.cpp
+++ b/src/util/params.cpp
@@ -1046,6 +1046,7 @@ void params::set_sym(char const * k, symbol const & v) {
 }
 
 #ifdef Z3DEBUG
+#include <iostream>
 void pp(params_ref const & p) {
     std::cout << p << std::endl;
 }
diff --git a/src/util/small_object_allocator.cpp b/src/util/small_object_allocator.cpp
index b74b094ef..bd980df34 100644
--- a/src/util/small_object_allocator.cpp
+++ b/src/util/small_object_allocator.cpp
@@ -24,6 +24,9 @@ Revision History:
 #include "util/util.h"
 #include "util/vector.h"
 #include<iomanip>
+#ifdef Z3DEBUG
+# include <iostream>
+#endif
 
 small_object_allocator::small_object_allocator(char const * id) {
     for (unsigned i = 0; i < NUM_SLOTS; i++) {