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 fad1884c9..3e03028ac 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -2235,6 +2235,46 @@ public class Context implements AutoCloseable {
         return (IntExpr)Expr.create(this, Native.mkSeqLastIndex(nCtx(), s.getNativeObject(), substr.getNativeObject()));
     }
 
+    /**
+     * Map function f over sequence s.
+     * Returns a new sequence where f is applied to each element of s.
+     */
+    public final <R extends Sort> SeqExpr<R> mkSeqMap(Expr<?> f, Expr<SeqSort<R>> s)
+    {
+        checkContextMatch(f, s);
+        return (SeqExpr<R>) Expr.create(this, Native.mkSeqMap(nCtx(), f.getNativeObject(), s.getNativeObject()));
+    }
+
+    /**
+     * Map function f over sequence s starting at index i.
+     * Returns a new sequence where f is applied to each element of s along with its index starting from i.
+     */
+    public final <R extends Sort> SeqExpr<R> mkSeqMapi(Expr<?> f, Expr<IntSort> i, Expr<SeqSort<R>> s)
+    {
+        checkContextMatch(f, i, s);
+        return (SeqExpr<R>) Expr.create(this, Native.mkSeqMapi(nCtx(), f.getNativeObject(), i.getNativeObject(), s.getNativeObject()));
+    }
+
+    /**
+     * Left fold of function f over sequence s with accumulator a.
+     * Applies f to accumulate values from left to right over the sequence.
+     */
+    public final <R extends Sort, A extends Sort> Expr<A> mkSeqFoldl(Expr<?> f, Expr<A> a, Expr<SeqSort<R>> s)
+    {
+        checkContextMatch(f, a, s);
+        return (Expr<A>) Expr.create(this, Native.mkSeqFoldl(nCtx(), f.getNativeObject(), a.getNativeObject(), s.getNativeObject()));
+    }
+
+    /**
+     * Left fold of function f over sequence s with accumulator a starting at index i.
+     * Applies f to accumulate values from left to right over the sequence, tracking the index starting from i.
+     */
+    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);
+        return (Expr<A>) Expr.create(this, Native.mkSeqFoldli(nCtx(), f.getNativeObject(), i.getNativeObject(), a.getNativeObject(), s.getNativeObject()));
+    }
+
     /**
      * Replace the first occurrence of src by dst in s.
      */
@@ -4430,6 +4470,14 @@ public class Context implements AutoCloseable {
         checkContextMatch(other3);
     }
 
+    void checkContextMatch(Z3Object other1, Z3Object other2, Z3Object other3, Z3Object other4)
+    {
+        checkContextMatch(other1);
+        checkContextMatch(other2);
+        checkContextMatch(other3);
+        checkContextMatch(other4);
+    }
+
     void checkContextMatch(Z3Object[] arr)
     {
         if (arr != null)