Fix non-idempotent rewrite in Array rewriter

This commit fixes bug 637 (
http://church.cims.nyu.edu/bugzilla3/show_bug.cgi?id=637 ) as
proposed in Bugzilla and adds the minified test case to the
regression tests.

diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index de10a861bd3cd8444b9e0e7fdf7389af77ecbce3..2726f386bcadd9a6e69cc134f95b2ec2f35294db 100644 (file)
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -370,8 +370,9 @@ public:
               indices.pop_back();
               elements.pop_back();
             }
+            Assert(n != node);
             Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n << std::endl;
-            return RewriteResponse(REWRITE_DONE, n);
+            return RewriteResponse(REWRITE_AGAIN, n);
           }
         }
         break;

diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am
index 19aab3e551e7232f85f4503dd03089322124a5e8..b974bc95e1eb06e4f768f0a52a49da4524a3487e 100644 (file)
--- a/test/regress/regress0/arrays/Makefile.am
+++ b/test/regress/regress0/arrays/Makefile.am
@@ -48,7 +48,8 @@ TESTS =       \
        constarr.cvc \
        constarr2.cvc \
        constarr3.cvc \
-       parsing_ringer.cvc
+       parsing_ringer.cvc \
+       bug637.delta.smt2
 
 EXTRA_DIST = $(TESTS)
 

diff --git a/test/regress/regress0/arrays/bug637.delta.smt2 b/test/regress/regress0/arrays/bug637.delta.smt2
new file mode 100644 (file)
index 0000000..45e09f2
--- /dev/null
+++ b/test/regress/regress0/arrays/bug637.delta.smt2
@@ -0,0 +1,14 @@
+(set-logic QF_ABV)
+(set-info :status unsat)
+(declare-fun x2 () (_ BitVec 32))
+(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
+(declare-fun x3 () (_ BitVec 32))
+
+(assert (not (=
+(store (store (store a x2 (select a (bvadd x2 (_ bv1 32))))
+             (bvadd x2 (_ bv1 32)) (select a (bvadd x2 (_ bv1 32))))
+       x2 (select a x2))
+
+       a)))
+(check-sat)
+(exit)