Rename public and private headers in src/include. (#6352)

54 files changed, 55 insertions, 54 deletions

diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h
index 7ed76ff05..f7266c578 100644
--- a/src/theory/arith/approx_simplex.h
+++ b/src/theory/arith/approx_simplex.h
@@ -16,7 +16,7 @@
  * \todo document this file
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #pragma once
 #include <vector>
diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h
index 28385f8ac..4d181b39f 100644
--- a/src/theory/arith/arith_ite_utils.h
+++ b/src/theory/arith/arith_ite_utils.h
@@ -18,7 +18,7 @@
 
 // Pass 1: label the ite as (constant) or (+ constant variable)
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__ARITH__ARITH_ITE_UTILS_H
 #define CVC5__THEORY__ARITH__ARITH_ITE_UTILS_H
diff --git a/src/theory/arith/arith_msum.h b/src/theory/arith/arith_msum.h
index bc5cb15dd..3c205c9b7 100644
--- a/src/theory/arith/arith_msum.h
+++ b/src/theory/arith/arith_msum.h
@@ -13,7 +13,7 @@
  * Arithmetic utilities regarding monomial sums.
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__ARITH__MSUM_H
 #define CVC5__THEORY__ARITH__MSUM_H
diff --git a/src/theory/arith/arith_preprocess.h b/src/theory/arith/arith_preprocess.h
index cea7d0695..ea24e5066 100644
--- a/src/theory/arith/arith_preprocess.h
+++ b/src/theory/arith/arith_preprocess.h
@@ -13,7 +13,7 @@
  * Arithmetic preprocess.
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__ARITH__ARITH_PREPROCESS_H
 #define CVC5__THEORY__ARITH__ARITH_PREPROCESS_H
diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index d7686658c..e476fbd62 100644
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -16,7 +16,7 @@
  * See theory/arith/normal_form.h for more information.
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__ARITH__ARITH_REWRITER_H
 #define CVC5__THEORY__ARITH__ARITH_REWRITER_H
diff --git a/src/theory/arith/arith_state.h b/src/theory/arith/arith_state.h
index 688665b65..0aa848f46 100644
--- a/src/theory/arith/arith_state.h
+++ b/src/theory/arith/arith_state.h
@@ -13,7 +13,7 @@
  * Arithmetic theory state.
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__ARITH__ARITH_STATE_H
 #define CVC5__THEORY__ARITH__ARITH_STATE_H
diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h
index 6e01d4a86..053730ec8 100644
--- a/src/theory/arith/arith_static_learner.h
+++ b/src/theory/arith/arith_static_learner.h
@@ -16,7 +16,7 @@
  * \todo document this file
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__ARITH__ARITH_STATIC_LEARNER_H
 #define CVC5__THEORY__ARITH__ARITH_STATIC_LEARNER_H
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index c2b98599d..0c6378bc2 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -13,7 +13,7 @@
  * Common functions for dealing with nodes.
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__ARITH__ARITH_UTILITIES_H
 #define CVC5__THEORY__ARITH__ARITH_UTILITIES_H
diff --git a/src/theory/arith/arithvar.h b/src/theory/arith/arithvar.h
index 0272ade52..b95c39e9e 100644
--- a/src/theory/arith/arithvar.h
+++ b/src/theory/arith/arithvar.h
@@ -18,7 +18,7 @@
  * This file also provides utilities for ArithVars.
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #pragma once
 
diff --git a/src/theory/arith/arithvar_node_map.h b/src/theory/arith/arithvar_node_map.h
index fffc48c2b..c8b7f62a4 100644
--- a/src/theory/arith/arithvar_node_map.h
+++ b/src/theory/arith/arithvar_node_map.h
@@ -16,7 +16,7 @@
  * \todo document this file
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__ARITH__ARITHVAR_NODE_MAP_H
 #define CVC5__THEORY__ARITH__ARITHVAR_NODE_MAP_H
diff --git a/src/theory/arith/attempt_solution_simplex.h b/src/theory/arith/attempt_solution_simplex.h
index 311a70567..25676a8b6 100644
--- a/src/theory/arith/attempt_solution_simplex.h
+++ b/src/theory/arith/attempt_solution_simplex.h
@@ -51,7 +51,7 @@
  *   These are theory valid and are currently turned into lemmas
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #pragma once
 
diff --git a/src/theory/arith/bound_counts.h b/src/theory/arith/bound_counts.h
index 545c1c064..9a707df85 100644
--- a/src/theory/arith/bound_counts.h
+++ b/src/theory/arith/bound_counts.h
@@ -16,7 +16,7 @@
  * \todo document this file
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 #pragma once
 
 #include "base/check.h"
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index b88f48e0c..c8abba880 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -16,7 +16,7 @@
  * \todo document this file
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #pragma once
 
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 856cf719a..bd27c6034 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -74,7 +74,7 @@
  *   proof.
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__ARITH__CONSTRAINT_H
 #define CVC5__THEORY__ARITH__CONSTRAINT_H
diff --git a/src/theory/arith/constraint_forward.h b/src/theory/arith/constraint_forward.h
index f6ceea311..5f0e124fb 100644
--- a/src/theory/arith/constraint_forward.h
+++ b/src/theory/arith/constraint_forward.h
@@ -22,9 +22,10 @@
 #ifndef CVC5__THEORY__ARITH__CONSTRAINT_FORWARD_H
 #define CVC5__THEORY__ARITH__CONSTRAINT_FORWARD_H
 
-#include "cvc4_private.h"
 #include <vector>
 
+#include "cvc5_private.h"
+
 namespace cvc5 {
 namespace theory {
 namespace arith {
diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h
index 86a3a165b..5929bbd5a 100644
--- a/src/theory/arith/cut_log.h
+++ b/src/theory/arith/cut_log.h
@@ -16,7 +16,7 @@
  * \todo document this file
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #pragma once
 
diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h
index fce3aebc8..7872ca01e 100644
--- a/src/theory/arith/delta_rational.h
+++ b/src/theory/arith/delta_rational.h
@@ -16,7 +16,7 @@
  * \todo document this file
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #pragma once
 
diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h
index 4f3a5e604..5e020d66e 100644
--- a/src/theory/arith/dio_solver.h
+++ b/src/theory/arith/dio_solver.h
@@ -13,7 +13,7 @@
  * A Diophantine equation solver for the theory of arithmetic.
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__ARITH__DIO_SOLVER_H
 #define CVC5__THEORY__ARITH__DIO_SOLVER_H
diff --git a/src/theory/arith/dual_simplex.h b/src/theory/arith/dual_simplex.h
index da0a11be8..7113bd329 100644
--- a/src/theory/arith/dual_simplex.h
+++ b/src/theory/arith/dual_simplex.h
@@ -51,7 +51,7 @@
  *   These are theory valid and are currently turned into lemmas
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #pragma once
 
diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h
index 809ca6aaa..21cc557b6 100644
--- a/src/theory/arith/error_set.h
+++ b/src/theory/arith/error_set.h
@@ -16,7 +16,7 @@
  * \todo document this file
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #pragma once
 
diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h
index 5217e988b..6c391393d 100644
--- a/src/theory/arith/fc_simplex.h
+++ b/src/theory/arith/fc_simplex.h
@@ -51,7 +51,7 @@
  *   These are theory valid and are currently turned into lemmas
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #pragma once
 
diff --git a/src/theory/arith/infer_bounds.h b/src/theory/arith/infer_bounds.h
index 4b17b253d..8a65c7c66 100644
--- a/src/theory/arith/infer_bounds.h
+++ b/src/theory/arith/infer_bounds.h
@@ -16,7 +16,7 @@
  * \todo document this file
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #pragma once
 
diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h
index 079f19fc2..287b89851 100644
--- a/src/theory/arith/inference_manager.h
+++ b/src/theory/arith/inference_manager.h
@@ -13,7 +13,7 @@
  * Customized inference manager for the theory of nonlinear arithmetic.
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__ARITH__INFERENCE_MANAGER_H
 #define CVC5__THEORY__ARITH__INFERENCE_MANAGER_H
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index 0f47bc741..e07ed6051 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -26,7 +26,7 @@
  * using both the Tableau and PartialModel.
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #pragma once
 
diff --git a/src/theory/arith/matrix.h b/src/theory/arith/matrix.h
index 4962b865d..7713dd2c3 100644
--- a/src/theory/arith/matrix.h
+++ b/src/theory/arith/matrix.h
@@ -15,7 +15,7 @@
  * This defines Matrix<T>, IntegerEqualityTables and Tableau.
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #pragma once
 
diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h
index eafe979a1..7973fda58 100644
--- a/src/theory/arith/nl/cad/cdcac.h
+++ b/src/theory/arith/nl/cad/cdcac.h
@@ -14,7 +14,7 @@
  * https://arxiv.org/pdf/2003.05633.pdf.
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__ARITH__NL__CAD__CDCAC_H
 #define CVC5__THEORY__ARITH__NL__CAD__CDCAC_H
diff --git a/src/theory/arith/nl/cad/cdcac_utils.h b/src/theory/arith/nl/cad/cdcac_utils.h
index f0f3c357b..8fde21fde 100644
--- a/src/theory/arith/nl/cad/cdcac_utils.h
+++ b/src/theory/arith/nl/cad/cdcac_utils.h
@@ -13,7 +13,7 @@
  * Implements utilities for cdcac.
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__ARITH__NL__CAD__CDCAC_UTILS_H
 #define CVC5__THEORY__ARITH__NL__CAD__CDCAC_UTILS_H
diff --git a/src/theory/arith/nl/cad/constraints.h b/src/theory/arith/nl/cad/constraints.h
index 3655ef5c0..f8a12065f 100644
--- a/src/theory/arith/nl/cad/constraints.h
+++ b/src/theory/arith/nl/cad/constraints.h
@@ -13,7 +13,7 @@
  * Implements a container for CAD constraints.
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__ARITH__NL__CAD__CONSTRAINTS_H
 #define CVC5__THEORY__ARITH__NL__CAD__CONSTRAINTS_H
diff --git a/src/theory/arith/nl/cad/projections.h b/src/theory/arith/nl/cad/projections.h
index 25deb0d0d..129c3515a 100644
--- a/src/theory/arith/nl/cad/projections.h
+++ b/src/theory/arith/nl/cad/projections.h
@@ -13,7 +13,7 @@
  * Implements utilities for CAD projection operators.
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__ARITH__NL__CAD_PROJECTIONS_H
 #define CVC5__THEORY__ARITH__NL__CAD_PROJECTIONS_H
diff --git a/src/theory/arith/nl/cad/proof_checker.h b/src/theory/arith/nl/cad/proof_checker.h
index 36d18c854..d7ce05b60 100644
--- a/src/theory/arith/nl/cad/proof_checker.h
+++ b/src/theory/arith/nl/cad/proof_checker.h
@@ -13,7 +13,7 @@
  * CAD proof checker utility.
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__ARITH__NL__CAD__PROOF_CHECKER_H
 #define CVC5__THEORY__ARITH__NL__CAD__PROOF_CHECKER_H
diff --git a/src/theory/arith/nl/cad/proof_generator.h b/src/theory/arith/nl/cad/proof_generator.h
index 440f25e49..27a711f75 100644
--- a/src/theory/arith/nl/cad/proof_generator.h
+++ b/src/theory/arith/nl/cad/proof_generator.h
@@ -13,7 +13,7 @@
  * Implements the proof generator for CAD.
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__ARITH__NL__CAD__PROOF_GENERATOR_H
 #define CVC5__THEORY__ARITH__NL__CAD__PROOF_GENERATOR_H
diff --git a/src/theory/arith/nl/cad/variable_ordering.h b/src/theory/arith/nl/cad/variable_ordering.h
index 00fbc8f49..2de262089 100644
--- a/src/theory/arith/nl/cad/variable_ordering.h
+++ b/src/theory/arith/nl/cad/variable_ordering.h
@@ -13,7 +13,7 @@
  * Implements variable orderings tailored to CAD.
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__ARITH__NL__CAD__VARIABLE_ORDERING_H
 #define CVC5__THEORY__ARITH__NL__CAD__VARIABLE_ORDERING_H
diff --git a/src/theory/arith/nl/ext/proof_checker.h b/src/theory/arith/nl/ext/proof_checker.h
index 21807a79d..400126510 100644
--- a/src/theory/arith/nl/ext/proof_checker.h
+++ b/src/theory/arith/nl/ext/proof_checker.h
@@ -13,7 +13,7 @@
  * NlExt proof checker utility.
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__ARITH__NL__EXT__PROOF_CHECKER_H
 #define CVC5__THEORY__ARITH__NL__EXT__PROOF_CHECKER_H
diff --git a/src/theory/arith/nl/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp
index af0f5e169..cc35a4675 100644
--- a/src/theory/arith/nl/iand_utils.cpp
+++ b/src/theory/arith/nl/iand_utils.cpp
@@ -17,7 +17,7 @@
 
 #include <cmath>
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 #include "theory/arith/nl/nl_model.h"
 #include "theory/rewriter.h"
 
diff --git a/src/theory/arith/nl/icp/candidate.h b/src/theory/arith/nl/icp/candidate.h
index 932698d71..ee8017cb7 100644
--- a/src/theory/arith/nl/icp/candidate.h
+++ b/src/theory/arith/nl/icp/candidate.h
@@ -16,7 +16,7 @@
 #ifndef CVC5__THEORY__ARITH__ICP__CANDIDATE_H
 #define CVC5__THEORY__ARITH__ICP__CANDIDATE_H
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifdef CVC5_POLY_IMP
 #include <poly/polyxx.h>
diff --git a/src/theory/arith/nl/icp/icp_solver.h b/src/theory/arith/nl/icp/icp_solver.h
index e7eb83bd4..c1b4b6dde 100644
--- a/src/theory/arith/nl/icp/icp_solver.h
+++ b/src/theory/arith/nl/icp/icp_solver.h
@@ -16,7 +16,7 @@
 #ifndef CVC5__THEORY__ARITH__ICP__ICP_SOLVER_H
 #define CVC5__THEORY__ARITH__ICP__ICP_SOLVER_H
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifdef CVC5_POLY_IMP
 #include <poly/polyxx.h>
diff --git a/src/theory/arith/nl/icp/intersection.h b/src/theory/arith/nl/icp/intersection.h
index 1911a397f..d7242054c 100644
--- a/src/theory/arith/nl/icp/intersection.h
+++ b/src/theory/arith/nl/icp/intersection.h
@@ -16,7 +16,7 @@
 #ifndef CVC5__THEORY__ARITH__ICP__INTERSECTION_H
 #define CVC5__THEORY__ARITH__ICP__INTERSECTION_H
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifdef CVC5_POLY_IMP
 
diff --git a/src/theory/arith/nl/icp/interval.h b/src/theory/arith/nl/icp/interval.h
index 4b47ae954..521a1f8ab 100644
--- a/src/theory/arith/nl/icp/interval.h
+++ b/src/theory/arith/nl/icp/interval.h
@@ -16,7 +16,7 @@
 #ifndef CVC5__THEORY__ARITH__ICP__INTERVAL_H
 #define CVC5__THEORY__ARITH__ICP__INTERVAL_H
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifdef CVC5_POLY_IMP
 #include <poly/polyxx.h>
diff --git a/src/theory/arith/nl/poly_conversion.h b/src/theory/arith/nl/poly_conversion.h
index 9e2b71ffe..3213df0ce 100644
--- a/src/theory/arith/nl/poly_conversion.h
+++ b/src/theory/arith/nl/poly_conversion.h
@@ -16,7 +16,7 @@
 #ifndef CVC5__THEORY__ARITH__NL__POLY_CONVERSION_H
 #define CVC5__THEORY__ARITH__NL__POLY_CONVERSION_H
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifdef CVC5_POLY_IMP
 
diff --git a/src/theory/arith/nl/stats.h b/src/theory/arith/nl/stats.h
index e80a66aca..988b647a6 100644
--- a/src/theory/arith/nl/stats.h
+++ b/src/theory/arith/nl/stats.h
@@ -13,7 +13,7 @@
  * Statistics for non-linear arithmetic.
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__ARITH__NL__STATS_H
 #define CVC5__THEORY__ARITH__NL__STATS_H
diff --git a/src/theory/arith/nl/transcendental/proof_checker.h b/src/theory/arith/nl/transcendental/proof_checker.h
index 1c0a00ca8..8675afe39 100644
--- a/src/theory/arith/nl/transcendental/proof_checker.h
+++ b/src/theory/arith/nl/transcendental/proof_checker.h
@@ -13,7 +13,7 @@
  * Proof checker utility for transcendental solver.
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__PROOF_CHECKER_H
 #define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__PROOF_CHECKER_H
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index 021562926..2f2d56962 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -16,7 +16,7 @@
  * \todo document this file
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__ARITH__NORMAL_FORM_H
 #define CVC5__THEORY__ARITH__NORMAL_FORM_H
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index 9b4503dd5..b88281495 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -17,7 +17,7 @@
  * and information derived from these.
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__ARITH__PARTIAL_MODEL_H
 #define CVC5__THEORY__ARITH__PARTIAL_MODEL_H
diff --git a/src/theory/arith/proof_checker.h b/src/theory/arith/proof_checker.h
index 341660c69..402656154 100644
--- a/src/theory/arith/proof_checker.h
+++ b/src/theory/arith/proof_checker.h
@@ -13,7 +13,7 @@
  * Arithmetic proof checker utility.
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__ARITH__PROOF_CHECKER_H
 #define CVC5__THEORY__ARITH__PROOF_CHECKER_H
diff --git a/src/theory/arith/proof_macros.h b/src/theory/arith/proof_macros.h
index 168ebfba6..c794c3b00 100644
--- a/src/theory/arith/proof_macros.h
+++ b/src/theory/arith/proof_macros.h
@@ -14,7 +14,7 @@
  * or unsat cores are enabled.
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__ARITH__PROOF_MACROS_H
 #define CVC5__THEORY__ARITH__PROOF_MACROS_H
diff --git a/src/theory/arith/rewrites.h b/src/theory/arith/rewrites.h
index a3a62097d..24b6abdd5 100644
--- a/src/theory/arith/rewrites.h
+++ b/src/theory/arith/rewrites.h
@@ -13,7 +13,7 @@
  * Type for rewrites for arithmetic.
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__ARITH__REWRITES_H
 #define CVC5__THEORY__ARITH__REWRITES_H
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 4cd9562e3..9cbb5bac2 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -51,7 +51,7 @@
  *   These are theory valid and are currently turned into lemmas
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #pragma once
 
diff --git a/src/theory/arith/simplex_update.h b/src/theory/arith/simplex_update.h
index 8431db16b..6216f53f6 100644
--- a/src/theory/arith/simplex_update.h
+++ b/src/theory/arith/simplex_update.h
@@ -25,7 +25,7 @@
  * using both the Tableau and PartialModel.
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #pragma once
 
diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h
index f6d97523d..7b2656752 100644
--- a/src/theory/arith/soi_simplex.h
+++ b/src/theory/arith/soi_simplex.h
@@ -51,7 +51,7 @@
  *   These are theory valid and are currently turned into lemmas
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #pragma once
 
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 4c34016b8..edec26260 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -16,7 +16,7 @@
  * \todo document this file
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #pragma once
 
diff --git a/src/theory/arith/tableau_sizes.h b/src/theory/arith/tableau_sizes.h
index 755a7b0ca..f23966c3c 100644
--- a/src/theory/arith/tableau_sizes.h
+++ b/src/theory/arith/tableau_sizes.h
@@ -16,7 +16,7 @@
  * \todo document this file
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #pragma once
 
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index b65159f50..26a33e247 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -13,7 +13,7 @@
  * Arithmetic theory.
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #pragma once
 
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index 1f5f565e2..2d56a26c7 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -15,7 +15,7 @@
  * [[ Add file-specific comments here ]]
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
 #define CVC5__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h
index 8abb23312..2b5582956 100644
--- a/src/theory/arith/type_enumerator.h
+++ b/src/theory/arith/type_enumerator.h
@@ -13,7 +13,7 @@
  * Enumerators for rationals and integers.
  */
 
-#include "cvc4_private.h"
+#include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__ARITH__TYPE_ENUMERATOR_H
 #define CVC5__THEORY__ARITH__TYPE_ENUMERATOR_H