mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-16 22:01:44 +00:00
Code Activity

Address code review feedback: use os.CreateTemp and remove unused vars

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-16 21:47:33 +00:00
parent 6d3c41143c
commit c99baf45d0
2 changed files with 23 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

10
examples/go/advanced_example.go
View file

@ -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)

36
examples/go/new_api_example.go
View file

@ -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