Fixed bug 590, added regression test

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index cf0eeb14bf2c0a3912ad54d213bb29856b1b40bc..13314b46e1b5e9d2d8ba9b43736390e22dde06ee 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -477,7 +477,21 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
 
     TNode a = d_equalityEngine.getRepresentative(node[0]);
 
-    d_mayEqualEqualityEngine.assertEquality(node.eqNode(a), true, d_true);
+    if (node.isConst()) {
+      // Can't use d_mayEqualEqualityEngine to merge node with a because they are both constants,
+      // so just set the default value manually for node.
+      Assert(a == node[0]);
+      d_mayEqualEqualityEngine.addTerm(node);
+      Assert(d_mayEqualEqualityEngine.getRepresentative(node) == node);
+      Assert(d_mayEqualEqualityEngine.getRepresentative(a) == a);
+      DefValMap::iterator it = d_defValues.find(a);
+      Assert(it != d_defValues.end());
+      d_defValues[node] = (*it).second;
+    }
+    else {
+      d_mayEqualEqualityEngine.assertEquality(node.eqNode(a), true, d_true);
+      Assert(d_mayEqualEqualityEngine.consistent());
+    }
 
     if (!options::arraysLazyRIntro1()) {
       TNode i = node[1];
@@ -887,7 +901,9 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel )
       rep = nm->mkNode(kind::STORE, rep, reads[j][1], reads[j]);
     }
     m->assertEquality(n, rep, true);
-    m->assertRepresentative(rep);
+    if (!n.isConst()) {
+      m->assertRepresentative(rep);
+    }
   }
 }
 
@@ -2097,6 +2113,7 @@ void TheoryArrays::mergeArrays(TNode a, TNode b)
       defValue = (*it2).second;
     }
     d_mayEqualEqualityEngine.assertEquality(a.eqNode(b), true, d_true);
+    Assert(d_mayEqualEqualityEngine.consistent());
     if (!defValue.isNull()) {
       mayRepA = d_mayEqualEqualityEngine.getRepresentative(a);
       d_defValues[mayRepA] = defValue;

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index e7b8e3b737962988193d0f8c60bb667649ef0c91..11d0647bc263fdf139144f9b65f2d0a001d2941b 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -165,7 +165,8 @@ BUG_TESTS = \
        bug576a.smt2 \
        bug578.smt2 \
        bug585.cvc \
-       bug586.cvc
+       bug586.cvc \
+       bug590.smt2
 
 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 

diff --git a/test/regress/regress0/bug590.smt2 b/test/regress/regress0/bug590.smt2
new file mode 100644 (file)
index 0000000..d5bd7fd
--- /dev/null
+++ b/test/regress/regress0/bug590.smt2
@@ -0,0 +1,60 @@
+(set-logic QF_ALL_SUPPORTED)
+(set-option :strings-exp true)
+(set-option :produce-models true)
+(set-info :status sat)
+
+(declare-fun text () String)
+(declare-fun output () String)
+
+; html_escape_table = {
+;    "&": "&",
+;    '"': """,
+;    "'": "'",
+;    ">": ">",
+;    "<": "&lt;",
+;    }
+(declare-fun html_escape_table () (Array String String))
+(assert (= html_escape_table 
+    (store (store (store (store (store ((as const (Array String String)) "A") 
+    "&" "&amp;") 
+    "\"" "&quot;")
+    "'" "&apos;") 
+    ">" "&gt;") 
+    "<" "&lt;")))
+(declare-fun html_escape_table_keys () (Array Int String))
+(assert (= html_escape_table_keys
+    (store (store (store (store (store ((as const (Array Int String)) "B")
+    0 "&")
+    1 "\"")
+    2 "'")
+    3 ">")
+    4 "<"))) 
+
+; charlst = [c for c in text]
+(declare-fun charlst () (Array Int String))
+(declare-fun charlstlen () Int)
+(assert (= charlstlen (str.len text)))
+(assert (forall ((i Int))
+    (= (select charlst i) (str.at text i))
+))
+
+; charlst2 = [html_escape_table.get(c, c) for c in charlst]
+(declare-fun charlst2 () (Array Int String))
+(declare-fun charlstlen2 () Int)
+(assert (= charlstlen2 charlstlen))
+(assert (forall ((i Int))
+    (or (or (< i 0) (>= i charlstlen2))
+        (and (exists ((j Int))
+               (= (select html_escape_table_keys j) (select charlst i))
+            )
+            (= (select charlst2 i) (select html_escape_table (select charlst i)))         
+        )
+        (and (not (exists ((j Int))
+                (= (select html_escape_table_keys j) (select charlst i))
+            ))
+            (= (select charlst2 i) (select charlst i))
+        )                        
+    )
+))
+(check-sat)
+(get-value (charlst2))

diff --git a/test/regress/regress0/bug590.smt2.expect b/test/regress/regress0/bug590.smt2.expect
new file mode 100644 (file)
index 0000000..67f25bb
--- /dev/null
+++ b/test/regress/regress0/bug590.smt2.expect
@@ -0,0 +1,2 @@
+% EXPECT: sat
+% EXPECT: ((charlst2 (store ((as const (Array Int String)) "C") 0 "<")))