Removing QUICK_CHECK, and other unused ones, from the Theory::Effort.

Seems to be working better <http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3749&category=&p=5&reference_id=3739>, and should fix the failing cases in the regressions.

Removing one test case from the integer regress0.

12 files changed, 123 insertions, 161 deletions

diff --git a/.cproject b/.cproject
index 2579ef3ae..6145dec05 100644
--- a/.cproject
+++ b/.cproject
@@ -20,7 +20,7 @@
 					<folderInfo id="cdt.managedbuild.toolchain.gnu.base.1461790692.1059214216" name="/" resourcePath="">
 						<toolChain id="cdt.managedbuild.toolchain.gnu.base.1311293674" name="cdt.managedbuild.toolchain.gnu.base" superClass="cdt.managedbuild.toolchain.gnu.base">
 							<targetPlatform archList="all" binaryParser="org.eclipse.cdt.core.ELF" id="cdt.managedbuild.target.gnu.platform.base.1799734525" name="Debug Platform" osList="linux,hpux,aix,qnx" superClass="cdt.managedbuild.target.gnu.platform.base"/>
-							<builder buildPath="${workspace_loc/cvc4/}" id="cdt.managedbuild.target.gnu.builder.base.549477204" incrementalBuildTarget="all" keepEnvironmentInBuildfile="false" managedBuildOn="false" name="Gnu Make Builder" parallelBuildOn="true" parallelizationNumber="2" superClass="cdt.managedbuild.target.gnu.builder.base">
+							<builder buildPath="${workspace_loc/cvc4/}" id="cdt.managedbuild.target.gnu.builder.base.549477204" incrementalBuildTarget="all" keepEnvironmentInBuildfile="false" managedBuildOn="false" name="Gnu Make Builder" parallelBuildOn="true" parallelizationNumber="10" superClass="cdt.managedbuild.target.gnu.builder.base">
 								<outputEntries>
 									<entry flags="VALUE_WORKSPACE_PATH|RESOLVED" kind="outputPath" name=""/>
 								</outputEntries>
@@ -57,7 +57,9 @@
 	<storageModule moduleId="cdtBuildSystem" version="4.0.0">
 		<project id="cvc4.null.1129006228" name="cvc4"/>
 	</storageModule>
-	<storageModule moduleId="refreshScope"/>
+	<storageModule moduleId="refreshScope" versionNumber="1">
+		<resource resourceType="PROJECT" workspacePath="/cvc4-trunk"/>
+	</storageModule>
 	<storageModule moduleId="scannerConfiguration">
 		<autodiscovery enabled="true" problemReportingEnabled="true" selectedProfileId=""/>
 		<profile id="org.eclipse.cdt.make.core.GCCStandardMakePerProjectProfile">
diff --git a/.project b/.project
index 1465eabe2..fec1cfaa5 100644
--- a/.project
+++ b/.project
@@ -32,7 +32,7 @@
 				</dictionary>
 				<dictionary>
 					<key>org.eclipse.cdt.make.core.buildArguments</key>
-					<value>-j2</value>
+					<value>-j10</value>
 				</dictionary>
 				<dictionary>
 					<key>org.eclipse.cdt.make.core.buildCommand</key>
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 678fe28dc..9f3285fff 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -248,7 +248,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable)
             Debug("minisat") << "got new unit " << ps[0] << " at assertion level " << assertionLevel << std::endl;
             trail_user.push(ps[0]);
           }
-          return ok = (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == CRef_Undef);
+          return ok = (propagate(CHECK_WITHOUTH_THEORY) == CRef_Undef);
         } else return ok;
       } else {
         CRef cr = ca.alloc(assertionLevel, ps, false);
@@ -654,8 +654,8 @@ CRef Solver::propagate(TheoryCheckType type)
 
     ScopedBool scoped_bool(minisat_busy, true);
 
-    // If we are not in the quick mode add the lemmas that were left begind
-    if (type != CHECK_WITHOUTH_PROPAGATION_QUICK && lemmas.size() > 0) {
+    // If we are not in the quick mode add the lemmas that were left behind
+    if (type != CHECK_WITHOUTH_THEORY && lemmas.size() > 0) {
       confl = updateLemmas();
       if (confl != CRef_Undef) {
         return confl;
@@ -664,9 +664,9 @@ CRef Solver::propagate(TheoryCheckType type)
 
     // If this is the final check, no need for Boolean propagation and
     // theory propagation
-    if (type == CHECK_WITHOUTH_PROPAGATION_FINAL) {
+    if (type == CHECK_FINAL) {
       // Do the theory check
-      theoryCheck(CVC4::theory::Theory::FULL_EFFORT);
+      theoryCheck(CVC4::theory::Theory::EFFORT_FULL);
       // If there are lemmas (or conflicts) update them
       if (lemmas.size() > 0) {
         recheck = true;
@@ -677,38 +677,24 @@ CRef Solver::propagate(TheoryCheckType type)
       }
     }
 
-    // The effort we will be using to theory check
-    CVC4::theory::Theory::Effort effort = type == CHECK_WITHOUTH_PROPAGATION_QUICK ?
-    		CVC4::theory::Theory::QUICK_CHECK : 
-    		CVC4::theory::Theory::STANDARD;
-
     // Keep running until we have checked everything, we
     // have no conflict and no new literals have been asserted
-    do {
-        do {
-          // Propagate on the clauses
-          confl = propagateBool();
-
-          // If no conflict, do the theory check
-          if (confl == CRef_Undef) {
-              // Do the theory check
-              theoryCheck(effort);
-              // If there are lemmas (or conflicts) update them
-              if (lemmas.size() > 0) {
-                  confl = updateLemmas();
-              }
-          }
-        } while (confl == CRef_Undef && qhead < trail.size());
-
-        // If still consistent do some theory propagation
-        if (confl == CRef_Undef && type == CHECK_WITH_PROPAGATION_STANDARD) {
-          propagateTheory();
-          if (lemmas.size() > 0) {
-              confl = updateLemmas();
-          }
+      do {
+        // Propagate on the clauses
+        confl = propagateBool();
+
+        // If no conflict, do the theory check
+        if (confl == CRef_Undef && type != CHECK_WITHOUTH_THEORY) {
+            // Do the theory check
+            theoryCheck(CVC4::theory::Theory::EFFORT_STANDARD);
+            // Pick up the theory propagated literals
+            propagateTheory();
+            // If there are lemmas (or conflicts) update them
+            if (lemmas.size() > 0) {
+                confl = updateLemmas();
+            }
         }
-
-    } while (confl == CRef_Undef && qhead < trail.size());
+      } while (confl == CRef_Undef && qhead < trail.size());
 
     return confl;
 }
@@ -931,7 +917,7 @@ bool Solver::simplify()
 {
     assert(decisionLevel() == 0);
 
-    if (!ok || propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != CRef_Undef)
+    if (!ok || propagate(CHECK_WITHOUTH_THEORY) != CRef_Undef)
         return ok = false;
 
     if (nAssigns() == simpDB_assigns || (simpDB_props > 0))
@@ -972,7 +958,7 @@ lbool Solver::search(int nof_conflicts)
     vec<Lit>    learnt_clause;
     starts++;
 
-    TheoryCheckType check_type = CHECK_WITH_PROPAGATION_STANDARD;
+    TheoryCheckType check_type = CHECK_WITH_THEORY;
     for (;;) {
 
         // Propagate and call the theory solvers
@@ -1025,14 +1011,14 @@ lbool Solver::search(int nof_conflicts)
             }
 
              // We have a conflict so, we are going back to standard checks
-            check_type = CHECK_WITH_PROPAGATION_STANDARD;
+            check_type = CHECK_WITH_THEORY;
         } else {
 
 	    // If this was a final check, we are satisfiable
-            if (check_type == CHECK_WITHOUTH_PROPAGATION_FINAL) {
+            if (check_type == CHECK_FINAL) {
               // Unless a lemma has added more stuff to the queues
               if (!order_heap.empty() || qhead < trail.size()) {
-                check_type = CHECK_WITH_PROPAGATION_STANDARD;
+                check_type = CHECK_WITH_THEORY;
                 continue;
               } else if (recheck) {
                 // There some additional stuff added, so we go for another full-check
@@ -1086,7 +1072,7 @@ lbool Solver::search(int nof_conflicts)
 
                 if (next == lit_Undef) {
                     // We need to do a full theory check to confirm
-                    check_type = CHECK_WITHOUTH_PROPAGATION_FINAL;
+                    check_type = CHECK_FINAL;
                     continue;
                 }
 
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index c0dd00166..8a5472725 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -303,12 +303,12 @@ protected:
     vec<bool>           theory;           // Is the variable representing a theory atom
 
     enum TheoryCheckType {
-      // Quick check, but don't perform theory propagation
-      CHECK_WITHOUTH_PROPAGATION_QUICK,
-      // Check and perform theory propagation
-      CHECK_WITH_PROPAGATION_STANDARD,
-      // The SAT problem is satisfiable, perform a full theory check
-      CHECK_WITHOUTH_PROPAGATION_FINAL
+      // Quick check, but don't perform theory reasoning
+      CHECK_WITHOUTH_THEORY,
+      // Check and perform theory reasoning
+      CHECK_WITH_THEORY,
+      // The SAT abstraction of the problem is satisfiable, perform a full theory check
+      CHECK_FINAL
     };
 
     // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 2b5468186..2cacfbcc0 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -214,7 +214,7 @@ bool SimpSolver::strengthenClause(CRef cr, Lit l)
         updateElimHeap(var(l));
     }
 
-    return c.size() == 1 ? enqueue(c[0]) && propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == CRef_Undef : true;
+    return c.size() == 1 ? enqueue(c[0]) && propagate(CHECK_WITHOUTH_THEORY) == CRef_Undef : true;
 }
 
 
@@ -321,7 +321,7 @@ bool SimpSolver::implied(const vec<Lit>& c)
             uncheckedEnqueue(~c[i]);
         }
 
-    bool result = propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != CRef_Undef;
+    bool result = propagate(CHECK_WITHOUTH_THEORY) != CRef_Undef;
     cancelUntil(0);
     return result;
 }
@@ -410,7 +410,7 @@ bool SimpSolver::asymm(Var v, CRef cr)
         else
             l = c[i];
 
-    if (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != CRef_Undef){
+    if (propagate(CHECK_WITHOUTH_THEORY) != CRef_Undef){
         cancelUntil(0);
         asymm_lits++;
         if (!strengthenClause(cr, l))
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index a1d57af66..3760e233d 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1109,65 +1109,63 @@ Node flattenAnd(Node n){
 }
 
 void TheoryArith::propagate(Effort e) {
-  if(quickCheckOrMore(e)){
-    bool propagated = false;
-    if(Options::current()->arithPropagation && hasAnyUpdates()){
-      propagateCandidates();
-    }else{
-      clearUpdates();
-    }
+  bool propagated = false;
+  if(Options::current()->arithPropagation && hasAnyUpdates()){
+    propagateCandidates();
+  }else{
+    clearUpdates();
+  }
 
-    while(d_propManager.hasMorePropagations()){
-      const PropManager::PropUnit next = d_propManager.getNextPropagation();
-      bool flag = next.flag;
-      TNode toProp = next.consequent;
-
-      TNode atom = (toProp.getKind() == kind::NOT) ? toProp[0] : toProp;
-
-      Debug("arith::propagate") << "propagate  @" << getContext()->getLevel() <<" flag: "<< flag << " " << toProp << endl;
-
-      if(flag) {
-        //Currently if the flag is set this came from an equality detected by the
-        //equality engine in the the difference manager.
-        if(toProp.getKind() == kind::EQUAL){
-          Node normalized = Rewriter::rewrite(toProp);
-          Node notNormalized = normalized.notNode();
-
-          if(d_diseq.find(notNormalized) == d_diseq.end()){
-            d_out->propagate(toProp);
-            propagated = true;
-          }else{
-            Node exp = d_differenceManager.explain(toProp);
-            Node lp = flattenAnd(exp.andNode(notNormalized));
-            Debug("arith::propagate") << "propagate conflict" <<  lp << endl;
-            d_out->conflict(lp);
-
-            propagated = true;
-            break;
-          }
-        }else{
+  while(d_propManager.hasMorePropagations()){
+    const PropManager::PropUnit next = d_propManager.getNextPropagation();
+    bool flag = next.flag;
+    TNode toProp = next.consequent;
+
+    TNode atom = (toProp.getKind() == kind::NOT) ? toProp[0] : toProp;
+
+    Debug("arith::propagate") << "propagate  @" << getContext()->getLevel() <<" flag: "<< flag << " " << toProp << endl;
+
+    if(flag) {
+      //Currently if the flag is set this came from an equality detected by the
+      //equality engine in the the difference manager.
+      if(toProp.getKind() == kind::EQUAL){
+        Node normalized = Rewriter::rewrite(toProp);
+        Node notNormalized = normalized.notNode();
+
+        if(d_diseq.find(notNormalized) == d_diseq.end()){
           d_out->propagate(toProp);
           propagated = true;
+        }else{
+          Node exp = d_differenceManager.explain(toProp);
+          Node lp = flattenAnd(exp.andNode(notNormalized));
+          Debug("arith::propagate") << "propagate conflict" <<  lp << endl;
+          d_out->conflict(lp);
+
+          propagated = true;
+          break;
         }
-      }else if(inContextAtom(atom)){
-        Node satValue = d_valuation.getSatValue(toProp);
-        AlwaysAssert(satValue.isNull());
-        propagated = true;
-        d_out->propagate(toProp);
       }else{
-        //Not clear if this is a good time to do this or not...
-        Debug("arith::propagate") << "Atom is not in context" << toProp << endl;
-#warning "enable remove atom in database"
-        //d_atomDatabase.removeAtom(atom);
+        d_out->propagate(toProp);
+        propagated = true;
       }
+    }else if(inContextAtom(atom)){
+      Node satValue = d_valuation.getSatValue(toProp);
+      AlwaysAssert(satValue.isNull());
+      propagated = true;
+      d_out->propagate(toProp);
+    }else{
+      //Not clear if this is a good time to do this or not...
+      Debug("arith::propagate") << "Atom is not in context" << toProp << endl;
+#warning "enable remove atom in database"
+      //d_atomDatabase.removeAtom(atom);
     }
+  }
 
-    if(!propagated){
-      //Opportunistically export previous conflicts
-      while(d_simplex.hasMoreLemmas()){
-        Node lemma = d_simplex.popLemma();
-        d_out->lemma(lemma);
-      }
+  if(!propagated){
+    //Opportunistically export previous conflicts
+    while(d_simplex.hasMoreLemmas()){
+      Node lemma = d_simplex.popLemma();
+      d_out->lemma(lemma);
     }
   }
 }
@@ -1387,7 +1385,7 @@ void TheoryArith::presolve(){
   }
 
   d_learner.clear();
-  check(FULL_EFFORT);
+  check(EFFORT_FULL);
 }
 
 EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 174513c72..6e0d45948 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -228,7 +228,7 @@ void TheoryDatatypes::check(Effort e) {
     }
   }
 
-  if( e == FULL_EFFORT ) {
+  if( e == EFFORT_FULL ) {
     Debug("datatypes-split") << "Check for splits " << e << endl;
     //do splitting
     for( EqLists::iterator i = d_labels.begin(); i != d_labels.end(); i++ ) {
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 76aabeb1f..0404bda3b 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -31,14 +31,12 @@ TheoryId Theory::s_uninterpretedSortOwner = THEORY_UF;
 
 std::ostream& operator<<(std::ostream& os, Theory::Effort level){
   switch(level){
-  case Theory::MIN_EFFORT:
-    os << "MIN_EFFORT"; break;
-  case Theory::QUICK_CHECK:
-    os << "QUICK_CHECK"; break;
-  case Theory::STANDARD:
-    os << "STANDARD"; break;
-  case Theory::FULL_EFFORT:
-    os << "FULL_EFFORT"; break;
+  case Theory::EFFORT_STANDARD:
+    os << "EFFORT_STANDARD"; break;
+  case Theory::EFFORT_FULL:
+    os << "EFFORT_FULL"; break;
+  case Theory::EFFORT_COMBINATION:
+    os << "EFFORT_COMBINATION"; break;
   default:
       Unreachable();
   }
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 35c81239f..1451568ab 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -241,7 +241,7 @@ public:
    * Returns the ID of the theory responsible for the given node.
    */
   static inline TheoryId theoryOf(TNode node) {
-    Trace("theory") << "theoryOf(" << node << ")" << std::endl;
+    Trace("theory::internal") << "theoryOf(" << node << ")" << std::endl;
     // Constants, variables, 0-ary constructors
     if (node.getMetaKind() == kind::metakind::VARIABLE || node.getMetaKind() == kind::metakind::CONSTANT) {
       return theoryOf(node.getType());
@@ -298,28 +298,29 @@ public:
    * with FULL_EFFORT.
    */
   enum Effort {
-    MIN_EFFORT = 0,
-    QUICK_CHECK = 10,
-    STANDARD = 50,
-    FULL_EFFORT = 100,
-    COMBINATION = 150
+    /**
+     * Standard effort where theory need not do anything
+     */
+    EFFORT_STANDARD = 50,
+    /**
+     * Full effort requires the theory make sure its assertions are satisfiable or not
+     */
+    EFFORT_FULL = 100,
+    /**
+     * Combination effort means that the individual theories are already satisfied, and
+     * it is time to put some effort into propagation of shared term equalities
+     */
+    EFFORT_COMBINATION = 150
   };/* enum Effort */
 
-  // simple, useful predicates for effort values
-  static inline bool minEffortOnly(Effort e) CVC4_CONST_FUNCTION
-    { return e == MIN_EFFORT; }
-  static inline bool quickCheckOrMore(Effort e) CVC4_CONST_FUNCTION
-    { return e >= QUICK_CHECK; }
-  static inline bool quickCheckOnly(Effort e) CVC4_CONST_FUNCTION
-    { return e >= QUICK_CHECK && e <  STANDARD; }
   static inline bool standardEffortOrMore(Effort e) CVC4_CONST_FUNCTION
-    { return e >= STANDARD; }
+    { return e >= EFFORT_STANDARD; }
   static inline bool standardEffortOnly(Effort e) CVC4_CONST_FUNCTION
-    { return e >= STANDARD && e <  FULL_EFFORT; }
+    { return e >= EFFORT_STANDARD && e <  EFFORT_FULL; }
   static inline bool fullEffort(Effort e) CVC4_CONST_FUNCTION
-    { return e == FULL_EFFORT; }
+    { return e == EFFORT_FULL; }
   static inline bool combination(Effort e) CVC4_CONST_FUNCTION 
-    { return e == COMBINATION; }
+    { return e == EFFORT_COMBINATION; }
 
   /**
    * Get the id for this Theory.
@@ -409,12 +410,12 @@ public:
    * - throw an exception
    * - or call get() until done() is true.
    */
-  virtual void check(Effort level = FULL_EFFORT) { }
+  virtual void check(Effort level = EFFORT_FULL) { }
 
   /**
    * T-propagate new literal assignments in the current context.
    */
-  virtual void propagate(Effort level = FULL_EFFORT) { }
+  virtual void propagate(Effort level = EFFORT_FULL) { }
 
   /**
    * Return an explanation for the literal represented by parameter n
diff --git a/test/regress/regress0/arith/integers/Makefile.am b/test/regress/regress0/arith/integers/Makefile.am
index ccfeb51f1..d55e12fbc 100644
--- a/test/regress/regress0/arith/integers/Makefile.am
+++ b/test/regress/regress0/arith/integers/Makefile.am
@@ -18,7 +18,6 @@ TESTS =	\
 	arith-int-013.cvc \
 	arith-int-022.cvc \
 	arith-int-024.cvc \
-	arith-int-041.cvc \
 	arith-int-042.cvc \
 	arith-int-042.min.cvc \
 	arith-int-047.cvc \
@@ -66,6 +65,7 @@ EXTRA_DIST = $(TESTS) \
 	arith-int-038.cvc \
 	arith-int-039.cvc \
 	arith-int-040.cvc \
+	arith-int-041.cvc \
 	arith-int-043.cvc \
 	arith-int-044.cvc \
 	arith-int-045.cvc \
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index 4787dfd21..41d370aac 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -64,7 +64,7 @@ class TheoryArithWhite : public CxxTest::TestSuite {
 
 public:
 
-  TheoryArithWhite() : d_level(Theory::FULL_EFFORT), d_zero(0), d_one(1), debug(false) {}
+  TheoryArithWhite() : d_level(Theory::EFFORT_FULL), d_zero(0), d_one(1), debug(false) {}
 
   void fakeTheoryEnginePreprocess(TNode inp){
     Node rewrite = inp; //FIXME this needs to enforce that inp is fully rewritten already!
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 76385219d..a737772ed 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -181,38 +181,15 @@ public:
   }
 
   void testEffort(){
-    Theory::Effort m = Theory::MIN_EFFORT;
-    Theory::Effort q = Theory::QUICK_CHECK;
-    Theory::Effort s = Theory::STANDARD;
-    Theory::Effort f = Theory::FULL_EFFORT;
-
-    TS_ASSERT( Theory::minEffortOnly(m));
-    TS_ASSERT(!Theory::minEffortOnly(q));
-    TS_ASSERT(!Theory::minEffortOnly(s));
-    TS_ASSERT(!Theory::minEffortOnly(f));
-
-    TS_ASSERT(!Theory::quickCheckOnly(m));
-    TS_ASSERT( Theory::quickCheckOnly(q));
-    TS_ASSERT(!Theory::quickCheckOnly(s));
-    TS_ASSERT(!Theory::quickCheckOnly(f));
-
-    TS_ASSERT(!Theory::standardEffortOnly(m));
-    TS_ASSERT(!Theory::standardEffortOnly(q));
+    Theory::Effort s = Theory::EFFORT_STANDARD;
+    Theory::Effort f = Theory::EFFORT_FULL;
+
     TS_ASSERT( Theory::standardEffortOnly(s));
     TS_ASSERT(!Theory::standardEffortOnly(f));
 
-    TS_ASSERT(!Theory::fullEffort(m));
-    TS_ASSERT(!Theory::fullEffort(q));
     TS_ASSERT(!Theory::fullEffort(s));
     TS_ASSERT( Theory::fullEffort(f));
 
-    TS_ASSERT(!Theory::quickCheckOrMore(m));
-    TS_ASSERT( Theory::quickCheckOrMore(q));
-    TS_ASSERT( Theory::quickCheckOrMore(s));
-    TS_ASSERT( Theory::quickCheckOrMore(f));
-
-    TS_ASSERT(!Theory::standardEffortOrMore(m));
-    TS_ASSERT(!Theory::standardEffortOrMore(q));
     TS_ASSERT( Theory::standardEffortOrMore(s));
     TS_ASSERT( Theory::standardEffortOrMore(f));
   }
@@ -225,7 +202,7 @@ public:
 
     TS_ASSERT(!d_dummy->doneWrapper());
 
-    d_dummy->check(Theory::FULL_EFFORT);
+    d_dummy->check(Theory::EFFORT_FULL);
 
     TS_ASSERT(d_dummy->doneWrapper());
   }