From c3407fc30444bc3c95ba5212231dad4423439391 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Date: Fri, 17 Jun 2022 17:11:18 +0100
Subject: [PATCH] fix build of tests

---
 src/test/algebraic.cpp                    | 1 +
 src/test/arith_rewriter.cpp               | 2 +-
 src/test/arith_simplifier_plugin.cpp      | 1 +
 src/test/bdd.cpp                          | 1 +
 src/test/bits.cpp                         | 1 +
 src/test/chashtable.cpp                   | 1 +
 src/test/cube_clause.cpp                  | 2 +-
 src/test/datalog_parser.cpp               | 1 +
 src/test/dl_query.cpp                     | 1 +
 src/test/dl_table.cpp                     | 1 +
 src/test/doc.cpp                          | 2 +-
 src/test/egraph.cpp                       | 1 +
 src/test/escaped.cpp                      | 1 +
 src/test/expr_substitution.cpp            | 1 +
 src/test/f2n.cpp                          | 1 +
 src/test/factor_rewriter.cpp              | 1 +
 src/test/get_consequences.cpp             | 1 +
 src/test/heap_trie.cpp                    | 1 +
 src/test/hilbert_basis.cpp                | 1 +
 src/test/horn_subsume_model_converter.cpp | 1 +
 src/test/hwf.cpp                          | 1 +
 src/test/interval.cpp                     | 1 +
 src/test/karr.cpp                         | 1 +
 src/test/model2expr.cpp                   | 1 +
 src/test/model_based_opt.cpp              | 1 +
 src/test/model_evaluator.cpp              | 2 +-
 src/test/model_retrieval.cpp              | 1 +
 src/test/mpbq.cpp                         | 1 +
 src/test/mpff.cpp                         | 1 +
 src/test/mpfx.cpp                         | 1 +
 src/test/mpq.cpp                          | 1 +
 src/test/mpz.cpp                          | 1 +
 src/test/nlarith_util.cpp                 | 1 +
 src/test/nlsat.cpp                        | 1 +
 src/test/old_interval.cpp                 | 1 +
 src/test/parray.cpp                       | 1 +
 src/test/pb2bv.cpp                        | 1 +
 src/test/pdd.cpp                          | 1 +
 src/test/pdd_solver.cpp                   | 1 +
 src/test/polynomial.cpp                   | 1 +
 src/test/polynorm.cpp                     | 2 +-
 src/test/prime_generator.cpp              | 1 +
 src/test/proof_checker.cpp                | 1 +
 src/test/qe_arith.cpp                     | 1 +
 src/test/quant_solve.cpp                  | 1 +
 src/test/rcf.cpp                          | 1 +
 src/test/sat_local_search.cpp             | 1 +
 src/test/sat_lookahead.cpp                | 1 +
 src/test/sat_user_scope.cpp               | 1 +
 src/test/scoped_timer.cpp                 | 1 +
 src/test/simplex.cpp                      | 1 +
 src/test/solver_pool.cpp                  | 1 +
 src/test/sorting_network.cpp              | 1 +
 src/test/substitution.cpp                 | 1 +
 src/test/tbv.cpp                          | 1 +
 src/test/theory_dl.cpp                    | 1 +
 src/test/theory_pb.cpp                    | 1 +
 src/test/total_order.cpp                  | 1 +
 src/test/trigo.cpp                        | 1 +
 src/test/udoc_relation.cpp                | 2 +-
 src/test/uint_set.cpp                     | 1 +
 src/test/upolynomial.cpp                  | 1 +
 src/test/value_generator.cpp              | 1 +
 src/test/value_sweep.cpp                  | 1 +
 src/test/var_subst.cpp                    | 1 +
 src/test/vector.cpp                       | 1 +
 src/test/zstring.cpp                      | 1 +
 67 files changed, 67 insertions(+), 6 deletions(-)

diff --git a/src/test/algebraic.cpp b/src/test/algebraic.cpp
index 5c91623d000..371997c023c 100644
--- a/src/test/algebraic.cpp
+++ b/src/test/algebraic.cpp
@@ -20,6 +20,7 @@ Module Name:
 #include "math/polynomial/polynomial_var2value.h"
 #include "util/mpbq.h"
 #include "util/rlimit.h"
+#include <iostream>
 
 static void display_anums(std::ostream & out, scoped_anum_vector const & rs) {
     out << "numbers in decimal:\n";
diff --git a/src/test/arith_rewriter.cpp b/src/test/arith_rewriter.cpp
index da49e58dcf6..d79f09cc318 100644
--- a/src/test/arith_rewriter.cpp
+++ b/src/test/arith_rewriter.cpp
@@ -10,7 +10,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "ast/rewriter/th_rewriter.h"
 #include "model/model.h"
 #include "parsers/smt2/smt2parser.h"
-
+#include <iostream>
 
 static expr_ref parse_fml(ast_manager& m, char const* str) {
     expr_ref result(m);
diff --git a/src/test/arith_simplifier_plugin.cpp b/src/test/arith_simplifier_plugin.cpp
index 63a6838d4b2..639fda76597 100644
--- a/src/test/arith_simplifier_plugin.cpp
+++ b/src/test/arith_simplifier_plugin.cpp
@@ -6,6 +6,7 @@ Copyright (c) 2015 Microsoft Corporation
 
 #include "smt/arith_eq_solver.h"
 #include "smt/params/smt_params.h"
+#include <iostream>
 
 typedef rational numeral;
 typedef vector<numeral> row;
diff --git a/src/test/bdd.cpp b/src/test/bdd.cpp
index 7c7af2fb43b..d08d10a11ca 100644
--- a/src/test/bdd.cpp
+++ b/src/test/bdd.cpp
@@ -1,4 +1,5 @@
 #include "math/dd/dd_bdd.h"
+#include <iostream>
 
 namespace dd {
     static void test1() {
diff --git a/src/test/bits.cpp b/src/test/bits.cpp
index 2bef6a0badc..2fc1efe0c08 100644
--- a/src/test/bits.cpp
+++ b/src/test/bits.cpp
@@ -10,6 +10,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "util/vector.h"
 #include "util/mpz.h"
 #include "util/bit_util.h"
+#include <iostream>
 
 static void tst_shl(unsigned src_sz, unsigned const * src, unsigned k, 
                     unsigned dst_sz, unsigned const * dst, bool trace = true) {
diff --git a/src/test/chashtable.cpp b/src/test/chashtable.cpp
index 8e4dadf993a..773509aba8c 100644
--- a/src/test/chashtable.cpp
+++ b/src/test/chashtable.cpp
@@ -20,6 +20,7 @@ Revision History:
 #include "util/hashtable.h"
 #include "util/hash.h"
 #include "util/util.h"
+#include <iostream>
 
 typedef chashtable<int, int_hash, default_eq<int> > int_table;
 typedef cmap<int, int, int_hash, default_eq<int> > int_map;
diff --git a/src/test/cube_clause.cpp b/src/test/cube_clause.cpp
index 0c783277b9a..920c5c57c46 100644
--- a/src/test/cube_clause.cpp
+++ b/src/test/cube_clause.cpp
@@ -1,7 +1,7 @@
 #include "ast/reg_decl_plugins.h"
 #include "solver/solver_pool.h"
 #include "smt/smt_solver.h"
-
+#include <iostream>
 
 void tst_cube_clause() {
     ast_manager m;
diff --git a/src/test/datalog_parser.cpp b/src/test/datalog_parser.cpp
index ca5e94f7578..ee69bff8b5a 100644
--- a/src/test/datalog_parser.cpp
+++ b/src/test/datalog_parser.cpp
@@ -11,6 +11,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "muz/fp/dl_register_engine.h"
 #include "smt/params/smt_params.h"
 #include "ast/reg_decl_plugins.h"
+#include <iostream>
 
 using namespace datalog;
 
diff --git a/src/test/dl_query.cpp b/src/test/dl_query.cpp
index 2181f97ad5a..34dc7e020ec 100644
--- a/src/test/dl_query.cpp
+++ b/src/test/dl_query.cpp
@@ -13,6 +13,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "util/stopwatch.h"
 #include "ast/reg_decl_plugins.h"
 #include "muz/rel/dl_relation_manager.h"
+#include <iostream>
 
 using namespace datalog;
 
diff --git a/src/test/dl_table.cpp b/src/test/dl_table.cpp
index b3082cc6a81..0f429d22374 100644
--- a/src/test/dl_table.cpp
+++ b/src/test/dl_table.cpp
@@ -6,6 +6,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "muz/rel/dl_table.h"
 #include "muz/fp/dl_register_engine.h"
 #include "muz/rel/dl_relation_manager.h"
+#include <iostream>
 
 typedef datalog::table_base* (*mk_table_fn)(datalog::relation_manager& m, datalog::table_signature& sig);
 
diff --git a/src/test/doc.cpp b/src/test/doc.cpp
index 4d84ff964be..f1b5cf2ce4d 100644
--- a/src/test/doc.cpp
+++ b/src/test/doc.cpp
@@ -17,7 +17,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "ast/ast_util.h"
 #include "ast/rewriter/expr_safe_replace.h"
 #include "ast/rewriter/th_rewriter.h"
-
+#include <iostream>
 
 static void tst_doc1(unsigned n) {
     doc_manager m(n);
diff --git a/src/test/egraph.cpp b/src/test/egraph.cpp
index 508384f8f06..a3c61abadbf 100644
--- a/src/test/egraph.cpp
+++ b/src/test/egraph.cpp
@@ -9,6 +9,7 @@ Copyright (c) 2020 Microsoft Corporation
 #include "ast/reg_decl_plugins.h"
 #include "ast/ast_pp.h"
 #include "ast/arith_decl_plugin.h"
+#include <iostream>
 
 static expr_ref mk_const(ast_manager& m, char const* name, sort* s) {
     return expr_ref(m.mk_const(symbol(name), s), m);
diff --git a/src/test/escaped.cpp b/src/test/escaped.cpp
index 9bc2aecec6d..4fb85960d47 100644
--- a/src/test/escaped.cpp
+++ b/src/test/escaped.cpp
@@ -17,6 +17,7 @@ Revision History:
 
 --*/
 #include "util/util.h"
+#include <iostream>
 
 void tst_escaped() {
     std::cout << "[" << escaped("\"hello\"\"world\"\n\n") << "]\n";
diff --git a/src/test/expr_substitution.cpp b/src/test/expr_substitution.cpp
index 3b74535e734..c66681c1bf5 100644
--- a/src/test/expr_substitution.cpp
+++ b/src/test/expr_substitution.cpp
@@ -13,6 +13,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "ast/arith_decl_plugin.h"
 #include "ast/reg_decl_plugins.h"
 #include "ast/rewriter/th_rewriter.h"
+#include <iostream>
 
 expr* mk_bv_xor(bv_util& bv, expr* a, expr* b) {
     expr* args[2];
diff --git a/src/test/f2n.cpp b/src/test/f2n.cpp
index 7831a31cf14..211cf6013d4 100644
--- a/src/test/f2n.cpp
+++ b/src/test/f2n.cpp
@@ -18,6 +18,7 @@ Revision History:
 #include "util/f2n.h"
 #include "util/hwf.h"
 #include "util/mpf.h"
+#include <iostream>
 
 static void tst1() {
     hwf_manager      hm;
diff --git a/src/test/factor_rewriter.cpp b/src/test/factor_rewriter.cpp
index 486221e5bf3..223527c11f3 100644
--- a/src/test/factor_rewriter.cpp
+++ b/src/test/factor_rewriter.cpp
@@ -8,6 +8,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "ast/bv_decl_plugin.h"
 #include "ast/ast_pp.h"
 #include "ast/reg_decl_plugins.h"
+#include <iostream>
 
 void tst_factor_rewriter() {
     ast_manager m;
diff --git a/src/test/get_consequences.cpp b/src/test/get_consequences.cpp
index 0e5124d5839..d8c070b6d23 100644
--- a/src/test/get_consequences.cpp
+++ b/src/test/get_consequences.cpp
@@ -12,6 +12,7 @@ Copyright (c) 2016 Microsoft Corporation
 #include "tactic/tactic.h"
 #include "model/model_smt2_pp.h"
 #include "tactic/fd_solver/fd_solver.h"
+#include <iostream>
 
 static expr_ref mk_const(ast_manager& m, char const* name, sort* s) {
     return expr_ref(m.mk_const(symbol(name), s), m);
diff --git a/src/test/heap_trie.cpp b/src/test/heap_trie.cpp
index b6f65163380..a86e0e741ac 100644
--- a/src/test/heap_trie.cpp
+++ b/src/test/heap_trie.cpp
@@ -5,6 +5,7 @@ Copyright (c) 2015 Microsoft Corporation
 --*/
 
 #include "math/hilbert/heap_trie.h"
+#include <iostream>
 
 struct unsigned_le {
     static bool le(unsigned i, unsigned j) { return i <= j; }
diff --git a/src/test/hilbert_basis.cpp b/src/test/hilbert_basis.cpp
index 06446e8e963..93c58374ef7 100644
--- a/src/test/hilbert_basis.cpp
+++ b/src/test/hilbert_basis.cpp
@@ -15,6 +15,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "util/rlimit.h"
 #include <signal.h>
 #include <time.h>
+#include <iostream>
 #include <sstream>
 
 static bool g_use_ordered_support = false;
diff --git a/src/test/horn_subsume_model_converter.cpp b/src/test/horn_subsume_model_converter.cpp
index 6d4dcc26f73..aea819d7ae0 100644
--- a/src/test/horn_subsume_model_converter.cpp
+++ b/src/test/horn_subsume_model_converter.cpp
@@ -9,6 +9,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "ast/arith_decl_plugin.h"
 #include "model/model_smt2_pp.h"
 #include "ast/reg_decl_plugins.h"
+#include <iostream>
 
 void tst_horn_subsume_model_converter() {
     ast_manager m;
diff --git a/src/test/hwf.cpp b/src/test/hwf.cpp
index 69767347335..8a019ec02b6 100644
--- a/src/test/hwf.cpp
+++ b/src/test/hwf.cpp
@@ -19,6 +19,7 @@ Revision History:
 #include "util/hwf.h"
 #include "util/f2n.h"
 #include "util/rational.h"
+#include <iostream>
 
 static void bug_set_double() {
     hwf_manager m;
diff --git a/src/test/interval.cpp b/src/test/interval.cpp
index 5180912f5bf..f289871deab 100644
--- a/src/test/interval.cpp
+++ b/src/test/interval.cpp
@@ -23,6 +23,7 @@ Revision History:
 #include "ast/ast.h"
 #include "util/debug.h"
 #include "util/rlimit.h"
+#include <iostream>
 
 template class interval_manager<im_default_config>;
 typedef im_default_config::interval interval;
diff --git a/src/test/karr.cpp b/src/test/karr.cpp
index cf58673240f..2ec13ecc267 100644
--- a/src/test/karr.cpp
+++ b/src/test/karr.cpp
@@ -5,6 +5,7 @@ Copyright (c) 2015 Microsoft Corporation
 --*/
 #include "util/rlimit.h"
 #include "math/hilbert/hilbert_basis.h"
+#include <iostream>
 
 /*
   Test generation of linear congruences a la Karr.
diff --git a/src/test/model2expr.cpp b/src/test/model2expr.cpp
index 41047825cf4..5163abade0e 100644
--- a/src/test/model2expr.cpp
+++ b/src/test/model2expr.cpp
@@ -9,6 +9,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "ast/arith_decl_plugin.h"
 #include "model/model_smt2_pp.h"
 #include "ast/reg_decl_plugins.h"
+#include <iostream>
 
 void tst_model2expr() {
     ast_manager m;
diff --git a/src/test/model_based_opt.cpp b/src/test/model_based_opt.cpp
index 1bae7435fcf..b307f85e47b 100644
--- a/src/test/model_based_opt.cpp
+++ b/src/test/model_based_opt.cpp
@@ -1,6 +1,7 @@
 #include "math/simplex/model_based_opt.h"
 #include "util/util.h"
 #include "util/uint_set.h"
+#include <iostream>
 
 typedef opt::model_based_opt::var var;
 
diff --git a/src/test/model_evaluator.cpp b/src/test/model_evaluator.cpp
index 3e1c95617a1..f4a64d4dc8b 100644
--- a/src/test/model_evaluator.cpp
+++ b/src/test/model_evaluator.cpp
@@ -4,7 +4,7 @@
 #include "ast/arith_decl_plugin.h"
 #include "ast/reg_decl_plugins.h"
 #include "ast/ast_pp.h"
-
+#include <iostream>
 
 void tst_model_evaluator() {
     ast_manager m;
diff --git a/src/test/model_retrieval.cpp b/src/test/model_retrieval.cpp
index e0fd2808840..415a5772c76 100644
--- a/src/test/model_retrieval.cpp
+++ b/src/test/model_retrieval.cpp
@@ -13,6 +13,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "ast/array_decl_plugin.h"
 #include "model/model_v2_pp.h"
 #include "ast/reg_decl_plugins.h"
+#include <iostream>
 
 void tst_model_retrieval()
 {          
diff --git a/src/test/mpbq.cpp b/src/test/mpbq.cpp
index 4dc92d80dd9..16dead4cfaa 100644
--- a/src/test/mpbq.cpp
+++ b/src/test/mpbq.cpp
@@ -17,6 +17,7 @@ Revision History:
 
 --*/
 #include "util/mpbq.h"
+#include <iostream>
 
 static void tst1() {
     unsynch_mpz_manager zm;
diff --git a/src/test/mpff.cpp b/src/test/mpff.cpp
index 83c500b49e5..b03cc5f2ecf 100644
--- a/src/test/mpff.cpp
+++ b/src/test/mpff.cpp
@@ -18,6 +18,7 @@ Revision History:
 --*/
 #include <sstream>
 #include <cstring>
+#include <iostream>
 #include "util/mpff.h"
 #include "util/mpz.h"
 #include "util/mpq.h"
diff --git a/src/test/mpfx.cpp b/src/test/mpfx.cpp
index f5cf7e2fb46..7752157fd39 100644
--- a/src/test/mpfx.cpp
+++ b/src/test/mpfx.cpp
@@ -17,6 +17,7 @@ Revision History:
 
 --*/
 #include "util/mpfx.h"
+#include <iostream>
 
 static void tst1() {
     mpfx_manager m;
diff --git a/src/test/mpq.cpp b/src/test/mpq.cpp
index 6294a97f742..6c15c855667 100644
--- a/src/test/mpq.cpp
+++ b/src/test/mpq.cpp
@@ -20,6 +20,7 @@ Revision History:
 #include "util/mpq.h"
 #include "util/rational.h"
 #include "util/timeit.h"
+#include <iostream>
 
 static void tst0() {
     synch_mpq_manager m;
diff --git a/src/test/mpz.cpp b/src/test/mpz.cpp
index fc2177ca213..694f13e9650 100644
--- a/src/test/mpz.cpp
+++ b/src/test/mpz.cpp
@@ -21,6 +21,7 @@ Revision History:
 #include "util/rational.h"
 #include "util/timeit.h"
 #include "util/scoped_numeral.h"
+#include <iostream>
 
 static void tst1() {
     synch_mpz_manager m;
diff --git a/src/test/nlarith_util.cpp b/src/test/nlarith_util.cpp
index 4769c1591d6..d6105cf8229 100644
--- a/src/test/nlarith_util.cpp
+++ b/src/test/nlarith_util.cpp
@@ -8,6 +8,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "ast/arith_decl_plugin.h"
 #include "ast/ast_pp.h"
 #include "ast/reg_decl_plugins.h"
+#include <iostream>
 
 void tst_nlarith_util() {
     ast_manager M;
diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp
index 44d4120fe27..9274938efc2 100644
--- a/src/test/nlsat.cpp
+++ b/src/test/nlsat.cpp
@@ -24,6 +24,7 @@ Module Name:
 #include "nlsat/nlsat_explain.h"
 #include "math/polynomial/polynomial_cache.h"
 #include "util/rlimit.h"
+#include <iostream>
 
 nlsat::interval_set_ref tst_interval(nlsat::interval_set_ref const & s1,
                                      nlsat::interval_set_ref const & s2,
diff --git a/src/test/old_interval.cpp b/src/test/old_interval.cpp
index 751f6fdbec9..bc2f9fb13a5 100644
--- a/src/test/old_interval.cpp
+++ b/src/test/old_interval.cpp
@@ -17,6 +17,7 @@ Revision History:
 
 --*/
 #include "smt/old_interval.h"
+#include <iostream>
 
 static void tst1() {
     ext_numeral inf(true);
diff --git a/src/test/parray.cpp b/src/test/parray.cpp
index 6aef4f3593e..7e6b78cd8fa 100644
--- a/src/test/parray.cpp
+++ b/src/test/parray.cpp
@@ -19,6 +19,7 @@ Revision History:
 #include "util/parray.h"
 #include "util/small_object_allocator.h"
 #include "ast/ast.h"
+#include <iostream>
 
 template<bool PRESERVE_ROOTS>
 struct int_parray_config {
diff --git a/src/test/pb2bv.cpp b/src/test/pb2bv.cpp
index 169df85adb3..8772fec92bf 100644
--- a/src/test/pb2bv.cpp
+++ b/src/test/pb2bv.cpp
@@ -19,6 +19,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "tactic/fd_solver/fd_solver.h"
 #include "solver/solver.h"
 #include "ast/arith_decl_plugin.h"
+#include <iostream>
 
 static void test1() {
     ast_manager m;
diff --git a/src/test/pdd.cpp b/src/test/pdd.cpp
index b10abb89146..b0cbb657c92 100644
--- a/src/test/pdd.cpp
+++ b/src/test/pdd.cpp
@@ -1,4 +1,5 @@
 #include "math/dd/dd_pdd.h"
+#include <iostream>
 
 namespace dd {
 
diff --git a/src/test/pdd_solver.cpp b/src/test/pdd_solver.cpp
index 7a1c071310f..a8650426697 100644
--- a/src/test/pdd_solver.cpp
+++ b/src/test/pdd_solver.cpp
@@ -9,6 +9,7 @@
 #include "tactic/goal.h"
 #include "tactic/tactic.h"
 #include "tactic/bv/bit_blaster_tactic.h"
+#include <iostream>
 
 namespace dd {
     void print_eqs(ptr_vector<solver::equation> const& eqs) {
diff --git a/src/test/polynomial.cpp b/src/test/polynomial.cpp
index 091d03c61f6..f259c42344e 100644
--- a/src/test/polynomial.cpp
+++ b/src/test/polynomial.cpp
@@ -22,6 +22,7 @@ Module Name:
 #include "math/polynomial/polynomial_cache.h"
 #include "math/polynomial/linear_eq_solver.h"
 #include "util/rlimit.h"
+#include <iostream>
 
 static void tst1() {
     std::cout << "\n----- Basic testing -------\n";
diff --git a/src/test/polynorm.cpp b/src/test/polynorm.cpp
index 58481938beb..80ff749040f 100644
--- a/src/test/polynorm.cpp
+++ b/src/test/polynorm.cpp
@@ -10,7 +10,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "ast/reg_decl_plugins.h"
 #include "ast/rewriter/arith_rewriter.h"
 #include "ast/ast_pp.h"
-
+#include <iostream>
 
 static expr_ref parse_fml(ast_manager& m, char const* str) {
     expr_ref result(m);
diff --git a/src/test/prime_generator.cpp b/src/test/prime_generator.cpp
index 3a63b805ac1..a604187779c 100644
--- a/src/test/prime_generator.cpp
+++ b/src/test/prime_generator.cpp
@@ -18,6 +18,7 @@ Module Name:
 --*/
 #include "util/mpz.h"
 #include "util/prime_generator.h"
+#include <iostream>
 
 void tst_prime_generator() {
     unsynch_mpz_manager m;
diff --git a/src/test/proof_checker.cpp b/src/test/proof_checker.cpp
index 7a9b619cd3f..bc3dd39ade7 100644
--- a/src/test/proof_checker.cpp
+++ b/src/test/proof_checker.cpp
@@ -6,6 +6,7 @@ Copyright (c) 2015 Microsoft Corporation
 
 #include "ast/proofs/proof_checker.h"
 #include "ast/ast_ll_pp.h"
+#include <iostream>
 
 void tst_checker1() {
     ast_manager m(PGM_ENABLED);
diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp
index ab268a65165..859d7f2e5bb 100644
--- a/src/test/qe_arith.cpp
+++ b/src/test/qe_arith.cpp
@@ -15,6 +15,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "smt/smt_context.h"
 #include "ast/expr_abstract.h"
 #include "ast/rewriter/expr_safe_replace.h"
+#include <iostream>
 
 static expr_ref parse_fml(ast_manager& m, char const* str) {
     expr_ref result(m);
diff --git a/src/test/quant_solve.cpp b/src/test/quant_solve.cpp
index fb89d1c8a10..08c857809a1 100644
--- a/src/test/quant_solve.cpp
+++ b/src/test/quant_solve.cpp
@@ -18,6 +18,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "model/model_smt2_pp.h"
 #include "parsers/smt2/smt2parser.h"
 #include "ast/rewriter/var_subst.h"
+#include <iostream>
 
 static void validate_quant_solution(ast_manager& m, expr* fml, expr* guard, qe::def_vector const& defs) {
     // verify:
diff --git a/src/test/rcf.cpp b/src/test/rcf.cpp
index c577cba4065..9b98d9e83a7 100644
--- a/src/test/rcf.cpp
+++ b/src/test/rcf.cpp
@@ -19,6 +19,7 @@ Module Name:
 #include "math/realclosure/realclosure.h"
 #include "math/realclosure/mpz_matrix.h"
 #include "util/rlimit.h"
+#include <iostream>
 
 static void tst1() {
     unsynch_mpq_manager qm;
diff --git a/src/test/sat_local_search.cpp b/src/test/sat_local_search.cpp
index 7ba9e61f762..525c12f2559 100644
--- a/src/test/sat_local_search.cpp
+++ b/src/test/sat_local_search.cpp
@@ -3,6 +3,7 @@
 #include "util/cancel_eh.h"
 #include "util/scoped_ctrl_c.h"
 #include "util/scoped_timer.h"
+#include <iostream>
 
 static bool build_instance(char const * filename, sat::solver& s, sat::local_search& local_search)
 {
diff --git a/src/test/sat_lookahead.cpp b/src/test/sat_lookahead.cpp
index 23c4a4738ec..24dd7e9196f 100644
--- a/src/test/sat_lookahead.cpp
+++ b/src/test/sat_lookahead.cpp
@@ -3,6 +3,7 @@
 #include "util/statistics.h"
 #include "sat/sat_lookahead.h"
 #include "sat/dimacs.h"
+#include <iostream>
 
 static void display_model(sat::model const & m) {
     for (unsigned i = 1; i < m.size(); i++) {
diff --git a/src/test/sat_user_scope.cpp b/src/test/sat_user_scope.cpp
index aeba0bf04a9..c3013cf824a 100644
--- a/src/test/sat_user_scope.cpp
+++ b/src/test/sat_user_scope.cpp
@@ -6,6 +6,7 @@ Copyright (c) 2015 Microsoft Corporation
 
 #include "sat/sat_solver.h"
 #include "util/util.h"
+#include <iostream>
 
 typedef sat::literal_vector clause_t;
 typedef vector<clause_t> clauses_t;
diff --git a/src/test/scoped_timer.cpp b/src/test/scoped_timer.cpp
index ff9d52b0612..742ea26521e 100644
--- a/src/test/scoped_timer.cpp
+++ b/src/test/scoped_timer.cpp
@@ -9,6 +9,7 @@
 #include "util/trace.h"
 #include <thread>
 #include <atomic>
+#include <iostream>
 
 class test_scoped_eh : public event_handler {
     std::atomic<bool> m_called = false;
diff --git a/src/test/simplex.cpp b/src/test/simplex.cpp
index 5c52642bd58..2e59b41719d 100644
--- a/src/test/simplex.cpp
+++ b/src/test/simplex.cpp
@@ -11,6 +11,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "util/vector.h"
 #include "util/rational.h"
 #include "util/rlimit.h"
+#include <iostream>
 
 #define R rational
 typedef simplex::simplex<simplex::mpz_ext> Simplex;
diff --git a/src/test/solver_pool.cpp b/src/test/solver_pool.cpp
index 4a2e533bff6..025106ad1e8 100644
--- a/src/test/solver_pool.cpp
+++ b/src/test/solver_pool.cpp
@@ -1,6 +1,7 @@
 #include "ast/reg_decl_plugins.h"
 #include "solver/solver_pool.h"
 #include "smt/smt_solver.h"
+#include <iostream>
 
 void tst_solver_pool() {
     ast_manager m;
diff --git a/src/test/sorting_network.cpp b/src/test/sorting_network.cpp
index b86f6ad8714..cd22ac9ae6b 100644
--- a/src/test/sorting_network.cpp
+++ b/src/test/sorting_network.cpp
@@ -14,6 +14,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "model/model_smt2_pp.h"
 #include "smt/smt_kernel.h"
 #include "smt/params/smt_params.h"
+#include <iostream>
 
 struct ast_ext {
     ast_manager& m;
diff --git a/src/test/substitution.cpp b/src/test/substitution.cpp
index 9b28927fc50..77087c84cb7 100644
--- a/src/test/substitution.cpp
+++ b/src/test/substitution.cpp
@@ -12,6 +12,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "ast/ast_pp.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/reg_decl_plugins.h"
+#include <iostream>
 
 void tst_substitution()
 {
diff --git a/src/test/tbv.cpp b/src/test/tbv.cpp
index c921551bd01..6107fad85f9 100644
--- a/src/test/tbv.cpp
+++ b/src/test/tbv.cpp
@@ -5,6 +5,7 @@ Copyright (c) 2015 Microsoft Corporation
 --*/
 
 #include "muz/rel/tbv.h"
+#include <iostream>
 
 static void tst1(unsigned num_bits) {
     tbv_manager m(num_bits);
diff --git a/src/test/theory_dl.cpp b/src/test/theory_dl.cpp
index 5b11069aadf..ad77195d52e 100644
--- a/src/test/theory_dl.cpp
+++ b/src/test/theory_dl.cpp
@@ -10,6 +10,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "ast/reg_decl_plugins.h"
 #include "smt/smt_context.h"
 #include "model/model_v2_pp.h"
+#include <iostream>
 
 void tst_theory_dl() {
     ast_manager m;
diff --git a/src/test/theory_pb.cpp b/src/test/theory_pb.cpp
index a6ccf733d02..72a48fa2ae8 100644
--- a/src/test/theory_pb.cpp
+++ b/src/test/theory_pb.cpp
@@ -10,6 +10,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "ast/reg_decl_plugins.h"
 #include "smt/theory_pb.h"
 #include "ast/rewriter/th_rewriter.h"
+#include <iostream>
 
 static unsigned populate_literals(unsigned k, smt::literal_vector& lits) {
     ENSURE(k < (1u << lits.size()));
diff --git a/src/test/total_order.cpp b/src/test/total_order.cpp
index a2ee234dba9..5f4ffbcad48 100644
--- a/src/test/total_order.cpp
+++ b/src/test/total_order.cpp
@@ -19,6 +19,7 @@ Revision History:
 
 #include "util/total_order.h"
 #include "util/timeit.h"
+#include <iostream>
 
 static void tst1() {
     uint_total_order to;
diff --git a/src/test/trigo.cpp b/src/test/trigo.cpp
index 68680016250..f03d5b3dab1 100644
--- a/src/test/trigo.cpp
+++ b/src/test/trigo.cpp
@@ -24,6 +24,7 @@ Revision History:
 #include "util/debug.h"
 #include "test/im_float_config.h"
 #include "util/rlimit.h"
+#include <iostream>
 
 #define PREC 100000
 
diff --git a/src/test/udoc_relation.cpp b/src/test/udoc_relation.cpp
index 0b49567b050..91e6076793f 100644
--- a/src/test/udoc_relation.cpp
+++ b/src/test/udoc_relation.cpp
@@ -22,7 +22,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "muz/rel/rel_context.h"
 #include "ast/bv_decl_plugin.h"
 #include "muz/rel/check_relation.h"
-
+#include <iostream>
 
 class udoc_tester {
     typedef datalog::relation_base relation_base;
diff --git a/src/test/uint_set.cpp b/src/test/uint_set.cpp
index 656eaf1b3e2..f0c170860fa 100644
--- a/src/test/uint_set.cpp
+++ b/src/test/uint_set.cpp
@@ -19,6 +19,7 @@ Revision History:
 
 #include "util/uint_set.h"
 #include "util/vector.h"
+#include <iostream>
 
 static void tst1(unsigned n) {
     uint_set       s1;
diff --git a/src/test/upolynomial.cpp b/src/test/upolynomial.cpp
index a020e104f48..aee3086ae23 100644
--- a/src/test/upolynomial.cpp
+++ b/src/test/upolynomial.cpp
@@ -19,6 +19,7 @@ Module Name:
 #include "math/polynomial/upolynomial.h"
 #include "util/timeit.h"
 #include "util/rlimit.h"
+#include <iostream>
 
 static void tst1() {
     reslimit rl;
diff --git a/src/test/value_generator.cpp b/src/test/value_generator.cpp
index ecde5885560..082a2aeba04 100644
--- a/src/test/value_generator.cpp
+++ b/src/test/value_generator.cpp
@@ -4,6 +4,7 @@
 #include "ast/datatype_decl_plugin.h"
 #include "ast/seq_decl_plugin.h"
 #include "ast/array_decl_plugin.h"
+#include <iostream>
 
 static void list(unsigned bound, ast_manager& m, sort* s) {
     value_generator gen(m);
diff --git a/src/test/value_sweep.cpp b/src/test/value_sweep.cpp
index 015a8be7cf2..7283c8e9311 100644
--- a/src/test/value_sweep.cpp
+++ b/src/test/value_sweep.cpp
@@ -3,6 +3,7 @@
 #include "ast/ast_pp.h"
 #include "ast/seq_decl_plugin.h"
 #include "ast/array_decl_plugin.h"
+#include <iostream>
 
 void tst_value_sweep() {
     ast_manager m;
diff --git a/src/test/var_subst.cpp b/src/test/var_subst.cpp
index 12646798fe0..a39c0e7f1cf 100644
--- a/src/test/var_subst.cpp
+++ b/src/test/var_subst.cpp
@@ -23,6 +23,7 @@ Revision History:
 #include "ast/array_decl_plugin.h"
 #include "ast/for_each_expr.h"
 #include "ast/reg_decl_plugins.h"
+#include <iostream>
 
 namespace find_q {
     struct proc {
diff --git a/src/test/vector.cpp b/src/test/vector.cpp
index c9a93dee40f..fe0b50ddbc6 100644
--- a/src/test/vector.cpp
+++ b/src/test/vector.cpp
@@ -17,6 +17,7 @@ Revision History:
 
 --*/
 #include "util/vector.h"
+#include <iostream>
 
 static void tst1() {
     svector<int> v1;
diff --git a/src/test/zstring.cpp b/src/test/zstring.cpp
index ffeda7fcef9..bd79d873f68 100644
--- a/src/test/zstring.cpp
+++ b/src/test/zstring.cpp
@@ -1,6 +1,7 @@
 #include "util/debug.h"
 #include "util/trace.h"
 #include "util/zstring.h"
+#include <iostream>
 
 // Encode and check for roundtrip all printable ASCII characters.
 static void tst_ascii_roundtrip() {