More model-based combination for arrays

diff --git a/src/theory/arrays/options b/src/theory/arrays/options
index 15220fbc218e63184f5e2060fd1ca9c3ca7752e1..baf0962bfb9b4e02381ab5fb2695f427746b0c39 100644 (file)
--- a/src/theory/arrays/options
+++ b/src/theory/arrays/options
@@ -12,7 +12,7 @@ option arraysLazyRIntro1 --arrays-lazy-rintro1 bool :default true :read-write
  turn on optimization to only perform RIntro1 rule lazily (see Jovanovic/Barrett 2012: Being Careful with Theory Combination)
 
 option arraysModelBased --arrays-model-based bool :default false :read-write
- turn on model-based arrray solver
+ turn on model-based array solver
 
 option arraysEagerIndexSplitting --arrays-eager-index bool :default true :read-write
  turn on eager index splitting for generated array lemmas

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 6b91400e81244431d0dca6d6662cb02419648789..bfbf046c345a7f4364308b826365ae7371eaebc8 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -990,7 +990,9 @@ void TheoryArrays::check(Effort e) {
   if(!options::arraysEagerLemmas() && fullEffort(e) && !d_conflict && !options::arraysModelBased()) {
     // generate the lemmas on the worklist
     Trace("arrays-lem")<<"Arrays::discharging lemmas: "<<d_RowQueue.size()<<"\n";
-    dischargeLemmas();
+    while (d_RowQueue.size() > 0 && !d_conflict) {
+      dischargeLemmas();
+    }
   }
 
   Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl;

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index ffe4258cd31d4e62394aedff9063ee3c15cc73ab..b943a7ee581a44e17c5880f5ab590e54fb0e6931 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -501,8 +501,8 @@ 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 (false) {
-      if (es == EQUALITY_TRUE_IN_MODEL) {
+    if (true) {
+      if (es == EQUALITY_TRUE || es == EQUALITY_TRUE_IN_MODEL) {
         Node e = ensureLiteral(equality);
         d_propEngine->requirePhase(e, true);
       }