Fix lazy initialization of maximize_ac_sharing causing inconsistent behavior

[Copilot]

The maximize_ac_sharing rewriter was initialized lazily in push_scope() rather than eagerly in the constructor. Queries without (push 1) never initialized the rewriter, leaving m_kinds empty and causing all rewrites to fail.

Changes

• maximize_ac_sharing.h: Moved init() from private to protected visibility
• maximize_ac_sharing.cpp: Added init() call to maximize_bv_sharing constructor

The init() method is idempotent (guarded by m_init flag), so calling it in both constructor and push_scope() is safe. Initialization cost is negligible—just registers 4 operator kinds (BADD, BMUL, BOR, BAND).

maximize_bv_sharing::maximize_bv_sharing(ast_manager & m):
    maximize_ac_sharing(m),
    m_util(m) {
    init();  // Ensure rewriter is always initialized
}

This ensures consistent AC sharing optimization regardless of whether queries use push/pop scoping.

Original prompt

---

This section details on the original issue you should resolve

<issue_title>Why is maximize_ac_sharing initialized lazily?</issue_title>
<issue_description>This (somewhat reduced) query from the Mariposa benchmark is unknown, and becomes unsat when I comment out the (push 1). Interestingly, this behavior persists even when I run Z3 with combined_solver.ignore_solver1=true, so both versions of the query use the incremental solver.

After some debugging, I have found that the two versions first start diverging due to a missing rewrite on the version without the (push 1) , and that this is because the maximize_ac_sharing rewriter in initialized in its push_scope handler, and not in the constructor. Moving the call to init() into the constructor makes both versions return unknown.

I suppose one could argue that it is reasonable for the solver to behave differently in response to the push, as this is very much the case with the combined solver. But I am still curious about what motivated the choice to initialize maximize_ac_sharing lazily. Is it particularly expensive to initialize?

</issue_description>

Comments on the Issue (you are @copilot in this section)

• Fixes Why is maximize_ac_sharing initialized lazily? #8062

---

💡 You can make Copilot smarter by setting up custom instructions, customizing its development environment and configuring Model Context Protocol (MCP) servers. Learn more Copilot coding agent tips in the docs.