1 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index ec5752d3a..1c01c35ab 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -141,7 +141,7 @@ void TheoryArith::addSharedTerm(TNode n){
   d_differenceManager.addSharedTerm(n);
 }
 
-Node TheoryArith::preprocess(TNode atom) {
+Node TheoryArith::ppRewrite(TNode atom) {
   Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl;
 
   Node a = d_pbSubstitutions.apply(atom);
@@ -167,7 +167,7 @@ Node TheoryArith::preprocess(TNode atom) {
   return a;
 }
 
-Theory::SolveStatus TheoryArith::solve(TNode in, SubstitutionMap& outSubstitutions) {
+Theory::PPAssertStatus TheoryArith::ppAsert(TNode in, SubstitutionMap& outSubstitutions) {
   TimerStat::CodeTimer codeTimer(d_statistics.d_simplifyTimer);
   Debug("simplify") << "TheoryArith::solve(" << in << ")" << endl;
 
@@ -220,7 +220,7 @@ Theory::SolveStatus TheoryArith::solve(TNode in, SubstitutionMap& outSubstitutio
           // substitution is integral
           Debug("simplify") << "TheoryArith::solve(): substitution " << minVar << " |-> " << elim << endl;
           outSubstitutions.addSubstitution(minVar, elim);
-          return SOLVE_STATUS_SOLVED;
+          return PP_ASSERT_STATUS_SOLVED;
         } else {
           Debug("simplify") << "TheoryArith::solve(): can't substitute b/c it's integer: " << minVar << ":" << minVar.getType() << " |-> " << elim << ":" << elim.getType() << endl;
         }
@@ -243,10 +243,10 @@ Theory::SolveStatus TheoryArith::solve(TNode in, SubstitutionMap& outSubstitutio
     break;
   }
 
-  return SOLVE_STATUS_UNSOLVED;
+  return PP_ASSERT_STATUS_UNSOLVED;
 }
 
-void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) {
+void TheoryArith::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
   TimerStat::CodeTimer codeTimer(d_statistics.d_staticLearningTimer);
 
   d_learner.staticLearning(n, learned);