Worked on the Z3Prover/z3 repository to address an internal bug related to user-defined properties and propagation decisions within the solver. Focused on refactoring the user_prop_decide function to utilize t_ref, and introduced a decide attribute to the UserPropagateBase class to clarify and stabilize propagation logic. This Python-based development improved the reliability of propagation for downstream users who rely on custom properties in solver workflows. The work required a strong understanding of solver development and API design, resulting in enhanced robustness and reduced propagation-related issues for users extending Z3 with their own property definitions and propagation strategies.