diff --git a/examples/go/test_new_api_additions.go b/examples/go/test_new_api_additions.go deleted file mode 100644 index 9a3549c13..000000000 --- a/examples/go/test_new_api_additions.go +++ /dev/null @@ -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! ✓") -}