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>

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