diff --git a/src/api/z3_logger.h b/src/api/z3_logger.h
index 646209575..2c95e18ca 100644
--- a/src/api/z3_logger.h
+++ b/src/api/z3_logger.h
@@ -16,6 +16,8 @@ Author:
 Notes:
     
 --*/
+#pragma once
+
 #include "util/symbol.h"
 
 void R();
diff --git a/src/api/z3_macros.h b/src/api/z3_macros.h
index 08756cf15..5f8659379 100644
--- a/src/api/z3_macros.h
+++ b/src/api/z3_macros.h
@@ -3,7 +3,7 @@
 Copyright (c) 2015 Microsoft Corporation
 
 --*/
-
+#pragma once
 
 #ifndef Z3_API
 # ifdef __GNUC__
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
index ae125a0ad..dc1df22a3 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
@@ -16,6 +16,8 @@ Author:
 Revision History:
 
 --*/
+#pragma once
+
 #include "util/rational.h"
 #include "util/common_msgs.h"
 #include "ast/rewriter/bit_blaster/bit_blaster_tpl.h"
diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h
index eb72ddd67..0a17fc375 100644
--- a/src/ast/rewriter/poly_rewriter_def.h
+++ b/src/ast/rewriter/poly_rewriter_def.h
@@ -16,6 +16,7 @@ Author:
 Notes:
 
 --*/
+#pragma once
 
 #include "util/container_util.h"
 #include "ast/rewriter/poly_rewriter.h"
diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index 4bf829be6..e9b9c316a 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -16,6 +16,8 @@ Author:
 Notes:
 
 --*/
+#pragma once
+
 #include "ast/rewriter/rewriter.h"
 #include "ast/ast_smt2_pp.h"
 #include "ast/ast_ll_pp.h"
diff --git a/src/cmd_context/extra_cmds/subpaving_cmds.h b/src/cmd_context/extra_cmds/subpaving_cmds.h
index 33ed347b7..651d5b161 100644
--- a/src/cmd_context/extra_cmds/subpaving_cmds.h
+++ b/src/cmd_context/extra_cmds/subpaving_cmds.h
@@ -15,6 +15,7 @@ Author:
 Notes:
 
 --*/
+#pragma once
 
 class cmd_context;
 
diff --git a/src/math/dd/pdd_eval.h b/src/math/dd/pdd_eval.h
index f7682927f..9872935cf 100644
--- a/src/math/dd/pdd_eval.h
+++ b/src/math/dd/pdd_eval.h
@@ -17,6 +17,8 @@ Author:
 Revision History:
 
 --*/
+#pragma once
+
 #include "math/dd/dd_pdd.h"
 
 namespace dd {
diff --git a/src/math/dd/pdd_interval.h b/src/math/dd/pdd_interval.h
index d8e2b8db1..c5b4c9e1c 100644
--- a/src/math/dd/pdd_interval.h
+++ b/src/math/dd/pdd_interval.h
@@ -17,6 +17,8 @@ Author:
 Revision History:
 
 --*/
+#pragma once
+
 #include "math/dd/dd_pdd.h"
 #include "math/interval/dep_intervals.h"
 
diff --git a/src/math/lp/binary_heap_priority_queue_def.h b/src/math/lp/binary_heap_priority_queue_def.h
index c17d70fb2..0e640d949 100644
--- a/src/math/lp/binary_heap_priority_queue_def.h
+++ b/src/math/lp/binary_heap_priority_queue_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include "util/vector.h"
 #include "math/lp/binary_heap_priority_queue.h"
 namespace lp {
diff --git a/src/math/lp/binary_heap_upair_queue_def.h b/src/math/lp/binary_heap_upair_queue_def.h
index a74f9e46a..65485a6eb 100644
--- a/src/math/lp/binary_heap_upair_queue_def.h
+++ b/src/math/lp/binary_heap_upair_queue_def.h
@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+#pragma once
 
 #include <set>
 #include "math/lp/lp_utils.h"
diff --git a/src/math/lp/core_solver_pretty_printer_def.h b/src/math/lp/core_solver_pretty_printer_def.h
index 2f54b175a..23417b691 100644
--- a/src/math/lp/core_solver_pretty_printer_def.h
+++ b/src/math/lp/core_solver_pretty_printer_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include <limits>
 #include <string>
 #include <algorithm>
diff --git a/src/math/lp/dense_matrix_def.h b/src/math/lp/dense_matrix_def.h
index f781dbf8f..8eb9ad5dd 100644
--- a/src/math/lp/dense_matrix_def.h
+++ b/src/math/lp/dense_matrix_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include "math/lp/lp_settings.h"
 #ifdef Z3DEBUG
 #include "util/vector.h"
diff --git a/src/math/lp/indexed_vector_def.h b/src/math/lp/indexed_vector_def.h
index 443ca160e..0e25ee271 100644
--- a/src/math/lp/indexed_vector_def.h
+++ b/src/math/lp/indexed_vector_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include "util/vector.h"
 #include "math/lp/indexed_vector.h"
 #include "math/lp/lp_settings.h"
diff --git a/src/math/lp/lar_core_solver_def.h b/src/math/lp/lar_core_solver_def.h
index f20aa7e6b..939a05114 100644
--- a/src/math/lp/lar_core_solver_def.h
+++ b/src/math/lp/lar_core_solver_def.h
@@ -9,6 +9,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include <string>
 #include "util/vector.h"
 #include "math/lp/lar_core_solver.h"
diff --git a/src/math/lp/lp_core_solver_base_def.h b/src/math/lp/lp_core_solver_base_def.h
index 42c2ddcf7..c1b64492b 100644
--- a/src/math/lp/lp_core_solver_base_def.h
+++ b/src/math/lp/lp_core_solver_base_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include <set>
 #include <string>
 #include "util/vector.h"
diff --git a/src/math/lp/lp_dual_core_solver_def.h b/src/math/lp/lp_dual_core_solver_def.h
index 4a847fe85..b42d644af 100644
--- a/src/math/lp/lp_dual_core_solver_def.h
+++ b/src/math/lp/lp_dual_core_solver_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include <algorithm>
 #include <string>
 #include "util/vector.h"
diff --git a/src/math/lp/lp_dual_simplex_def.h b/src/math/lp/lp_dual_simplex_def.h
index c21429c88..8af9d87c1 100644
--- a/src/math/lp/lp_dual_simplex_def.h
+++ b/src/math/lp/lp_dual_simplex_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include "math/lp/lp_dual_simplex.h"
 namespace lp{
 
diff --git a/src/math/lp/lp_primal_core_solver_def.h b/src/math/lp/lp_primal_core_solver_def.h
index 75eff208a..7b5dec945 100644
--- a/src/math/lp/lp_primal_core_solver_def.h
+++ b/src/math/lp/lp_primal_core_solver_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include <list>
 #include "util/vector.h"
 #include <fstream>
diff --git a/src/math/lp/lp_primal_core_solver_tableau_def.h b/src/math/lp/lp_primal_core_solver_tableau_def.h
index 03f07115b..46297a63e 100644
--- a/src/math/lp/lp_primal_core_solver_tableau_def.h
+++ b/src/math/lp/lp_primal_core_solver_tableau_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 // this is a part of lp_primal_core_solver that deals with the tableau
 #include "math/lp/lp_primal_core_solver.h"
 namespace lp {
diff --git a/src/math/lp/lp_primal_simplex_def.h b/src/math/lp/lp_primal_simplex_def.h
index e805ecc88..7ffe819b2 100644
--- a/src/math/lp/lp_primal_simplex_def.h
+++ b/src/math/lp/lp_primal_simplex_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include <string>
 #include "util/vector.h"
 #include "math/lp/lp_primal_simplex.h"
diff --git a/src/math/lp/lp_settings_def.h b/src/math/lp/lp_settings_def.h
index 4c783049c..2aba35946 100644
--- a/src/math/lp/lp_settings_def.h
+++ b/src/math/lp/lp_settings_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include <cmath>
 #include <string>
 #include "util/vector.h"
diff --git a/src/math/lp/lp_solver_def.h b/src/math/lp/lp_solver_def.h
index 4b5bc6db7..191832a24 100644
--- a/src/math/lp/lp_solver_def.h
+++ b/src/math/lp/lp_solver_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include <string>
 #include <algorithm>
 #include "util/vector.h"
diff --git a/src/math/lp/lu_def.h b/src/math/lp/lu_def.h
index df0f53730..80c9cdf0e 100644
--- a/src/math/lp/lu_def.h
+++ b/src/math/lp/lu_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include <string>
 #include <algorithm>
 #include <set>
diff --git a/src/math/lp/matrix_def.h b/src/math/lp/matrix_def.h
index 8dba9d0b8..95810bd5a 100644
--- a/src/math/lp/matrix_def.h
+++ b/src/math/lp/matrix_def.h
@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+#pragma once
 
 #include <cmath>
 #include <string>
diff --git a/src/math/lp/permutation_matrix_def.h b/src/math/lp/permutation_matrix_def.h
index c6ad20a39..703830ffc 100644
--- a/src/math/lp/permutation_matrix_def.h
+++ b/src/math/lp/permutation_matrix_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include "util/vector.h"
 #include "math/lp/permutation_matrix.h"
 namespace lp {
diff --git a/src/math/lp/random_updater_def.h b/src/math/lp/random_updater_def.h
index 25ef6f82f..7d167a4a0 100644
--- a/src/math/lp/random_updater_def.h
+++ b/src/math/lp/random_updater_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include "math/lp/random_updater.h"
 #include "math/lp/static_matrix.h"
 #include "math/lp/lar_solver.h"
diff --git a/src/math/lp/row_eta_matrix_def.h b/src/math/lp/row_eta_matrix_def.h
index 817d39481..faac5c6fe 100644
--- a/src/math/lp/row_eta_matrix_def.h
+++ b/src/math/lp/row_eta_matrix_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include "util/vector.h"
 #include "math/lp/row_eta_matrix.h"
 namespace lp {
diff --git a/src/math/lp/scaler_def.h b/src/math/lp/scaler_def.h
index c05b25a16..8604a67a1 100644
--- a/src/math/lp/scaler_def.h
+++ b/src/math/lp/scaler_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include <algorithm>
 #include "math/lp/scaler.h"
 #include "math/lp/numeric_pair.h"
diff --git a/src/math/lp/square_dense_submatrix_def.h b/src/math/lp/square_dense_submatrix_def.h
index 8b565f92e..3a9006b4d 100644
--- a/src/math/lp/square_dense_submatrix_def.h
+++ b/src/math/lp/square_dense_submatrix_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include "util/vector.h"
 #include "math/lp/square_dense_submatrix.h"
 namespace lp {
diff --git a/src/math/lp/square_sparse_matrix_def.h b/src/math/lp/square_sparse_matrix_def.h
index 0a2cffd61..3533ba066 100644
--- a/src/math/lp/square_sparse_matrix_def.h
+++ b/src/math/lp/square_sparse_matrix_def.h
@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+#pragma once
 
 #include "util/vector.h"
 #include "math/lp/square_sparse_matrix.h"
diff --git a/src/math/lp/static_matrix_def.h b/src/math/lp/static_matrix_def.h
index 45d5d6d89..af2eac360 100644
--- a/src/math/lp/static_matrix_def.h
+++ b/src/math/lp/static_matrix_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include "util/vector.h"
 #include <utility>
 #include <set>
diff --git a/src/math/subpaving/subpaving_t_def.h b/src/math/subpaving/subpaving_t_def.h
index c31e920ab..89f6dad0f 100644
--- a/src/math/subpaving/subpaving_t_def.h
+++ b/src/math/subpaving/subpaving_t_def.h
@@ -16,6 +16,8 @@ Author:
 Revision History:
 
 --*/
+#pragma once
+
 #include "math/subpaving/subpaving_t.h"
 #include "math/interval/interval_def.h"
 #include "util/buffer.h"
diff --git a/src/muz/base/dl_boogie_proof.h b/src/muz/base/dl_boogie_proof.h
index ed2f5a801..5107d9529 100644
--- a/src/muz/base/dl_boogie_proof.h
+++ b/src/muz/base/dl_boogie_proof.h
@@ -3,6 +3,7 @@
 Copyright (c) 2015 Microsoft Corporation
 
 --*/
+#pragma once
 
 /**
 
diff --git a/src/muz/spacer/spacer_legacy_frames.h b/src/muz/spacer/spacer_legacy_frames.h
index 7ff4b6fad..cb78ec6a9 100644
--- a/src/muz/spacer/spacer_legacy_frames.h
+++ b/src/muz/spacer/spacer_legacy_frames.h
@@ -5,6 +5,7 @@
 
   Notes: this file is included from the middle of spacer_context.h
 */
+#pragma once
 
 class legacy_frames
 {
diff --git a/src/sat/sat_cutset_compute_shift.h b/src/sat/sat_cutset_compute_shift.h
index 7a9aff612..45d2e1de8 100644
--- a/src/sat/sat_cutset_compute_shift.h
+++ b/src/sat/sat_cutset_compute_shift.h
@@ -18,6 +18,7 @@
     The truth table covers up to 6 inputs, which fits in 64 bits.
 
   --*/
+#pragma once
 
 static uint64_t compute_shift(uint64_t x, unsigned code) {
     switch (code) {
diff --git a/src/shell/options.h b/src/shell/options.h
index ee1de00fb..39fe2fe8f 100644
--- a/src/shell/options.h
+++ b/src/shell/options.h
@@ -3,6 +3,7 @@
 Copyright (c) 2015 Microsoft Corporation
 
 --*/
+#pragma once
 
 
 /**
diff --git a/src/smt/database.h b/src/smt/database.h
index 3edb87f1f..f1ce25f26 100644
--- a/src/smt/database.h
+++ b/src/smt/database.h
@@ -3,6 +3,7 @@
 Copyright (c) 2015 Microsoft Corporation
 
 --*/
+#pragma once
 
 static char const g_pattern_database[] =
 "(benchmark patterns \n"
diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h
index 2d62bb7ac..f713877b3 100644
--- a/src/smt/theory_pb.h
+++ b/src/smt/theory_pb.h
@@ -19,6 +19,7 @@ Notes:
     It performs unit propagation and switches to creating
     sorting circuits if it keeps having to propagate (create new clauses).
 --*/
+#pragma once
 
 #include "smt/smt_theory.h"
 #include "ast/pb_decl_plugin.h"
diff --git a/src/test/lp/argument_parser.h b/src/test/lp/argument_parser.h
index f2a74f122..12ab02831 100644
--- a/src/test/lp/argument_parser.h
+++ b/src/test/lp/argument_parser.h
@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+#pragma once
 
 #include <unordered_map>
 #include <vector>
diff --git a/src/test/lp/gomory_test.h b/src/test/lp/gomory_test.h
index c7b0002cd..890ff90e3 100644
--- a/src/test/lp/gomory_test.h
+++ b/src/test/lp/gomory_test.h
@@ -1,3 +1,5 @@
+#pragma once
+
 namespace lp {
 #include "math/lp/lp_utils.h"
 struct gomory_test {
diff --git a/src/util/max_cliques.h b/src/util/max_cliques.h
index 2841db609..de68b6b10 100644
--- a/src/util/max_cliques.h
+++ b/src/util/max_cliques.h
@@ -17,6 +17,7 @@ Notes:
 
 
 --*/
+#pragma once
 
 #include "util/vector.h"
 #include "util/uint_set.h"