3 files changed, 12 insertions, 2 deletions
diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am
index e4c814660..8b8a5bd48 100644
--- a/src/theory/arrays/Makefile.am
+++ b/src/theory/arrays/Makefile.am
@@ -22,4 +22,5 @@ libarrays_la_SOURCES = \
 	theory_arrays_model.h \
 	theory_arrays_model.cpp
 
-EXTRA_DIST = kinds
+EXTRA_DIST = \
+	kinds
diff --git a/src/theory/arrays/options b/src/theory/arrays/options
new file mode 100644
index 000000000..bf8afc589
--- /dev/null
+++ b/src/theory/arrays/options
@@ -0,0 +1,8 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module ARRAYS "theory/arrays/options.h" Arrays theory
+
+endmodule
diff --git a/src/theory/arrays/theory_arrays_instantiator.cpp b/src/theory/arrays/theory_arrays_instantiator.cpp
index 67c42d124..f5a722737 100644
--- a/src/theory/arrays/theory_arrays_instantiator.cpp
+++ b/src/theory/arrays/theory_arrays_instantiator.cpp
@@ -17,6 +17,7 @@
 #include "theory/theory_engine.h"
 #include "theory/arrays/theory_arrays_instantiator.h"
 #include "theory/arrays/theory_arrays.h"
+#include "theory/quantifiers/options.h"
 #include "theory/rr_candidate_generator.h"
 
 using namespace std;
@@ -38,7 +39,7 @@ void InstantiatorTheoryArrays::preRegisterTerm( Node t ){
 void InstantiatorTheoryArrays::assertNode( Node assertion ){
   Debug("quant-arrays-assert") << "InstantiatorTheoryArrays::assertNode: " << assertion << std::endl;
   d_quantEngine->addTermToDatabase( assertion );
-  if( Options::current()->cbqi ){
+  if( options::cbqi() ){
     if( assertion.hasAttribute(InstConstantAttribute()) ){
       setHasConstraintsFrom( assertion.getAttribute(InstConstantAttribute()) );
     }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){