diff --git a/examples/go/advanced_example.go b/examples/go/advanced_example.go index 2a3bc1608..844839ffa 100644 --- a/examples/go/advanced_example.go +++ b/examples/go/advanced_example.go @@ -89,10 +89,8 @@ func main() { solver.Reset() intSort := ctx.MkIntSort() - listSort, nilDecl, consDecl, isNilDecl, isConsDecl, headDecl, tailDecl := + listSort, nilDecl, consDecl, _, _, headDecl, _ := 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) @@ -138,16 +136,12 @@ func main() { fmt.Println("\nExample 6: Enumeration types") solver.Reset() - colorSort, colorConsts, colorTesters := ctx.MkEnumSort( + colorSort, colorConsts, _ := ctx.MkEnumSort( "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) diff --git a/examples/go/new_api_example.go b/examples/go/new_api_example.go index bcda9ce71..28e1ea3c8 100644 --- a/examples/go/new_api_example.go +++ b/examples/go/new_api_example.go @@ -53,26 +53,32 @@ func main() { fmt.Println("\nExample 3: FromFile() - Load SMT-LIB2 from file") // Create a temporary SMT-LIB2 file - tmpFile := "/tmp/test.smt2" - content := `(declare-const p Bool) -(declare-const q Bool) -(assert (or p q)) -(assert (or (not p) (not q)))` - - err := os.WriteFile(tmpFile, []byte(content), 0644) + tmpFile, err := os.CreateTemp("", "test-*.smt2") if err != nil { fmt.Println("Error creating temp file:", err) } else { - solver3 := ctx.NewSolver() - solver3.FromFile(tmpFile) - fmt.Println("Loaded SMT-LIB2 assertions from file") + content := `(declare-const p Bool) +(declare-const q Bool) +(assert (or p q)) +(assert (or (not p) (not q)))` - status3 := solver3.Check() - fmt.Println("Status:", status3.String()) - if status3 == z3.Satisfiable { - fmt.Println("Found satisfying assignment") + _, err = tmpFile.WriteString(content) + tmpFile.Close() + + if err != nil { + fmt.Println("Error writing temp file:", err) + } else { + solver3 := ctx.NewSolver() + solver3.FromFile(tmpFile.Name()) + fmt.Println("Loaded SMT-LIB2 assertions from file") + + status3 := solver3.Check() + fmt.Println("Status:", status3.String()) + if status3 == z3.Satisfiable { + fmt.Println("Found satisfying assignment") + } } - os.Remove(tmpFile) // Clean up + os.Remove(tmpFile.Name()) // Clean up } // Example 4: Parameter configuration