diff --git a/src/api/go/README.md b/src/api/go/README.md index 8814b72a1e..e499cea244 100644 --- a/src/api/go/README.md +++ b/src/api/go/README.md @@ -310,7 +310,7 @@ go run basic_example.go ## Memory Management -The Go bindings use `runtime.SetFinalizer` to automatically manage Z3 reference counts. You don't need to manually call inc_ref/dec_ref. However, be aware that finalizers run during garbage collection, so resources may not be freed immediately. +The Go bindings use `runtime.SetFinalizer` to automatically manage Z3 reference counts. You don't need to manually call inc_ref/dec_ref. However, be aware that finalizers run during garbage collection, so resources may not be freed immediately. The bindings enable `Z3_enable_concurrent_dec_ref` when creating contexts so finalizer-driven decref operations are safe with concurrent GC. ## Thread Safety diff --git a/src/api/go/z3.go b/src/api/go/z3.go index 4e982111e3..7c37b31332 100644 --- a/src/api/go/z3.go +++ b/src/api/go/z3.go @@ -89,6 +89,7 @@ type Context struct { // NewContext creates a new Z3 context with default configuration. func NewContext() *Context { ctx := &Context{ptr: C.Z3_mk_context_rc(C.Z3_mk_config())} + C.Z3_enable_concurrent_dec_ref(ctx.ptr) runtime.SetFinalizer(ctx, func(c *Context) { C.Z3_del_context(c.ptr) }) @@ -98,6 +99,7 @@ func NewContext() *Context { // NewContextWithConfig creates a new Z3 context with the given configuration. func NewContextWithConfig(cfg *Config) *Context { ctx := &Context{ptr: C.Z3_mk_context_rc(cfg.ptr)} + C.Z3_enable_concurrent_dec_ref(ctx.ptr) runtime.SetFinalizer(ctx, func(c *Context) { C.Z3_del_context(c.ptr) })