enable arrays

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 17d0779ca276b1936b48a620785e24f3f5e2c659..4d2f502fd140b0e52bdc37c184d27ba0dbd43216 100644 (file)
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -36,8 +36,8 @@ public:
 
   void preRegisterTerm(TNode n) { Unimplemented(); }
   void registerTerm(TNode n) { Unimplemented(); }
-  void check(Effort e) { Unimplemented(); }
-  void propagate(Effort e) { Unimplemented(); }
+  void check(Effort e) {}
+  void propagate(Effort e) {}
   void explain(TNode n, Effort e) { Unimplemented(); }
   std::string identify() const { return std::string("TheoryBV"); }
 };/* class TheoryBV */

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 92008cc99086bf9ff1c55e314072257abfcafc56..24d1f4790b8ce332f750ee0f59e92ca0d723af73 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -265,7 +265,7 @@ public:
       //d_bool.check(effort);
       d_uf.check(effort);
       d_arith.check(effort);
-      //d_arrays.check(effort);
+      d_arrays.check(effort);
       //d_bv.check(effort);
     } catch(const theory::Interrupted&) {
       Debug("theory") << "TheoryEngine::check() => conflict" << std::endl;
@@ -301,8 +301,12 @@ public:
   inline void propagate() {
     d_theoryOut.d_propagatedLiterals.clear();
     // Do the propagation
+    //d_builtin.propagate(theory::Theory::FULL_EFFORT);
+    //d_bool.propagate(theory::Theory::FULL_EFFORT);
     d_uf.propagate(theory::Theory::FULL_EFFORT);
     d_arith.propagate(theory::Theory::FULL_EFFORT);
+    d_arrays.propagate(theory::Theory::FULL_EFFORT);
+    //d_bv.propagate(theory::Theory::FULL_EFFORT);
   }
 
   inline Node getExplanation(TNode node){