diff --git a/src/api/js/examples/regex-example.md b/src/api/js/examples/regex-example.md
new file mode 100644
index 000000000..a386d6b7e
--- /dev/null
+++ b/src/api/js/examples/regex-example.md
@@ -0,0 +1,268 @@
+# Regular Expression Support in Z3 TypeScript API
+
+This document demonstrates the new regular expression support added to the Z3 TypeScript API.
+
+## Basic Usage
+
+### Creating Regular Expressions
+
+```typescript
+const { Re, String: Str, InRe, Solver } = Context('main');
+
+// Create a regex from a string
+const hello = Re.toRe('hello');
+
+// Check if a string matches
+const solver = new Solver();
+solver.add(InRe('hello', hello));
+await solver.check(); // sat
+```
+
+### Star Operator (Zero or More)
+
+```typescript
+const { Re, InRe, Star } = Context('main');
+
+const a = Re.toRe('a');
+const aStar = Star(a);
+
+// Empty string matches a*
+InRe('', aStar);     // true
+
+// Multiple 'a's match
+InRe('aaa', aStar);  // true
+```
+
+### Plus Operator (One or More)
+
+```typescript
+const { Re, InRe, Plus } = Context('main');
+
+const a = Re.toRe('a');
+const aPlus = Plus(a);
+
+// Empty string does NOT match a+
+InRe('', aPlus);     // false
+
+// One or more 'a's match
+InRe('aa', aPlus);   // true
+```
+
+### Option Operator (Zero or One)
+
+```typescript
+const { Re, InRe, Option } = Context('main');
+
+const a = Re.toRe('a');
+const aOpt = Option(a);
+
+// Both empty and 'a' match a?
+InRe('', aOpt);      // true
+InRe('a', aOpt);     // true
+InRe('aa', aOpt);    // false
+```
+
+### Union (Or)
+
+```typescript
+const { Re, InRe, Union } = Context('main');
+
+const a = Re.toRe('a');
+const b = Re.toRe('b');
+const aOrB = Union(a, b);
+
+// Either 'a' or 'b' match
+InRe('a', aOrB);     // true
+InRe('b', aOrB);     // true
+InRe('c', aOrB);     // false
+```
+
+### Intersect (And)
+
+```typescript
+const { Re, InRe, Intersect, Star } = Context('main');
+
+const a = Re.toRe('a');
+const b = Re.toRe('b');
+const both = Intersect(Star(a), Star(b));
+
+// Only empty string matches both a* and b*
+InRe('', both);      // true
+InRe('a', both);     // false
+```
+
+### Range
+
+```typescript
+const { Range, InRe } = Context('main');
+
+const azRange = Range('a', 'z');
+
+// Lowercase letters match
+InRe('m', azRange);  // true
+
+// Others don't
+InRe('1', azRange);  // false
+InRe('Z', azRange);  // false
+```
+
+### Loop (Bounded Repetition)
+
+```typescript
+const { Re, InRe, Loop } = Context('main');
+
+const a = Re.toRe('a');
+
+// Between 2 and 3 repetitions
+const a2to3 = Loop(a, 2, 3);
+InRe('aa', a2to3);   // true
+InRe('aaa', a2to3);  // true
+InRe('a', a2to3);    // false
+InRe('aaaa', a2to3); // false
+
+// At least 2 repetitions (hi=0 or omitted means unbounded)
+const a2Plus = Loop(a, 2, 0);  // or Loop(a, 2)
+InRe('aa', a2Plus);   // true
+InRe('aaa', a2Plus);  // true
+InRe('aaaa', a2Plus); // true
+InRe('a', a2Plus);    // false
+```
+
+### Power (Exact Repetition)
+
+```typescript
+const { Re, InRe, Power } = Context('main');
+
+const a = Re.toRe('a');
+const a3 = Power(a, 3);
+
+// Exactly 3 repetitions match
+InRe('aaa', a3);     // true
+
+// Others don't
+InRe('aa', a3);      // false
+InRe('aaaa', a3);    // false
+```
+
+### Complement (Negation)
+
+```typescript
+const { Re, InRe, Complement } = Context('main');
+
+const a = Re.toRe('a');
+const notA = Complement(a);
+
+// Everything except 'a' matches
+InRe('a', notA);     // false
+InRe('b', notA);     // true
+InRe('', notA);      // true
+```
+
+### Diff (Set Difference)
+
+```typescript
+const { Re, InRe, Diff, Star } = Context('main');
+
+const a = Re.toRe('a');
+const b = Re.toRe('b');
+const diff = Diff(Star(a), b);
+
+// a* except 'b'
+InRe('aaa', diff);   // true
+InRe('b', diff);     // false
+```
+
+### ReConcat (Concatenation)
+
+```typescript
+const { Re, InRe, ReConcat } = Context('main');
+
+const hello = Re.toRe('hello');
+const world = Re.toRe('world');
+const helloworld = ReConcat(hello, world);
+
+// Concatenated strings match
+InRe('helloworld', helloworld);  // true
+InRe('hello', helloworld);       // false
+```
+
+## Method Chaining
+
+Regular expression objects support method chaining:
+
+```typescript
+const { Re, InRe } = Context('main');
+
+const a = Re.toRe('a');
+
+// Using methods
+const aStar = a.star();
+const aPlus = a.plus();
+const aOpt = a.option();
+const notA = a.complement();
+
+// Chaining
+const complex = a.plus().union(Re.toRe('b').star());
+```
+
+## Complex Example: Pattern Matching
+
+```typescript
+const { Re, String: Str, InRe, Union, Star, Solver } = Context('main');
+
+const x = Str.const('x');
+const a = Re.toRe('a');
+const b = Re.toRe('b');
+
+// Pattern: any combination of 'a' and 'b'
+const pattern = Star(Union(a, b));
+
+const solver = new Solver();
+solver.add(InRe(x, pattern));
+solver.add(x.length().eq(5));
+
+if (await solver.check() === 'sat') {
+  const model = solver.model();
+  const result = model.eval(x);
+  // Result will be a 5-character string containing only 'a' and 'b'
+  console.log(result.asString()); // e.g., "aabba"
+}
+```
+
+## API Reference
+
+### Factory Methods
+
+- `Re.sort(seqSort)` - Create a regex sort
+- `Re.toRe(seq)` - Convert sequence/string to regex
+
+### Operators
+
+- `Star(re)` - Zero or more repetitions (*)
+- `Plus(re)` - One or more repetitions (+)
+- `Option(re)` - Zero or one repetition (?)
+- `Union(...res)` - Or operation (|)
+- `Intersect(...res)` - And operation (&)
+- `ReConcat(...res)` - Concatenation
+- `Complement(re)` - Negation (~)
+- `Diff(a, b)` - Set difference (a \ b)
+- `Range(lo, hi)` - Character range
+- `Loop(re, lo, hi?)` - Bounded repetition {lo,hi} or at least lo if hi=0 or omitted
+- `Power(re, n)` - Exact repetition {n}
+
+### Special Patterns
+
+- `AllChar(reSort)` - Match any single character
+- `Empty(reSort)` - Empty language
+- `Full(reSort)` - Match all strings
+
+### Membership Test
+
+- `InRe(seq, re)` - Test if sequence matches regex
+
+## Notes
+
+- All regex operations are symbolic - they create constraints rather than executing pattern matching
+- The solver finds strings that satisfy the regex constraints
+- Regular expressions can be combined with other Z3 constraints (length, containment, etc.)
+- This implementation follows the SMT-LIB2 regular expression theory
diff --git a/src/api/js/src/high-level/high-level.test.ts b/src/api/js/src/high-level/high-level.test.ts
index 18fb8fab3..c908a480f 100644
--- a/src/api/js/src/high-level/high-level.test.ts
+++ b/src/api/js/src/high-level/high-level.test.ts
@@ -1844,6 +1844,252 @@ describe('high-level', () => {
     });
   });
 
+  describe('regular expressions', () => {
+    it('can create regex sort', () => {
+      const { Re, String: Str, eqIdentity } = api.Context('main');
+
+      const reSort = Re.sort(Str.sort());
+      expect(eqIdentity(reSort.basis(), Str.sort())).toBe(true);
+    });
+
+    it('can convert string to regex', async () => {
+      const { Re, String: Str, InRe, Solver } = api.Context('main');
+
+      const hello = Str.val('hello');
+      const re = Re.toRe(hello);
+
+      const solver = new Solver();
+      solver.add(InRe('hello', re));
+
+      const result = await solver.check();
+      expect(result).toBe('sat');
+    });
+
+    it('can use star operator', async () => {
+      const { Re, String: Str, InRe, Star, Solver } = api.Context('main');
+
+      const a = Re.toRe('a');
+      const aStar = Star(a);
+
+      const solver = new Solver();
+      // Empty string matches a*
+      solver.add(InRe('', aStar));
+
+      const result = await solver.check();
+      expect(result).toBe('sat');
+    });
+
+    it('can use plus operator', async () => {
+      const { Re, String: Str, InRe, Plus, Solver } = api.Context('main');
+
+      const a = Re.toRe('a');
+      const aPlus = Plus(a);
+
+      const solver = new Solver();
+      // "aa" matches a+
+      solver.add(InRe('aa', aPlus));
+
+      const result = await solver.check();
+      expect(result).toBe('sat');
+    });
+
+    it('can use option operator', async () => {
+      const { Re, InRe, Option, Solver } = api.Context('main');
+
+      const a = Re.toRe('a');
+      const aOpt = Option(a);
+
+      const solver1 = new Solver();
+      // Empty string matches a?
+      solver1.add(InRe('', aOpt));
+      expect(await solver1.check()).toBe('sat');
+
+      const solver2 = new Solver();
+      // "a" matches a?
+      solver2.add(InRe('a', aOpt));
+      expect(await solver2.check()).toBe('sat');
+    });
+
+    it('can use union operator', async () => {
+      const { Re, InRe, Union, Solver } = api.Context('main');
+
+      const a = Re.toRe('a');
+      const b = Re.toRe('b');
+      const aOrB = Union(a, b);
+
+      const solver1 = new Solver();
+      solver1.add(InRe('a', aOrB));
+      expect(await solver1.check()).toBe('sat');
+
+      const solver2 = new Solver();
+      solver2.add(InRe('b', aOrB));
+      expect(await solver2.check()).toBe('sat');
+
+      const solver3 = new Solver();
+      solver3.add(InRe('c', aOrB));
+      expect(await solver3.check()).toBe('unsat');
+    });
+
+    it('can use intersect operator', async () => {
+      const { Re, InRe, Intersect, Star, Solver } = api.Context('main');
+
+      const a = Re.toRe('a');
+      const b = Re.toRe('b');
+      const aStar = Star(a);
+      const bStar = Star(b);
+      const both = Intersect(aStar, bStar);
+
+      const solver = new Solver();
+      // Only empty string matches both a* and b*
+      solver.add(InRe('', both));
+      expect(await solver.check()).toBe('sat');
+    });
+
+    it('can use range operator', async () => {
+      const { Range, InRe, Solver } = api.Context('main');
+
+      const azRange = Range('a', 'z');
+
+      const solver1 = new Solver();
+      solver1.add(InRe('m', azRange));
+      expect(await solver1.check()).toBe('sat');
+
+      const solver2 = new Solver();
+      solver2.add(InRe('1', azRange));
+      expect(await solver2.check()).toBe('unsat');
+    });
+
+    it('can use loop operator', async () => {
+      const { Re, InRe, Loop, Solver } = api.Context('main');
+
+      const a = Re.toRe('a');
+      const a2to3 = Loop(a, 2, 3);
+
+      const solver1 = new Solver();
+      solver1.add(InRe('aa', a2to3));
+      expect(await solver1.check()).toBe('sat');
+
+      const solver2 = new Solver();
+      solver2.add(InRe('aaa', a2to3));
+      expect(await solver2.check()).toBe('sat');
+
+      const solver3 = new Solver();
+      solver3.add(InRe('a', a2to3));
+      expect(await solver3.check()).toBe('unsat');
+
+      const solver4 = new Solver();
+      solver4.add(InRe('aaaa', a2to3));
+      expect(await solver4.check()).toBe('unsat');
+    });
+
+    it('can use power operator', async () => {
+      const { Re, InRe, Power, Solver } = api.Context('main');
+
+      const a = Re.toRe('a');
+      const a3 = Power(a, 3);
+
+      const solver1 = new Solver();
+      solver1.add(InRe('aaa', a3));
+      expect(await solver1.check()).toBe('sat');
+
+      const solver2 = new Solver();
+      solver2.add(InRe('aa', a3));
+      expect(await solver2.check()).toBe('unsat');
+    });
+
+    it('can use complement operator', async () => {
+      const { Re, InRe, Complement, Solver } = api.Context('main');
+
+      const a = Re.toRe('a');
+      const notA = Complement(a);
+
+      const solver1 = new Solver();
+      solver1.add(InRe('a', notA));
+      expect(await solver1.check()).toBe('unsat');
+
+      const solver2 = new Solver();
+      solver2.add(InRe('b', notA));
+      expect(await solver2.check()).toBe('sat');
+    });
+
+    it('can use diff operator', async () => {
+      const { Re, InRe, Diff, Star, Solver } = api.Context('main');
+
+      const a = Re.toRe('a');
+      const b = Re.toRe('b');
+      const aStar = Star(a);
+      const diff = Diff(aStar, b);
+
+      const solver1 = new Solver();
+      solver1.add(InRe('aaa', diff));
+      expect(await solver1.check()).toBe('sat');
+
+      const solver2 = new Solver();
+      solver2.add(InRe('b', diff));
+      expect(await solver2.check()).toBe('unsat');
+    });
+
+    it('can use ReConcat operator', async () => {
+      const { Re, InRe, ReConcat, Solver } = api.Context('main');
+
+      const hello = Re.toRe('hello');
+      const world = Re.toRe('world');
+      const helloworld = ReConcat(hello, world);
+
+      const solver1 = new Solver();
+      solver1.add(InRe('helloworld', helloworld));
+      expect(await solver1.check()).toBe('sat');
+
+      const solver2 = new Solver();
+      solver2.add(InRe('hello', helloworld));
+      expect(await solver2.check()).toBe('unsat');
+    });
+
+    it('can use method chaining', async () => {
+      const { Re, InRe, Solver } = api.Context('main');
+
+      const a = Re.toRe('a');
+      const aStar = a.star();
+      const aPlus = a.plus();
+
+      const solver1 = new Solver();
+      solver1.add(InRe('', aStar));
+      expect(await solver1.check()).toBe('sat');
+
+      const solver2 = new Solver();
+      solver2.add(InRe('', aPlus));
+      expect(await solver2.check()).toBe('unsat');
+    });
+
+    it('can solve complex regex constraints', async () => {
+      const { Re, String: Str, InRe, Union, Star, Solver } = api.Context('main');
+
+      const x = Str.const('x');
+      const a = Re.toRe('a');
+      const b = Re.toRe('b');
+      const pattern = Star(Union(a, b));
+
+      const solver = new Solver();
+      solver.add(InRe(x, pattern));
+      solver.add(x.length().eq(5));
+
+      const result = await solver.check();
+      expect(result).toBe('sat');
+      
+      if (result === 'sat') {
+        const model = solver.model();
+        const xVal = model.eval(x);
+        // Check if it's a string using the isString method if available
+        if ('isString' in xVal && typeof xVal.isString === 'function' && xVal.isString()) {
+          const strVal = (xVal as any).asString();
+          expect(strVal.length).toBe(5);
+          // Verify it only contains 'a' and 'b'
+          expect(/^[ab]+$/.test(strVal)).toBe(true);
+        }
+      }
+    });
+  });
+
   describe('Params API', () => {
     it('can create params', () => {
       const { Params } = api.Context('main');
diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts
index a3f50f16e..006e3da37 100644
--- a/src/api/js/src/high-level/high-level.ts
+++ b/src/api/js/src/high-level/high-level.ts
@@ -96,6 +96,9 @@ import {
   RatNum,
   RCFNum,
   RCFNumCreation,
+  Re,
+  ReSort,
+  ReCreation,
   Seq,
   SeqSort,
   Simplifier,
@@ -297,6 +300,8 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
           return new FPRMSortImpl(ast);
         case Z3_sort_kind.Z3_SEQ_SORT:
           return new SeqSortImpl(ast);
+        case Z3_sort_kind.Z3_RE_SORT:
+          return new ReSortImpl(ast);
         case Z3_sort_kind.Z3_ARRAY_SORT:
           return new ArraySortImpl(ast);
         default:
@@ -340,6 +345,8 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
           return new FPRMImpl(ast);
         case Z3_sort_kind.Z3_SEQ_SORT:
           return new SeqImpl(ast);
+        case Z3_sort_kind.Z3_RE_SORT:
+          return new ReImpl(ast);
         case Z3_sort_kind.Z3_ARRAY_SORT:
           return new ArrayImpl(ast);
         default:
@@ -611,6 +618,18 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       return r;
     }
 
+    function isReSort(obj: unknown): obj is ReSort<Name> {
+      const r = obj instanceof ReSortImpl;
+      r && _assertContext(obj);
+      return r;
+    }
+
+    function isRe(obj: unknown): obj is Re<Name> {
+      const r = obj instanceof ReImpl;
+      r && _assertContext(obj);
+      return r;
+    }
+
     function isStringSort(obj: unknown): obj is SeqSort<Name> {
       return isSeqSort(obj) && obj.isString();
     }
@@ -1000,6 +1019,17 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       },
     };
 
+    const Re = {
+      sort<SeqSortRef extends SeqSort<Name>>(seqSort: SeqSortRef): ReSort<Name, SeqSortRef> {
+        return new ReSortImpl<SeqSortRef>(Z3.mk_re_sort(contextPtr, seqSort.ptr));
+      },
+
+      toRe(seq: Seq<Name> | string): Re<Name> {
+        const seqExpr = isSeq(seq) ? seq : String.val(seq);
+        return new ReImpl(check(Z3.mk_seq_to_re(contextPtr, seqExpr.ast)));
+      },
+    };
+
     const Array = {
       sort<DomainSort extends NonEmptySortArray<Name>, RangeSort extends AnySort<Name>>(
         ...sig: [...DomainSort, RangeSort]
@@ -1765,6 +1795,97 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       return new BoolImpl(check(Z3.mk_set_subset(contextPtr, a.ast, b.ast)));
     }
 
+    //////////////////////
+    // Regular Expressions
+    //////////////////////
+
+    function InRe(seq: Seq<Name> | string, re: Re<Name>): Bool<Name> {
+      const seqExpr = isSeq(seq) ? seq : String.val(seq);
+      return new BoolImpl(check(Z3.mk_seq_in_re(contextPtr, seqExpr.ast, re.ast)));
+    }
+
+    function Union<SeqSortRef extends SeqSort<Name>>(...res: Re<Name, SeqSortRef>[]): Re<Name, SeqSortRef> {
+      if (res.length === 0) {
+        throw new Error('Union requires at least one argument');
+      }
+      if (res.length === 1) {
+        return res[0];
+      }
+      return new ReImpl<SeqSortRef>(check(Z3.mk_re_union(contextPtr, res.map(r => r.ast))));
+    }
+
+    function Intersect<SeqSortRef extends SeqSort<Name>>(...res: Re<Name, SeqSortRef>[]): Re<Name, SeqSortRef> {
+      if (res.length === 0) {
+        throw new Error('Intersect requires at least one argument');
+      }
+      if (res.length === 1) {
+        return res[0];
+      }
+      return new ReImpl<SeqSortRef>(check(Z3.mk_re_intersect(contextPtr, res.map(r => r.ast))));
+    }
+
+    function ReConcat<SeqSortRef extends SeqSort<Name>>(...res: Re<Name, SeqSortRef>[]): Re<Name, SeqSortRef> {
+      if (res.length === 0) {
+        throw new Error('ReConcat requires at least one argument');
+      }
+      if (res.length === 1) {
+        return res[0];
+      }
+      return new ReImpl<SeqSortRef>(check(Z3.mk_re_concat(contextPtr, res.map(r => r.ast))));
+    }
+
+    function Plus<SeqSortRef extends SeqSort<Name>>(re: Re<Name, SeqSortRef>): Re<Name, SeqSortRef> {
+      return new ReImpl<SeqSortRef>(check(Z3.mk_re_plus(contextPtr, re.ast)));
+    }
+
+    function Star<SeqSortRef extends SeqSort<Name>>(re: Re<Name, SeqSortRef>): Re<Name, SeqSortRef> {
+      return new ReImpl<SeqSortRef>(check(Z3.mk_re_star(contextPtr, re.ast)));
+    }
+
+    function Option<SeqSortRef extends SeqSort<Name>>(re: Re<Name, SeqSortRef>): Re<Name, SeqSortRef> {
+      return new ReImpl<SeqSortRef>(check(Z3.mk_re_option(contextPtr, re.ast)));
+    }
+
+    function Complement<SeqSortRef extends SeqSort<Name>>(re: Re<Name, SeqSortRef>): Re<Name, SeqSortRef> {
+      return new ReImpl<SeqSortRef>(check(Z3.mk_re_complement(contextPtr, re.ast)));
+    }
+
+    function Diff<SeqSortRef extends SeqSort<Name>>(a: Re<Name, SeqSortRef>, b: Re<Name, SeqSortRef>): Re<Name, SeqSortRef> {
+      return new ReImpl<SeqSortRef>(check(Z3.mk_re_diff(contextPtr, a.ast, b.ast)));
+    }
+
+    function Range<SeqSortRef extends SeqSort<Name>>(lo: Seq<Name, SeqSortRef> | string, hi: Seq<Name, SeqSortRef> | string): Re<Name, SeqSortRef> {
+      const loSeq = isSeq(lo) ? lo : String.val(lo);
+      const hiSeq = isSeq(hi) ? hi : String.val(hi);
+      return new ReImpl<SeqSortRef>(check(Z3.mk_re_range(contextPtr, loSeq.ast, hiSeq.ast)));
+    }
+
+    /**
+     * Create a bounded repetition regex.
+     * @param re The regex to repeat
+     * @param lo Minimum number of repetitions
+     * @param hi Maximum number of repetitions (0 means unbounded, i.e., at least lo)
+     */
+    function Loop<SeqSortRef extends SeqSort<Name>>(re: Re<Name, SeqSortRef>, lo: number, hi: number = 0): Re<Name, SeqSortRef> {
+      return new ReImpl<SeqSortRef>(check(Z3.mk_re_loop(contextPtr, re.ast, lo, hi)));
+    }
+
+    function Power<SeqSortRef extends SeqSort<Name>>(re: Re<Name, SeqSortRef>, n: number): Re<Name, SeqSortRef> {
+      return new ReImpl<SeqSortRef>(check(Z3.mk_re_power(contextPtr, re.ast, n)));
+    }
+
+    function AllChar<SeqSortRef extends SeqSort<Name>>(reSort: ReSort<Name, SeqSortRef>): Re<Name, SeqSortRef> {
+      return new ReImpl<SeqSortRef>(check(Z3.mk_re_allchar(contextPtr, reSort.ptr)));
+    }
+
+    function Empty<SeqSortRef extends SeqSort<Name>>(reSort: ReSort<Name, SeqSortRef>): Re<Name, SeqSortRef> {
+      return new ReImpl<SeqSortRef>(check(Z3.mk_re_empty(contextPtr, reSort.ptr)));
+    }
+
+    function Full<SeqSortRef extends SeqSort<Name>>(reSort: ReSort<Name, SeqSortRef>): Re<Name, SeqSortRef> {
+      return new ReImpl<SeqSortRef>(check(Z3.mk_re_full(contextPtr, reSort.ptr)));
+    }
+
     function mkPartialOrder(sort: Sort<Name>, index: number): FuncDecl<Name> {
       return new FuncDeclImpl(check(Z3.mk_partial_order(contextPtr, sort.ptr, index)));
     }
@@ -4024,6 +4145,76 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       }
     }
 
+    class ReSortImpl<SeqSortRef extends SeqSort<Name> = SeqSort<Name>> extends SortImpl implements ReSort<Name, SeqSortRef> {
+      declare readonly __typename: ReSort['__typename'];
+
+      basis(): SeqSortRef {
+        return _toSort(check(Z3.get_re_sort_basis(contextPtr, this.ptr))) as SeqSortRef;
+      }
+
+      cast(other: Re<Name, SeqSortRef>): Re<Name, SeqSortRef>;
+      cast(other: CoercibleToExpr<Name>): Expr<Name>;
+      cast(other: any): any {
+        if (isRe(other)) {
+          _assertContext(other);
+          return other;
+        }
+        throw new Error("Can't cast to ReSort");
+      }
+    }
+
+    class ReImpl<SeqSortRef extends SeqSort<Name> = SeqSort<Name>>
+      extends ExprImpl<Z3_ast, ReSortImpl<SeqSortRef>>
+      implements Re<Name, SeqSortRef>
+    {
+      declare readonly __typename: Re['__typename'];
+
+      plus(): Re<Name, SeqSortRef> {
+        return new ReImpl<SeqSortRef>(check(Z3.mk_re_plus(contextPtr, this.ast)));
+      }
+
+      star(): Re<Name, SeqSortRef> {
+        return new ReImpl<SeqSortRef>(check(Z3.mk_re_star(contextPtr, this.ast)));
+      }
+
+      option(): Re<Name, SeqSortRef> {
+        return new ReImpl<SeqSortRef>(check(Z3.mk_re_option(contextPtr, this.ast)));
+      }
+
+      complement(): Re<Name, SeqSortRef> {
+        return new ReImpl<SeqSortRef>(check(Z3.mk_re_complement(contextPtr, this.ast)));
+      }
+
+      union(other: Re<Name, SeqSortRef>): Re<Name, SeqSortRef> {
+        return new ReImpl<SeqSortRef>(check(Z3.mk_re_union(contextPtr, [this.ast, other.ast])));
+      }
+
+      intersect(other: Re<Name, SeqSortRef>): Re<Name, SeqSortRef> {
+        return new ReImpl<SeqSortRef>(check(Z3.mk_re_intersect(contextPtr, [this.ast, other.ast])));
+      }
+
+      diff(other: Re<Name, SeqSortRef>): Re<Name, SeqSortRef> {
+        return new ReImpl<SeqSortRef>(check(Z3.mk_re_diff(contextPtr, this.ast, other.ast)));
+      }
+
+      concat(other: Re<Name, SeqSortRef>): Re<Name, SeqSortRef> {
+        return new ReImpl<SeqSortRef>(check(Z3.mk_re_concat(contextPtr, [this.ast, other.ast])));
+      }
+
+      /**
+       * Create a bounded repetition of this regex
+       * @param lo Minimum number of repetitions
+       * @param hi Maximum number of repetitions (0 means unbounded, i.e., at least lo)
+       */
+      loop(lo: number, hi: number = 0): Re<Name, SeqSortRef> {
+        return new ReImpl<SeqSortRef>(check(Z3.mk_re_loop(contextPtr, this.ast, lo, hi)));
+      }
+
+      power(n: number): Re<Name, SeqSortRef> {
+        return new ReImpl<SeqSortRef>(check(Z3.mk_re_power(contextPtr, this.ast, n)));
+      }
+    }
+
     class ArraySortImpl<DomainSort extends NonEmptySortArray<Name>, RangeSort extends Sort<Name>>
       extends SortImpl
       implements SMTArraySort<Name, DomainSort, RangeSort>
@@ -4731,6 +4922,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       FloatRM,
       String,
       Seq,
+      Re,
       Array,
       Set,
       Datatype,
@@ -4823,6 +5015,23 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       FullSet,
       isMember,
       isSubset,
+
+      InRe,
+      Union,
+      Intersect,
+      ReConcat,
+      Plus,
+      Star,
+      Option,
+      Complement,
+      Diff,
+      Range,
+      Loop,
+      Power,
+      AllChar,
+      Empty,
+      Full,
+
       mkPartialOrder,
       mkTransitiveClosure,
       polynomialSubresultants,
diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts
index b252f6921..351eb6087 100644
--- a/src/api/js/src/high-level/types.ts
+++ b/src/api/js/src/high-level/types.ts
@@ -36,7 +36,8 @@ export type AnySort<Name extends string = 'main'> =
   | SMTArraySort<Name>
   | FPSort<Name>
   | FPRMSort<Name>
-  | SeqSort<Name>;
+  | SeqSort<Name>
+  | ReSort<Name>;
 /** @hidden */
 export type AnyExpr<Name extends string = 'main'> =
   | Expr<Name>
@@ -50,7 +51,8 @@ export type AnyExpr<Name extends string = 'main'> =
   | FP<Name>
   | FPNum<Name>
   | FPRM<Name>
-  | Seq<Name>;
+  | Seq<Name>
+  | Re<Name>;
 /** @hidden */
 export type AnyAst<Name extends string = 'main'> = AnyExpr<Name> | AnySort<Name> | FuncDecl<Name>;
 
@@ -70,6 +72,8 @@ export type SortToExprMap<S extends AnySort<Name>, Name extends string = 'main'>
   ? FPRM<Name>
   : S extends SeqSort<Name>
   ? Seq<Name>
+  : S extends ReSort<Name>
+  ? Re<Name>
   : S extends Sort<Name>
   ? Expr<Name, S, Z3_ast>
   : never;
@@ -458,6 +462,8 @@ export interface Context<Name extends string = 'main'> {
   /** @category Expressions */
   readonly Seq: SeqCreation<Name>;
   /** @category Expressions */
+  readonly Re: ReCreation<Name>;
+  /** @category Expressions */
   readonly Array: SMTArrayCreation<Name>;
   /** @category Expressions */
   readonly Set: SMTSetCreation<Name>;
@@ -846,6 +852,61 @@ export interface Context<Name extends string = 'main'> {
   /** @category Operations */
   isSubset<ElemSort extends AnySort<Name>>(a: SMTSet<Name, ElemSort>, b: SMTSet<Name, ElemSort>): Bool<Name>;
 
+  //////////////////////
+  // Regular Expressions
+  //////////////////////
+
+  /** @category RegularExpression */
+  InRe(seq: Seq<Name> | string, re: Re<Name>): Bool<Name>;
+
+  /** @category RegularExpression */
+  Union<SeqSortRef extends SeqSort<Name>>(...res: Re<Name, SeqSortRef>[]): Re<Name, SeqSortRef>;
+
+  /** @category RegularExpression */
+  Intersect<SeqSortRef extends SeqSort<Name>>(...res: Re<Name, SeqSortRef>[]): Re<Name, SeqSortRef>;
+
+  /** @category RegularExpression */
+  ReConcat<SeqSortRef extends SeqSort<Name>>(...res: Re<Name, SeqSortRef>[]): Re<Name, SeqSortRef>;
+
+  /** @category RegularExpression */
+  Plus<SeqSortRef extends SeqSort<Name>>(re: Re<Name, SeqSortRef>): Re<Name, SeqSortRef>;
+
+  /** @category RegularExpression */
+  Star<SeqSortRef extends SeqSort<Name>>(re: Re<Name, SeqSortRef>): Re<Name, SeqSortRef>;
+
+  /** @category RegularExpression */
+  Option<SeqSortRef extends SeqSort<Name>>(re: Re<Name, SeqSortRef>): Re<Name, SeqSortRef>;
+
+  /** @category RegularExpression */
+  Complement<SeqSortRef extends SeqSort<Name>>(re: Re<Name, SeqSortRef>): Re<Name, SeqSortRef>;
+
+  /** @category RegularExpression */
+  Diff<SeqSortRef extends SeqSort<Name>>(a: Re<Name, SeqSortRef>, b: Re<Name, SeqSortRef>): Re<Name, SeqSortRef>;
+
+  /** @category RegularExpression */
+  Range<SeqSortRef extends SeqSort<Name>>(lo: Seq<Name, SeqSortRef> | string, hi: Seq<Name, SeqSortRef> | string): Re<Name, SeqSortRef>;
+
+  /**
+   * Create a bounded repetition regex
+   * @param re The regex to repeat
+   * @param lo Minimum number of repetitions
+   * @param hi Maximum number of repetitions (0 means unbounded, i.e., at least lo)
+   * @category RegularExpression
+   */
+  Loop<SeqSortRef extends SeqSort<Name>>(re: Re<Name, SeqSortRef>, lo: number, hi?: number): Re<Name, SeqSortRef>;
+
+  /** @category RegularExpression */
+  Power<SeqSortRef extends SeqSort<Name>>(re: Re<Name, SeqSortRef>, n: number): Re<Name, SeqSortRef>;
+
+  /** @category RegularExpression */
+  AllChar<SeqSortRef extends SeqSort<Name>>(reSort: ReSort<Name, SeqSortRef>): Re<Name, SeqSortRef>;
+
+  /** @category RegularExpression */
+  Empty<SeqSortRef extends SeqSort<Name>>(reSort: ReSort<Name, SeqSortRef>): Re<Name, SeqSortRef>;
+
+  /** @category RegularExpression */
+  Full<SeqSortRef extends SeqSort<Name>>(reSort: ReSort<Name, SeqSortRef>): Re<Name, SeqSortRef>;
+
   /**
    * Create a partial order relation over a sort.
    * @param sort The sort of the relation
@@ -1641,7 +1702,8 @@ export interface Sort<Name extends string = 'main'> extends Ast<Name, Z3_sort> {
     | DatatypeSort['__typename']
     | FPSort['__typename']
     | FPRMSort['__typename']
-    | SeqSort['__typename'];
+    | SeqSort['__typename']
+    | ReSort['__typename'];
 
   kind(): Z3_sort_kind;
 
@@ -1768,6 +1830,7 @@ export interface Expr<Name extends string = 'main', S extends Sort<Name> = AnySo
     | FP['__typename']
     | FPRM['__typename']
     | Seq['__typename']
+    | Re['__typename']
     | SMTArray['__typename']
     | DatatypeExpr['__typename'];
 
@@ -3129,6 +3192,85 @@ export interface Seq<Name extends string = 'main', ElemSort extends Sort<Name> =
   replaceAll(src: Seq<Name, ElemSort> | string, dst: Seq<Name, ElemSort> | string): Seq<Name, ElemSort>;
 }
 
+///////////////////////
+// Regular Expressions
+///////////////////////
+
+/**
+ * Regular expression sort
+ * @category RegularExpression
+ */
+export interface ReSort<Name extends string = 'main', SeqSortRef extends SeqSort<Name> = SeqSort<Name>> extends Sort<Name> {
+  /** @hidden */
+  readonly __typename: 'ReSort';
+
+  /**
+   * Get the basis (underlying sequence sort) of this regular expression sort
+   */
+  basis(): SeqSortRef;
+
+  cast(other: Re<Name, SeqSortRef>): Re<Name, SeqSortRef>;
+  cast(other: CoercibleToExpr<Name>): Expr<Name>;
+}
+
+/** @category RegularExpression */
+export interface ReCreation<Name extends string> {
+  /**
+   * Create a regular expression sort over the given sequence sort
+   */
+  sort<SeqSortRef extends SeqSort<Name>>(seqSort: SeqSortRef): ReSort<Name, SeqSortRef>;
+
+  /**
+   * Convert a sequence to a regular expression that accepts exactly that sequence
+   */
+  toRe(seq: Seq<Name> | string): Re<Name>;
+}
+
+/**
+ * Regular expression expression
+ * @category RegularExpression
+ */
+export interface Re<Name extends string = 'main', SeqSortRef extends SeqSort<Name> = SeqSort<Name>>
+  extends Expr<Name, ReSort<Name, SeqSortRef>, Z3_ast> {
+  /** @hidden */
+  readonly __typename: 'Re';
+
+  /** @category Operations */
+  plus(): Re<Name, SeqSortRef>;
+
+  /** @category Operations */
+  star(): Re<Name, SeqSortRef>;
+
+  /** @category Operations */
+  option(): Re<Name, SeqSortRef>;
+
+  /** @category Operations */
+  complement(): Re<Name, SeqSortRef>;
+
+  /** @category Operations */
+  union(other: Re<Name, SeqSortRef>): Re<Name, SeqSortRef>;
+
+  /** @category Operations */
+  intersect(other: Re<Name, SeqSortRef>): Re<Name, SeqSortRef>;
+
+  /** @category Operations */
+  diff(other: Re<Name, SeqSortRef>): Re<Name, SeqSortRef>;
+
+  /** @category Operations */
+  concat(other: Re<Name, SeqSortRef>): Re<Name, SeqSortRef>;
+
+  /**
+   * Create a bounded repetition of this regex
+   * @param lo Minimum number of repetitions
+   * @param hi Maximum number of repetitions (0 means unbounded, i.e., at least lo)
+   * @category Operations
+   */
+  loop(lo: number, hi?: number): Re<Name, SeqSortRef>;
+
+  /** @category Operations */
+  power(n: number): Re<Name, SeqSortRef>;
+}
+
 /**
  * Defines the expression type of the body of a quantifier expression
  *