diff --git a/src/test/algebraic.cpp b/src/test/algebraic.cpp index 5c91623d0..371997c02 100644 --- a/src/test/algebraic.cpp +++ b/src/test/algebraic.cpp @@ -20,6 +20,7 @@ Notes: #include "math/polynomial/polynomial_var2value.h" #include "util/mpbq.h" #include "util/rlimit.h" +#include 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 da49e58dc..d79f09cc3 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 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 63a6838d4..639fda765 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 typedef rational numeral; typedef vector row; diff --git a/src/test/bdd.cpp b/src/test/bdd.cpp index 7c7af2fb4..d08d10a11 100644 --- a/src/test/bdd.cpp +++ b/src/test/bdd.cpp @@ -1,4 +1,5 @@ #include "math/dd/dd_bdd.h" +#include namespace dd { static void test1() { diff --git a/src/test/bits.cpp b/src/test/bits.cpp index 2bef6a0ba..2fc1efe0c 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 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 8e4dadf99..773509aba 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 typedef chashtable > int_table; typedef cmap > int_map; diff --git a/src/test/cube_clause.cpp b/src/test/cube_clause.cpp index 0c783277b..920c5c57c 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 void tst_cube_clause() { ast_manager m; diff --git a/src/test/datalog_parser.cpp b/src/test/datalog_parser.cpp index ca5e94f75..ee69bff8b 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 using namespace datalog; diff --git a/src/test/dl_query.cpp b/src/test/dl_query.cpp index 2181f97ad..34dc7e020 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 using namespace datalog; diff --git a/src/test/dl_table.cpp b/src/test/dl_table.cpp index b3082cc6a..0f429d223 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 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 4d84ff964..f1b5cf2ce 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 static void tst_doc1(unsigned n) { doc_manager m(n); diff --git a/src/test/egraph.cpp b/src/test/egraph.cpp index 508384f8f..a3c61abad 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 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 9bc2aecec..4fb85960d 100644 --- a/src/test/escaped.cpp +++ b/src/test/escaped.cpp @@ -17,6 +17,7 @@ Revision History: --*/ #include "util/util.h" +#include 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 3b74535e7..c66681c1b 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 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 7831a31cf..211cf6013 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 static void tst1() { hwf_manager hm; diff --git a/src/test/factor_rewriter.cpp b/src/test/factor_rewriter.cpp index 486221e5b..223527c11 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 void tst_factor_rewriter() { ast_manager m; diff --git a/src/test/get_consequences.cpp b/src/test/get_consequences.cpp index 0e5124d58..d8c070b6d 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 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 b6f651633..a86e0e741 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 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 06446e8e9..93c58374e 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 #include +#include #include 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 6d4dcc26f..aea819d7a 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 void tst_horn_subsume_model_converter() { ast_manager m; diff --git a/src/test/hwf.cpp b/src/test/hwf.cpp index 697673473..8a019ec02 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 static void bug_set_double() { hwf_manager m; diff --git a/src/test/interval.cpp b/src/test/interval.cpp index 5180912f5..f289871de 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 template class interval_manager; typedef im_default_config::interval interval; diff --git a/src/test/karr.cpp b/src/test/karr.cpp index cf5867324..2ec13ecc2 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 /* Test generation of linear congruences a la Karr. diff --git a/src/test/model2expr.cpp b/src/test/model2expr.cpp index 41047825c..5163abade 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 void tst_model2expr() { ast_manager m; diff --git a/src/test/model_based_opt.cpp b/src/test/model_based_opt.cpp index 1bae7435f..b307f85e4 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 typedef opt::model_based_opt::var var; diff --git a/src/test/model_evaluator.cpp b/src/test/model_evaluator.cpp index 3e1c95617..f4a64d4dc 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 void tst_model_evaluator() { ast_manager m; diff --git a/src/test/model_retrieval.cpp b/src/test/model_retrieval.cpp index e0fd28088..415a5772c 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 void tst_model_retrieval() { diff --git a/src/test/mpbq.cpp b/src/test/mpbq.cpp index 4dc92d80d..16dead4cf 100644 --- a/src/test/mpbq.cpp +++ b/src/test/mpbq.cpp @@ -17,6 +17,7 @@ Revision History: --*/ #include "util/mpbq.h" +#include static void tst1() { unsynch_mpz_manager zm; diff --git a/src/test/mpff.cpp b/src/test/mpff.cpp index 83c500b49..b03cc5f2e 100644 --- a/src/test/mpff.cpp +++ b/src/test/mpff.cpp @@ -18,6 +18,7 @@ Revision History: --*/ #include #include +#include #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 f5cf7e2fb..7752157fd 100644 --- a/src/test/mpfx.cpp +++ b/src/test/mpfx.cpp @@ -17,6 +17,7 @@ Revision History: --*/ #include "util/mpfx.h" +#include static void tst1() { mpfx_manager m; diff --git a/src/test/mpq.cpp b/src/test/mpq.cpp index 6294a97f7..6c15c8556 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 static void tst0() { synch_mpq_manager m; diff --git a/src/test/mpz.cpp b/src/test/mpz.cpp index fc2177ca2..694f13e96 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 static void tst1() { synch_mpz_manager m; diff --git a/src/test/nlarith_util.cpp b/src/test/nlarith_util.cpp index 4769c1591..d6105cf82 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 void tst_nlarith_util() { ast_manager M; diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp index 44d4120fe..9274938ef 100644 --- a/src/test/nlsat.cpp +++ b/src/test/nlsat.cpp @@ -24,6 +24,7 @@ Notes: #include "nlsat/nlsat_explain.h" #include "math/polynomial/polynomial_cache.h" #include "util/rlimit.h" +#include 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 751f6fdbe..bc2f9fb13 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 static void tst1() { ext_numeral inf(true); diff --git a/src/test/parray.cpp b/src/test/parray.cpp index 6aef4f359..7e6b78cd8 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 template struct int_parray_config { diff --git a/src/test/pb2bv.cpp b/src/test/pb2bv.cpp index 169df85ad..8772fec92 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 static void test1() { ast_manager m; diff --git a/src/test/pdd.cpp b/src/test/pdd.cpp index b10abb891..b0cbb657c 100644 --- a/src/test/pdd.cpp +++ b/src/test/pdd.cpp @@ -1,4 +1,5 @@ #include "math/dd/dd_pdd.h" +#include namespace dd { diff --git a/src/test/pdd_solver.cpp b/src/test/pdd_solver.cpp index 7a1c07131..a86504266 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 namespace dd { void print_eqs(ptr_vector const& eqs) { diff --git a/src/test/polynomial.cpp b/src/test/polynomial.cpp index 091d03c61..f259c4234 100644 --- a/src/test/polynomial.cpp +++ b/src/test/polynomial.cpp @@ -22,6 +22,7 @@ Notes: #include "math/polynomial/polynomial_cache.h" #include "math/polynomial/linear_eq_solver.h" #include "util/rlimit.h" +#include static void tst1() { std::cout << "\n----- Basic testing -------\n"; diff --git a/src/test/polynorm.cpp b/src/test/polynorm.cpp index 58481938b..80ff74904 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 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 3a63b805a..a60418777 100644 --- a/src/test/prime_generator.cpp +++ b/src/test/prime_generator.cpp @@ -18,6 +18,7 @@ Notes: --*/ #include "util/mpz.h" #include "util/prime_generator.h" +#include void tst_prime_generator() { unsynch_mpz_manager m; diff --git a/src/test/proof_checker.cpp b/src/test/proof_checker.cpp index 7a9b619cd..bc3dd39ad 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 void tst_checker1() { ast_manager m(PGM_ENABLED); diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp index ab268a651..859d7f2e5 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 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 fb89d1c8a..08c857809 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 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 c577cba40..9b98d9e83 100644 --- a/src/test/rcf.cpp +++ b/src/test/rcf.cpp @@ -19,6 +19,7 @@ Notes: #include "math/realclosure/realclosure.h" #include "math/realclosure/mpz_matrix.h" #include "util/rlimit.h" +#include static void tst1() { unsynch_mpq_manager qm; diff --git a/src/test/sat_local_search.cpp b/src/test/sat_local_search.cpp index 7ba9e61f7..525c12f25 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 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 23c4a4738..24dd7e919 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 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 aeba0bf04..c3013cf82 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 typedef sat::literal_vector clause_t; typedef vector clauses_t; diff --git a/src/test/scoped_timer.cpp b/src/test/scoped_timer.cpp index ff9d52b06..742ea2652 100644 --- a/src/test/scoped_timer.cpp +++ b/src/test/scoped_timer.cpp @@ -9,6 +9,7 @@ #include "util/trace.h" #include #include +#include class test_scoped_eh : public event_handler { std::atomic m_called = false; diff --git a/src/test/simplex.cpp b/src/test/simplex.cpp index 5c52642bd..2e59b4171 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 #define R rational typedef simplex::simplex Simplex; diff --git a/src/test/solver_pool.cpp b/src/test/solver_pool.cpp index 4a2e533bf..025106ad1 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 void tst_solver_pool() { ast_manager m; diff --git a/src/test/sorting_network.cpp b/src/test/sorting_network.cpp index b86f6ad87..cd22ac9ae 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 struct ast_ext { ast_manager& m; diff --git a/src/test/substitution.cpp b/src/test/substitution.cpp index 9b28927fc..77087c84c 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 void tst_substitution() { diff --git a/src/test/tbv.cpp b/src/test/tbv.cpp index c921551bd..6107fad85 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 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 5b11069aa..ad77195d5 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 void tst_theory_dl() { ast_manager m; diff --git a/src/test/theory_pb.cpp b/src/test/theory_pb.cpp index a6ccf733d..72a48fa2a 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 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 a2ee234db..5f4ffbcad 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 static void tst1() { uint_total_order to; diff --git a/src/test/trigo.cpp b/src/test/trigo.cpp index 686800162..f03d5b3da 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 #define PREC 100000 diff --git a/src/test/udoc_relation.cpp b/src/test/udoc_relation.cpp index 0b49567b0..91e607679 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 class udoc_tester { typedef datalog::relation_base relation_base; diff --git a/src/test/uint_set.cpp b/src/test/uint_set.cpp index 656eaf1b3..f0c170860 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 static void tst1(unsigned n) { uint_set s1; diff --git a/src/test/upolynomial.cpp b/src/test/upolynomial.cpp index a020e104f..aee3086ae 100644 --- a/src/test/upolynomial.cpp +++ b/src/test/upolynomial.cpp @@ -19,6 +19,7 @@ Notes: #include "math/polynomial/upolynomial.h" #include "util/timeit.h" #include "util/rlimit.h" +#include static void tst1() { reslimit rl; diff --git a/src/test/value_generator.cpp b/src/test/value_generator.cpp index ecde58855..082a2aeba 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 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 015a8be7c..7283c8e93 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 void tst_value_sweep() { ast_manager m; diff --git a/src/test/var_subst.cpp b/src/test/var_subst.cpp index 12646798f..a39c0e7f1 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 namespace find_q { struct proc { diff --git a/src/test/vector.cpp b/src/test/vector.cpp index c9a93dee4..fe0b50ddb 100644 --- a/src/test/vector.cpp +++ b/src/test/vector.cpp @@ -17,6 +17,7 @@ Revision History: --*/ #include "util/vector.h" +#include static void tst1() { svector v1; diff --git a/src/test/zstring.cpp b/src/test/zstring.cpp index ffeda7fce..bd79d873f 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 // Encode and check for roundtrip all printable ASCII characters. static void tst_ascii_roundtrip() {