From ff3efb7f258c04a3371e28da3558451a4c81f000 Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Tue, 21 Oct 2014 13:03:40 -0700
Subject: [PATCH] Fixed bug 590, added regression test

---
 src/theory/arrays/theory_arrays.cpp      | 21 ++++++++-
 test/regress/regress0/Makefile.am        |  3 +-
 test/regress/regress0/bug590.smt2        | 60 ++++++++++++++++++++++++
 test/regress/regress0/bug590.smt2.expect |  2 +
 4 files changed, 83 insertions(+), 3 deletions(-)
 create mode 100644 test/regress/regress0/bug590.smt2
 create mode 100644 test/regress/regress0/bug590.smt2.expect

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index cf0eeb14b..13314b46e 100644
--- 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 e7b8e3b73..11d0647bc 100644
--- 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
index 000000000..d5bd7fd56
--- /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 = {
+;    "&": "&amp;",
+;    '"': "&quot;",
+;    "'": "&apos;",
+;    ">": "&gt;",
+;    "<": "&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
index 000000000..67f25bb72
--- /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 "&lt;")))
-- 
2.30.2