From 34ba2962efa7a0389124cca7391359507fea7bb9 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Thu, 21 May 2026 11:15:42 -0700
Subject: [PATCH] Fix unsound array equality rewrite for const-array store
 chains (#9572)

Z3 could return `sat` for an unsatisfiable QF_ABV formula equating two
store chains over distinct constant arrays. The rewrite path for array
equalities was missing a necessary base-value constraint in
finite-domain cases where stores cannot cover all indices.

- **Root cause**
- In `array_rewriter::mk_eq_core`, equality rewriting for nested stores
over const-array bases did not enforce equality of the underlying const
values when the index domain size exceeds the number of updated indices.

- **Rewriter fix**
  - Added a sound rewrite branch for:
    - `store* ((as const ...) v)` vs `store* ((as const ...) w)`
  - When `|domain| > (#stores_lhs + #stores_rhs)`, rewrite now includes:
    - select equalities for touched indices (existing behavior)
    - **and** base-value equality `v = w` (new requirement)
- This prevents spurious models where only updated indices are
constrained.

- **Regression coverage**
- Added a focused regression in `src/test/mod_factor.cpp` that asserts
`unsat` for a minimized constant-array/store-chain BV case with
`(distinct x y)` and one store per side.

```cpp
(assert (distinct x y))
(assert (= (store A0 i0 e0) (store A1 i1 e1)))
(check-sat) ; expected: unsat
```

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/ast/rewriter/array_rewriter.cpp | 48 ++++++++++++++++++++++-------
 src/test/mod_factor.cpp             | 25 +++++++++++++++
 2 files changed, 62 insertions(+), 11 deletions(-)

diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp
index 2e5e806fa..5d3ddf1dd 100644
--- a/src/ast/rewriter/array_rewriter.cpp
+++ b/src/ast/rewriter/array_rewriter.cpp
@@ -861,19 +861,45 @@ br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result)
         return false;        
     };
 
+    auto domain_is_larger_than = [&](sort* s, unsigned num_stores) {
+        unsigned sz = get_array_arity(s);
+        rational dsz(1);
+        for (unsigned i = 0; i < sz; ++i) {
+            sort* d = get_array_domain(s, i);
+            if (d->is_infinite())
+                return true;
+            if (d->is_very_big())
+                return false;
+            dsz *= rational(d->get_num_elements().size(), rational::ui64());
+            if (dsz > rational(num_stores, rational::ui64()))
+                return true;
+        }
+        return false;
+    };
+
+    expr* lhs1 = lhs;
+    expr* rhs1 = rhs;
+    unsigned num_lhs = 0, num_rhs = 0;
+    while (m_util.is_store(lhs1)) {
+        lhs1 = to_app(lhs1)->get_arg(0);
+        ++num_lhs;
+    }
+    while (m_util.is_store(rhs1)) {
+        rhs1 = to_app(rhs1)->get_arg(0);
+        ++num_rhs;
+    }
+
+    if (m_util.is_const(lhs1, v) && m_util.is_const(rhs1, w) &&
+        domain_is_larger_than(lhs->get_sort(), num_lhs + num_rhs)) {
+        mk_eq(lhs, lhs, rhs, fmls);
+        mk_eq(rhs, lhs, rhs, fmls);
+        fmls.push_back(m().mk_eq(v, w));
+        result = m().mk_and(fmls);
+        return BR_REWRITE_FULL;
+    }
+
 
     if (m_expand_store_eq) {
-        expr* lhs1 = lhs;
-        expr* rhs1 = rhs;
-        unsigned num_lhs = 0, num_rhs = 0;
-        while (m_util.is_store(lhs1)) {
-            lhs1 = to_app(lhs1)->get_arg(0);
-            ++num_lhs;
-        }
-        while (m_util.is_store(rhs1)) {
-            rhs1 = to_app(rhs1)->get_arg(0);
-            ++num_rhs;
-        }
         if (lhs1 == rhs1) {
             mk_eq(lhs, lhs, rhs, fmls);
             mk_eq(rhs, lhs, rhs, fmls);
diff --git a/src/test/mod_factor.cpp b/src/test/mod_factor.cpp
index 069802522..314537ca8 100644
--- a/src/test/mod_factor.cpp
+++ b/src/test/mod_factor.cpp
@@ -4,6 +4,7 @@ Copyright (c) 2025 Microsoft Corporation
 
 #include "api/z3.h"
 #include "util/util.h"
+#include <string>
 
 // x mod 7 = 0 & (x*y) mod 7 != 0 should be unsat
 // Exercises: mod internalization path (is_mod with numeric divisor)
@@ -60,7 +61,31 @@ static void test_mod_factor_idiv_path() {
     Z3_del_context(ctx);
 }
 
+static void test_const_array_store_chain_unsat() {
+    Z3_config cfg = Z3_mk_config();
+    Z3_context ctx = Z3_mk_context(cfg);
+    const char* script = R"(
+(set-logic QF_ABV)
+(declare-const x (_ BitVec 8))
+(declare-const y (_ BitVec 8))
+(define-fun A0 () (Array (_ BitVec 2) (_ BitVec 8)) ((as const (Array (_ BitVec 2) (_ BitVec 8))) x))
+(define-fun A1 () (Array (_ BitVec 2) (_ BitVec 8)) ((as const (Array (_ BitVec 2) (_ BitVec 8))) y))
+(declare-const i0 (_ BitVec 2))
+(declare-const e0 (_ BitVec 8))
+(declare-const i1 (_ BitVec 2))
+(declare-const e1 (_ BitVec 8))
+(assert (distinct x y))
+(assert (= (store A0 i0 e0) (store A1 i1 e1)))
+(check-sat)
+)";
+    std::string resp = Z3_eval_smtlib2_string(ctx, script);
+    ENSURE(resp.find("unsat") != std::string::npos);
+    Z3_del_config(cfg);
+    Z3_del_context(ctx);
+}
+
 void tst_mod_factor() {
     test_mod_factor_mod_path();
     test_mod_factor_idiv_path();
+    test_const_array_store_chain_unsat();
 }