1 files changed, 11 insertions, 11 deletions

diff --git a/src/main/util.cpp b/src/main/util.cpp
index 5877704ae..756c7d7a9 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -27,7 +27,7 @@
 
 #include "util/Assert.h"
 #include "util/exception.h"
-#include "util/options.h"
+#include "options/options.h"
 #include "util/stats.h"
 
 #include "cvc4autoconfig.h"
@@ -52,7 +52,7 @@ bool segvNoSpin = false;
 /** Handler for SIGXCPU, i.e., timeout. */
 void timeout_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 interrupted by timeout.\n");
-  if(pOptions->statistics && pStatistics != NULL) {
+  if((*pOptions)[options::statistics] && pStatistics != NULL) {
     pStatistics->flushInformation(cerr);
   }
   abort();
@@ -61,7 +61,7 @@ void timeout_handler(int sig, siginfo_t* info, void*) {
 /** Handler for SIGINT, i.e., when the user hits control C. */
 void sigint_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 interrupted by user.\n");
-  if(pOptions->statistics && pStatistics != NULL) {
+  if((*pOptions)[options::statistics] && pStatistics != NULL) {
     pStatistics->flushInformation(cerr);
   }
   abort();
@@ -86,7 +86,7 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
 
   if(segvNoSpin) {
     fprintf(stderr, "No-spin requested, aborting...\n");
-    if(pOptions->statistics && pStatistics != NULL) {
+    if((*pOptions)[options::statistics] && pStatistics != NULL) {
       pStatistics->flushInformation(cerr);
     }
     abort();
@@ -106,7 +106,7 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
   } else if(addr < 10*1024) {
     cerr << "Looks like a NULL pointer was dereferenced." << endl;
   }
-  if(pOptions->statistics && pStatistics != NULL) {
+  if((*pOptions)[options::statistics] && pStatistics != NULL) {
     pStatistics->flushInformation(cerr);
   }
   abort();
@@ -119,7 +119,7 @@ void ill_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 executed an illegal instruction in DEBUG mode.\n");
   if(segvNoSpin) {
     fprintf(stderr, "No-spin requested, aborting...\n");
-    if(pOptions->statistics && pStatistics != NULL) {
+    if((*pOptions)[options::statistics] && pStatistics != NULL) {
       pStatistics->flushInformation(cerr);
     }
     abort();
@@ -132,7 +132,7 @@ void ill_handler(int sig, siginfo_t* info, void*) {
   }
 #else /* CVC4_DEBUG */
   fprintf(stderr, "CVC4 executed an illegal instruction.\n");
-  if(pOptions->statistics && pStatistics != NULL) {
+  if((*pOptions)[options::statistics] && pStatistics != NULL) {
     pStatistics->flushInformation(cerr);
   }
   abort();
@@ -156,7 +156,7 @@ void cvc4unexpected() {
   }
   if(segvNoSpin) {
     fprintf(stderr, "No-spin requested.\n");
-    if(pOptions->statistics && pStatistics != NULL) {
+    if((*pOptions)[options::statistics] && pStatistics != NULL) {
       pStatistics->flushInformation(cerr);
     }
     set_terminate(default_terminator);
@@ -169,7 +169,7 @@ void cvc4unexpected() {
   }
 #else /* CVC4_DEBUG */
   fprintf(stderr, "CVC4 threw an \"unexpected\" exception.\n");
-  if(pOptions->statistics && pStatistics != NULL) {
+  if((*pOptions)[options::statistics] && pStatistics != NULL) {
     pStatistics->flushInformation(cerr);
   }
   set_terminate(default_terminator);
@@ -182,7 +182,7 @@ void cvc4terminate() {
           "CVC4 was terminated by the C++ runtime.\n"
           "Perhaps an exception was thrown during stack unwinding.  "
           "(Don't do that.)\n");
-  if(pOptions->statistics && pStatistics != NULL) {
+  if((*pOptions)[options::statistics] && pStatistics != NULL) {
     pStatistics->flushInformation(cerr);
   }
   default_terminator();
@@ -190,7 +190,7 @@ void cvc4terminate() {
   fprintf(stderr,
           "CVC4 was terminated by the C++ runtime.\n"
           "Perhaps an exception was thrown during stack unwinding.\n");
-  if(pOptions->statistics && pStatistics != NULL) {
+  if((*pOptions)[options::statistics] && pStatistics != NULL) {
     pStatistics->flushInformation(cerr);
   }
   default_terminator();