From 7dc25e73d545dcfd1d4b077d01ca08402b93b9d5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 3 Jun 2026 11:41:37 -0700
Subject: [PATCH] make reset private

---
 src/ast/rewriter/seq_derive.cpp | 2 ++
 src/ast/rewriter/seq_derive.h   | 4 ++--
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp
index 5e7a82ced..cce202f92 100644
--- a/src/ast/rewriter/seq_derive.cpp
+++ b/src/ast/rewriter/seq_derive.cpp
@@ -47,6 +47,8 @@ namespace seq {
 
     expr_ref derive::operator()(expr* ele, expr* r) {
         SASSERT(m_util.is_re(r));
+        if (m_trail.size() > 1000)
+            reset();
         m_ele = ele;
         m_depth = 0;
         expr_ref result = derive_rec(r);
diff --git a/src/ast/rewriter/seq_derive.h b/src/ast/rewriter/seq_derive.h
index 27a7819c5..183fc8ae4 100644
--- a/src/ast/rewriter/seq_derive.h
+++ b/src/ast/rewriter/seq_derive.h
@@ -107,6 +107,8 @@ namespace seq {
         sort* seq_sort(expr* r) { sort* s = nullptr; m_util.is_re(r, s); return s; }
         sort* ele_sort(expr* r) { sort* s = seq_sort(r); sort* e = nullptr; m_util.is_seq(s, e); return e; }
 
+        void reset();
+
     public:
         derive(ast_manager& m);
 
@@ -121,8 +123,6 @@ namespace seq {
          * Convenience: symbolic derivative using de Bruijn var 0.
          */
         expr_ref operator()(expr* r);
-
-        void reset();
     };
 
 }