From: Andres Noetzli <noetzli@stanford.edu>
Date: Wed, 4 Jan 2017 17:20:34 +0000 (-0800)
Subject: Fix non-idempotent rewrite in Array rewriter
X-Git-Tag: cvc5-1.0.0~5912
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a8a7949ec3e1a7f2a2d241d0fc58e08cbf4b7aec;p=cvc5.git

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 de10a861b..2726f386b 100644
--- 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 19aab3e55..b974bc95e 100644
--- 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
index 000000000..45e09f261
--- /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)