Added internal support for constant arrays.

1 files changed, 12 insertions, 10 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index b943a7ee5..ed56890ae 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -501,16 +501,18 @@ void TheoryEngine::combineTheories() {
     // We need to split on it
     Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl;
     lemma(equality.orNode(equality.notNode()), false, false, false, carePair.theory);
-    if (true) {
-      if (es == EQUALITY_TRUE || es == EQUALITY_TRUE_IN_MODEL) {
-        Node e = ensureLiteral(equality);
-        d_propEngine->requirePhase(e, true);
-      }
-      else if (es == EQUALITY_FALSE_IN_MODEL) {
-        Node e = ensureLiteral(equality);
-        d_propEngine->requirePhase(e, false);
-      }
-    }
+    // This code is supposed to force preference to follow what the theory models already have
+    // but it doesn't seem to make a big difference - need to explore more -Clark
+    // if (true) {
+    //   if (es == EQUALITY_TRUE || es == EQUALITY_TRUE_IN_MODEL) {
+    //     Node e = ensureLiteral(equality);
+    //     d_propEngine->requirePhase(e, true);
+    //   }
+    //   else if (es == EQUALITY_FALSE_IN_MODEL) {
+    //     Node e = ensureLiteral(equality);
+    //     d_propEngine->requirePhase(e, false);
+    //   }
+    // }
   }
 }