Fix for bug543

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 7569b3e932e4f54db27541fdd5ad2f98fa2205e0..caeae891fca00cf5bd6edd1ed554b15084858535 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -727,7 +727,7 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel )
           termSet.insert(r);
         }
         else if (!computeRep) {
-          arrays.push_back(eqc);
+          arrays.push_back(n);
           computeRep = true;
         }
       }
@@ -818,15 +818,16 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel )
   // 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) {
       // Compute default value for this array - there is one default value for every mayEqual equivalence class
-      d_mayEqualEqualityEngine.addTerm(n); // add the term in case it isn't there already
-      TNode mayRep = d_mayEqualEqualityEngine.getRepresentative(n);
+      d_mayEqualEqualityEngine.addTerm(nrep); // add the term in case it isn't there already
+      TNode mayRep = d_mayEqualEqualityEngine.getRepresentative(nrep);
       it = defValues.find(mayRep);
       // If this mayEqual EC doesn't have a default value associated, get the next available default value for the associated array element type
       if (it == defValues.end()) {
-        TypeNode valueType = n.getType().getArrayConstituentType();
+        TypeNode valueType = nrep.getType().getArrayConstituentType();
         rep = defaultValuesSet.nextTypeEnum(valueType);
         if (rep.isNull()) {
           Assert(defaultValuesSet.getSet(valueType)->begin() != defaultValuesSet.getSet(valueType)->end());
@@ -840,7 +841,7 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel )
       }
 
       // Build the STORE_ALL term with the default value
-      rep = nm->mkConst(ArrayStoreAll(n.getType().toType(), rep.toExpr()));
+      rep = nm->mkConst(ArrayStoreAll(nrep.getType().toType(), rep.toExpr()));
     }
     else {
       std::hash_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(n);
@@ -854,7 +855,7 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel )
     }
 
     // For each read, require that the rep stores the right value
-    vector<Node>& reads = selects[n];
+    vector<Node>& reads = selects[nrep];
     for (unsigned j = 0; j < reads.size(); ++j) {
       rep = nm->mkNode(kind::STORE, rep, reads[j][1], reads[j]);
     }

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 3c9ec7eb0b8ea597b22692bacd6064cf56eaae84..d65fd20c5923d417850466b885e9c950dc038658 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -156,6 +156,7 @@ BUG_TESTS = \
        bug522.smt2 \
        bug528a.smt2 \
        bug541.smt2 \
+       bug543.smt2 \
        bug544.smt2 \
        bug548a.smt2 \
        bug567.smt2

diff --git a/test/regress/regress0/bug543.smt2 b/test/regress/regress0/bug543.smt2
new file mode 100644 (file)
index 0000000..9155de7
--- /dev/null
+++ b/test/regress/regress0/bug543.smt2
@@ -0,0 +1,20 @@
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+(set-option :produce-models true)
+(set-logic QF_ALL_SUPPORTED)
+(declare-fun _substvar_1807_ () Bool)
+(declare-fun local_id_x$1 () (_ BitVec 32))
+(declare-fun local_id_x$2 () (_ BitVec 32))
+(declare-fun $$_ZZ19bitonic_sort_kernelPfjjE7sh_data@5 () (Array Bool (Array (_ BitVec 32) (_ BitVec 32))))
+(declare-fun $$_ZZ19bitonic_sort_kernelPfjjE7sh_data () (Array Bool (Array (_ BitVec 32) (_ BitVec 32))))
+(declare-fun $0$1@2 () (_ BitVec 32))
+(declare-fun $$_ZZ19bitonic_sort_kernelPfjjE7sh_data@0 () (Array Bool (Array (_ BitVec 32) (_ BitVec 32))))
+(declare-fun v1$1@0 () (_ BitVec 32))
+(declare-fun $$_ZZ19bitonic_sort_kernelPfjjE7sh_data@1 () (Array Bool (Array (_ BitVec 32) (_ BitVec 32))))
+(declare-fun v1$2@0 () (_ BitVec 32))
+(assert (not (= #b1 #b0)))
+(define-fun $_Z19bitonic_sort_kernelPfjj () Bool (=> true (let ((__partitioned_block_$truebb_0$7_correct (=> true (=> true (=> (and true true (= $$_ZZ19bitonic_sort_kernelPfjjE7sh_data@5 (store $$_ZZ19bitonic_sort_kernelPfjjE7sh_data true (store (select $$_ZZ19bitonic_sort_kernelPfjjE7sh_data true) local_id_x$1 $0$1@2))) true true) false))))) (let ((inline$_UPDATE_WRITE_READ_BENIGN_FLAG_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$1$_UPDATE_BENIGN_FLAG_correct (=> true (=> true __partitioned_block_$truebb_0$7_correct)))) (let ((inline$_LOG_WRITE_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$1$_LOG_WRITE_correct (=> true (=> true inline$_UPDATE_WRITE_READ_BENIGN_FLAG_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$1$_UPDATE_BENIGN_FLAG_correct)))) (let ((inline$_LOG_WRITE_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$1$Entry_correct (=> true (=> true inline$_LOG_WRITE_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$1$_LOG_WRITE_correct)))) (let ((inline$$bugle_barrier$1$anon8_Then_correct (=> true (=> true inline$_LOG_WRITE_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$1$Entry_correct)))) (let ((inline$$bugle_barrier$1$anon3_correct (=> true (=> true (=> true (=> true inline$$bugle_barrier$1$anon8_Then_correct)))))) (let ((inline$$bugle_barrier$1$anon7_Then_correct (=> true (=> true inline$$bugle_barrier$1$anon3_correct)))) (let ((inline$$bugle_barrier$1$anon6_Else_correct (=> true (=> true (=> true (=> true inline$$bugle_barrier$1$anon7_Then_correct)))))) (let ((inline$$bugle_barrier$1$Entry_correct (=> true (=> true (=> true inline$$bugle_barrier$1$anon6_Else_correct))))) (let ((__partitioned_block_$truebb_0$4_correct (=> true (=> true (=> true inline$$bugle_barrier$1$Entry_correct))))) (let ((inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$4$_LOG_READ_correct (=> true (=> true __partitioned_block_$truebb_0$4_correct)))) (let ((inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$4$Entry_correct (=> true (=> true (=> true inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$4$_LOG_READ_correct))))) (let ((__partitioned_block_$truebb_0$3_correct (=> true (=> true (=> true inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$4$Entry_correct))))) (let ((inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$3$_LOG_READ_correct (=> true (=> true __partitioned_block_$truebb_0$3_correct)))) (let ((inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$3$Entry_correct (=> true (=> true inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$3$_LOG_READ_correct)))) (let ((__partitioned_block_$truebb_0$2_correct (=> true (=> true inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$3$Entry_correct)))) (let ((inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$2$_LOG_READ_correct (=> true (=> true __partitioned_block_$truebb_0$2_correct)))) (let ((inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$2$Entry_correct (=> true (=> true (=> true inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$2$_LOG_READ_correct))))) (let ((__partitioned_block_$truebb_0$1_correct (=> true (=> true (=> true inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$2$Entry_correct))))) (let ((inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$1$_LOG_READ_correct (=> true (=> true __partitioned_block_$truebb_0$1_correct)))) (let ((inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$1$Entry_correct (=> true (=> true (=> true inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$1$_LOG_READ_correct))))) (let ((__partitioned_block_$truebb_0_correct (=> true (=> true inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$1$Entry_correct)))) (let (($1_correct (=> true (=> true (=> true (=> true (=> true __partitioned_block_$truebb_0_correct))))))) (let ((__partitioned_block_$0_0$4_correct (=> true (=> true (=> true (=> true (=> true (=> true (=> true (and _substvar_1807_ (=> true (=> true (=> true (=> true (=> true (=> true (=> true (=> true (=> true (=> true (=> true (=> true (=> true (=> true (=> true (=> true (=> true (=> true $1_correct)))))))))))))))))))))))))))) (let ((inline$$bugle_barrier$0$Return_correct (=> true (=> true __partitioned_block_$0_0$4_correct)))) (let ((inline$$bugle_barrier$0$anon8_Else_correct (=> true (=> true inline$$bugle_barrier$0$Return_correct)))) (let ((inline$$bugle_barrier$0$anon3_correct (=> true (=> true (=> true (=> true inline$$bugle_barrier$0$anon8_Else_correct)))))) (let ((inline$$bugle_barrier$0$anon7_Then_correct (=> true (=> true inline$$bugle_barrier$0$anon3_correct)))) (let ((inline$$bugle_barrier$0$anon6_Else_correct (=> true (=> true (=> true (=> true inline$$bugle_barrier$0$anon7_Then_correct)))))) (let ((inline$$bugle_barrier$0$Entry_correct (=> true (=> true (=> true inline$$bugle_barrier$0$anon6_Else_correct))))) (let ((__partitioned_block_$0_0$3_correct (=> true (=> true (=> (and true true (= $$_ZZ19bitonic_sort_kernelPfjjE7sh_data@0 (store $$_ZZ19bitonic_sort_kernelPfjjE7sh_data true (store (select $$_ZZ19bitonic_sort_kernelPfjjE7sh_data true) local_id_x$1 v1$1@0))) (= $$_ZZ19bitonic_sort_kernelPfjjE7sh_data@1 (store $$_ZZ19bitonic_sort_kernelPfjjE7sh_data@0 false (store (select $$_ZZ19bitonic_sort_kernelPfjjE7sh_data@0 false) local_id_x$2 v1$2@0))) true) inline$$bugle_barrier$0$Entry_correct))))) (let ((inline$_UPDATE_WRITE_READ_BENIGN_FLAG_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$0$_UPDATE_BENIGN_FLAG_correct (=> true (=> true __partitioned_block_$0_0$3_correct)))) (let ((inline$_LOG_WRITE_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$0$_LOG_WRITE_correct (=> true (=> true inline$_UPDATE_WRITE_READ_BENIGN_FLAG_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$0$_UPDATE_BENIGN_FLAG_correct)))) (let ((inline$_LOG_WRITE_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$0$Entry_correct (=> true (=> true inline$_LOG_WRITE_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$0$_LOG_WRITE_correct)))) (let ((__partitioned_block_$0_0$1_correct (=> true (=> true (=> true inline$_LOG_WRITE_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$0$Entry_correct))))) (let ((inline$_LOG_READ_$$data$0$_LOG_READ_correct (=> true (=> true __partitioned_block_$0_0$1_correct)))) (let ((inline$_LOG_READ_$$data$0$Entry_correct (=> true (=> true inline$_LOG_READ_$$data$0$_LOG_READ_correct)))) (let ((__partitioned_block_$0_0_correct (=> true (=> true (=> true inline$_LOG_READ_$$data$0$Entry_correct))))) (let ((PreconditionGeneratedEntry_correct (=> true (=> true (=> true __partitioned_block_$0_0_correct))))) PreconditionGeneratedEntry_correct)))))))))))))))))))))))))))))))))))))))))
+(push 1)
+(assert (not (=> true $_Z19bitonic_sort_kernelPfjj)))
+(check-sat)
+