diff --git a/examples/go/test_new_apis.go b/examples/go/test_new_apis.go
index f76845471..2fe323578 100644
--- a/examples/go/test_new_apis.go
+++ b/examples/go/test_new_apis.go
@@ -44,9 +44,11 @@ func main() {
 			fmt.Printf("  NonUnit %d: %s\n", i, nu.String())
 		}
 		
-		// Note: Trail() and TrailLevels() only work with SimpleSolver
-		// For default solvers created with NewSolver(), these may not be available
-		fmt.Println("Note: Trail() and TrailLevels() are available primarily for SimpleSolver")
+		// 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")
 	}
 
 	// Test congruence closure APIs
diff --git a/src/api/go/solver.go b/src/api/go/solver.go
index fa2471a63..6fa352b2d 100644
--- a/src/api/go/solver.go
+++ b/src/api/go/solver.go
@@ -214,6 +214,8 @@ func (s *Solver) NonUnits() []*Expr {
 // Trail returns the decision trail of the solver.
 // The trail contains the sequence of literals assigned during search.
 // This is useful for understanding the solver's decision history.
+// Note: This function works primarily with SimpleSolver. For solvers created
+// using tactics (e.g., NewSolver()), it may return an error.
 func (s *Solver) Trail() []*Expr {
 	vec := C.Z3_solver_get_trail(s.ctx.ptr, s.ptr)
 	return astVectorToExprs(s.ctx, vec)
@@ -223,6 +225,8 @@ func (s *Solver) Trail() []*Expr {
 // The returned slice has the same length as the trail, where each element
 // indicates the decision level at which the corresponding trail literal was assigned.
 // This is useful for understanding the structure of the search tree.
+// Note: This function works primarily with SimpleSolver. For solvers created
+// using tactics (e.g., NewSolver()), it may return an error.
 func (s *Solver) TrailLevels() []uint {
 	// Get the trail vector directly from the C API
 	trailVec := C.Z3_solver_get_trail(s.ctx.ptr, s.ptr)
@@ -250,8 +254,8 @@ func (s *Solver) TrailLevels() []uint {
 
 // CongruenceRoot returns the congruence class representative of the given expression.
 // This returns the root element in the congruence closure for the term.
-// The function primarily works for SimpleSolver. Terms and variables that are
-// eliminated during pre-processing are not visible to the congruence closure.
+// Note: This function works primarily with SimpleSolver. Terms and variables that
+// are eliminated during pre-processing are not visible to the congruence closure.
 func (s *Solver) CongruenceRoot(expr *Expr) *Expr {
 	ast := C.Z3_solver_congruence_root(s.ctx.ptr, s.ptr, expr.ptr)
 	return newExpr(s.ctx, ast)
@@ -259,8 +263,8 @@ func (s *Solver) CongruenceRoot(expr *Expr) *Expr {
 
 // CongruenceNext returns the next element in the congruence class of the given expression.
 // This allows iteration through all elements in a congruence class.
-// The function primarily works for SimpleSolver. Terms and variables that are
-// eliminated during pre-processing are not visible to the congruence closure.
+// Note: This function works primarily with SimpleSolver. Terms and variables that
+// are eliminated during pre-processing are not visible to the congruence closure.
 func (s *Solver) CongruenceNext(expr *Expr) *Expr {
 	ast := C.Z3_solver_congruence_next(s.ctx.ptr, s.ptr, expr.ptr)
 	return newExpr(s.ctx, ast)
@@ -268,8 +272,8 @@ func (s *Solver) CongruenceNext(expr *Expr) *Expr {
 
 // CongruenceExplain returns an explanation for why two expressions are congruent.
 // The result is an expression that justifies the congruence between a and b.
-// The function primarily works for SimpleSolver. Terms and variables that are
-// eliminated during pre-processing are not visible to the congruence closure.
+// Note: This function works primarily with SimpleSolver. Terms and variables that
+// are eliminated during pre-processing are not visible to the congruence closure.
 func (s *Solver) CongruenceExplain(a, b *Expr) *Expr {
 	ast := C.Z3_solver_congruence_explain(s.ctx.ptr, s.ptr, a.ptr, b.ptr)
 	return newExpr(s.ctx, ast)