From 624c3a36632b24fa9fa7d34334467bc0fa1fd636 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sat, 17 Jan 2026 19:00:00 +0000
Subject: [PATCH] Fix checkContextMatch call and add test for sequence
 operations

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 examples/java/SeqOperationsExample.java | 84 +++++++++++++++++++++++++
 src/api/java/Context.java               |  2 +-
 2 files changed, 85 insertions(+), 1 deletion(-)
 create mode 100644 examples/java/SeqOperationsExample.java

diff --git a/examples/java/SeqOperationsExample.java b/examples/java/SeqOperationsExample.java
new file mode 100644
index 000000000..2ecb44193
--- /dev/null
+++ b/examples/java/SeqOperationsExample.java
@@ -0,0 +1,84 @@
+/**
+ * Test example for new sequence operations (SeqMap, SeqMapi, SeqFoldl, SeqFoldli)
+ */
+
+import com.microsoft.z3.*;
+
+public class SeqOperationsExample {
+    public static void main(String[] args) {
+        Context ctx = new Context();
+        
+        try {
+            System.out.println("Testing new sequence operations in Java API\n");
+            
+            // Test 1: mkSeqMap
+            System.out.println("Test 1: mkSeqMap");
+            IntSort intSort = ctx.mkIntSort();
+            SeqSort<IntSort> seqIntSort = ctx.mkSeqSort(intSort);
+            
+            // Create a sequence variable
+            Expr<SeqSort<IntSort>> seq = ctx.mkConst("s", seqIntSort);
+            
+            // Create a lambda function that adds 1 to an integer: (lambda (x) (+ x 1))
+            Expr<IntSort> x = ctx.mkIntConst("x");
+            Lambda<IntSort> f = ctx.mkLambda(new Expr<?>[] { x }, ctx.mkAdd(x, ctx.mkInt(1)));
+            
+            // Create map expression (conceptually maps f over seq)
+            SeqExpr<IntSort> mapped = ctx.mkSeqMap(f, seq);
+            System.out.println("mkSeqMap result type: " + mapped.getClass().getName());
+            System.out.println("mkSeqMap created successfully: " + mapped);
+            System.out.println();
+            
+            // Test 2: mkSeqMapi
+            System.out.println("Test 2: mkSeqMapi");
+            // Lambda that takes index and element: (lambda (i x) (+ x i))
+            Expr<IntSort> xElem = ctx.mkIntConst("xElem");
+            Expr<IntSort> iIdx = ctx.mkIntConst("iIdx");
+            Lambda<IntSort> fWithIdx = ctx.mkLambda(new Expr<?>[] { iIdx, xElem }, ctx.mkAdd(xElem, iIdx));
+            IntExpr i = ctx.mkIntConst("start_idx");
+            SeqExpr<IntSort> mappedWithIndex = ctx.mkSeqMapi(fWithIdx, i, seq);
+            System.out.println("mkSeqMapi result type: " + mappedWithIndex.getClass().getName());
+            System.out.println("mkSeqMapi created successfully: " + mappedWithIndex);
+            System.out.println();
+            
+            // Test 3: mkSeqFoldl
+            System.out.println("Test 3: mkSeqFoldl");
+            // Lambda that accumulates: (lambda (acc elem) (+ acc elem))
+            IntExpr accVar = ctx.mkIntConst("accVar");
+            IntExpr elemVar = ctx.mkIntConst("elemVar");
+            Lambda<IntSort> foldFunc = ctx.mkLambda(new Expr<?>[] { accVar, elemVar }, ctx.mkAdd(accVar, elemVar));
+            IntExpr acc = ctx.mkIntConst("acc");
+            Expr<IntSort> folded = ctx.mkSeqFoldl(foldFunc, acc, seq);
+            System.out.println("mkSeqFoldl result type: " + folded.getClass().getName());
+            System.out.println("mkSeqFoldl created successfully: " + folded);
+            System.out.println();
+            
+            // Test 4: mkSeqFoldli
+            System.out.println("Test 4: mkSeqFoldli");
+            // Lambda with index: (lambda (idx acc elem) (+ acc elem idx))
+            IntExpr idxVar = ctx.mkIntConst("idxVar");
+            IntExpr accVar2 = ctx.mkIntConst("accVar2");
+            IntExpr elemVar2 = ctx.mkIntConst("elemVar2");
+            ArithExpr<?> tempSum = ctx.mkAdd(accVar2, elemVar2);
+            ArithExpr<?> finalSum = ctx.mkAdd(tempSum, idxVar);
+            Lambda<IntSort> foldFuncWithIdx = ctx.mkLambda(
+                new Expr<?>[] { idxVar, accVar2, elemVar2 }, 
+                (IntExpr) finalSum);
+            IntExpr idx = ctx.mkIntConst("start_idx2");
+            IntExpr acc2 = ctx.mkIntConst("acc2");
+            Expr<IntSort> foldedWithIndex = ctx.mkSeqFoldli(foldFuncWithIdx, idx, acc2, seq);
+            System.out.println("mkSeqFoldli result type: " + foldedWithIndex.getClass().getName());
+            System.out.println("mkSeqFoldli created successfully: " + foldedWithIndex);
+            System.out.println();
+            
+            System.out.println("All tests passed!");
+            
+        } catch (Exception e) {
+            System.err.println("Error: " + e.getMessage());
+            e.printStackTrace();
+            System.exit(1);
+        } finally {
+            ctx.close();
+        }
+    }
+}
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index 01ca3f293..5292275fa 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -2271,7 +2271,7 @@ public class Context implements AutoCloseable {
      */
     public final <R extends Sort, A extends Sort> Expr<A> mkSeqFoldli(Expr<?> f, Expr<IntSort> i, Expr<A> a, Expr<SeqSort<R>> s)
     {
-        checkContextMatch(f, i, a, s);
+        checkContextMatch(new Z3Object[] { f, i, a, s });
         return (Expr<A>) Expr.create(this, Native.mkSeqFoldli(nCtx(), f.getNativeObject(), i.getNativeObject(), a.getNativeObject(), s.getNativeObject()));
     }