diff --git a/scripts/update_api.py b/scripts/update_api.py
index 24cf3745b..6c932d8ca 100755
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -1771,7 +1771,6 @@ def write_log_h_preamble(log_h):
 
 def write_log_c_preamble(log_c):
   log_c.write('// Automatically generated file\n')
-  log_c.write('#include<iostream>\n')
   log_c.write('#include\"api/z3.h\"\n')
   log_c.write('#include\"api/api_log_macros.h\"\n')
   log_c.write('#include\"api/z3_logger.h\"\n')
diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index 7cd3b2dd9..647cc8631 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -15,7 +15,6 @@ Author:
 Revision History:
 
 --*/
-#include<iostream>
 #include "api/api_log_macros.h"
 #include "api/api_context.h"
 #include "api/api_util.h"
diff --git a/src/api/api_ast_map.cpp b/src/api/api_ast_map.cpp
index e252b9aca..5976d0e41 100644
--- a/src/api/api_ast_map.cpp
+++ b/src/api/api_ast_map.cpp
@@ -15,7 +15,6 @@ Author:
 Revision History:
 
 --*/
-#include<iostream>
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "api/api_context.h"
diff --git a/src/api/api_ast_vector.cpp b/src/api/api_ast_vector.cpp
index a8a64ce2c..028b971d3 100644
--- a/src/api/api_ast_vector.cpp
+++ b/src/api/api_ast_vector.cpp
@@ -15,7 +15,6 @@ Author:
 Revision History:
 
 --*/
-#include<iostream>
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "api/api_context.h"
diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp
index 37c86e317..2dda84af4 100644
--- a/src/api/api_fpa.cpp
+++ b/src/api/api_fpa.cpp
@@ -16,7 +16,6 @@ Author:
 Notes:
 
 --*/
-#include<iostream>
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "api/api_context.h"
diff --git a/src/api/api_goal.cpp b/src/api/api_goal.cpp
index dd9f8959f..086e8f302 100644
--- a/src/api/api_goal.cpp
+++ b/src/api/api_goal.cpp
@@ -15,7 +15,6 @@ Author:
 Revision History:
 
 --*/
-#include<iostream>
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "api/api_context.h"
diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp
index 7e655c9d1..60d663638 100644
--- a/src/api/api_numeral.cpp
+++ b/src/api/api_numeral.cpp
@@ -16,7 +16,6 @@ Revision History:
 
 --*/
 #include<cmath>
-#include<iostream>
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "api/api_context.h"
diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp
index 140c655cd..ebbe1a3db 100644
--- a/src/api/api_opt.cpp
+++ b/src/api/api_opt.cpp
@@ -15,7 +15,6 @@ Author:
 Revision History:
 
 --*/
-#include<iostream>
 #include "util/cancel_eh.h"
 #include "util/scoped_timer.h"
 #include "util/scoped_ctrl_c.h"
diff --git a/src/api/api_params.cpp b/src/api/api_params.cpp
index 6e06fbf78..1454525d6 100644
--- a/src/api/api_params.cpp
+++ b/src/api/api_params.cpp
@@ -17,7 +17,6 @@ Author:
 Revision History:
 
 --*/
-#include<iostream>
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "api/api_context.h"
diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp
index 94132a361..1c5afb34f 100644
--- a/src/api/api_parsers.cpp
+++ b/src/api/api_parsers.cpp
@@ -15,7 +15,6 @@ Author:
 Revision History:
 
 --*/
-#include<iostream>
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "api/api_context.h"
diff --git a/src/api/api_qe.cpp b/src/api/api_qe.cpp
index d1e5d195b..328b1f249 100644
--- a/src/api/api_qe.cpp
+++ b/src/api/api_qe.cpp
@@ -17,7 +17,6 @@ Notes:
 
 --*/
 
-#include <iostream>
 #include "ast/expr_map.h"
 #include "api/z3.h"
 #include "api/api_log_macros.h"
diff --git a/src/api/api_rcf.cpp b/src/api/api_rcf.cpp
index 7c168dc62..8a000be1a 100644
--- a/src/api/api_rcf.cpp
+++ b/src/api/api_rcf.cpp
@@ -19,7 +19,6 @@ Author:
 Notes:
     
 --*/
-#include<iostream>
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "api/api_context.h"
diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index b8765a69b..3a28da0fd 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -16,7 +16,6 @@ Author:
 Revision History:
 
 --*/
-#include<iostream>
 #include<thread>
 #include "util/scoped_ctrl_c.h"
 #include "util/cancel_eh.h"
diff --git a/src/api/api_special_relations.cpp b/src/api/api_special_relations.cpp
index 3b4872435..f29254cba 100644
--- a/src/api/api_special_relations.cpp
+++ b/src/api/api_special_relations.cpp
@@ -17,7 +17,6 @@ Revision History:
 
 --*/
 
-#include <iostream>
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "api/api_context.h"
diff --git a/src/api/api_stats.cpp b/src/api/api_stats.cpp
index 01b521ed6..c90850404 100644
--- a/src/api/api_stats.cpp
+++ b/src/api/api_stats.cpp
@@ -15,7 +15,6 @@ Author:
 Revision History:
 
 --*/
-#include<iostream>
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "api/api_context.h"
diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp
index edf9ab262..b3e3ca922 100644
--- a/src/api/api_tactic.cpp
+++ b/src/api/api_tactic.cpp
@@ -15,7 +15,6 @@ Author:
 Revision History:
 
 --*/
-#include<iostream>
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "api/api_context.h"
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index de55bb765..10116d751 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -21,7 +21,7 @@ Notes:
 #pragma once
 
 #include<cassert>
-#include<iostream>
+#include<ostream>
 #include<string>
 #include<sstream>
 #include<memory>
diff --git a/src/api/z3_private.h b/src/api/z3_private.h
index 528033c72..9a32eb06f 100644
--- a/src/api/z3_private.h
+++ b/src/api/z3_private.h
@@ -18,7 +18,6 @@ Notes:
 
 --*/
 
-#include<iostream>
 #include "util/rational.h"
 #include "api/z3_macros.h"
 
diff --git a/src/api/z3_replayer.cpp b/src/api/z3_replayer.cpp
index 398290b9e..ad5bc9523 100644
--- a/src/api/z3_replayer.cpp
+++ b/src/api/z3_replayer.cpp
@@ -22,6 +22,7 @@ Notes:
 #include "util/stream_buffer.h"
 #include "util/symbol.h"
 #include "util/trace.h"
+#include<iostream>
 #include<sstream>
 #include<vector>
 
diff --git a/src/api/z3_replayer.h b/src/api/z3_replayer.h
index b5388251f..8c77f0e0a 100644
--- a/src/api/z3_replayer.h
+++ b/src/api/z3_replayer.h
@@ -18,7 +18,6 @@ Notes:
 --*/
 #pragma once
 
-#include<iostream>
 #include "api/z3.h"
 #include "util/z3_exception.h"
 
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 190da1366..5c48f31d0 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -30,6 +30,7 @@ Revision History:
 #include "ast/arith_decl_plugin.h"
 #include "ast/ast_translation.h"
 #include "util/z3_version.h"
+#include <iostream>
 
 
 // -----------------------------------
diff --git a/src/ast/ast_ll_pp.cpp b/src/ast/ast_ll_pp.cpp
index 4c48bc7e7..5de98c644 100644
--- a/src/ast/ast_ll_pp.cpp
+++ b/src/ast/ast_ll_pp.cpp
@@ -17,7 +17,7 @@ Revision History:
 
 --*/
 
-#include<iostream>
+#include "ast/ast_ll_pp.h"
 #include "ast/for_each_ast.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/datatype_decl_plugin.h"
diff --git a/src/ast/ast_ll_pp.h b/src/ast/ast_ll_pp.h
index 17de34687..da0c1529b 100644
--- a/src/ast/ast_ll_pp.h
+++ b/src/ast/ast_ll_pp.h
@@ -19,7 +19,7 @@ Revision History:
 #pragma once
 
 #include "ast/ast.h"
-#include<iostream>
+#include<ostream>
 
 void ast_ll_pp(std::ostream & out, ast_manager & m, ast * n, bool only_exprs=true, bool compact=true);
 void ast_ll_pp(std::ostream & out, ast_manager & m, ast * n, ast_mark & visited, bool only_exprs=true, bool compact=true);
diff --git a/src/ast/ast_pp_dot.h b/src/ast/ast_pp_dot.h
index 7b4420a33..6860eaef5 100644
--- a/src/ast/ast_pp_dot.h
+++ b/src/ast/ast_pp_dot.h
@@ -6,7 +6,7 @@ Abstract: Pretty-printer for proofs in Graphviz format
 
 #pragma once
 
-#include <iostream>
+#include <ostream>
 #include "ast/ast_pp.h"
 
 class ast_pp_dot {
diff --git a/src/ast/ast_printer.cpp b/src/ast/ast_printer.cpp
index 7f2460e06..7f717df96 100644
--- a/src/ast/ast_printer.cpp
+++ b/src/ast/ast_printer.cpp
@@ -18,6 +18,7 @@ Revision History:
 --*/
 #include "ast/ast_printer.h"
 #include "ast/pp.h"
+#include <iostream>
 
 class simple_ast_printer_context : public ast_printer_context {
     ast_manager & m_manager;
@@ -51,3 +52,6 @@ public:
 ast_printer_context * mk_simple_ast_printer_context(ast_manager & m) {
     return alloc(simple_ast_printer_context, m);
 }
+
+std::ostream & ast_printer_context::regular_stream() { return std::cout; }
+std::ostream & ast_printer_context::diagnostic_stream() { return std::cerr; }
diff --git a/src/ast/ast_printer.h b/src/ast/ast_printer.h
index 1cfb9b800..d57a9b845 100644
--- a/src/ast/ast_printer.h
+++ b/src/ast/ast_printer.h
@@ -20,6 +20,7 @@ Revision History:
 
 #include "ast/ast.h"
 #include "ast/ast_smt2_pp.h"
+#include <ostream>
 
 class ast_printer {
 public:
@@ -46,8 +47,8 @@ class ast_printer_context : public ast_printer {
 public:
     ~ast_printer_context() override {}
     virtual ast_manager & get_ast_manager() = 0;
-    virtual std::ostream & regular_stream() { return std::cout; }
-    virtual std::ostream & diagnostic_stream() { return std::cerr; }
+    virtual std::ostream & regular_stream();
+    virtual std::ostream & diagnostic_stream();
 };
 
 
diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp
index dabf11d69..f40b8a554 100644
--- a/src/ast/ast_smt_pp.cpp
+++ b/src/ast/ast_smt_pp.cpp
@@ -20,7 +20,7 @@ Revision History:
 --*/
 
 #include<sstream>
-#include<iostream>
+#include<ostream>
 #include "util/vector.h"
 #include "util/smt2_util.h"
 #include "ast/ast_smt_pp.h"
diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp
index 3611f848a..c541f72d0 100644
--- a/src/ast/fpa/bv2fpa_converter.cpp
+++ b/src/ast/fpa/bv2fpa_converter.cpp
@@ -162,7 +162,7 @@ expr_ref bv2fpa_converter::convert_bv2rm(expr * bv_rm) {
         }
     }
     else {
-        std::cout << expr_ref(bv_rm, m) << " not converted\n";
+        //std::cout << expr_ref(bv_rm, m) << " not converted\n";
     }
 
     return res;
diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index 64155d48b..862fe6929 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -124,7 +124,7 @@ void fpa2bv_converter::mk_ite(expr * c, expr * t, expr * f, expr_ref & result) {
         result = m_util.mk_bv2rm(result);
     }
     else {
-        std::cout << mk_pp(t, m) << " " << mk_pp(f, m) << "\n";
+        //std::cout << mk_pp(t, m) << " " << mk_pp(f, m) << "\n";
         UNREACHABLE();
 
     }
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 9bd6e6556..2174c9e0b 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -51,6 +51,7 @@ Notes:
 #include "solver/smt_logics.h"
 #include "cmd_context/basic_cmds.h"
 #include "cmd_context/cmd_context.h"
+#include <iostream>
 
 func_decls::func_decls(ast_manager & m, func_decl * f):
     m_decls(TAG(func_decl*, f, 0)) {
diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h
index 2be55dcb1..aa06cb263 100644
--- a/src/math/lp/lp_settings.h
+++ b/src/math/lp/lp_settings.h
@@ -24,6 +24,7 @@ Revision History:
 #include <algorithm>
 #include <limits>
 #include <iomanip>
+#include <iostream>
 #include <cstring>
 #include "util/stopwatch.h"
 #include "util/statistics.h"
diff --git a/src/math/lp/lu.h b/src/math/lp/lu.h
index f5289211f..aca59065d 100644
--- a/src/math/lp/lu.h
+++ b/src/math/lp/lu.h
@@ -33,7 +33,7 @@ Revision History:
 #include "math/lp/static_matrix.h"
 #include <string>
 #include "math/lp/numeric_pair.h"
-#include <iostream>
+#include <ostream>
 #include <fstream>
 #include "math/lp/row_eta_matrix.h"
 #include "math/lp/square_dense_submatrix.h"
diff --git a/src/math/lp/mps_reader.h b/src/math/lp/mps_reader.h
index f165b08b3..f0fa074cc 100644
--- a/src/math/lp/mps_reader.h
+++ b/src/math/lp/mps_reader.h
@@ -26,7 +26,7 @@ Revision History:
 #include <string>
 #include "util/vector.h"
 #include <unordered_map>
-#include <iostream>
+#include <ostream>
 #include <fstream>
 #include <locale>
 #include "math/lp/lp_primal_simplex.h"
diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp
index 471c419ac..1ff2785ae 100644
--- a/src/math/realclosure/realclosure.cpp
+++ b/src/math/realclosure/realclosure.cpp
@@ -29,6 +29,7 @@ Notes:
 #include "util/ref_vector.h"
 #include "util/ref_buffer.h"
 #include "util/common_msgs.h"
+#include <iostream>
 
 #ifndef REALCLOSURE_INI_BUFFER_SIZE
 #define REALCLOSURE_INI_BUFFER_SIZE 32
diff --git a/src/math/simplex/sparse_matrix.h b/src/math/simplex/sparse_matrix.h
index e26531c82..a33ea55bd 100644
--- a/src/math/simplex/sparse_matrix.h
+++ b/src/math/simplex/sparse_matrix.h
@@ -281,7 +281,7 @@ namespace simplex {
             vector<_row> const& m_rows;
             void move_to_next() {
                 while (m_curr < m_rows.size() && m_rows[m_curr].size() == 0) {
-                    std::cout << "size is 0 for " << m_curr << "\n";
+                    //std::cout << "size is 0 for " << m_curr << "\n";
                     ++m_curr;
                 }
             }
diff --git a/src/math/subpaving/subpaving_t.h b/src/math/subpaving/subpaving_t.h
index 79abf0cc7..cfe3aea70 100644
--- a/src/math/subpaving/subpaving_t.h
+++ b/src/math/subpaving/subpaving_t.h
@@ -18,7 +18,7 @@ Revision History:
 --*/
 #pragma once
 
-#include<iostream>
+#include<ostream>
 #include "util/tptr.h"
 #include "util/small_object_allocator.h"
 #include "util/chashtable.h"
diff --git a/src/math/subpaving/tactic/subpaving_tactic.cpp b/src/math/subpaving/tactic/subpaving_tactic.cpp
index 6124e726e..cdd8bac0a 100644
--- a/src/math/subpaving/tactic/subpaving_tactic.cpp
+++ b/src/math/subpaving/tactic/subpaving_tactic.cpp
@@ -26,6 +26,7 @@ Revision History:
 #include "util/mpff.h"
 #include "util/mpfx.h"
 #include "util/f2n.h"
+#include <iostream>
 
 class subpaving_tactic : public tactic {
 
diff --git a/src/model/model_pp.h b/src/model/model_pp.h
index e71cab05c..b6450e677 100644
--- a/src/model/model_pp.h
+++ b/src/model/model_pp.h
@@ -19,7 +19,7 @@ Revision History:
 --*/
 #pragma once
 
-#include<iostream>
+#include<ostream>
 class model_core;
 
 void model_pp(std::ostream & out, model_core const & m);
diff --git a/src/model/model_v2_pp.cpp b/src/model/model_v2_pp.cpp
index e50d70079..5ade6ba63 100644
--- a/src/model/model_v2_pp.cpp
+++ b/src/model/model_v2_pp.cpp
@@ -18,6 +18,7 @@ Revision History:
 #include "model/model_v2_pp.h"
 #include "model/model_core.h"
 #include "ast/ast_pp.h"
+#include <iostream>
 
 static void display_function(std::ostream & out, model_core const & md, func_decl * f, bool partial) {
     ast_manager & m = md.get_manager();
diff --git a/src/model/model_v2_pp.h b/src/model/model_v2_pp.h
index c61175544..16edbd732 100644
--- a/src/model/model_v2_pp.h
+++ b/src/model/model_v2_pp.h
@@ -17,7 +17,7 @@ Revision History:
 --*/
 #pragma once
 
-#include<iostream>
+#include<ostream>
 class model_core;
 
 void model_v2_pp(std::ostream & out, model_core const & m, bool partial = false);
diff --git a/src/muz/base/dl_boogie_proof.cpp b/src/muz/base/dl_boogie_proof.cpp
index 97e4689dc..889ec8a32 100644
--- a/src/muz/base/dl_boogie_proof.cpp
+++ b/src/muz/base/dl_boogie_proof.cpp
@@ -121,11 +121,11 @@ namespace datalog {
     }
     
     void boogie_proof::set_proof(proof* p) {
-        std::cout << "set proof\n";
+        //std::cout << "set proof\n";
         m_proof = p;
         proof_utils::push_instantiations_up(m_proof);
         mk_input_resolution(m_proof);
-        std::cout << "proof set\n";
+        //std::cout << "proof set\n";
     }
         
     void boogie_proof::set_model(model* m) {
@@ -201,7 +201,7 @@ namespace datalog {
         ptr_vector<proof> todo;
         todo.push_back(p);
         ast_mark visited;
-        std::cout << "get_subst\n" << mk_pp(p, m) << "\n";
+        //std::cout << "get_subst\n" << mk_pp(p, m) << "\n";
         while (!todo.empty()) {
             proof* p = todo.back();
             todo.pop_back();
diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index 6d95b705f..01523e8d2 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -17,6 +17,7 @@ Revision History:
 
 --*/
 
+#include<iostream>
 #include<sstream>
 #include<limits>
 #include "ast/arith_decl_plugin.h"
diff --git a/src/muz/base/dl_util.h b/src/muz/base/dl_util.h
index 565b58c84..46e0b42bf 100644
--- a/src/muz/base/dl_util.h
+++ b/src/muz/base/dl_util.h
@@ -257,12 +257,14 @@ namespace datalog {
             }
             container[i-ofs] = container[i];
         }
+#if 0
         if (r_i != removed_col_cnt) {
             for (unsigned i = 0; i < removed_col_cnt; ++i) {
                 std::cout << removed_cols[i] << " ";
             }
             std::cout << " container size: " << n << "\n";
         }
+#endif
         SASSERT(r_i==removed_col_cnt);
         container.resize(n-removed_col_cnt);
     }
diff --git a/src/muz/ddnf/ddnf.cpp b/src/muz/ddnf/ddnf.cpp
index ad1994865..c0c3d839c 100644
--- a/src/muz/ddnf/ddnf.cpp
+++ b/src/muz/ddnf/ddnf.cpp
@@ -26,6 +26,7 @@ Revision History:
 #include "ast/scoped_proof.h"
 #include "ast/bv_decl_plugin.h"
 #include "muz/rel/tbv.h"
+#include <iostream>
 
 namespace datalog {
 
@@ -224,9 +225,9 @@ namespace datalog {
         }
 
         void display_statistics(std::ostream& out) const {            
-            std::cout << "Number of insertions:  " << m_stats.m_num_inserts << "\n";
-            std::cout << "Number of comparisons: " << m_stats.m_num_comparisons << "\n";
-            std::cout << "Number of nodes:       " << size() << "\n";
+            out << "Number of insertions:  " << m_stats.m_num_inserts << "\n"
+                   "Number of comparisons: " << m_stats.m_num_comparisons << "\n"
+                   "Number of nodes:       " << size() << "\n";
         }
 
         void display(std::ostream& out) const {            
diff --git a/src/muz/rel/aig_exporter.cpp b/src/muz/rel/aig_exporter.cpp
index d22f1761b..c8ef1321f 100644
--- a/src/muz/rel/aig_exporter.cpp
+++ b/src/muz/rel/aig_exporter.cpp
@@ -108,13 +108,11 @@ namespace datalog {
                 rule *r = *II;
                 unsigned numqs = r->get_positive_tail_size();
                 if (numqs > 1) {
-                    std::cerr << "non-linear clauses not supported\n";
-                    exit(-1);
+                    throw default_exception("non-linear clauses not supported");
                 }
 
                 if (numqs != r->get_uninterpreted_tail_size()) {
-                    std::cerr << "negation of queries not supported\n";
-                    exit(-1);
+                    throw default_exception("negation of queries not supported");
                 }
 
                 exprs.reset();
diff --git a/src/muz/rel/dl_compiler.h b/src/muz/rel/dl_compiler.h
index 601b01eaa..106d1b791 100644
--- a/src/muz/rel/dl_compiler.h
+++ b/src/muz/rel/dl_compiler.h
@@ -18,8 +18,6 @@ Revision History:
 --*/
 #pragma once
 
-#include<iostream>
-#include<list>
 #include<utility>
 
 #include "ast/ast.h"
diff --git a/src/muz/rel/dl_instruction.h b/src/muz/rel/dl_instruction.h
index 8e56da545..1edacc94f 100644
--- a/src/muz/rel/dl_instruction.h
+++ b/src/muz/rel/dl_instruction.h
@@ -18,7 +18,7 @@ Revision History:
 --*/
 #pragma once
 
-#include<iostream>
+#include<ostream>
 #include<string>
 #include<utility>
 #include "ast/ast.h"
diff --git a/src/muz/rel/dl_sparse_table.h b/src/muz/rel/dl_sparse_table.h
index a14512730..73e877401 100644
--- a/src/muz/rel/dl_sparse_table.h
+++ b/src/muz/rel/dl_sparse_table.h
@@ -19,7 +19,6 @@ Revision History:
 
 #pragma once
 
-#include<iostream>
 #include<list>
 #include<utility>
 
diff --git a/src/muz/rel/dl_table.h b/src/muz/rel/dl_table.h
index 967c6e25b..96f68f44c 100644
--- a/src/muz/rel/dl_table.h
+++ b/src/muz/rel/dl_table.h
@@ -18,7 +18,6 @@ Revision History:
 --*/
 #pragma once
 
-#include<iostream>
 #include<list>
 #include<utility>
 
diff --git a/src/muz/spacer/spacer_json.h b/src/muz/spacer/spacer_json.h
index 1aa1dfae3..bb330cc03 100644
--- a/src/muz/spacer/spacer_json.h
+++ b/src/muz/spacer/spacer_json.h
@@ -19,7 +19,7 @@ Notes:
 
 #pragma once
 
-#include<iostream>
+#include<ostream>
 #include<map>
 #include "util/ref.h"
 #include "util/ref_vector.h"
diff --git a/src/muz/transforms/dl_mk_array_instantiation.cpp b/src/muz/transforms/dl_mk_array_instantiation.cpp
index 5e54afed1..32c622ca2 100644
--- a/src/muz/transforms/dl_mk_array_instantiation.cpp
+++ b/src/muz/transforms/dl_mk_array_instantiation.cpp
@@ -39,6 +39,7 @@ namespace datalog {
     }
 
     rule_set * mk_array_instantiation::operator()(rule_set const & source)  {
+#if 0
         std::cout<<"Array Instantiation called with parameters :"
                  <<" enforce="<<m_ctx.get_params().xform_instantiate_arrays_enforce()
                  <<" nb_quantifier="<<m_ctx.get_params().xform_instantiate_arrays_nb_quantifier()
@@ -46,6 +47,7 @@ namespace datalog {
                  <<"\n";
         std::cout<<"Input rules = \n";
         source.display(std::cout);
+#endif
         src_set = &source;
         scoped_ptr<rule_set> result = alloc(rule_set, m_ctx);
         dst = result.get();
@@ -55,8 +57,10 @@ namespace datalog {
             rule & r = *source.get_rule(i);
             instantiate_rule(r, *result);
         }
+#if 0
         std::cout<<"\n\nOutput rules = \n";
         result->display(std::cout);
+#endif
         return result.detach();
     }
 
diff --git a/src/opt/opt_parse.cpp b/src/opt/opt_parse.cpp
index f1aa40886..29e8a604c 100644
--- a/src/opt/opt_parse.cpp
+++ b/src/opt/opt_parse.cpp
@@ -18,7 +18,7 @@ Revision History:
 --*/
 #include "opt/opt_context.h"
 #include "opt/opt_parse.h"
-
+#include <iostream>
 
 class opt_stream_buffer {
     std::istream & m_stream;
diff --git a/src/parsers/smt2/marshal.h b/src/parsers/smt2/marshal.h
index 0e996b41f..82eb02786 100644
--- a/src/parsers/smt2/marshal.h
+++ b/src/parsers/smt2/marshal.h
@@ -12,7 +12,7 @@ Abstract:
 #pragma once
 
 #include <string>
-#include <iostream>
+#include <ostream>
 
 #include "ast/ast.h"
 
diff --git a/src/parsers/smt2/smt2scanner.h b/src/parsers/smt2/smt2scanner.h
index 07e4ed678..5fb59c7cd 100644
--- a/src/parsers/smt2/smt2scanner.h
+++ b/src/parsers/smt2/smt2scanner.h
@@ -18,7 +18,7 @@ Revision History:
 --*/
 #pragma once
 
-#include<iostream>
+#include<istream>
 #include "util/symbol.h"
 #include "util/vector.h"
 #include "util/rational.h"
diff --git a/src/parsers/util/cost_parser.h b/src/parsers/util/cost_parser.h
index e3e57e236..70db48171 100644
--- a/src/parsers/util/cost_parser.h
+++ b/src/parsers/util/cost_parser.h
@@ -26,7 +26,6 @@ class cost_parser : public simple_parser {
     var_ref_vector m_vars;
 public:
     cost_parser(ast_manager & m);
-    ~cost_parser() override {}
     expr * parse_int(rational const & r) override;
     expr * parse_float(rational const & r) override;
     unsigned add_var(symbol name);
diff --git a/src/parsers/util/scanner.cpp b/src/parsers/util/scanner.cpp
index 2a5923ee2..db8453ffe 100644
--- a/src/parsers/util/scanner.cpp
+++ b/src/parsers/util/scanner.cpp
@@ -17,6 +17,7 @@ Revision History:
 
 --*/
 #include "parsers/util/scanner.h"
+#include <iostream>
 
 inline int scanner::read_char() {
     if (m_is_interactive) {
diff --git a/src/parsers/util/simple_parser.cpp b/src/parsers/util/simple_parser.cpp
index 0157f1c11..6c3303e5c 100644
--- a/src/parsers/util/simple_parser.cpp
+++ b/src/parsers/util/simple_parser.cpp
@@ -17,6 +17,7 @@ Revision History:
 
 --*/
 #include<fstream>
+#include<iostream>
 #include<sstream>
 #include "parsers/util/simple_parser.h"
 #include "util/warning.h"
diff --git a/src/sat/sat_aig_cuts.cpp b/src/sat/sat_aig_cuts.cpp
index 3474029ea..20f62cbdd 100644
--- a/src/sat/sat_aig_cuts.cpp
+++ b/src/sat/sat_aig_cuts.cpp
@@ -818,11 +818,12 @@ namespace sat {
             lbool r = s.check();
             IF_VERBOSE(10, verbose_stream() << "check: " << r << "\n");
             if (r == l_true) {
-                std::sort(vars.begin(), vars.end());
-                s.display(std::cout);
-                for (auto v : vars) std::cout << v << " := " << s.get_model()[v] << "\n";
-                std::string line;
-                std::getline(std::cin, line);
+                IF_VERBOSE(0,
+                    std::sort(vars.begin(), vars.end());
+                    s.display(verbose_stream());
+                    for (auto v : vars) verbose_stream() << v << " := " << s.get_model()[v] << "\n";
+                );
+                UNREACHABLE();
             }
         }
     };
diff --git a/src/sat/sat_cut_simplifier.cpp b/src/sat/sat_cut_simplifier.cpp
index c10a35d11..d43219f25 100644
--- a/src/sat/sat_cut_simplifier.cpp
+++ b/src/sat/sat_cut_simplifier.cpp
@@ -75,8 +75,7 @@ namespace sat {
                 IF_VERBOSE(0, 
                            verbose_stream() << "not validated: " << clause << "\n";
                            s.display(verbose_stream()););
-                std::string line;
-                std::getline(std::cin, line);                
+                UNREACHABLE();
             }
         }
     };
diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp
index d5ea181c4..9cac2e5ef 100644
--- a/src/sat/sat_drat.cpp
+++ b/src/sat/sat_drat.cpp
@@ -467,9 +467,7 @@ namespace sat {
         literal_vector lits(n, c);
         IF_VERBOSE(0, verbose_stream() << "Verification of " << lits << " failed\n");
         // s.display(std::cout);
-        std::string line;
-        std::getline(std::cin, line);
-        exit(0);
+        UNREACHABLE();
 #if 0
         SASSERT(false);
         INVOKE_DEBUGGER();
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index b3521452b..ea936600c 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -1831,8 +1831,8 @@ namespace sat {
             if (not_l == l2)
                 continue;
             if ((~l2).index() >= m_visited.size()) {
-                s.display(std::cout << l2 << " " << s.num_vars() << " " << m_visited.size() << "\n");
-                exit(0);
+                //s.display(std::cout << l2 << " " << s.num_vars() << " " << m_visited.size() << "\n");
+                UNREACHABLE();
             }
             if (m_visited[(~l2).index()]) {
                 res = false;
diff --git a/src/sat/smt/array_diagnostics.cpp b/src/sat/smt/array_diagnostics.cpp
index c1230ea7f..11ed4384d 100644
--- a/src/sat/smt/array_diagnostics.cpp
+++ b/src/sat/smt/array_diagnostics.cpp
@@ -93,8 +93,10 @@ namespace array {
                         validate_extensionality(n, k);
             }
             expr* x = nullptr, *y = nullptr;
+#if 0
             if (m.is_eq(n->get_expr(), x, y) && a.is_array(x))
                 std::cout << ctx.bpp(n) << " " << s().value(n->bool_var()) << "\n";
+#endif
             if (m.is_eq(n->get_expr(), x, y) && a.is_array(x) && s().value(n->bool_var()) == l_false)
                 validate_extensionality(expr2enode(x), expr2enode(y));
         }        
diff --git a/src/sat/smt/bv_invariant.cpp b/src/sat/smt/bv_invariant.cpp
index c73c9806d..490fa53e3 100644
--- a/src/sat/smt/bv_invariant.cpp
+++ b/src/sat/smt/bv_invariant.cpp
@@ -93,6 +93,7 @@ namespace bv {
         } while (curr != v);
 
         zero_one_bits const& _bits = m_zero_one_bits[v];
+#if 0
         if (_bits.size() != num_bits) {
             std::cout << "v" << v << " " << _bits.size() << " " << num_bits << "\n";
             std::cout << "true: " << mk_true() << "\n";
@@ -102,6 +103,7 @@ namespace bv {
             }
             while (curr != v);
         }
+#endif
         SASSERT(_bits.size() == num_bits);
         VERIFY(_bits.size() == num_bits);
         bool_vector already_found;
diff --git a/src/sat/smt/pb_solver.cpp b/src/sat/smt/pb_solver.cpp
index ff08ab284..f85872db6 100644
--- a/src/sat/smt/pb_solver.cpp
+++ b/src/sat/smt/pb_solver.cpp
@@ -1624,7 +1624,7 @@ namespace pb {
             CTRACE("ba", coeff == 0, display(tout << l << " coeff: " << coeff << "\n", p, true);); 
             
             if (_debug_conflict) {
-                std::cout << "coeff " << coeff << "\n";
+                IF_VERBOSE(0, verbose_stream() << "coeff " << coeff << "\n";);
             }
 
             SASSERT(coeff > 0);
@@ -2256,7 +2256,7 @@ namespace pb {
         SASSERT(c.lit() == sat::null_literal || c.is_watched(*this, c.lit()));
 
         // pre-condition is that the literals, except c.lit(), in c are unwatched.
-        if (c.id() == _bad_id) std::cout << "recompile: " << c << "\n";
+        //if (c.id() == _bad_id) std::cout << "recompile: " << c << "\n";
         m_weights.resize(2*s().num_vars(), 0);
         for (literal l : c) {
             ++m_weights[l.index()];
diff --git a/src/sat/smt/q_model_fixer.cpp b/src/sat/smt/q_model_fixer.cpp
index cdea60d23..52d1a064c 100644
--- a/src/sat/smt/q_model_fixer.cpp
+++ b/src/sat/smt/q_model_fixer.cpp
@@ -302,9 +302,10 @@ namespace q {
             return md->v2t[md->values[j]];
         };
         
+#if 0
         for (unsigned j = 0; j < sz; ++j)
             std::cout << mk_pp(md->values[j], m) << "\n";
-
+#endif
 
         expr* arg = t->get_arg(i);
 
diff --git a/src/shell/lp_frontend.cpp b/src/shell/lp_frontend.cpp
index 0234e61b4..70d2cffb1 100644
--- a/src/shell/lp_frontend.cpp
+++ b/src/shell/lp_frontend.cpp
@@ -15,6 +15,7 @@ Author:
 #include "util/rlimit.h"
 #include "util/gparams.h"
 #include "util/mutex.h"
+#include <iostream>
 #include <signal.h>
 #include "smt/params/smt_params_helper.hpp"
 
diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp
index 78102eb6e..c02d4ef03 100644
--- a/src/shell/opt_frontend.cpp
+++ b/src/shell/opt_frontend.cpp
@@ -4,6 +4,7 @@ Copyright (c) 2015 Microsoft Corporation
 --*/
 
 #include<fstream>
+#include<iostream>
 #include<signal.h>
 #include<time.h>
 #include "util/gparams.h"
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 49fe8f22f..1b6088c1f 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -42,6 +42,7 @@ Revision History:
 #include "smt/smt_model_finder.h"
 #include "smt/smt_parallel.h"
 #include "smt/smt_arith_value.h"
+#include <iostream>
 
 namespace smt {
 
@@ -3943,8 +3944,7 @@ namespace smt {
         if (m_fparams.m_model_on_final_check) {
             mk_proto_model();
             model_pp(std::cout, *m_proto_model);
-            std::cout << "END_OF_MODEL\n";
-            std::cout.flush();
+            std::cout << "END_OF_MODEL" << std::endl;
         }
 
         m_stats.m_num_final_checks++;
diff --git a/src/smt/smt_context_stat.cpp b/src/smt/smt_context_stat.cpp
index 9899ba322..5b2a541a2 100644
--- a/src/smt/smt_context_stat.cpp
+++ b/src/smt/smt_context_stat.cpp
@@ -136,9 +136,9 @@ namespace smt {
     }
 
     void context::display_profile_res_sub(std::ostream & out) const {
-        display_var_occs_histogram(std::cerr);
-        display_num_min_occs(std::cerr);
-        std::cerr << "\n";
+        display_var_occs_histogram(out);
+        display_num_min_occs(out);
+        out << "\n";
     }
 
     void context::display_profile(std::ostream & out) const {
diff --git a/src/smt/smt_statistics.h b/src/smt/smt_statistics.h
index 45022b31c..ce773864a 100644
--- a/src/smt/smt_statistics.h
+++ b/src/smt/smt_statistics.h
@@ -18,8 +18,6 @@ Revision History:
 --*/
 #pragma once
 
-#include<iostream>
-
 namespace smt {
 
     struct statistics {
diff --git a/src/smt/theory_array_bapa.cpp b/src/smt/theory_array_bapa.cpp
index 7b7f93f02..9379c939f 100644
--- a/src/smt/theory_array_bapa.cpp
+++ b/src/smt/theory_array_bapa.cpp
@@ -272,12 +272,14 @@ namespace smt {
             std::cout << smt << "\n";
             std::cout << tns << "\n";
 #endif
+#if 0
             if (tns == sz1) {
                 std::cout << "SEEN " << tms << "\n";
             }
             if (tns == sz2) {
                 std::cout << "SEEN " << smt << "\n";                
             }
+#endif
             ctx().push_trail(value_trail<bool>(i1.m_is_leaf, false));
             ctx().push_trail(value_trail<bool>(i2.m_is_leaf, false));
             expr_ref k1(m), k2(m), k3(m);
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 0dc52c1b2..f24e4746d 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -1598,10 +1598,12 @@ namespace smt {
         lbool is_sat = k.check();
         validating = false;
         // std::cout << is_sat << "\n";
+#if 0
         if (is_sat == l_true) {
             std::cout << A << "\n";
             std::cout << B << "\n";
         }
+#endif
         SASSERT(is_sat != l_true);
         return true;
     }
diff --git a/src/tactic/arith/bv2real_rewriter.cpp b/src/tactic/arith/bv2real_rewriter.cpp
index 03acc8161..f94965fe9 100644
--- a/src/tactic/arith/bv2real_rewriter.cpp
+++ b/src/tactic/arith/bv2real_rewriter.cpp
@@ -368,7 +368,6 @@ br_status bv2real_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr *
           tout << "\n";);
     
     if (u().memory_exceeded()) {
-        std::cout << "tactic exception\n";
         throw tactic_exception("bv2real-memory exceeded");
     }
     if(f->get_family_id() == m_arith.get_family_id()) {
diff --git a/src/tactic/core/collect_statistics_tactic.cpp b/src/tactic/core/collect_statistics_tactic.cpp
index dc906cb32..04750a7c3 100644
--- a/src/tactic/core/collect_statistics_tactic.cpp
+++ b/src/tactic/core/collect_statistics_tactic.cpp
@@ -29,6 +29,7 @@ Notes:
 #include "ast/fpa_decl_plugin.h"
 #include "tactic/tactical.h"
 #include "util/stats.h"
+#include <iostream>
 
 #include "tactic/core/collect_statistics_tactic.h"
 
diff --git a/src/util/approx_nat.h b/src/util/approx_nat.h
index 08b1274d2..67e672f84 100644
--- a/src/util/approx_nat.h
+++ b/src/util/approx_nat.h
@@ -19,7 +19,7 @@ Notes:
 --*/
 #pragma once
 
-#include<iostream>
+#include<ostream>
 #include<climits>
 
 class approx_nat {
diff --git a/src/util/approx_set.h b/src/util/approx_set.h
index 7355437b9..aa6f8d383 100644
--- a/src/util/approx_set.h
+++ b/src/util/approx_set.h
@@ -17,7 +17,7 @@ Revision History:
 
 --*/
 #pragma once
-#include<iostream>
+#include<ostream>
 #include "util/debug.h"
 
 template<typename T> class approx_set_traits;
diff --git a/src/util/cmd_context_types.cpp b/src/util/cmd_context_types.cpp
index 61a7bd755..9506b93cc 100644
--- a/src/util/cmd_context_types.cpp
+++ b/src/util/cmd_context_types.cpp
@@ -14,7 +14,6 @@ Author:
 Notes:
 
 --*/
-#include<iostream>
 #include "util/cmd_context_types.h"
 
 std::ostream & operator<<(std::ostream & out, cmd_arg_kind k) {
diff --git a/src/util/cmd_context_types.h b/src/util/cmd_context_types.h
index f2d0d2a0c..80e284d90 100644
--- a/src/util/cmd_context_types.h
+++ b/src/util/cmd_context_types.h
@@ -18,6 +18,7 @@ Notes:
 
 #include "util/symbol.h"
 #include "util/z3_exception.h"
+#include <ostream>
 #include<sstream>
 class rational;
 class expr;
diff --git a/src/util/ext_numeral.h b/src/util/ext_numeral.h
index 93bda8d32..cc2682c27 100644
--- a/src/util/ext_numeral.h
+++ b/src/util/ext_numeral.h
@@ -19,7 +19,7 @@ Revision History:
 --*/
 #pragma once
 
-#include<iostream>
+#include<ostream>
 #include "util/debug.h"
     
 enum ext_numeral_kind { EN_MINUS_INFINITY, EN_NUMERAL, EN_PLUS_INFINITY };
diff --git a/src/util/permutation.h b/src/util/permutation.h
index 2b0623fe9..1fb7dc9e7 100644
--- a/src/util/permutation.h
+++ b/src/util/permutation.h
@@ -18,7 +18,7 @@ Revision History:
 --*/
 #pragma once
 
-#include<iostream>
+#include<ostream>
 #include "util/vector.h"
 
 class permutation {
diff --git a/src/util/region.h b/src/util/region.h
index f3f0d35ab..9f28be908 100644
--- a/src/util/region.h
+++ b/src/util/region.h
@@ -18,7 +18,7 @@ Revision History:
 --*/
 #pragma once
 #include<cstdlib>
-#include<iostream>
+#include<ostream>
 
 #ifdef Z3DEBUG
 
diff --git a/src/util/scoped_ctrl_c.cpp b/src/util/scoped_ctrl_c.cpp
index e6214cfab..a3f5ee772 100644
--- a/src/util/scoped_ctrl_c.cpp
+++ b/src/util/scoped_ctrl_c.cpp
@@ -17,7 +17,6 @@ Revision History:
 
 --*/
 #include<signal.h>
-#include<iostream>
 #include "util/scoped_ctrl_c.h"
 
 static scoped_ctrl_c * g_obj = nullptr;
diff --git a/src/util/statistics.h b/src/util/statistics.h
index cea9099d1..32d6bac9f 100644
--- a/src/util/statistics.h
+++ b/src/util/statistics.h
@@ -18,7 +18,7 @@ Notes:
 --*/
 #pragma once
 
-#include<iostream>
+#include<ostream>
 #include "util/vector.h"
 #include "util/rlimit.h"
 
diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h
index 78482c0f1..bb170abe7 100644
--- a/src/util/stopwatch.h
+++ b/src/util/stopwatch.h
@@ -21,7 +21,7 @@ Revision History:
 
 #include "util/debug.h"
 #include <chrono>
-#include <iostream>
+#include <ostream>
 #include<iomanip>
 
 
diff --git a/src/util/stream_buffer.h b/src/util/stream_buffer.h
index 104b22eac..f4b916ae7 100644
--- a/src/util/stream_buffer.h
+++ b/src/util/stream_buffer.h
@@ -20,7 +20,7 @@ Revision History:
 --*/
 #pragma once
 
-#include<iostream>
+#include<istream>
 
 class stream_buffer {
     std::istream & m_stream;
@@ -40,5 +40,3 @@ public:
         m_val = m_stream.get();
     }
 };
-
-
diff --git a/src/util/timeit.cpp b/src/util/timeit.cpp
index 2a78f08a3..5db58705f 100644
--- a/src/util/timeit.cpp
+++ b/src/util/timeit.cpp
@@ -16,11 +16,11 @@ Author:
 Revision History:
 
 --*/
-#include<iostream>
 #include "util/timeit.h"
 #include "util/memory_manager.h"
 #include "util/stopwatch.h"
 #include<iomanip>
+#include<iostream>
 
 struct timeit::imp {
     stopwatch      m_watch;
@@ -45,9 +45,9 @@ struct timeit::imp {
     }
 };
 
-timeit::timeit(bool enable, char const * msg, std::ostream & out) {
+timeit::timeit(bool enable, char const * msg, std::ostream * out) {
     if (enable)
-        m_imp = alloc(imp, msg, out);
+        m_imp = alloc(imp, msg, out ? *out : std::cerr);
     else
         m_imp = nullptr;
 }
diff --git a/src/util/timeit.h b/src/util/timeit.h
index e29284a04..7b161103f 100644
--- a/src/util/timeit.h
+++ b/src/util/timeit.h
@@ -21,11 +21,14 @@ Revision History:
 --*/
 #pragma once
 
+#include<ostream>
+
 class timeit {
     struct imp;
     imp *  m_imp;
 public:
-    timeit(bool enable, char const * msg, std::ostream & out = std::cerr);
+    timeit(bool enable, char const * msg, std::ostream * out = nullptr);
+    timeit(bool enable, char const * msg, std::ostream & out) : timeit(enable, msg, &out) {}
     ~timeit();
 };
 
diff --git a/src/util/util.cpp b/src/util/util.cpp
index a59b26990..ee1e734af 100644
--- a/src/util/util.cpp
+++ b/src/util/util.cpp
@@ -18,7 +18,7 @@ Revision History:
 --*/
 
 #include "util/util.h"
-
+#include <iostream>
 
 static unsigned g_verbosity_level = 0;
 
diff --git a/src/util/util.h b/src/util/util.h
index 4cac2123a..f08558f37 100644
--- a/src/util/util.h
+++ b/src/util/util.h
@@ -20,7 +20,7 @@ Revision History:
 
 #include "util/debug.h"
 #include "util/memory_manager.h"
-#include<iostream>
+#include<ostream>
 #include<climits>
 #include<limits>
 #include<stdint.h>
diff --git a/src/util/warning.h b/src/util/warning.h
index 203fa6fe4..5a74ebd2d 100644
--- a/src/util/warning.h
+++ b/src/util/warning.h
@@ -17,7 +17,7 @@ Revision History:
 
 --*/
 #pragma once
-#include<iostream>
+#include<ostream>
 #include<stdarg.h>
 
 void send_warnings_to_stdout(bool flag);