From 6d3c41143ca701c087fd6683ff11a9debd3e029c Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Mon, 16 Feb 2026 21:46:23 +0000
Subject: [PATCH] Fix duplicate example in advanced_example.go and add silent
 markers for unused vars

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 examples/go/advanced_example.go | 52 ++++++---------------------------
 1 file changed, 9 insertions(+), 43 deletions(-)

diff --git a/examples/go/advanced_example.go b/examples/go/advanced_example.go
index 0db4b6daf..2a3bc1608 100644
--- a/examples/go/advanced_example.go
+++ b/examples/go/advanced_example.go
@@ -91,6 +91,8 @@ func main() {
 	intSort := ctx.MkIntSort()
 	listSort, nilDecl, consDecl, isNilDecl, isConsDecl, headDecl, tailDecl := 
 		ctx.MkListSort("IntList", intSort)
+	// Silence unused warnings (these constructors may be needed in more complex examples)
+	_, _, _ = isNilDecl, isConsDecl, tailDecl
 	
 	// Create list: cons(1, cons(2, nil))
 	nilList := ctx.MkApp(nilDecl)
@@ -140,10 +142,12 @@ func main() {
 		"Color",
 		[]string{"Red", "Green", "Blue"},
 	)
+	_ = colorTesters // Silence unused warning
 	
 	red := ctx.MkApp(colorConsts[0])
 	green := ctx.MkApp(colorConsts[1])
 	blue := ctx.MkApp(colorConsts[2])
+	_, _ = green, blue // Silence unused warning
 	
 	c1 := ctx.MkConst(ctx.MkStringSymbol("c1"), colorSort)
 	c2 := ctx.MkConst(ctx.MkStringSymbol("c2"), colorSort)
@@ -201,18 +205,18 @@ func main() {
 	str := ctx.MkConst(ctx.MkStringSymbol("str"), ctx.MkStringSort())
 	
 	// Create regex: (a|b)*c+ (zero or more 'a' or 'b', followed by one or more 'c')
-	a := ctx.MkToRe(ctx.MkString("a"))
-	b := ctx.MkToRe(ctx.MkString("b"))
-	c := ctx.MkToRe(ctx.MkString("c"))
+	reA := ctx.MkToRe(ctx.MkString("a"))
+	reB := ctx.MkToRe(ctx.MkString("b"))
+	reC := ctx.MkToRe(ctx.MkString("c"))
 	
 	// (a|b)
-	aOrB := ctx.MkReUnion(a, b)
+	aOrB := ctx.MkReUnion(reA, reB)
 	
 	// (a|b)*
 	aOrBStar := ctx.MkReStar(aOrB)
 	
 	// c+
-	cPlus := ctx.MkRePlus(c)
+	cPlus := ctx.MkRePlus(reC)
 	
 	// (a|b)*c+
 	regex := ctx.MkReConcat(aOrBStar, cPlus)
@@ -233,44 +237,6 @@ func main() {
 		}
 	}
 
-	// Example 8: Regular expressions
-	fmt.Println("\nExample 8: Regular expressions")
-	solver.Reset()
-	
-	// Create a string variable
-	str := ctx.MkConst(ctx.MkStringSymbol("str"), ctx.MkStringSort())
-	
-	// Create regex: (a|b)*c+ (zero or more 'a' or 'b', followed by one or more 'c')
-	a := ctx.MkToRe(ctx.MkString("a"))
-	b := ctx.MkToRe(ctx.MkString("b"))
-	c := ctx.MkToRe(ctx.MkString("c"))
-	
-	// (a|b)*
-	aOrB := ctx.MkReUnion(a, b)
-	aOrBStar := ctx.MkReStar(aOrB)
-	
-	// c+
-	cPlus := ctx.MkRePlus(c)
-	
-	// (a|b)*c+
-	regex := ctx.MkReConcat(aOrBStar, cPlus)
-	
-	// Assert that string matches the regex
-	solver.Assert(ctx.MkInRe(str, regex))
-	
-	// Also assert that length is less than 10
-	strLen := ctx.MkSeqLength(str)
-	tenStr := ctx.MkInt(10, ctx.MkIntSort())
-	solver.Assert(ctx.MkLt(strLen, tenStr))
-	
-	if solver.Check() == z3.Satisfiable {
-		model := solver.Model()
-		fmt.Println("Satisfiable!")
-		if strVal, ok := model.Eval(str, true); ok {
-			fmt.Println("String matching (a|b)*c+:", strVal.String())
-		}
-	}
-
 	// Example 9: Optimization
 	fmt.Println("\nExample 9: Optimization (maximize/minimize)")