From 165a4a42bc80f3293c943b40841cb588817557ab Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Tue, 7 Jul 2026 13:26:44 -0700
Subject: [PATCH] Fix debug-only well-sorted traversal freeing temporary
 assertions (#10067)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The Ubuntu `python make - MT` job was failing in unit tests because the
debug-time well-sorted check could invalidate freshly constructed
assertion expressions during solver entry. This surfaced as crashes in
`theory_dl` and `seq_rewriter`, not as logic bugs in those tests.

- **Root cause**
- `is_well_sorted` traversed the input through a temporary
`expr_ref`/`subterms` wrapper.
- For freshly built assertions passed directly into `assert_expr`, that
temporary ownership could drop the last refcount during validation and
free the AST before the solver used it.

- **Change**
- Reworked the traversal in `src/ast/well_sorted.cpp` to walk raw
`expr*` nodes explicitly.
- The checker now validates subterms without taking transient ownership
of the asserted expression.

- **Effect**
  - Debug validation remains intact.
- Temporary formulas survive the well-sorted check, so assertion-time
validation no longer corrupts the caller’s AST.

- **Representative change**
  ```cpp
  ptr_vector<expr> todo;
  expr_mark visited;
  todo.push_back(e);
  while (!todo.empty()) {
      expr* term = todo.back();
      todo.pop_back();
      if (visited.is_marked(term))
          continue;
      visited.mark(term, true);
      if (is_app(term)) {
          for (expr* arg : *to_app(term))
              if (!visited.is_marked(arg))
                  todo.push_back(arg);
          check_app(to_app(term));
      }
      else if (is_var(term)) {
          check_var(to_var(term));
      }
      else if (is_quantifier(term)) {
          check_quantifier(to_quantifier(term));
      }
  }
  ```

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
---
 src/ast/well_sorted.cpp | 23 ++++++++++++++++++-----
 1 file changed, 18 insertions(+), 5 deletions(-)

diff --git a/src/ast/well_sorted.cpp b/src/ast/well_sorted.cpp
index a498b0dae5..3fe519369d 100644
--- a/src/ast/well_sorted.cpp
+++ b/src/ast/well_sorted.cpp
@@ -36,13 +36,27 @@ struct well_sorted_proc {
     well_sorted_proc(ast_manager & m):m(m), m_error(false) {}
 
     void check(expr* e) {
-        for (auto term : subterms::ground(expr_ref(e, m))) {
-            if (is_app(term))
+        ptr_vector<expr> todo;
+        expr_mark visited;
+        todo.push_back(e);
+        while (!todo.empty()) {
+            expr* term = todo.back();
+            todo.pop_back();
+            if (visited.is_marked(term))
+                continue;
+            visited.mark(term, true);
+            if (is_app(term)) {
+                for (expr* arg : *to_app(term))
+                    if (!visited.is_marked(arg))
+                        todo.push_back(arg);
                 check_app(to_app(term));
-            else if (is_var(term))
+            }
+            else if (is_var(term)) {
                 check_var(to_var(term));
-            else if (is_quantifier(term))
+            }
+            else if (is_quantifier(term)) {
                 check_quantifier(to_quantifier(term));
+            }
         }
     }
 
@@ -119,4 +133,3 @@ bool is_well_sorted(ast_manager const & m, expr * n) {
     return !p.m_error;
 }
 
-