1 files changed, 12 insertions, 11 deletions
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 10d2aee8c..9ed2202fe 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -25,6 +25,7 @@
 #include "theory/rewriter.h"
 #include "expr/expr_stream.h"
 #include "decision/decision_engine.h"
+#include "decision/options.h"
 #include "util/lemma_input_channel.h"
 #include "util/lemma_output_channel.h"
 
@@ -94,7 +95,7 @@ SatLiteral TheoryProxy::getNextDecisionRequest(bool &stopSearch) {
   if(stopSearch) {
     Trace("decision") << "  ***  Decision Engine stopped search *** " << std::endl;
   }
-  return Options::current()->decisionOptions.stopOnly ? undefSatLiteral : ret;
+  return options::decisionStopOnly() ? undefSatLiteral : ret;
 }
 
 bool TheoryProxy::theoryNeedCheck() const {
@@ -115,10 +116,10 @@ void TheoryProxy::notifyRestart() {
 
   static uint32_t lemmaCount = 0;
 
-  if(Options::current()->lemmaInputChannel != NULL) {
-    while(Options::current()->lemmaInputChannel->hasNewLemma()) {
+  if(options::lemmaInputChannel() != NULL) {
+    while(options::lemmaInputChannel()->hasNewLemma()) {
       Debug("shared") << "shared" << std::endl;
-      Expr lemma = Options::current()->lemmaInputChannel->getNewLemma();
+      Expr lemma = options::lemmaInputChannel()->getNewLemma();
       Node asNode = lemma.getNode();
       asNode = theory::Rewriter::rewrite(asNode);
 
@@ -142,10 +143,10 @@ void TheoryProxy::notifyRestart() {
 
 void TheoryProxy::notifyNewLemma(SatClause& lemma) {
   Assert(lemma.size() > 0);
-  if(Options::current()->lemmaOutputChannel != NULL) {
+  if(options::lemmaOutputChannel() != NULL) {
     if(lemma.size() == 1) {
       // cannot share units yet
-      //Options::current()->lemmaOutputChannel->notifyNewLemma(d_cnfStream->getNode(lemma[0]).toExpr());
+      //options::lemmaOutputChannel()->notifyNewLemma(d_cnfStream->getNode(lemma[0]).toExpr());
     } else {
       NodeBuilder<> b(kind::OR);
       for(unsigned i = 0, i_end = lemma.size(); i < i_end; ++i) {
@@ -155,7 +156,7 @@ void TheoryProxy::notifyNewLemma(SatClause& lemma) {
 
       if(d_shared.find(n) == d_shared.end()) {
         d_shared.insert(n);
-        Options::current()->lemmaOutputChannel->notifyNewLemma(n.toExpr());
+        options::lemmaOutputChannel()->notifyNewLemma(n.toExpr());
       } else {
         Debug("shared") <<"drop new " << n << std::endl;
       }
@@ -165,8 +166,8 @@ void TheoryProxy::notifyNewLemma(SatClause& lemma) {
 
 SatLiteral TheoryProxy::getNextReplayDecision() {
 #ifdef CVC4_REPLAY
-  if(Options::current()->replayStream != NULL) {
-    Expr e = Options::current()->replayStream->nextExpr();
+  if(options::replayStream() != NULL) {
+    Expr e = options::replayStream()->nextExpr();
     if(!e.isNull()) { // we get null node when out of decisions to replay
       // convert & return
       return d_cnfStream->getLiteral(e);
@@ -179,9 +180,9 @@ SatLiteral TheoryProxy::getNextReplayDecision() {
 
 void TheoryProxy::logDecision(SatLiteral lit) {
 #ifdef CVC4_REPLAY
-  if(Options::current()->replayLog != NULL) {
+  if(options::replayLog() != NULL) {
     Assert(lit != undefSatLiteral, "logging an `undef' decision ?!");
-    *Options::current()->replayLog << d_cnfStream->getNode(lit) << std::endl;
+    *options::replayLog() << d_cnfStream->getNode(lit) << std::endl;
   }
 #endif /* CVC4_REPLAY */
 }