From 51cbbe0a0ea3259ec92255e86e5818d1d6a9e523 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 23 Apr 2026 17:19:48 -0700 Subject: [PATCH] fix #9293 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/array_rewriter.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index 67f969197..2e5e806fa 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -750,7 +750,10 @@ bool array_rewriter::add_store(expr_ref_vector& args, unsigned num_idxs, expr* e } if (is_var(e1) && is_ground(e2)) { unsigned idx = to_var(e1)->get_idx(); - args[num_idxs - idx - 1] = e2; + unsigned nidx = num_idxs - idx - 1; + if (args.get(nidx) && args.get(nidx) != e2) + return false; + args[nidx] = e2; } else { return false;