From f87f038c5f0821d0fefb01cea00bfdec6004da91 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Fri, 9 Apr 2021 17:22:07 -0700
Subject: Rename CVC4_ macros to CVC5_. (#6327)

---
 src/theory/theory_model_builder.cpp | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'src/theory/theory_model_builder.cpp')

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index a8dd647f0..c06c6cd89 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -459,7 +459,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
     bool evaluable = false;
     // Set to true if a term in the current equivalence class has been given an
     // assignment exclusion set.
-    bool hasESet CVC4_UNUSED = false;
+    bool hasESet CVC5_UNUSED = false;
     // Set to true if we found that a term in the current equivalence class has
     // been given an assignment exclusion set, and we have not seen this term
     // as part of a previous assignment exclusion group. In other words, when
@@ -838,7 +838,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
         isCorecursive = dt.isCodatatype()
                         && (!dt.isFinite(t) || dt.isRecursiveSingleton(t));
       }
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
       bool isUSortFiniteRestricted = false;
       if (options::finiteModelFind())
       {
@@ -861,7 +861,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
       }
       Trace("model-builder") << "  Assign phase, working on type: " << t
                              << endl;
-      bool assignable, evaluable CVC4_UNUSED;
+      bool assignable, evaluable CVC5_UNUSED;
       std::map<Node, Assigner>::iterator itAssigner;
       std::map<Node, Node>::iterator itAssignerM;
       set<Node>* repSet = typeRepSet.getSet(t);
@@ -935,7 +935,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
               success = true;
               Trace("model-builder-debug") << "Check if excluded : " << n
                                            << std::endl;
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
               if (isUSortFiniteRestricted)
               {
                 // must not involve uninterpreted constants beyond cardinality
@@ -1012,7 +1012,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
     }
   }
 
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   // Assert that all representatives have been converted to constants
   for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it)
   {
@@ -1024,7 +1024,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
       Assert(false);
     }
   }
-#endif /* CVC4_ASSERTIONS */
+#endif /* CVC5_ASSERTIONS */
 
   Trace("model-builder") << "Copy representatives to model..." << std::endl;
   tm->d_reps.clear();
@@ -1081,7 +1081,7 @@ void TheoryEngineModelBuilder::postProcessModel(bool incomplete, TheoryModel* m)
 
 void TheoryEngineModelBuilder::debugCheckModel(TheoryModel* tm)
 {
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   if (tm->hasApproximations())
   {
     // models with approximations may fail the assertions below
@@ -1125,7 +1125,7 @@ void TheoryEngineModelBuilder::debugCheckModel(TheoryModel* tm)
       }
     }
   }
-#endif /* CVC4_ASSERTIONS */
+#endif /* CVC5_ASSERTIONS */
 
   // builder-specific debugging
   debugModel(tm);
-- 
cgit v1.2.3