1 files changed, 5 insertions, 5 deletions

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 945c82bf9..bb8fafb14 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -61,7 +61,7 @@ void TermDb::addTermEfficient( Node n, std::set< Node >& added){
 
 void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
   //don't add terms in quantifier bodies
-  if( withinQuant && !Options::current()->registerQuantBodyTerms ){
+  if( withinQuant && !options::registerQuantBodyTerms() ){
     return;
   }
   if( d_processed.find( n )==d_processed.end() ){
@@ -82,7 +82,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
         uf::InstantiatorTheoryUf* d_ith = (uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( THEORY_UF );
         for( int i=0; i<(int)n.getNumChildren(); i++ ){
           addTerm( n[i], added, withinQuant );
-          if( Options::current()->efficientEMatching ){
+          if( options::efficientEMatching() ){
             if( d_parents[n[i]][op].empty() ){
               //must add parent to equivalence class info
               Node nir = d_ith->getRepresentative( n[i] );
@@ -97,7 +97,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
               Assert(!getParents(n[i],op,i).empty());
             }
           }
-          if( Options::current()->eagerInstQuant ){
+          if( options::eagerInstQuant() ){
             if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
               int addedLemmas = 0;
               for( int i=0; i<(int)d_ith->d_op_triggers[op].size(); i++ ){
@@ -115,7 +115,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
       }
     }
   }else{
-    if( Options::current()->efficientEMatching && !n.hasAttribute(InstConstantAttribute())){
+    if( options::efficientEMatching() && !n.hasAttribute(InstConstantAttribute())){
       //Efficient e-matching must be notified
       //The term in triggers are not important here
       Debug("term-db") << "New in this branch term " << n << std::endl;
@@ -196,7 +196,7 @@ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
     Node mbt;
     if( d_type_map[ tn ].empty() ){
       std::stringstream ss;
-      ss << Expr::setlanguage(Options::current()->outputLanguage);
+      ss << Expr::setlanguage(options::outputLanguage());
       ss << "e_" << tn;
       mbt = NodeManager::currentNM()->mkVar( ss.str(), tn );
     }else{