From 56bf04e30a9cfd601b1dcb4159604e81929a02ee Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Mon, 29 Jun 2026 09:53:02 -0700
Subject: [PATCH] =?UTF-8?q?Fix=20qe-lite=20de=E2=80=AFBruijn=20reindexing?=
 =?UTF-8?q?=20after=20bounded=20quantifier=20expansion=20(#9996)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`qe-lite` could produce malformed formulas when expanding bounded
quantifiers under nested binders, leaving outer de Bruijn indices
unshifted after eliminating an inner quantifier (e.g., `(:var 1)`
escaping capture). This change fixes index normalization in that rewrite
path and adds a regression for the reported forall/exists arithmetic
case.

- **Rewrite correctness in bounded quantifier expansion**
- In `src/qe/lite/qe_lite_tactic.cpp`, after substituting bounded
variables in payload conjuncts, apply `inv_var_shifter(num_decls)` so
outer bound variables are reindexed relative to the removed binder.
- This preserves quantifier structure correctness when
`try_expand_bounded_quantifier` eliminates an inner quantifier.

- **Regression coverage for the reported pattern**
- In `src/test/smt_context.cpp`, add a focused quantified arithmetic
formula matching the bug shape:
    - outer `forall (x, x4)`
    - inner `exists (y)`
    - mixed inequalities that trigger qe-lite bounded expansion
- Assert the formula is unsatisfiable, preventing reintroduction of
invalid index handling in this path.

```c++
inst = vs(p, subst_map.size(), subst_map.data());
shift(inst, num_decls, inst); // reindex outer de Bruijn vars after eliminating inner quantifier
```

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
---
 src/qe/lite/qe_lite_tactic.cpp |  2 ++
 src/test/smt_context.cpp       | 28 ++++++++++++++++++++++++++++
 2 files changed, 30 insertions(+)

diff --git a/src/qe/lite/qe_lite_tactic.cpp b/src/qe/lite/qe_lite_tactic.cpp
index 4f234a58e7..774c619cfc 100644
--- a/src/qe/lite/qe_lite_tactic.cpp
+++ b/src/qe/lite/qe_lite_tactic.cpp
@@ -2467,6 +2467,7 @@ private:
             cur_vals[i] = var_lbs[i];
 
         var_subst vs(m, false);
+        inv_var_shifter shift(m);
         expr_ref_vector disjuncts(m);
 
         while (true) {
@@ -2479,6 +2480,7 @@ private:
             for (expr* p : payload) {
                 expr_ref inst(m);
                 inst = vs(p, subst_map.size(), subst_map.data());
+                shift(inst, num_decls, inst);
                 inst_conjs.push_back(inst);
             }
             expr_ref inst_body(m);
diff --git a/src/test/smt_context.cpp b/src/test/smt_context.cpp
index d7297c9d0a..215f3285cc 100644
--- a/src/test/smt_context.cpp
+++ b/src/test/smt_context.cpp
@@ -6,6 +6,7 @@ Copyright (c) 2015 Microsoft Corporation
 
 #include "smt/smt_context.h"
 #include "ast/reg_decl_plugins.h"
+#include "ast/arith_decl_plugin.h"
 
 void tst_smt_context()
 {
@@ -34,4 +35,31 @@ void tst_smt_context()
     }
 
     ctx.check();
+
+    {
+        arith_util a(m);
+        expr_ref x(m.mk_var(2, a.mk_int()), m);
+        expr_ref x4(m.mk_var(1, a.mk_int()), m);
+        expr_ref y(m.mk_var(0, a.mk_int()), m);
+        expr_ref zero(a.mk_int(0), m);
+        expr_ref two(a.mk_int(2), m);
+        expr_ref_vector conjs(m);
+        conjs.push_back(a.mk_gt(x, y));
+        conjs.push_back(a.mk_gt(zero, x4));
+        conjs.push_back(a.mk_gt(zero, a.mk_uminus(y)));
+        conjs.push_back(a.mk_lt(zero, a.mk_uminus(a.mk_mul(two, y))));
+        expr_ref body(m.mk_and(conjs), m);
+
+        sort* y_sort = a.mk_int();
+        symbol y_name("y");
+        body = m.mk_exists(1, &y_sort, &y_name, body);
+
+        sort* sorts[2] = { a.mk_int(), a.mk_int() };
+        symbol names[2] = { symbol("x"), symbol("x4") };
+        expr_ref q(m.mk_forall(2, sorts, names, body), m);
+
+        smt::context qctx(m, params);
+        qctx.assert_expr(q);
+        VERIFY(l_false == qctx.check());
+    }
 }