From e011aead11e75329a3d7ff754c3bcc848ade27f9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 17 Jun 2026 10:06:43 -0600 Subject: [PATCH] perf Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_derive.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp index 30153999e..6a95f2797 100644 --- a/src/ast/rewriter/seq_derive.cpp +++ b/src/ast/rewriter/seq_derive.cpp @@ -57,6 +57,7 @@ namespace seq { // Reset only operation caches (union/inter/concat/complement) // while preserving derivative caches (m_cache, m_top_cache) + // The op cache does index on m_ele so it has to be reset if m_ele changes. void derive::reset_op_caches() { m_union_cache.reset(); m_inter_cache.reset(); @@ -81,8 +82,9 @@ namespace seq { result = cached; return result; } - // Cache and pin the final result + // Pin ele and r m_trail.push_back(ele); + m_trail.push_back(r); // Always compute the SYMBOLIC derivative wrt the canonical // variable v (so the cached result is reusable for any @@ -100,7 +102,7 @@ namespace seq { result = derive_rec(r); m_top_cache.insert(ele, r, result); - m_trail.push_back(r); + // pin the final result m_trail.push_back(result); return result; }