Fixing name changes that cam in from the merge.

diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp
index 61bf5c76e4d88903d30cae580edd8ef862920be6..4f182fb691af8b6d053c739465ea24ddd3f1e6fa 100644 (file)
--- a/src/theory/arith/arith_ite_utils.cpp
+++ b/src/theory/arith/arith_ite_utils.cpp
@@ -120,7 +120,7 @@ Node ArithIteUtils::reduceVariablesInItes(Node n){
   return Node::null();
 }
 
-ArithIteUtils::ArithIteUtils(ContainsTermITEVistor& contains,
+ArithIteUtils::ArithIteUtils(ContainsTermITEVisitor& contains,
                              context::Context* uc,
                              TheoryModel* model)
   : d_contains(contains)

diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h
index fab0f32cbc0cb3dd80f7c50839de8dea14a9e781..5bdcd52da5812ade049b089ec7c3a6e976f04711 100644 (file)
--- a/src/theory/arith/arith_ite_utils.h
+++ b/src/theory/arith/arith_ite_utils.h
@@ -18,14 +18,14 @@
 
 namespace CVC4 {
 namespace theory {
-class ContainsTermITEVistor;
+class ContainsTermITEVisitor;
 class SubstitutionMap;
 class TheoryModel;
 
 namespace arith {
 
 class ArithIteUtils {
-  ContainsTermITEVistor& d_contains;
+  ContainsTermITEVisitor& d_contains;
   SubstitutionMap* d_subs;
   TheoryModel* d_model;
 
@@ -56,7 +56,7 @@ class ArithIteUtils {
   std::vector<Node> d_orBinEqs;
 
 public:
-  ArithIteUtils(ContainsTermITEVistor& contains,
+  ArithIteUtils(ContainsTermITEVisitor& contains,
                 context::Context* userContext,
                 TheoryModel* model);
   ~ArithIteUtils();

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 2a263857a63c79b5218f8182d45baef0714a0b5c..80d1152dac190bfe264f968db323b7508ea934a0 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1492,7 +1492,7 @@ bool TheoryEngine::donePPSimpITE(std::vector<Node>& assertions){
   // Do theory specific preprocessing passes
   if(d_logicInfo.isTheoryEnabled(theory::THEORY_ARITH)){
     if(!simpDidALotOfWork){
-      ContainsTermITEVistor& contains = *d_iteRemover.getContainsVisitor();
+      ContainsTermITEVisitor& contains = *d_iteRemover.getContainsVisitor();
       arith::ArithIteUtils aiteu(contains, d_userContext, getModel());
       bool anyItes = false;
       for(size_t i = 0;  i < assertions.size(); ++i){