From 0678c8b88991be7383d1e7cdfd211b5fbd70605b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 28 Oct 2025 15:46:37 -0700
Subject: [PATCH] Delete examples/java/TestJavaAPICompleteness.java

---
 examples/java/TestJavaAPICompleteness.java | 86 ----------------------
 1 file changed, 86 deletions(-)
 delete mode 100644 examples/java/TestJavaAPICompleteness.java

diff --git a/examples/java/TestJavaAPICompleteness.java b/examples/java/TestJavaAPICompleteness.java
deleted file mode 100644
index d0a5b948b..000000000
--- a/examples/java/TestJavaAPICompleteness.java
+++ /dev/null
@@ -1,86 +0,0 @@
-/*++
-Copyright (c) 2025 Microsoft Corporation
-
-Module Name:
-
-    TestJavaAPICompleteness.java
-
-Abstract:
-
-    Test for Java API completeness fixes:
-    1. mkLastIndexOf method
-    2. CharSort support in Sort.create()
-
-Author:
-
-    Z3Prover Contributors 2025-10-28
-
-Notes:
-    
---*/
-
-import com.microsoft.z3.*;
-
-public class TestJavaAPICompleteness
-{
-    public static void main(String[] args)
-    {
-        try {
-            testMkLastIndexOf();
-            testCharSort();
-            System.out.println("All tests passed!");
-        } catch (Exception e) {
-            System.err.println("Test failed: " + e.getMessage());
-            e.printStackTrace();
-            System.exit(1);
-        }
-    }
-
-    static void testMkLastIndexOf() throws Exception
-    {
-        System.out.println("Testing mkLastIndexOf...");
-        
-        try (Context ctx = new Context()) {
-            // Create string expressions
-            SeqExpr<CharSort> s = ctx.mkString("hello world hello");
-            SeqExpr<CharSort> substr = ctx.mkString("hello");
-            
-            // Test mkLastIndexOf
-            IntExpr lastIdx = ctx.mkLastIndexOf(s, substr);
-            
-            // Create solver and check
-            Solver solver = ctx.mkSolver();
-            solver.add(ctx.mkGe(lastIdx, ctx.mkInt(0)));
-            
-            if (solver.check() == Status.SATISFIABLE) {
-                Model m = solver.getModel();
-                System.out.println("  mkLastIndexOf works correctly");
-                System.out.println("  Result: " + m.eval(lastIdx, false));
-            } else {
-                throw new Exception("mkLastIndexOf test failed: unsatisfiable");
-            }
-        }
-    }
-
-    static void testCharSort() throws Exception
-    {
-        System.out.println("Testing CharSort support in Sort.create()...");
-        
-        try (Context ctx = new Context()) {
-            // Create a char sort
-            CharSort charSort = ctx.mkCharSort();
-            
-            // Create a string which internally uses CharSort
-            SeqExpr<CharSort> str = ctx.mkString("test");
-            
-            // Get the element sort of the sequence (should be CharSort)
-            SeqSort<CharSort> seqSort = ctx.mkSeqSort(charSort);
-            
-            // Verify that CharSort works correctly
-            // This would previously throw "Unknown sort kind" exception when
-            // Z3 internally tries to create Sort objects
-            System.out.println("  CharSort is correctly handled in Sort.create()");
-            System.out.println("  CharSort: " + charSort);
-        }
-    }
-}