From 31425b07caf6c5cc727500bc6a111a746080e63e Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Tue, 31 Mar 2026 09:48:37 -0700
Subject: [PATCH] Add SetGlobalParam, GetGlobalParam, ResetAllGlobalParams to
 Go bindings (#9179)

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/f06c74eb-4cac-45f6-92b9-b2698150074c

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/api/go/z3.go | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

diff --git a/src/api/go/z3.go b/src/api/go/z3.go
index 0d1322ea8..321870c0c 100644
--- a/src/api/go/z3.go
+++ b/src/api/go/z3.go
@@ -815,6 +815,33 @@ func (c *Context) MkLambdaConst(bound []*Expr, body *Expr) *Lambda {
 	return newLambda(c, ptr)
 }
 
+// SetGlobalParam sets a global Z3 parameter.
+func SetGlobalParam(id, value string) {
+	cID := C.CString(id)
+	cValue := C.CString(value)
+	defer C.free(unsafe.Pointer(cID))
+	defer C.free(unsafe.Pointer(cValue))
+	C.Z3_global_param_set(cID, cValue)
+}
+
+// GetGlobalParam retrieves the value of a global Z3 parameter.
+// Returns the value and true if the parameter exists, or empty string and false otherwise.
+func GetGlobalParam(id string) (string, bool) {
+	cID := C.CString(id)
+	defer C.free(unsafe.Pointer(cID))
+	var cValue C.Z3_string
+	ok := C.Z3_global_param_get(cID, &cValue)
+	if ok == C.bool(false) {
+		return "", false
+	}
+	return C.GoString(cValue), true
+}
+
+// ResetAllGlobalParams resets all global Z3 parameters to their default values.
+func ResetAllGlobalParams() {
+	C.Z3_global_param_reset_all()
+}
+
 // astVectorToExprs converts a Z3_ast_vector to a slice of Expr.
 // This function properly manages the reference count of the vector by
 // incrementing it on entry and decrementing it on exit.