From 87812a99c023eac4e62d53dadf8568473be094ab Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Tue, 17 Feb 2026 16:43:12 +0000
Subject: [PATCH] Add safety comment and improve test documentation

- Add comment about safety of &levels[0] after n > 0 check
- Improve test documentation about SimpleSolver limitations
- Clarify that Units/NonUnits are more reliable for general use

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 examples/go/test_new_apis.go | 14 +++++++++-----
 src/api/go/solver.go         |  1 +
 2 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/examples/go/test_new_apis.go b/examples/go/test_new_apis.go
index 2fe323578..cb421ce52 100644
--- a/examples/go/test_new_apis.go
+++ b/examples/go/test_new_apis.go
@@ -44,11 +44,15 @@ func main() {
 			fmt.Printf("  NonUnit %d: %s\n", i, nu.String())
 		}
 		
-		// Note: Trail() and TrailLevels() work primarily with SimpleSolver.
-		// With default solvers (created with NewSolver()), they may return
-		// errors like "cannot retrieve trail from solvers created using tactics".
-		// For those use cases, Units() and NonUnits() provide similar diagnostic info.
-		fmt.Println("Note: Trail() and TrailLevels() work primarily with SimpleSolver")
+		// Note: Trail() and TrailLevels() work primarily with SimpleSolver,
+		// which is used internally by Z3 but not directly exposed in the Go API.
+		// With default solvers (created with NewSolver()), they return errors like
+		// "cannot retrieve trail from solvers created using tactics".
+		// Units() and NonUnits() provide similar diagnostic information without
+		// this limitation and work with all solver types.
+		fmt.Println("\nNote: Trail() and TrailLevels() work primarily with SimpleSolver")
+		fmt.Println("      These functions may return errors with default solvers")
+		fmt.Println("      For general diagnostic purposes, Units() and NonUnits() are more reliable")
 	}
 
 	// Test congruence closure APIs
diff --git a/src/api/go/solver.go b/src/api/go/solver.go
index 6fa352b2d..eab330e5f 100644
--- a/src/api/go/solver.go
+++ b/src/api/go/solver.go
@@ -242,6 +242,7 @@ func (s *Solver) TrailLevels() []uint {
 	levels := make([]C.uint, n)
 
 	// Get the levels using the trail vector directly
+	// Safe to pass &levels[0] because we checked n > 0 above
 	C.Z3_solver_get_levels(s.ctx.ptr, s.ptr, trailVec, C.uint(n), &levels[0])
 
 	// Convert to Go slice