Delete examples/go/test_new_api_additions.go

examples/go/test_new_api_additions.go

@@ -1,74 +0,0 @@
-package main
-
-import (
-	"fmt"
-	"os"
-	"path/filepath"
-
-	"github.com/Z3Prover/z3/src/api/go"
-)
-
-func main() {
-	// Test SetInitialValue
-	fmt.Println("\nTesting Solver.SetInitialValue()...")
-	ctx2 := z3.NewContext()
-	solver2 := ctx2.NewSolver()
-
-	x := ctx2.MkIntConst("x")
-	y := ctx2.MkIntConst("y")
-
-	// Set initial values to guide the solver
-	solver2.SetInitialValue(x, ctx2.MkInt(5, ctx2.MkIntSort()))
-	solver2.SetInitialValue(y, ctx2.MkInt(10, ctx2.MkIntSort()))
-
-	// Add constraints
-	solver2.Assert(ctx2.MkGt(x, ctx2.MkInt(0, ctx2.MkIntSort())))
-	solver2.Assert(ctx2.MkGt(y, ctx2.MkInt(0, ctx2.MkIntSort())))
-
-	if solver2.Check() == z3.Satisfiable {
-		fmt.Println("  ✓ SetInitialValue works (solver found solution)")
-	} else {
-		fmt.Println("  ✗ SetInitialValue failed")
-		os.Exit(1)
-	}
-
-	// Test FromString
-	fmt.Println("\nTesting Solver.FromString()...")
-	ctx3 := z3.NewContext()
-	solver3 := ctx3.NewSolver()
-
-	smtString := "(declare-const z Int)(assert (> z 42))"
-	solver3.FromString(smtString)
-
-	if solver3.Check() == z3.Satisfiable {
-		fmt.Println("  ✓ FromString works correctly")
-	} else {
-		fmt.Println("  ✗ FromString failed")
-		os.Exit(1)
-	}
-
-	// Test FromFile
-	fmt.Println("\nTesting Solver.FromFile()...")
-	ctx4 := z3.NewContext()
-	solver4 := ctx4.NewSolver()
-
-	// Create a temporary SMT file
-	tmpDir := os.TempDir()
-	smtFile := filepath.Join(tmpDir, "test.smt2")
-	err := os.WriteFile(smtFile, []byte("(declare-const w Int)\n(assert (< w 100))\n"), 0644)
-	if err != nil {
-		fmt.Printf("  ✗ Failed to create test file: %v\n", err)
-		os.Exit(1)
-	}
-	defer os.Remove(smtFile)
-
-	solver4.FromFile(smtFile)
-	if solver4.Check() == z3.Satisfiable {
-		fmt.Println("  ✓ FromFile works correctly")
-	} else {
-		fmt.Println("  ✗ FromFile failed")
-		os.Exit(1)
-	}
-
-	fmt.Println("\nAll tests passed! ✓")
-}