Minor change to F-Length inference in strings. No internal tracking of cardinality assertions in uf. Change fullModel false array collectModelInfo to assign constants.

1 files changed, 5 insertions, 3 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 8f1ba5fca..631785437 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -1133,7 +1133,7 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel )
   TypeSet defaultValuesSet;
 
   // Compute all default values already in use
-  if (fullModel) {
+  //if (fullModel) {
     for (size_t i=0; i<arrays.size(); ++i) {
       TNode nrep = d_equalityEngine.getRepresentative(arrays[i]);
       d_mayEqualEqualityEngine.addTerm(nrep); // add the term in case it isn't there already
@@ -1143,14 +1143,14 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel )
         defaultValuesSet.add(nrep.getType().getArrayConstituentType(), (*it).second);
       }
     }
-  }
+  //}
 
   // Loop through all array equivalence classes that need a representative computed
   for (size_t i=0; i<arrays.size(); ++i) {
     TNode n = arrays[i];
     TNode nrep = d_equalityEngine.getRepresentative(n);
 
-    if (fullModel) {
+    //if (fullModel) {
       // Compute default value for this array - there is one default value for every mayEqual equivalence class
       TNode mayRep = d_mayEqualEqualityEngine.getRepresentative(nrep);
       it = d_defValues.find(mayRep);
@@ -1171,6 +1171,7 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel )
 
       // Build the STORE_ALL term with the default value
       rep = nm->mkConst(ArrayStoreAll(nrep.getType().toType(), rep.toExpr()));
+      /*
     }
     else {
       std::hash_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(n);
@@ -1182,6 +1183,7 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel )
         rep = (*it).second;
       }
     }
+*/
 
     // For each read, require that the rep stores the right value
     vector<Node>& reads = selects[nrep];