From 8ad9766a5e873e1b51e6197567fdd1ec296bc9a4 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 12 Dec 2025 09:00:20 +0000
Subject: [PATCH 1/2] Initial plan


From 06e38fb0b9f253c78a95821842b277988de39ce6 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 12 Dec 2025 09:23:37 +0000
Subject: [PATCH 2/2] Fix lazy initialization of maximize_ac_sharing rewriter

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/ast/rewriter/maximize_ac_sharing.cpp |  1 +
 src/ast/rewriter/maximize_ac_sharing.h   | 17 ++++++++---------
 2 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/src/ast/rewriter/maximize_ac_sharing.cpp b/src/ast/rewriter/maximize_ac_sharing.cpp
index 6749f1c21..d72773898 100644
--- a/src/ast/rewriter/maximize_ac_sharing.cpp
+++ b/src/ast/rewriter/maximize_ac_sharing.cpp
@@ -169,4 +169,5 @@ bool maximize_bv_sharing::is_numeral(expr * n) const {
 maximize_bv_sharing::maximize_bv_sharing(ast_manager & m):
     maximize_ac_sharing(m),
     m_util(m) {
+    init();
 }
diff --git a/src/ast/rewriter/maximize_ac_sharing.h b/src/ast/rewriter/maximize_ac_sharing.h
index a2741aa89..939fcca88 100644
--- a/src/ast/rewriter/maximize_ac_sharing.h
+++ b/src/ast/rewriter/maximize_ac_sharing.h
@@ -67,6 +67,14 @@ class maximize_ac_sharing : public default_rewriter_cfg {
 
 protected:
     void register_kind(decl_kind k);
+    void init() {
+        if (!m_init) {
+            init_core();
+            m_init = true;
+        }
+    }
+    virtual void init_core() = 0; 
+    virtual bool is_numeral(expr * n) const = 0;
 
 private:
     ast_manager &     m;
@@ -80,15 +88,6 @@ private:
     bool contains(func_decl * f, expr * arg1, expr * arg2);
     void insert(func_decl * f, expr * arg1, expr * arg2);
     void restore_entries(unsigned old_lim);
-    void init() {
-        if (!m_init) {
-            init_core();
-            m_init = true;
-        }
-    }
-protected:
-    virtual void init_core() = 0; 
-    virtual bool is_numeral(expr * n) const = 0;
 public:
     maximize_ac_sharing(ast_manager & m);
     virtual ~maximize_ac_sharing();