From bffbe2475fb970eceee1bb1a94df00dc71eaf114 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
Date: Thu, 30 Jul 2026 20:04:53 -0700
Subject: [PATCH] Fix reversed precondition assertion in grobner::pop_scope
 (#10318)

### What it does

Fixes an inverted precondition assertion in `grobner::pop_scope`
(`src/math/grobner/grobner.cpp`).

```cpp
void grobner::pop_scope(unsigned num_scopes) {
    SASSERT(num_scopes >= get_scope_level());          // was reversed
    unsigned new_lvl = get_scope_level() - num_scopes; // requires num_scopes <= level
    ...
    m_scopes.shrink(new_lvl);
}
```

`get_scope_level()` returns `m_scopes.size()` (grobner.h). The body
computes
`new_lvl = get_scope_level() - num_scopes` and calls
`m_scopes.shrink(new_lvl)`,
which is only well-defined when `num_scopes <= get_scope_level()`. The
assertion
stated the opposite (`>=`), so in debug builds it would fire on any
valid partial
pop (e.g. popping one of several scopes) while failing to catch the
unsigned
underflow it was meant to guard against. Changed to `<=`.

### Evidence

- `get_scope_level() const { return m_scopes.size(); }`
(`src/math/grobner/grobner.h`).
- Compiled the translation unit with MSVC and `Z3DEBUG` defined (so the
`SASSERT`
  is active): builds cleanly.

### What we did not verify

This is a debug-only (`SASSERT`) correctness fix and has no effect on
release
builds. No behavioral test was added.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: ad2c295d-7523-48cf-b786-b435b833e3af
---
 src/math/grobner/grobner.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/math/grobner/grobner.cpp b/src/math/grobner/grobner.cpp
index cf4e689167..e83a880595 100644
--- a/src/math/grobner/grobner.cpp
+++ b/src/math/grobner/grobner.cpp
@@ -98,7 +98,7 @@ void grobner::push_scope() {
 }
 
 void grobner::pop_scope(unsigned num_scopes) {
-    SASSERT(num_scopes >= get_scope_level());
+    SASSERT(num_scopes <= get_scope_level());
     unsigned new_lvl = get_scope_level() - num_scopes;
     scope & s        = m_scopes[new_lvl];
     unfreeze_equations(s.m_equations_to_unfreeze_lim);