From c1ddfb10d4e8ed7ae1738647a67d28edb4ccdb55 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Tue, 13 Nov 2012 02:28:05 +0000 Subject: Fixed an array rewriting bug found by fuzzer --- src/theory/arrays/theory_arrays_rewriter.h | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index dbbfd04dd..62782f90e 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -344,7 +344,14 @@ public: elements.push_back(store[2]); store = store[0]; } - n = nm->mkNode(kind::STORE, store, index, value); + if (value.getKind() == kind::SELECT && + value[0] == store && + value[1] == index) { + n = store; + } + else { + n = nm->mkNode(kind::STORE, store, index, value); + } while (!indices.empty()) { n = nm->mkNode(kind::STORE, n, indices.back(), elements.back()); indices.pop_back(); -- cgit v1.2.3