diff --git a/README.md b/README.md
index a652119be..c2166b9fe 100644
--- a/README.md
+++ b/README.md
@@ -14,9 +14,9 @@ repositories {
 }
 
 // core 
-implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.0")
+implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.1")
 // z3 solver
-implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.0")
+implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.1")
 ```
 
 ## Usage
diff --git a/Requirements.md b/Requirements.md
index 42990e685..272a2982f 100644
--- a/Requirements.md
+++ b/Requirements.md
@@ -12,7 +12,7 @@
 | [Yices2 solver support](#yices2-solver-support)                                  | Done           |
 | [CVC5 solver support](#cvc5-solver-support)                                      | In progress    |
 | [External process runner](#external-process-runner)                              | Done           |
-| [Portfolio solver](#portfolio-solver)                                            | In progress    |
+| [Portfolio solver](#portfolio-solver)                                            | Done           |
 | [Solver configuration API](#solver-configuration-api)                            | Done           |
 | [Deployment](#deployment)                                                        | Done partially |
 | [Expression simplification / evaluation](#expression-simplification--evaluation) | Done           |
diff --git a/buildSrc/src/main/kotlin/org.ksmt.ksmt-base.gradle.kts b/buildSrc/src/main/kotlin/org.ksmt.ksmt-base.gradle.kts
index 167ffca2a..c1152caaf 100644
--- a/buildSrc/src/main/kotlin/org.ksmt.ksmt-base.gradle.kts
+++ b/buildSrc/src/main/kotlin/org.ksmt.ksmt-base.gradle.kts
@@ -9,7 +9,7 @@ plugins {
 }
 
 group = "org.ksmt"
-version = "0.4.0"
+version = "0.4.1"
 
 repositories {
     mavenCentral()
diff --git a/docs/getting-started.md b/docs/getting-started.md
index 7955709ec..e257b3de8 100644
--- a/docs/getting-started.md
+++ b/docs/getting-started.md
@@ -18,7 +18,7 @@ repositories {
 ```kotlin
 dependencies {
     // core 
-    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.0")    
+    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.1")    
 }
 ```
 
@@ -26,9 +26,9 @@ dependencies {
 ```kotlin
 dependencies {
     // z3 
-    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.0")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.1")
     // bitwuzla
-    implementation("com.github.UnitTestBot.ksmt:ksmt-bitwuzla:0.4.0")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-bitwuzla:0.4.1")
 }
 ```
 SMT solver specific packages are provided with solver native binaries. 
diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts
index 43f1605a6..801332a7a 100644
--- a/examples/build.gradle.kts
+++ b/examples/build.gradle.kts
@@ -10,9 +10,9 @@ repositories {
 
 dependencies {
     // core
-    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.0")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.1")
     // z3 solver
-    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.0")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.1")
 }
 
 java {
diff --git a/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaContext.kt b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaContext.kt
index b678fe7b7..43d93a43d 100644
--- a/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaContext.kt
+++ b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaContext.kt
@@ -3,7 +3,10 @@ package org.ksmt.solver.bitwuzla
 import org.ksmt.KContext
 import org.ksmt.decl.KDecl
 import org.ksmt.decl.KFuncDecl
+import org.ksmt.expr.KArray2Lambda
+import org.ksmt.expr.KArray3Lambda
 import org.ksmt.expr.KArrayLambda
+import org.ksmt.expr.KArrayNLambda
 import org.ksmt.expr.KConst
 import org.ksmt.expr.KExistentialQuantifier
 import org.ksmt.expr.KExpr
@@ -16,7 +19,11 @@ import org.ksmt.solver.bitwuzla.bindings.BitwuzlaNativeException
 import org.ksmt.solver.bitwuzla.bindings.BitwuzlaSort
 import org.ksmt.solver.bitwuzla.bindings.BitwuzlaTerm
 import org.ksmt.solver.bitwuzla.bindings.Native
+import org.ksmt.sort.KArray2Sort
+import org.ksmt.sort.KArray3Sort
+import org.ksmt.sort.KArrayNSort
 import org.ksmt.sort.KArraySort
+import org.ksmt.sort.KArraySortBase
 import org.ksmt.sort.KBoolSort
 import org.ksmt.sort.KBvSort
 import org.ksmt.sort.KFpRoundingModeSort
@@ -277,6 +284,24 @@ open class KBitwuzlaContext(val ctx: KContext) : AutoCloseable {
             sort.range.accept(this)
         }
 
+        override fun <D0 : KSort, D1 : KSort, R : KSort> visit(sort: KArray2Sort<D0, D1, R>) {
+            sort.domain0.accept(this)
+            sort.domain1.accept(this)
+            sort.range.accept(this)
+        }
+
+        override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> visit(sort: KArray3Sort<D0, D1, D2, R>) {
+            sort.domain0.accept(this)
+            sort.domain1.accept(this)
+            sort.domain2.accept(this)
+            sort.range.accept(this)
+        }
+
+        override fun <R : KSort> visit(sort: KArrayNSort<R>) {
+            sort.domainSorts.forEach { it.accept(this) }
+            sort.range.accept(this)
+        }
+
         override fun visit(sort: KBoolSort) {
         }
 
@@ -344,7 +369,7 @@ open class KBitwuzlaContext(val ctx: KContext) : AutoCloseable {
             return super.transform(expr)
         }
 
-        override fun <D : KSort, R : KSort> transform(expr: KFunctionAsArray<D, R>): KExpr<KArraySort<D, R>> {
+        override fun <A : KArraySortBase<R>, R : KSort> transform(expr: KFunctionAsArray<A, R>): KExpr<A> {
             registerDeclIfNotIgnored(expr.function)
             return super.transform(expr)
         }
@@ -365,7 +390,20 @@ open class KBitwuzlaContext(val ctx: KContext) : AutoCloseable {
         }
 
         override fun <D : KSort, R : KSort> transform(expr: KArrayLambda<D, R>): KExpr<KArraySort<D, R>> =
-            expr.transformQuantifier(listOf(expr.indexVarDecl), expr.body)
+            expr.transformQuantifier(expr.indexVarDeclarations, expr.body)
+
+        override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+            expr: KArray2Lambda<D0, D1, R>
+        ): KExpr<KArray2Sort<D0, D1, R>> =
+            expr.transformQuantifier(expr.indexVarDeclarations, expr.body)
+
+        override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+            expr: KArray3Lambda<D0, D1, D2, R>
+        ): KExpr<KArray3Sort<D0, D1, D2, R>> =
+            expr.transformQuantifier(expr.indexVarDeclarations, expr.body)
+
+        override fun <R : KSort> transform(expr: KArrayNLambda<R>): KExpr<KArrayNSort<R>> =
+            expr.transformQuantifier(expr.indexVarDeclarations, expr.body)
 
         override fun transform(expr: KExistentialQuantifier): KExpr<KBoolSort> =
             expr.transformQuantifier(expr.bounds, expr.body)
diff --git a/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaExprConverter.kt b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaExprConverter.kt
index 65d148c62..a0d82692b 100644
--- a/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaExprConverter.kt
+++ b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaExprConverter.kt
@@ -136,7 +136,7 @@ open class KBitwuzlaExprConverter(
 
             // array
             BitwuzlaKind.BITWUZLA_KIND_CONST_ARRAY -> expr.convert { value: KExpr<KSort> ->
-                val sort = Native.bitwuzlaTermGetSort(expr).convertSort() as KArraySort<*, *>
+                val sort: KArraySort<KSort, KSort> = Native.bitwuzlaTermGetSort(expr).convertSort().uncheckedCast()
                 convertConstArrayExpr(sort, value)
             }
 
@@ -652,7 +652,7 @@ open class KBitwuzlaExprConverter(
     fun convertConstArrayExpr(
         currentSort: KArraySort<KSort, KSort>,
         value: KExpr<KSort>
-    ): KArrayConst<KSort, KSort> = with(ctx) {
+    ): KArrayConst<KArraySort<KSort, KSort>, KSort> = with(ctx) {
         val expectedValueSort = selectExpectedSort(currentSort.range, value.sort)
         val expectedArraySort = mkArraySort(currentSort.domain, expectedValueSort)
         return mkArrayConst(expectedArraySort, value.convertToExpectedIfNeeded(expectedValueSort))
@@ -796,7 +796,8 @@ open class KBitwuzlaExprConverter(
                 check(expectedDomain !is KArraySort<*, *> && expectedRange !is KArraySort<*, *>) {
                     "Bitwuzla doesn't support nested arrays"
                 }
-                ArrayAdapterExpr(this@ensureArrayExprSortMatch, expectedDomain, expectedRange)
+                val array: KExpr<KArraySort<KSort, KSort>> = this@ensureArrayExprSortMatch.uncheckedCast()
+                ArrayAdapterExpr(array, expectedDomain, expectedRange)
             }
         }
     }
diff --git a/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaExprInternalizer.kt b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaExprInternalizer.kt
index 7680d39cf..c867b7f89 100644
--- a/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaExprInternalizer.kt
+++ b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaExprInternalizer.kt
@@ -7,8 +7,17 @@ import org.ksmt.decl.KDeclVisitor
 import org.ksmt.decl.KFuncDecl
 import org.ksmt.expr.KAddArithExpr
 import org.ksmt.expr.KAndExpr
+import org.ksmt.expr.KArray2Lambda
+import org.ksmt.expr.KArray2Select
+import org.ksmt.expr.KArray2Store
+import org.ksmt.expr.KArray3Lambda
+import org.ksmt.expr.KArray3Select
+import org.ksmt.expr.KArray3Store
 import org.ksmt.expr.KArrayConst
 import org.ksmt.expr.KArrayLambda
+import org.ksmt.expr.KArrayNLambda
+import org.ksmt.expr.KArrayNSelect
+import org.ksmt.expr.KArrayNStore
 import org.ksmt.expr.KArraySelect
 import org.ksmt.expr.KArrayStore
 import org.ksmt.expr.KBitVec16Value
@@ -148,7 +157,11 @@ import org.ksmt.solver.bitwuzla.bindings.BitwuzlaTerm
 import org.ksmt.solver.bitwuzla.bindings.Native
 import org.ksmt.solver.util.KExprInternalizerBase
 import org.ksmt.sort.KArithSort
+import org.ksmt.sort.KArray2Sort
+import org.ksmt.sort.KArray3Sort
+import org.ksmt.sort.KArrayNSort
 import org.ksmt.sort.KArraySort
+import org.ksmt.sort.KArraySortBase
 import org.ksmt.sort.KBoolSort
 import org.ksmt.sort.KBv16Sort
 import org.ksmt.sort.KBv32Sort
@@ -696,6 +709,22 @@ open class KBitwuzlaExprInternalizer(
         }
     }
 
+    override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+        expr: KArray2Store<D0, D1, R>
+    ): KExpr<KArray2Sort<D0, D1, R>> {
+        TODO("Multi-indexed arrays are not supported")
+    }
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Store<D0, D1, D2, R>
+    ): KExpr<KArray3Sort<D0, D1, D2, R>> {
+        TODO("Multi-indexed arrays are not supported")
+    }
+
+    override fun <R : KSort> transform(expr: KArrayNStore<R>): KExpr<KArrayNSort<R>> {
+        TODO("Multi-indexed arrays are not supported")
+    }
+
     override fun <D : KSort, R : KSort> transform(expr: KArraySelect<D, R>) = with(expr) {
         transform(array, index) { a: BitwuzlaTerm, i: BitwuzlaTerm ->
             mkArraySelectTerm(Native.bitwuzlaTermGetBitwuzlaKind(a), a, i)
@@ -709,7 +738,21 @@ open class KBitwuzlaExprInternalizer(
             Native.bitwuzlaMkTerm2(bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_ARRAY_SELECT, array, idx)
         }
 
-    override fun <D : KSort, R : KSort> transform(expr: KArrayConst<D, R>) = with(expr) {
+    override fun <D0 : KSort, D1 : KSort, R : KSort> transform(expr: KArray2Select<D0, D1, R>): KExpr<R> {
+        TODO("Multi-indexed arrays are not supported")
+    }
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Select<D0, D1, D2, R>
+    ): KExpr<R> {
+        TODO("Multi-indexed arrays are not supported")
+    }
+
+    override fun <R : KSort> transform(expr: KArrayNSelect<R>): KExpr<R> {
+        TODO("Multi-indexed arrays are not supported")
+    }
+
+    override fun <A : KArraySortBase<R>, R : KSort> transform(expr: KArrayConst<A, R>) = with(expr) {
         transform(value) { value: BitwuzlaTerm ->
             Native.bitwuzlaMkConstArray(bitwuzlaCtx.bitwuzla, sort.internalizeSort(), value)
         }
@@ -732,6 +775,24 @@ open class KBitwuzlaExprInternalizer(
     private fun mkLambdaTerm(boundVar: BitwuzlaTerm, body: BitwuzlaTerm): BitwuzlaTerm =
         Native.bitwuzlaMkTerm2(bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_LAMBDA, boundVar, body)
 
+    override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+        expr: KArray2Lambda<D0, D1, R>
+    ): KExpr<KArray2Sort<D0, D1, R>> {
+        TODO("Multi-indexed arrays are not supported")
+    }
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Lambda<D0, D1, D2, R>
+    ): KExpr<KArray3Sort<D0, D1, D2, R>> {
+        TODO("Multi-indexed arrays are not supported")
+    }
+
+    override fun <R : KSort> transform(
+        expr: KArrayNLambda<R>
+    ): KExpr<KArrayNSort<R>> {
+        TODO("Multi-indexed arrays are not supported")
+    }
+
     override fun transform(
         expr: KExistentialQuantifier
     ): KExpr<KBoolSort> = expr.internalizeQuantifier { args ->
@@ -1007,7 +1068,7 @@ open class KBitwuzlaExprInternalizer(
         }
     }
 
-    override fun <D : KSort, R : KSort> transform(expr: KFunctionAsArray<D, R>): KExpr<KArraySort<D, R>> {
+    override fun <A : KArraySortBase<R>, R : KSort> transform(expr: KFunctionAsArray<A, R>): KExpr<A> {
         TODO("KFunctionAsArray internalization is not implemented in bitwuzla")
     }
 
@@ -1079,6 +1140,20 @@ open class KBitwuzlaExprInternalizer(
                 Native.bitwuzlaMkArraySort(bitwuzlaCtx.bitwuzla, domain, range)
             }
 
+        override fun <D0 : KSort, D1 : KSort, R : KSort> visit(sort: KArray2Sort<D0, D1, R>): BitwuzlaSort {
+            TODO("Multi-indexed arrays are not supported")
+        }
+
+        override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> visit(
+            sort: KArray3Sort<D0, D1, D2, R>
+        ): BitwuzlaSort {
+            TODO("Multi-indexed arrays are not supported")
+        }
+
+        override fun <R : KSort> visit(sort: KArrayNSort<R>): BitwuzlaSort {
+            TODO("Multi-indexed arrays are not supported")
+        }
+
         override fun <S : KBvSort> visit(sort: S): BitwuzlaSort =
             bitwuzlaCtx.internalizeSort(sort) {
                 val size = sort.sizeBits.toInt()
@@ -1208,6 +1283,16 @@ open class KBitwuzlaExprInternalizer(
         override fun <D : KSort, R : KSort> visit(sort: KArraySort<D, R>): Boolean =
             sort.domain.accept(this) || sort.range.accept(this)
 
+        override fun <D0 : KSort, D1 : KSort, R : KSort> visit(sort: KArray2Sort<D0, D1, R>): Boolean =
+            sort.domain0.accept(this) || sort.domain1.accept(this) || sort.range.accept(this)
+
+        override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> visit(sort: KArray3Sort<D0, D1, D2, R>): Boolean =
+            sort.domain0.accept(this) || sort.domain1.accept(this)
+                || sort.domain2.accept(this) || sort.range.accept(this)
+
+        override fun <R : KSort> visit(sort: KArrayNSort<R>): Boolean =
+            sort.domainSorts.any { it.accept(this) } || sort.range.accept(this)
+
         override fun visit(sort: KBoolSort): Boolean = false
         override fun visit(sort: KIntSort): Boolean = false
         override fun visit(sort: KRealSort): Boolean = false
diff --git a/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaModel.kt b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaModel.kt
index 13d583a2e..645c36d15 100644
--- a/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaModel.kt
+++ b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaModel.kt
@@ -142,7 +142,7 @@ open class KBitwuzlaModel(
         decl: KDecl<T>,
         term: BitwuzlaTerm
     ): KModel.KFuncInterp<T> = with(converter) {
-        val sort = decl.sort as KArraySort<*, *>
+        val sort: KArraySort<KSort, KSort> = decl.sort.uncheckedCast()
         val entries = mutableListOf<KModel.KFuncInterpEntry<KSort>>()
         val interp = Native.bitwuzlaGetArrayValue(bitwuzlaCtx.bitwuzla, term)
 
@@ -168,7 +168,7 @@ open class KBitwuzlaModel(
             decl = decl,
             vars = emptyList(),
             entries = emptyList(),
-            default = mkFunctionAsArray<KSort, KSort>(arrayInterpDecl).uncheckedCast()
+            default = mkFunctionAsArray(sort, arrayInterpDecl).uncheckedCast()
         )
     }
 
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/KContext.kt b/ksmt-core/src/main/kotlin/org/ksmt/KContext.kt
index 2749089b6..fd8612688 100644
--- a/ksmt-core/src/main/kotlin/org/ksmt/KContext.kt
+++ b/ksmt-core/src/main/kotlin/org/ksmt/KContext.kt
@@ -21,7 +21,13 @@ import org.ksmt.decl.KArithMulDecl
 import org.ksmt.decl.KArithPowerDecl
 import org.ksmt.decl.KArithSubDecl
 import org.ksmt.decl.KArithUnaryMinusDecl
+import org.ksmt.decl.KArray2SelectDecl
+import org.ksmt.decl.KArray2StoreDecl
+import org.ksmt.decl.KArray3SelectDecl
+import org.ksmt.decl.KArray3StoreDecl
 import org.ksmt.decl.KArrayConstDecl
+import org.ksmt.decl.KArrayNSelectDecl
+import org.ksmt.decl.KArrayNStoreDecl
 import org.ksmt.decl.KArraySelectDecl
 import org.ksmt.decl.KArrayStoreDecl
 import org.ksmt.decl.KBitVec16ValueDecl
@@ -139,8 +145,17 @@ import org.ksmt.decl.KZeroExtDecl
 import org.ksmt.expr.KAddArithExpr
 import org.ksmt.expr.KAndExpr
 import org.ksmt.expr.KApp
+import org.ksmt.expr.KArray2Lambda
+import org.ksmt.expr.KArray2Select
+import org.ksmt.expr.KArray2Store
+import org.ksmt.expr.KArray3Lambda
+import org.ksmt.expr.KArray3Select
+import org.ksmt.expr.KArray3Store
 import org.ksmt.expr.KArrayConst
 import org.ksmt.expr.KArrayLambda
+import org.ksmt.expr.KArrayNLambda
+import org.ksmt.expr.KArrayNSelect
+import org.ksmt.expr.KArrayNStore
 import org.ksmt.expr.KArraySelect
 import org.ksmt.expr.KArrayStore
 import org.ksmt.expr.KBitVec16Value
@@ -283,7 +298,9 @@ import org.ksmt.expr.rewrite.simplify.simplifyArithPower
 import org.ksmt.expr.rewrite.simplify.simplifyArithSub
 import org.ksmt.expr.rewrite.simplify.simplifyArithUnaryMinus
 import org.ksmt.expr.rewrite.simplify.simplifyArraySelect
+import org.ksmt.expr.rewrite.simplify.simplifyArrayNSelect
 import org.ksmt.expr.rewrite.simplify.simplifyArrayStore
+import org.ksmt.expr.rewrite.simplify.simplifyArrayNStore
 import org.ksmt.expr.rewrite.simplify.simplifyBv2IntExpr
 import org.ksmt.expr.rewrite.simplify.simplifyBvAddExpr
 import org.ksmt.expr.rewrite.simplify.simplifyBvAddNoOverflowExpr
@@ -375,7 +392,11 @@ import org.ksmt.expr.rewrite.simplify.simplifyRealToFpExpr
 import org.ksmt.expr.rewrite.simplify.simplifyRealToInt
 import org.ksmt.expr.rewrite.simplify.simplifyXor
 import org.ksmt.sort.KArithSort
+import org.ksmt.sort.KArray2Sort
+import org.ksmt.sort.KArray3Sort
+import org.ksmt.sort.KArrayNSort
 import org.ksmt.sort.KArraySort
+import org.ksmt.sort.KArraySortBase
 import org.ksmt.sort.KBoolSort
 import org.ksmt.sort.KBv16Sort
 import org.ksmt.sort.KBv1Sort
@@ -487,12 +508,41 @@ open class KContext(
 
     fun mkBoolSort(): KBoolSort = boolSort
 
-    private val arraySortCache = mkCache<Pair<KSort, KSort>, KArraySort<*, *>>(operationMode)
+    private val arraySortCache = mkCache<KArraySort<*, *>, KArraySort<*, *>>(operationMode)
+    private val array2SortCache = mkCache<KArray2Sort<*, *, *>, KArray2Sort<*, *, *>>(operationMode)
+    private val array3SortCache = mkCache<KArray3Sort<*, *, *, *>, KArray3Sort<*, *, *, *>>(operationMode)
+    private val arrayNSortCache = mkCache<KArrayNSort<*>, KArrayNSort<*>>(operationMode)
 
     fun <D : KSort, R : KSort> mkArraySort(domain: D, range: R): KArraySort<D, R> =
         ensureContextActive {
             ensureContextMatch(domain, range)
-            arraySortCache.getOrPut(domain to range) { KArraySort(this, domain, range) }.uncheckedCast()
+            val sort = KArraySort(this, domain, range)
+            (arraySortCache.putIfAbsent(sort, sort) ?: sort).uncheckedCast()
+        }
+
+    fun <D0 : KSort, D1 : KSort, R : KSort> mkArraySort(domain0: D0, domain1: D1, range: R): KArray2Sort<D0, D1, R> =
+        ensureContextActive {
+            ensureContextMatch(domain0, domain1, range)
+            val sort = KArray2Sort(this, domain0, domain1, range)
+            (array2SortCache.putIfAbsent(sort, sort) ?: sort).uncheckedCast()
+        }
+
+    fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> mkArraySort(
+        domain0: D0, domain1: D1, domain2: D2, range: R
+    ): KArray3Sort<D0, D1, D2, R> =
+        ensureContextActive {
+            ensureContextMatch(domain0, domain1, domain2, range)
+            val sort = KArray3Sort(this, domain0, domain1, domain2, range)
+            (array3SortCache.putIfAbsent(sort, sort) ?: sort).uncheckedCast()
+        }
+
+    fun <R : KSort> mkArrayNSort(domain: List<KSort>, range: R): KArrayNSort<R> =
+        ensureContextActive {
+            ensureContextMatch(range)
+            ensureContextMatch(domain)
+
+            val sort = KArrayNSort(this, domain, range)
+            (arrayNSortCache.putIfAbsent(sort, sort) ?: sort).uncheckedCast()
         }
 
     private val intSortCache by lazy {
@@ -760,6 +810,9 @@ open class KContext(
 
     // array
     private val arrayStoreCache = mkAstInterner<KArrayStore<out KSort, out KSort>>()
+    private val array2StoreCache = mkAstInterner<KArray2Store<out KSort, out KSort, out KSort>>()
+    private val array3StoreCache = mkAstInterner<KArray3Store<out KSort, out KSort, out KSort, out KSort>>()
+    private val arrayNStoreCache = mkAstInterner<KArrayNStore<out KSort>>()
 
     fun <D : KSort, R : KSort> mkArrayStore(
         array: KExpr<KArraySort<D, R>>,
@@ -768,6 +821,30 @@ open class KContext(
     ): KExpr<KArraySort<D, R>> =
         mkSimplified(array, index, value, KContext::simplifyArrayStore, ::mkArrayStoreNoSimplify)
 
+    fun <D0 : KSort, D1 : KSort, R : KSort> mkArrayStore(
+        array: KExpr<KArray2Sort<D0, D1, R>>,
+        index0: KExpr<D0>,
+        index1: KExpr<D1>,
+        value: KExpr<R>
+    ): KExpr<KArray2Sort<D0, D1, R>> =
+        mkSimplified(array, index0, index1, value, KContext::simplifyArrayStore, ::mkArrayStoreNoSimplify)
+
+    fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> mkArrayStore(
+        array: KExpr<KArray3Sort<D0, D1, D2, R>>,
+        index0: KExpr<D0>,
+        index1: KExpr<D1>,
+        index2: KExpr<D2>,
+        value: KExpr<R>
+    ): KExpr<KArray3Sort<D0, D1, D2, R>> =
+        mkSimplified(array, index0, index1, index2, value, KContext::simplifyArrayStore, ::mkArrayStoreNoSimplify)
+
+    fun <R : KSort> mkArrayNStore(
+        array: KExpr<KArrayNSort<R>>,
+        indices: List<KExpr<*>>,
+        value: KExpr<R>
+    ): KExpr<KArrayNSort<R>> =
+        mkSimplified(array, indices, value, KContext::simplifyArrayNStore, ::mkArrayNStoreNoSimplify)
+
     fun <D : KSort, R : KSort> mkArrayStoreNoSimplify(
         array: KExpr<KArraySort<D, R>>,
         index: KExpr<D>,
@@ -777,13 +854,66 @@ open class KContext(
         KArrayStore(this, array, index, value)
     }.cast()
 
+    fun <D0 : KSort, D1 : KSort, R : KSort> mkArrayStoreNoSimplify(
+        array: KExpr<KArray2Sort<D0, D1, R>>,
+        index0: KExpr<D0>,
+        index1: KExpr<D1>,
+        value: KExpr<R>
+    ): KArray2Store<D0, D1, R> = array2StoreCache.createIfContextActive {
+        ensureContextMatch(array, index0, index1, value)
+        KArray2Store(this, array, index0, index1, value)
+    }.cast()
+
+    fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> mkArrayStoreNoSimplify(
+        array: KExpr<KArray3Sort<D0, D1, D2, R>>,
+        index0: KExpr<D0>,
+        index1: KExpr<D1>,
+        index2: KExpr<D2>,
+        value: KExpr<R>
+    ): KArray3Store<D0, D1, D2, R> = array3StoreCache.createIfContextActive {
+        ensureContextMatch(array, index0, index1, index2, value)
+        KArray3Store(this, array, index0, index1, index2, value)
+    }.cast()
+
+    fun <R : KSort> mkArrayNStoreNoSimplify(
+        array: KExpr<KArrayNSort<R>>,
+        indices: List<KExpr<*>>,
+        value: KExpr<R>
+    ): KArrayNStore<R> = arrayNStoreCache.createIfContextActive {
+        ensureContextMatch(indices)
+        ensureContextMatch(array, value)
+
+        KArrayNStore(this, array, indices.uncheckedCast(), value)
+    }.cast()
+
     private val arraySelectCache = mkAstInterner<KArraySelect<out KSort, out KSort>>()
+    private val array2SelectCache = mkAstInterner<KArray2Select<out KSort, out KSort, out KSort>>()
+    private val array3SelectCache = mkAstInterner<KArray3Select<out KSort, out KSort, out KSort, out KSort>>()
+    private val arrayNSelectCache = mkAstInterner<KArrayNSelect<out KSort>>()
 
     fun <D : KSort, R : KSort> mkArraySelect(
         array: KExpr<KArraySort<D, R>>,
         index: KExpr<D>
     ): KExpr<R> = mkSimplified(array, index, KContext::simplifyArraySelect, ::mkArraySelectNoSimplify)
 
+    fun <D0 : KSort, D1 : KSort, R : KSort> mkArraySelect(
+        array: KExpr<KArray2Sort<D0, D1, R>>,
+        index0: KExpr<D0>,
+        index1: KExpr<D1>
+    ): KExpr<R> = mkSimplified(array, index0, index1, KContext::simplifyArraySelect, ::mkArraySelectNoSimplify)
+
+    fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> mkArraySelect(
+        array: KExpr<KArray3Sort<D0, D1, D2, R>>,
+        index0: KExpr<D0>,
+        index1: KExpr<D1>,
+        index2: KExpr<D2>
+    ): KExpr<R> = mkSimplified(array, index0, index1, index2, KContext::simplifyArraySelect, ::mkArraySelectNoSimplify)
+
+    fun <R : KSort> mkArrayNSelect(
+        array: KExpr<KArrayNSort<R>>,
+        indices: List<KExpr<*>>
+    ): KExpr<R> = mkSimplified(array, indices, KContext::simplifyArrayNSelect, ::mkArrayNSelectNoSimplify)
+
     fun <D : KSort, R : KSort> mkArraySelectNoSimplify(
         array: KExpr<KArraySort<D, R>>,
         index: KExpr<D>
@@ -792,37 +922,112 @@ open class KContext(
         KArraySelect(this, array, index)
     }.cast()
 
-    private val arrayConstCache = mkAstInterner<KArrayConst<out KSort, out KSort>>()
+    fun <D0 : KSort, D1 : KSort, R : KSort> mkArraySelectNoSimplify(
+        array: KExpr<KArray2Sort<D0, D1, R>>,
+        index0: KExpr<D0>,
+        index1: KExpr<D1>
+    ): KArray2Select<D0, D1, R> = array2SelectCache.createIfContextActive {
+        ensureContextMatch(array, index0, index1)
+        KArray2Select(this, array, index0, index1)
+    }.cast()
+
+    fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> mkArraySelectNoSimplify(
+        array: KExpr<KArray3Sort<D0, D1, D2, R>>,
+        index0: KExpr<D0>,
+        index1: KExpr<D1>,
+        index2: KExpr<D2>
+    ): KArray3Select<D0, D1, D2, R> = array3SelectCache.createIfContextActive {
+        ensureContextMatch(array, index0, index1, index2)
+        KArray3Select(this, array, index0, index1, index2)
+    }.cast()
+
+    fun <R : KSort> mkArrayNSelectNoSimplify(
+        array: KExpr<KArrayNSort<R>>,
+        indices: List<KExpr<*>>
+    ): KArrayNSelect<R> = arrayNSelectCache.createIfContextActive {
+        ensureContextMatch(array)
+        ensureContextMatch(indices)
 
-    fun <D : KSort, R : KSort> mkArrayConst(
-        arraySort: KArraySort<D, R>,
+        KArrayNSelect(this, array, indices.uncheckedCast())
+    }.cast()
+
+    private val arrayConstCache = mkAstInterner<KArrayConst<out KArraySortBase<out KSort>, out KSort>>()
+
+    fun <A : KArraySortBase<R>, R : KSort> mkArrayConst(
+        arraySort: A,
         value: KExpr<R>
-    ): KArrayConst<D, R> = arrayConstCache.createIfContextActive {
+    ): KArrayConst<A, R> = arrayConstCache.createIfContextActive {
         ensureContextMatch(arraySort, value)
         KArrayConst(this, arraySort, value)
     }.cast()
 
-    private val functionAsArrayCache = mkAstInterner<KFunctionAsArray<out KSort, out KSort>>()
+    private val functionAsArrayCache = mkAstInterner<KFunctionAsArray<out KArraySortBase<out KSort>, out KSort>>()
 
-    fun <D : KSort, R : KSort> mkFunctionAsArray(function: KFuncDecl<R>): KFunctionAsArray<D, R> =
+    fun <A : KArraySortBase<R>, R : KSort> mkFunctionAsArray(sort: A, function: KFuncDecl<R>): KFunctionAsArray<A, R> =
         functionAsArrayCache.createIfContextActive {
             ensureContextMatch(function)
-            KFunctionAsArray<D, R>(this, function)
+            KFunctionAsArray(this, sort, function)
         }.cast()
 
     private val arrayLambdaCache = mkAstInterner<KArrayLambda<out KSort, out KSort>>()
+    private val array2LambdaCache = mkAstInterner<KArray2Lambda<out KSort, out KSort, out KSort>>()
+    private val array3LambdaCache = mkAstInterner<KArray3Lambda<out KSort, out KSort, out KSort, out KSort>>()
+    private val arrayNLambdaCache = mkAstInterner<KArrayNLambda<out KSort>>()
+
+    fun <D : KSort, R : KSort> mkArrayLambda(
+        indexVar: KDecl<D>, body: KExpr<R>
+    ): KArrayLambda<D, R> = arrayLambdaCache.createIfContextActive {
+        ensureContextMatch(indexVar, body)
+        KArrayLambda(this, indexVar, body)
+    }.cast()
 
-    fun <D : KSort, R : KSort> mkArrayLambda(indexVar: KDecl<D>, body: KExpr<R>): KArrayLambda<D, R> =
-        arrayLambdaCache.createIfContextActive {
-            ensureContextMatch(indexVar, body)
-            KArrayLambda(this, indexVar, body)
-        }.cast()
+    fun <D0 : KSort, D1 : KSort, R : KSort> mkArrayLambda(
+        indexVar0: KDecl<D0>, indexVar1: KDecl<D1>, body: KExpr<R>
+    ): KArray2Lambda<D0, D1, R> = array2LambdaCache.createIfContextActive {
+        ensureContextMatch(indexVar0, indexVar1, body)
+        KArray2Lambda(this, indexVar0, indexVar1, body)
+    }.cast()
+
+    fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> mkArrayLambda(
+        indexVar0: KDecl<D0>, indexVar1: KDecl<D1>, indexVar2: KDecl<D2>, body: KExpr<R>
+    ): KArray3Lambda<D0, D1, D2, R> = array3LambdaCache.createIfContextActive {
+        ensureContextMatch(indexVar0, indexVar1, indexVar2, body)
+        KArray3Lambda(this, indexVar0, indexVar1, indexVar2, body)
+    }.cast()
+
+    fun <R : KSort> mkArrayNLambda(
+        indices: List<KDecl<*>>, body: KExpr<R>
+    ): KArrayNLambda<R> = arrayNLambdaCache.createIfContextActive {
+        ensureContextMatch(indices)
+        ensureContextMatch(body)
+
+        KArrayNLambda(this, indices, body)
+    }.cast()
 
     fun <D : KSort, R : KSort> KExpr<KArraySort<D, R>>.store(index: KExpr<D>, value: KExpr<R>) =
         mkArrayStore(this, index, value)
 
+    fun <D0 : KSort, D1 : KSort, R : KSort> KExpr<KArray2Sort<D0, D1, R>>.store(
+        index0: KExpr<D0>, index1: KExpr<D1>, value: KExpr<R>
+    ) = mkArrayStore(this, index0, index1, value)
+
+    fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> KExpr<KArray3Sort<D0, D1, D2, R>>.store(
+        index0: KExpr<D0>, index1: KExpr<D1>, index2: KExpr<D2>, value: KExpr<R>
+    ) = mkArrayStore(this, index0, index1, index2, value)
+
     fun <D : KSort, R : KSort> KExpr<KArraySort<D, R>>.select(index: KExpr<D>) = mkArraySelect(this, index)
 
+    fun <D0 : KSort, D1 : KSort, R : KSort> KExpr<KArray2Sort<D0, D1, R>>.select(
+        index0: KExpr<D0>,
+        index1: KExpr<D1>
+    ) = mkArraySelect(this, index0, index1)
+
+    fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> KExpr<KArray3Sort<D0, D1, D2, R>>.select(
+        index0: KExpr<D0>,
+        index1: KExpr<D1>,
+        index2: KExpr<D2>
+    ) = mkArraySelect(this, index0, index1, index2)
+
     // arith
     private val arithAddCache = mkAstInterner<KAddArithExpr<out KArithSort>>()
 
@@ -1764,6 +1969,7 @@ open class KContext(
             mkFp16WithoutNaNCheck(normalizedValue)
         }
     }
+
     fun mkFp16NaN(): KFp16Value = mkFp16WithoutNaNCheck(Float.NaN)
     private fun mkFp16WithoutNaNCheck(value: Float): KFp16Value =
         fp16Cache.createIfContextActive { KFp16Value(this, value) }
@@ -1791,9 +1997,9 @@ open class KContext(
         biasedExponent: KBitVecValue<*>,
         signBit: Boolean
     ): KFp128Value = fp128Cache.createIfContextActive {
-            ensureContextMatch(significand, biasedExponent)
-            KFp128Value(this, significand, biasedExponent, signBit)
-        }
+        ensureContextMatch(significand, biasedExponent)
+        KFp128Value(this, significand, biasedExponent, signBit)
+    }
 
     fun mkFp128(significand: KBitVecValue<*>, unbiasedExponent: KBitVecValue<*>, signBit: Boolean): KFp128Value =
         mkFp128Biased(
@@ -1906,7 +2112,7 @@ open class KContext(
         significand: KBitVecValue<*>,
         biasedExponent: KBitVecValue<*>,
         signBit: Boolean
-    ): KFpValue<T>  {
+    ): KFpValue<T> {
         val intSignBit = if (signBit) 1 else 0
 
         return when (sort) {
@@ -2708,10 +2914,32 @@ open class KContext(
     fun <D : KSort, R : KSort> mkArraySelectDecl(array: KArraySort<D, R>): KArraySelectDecl<D, R> =
         KArraySelectDecl(this, array)
 
+    fun <D0 : KSort, D1 : KSort, R : KSort> mkArraySelectDecl(
+        array: KArray2Sort<D0, D1, R>
+    ): KArray2SelectDecl<D0, D1, R> = KArray2SelectDecl(this, array)
+
+    fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> mkArraySelectDecl(
+        array: KArray3Sort<D0, D1, D2, R>
+    ): KArray3SelectDecl<D0, D1, D2, R> = KArray3SelectDecl(this, array)
+
+    fun <R : KSort> mkArrayNSelectDecl(array: KArrayNSort<R>): KArrayNSelectDecl<R> =
+        KArrayNSelectDecl(this, array)
+
     fun <D : KSort, R : KSort> mkArrayStoreDecl(array: KArraySort<D, R>): KArrayStoreDecl<D, R> =
         KArrayStoreDecl(this, array)
 
-    fun <D : KSort, R : KSort> mkArrayConstDecl(array: KArraySort<D, R>): KArrayConstDecl<D, R> =
+    fun <D0 : KSort, D1 : KSort, R : KSort> mkArrayStoreDecl(
+        array: KArray2Sort<D0, D1, R>
+    ): KArray2StoreDecl<D0, D1, R> = KArray2StoreDecl(this, array)
+
+    fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> mkArrayStoreDecl(
+        array: KArray3Sort<D0, D1, D2, R>
+    ): KArray3StoreDecl<D0, D1, D2, R> = KArray3StoreDecl(this, array)
+
+    fun <R : KSort> mkArrayNStoreDecl(array: KArrayNSort<R>): KArrayNStoreDecl<R> =
+        KArrayNStoreDecl(this, array)
+
+    fun <A : KArraySortBase<R>, R : KSort> mkArrayConstDecl(array: A): KArrayConstDecl<A, R> =
         KArrayConstDecl(this, array)
 
     // arith
@@ -3244,4 +3472,16 @@ open class KContext(
             NO_SIMPLIFY -> createNoSimplify(a0, a1, a2, a3)
         }
     }
+
+    @Suppress("LongParameterList")
+    private inline fun <T : KSort, A0, A1, A2, A3, A4> mkSimplified(
+        a0: A0, a1: A1, a2: A2, a3: A3, a4: A4,
+        simplifier: KContext.(A0, A1, A2, A3, A4) -> KExpr<T>,
+        createNoSimplify: (A0, A1, A2, A3, A4) -> KExpr<T>
+    ): KExpr<T> = ensureContextActive {
+        when (simplificationMode) {
+            SIMPLIFY -> simplifier(a0, a1, a2, a3, a4)
+            NO_SIMPLIFY -> createNoSimplify(a0, a1, a2, a3, a4)
+        }
+    }
 }
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/decl/Array.kt b/ksmt-core/src/main/kotlin/org/ksmt/decl/Array.kt
index 71b00b76f..c62b5043d 100644
--- a/ksmt-core/src/main/kotlin/org/ksmt/decl/Array.kt
+++ b/ksmt-core/src/main/kotlin/org/ksmt/decl/Array.kt
@@ -3,51 +3,168 @@ package org.ksmt.decl
 import org.ksmt.KContext
 import org.ksmt.expr.KApp
 import org.ksmt.expr.KExpr
+import org.ksmt.sort.KArray2Sort
+import org.ksmt.sort.KArray3Sort
+import org.ksmt.sort.KArrayNSort
 import org.ksmt.sort.KArraySort
+import org.ksmt.sort.KArraySortBase
 import org.ksmt.sort.KSort
+import org.ksmt.utils.uncheckedCast
 
-class KArrayStoreDecl<D : KSort, R : KSort> internal constructor(
+sealed class KArrayStoreDeclBase<A : KArraySortBase<R>, R : KSort>(
     ctx: KContext,
-    sort: KArraySort<D, R>
-) : KFuncDecl3<KArraySort<D, R>, KArraySort<D, R>, D, R>(
-    ctx,
+    sort: A
+) : KFuncDecl<A>(
+    ctx = ctx,
     name = "store",
     resultSort = sort,
-    arg0Sort = sort,
-    arg1Sort = sort.domain,
-    arg2Sort = sort.range
-) {
-    override fun KContext.apply(
-        arg0: KExpr<KArraySort<D, R>>,
-        arg1: KExpr<D>, arg2: KExpr<R>
-    ): KApp<KArraySort<D, R>, *> = mkArrayStoreNoSimplify(arg0, arg1, arg2)
+    argSorts = buildList {
+        add(sort)
+        addAll(sort.domainSorts)
+        add(sort.range)
+    }
+)
+
+class KArrayStoreDecl<D : KSort, R : KSort> internal constructor(
+    ctx: KContext,
+    sort: KArraySort<D, R>
+) : KArrayStoreDeclBase<KArraySort<D, R>, R>(ctx, sort) {
+    override fun apply(args: List<KExpr<*>>): KApp<KArraySort<D, R>, *> {
+        val (array, index, value) = args
+        return ctx.mkArrayStoreNoSimplify(
+            array = array.uncheckedCast(),
+            index = index.uncheckedCast(),
+            value = value.uncheckedCast()
+        )
+    }
+
+    override fun <R> accept(visitor: KDeclVisitor<R>): R = visitor.visit(this)
+}
+
+class KArray2StoreDecl<D0 : KSort, D1 : KSort, R : KSort> internal constructor(
+    ctx: KContext,
+    sort: KArray2Sort<D0, D1, R>
+) : KArrayStoreDeclBase<KArray2Sort<D0, D1, R>, R>(ctx, sort) {
+    override fun apply(args: List<KExpr<*>>): KApp<KArray2Sort<D0, D1, R>, *> {
+        val (array, index0, index1, value) = args
+        return ctx.mkArrayStoreNoSimplify(
+            array = array.uncheckedCast(),
+            index0 = index0.uncheckedCast(),
+            index1 = index1.uncheckedCast(),
+            value = value.uncheckedCast()
+        )
+    }
 
     override fun <R> accept(visitor: KDeclVisitor<R>): R = visitor.visit(this)
 }
 
+class KArray3StoreDecl<D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> internal constructor(
+    ctx: KContext,
+    sort: KArray3Sort<D0, D1, D2, R>
+) : KArrayStoreDeclBase<KArray3Sort<D0, D1, D2, R>, R>(ctx, sort) {
+    override fun apply(args: List<KExpr<*>>): KApp<KArray3Sort<D0, D1, D2, R>, *> {
+        val (array, index0, index1, index2, value) = args
+        return ctx.mkArrayStoreNoSimplify(
+            array = array.uncheckedCast(),
+            index0 = index0.uncheckedCast(),
+            index1 = index1.uncheckedCast(),
+            index2 = index2.uncheckedCast(),
+            value = value.uncheckedCast()
+        )
+    }
+
+    override fun <R> accept(visitor: KDeclVisitor<R>): R = visitor.visit(this)
+}
+
+class KArrayNStoreDecl<R : KSort> internal constructor(
+    ctx: KContext,
+    sort: KArrayNSort<R>
+) : KArrayStoreDeclBase<KArrayNSort<R>, R>(ctx, sort) {
+    override fun apply(args: List<KExpr<*>>): KApp<KArrayNSort<R>, *> =
+        ctx.mkArrayNStoreNoSimplify(
+            array = args.first().uncheckedCast(),
+            indices = args.subList(fromIndex = 1, toIndex = args.size - 1).uncheckedCast(),
+            value = args.last().uncheckedCast()
+        )
+
+    override fun <R> accept(visitor: KDeclVisitor<R>): R = visitor.visit(this)
+}
+
+sealed class KArraySelectDeclBase<A : KArraySortBase<R>, R : KSort>(
+    ctx: KContext,
+    sort: A
+) : KFuncDecl<R>(ctx, "select", sort.range, listOf(sort) + sort.domainSorts)
+
 class KArraySelectDecl<D : KSort, R : KSort> internal constructor(
     ctx: KContext,
     sort: KArraySort<D, R>
-) : KFuncDecl2<R, KArraySort<D, R>, D>(
-    ctx,
-    name = "select",
-    resultSort = sort.range,
-    arg0Sort = sort,
-    arg1Sort = sort.domain
-) {
-    override fun KContext.apply(
-        arg0: KExpr<KArraySort<D, R>>,
-        arg1: KExpr<D>
-    ): KApp<R, *> = mkArraySelectNoSimplify(arg0, arg1)
+) : KArraySelectDeclBase<KArraySort<D, R>, R>(ctx, sort) {
+
+    override fun apply(args: List<KExpr<*>>): KApp<R, *> {
+        val (array, index) = args
+        return ctx.mkArraySelectNoSimplify(
+            array = array.uncheckedCast(),
+            index = index.uncheckedCast<_, KExpr<D>>()
+        )
+    }
 
     override fun <R> accept(visitor: KDeclVisitor<R>): R = visitor.visit(this)
 }
 
-class KArrayConstDecl<D : KSort, R : KSort>(
+class KArray2SelectDecl<D0 : KSort, D1 : KSort, R : KSort> internal constructor(
     ctx: KContext,
-    sort: KArraySort<D, R>
-) : KFuncDecl1<KArraySort<D, R>, R>(ctx, "const", sort, sort.range) {
-    override fun KContext.apply(arg: KExpr<R>): KApp<KArraySort<D, R>, R> = mkArrayConst(sort, arg)
+    sort: KArray2Sort<D0, D1, R>
+) : KArraySelectDeclBase<KArray2Sort<D0, D1, R>, R>(ctx, sort) {
+
+    override fun apply(args: List<KExpr<*>>): KApp<R, *> {
+        val (array, index0, index1) = args
+        return ctx.mkArraySelectNoSimplify(
+            array = array.uncheckedCast(),
+            index0 = index0.uncheckedCast<_, KExpr<D0>>(),
+            index1 = index1.uncheckedCast<_, KExpr<D1>>()
+        )
+    }
+
+    override fun <R> accept(visitor: KDeclVisitor<R>): R = visitor.visit(this)
+}
+
+class KArray3SelectDecl<D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> internal constructor(
+    ctx: KContext,
+    sort: KArray3Sort<D0, D1, D2, R>
+) : KArraySelectDeclBase<KArray3Sort<D0, D1, D2, R>, R>(ctx, sort) {
+
+    override fun apply(args: List<KExpr<*>>): KApp<R, *> {
+        val (array, index0, index1, index2) = args
+        return ctx.mkArraySelectNoSimplify(
+            array = array.uncheckedCast(),
+            index0 = index0.uncheckedCast<_, KExpr<D0>>(),
+            index1 = index1.uncheckedCast<_, KExpr<D1>>(),
+            index2 = index2.uncheckedCast<_, KExpr<D2>>()
+        )
+    }
+
+    override fun <R> accept(visitor: KDeclVisitor<R>): R = visitor.visit(this)
+}
+
+class KArrayNSelectDecl<R : KSort> internal constructor(
+    ctx: KContext,
+    sort: KArrayNSort<R>
+) : KArraySelectDeclBase<KArrayNSort<R>, R>(ctx, sort) {
+
+    override fun apply(args: List<KExpr<*>>): KApp<R, *> =
+        ctx.mkArrayNSelectNoSimplify(
+            array = args.first().uncheckedCast(),
+            indices = args.drop(1)
+        )
+
+    override fun <R> accept(visitor: KDeclVisitor<R>): R = visitor.visit(this)
+}
+
+class KArrayConstDecl<A : KArraySortBase<R>, R : KSort>(
+    ctx: KContext,
+    sort: A
+) : KFuncDecl1<A, R>(ctx, "const", sort, sort.range) {
+    override fun KContext.apply(arg: KExpr<R>): KApp<A, R> = mkArrayConst(sort, arg)
 
     override fun <R> accept(visitor: KDeclVisitor<R>): R = visitor.visit(this)
 }
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/decl/KDeclVisitor.kt b/ksmt-core/src/main/kotlin/org/ksmt/decl/KDeclVisitor.kt
index 99d10651d..f25449dda 100644
--- a/ksmt-core/src/main/kotlin/org/ksmt/decl/KDeclVisitor.kt
+++ b/ksmt-core/src/main/kotlin/org/ksmt/decl/KDeclVisitor.kt
@@ -1,7 +1,11 @@
 package org.ksmt.decl
 
 import org.ksmt.sort.KArithSort
+import org.ksmt.sort.KArray2Sort
+import org.ksmt.sort.KArray3Sort
+import org.ksmt.sort.KArrayNSort
 import org.ksmt.sort.KArraySort
+import org.ksmt.sort.KArraySortBase
 import org.ksmt.sort.KBoolSort
 import org.ksmt.sort.KBv16Sort
 import org.ksmt.sort.KBv1Sort
@@ -31,8 +35,27 @@ interface KDeclVisitor<T> {
     fun <S : KSort> visit(decl: KIteDecl<S>): T = visit(decl as KFuncDecl<S>)
 
     fun <D : KSort, R : KSort> visit(decl: KArraySelectDecl<D, R>): T = visit(decl as KFuncDecl<R>)
+    fun <D0 : KSort, D1 : KSort, R : KSort> visit(decl: KArray2SelectDecl<D0, D1, R>): T = visit(decl as KFuncDecl<R>)
+
+    fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> visit(
+        decl: KArray3SelectDecl<D0, D1, D2, R>
+    ): T = visit(decl as KFuncDecl<R>)
+
+    fun <R : KSort> visit(decl: KArrayNSelectDecl<R>): T = visit(decl as KFuncDecl<R>)
+
     fun <D : KSort, R : KSort> visit(decl: KArrayStoreDecl<D, R>): T = visit(decl as KFuncDecl<KArraySort<D, R>>)
-    fun <D : KSort, R : KSort> visit(decl: KArrayConstDecl<D, R>): T = visit(decl as KFuncDecl<KArraySort<D, R>>)
+
+    fun <D0 : KSort, D1 : KSort, R : KSort> visit(
+        decl: KArray2StoreDecl<D0, D1, R>
+    ): T = visit(decl as KFuncDecl<KArray2Sort<D0, D1, R>>)
+
+    fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> visit(
+        decl: KArray3StoreDecl<D0, D1, D2, R>
+    ): T = visit(decl as KFuncDecl<KArray3Sort<D0, D1, D2, R>>)
+
+    fun <R : KSort> visit(decl: KArrayNStoreDecl<R>): T = visit(decl as KFuncDecl<KArrayNSort<R>>)
+
+    fun <A : KArraySortBase<R>, R : KSort> visit(decl: KArrayConstDecl<A, R>): T = visit(decl as KFuncDecl<A>)
 
     fun <S : KArithSort> visit(decl: KArithSubDecl<S>): T = visit(decl as KFuncDecl<S>)
     fun <S : KArithSort> visit(decl: KArithMulDecl<S>): T = visit(decl as KFuncDecl<S>)
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/expr/Array.kt b/ksmt-core/src/main/kotlin/org/ksmt/expr/Array.kt
index b406e0adc..60af6cf2c 100644
--- a/ksmt-core/src/main/kotlin/org/ksmt/expr/Array.kt
+++ b/ksmt-core/src/main/kotlin/org/ksmt/expr/Array.kt
@@ -9,114 +9,277 @@ import org.ksmt.decl.KFuncDecl
 import org.ksmt.expr.printer.ExpressionPrinter
 import org.ksmt.expr.transformer.KTransformerBase
 import org.ksmt.sort.KArraySort
+import org.ksmt.sort.KArray2Sort
+import org.ksmt.sort.KArray3Sort
+import org.ksmt.sort.KArraySortBase
+import org.ksmt.sort.KArrayNSort
 import org.ksmt.sort.KSort
 import org.ksmt.utils.uncheckedCast
 
+sealed class KArrayStoreBase<A : KArraySortBase<R>, R : KSort>(
+    ctx: KContext,
+    val array: KExpr<A>,
+    val value: KExpr<R>
+) : KApp<A, KSort>(ctx) {
+    override val sort: A = array.sort
+
+    abstract val indices: List<KExpr<KSort>>
+
+    override val args: List<KExpr<KSort>>
+        get() = buildList {
+            add(array)
+            addAll(indices)
+            add(value)
+        }.uncheckedCast()
+}
+
 class KArrayStore<D : KSort, R : KSort> internal constructor(
     ctx: KContext,
-    val array: KExpr<KArraySort<D, R>>,
+    array: KExpr<KArraySort<D, R>>,
     val index: KExpr<D>,
-    val value: KExpr<R>
-) : KApp<KArraySort<D, R>, KSort>(ctx) {
+    value: KExpr<R>
+) : KArrayStoreBase<KArraySort<D, R>, R>(ctx, array, value) {
+    override val indices: List<KExpr<KSort>>
+        get() = listOf(index).uncheckedCast()
 
     override val decl: KDecl<KArraySort<D, R>>
         get() = ctx.mkArrayStoreDecl(array.sort)
 
-    override val args: List<KExpr<KSort>>
-        get() = listOf(array, index, value).uncheckedCast()
-
     override fun accept(transformer: KTransformerBase): KExpr<KArraySort<D, R>> = transformer.transform(this)
 
-    override val sort: KArraySort<D, R> = array.sort
-
     override fun internHashCode(): Int = hash(array, index, value)
     override fun internEquals(other: Any): Boolean = structurallyEqual(other, { array }, { index }, { value })
 }
 
+class KArray2Store<D0 : KSort, D1 : KSort, R : KSort> internal constructor(
+    ctx: KContext,
+    array: KExpr<KArray2Sort<D0, D1, R>>,
+    val index0: KExpr<D0>,
+    val index1: KExpr<D1>,
+    value: KExpr<R>
+) : KArrayStoreBase<KArray2Sort<D0, D1, R>, R>(ctx, array, value) {
+    override val indices: List<KExpr<KSort>>
+        get() = listOf(index0, index1).uncheckedCast()
+
+    override val decl: KDecl<KArray2Sort<D0, D1, R>>
+        get() = ctx.mkArrayStoreDecl(array.sort)
+
+    override fun accept(transformer: KTransformerBase): KExpr<KArray2Sort<D0, D1, R>> =
+        transformer.transform(this)
+
+    override fun internHashCode(): Int =
+        hash(array, index0, index1, value)
+
+    override fun internEquals(other: Any): Boolean =
+        structurallyEqual(other, { array }, { index0 }, { index1 }, { value })
+}
+
+class KArray3Store<D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> internal constructor(
+    ctx: KContext,
+    array: KExpr<KArray3Sort<D0, D1, D2, R>>,
+    val index0: KExpr<D0>,
+    val index1: KExpr<D1>,
+    val index2: KExpr<D2>,
+    value: KExpr<R>
+) : KArrayStoreBase<KArray3Sort<D0, D1, D2, R>, R>(ctx, array, value) {
+    override val indices: List<KExpr<KSort>>
+        get() = listOf(index0, index1, index2).uncheckedCast()
+
+    override val decl: KDecl<KArray3Sort<D0, D1, D2, R>>
+        get() = ctx.mkArrayStoreDecl(array.sort)
+
+    override fun accept(transformer: KTransformerBase): KExpr<KArray3Sort<D0, D1, D2, R>> =
+        transformer.transform(this)
+
+    override fun internHashCode(): Int =
+        hash(array, index0, index1, index2, value)
+
+    override fun internEquals(other: Any): Boolean =
+        structurallyEqual(other, { array }, { index0 }, { index1 }, { index2 }, { value })
+}
+
+class KArrayNStore<R : KSort> internal constructor(
+    ctx: KContext,
+    array: KExpr<KArrayNSort<R>>,
+    override val indices: List<KExpr<KSort>>,
+    value: KExpr<R>
+) : KArrayStoreBase<KArrayNSort<R>, R>(ctx, array, value) {
+    init {
+        require(indices.size == array.sort.domainSorts.size) {
+            "Array domain size mismatch: expected ${array.sort.domainSorts.size}, provided: ${indices.size}"
+        }
+    }
+
+    override val decl: KDecl<KArrayNSort<R>>
+        get() = ctx.mkArrayNStoreDecl(array.sort)
+
+    override fun accept(transformer: KTransformerBase): KExpr<KArrayNSort<R>> =
+        transformer.transform(this)
+
+    override fun internHashCode(): Int = hash(array, indices, value)
+    override fun internEquals(other: Any): Boolean = structurallyEqual(other, { array }, { indices }, { value })
+}
+
+sealed class KArraySelectBase<A : KArraySortBase<R>, R : KSort>(
+    ctx: KContext,
+    val array: KExpr<A>
+) : KApp<R, KSort>(ctx) {
+    override val sort: R = array.sort.range
+
+    abstract val indices: List<KExpr<KSort>>
+
+    override val args: List<KExpr<KSort>>
+        get() = buildList {
+            add(array)
+            addAll(indices)
+        }.uncheckedCast()
+}
+
 class KArraySelect<D : KSort, R : KSort> internal constructor(
     ctx: KContext,
-    val array: KExpr<KArraySort<D, R>>,
+    array: KExpr<KArraySort<D, R>>,
     val index: KExpr<D>
-) : KApp<R, KSort>(ctx) {
+) : KArraySelectBase<KArraySort<D, R>, R>(ctx, array) {
+    override val indices: List<KExpr<KSort>>
+        get() = listOf(index).uncheckedCast()
 
     override val decl: KDecl<R>
         get() = ctx.mkArraySelectDecl(array.sort)
 
-    override val args: List<KExpr<KSort>>
-        get() = listOf(array, index).uncheckedCast()
-
     override fun accept(transformer: KTransformerBase): KExpr<R> = transformer.transform(this)
 
-    override val sort: R = array.sort.range
-
     override fun internHashCode(): Int = hash(array, index)
     override fun internEquals(other: Any): Boolean = structurallyEqual(other, { array }, { index })
 }
 
-class KArrayConst<D : KSort, R : KSort> internal constructor(
+class KArray2Select<D0 : KSort, D1 : KSort, R : KSort> internal constructor(
     ctx: KContext,
-    override val sort: KArraySort<D, R>,
+    array: KExpr<KArray2Sort<D0, D1, R>>,
+    val index0: KExpr<D0>,
+    val index1: KExpr<D1>
+) : KArraySelectBase<KArray2Sort<D0, D1, R>, R>(ctx, array) {
+    override val indices: List<KExpr<KSort>>
+        get() = listOf(index0, index1).uncheckedCast()
+
+    override val decl: KDecl<R>
+        get() = ctx.mkArraySelectDecl(array.sort)
+
+    override fun accept(transformer: KTransformerBase): KExpr<R> = transformer.transform(this)
+
+    override fun internHashCode(): Int = hash(array, index0, index1)
+    override fun internEquals(other: Any): Boolean =
+        structurallyEqual(other, { array }, { index0 }, { index1 })
+}
+
+class KArray3Select<D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> internal constructor(
+    ctx: KContext,
+    array: KExpr<KArray3Sort<D0, D1, D2, R>>,
+    val index0: KExpr<D0>,
+    val index1: KExpr<D1>,
+    val index2: KExpr<D2>
+) : KArraySelectBase<KArray3Sort<D0, D1, D2, R>, R>(ctx, array) {
+    override val indices: List<KExpr<KSort>>
+        get() = listOf(index0, index1, index2).uncheckedCast()
+
+    override val decl: KDecl<R>
+        get() = ctx.mkArraySelectDecl(array.sort)
+
+    override fun accept(transformer: KTransformerBase): KExpr<R> = transformer.transform(this)
+
+    override fun internHashCode(): Int = hash(array, index0, index1, index2)
+    override fun internEquals(other: Any): Boolean =
+        structurallyEqual(other, { array }, { index0 }, { index1 }, { index2 })
+}
+
+class KArrayNSelect<R : KSort> internal constructor(
+    ctx: KContext,
+    array: KExpr<KArrayNSort<R>>,
+    override val indices: List<KExpr<KSort>>
+) : KArraySelectBase<KArrayNSort<R>, R>(ctx, array) {
+    init {
+        require(indices.size == array.sort.domainSorts.size) {
+            "Array domain size mismatch: expected ${array.sort.domainSorts.size}, provided: ${indices.size}"
+        }
+    }
+
+    override val decl: KDecl<R>
+        get() = ctx.mkArrayNSelectDecl(array.sort)
+
+    override fun accept(transformer: KTransformerBase): KExpr<R> = transformer.transform(this)
+
+    override fun internHashCode(): Int = hash(array, indices)
+    override fun internEquals(other: Any): Boolean = structurallyEqual(other, { array }, { indices })
+}
+
+class KArrayConst<A : KArraySortBase<R>, R : KSort> internal constructor(
+    ctx: KContext,
+    override val sort: A,
     val value: KExpr<R>
-) : KApp<KArraySort<D, R>, R>(ctx) {
+) : KApp<A, R>(ctx) {
 
-    override val decl: KArrayConstDecl<D, R>
+    override val decl: KArrayConstDecl<A, R>
         get() = ctx.mkArrayConstDecl(sort)
 
     override val args: List<KExpr<R>>
         get() = listOf(value)
 
-    override fun accept(transformer: KTransformerBase): KExpr<KArraySort<D, R>> = transformer.transform(this)
+    override fun accept(transformer: KTransformerBase): KExpr<A> =
+        transformer.transform(this)
 
     override fun internHashCode(): Int = hash(sort, value)
     override fun internEquals(other: Any): Boolean = structurallyEqual(other, { sort }, { value })
 }
 
-class KFunctionAsArray<D : KSort, R : KSort> internal constructor(
+class KFunctionAsArray<A : KArraySortBase<R>, R : KSort> internal constructor(
     ctx: KContext,
+    override val sort: A,
     val function: KFuncDecl<R>
-) : KExpr<KArraySort<D, R>>(ctx) {
-    val domainSort: D
+) : KExpr<A>(ctx) {
 
     init {
-        check(function.argSorts.size == 1) {
-            "Function with single argument required"
+        check(function.argSorts == sort.domainSorts) {
+            "Function arguments sort mismatch"
         }
-        @Suppress("UNCHECKED_CAST")
-        domainSort = function.argSorts.single() as D
     }
 
-    override val sort: KArraySort<D, R> = ctx.mkArraySort(domainSort, function.sort)
-
     override fun print(printer: ExpressionPrinter): Unit = with(printer) {
         append("(asArray ")
         append(function.name)
         append(")")
     }
 
-    override fun accept(transformer: KTransformerBase): KExpr<KArraySort<D, R>> = transformer.transform(this)
+    override fun accept(transformer: KTransformerBase): KExpr<A> =
+        transformer.transform(this)
 
     override fun internHashCode(): Int = hash(function)
     override fun internEquals(other: Any): Boolean = structurallyEqual(other) { function }
 }
 
-/** Array lambda binding.
+/**
+ * Array lambda binding.
  *
  * [Defined as in the Z3 solver](https://microsoft.github.io/z3guide/docs/logic/Lambdas)
  * */
-class KArrayLambda<D : KSort, R : KSort> internal constructor(
+sealed class KArrayLambdaBase<A : KArraySortBase<R>, R : KSort>(
     ctx: KContext,
-    val indexVarDecl: KDecl<D>,
+    override val sort: A,
     val body: KExpr<R>
-) : KExpr<KArraySort<D, R>>(ctx) {
+) : KExpr<A>(ctx) {
+    abstract val indexVarDeclarations: List<KDecl<*>>
 
     override fun print(printer: ExpressionPrinter) {
         val str = buildString {
-            append("(lambda ((")
-            append(indexVarDecl.name)
-            append(' ')
+            append("(lambda (")
+
+            indexVarDeclarations.forEach {
+                append('(')
+                append(it.name)
+                append(' ')
+                it.sort.print(this)
+                append(')')
+            }
 
-            indexVarDecl.sort.print(this)
-            append(")) ")
+            append(") ")
 
             body.print(this)
 
@@ -124,11 +287,80 @@ class KArrayLambda<D : KSort, R : KSort> internal constructor(
         }
         printer.append(str)
     }
+}
 
-    override fun accept(transformer: KTransformerBase): KExpr<KArraySort<D, R>> = transformer.transform(this)
+class KArrayLambda<D : KSort, R : KSort> internal constructor(
+    ctx: KContext,
+    val indexVarDecl: KDecl<D>,
+    body: KExpr<R>
+) : KArrayLambdaBase<KArraySort<D, R>, R>(
+    ctx,
+    ctx.mkArraySort(indexVarDecl.sort, body.sort),
+    body
+) {
+    override val indexVarDeclarations: List<KDecl<*>>
+        get() = listOf(indexVarDecl)
 
-    override val sort: KArraySort<D, R> = ctx.mkArraySort(indexVarDecl.sort, body.sort)
+    override fun accept(transformer: KTransformerBase): KExpr<KArraySort<D, R>> = transformer.transform(this)
 
     override fun internHashCode(): Int = hash(indexVarDecl, body)
     override fun internEquals(other: Any): Boolean = structurallyEqual(other, { indexVarDecl }, { body })
 }
+
+class KArray2Lambda<D0 : KSort, D1 : KSort, R : KSort> internal constructor(
+    ctx: KContext,
+    val indexVar0Decl: KDecl<D0>,
+    val indexVar1Decl: KDecl<D1>,
+    body: KExpr<R>
+) : KArrayLambdaBase<KArray2Sort<D0, D1, R>, R>(
+    ctx,
+    ctx.mkArraySort(indexVar0Decl.sort, indexVar1Decl.sort, body.sort),
+    body
+) {
+    override val indexVarDeclarations: List<KDecl<*>>
+        get() = listOf(indexVar0Decl, indexVar1Decl)
+
+    override fun accept(transformer: KTransformerBase): KExpr<KArray2Sort<D0, D1, R>> =
+        transformer.transform(this)
+
+    override fun internHashCode(): Int = hash(indexVar0Decl, indexVar1Decl, body)
+    override fun internEquals(other: Any): Boolean =
+        structurallyEqual(other, { indexVar0Decl }, { indexVar1Decl }, { body })
+}
+
+class KArray3Lambda<D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> internal constructor(
+    ctx: KContext,
+    val indexVar0Decl: KDecl<D0>,
+    val indexVar1Decl: KDecl<D1>,
+    val indexVar2Decl: KDecl<D2>,
+    body: KExpr<R>
+) : KArrayLambdaBase<KArray3Sort<D0, D1, D2, R>, R>(
+    ctx,
+    ctx.mkArraySort(indexVar0Decl.sort, indexVar1Decl.sort, indexVar2Decl.sort, body.sort),
+    body
+) {
+    override val indexVarDeclarations: List<KDecl<*>>
+        get() = listOf(indexVar0Decl, indexVar1Decl, indexVar2Decl)
+
+    override fun accept(transformer: KTransformerBase): KExpr<KArray3Sort<D0, D1, D2, R>> =
+        transformer.transform(this)
+
+    override fun internHashCode(): Int = hash(indexVar0Decl, indexVar1Decl, indexVar2Decl, body)
+    override fun internEquals(other: Any): Boolean =
+        structurallyEqual(other, { indexVar0Decl }, { indexVar1Decl }, { indexVar2Decl }, { body })
+}
+
+class KArrayNLambda<R : KSort> internal constructor(
+    ctx: KContext,
+    override val indexVarDeclarations: List<KDecl<*>>,
+    body: KExpr<R>
+) : KArrayLambdaBase<KArrayNSort<R>, R>(
+    ctx,
+    ctx.mkArrayNSort(indexVarDeclarations.map { it.sort }, body.sort),
+    body
+) {
+    override fun accept(transformer: KTransformerBase): KExpr<KArrayNSort<R>> = transformer.transform(this)
+
+    override fun internHashCode(): Int = hash(indexVarDeclarations, body)
+    override fun internEquals(other: Any): Boolean = structurallyEqual(other, { indexVarDeclarations }, { body })
+}
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/KExprSubstitutor.kt b/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/KExprSubstitutor.kt
index 5232277be..05bf357dd 100644
--- a/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/KExprSubstitutor.kt
+++ b/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/KExprSubstitutor.kt
@@ -4,14 +4,21 @@ import org.ksmt.KContext
 import org.ksmt.decl.KDecl
 import org.ksmt.decl.KFuncDecl
 import org.ksmt.expr.KApp
+import org.ksmt.expr.KArray2Lambda
+import org.ksmt.expr.KArray3Lambda
 import org.ksmt.expr.KArrayLambda
+import org.ksmt.expr.KArrayNLambda
 import org.ksmt.expr.KExistentialQuantifier
 import org.ksmt.expr.KExpr
 import org.ksmt.expr.KFunctionAsArray
 import org.ksmt.expr.KUniversalQuantifier
 import org.ksmt.expr.rewrite.KExprUninterpretedDeclCollector.Companion.collectUninterpretedDeclarations
 import org.ksmt.expr.transformer.KNonRecursiveTransformer
+import org.ksmt.sort.KArray2Sort
+import org.ksmt.sort.KArray3Sort
+import org.ksmt.sort.KArrayNSort
 import org.ksmt.sort.KArraySort
+import org.ksmt.sort.KArraySortBase
 import org.ksmt.sort.KBoolSort
 import org.ksmt.sort.KSort
 import org.ksmt.utils.uncheckedCast
@@ -49,27 +56,60 @@ open class KExprSubstitutor(ctx: KContext) : KNonRecursiveTransformer(ctx) {
         return transformExpr(transformedApp)
     }
 
-    override fun <D : KSort, R : KSort> transform(expr: KFunctionAsArray<D, R>): KExpr<KArraySort<D, R>> {
+    override fun <A : KArraySortBase<R>, R : KSort> transform(expr: KFunctionAsArray<A, R>): KExpr<A> {
         val declSubstitution = declDeclSubstitution[expr.function]?.uncheckedCast() ?: expr.function
-        return transformExpr(ctx.mkFunctionAsArray(declSubstitution))
+        return transformExpr(ctx.mkFunctionAsArray(expr.sort, declSubstitution))
     }
 
-    override fun <D : KSort, R : KSort> transform(expr: KArrayLambda<D, R>): KExpr<KArraySort<D, R>> =
-        transformQuantifiedExpression(expr, setOf(expr.indexVarDecl), expr.body) { body, bounds ->
-            ctx.mkArrayLambda(bounds.single().uncheckedCast(), body)
-        }
+    override fun <D : KSort, R : KSort> transform(
+        expr: KArrayLambda<D, R>
+    ): KExpr<KArraySort<D, R>> = transformQuantifiedExpression(
+        expr, listOf(expr.indexVarDecl), expr.body
+    ) { body, bounds ->
+        val boundVar: KDecl<D> = bounds.single().uncheckedCast()
+        ctx.mkArrayLambda(boundVar, body)
+    }
+
+    override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+        expr: KArray2Lambda<D0, D1, R>
+    ): KExpr<KArray2Sort<D0, D1, R>> = transformQuantifiedExpression(
+        expr, listOf(expr.indexVar0Decl, expr.indexVar1Decl), expr.body
+    ) { body, (b0, b1) ->
+        val bound0: KDecl<D0> = b0.uncheckedCast()
+        val bound1: KDecl<D1> = b1.uncheckedCast()
+        ctx.mkArrayLambda(bound0, bound1, body)
+    }
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Lambda<D0, D1, D2, R>
+    ): KExpr<KArray3Sort<D0, D1, D2, R>>  = transformQuantifiedExpression(
+        expr, listOf(expr.indexVar0Decl, expr.indexVar1Decl, expr.indexVar2Decl), expr.body
+    ) { body, (b0, b1, b2) ->
+        val bound0: KDecl<D0> = b0.uncheckedCast()
+        val bound1: KDecl<D1> = b1.uncheckedCast()
+        val bound2: KDecl<D2> = b2.uncheckedCast()
+        ctx.mkArrayLambda(bound0, bound1, bound2, body)
+    }
+
+    override fun <R : KSort> transform(
+        expr: KArrayNLambda<R>
+    ): KExpr<KArrayNSort<R>> = transformQuantifiedExpression(
+        expr, expr.indexVarDeclarations, expr.body
+    ) { body, bounds ->
+        ctx.mkArrayNLambda(bounds, body)
+    }
 
     override fun transform(expr: KExistentialQuantifier): KExpr<KBoolSort> =
-        transformQuantifiedExpression(expr, expr.bounds.toSet(), expr.body) { body, bounds ->
-            ctx.mkExistentialQuantifier(body, bounds.toList())
+        transformQuantifiedExpression(expr, expr.bounds, expr.body) { body, bounds ->
+            ctx.mkExistentialQuantifier(body, bounds)
         }
 
     override fun transform(expr: KUniversalQuantifier): KExpr<KBoolSort> =
-        transformQuantifiedExpression(expr, expr.bounds.toSet(), expr.body) { body, bounds ->
-            ctx.mkUniversalQuantifier(body, bounds.toList())
+        transformQuantifiedExpression(expr, expr.bounds, expr.body) { body, bounds ->
+            ctx.mkUniversalQuantifier(body, bounds)
         }
 
-    private val unprocessedQuantifiers = hashMapOf<KExpr<*>, Pair<Set<KDecl<*>>, KExpr<*>>>()
+    private val unprocessedQuantifiers = hashMapOf<KExpr<*>, Pair<List<KDecl<*>>, KExpr<*>>>()
 
     /**
      * Resolve quantifier bound vars shadowing.
@@ -83,9 +123,9 @@ open class KExprSubstitutor(ctx: KContext) : KNonRecursiveTransformer(ctx) {
      * */
     private inline fun <B : KSort, T: KSort> transformQuantifiedExpression(
         quantifiedExpr: KExpr<T>,
-        quantifiedVars: Set<KDecl<*>>,
+        quantifiedVars: List<KDecl<*>>,
         body: KExpr<B>,
-        crossinline quantifierBuilder: (KExpr<B>, Set<KDecl<*>>) -> KExpr<T>
+        crossinline quantifierBuilder: (KExpr<B>, List<KDecl<*>>) -> KExpr<T>
     ): KExpr<T> {
         val (unshadowedBounds, unshadowedBody) = unprocessedQuantifiers.getOrPut(quantifiedExpr) {
             resolveQuantifierShadowedVars(quantifiedVars, body)
@@ -98,9 +138,9 @@ open class KExprSubstitutor(ctx: KContext) : KNonRecursiveTransformer(ctx) {
     }
 
     private fun <B : KSort> resolveQuantifierShadowedVars(
-        quantifiedVars: Set<KDecl<*>>,
+        quantifiedVars: List<KDecl<*>>,
         body: KExpr<B>,
-    ): Pair<Set<KDecl<*>>, KExpr<*>> {
+    ): Pair<List<KDecl<*>>, KExpr<*>> {
         val usedDeclarationsList = exprExprSubstitution.flatMap {
             collectUninterpretedDeclarations(it.key) + collectUninterpretedDeclarations(it.value)
         } + declDeclSubstitution.keys + declDeclSubstitution.values
@@ -113,7 +153,7 @@ open class KExprSubstitutor(ctx: KContext) : KNonRecursiveTransformer(ctx) {
         }
 
         val shadowedBoundsReplacement = shadowedDeclarations.associateWith { it.freshStub() }
-        val unshadowedQuantifiedVars = quantifiedVars.mapTo(hashSetOf()) { shadowedBoundsReplacement[it] ?: it }
+        val unshadowedQuantifiedVars = quantifiedVars.map { shadowedBoundsReplacement[it] ?: it }
         val shadowedBoundRemover = KExprSubstitutor(ctx).also { remover ->
             shadowedBoundsReplacement.forEach {
                 @Suppress("UNCHECKED_CAST")
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/KExprUninterpretedDeclCollector.kt b/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/KExprUninterpretedDeclCollector.kt
index c93580b83..e6193a14f 100644
--- a/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/KExprUninterpretedDeclCollector.kt
+++ b/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/KExprUninterpretedDeclCollector.kt
@@ -2,7 +2,10 @@ package org.ksmt.expr.rewrite
 
 import org.ksmt.KContext
 import org.ksmt.decl.KDecl
+import org.ksmt.expr.KArray2Lambda
+import org.ksmt.expr.KArray3Lambda
 import org.ksmt.expr.KArrayLambda
+import org.ksmt.expr.KArrayNLambda
 import org.ksmt.expr.KConst
 import org.ksmt.expr.KExistentialQuantifier
 import org.ksmt.expr.KExpr
@@ -10,7 +13,11 @@ import org.ksmt.expr.KFunctionApp
 import org.ksmt.expr.KFunctionAsArray
 import org.ksmt.expr.KUniversalQuantifier
 import org.ksmt.expr.transformer.KNonRecursiveTransformer
+import org.ksmt.sort.KArray2Sort
+import org.ksmt.sort.KArray3Sort
+import org.ksmt.sort.KArrayNSort
 import org.ksmt.sort.KArraySort
+import org.ksmt.sort.KArraySortBase
 import org.ksmt.sort.KBoolSort
 import org.ksmt.sort.KSort
 
@@ -30,7 +37,7 @@ open class KExprUninterpretedDeclCollector(ctx: KContext) : KNonRecursiveTransfo
         return super.transform(expr)
     }
 
-    override fun <D : KSort, R : KSort> transform(expr: KFunctionAsArray<D, R>): KExpr<KArraySort<D, R>> {
+    override fun <A : KArraySortBase<R>, R : KSort> transform(expr: KFunctionAsArray<A, R>): KExpr<A> {
         declarations += expr.function
         return super.transform(expr)
     }
@@ -40,6 +47,25 @@ open class KExprUninterpretedDeclCollector(ctx: KContext) : KNonRecursiveTransfo
         return expr
     }
 
+    override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+        expr: KArray2Lambda<D0, D1, R>
+    ): KExpr<KArray2Sort<D0, D1, R>> {
+        transformQuantifier(setOf(expr.indexVar0Decl, expr.indexVar1Decl), expr.body)
+        return expr
+    }
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Lambda<D0, D1, D2, R>
+    ): KExpr<KArray3Sort<D0, D1, D2, R>> {
+        transformQuantifier(setOf(expr.indexVar0Decl, expr.indexVar1Decl, expr.indexVar2Decl), expr.body)
+        return expr
+    }
+
+    override fun <R : KSort> transform(expr: KArrayNLambda<R>): KExpr<KArrayNSort<R>> {
+        transformQuantifier(expr.indexVarDeclarations.toSet(), expr.body)
+        return expr
+    }
+
     override fun transform(expr: KExistentialQuantifier): KExpr<KBoolSort> {
         transformQuantifier(expr.bounds.toSet(), expr.body)
         return expr
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/ArraySimplification.kt b/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/ArraySimplification.kt
index 96afb2ac7..fef9b7727 100644
--- a/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/ArraySimplification.kt
+++ b/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/ArraySimplification.kt
@@ -1,48 +1,128 @@
 package org.ksmt.expr.rewrite.simplify
 
 import org.ksmt.KContext
+import org.ksmt.expr.KArray2Lambda
+import org.ksmt.expr.KArray2Select
+import org.ksmt.expr.KArray2Store
+import org.ksmt.expr.KArray3Lambda
+import org.ksmt.expr.KArray3Select
+import org.ksmt.expr.KArray3Store
 import org.ksmt.expr.KArrayConst
 import org.ksmt.expr.KArrayLambda
+import org.ksmt.expr.KArrayLambdaBase
+import org.ksmt.expr.KArrayNLambda
+import org.ksmt.expr.KArrayNSelect
+import org.ksmt.expr.KArrayNStore
 import org.ksmt.expr.KArraySelect
+import org.ksmt.expr.KArraySelectBase
 import org.ksmt.expr.KArrayStore
+import org.ksmt.expr.KArrayStoreBase
 import org.ksmt.expr.KExpr
 import org.ksmt.expr.KInterpretedValue
 import org.ksmt.expr.rewrite.KExprSubstitutor
+import org.ksmt.sort.KArray2Sort
+import org.ksmt.sort.KArray3Sort
+import org.ksmt.sort.KArrayNSort
 import org.ksmt.sort.KArraySort
+import org.ksmt.sort.KArraySortBase
 import org.ksmt.sort.KSort
+import org.ksmt.utils.uncheckedCast
 
-fun <D : KSort, R : KSort> KContext.simplifyArrayStore(
-    array: KExpr<KArraySort<D, R>>,
-    index: KExpr<D>,
-    value: KExpr<R>
-) : KExpr<KArraySort<D, R>> {
+private inline fun <
+    reified A : KArraySortBase<R>, R : KSort,
+    reified S : KArraySelectBase<out A, R>
+> simplifyArrayStore(
+    array: KExpr<A>,
+    value: KExpr<R>,
+    selectIndicesMatch: (S) -> Boolean,
+    default: () -> KExpr<A>
+): KExpr<A> {
     // (store (const v) i v) ==> (const v)
-    if (array is KArrayConst<D, R> && array.value == value) {
+    if (array is KArrayConst<A, *> && array.value == value) {
         return array
     }
 
     // (store a i (select a i)) ==> a
-    if (value is KArraySelect<*, *> && array == value.array && index == value.index) {
+    if (value is S && array == value.array && selectIndicesMatch(value)) {
         return array
     }
 
-    return mkArrayStoreNoSimplify(array, index, value)
+    return default()
 }
 
-fun <D : KSort, R : KSort> KContext.simplifyArraySelect(
+fun <D : KSort, R : KSort> KContext.simplifyArrayStore(
     array: KExpr<KArraySort<D, R>>,
-    index: KExpr<D>
+    index: KExpr<D>,
+    value: KExpr<R>
+): KExpr<KArraySort<D, R>> = simplifyArrayStore(
+    array,
+    value,
+    selectIndicesMatch = { select: KArraySelect<D, R> -> index == select.index },
+    default = { mkArrayStoreNoSimplify(array, index, value) }
+)
+
+fun <D0 : KSort, D1 : KSort, R : KSort> KContext.simplifyArrayStore(
+    array: KExpr<KArray2Sort<D0, D1, R>>,
+    index0: KExpr<D0>,
+    index1: KExpr<D1>,
+    value: KExpr<R>
+): KExpr<KArray2Sort<D0, D1, R>> = simplifyArrayStore(
+    array,
+    value,
+    selectIndicesMatch = { select: KArray2Select<D0, D1, R> -> index0 == select.index0 && index1 == select.index1 },
+    default = { mkArrayStoreNoSimplify(array, index0, index1, value) }
+)
+
+fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> KContext.simplifyArrayStore(
+    array: KExpr<KArray3Sort<D0, D1, D2, R>>,
+    index0: KExpr<D0>,
+    index1: KExpr<D1>,
+    index2: KExpr<D2>,
+    value: KExpr<R>
+): KExpr<KArray3Sort<D0, D1, D2, R>> = simplifyArrayStore(
+    array,
+    value,
+    selectIndicesMatch = { select: KArray3Select<D0, D1, D2, R> ->
+        index0 == select.index0 && index1 == select.index1 && index2 == select.index2
+    },
+    default = { mkArrayStoreNoSimplify(array, index0, index1, index2, value) }
+)
+
+fun <R : KSort> KContext.simplifyArrayNStore(
+    array: KExpr<KArrayNSort<R>>,
+    indices: List<KExpr<*>>,
+    value: KExpr<R>
+): KExpr<KArrayNSort<R>> = simplifyArrayStore(
+    array,
+    value,
+    selectIndicesMatch = { select: KArrayNSelect<R> -> indices == select.indices },
+    default = { mkArrayNStoreNoSimplify(array, indices, value) }
+)
+
+@Suppress("LongParameterList")
+private inline fun <
+    reified A : KArraySortBase<R>,
+    R : KSort,
+    reified S : KArrayStoreBase<A, R>,
+    reified L : KArrayLambdaBase<A, R>
+> KContext.simplifyArraySelect(
+    array: KExpr<A>,
+    indicesAreValues: () -> Boolean,
+    storeIndicesMatch: (S) -> Boolean,
+    storeIndicesAreValues: (S) -> Boolean,
+    mkLambdaSubstitution: KExprSubstitutor.(L) -> Unit,
+    default: (KExpr<A>) -> KExpr<R>
 ): KExpr<R> {
     var currentArray = array
 
-    while (currentArray is KArrayStore<D, R>) {
+    while (currentArray is S) {
         // (select (store i v) i) ==> v
-        if (currentArray.index == index) {
+        if (storeIndicesMatch(currentArray)) {
             return currentArray.value
         }
 
         // (select (store a i v) j), i != j ==> (select a j)
-        if (index is KInterpretedValue<D> && currentArray.index is KInterpretedValue<D>) {
+        if (indicesAreValues() && storeIndicesAreValues(currentArray)) {
             currentArray = currentArray.array
         } else {
             // possibly equal index, we can't expand stores
@@ -52,18 +132,91 @@ fun <D : KSort, R : KSort> KContext.simplifyArraySelect(
 
     when (currentArray) {
         // (select (const v) i) ==> v
-        is KArrayConst<D, R> -> {
-            return currentArray.value
+        is KArrayConst<A, *> -> {
+            return currentArray.value.uncheckedCast()
         }
         // (select (lambda x body) i) ==> body[i/x]
-        is KArrayLambda<D, R> -> {
+        is L -> {
             val resolvedBody = KExprSubstitutor(this).apply {
-                val indexVarExpr = mkConstApp(currentArray.indexVarDecl)
-                substitute(indexVarExpr, index)
+                mkLambdaSubstitution(currentArray)
             }.apply(currentArray.body)
             return resolvedBody
         }
     }
 
-    return mkArraySelectNoSimplify(currentArray, index)
+    return default(currentArray)
 }
+
+fun <D : KSort, R : KSort> KContext.simplifyArraySelect(
+    array: KExpr<KArraySort<D, R>>,
+    index: KExpr<D>
+): KExpr<R> = simplifyArraySelect(
+    array = array,
+    indicesAreValues = { index is KInterpretedValue<D> },
+    storeIndicesMatch = { store: KArrayStore<D, R> -> index == store.index },
+    storeIndicesAreValues = { store: KArrayStore<D, R> -> store.index is KInterpretedValue<D> },
+    mkLambdaSubstitution = { lambda: KArrayLambda<D, R> ->
+        substitute(mkConstApp(lambda.indexVarDecl), index)
+    },
+    default = { mkArraySelectNoSimplify(it, index) }
+)
+
+fun <D0 : KSort, D1 : KSort, R : KSort> KContext.simplifyArraySelect(
+    array: KExpr<KArray2Sort<D0, D1, R>>,
+    index0: KExpr<D0>,
+    index1: KExpr<D1>
+): KExpr<R> = simplifyArraySelect(
+    array = array,
+    indicesAreValues = { index0 is KInterpretedValue<D0> && index1 is KInterpretedValue<D1> },
+    storeIndicesMatch = { store: KArray2Store<D0, D1, R> ->
+        index0 == store.index0 && index1 == store.index1
+    },
+    storeIndicesAreValues = { store: KArray2Store<D0, D1, R> ->
+        store.index0 is KInterpretedValue<D0> && store.index1 is KInterpretedValue<D1>
+    },
+    mkLambdaSubstitution = { lambda: KArray2Lambda<D0, D1, R> ->
+        substitute(mkConstApp(lambda.indexVar0Decl), index0)
+        substitute(mkConstApp(lambda.indexVar1Decl), index1)
+    },
+    default = { mkArraySelectNoSimplify(it, index0, index1) }
+)
+
+fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> KContext.simplifyArraySelect(
+    array: KExpr<KArray3Sort<D0, D1, D2, R>>,
+    index0: KExpr<D0>,
+    index1: KExpr<D1>,
+    index2: KExpr<D2>
+): KExpr<R> = simplifyArraySelect(
+    array = array,
+    indicesAreValues = {
+        index0 is KInterpretedValue<D0> && index1 is KInterpretedValue<D1> && index2 is KInterpretedValue<D2>
+    },
+    storeIndicesMatch = { store: KArray3Store<D0, D1, D2, R> ->
+        index0 == store.index0 && index1 == store.index1 && index2 == store.index2
+    },
+    storeIndicesAreValues = { s: KArray3Store<D0, D1, D2, R> ->
+        s.index0 is KInterpretedValue<D0> && s.index1 is KInterpretedValue<D1> && s.index2 is KInterpretedValue<D2>
+    },
+    mkLambdaSubstitution = { lambda: KArray3Lambda<D0, D1, D2, R> ->
+        substitute(mkConstApp(lambda.indexVar0Decl), index0)
+        substitute(mkConstApp(lambda.indexVar1Decl), index1)
+        substitute(mkConstApp(lambda.indexVar2Decl), index2)
+    },
+    default = { mkArraySelectNoSimplify(it, index0, index1, index2) }
+)
+
+fun <R : KSort> KContext.simplifyArrayNSelect(
+    array: KExpr<KArrayNSort<R>>,
+    indices: List<KExpr<*>>
+): KExpr<R> = simplifyArraySelect(
+    array = array,
+    indicesAreValues = { indices.all { it is KInterpretedValue<*> } },
+    storeIndicesMatch = { store: KArrayNStore<R> -> indices == store.indices },
+    storeIndicesAreValues = { store: KArrayNStore<R> -> store.indices.all { it is KInterpretedValue<*> } },
+    mkLambdaSubstitution = { lambda: KArrayNLambda<R> ->
+        lambda.indexVarDeclarations.zip(indices) { varDecl, index ->
+            substitute(mkConstApp(varDecl).uncheckedCast<_, KExpr<KSort>>(), index.uncheckedCast())
+        }
+    },
+    default = { mkArrayNSelectNoSimplify(it, indices) }
+)
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/KArrayExprSimplifier.kt b/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/KArrayExprSimplifier.kt
index 88954806f..274762446 100644
--- a/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/KArrayExprSimplifier.kt
+++ b/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/KArrayExprSimplifier.kt
@@ -3,31 +3,50 @@ package org.ksmt.expr.rewrite.simplify
 import org.ksmt.KContext
 import org.ksmt.decl.KDecl
 import org.ksmt.expr.KAndExpr
-import org.ksmt.expr.KApp
+import org.ksmt.expr.KArray2Lambda
+import org.ksmt.expr.KArray2Select
+import org.ksmt.expr.KArray2Store
+import org.ksmt.expr.KArray3Lambda
+import org.ksmt.expr.KArray3Select
+import org.ksmt.expr.KArray3Store
 import org.ksmt.expr.KArrayConst
 import org.ksmt.expr.KArrayLambda
+import org.ksmt.expr.KArrayLambdaBase
+import org.ksmt.expr.KArrayNLambda
+import org.ksmt.expr.KArrayNSelect
+import org.ksmt.expr.KArrayNStore
 import org.ksmt.expr.KArraySelect
+import org.ksmt.expr.KArraySelectBase
 import org.ksmt.expr.KArrayStore
+import org.ksmt.expr.KArrayStoreBase
 import org.ksmt.expr.KEqExpr
 import org.ksmt.expr.KExpr
+import org.ksmt.expr.KFunctionApp
+import org.ksmt.expr.KFunctionAsArray
 import org.ksmt.expr.KInterpretedValue
+import org.ksmt.expr.printer.ExpressionPrinter
 import org.ksmt.expr.rewrite.KExprSubstitutor
 import org.ksmt.expr.transformer.KTransformerBase
+import org.ksmt.sort.KArray2Sort
+import org.ksmt.sort.KArray3Sort
+import org.ksmt.sort.KArrayNSort
 import org.ksmt.sort.KArraySort
+import org.ksmt.sort.KArraySortBase
 import org.ksmt.sort.KBoolSort
 import org.ksmt.sort.KSort
 import org.ksmt.utils.uncheckedCast
 
+@Suppress("LargeClass")
 interface KArrayExprSimplifier : KExprSimplifierBase {
 
-    fun <D : KSort, R : KSort> simplifyEqArray(
-        lhs: KExpr<KArraySort<D, R>>,
-        rhs: KExpr<KArraySort<D, R>>
+    fun <A : KArraySortBase<R>, R : KSort> simplifyEqArray(
+        lhs: KExpr<A>,
+        rhs: KExpr<A>
     ): KExpr<KBoolSort> = with(ctx) {
         if (lhs == rhs) return trueExpr
 
-        val leftArray = flatStores(lhs)
-        val rightArray = flatStores(rhs)
+        val leftArray = flatStoresGeneric(lhs.sort, lhs)
+        val rightArray = flatStoresGeneric(rhs.sort, rhs)
         val lBase = leftArray.base
         val rBase = rightArray.base
 
@@ -39,7 +58,7 @@ interface KArrayExprSimplifier : KExprSimplifierBase {
          *   (= a b)
          * )
          */
-        if (lBase == rBase || lBase is KArrayConst<D, R> && rBase is KArrayConst<D, R>) {
+        if (lBase == rBase || lBase is KArrayConst<*, *> && rBase is KArrayConst<*, *>) {
             val simplifiedExpr = simplifyArrayStoreEq(lhs, leftArray, rhs, rightArray)
             return rewrite(simplifiedExpr)
         }
@@ -55,16 +74,20 @@ interface KArrayExprSimplifier : KExprSimplifierBase {
      *   (= a b)
      * )
      */
-    private fun <D : KSort, R : KSort> simplifyArrayStoreEq(
-        lhs: KExpr<KArraySort<D, R>>,
-        leftArray: SimplifierFlatArrayStoreExpr<D, R>,
-        rhs: KExpr<KArraySort<D, R>>,
-        rightArray: SimplifierFlatArrayStoreExpr<D, R>,
+    private fun <A : KArraySortBase<R>, R : KSort> simplifyArrayStoreEq(
+        lhs: KExpr<A>,
+        leftArray: SimplifierFlatArrayStoreBaseExpr<A, R>,
+        rhs: KExpr<A>,
+        rightArray: SimplifierFlatArrayStoreBaseExpr<A, R>,
     ): SimplifierAuxExpression<KBoolSort> = auxExpr {
         val checks = arrayListOf<KExpr<KBoolSort>>()
-        if (leftArray.base is KArrayConst<D, R> && rightArray.base is KArrayConst<D, R>) {
+        if (leftArray.base is KArrayConst<A, *> && rightArray.base is KArrayConst<A, *>) {
             // (= (const a) (const b)) ==> (= a b)
-            checks += KEqExpr(ctx, leftArray.base.value, rightArray.base.value)
+            checks += KEqExpr(
+                ctx,
+                leftArray.base.value.uncheckedCast<_, KExpr<KSort>>(),
+                rightArray.base.value.uncheckedCast()
+            )
         } else {
             check(leftArray.base == rightArray.base) {
                 "Base arrays expected to be equal or constant"
@@ -74,7 +97,7 @@ interface KArrayExprSimplifier : KExprSimplifierBase {
         val leftArraySearchInfo = analyzeArrayStores(leftArray)
         val rightArraySearchInfo = analyzeArrayStores(rightArray)
 
-        val allIndices = leftArray.indices.toSet() + rightArray.indices.toSet()
+        val allIndices = leftArraySearchInfo.storeIndices.keys + rightArraySearchInfo.storeIndices.keys
         for (idx in allIndices) {
             val lValue = selectArrayValue(idx, leftArraySearchInfo, lhs, leftArray)
             val rValue = selectArrayValue(idx, rightArraySearchInfo, rhs, rightArray)
@@ -86,46 +109,38 @@ interface KArrayExprSimplifier : KExprSimplifierBase {
         KAndExpr(ctx, checks)
     }
 
-    private class ArrayStoreSearchInfo<D : KSort, R : KSort>(
-        val storeIndices: Map<KExpr<D>, Int>,
+    private class ArrayStoreSearchInfo<A : KArraySortBase<R>, R : KSort>(
+        val storeIndices: Map<List<KExpr<*>>, Int>,
         val storeValues: List<KExpr<R>>,
-        val nonConstants: List<KExpr<D>>,
+        val nonConstants: List<List<KExpr<*>>>,
         val nonConstantsToCheck: IntArray
     )
 
-    private fun <D : KSort, R : KSort> selectArrayValue(
-        selectIndex: KExpr<D>,
-        arraySearchInfo: ArrayStoreSearchInfo<D, R>,
-        originalArrayExpr: KExpr<KArraySort<D, R>>,
-        flatArray: SimplifierFlatArrayStoreExpr<D, R>
+    private fun <A : KArraySortBase<R>, R : KSort> selectArrayValue(
+        selectIndex: List<KExpr<*>>,
+        arraySearchInfo: ArrayStoreSearchInfo<A, R>,
+        originalArrayExpr: KExpr<A>,
+        flatArray: SimplifierFlatArrayStoreBaseExpr<A, R>
     ): KExpr<R> =
         findStoredArrayValue(arraySearchInfo, selectIndex)
-            ?: SimplifierFlatArraySelectExpr(
-                ctx,
-                originalArrayExpr,
-                flatArray.base,
-                flatArray.indices,
-                flatArray.values,
-                selectIndex
-            )
+            ?: flatArray.selectValue(originalArrayExpr, selectIndex)
 
     /**
      * Preprocess flat array stores for faster index search.
      * @see [findStoredArrayValue]
      * */
-    private fun <D : KSort, R : KSort> analyzeArrayStores(
-        array: SimplifierFlatArrayStoreExpr<D, R>
-    ): ArrayStoreSearchInfo<D, R> {
-        val indices = array.indices
-        val indexId = hashMapOf<KExpr<D>, Int>()
-        val nonConstants = arrayListOf<KExpr<D>>()
-        val nonConstantsToCheck = IntArray(indices.size)
-
-        for (i in indices.indices) {
-            val storeIndex = indices[i]
+    private fun <A : KArraySortBase<R>, R : KSort> analyzeArrayStores(
+        array: SimplifierFlatArrayStoreBaseExpr<A, R>
+    ): ArrayStoreSearchInfo<A, R> {
+        val indexId = hashMapOf<List<KExpr<*>>, Int>()
+        val nonConstants = arrayListOf<List<KExpr<*>>>()
+        val nonConstantsToCheck = IntArray(array.numIndices)
+
+        for (i in 0 until array.numIndices) {
+            val storeIndex = array.getStoreIndex(i)
             if (storeIndex !in indexId) {
                 indexId[storeIndex] = i
-                if (!storeIndex.definitelyIsConstant) {
+                if (!storeIndex.all { it.definitelyIsConstant }) {
                     nonConstants += storeIndex
                 }
             }
@@ -145,9 +160,9 @@ interface KArrayExprSimplifier : KExprSimplifierBase {
      * @return null if there is no such index in the array,
      * or it is impossible to establish equality of some of the stored indices.
      * */
-    private fun <D : KSort, R : KSort> findStoredArrayValue(
-        array: ArrayStoreSearchInfo<D, R>,
-        selectIndex: KExpr<D>,
+    private fun <A : KArraySortBase<R>, R : KSort> findStoredArrayValue(
+        array: ArrayStoreSearchInfo<A, R>,
+        selectIndex: List<KExpr<*>>,
     ): KExpr<R>? {
         val storeIndex = array.storeIndices[selectIndex] ?: return null
 
@@ -172,115 +187,312 @@ interface KArrayExprSimplifier : KExprSimplifierBase {
             preprocess = { flatStores(expr) }
         )
 
-    override fun <D : KSort, R : KSort> transform(expr: KArraySelect<D, R>): KExpr<R> =
+    override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+        expr: KArray2Store<D0, D1, R>
+    ): KExpr<KArray2Sort<D0, D1, R>> =
+        simplifyExpr(
+            expr = expr,
+            preprocess = { flatStores2(expr) }
+        )
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Store<D0, D1, D2, R>
+    ): KExpr<KArray3Sort<D0, D1, D2, R>> =
         simplifyExpr(
             expr = expr,
-            preprocess = {
-                val array = flatStores(expr.array)
-                SimplifierFlatArraySelectExpr(
-                    ctx,
-                    original = expr.array,
-                    baseArray = array.base,
-                    storedValues = array.values,
-                    storedIndices = array.indices,
-                    index = expr.index
+            preprocess = { flatStores3(expr) }
+        )
+
+    override fun <R : KSort> transform(expr: KArrayNStore<R>): KExpr<KArrayNSort<R>> =
+        simplifyExpr(
+            expr = expr,
+            preprocess = { flatStoresN(expr) }
+        )
+
+    private fun <D : KSort, R : KSort> transform(expr: SimplifierFlatArrayStoreExpr<D, R>): KExpr<KArraySort<D, R>> =
+        simplifyExpr(expr, expr.unwrap()) { args: List<KExpr<KSort>> ->
+            simplifyArrayStore(expr.wrap(args))
+        }
+
+    private fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+        expr: SimplifierFlatArray2StoreExpr<D0, D1, R>
+    ): KExpr<KArray2Sort<D0, D1, R>> =
+        simplifyExpr(expr, expr.unwrap()) { args: List<KExpr<KSort>> ->
+            simplifyArrayStore(expr.wrap(args))
+        }
+
+    private fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: SimplifierFlatArray3StoreExpr<D0, D1, D2, R>
+    ): KExpr<KArray3Sort<D0, D1, D2, R>> =
+        simplifyExpr(expr, expr.unwrap()) { args: List<KExpr<KSort>> ->
+            simplifyArrayStore(expr.wrap(args))
+        }
+
+    private fun <R : KSort> transform(expr: SimplifierFlatArrayNStoreExpr<R>): KExpr<KArrayNSort<R>> =
+        simplifyExpr(expr, expr.unwrap()) { args: List<KExpr<KSort>> ->
+            simplifyArrayStore(expr.wrap(args))
+        }
+
+    private fun <D : KSort, R : KSort> simplifyArrayStore(
+        expr: SimplifierFlatArrayStoreExpr<D, R>
+    ): KExpr<KArraySort<D, R>> {
+        val indices = expr.indices
+        val storedIndices = hashMapOf<KExpr<D>, Int>()
+        val simplifiedIndices = arrayListOf<KExpr<D>>()
+
+        return simplifyArrayStore(
+            expr = expr,
+            findStoredIndexPosition = { i ->
+                storedIndices[indices[i]]
+            },
+            saveStoredIndexPosition = { i, indexPosition ->
+                storedIndices[indices[i]] = indexPosition
+            },
+            indexIsConstant = { i ->
+                indices[i].definitelyIsConstant
+            },
+            addSimplifiedIndex = { i ->
+                simplifiedIndices.add(indices[i])
+            },
+            distinctWithSimplifiedIndex = { i, simplifiedIdx ->
+                areDefinitelyDistinct(indices[i], simplifiedIndices[simplifiedIdx])
+            },
+            selectIndicesMatch = { select: KArraySelect<D, R>, i ->
+                indices[i] == select.index
+            },
+            mkSimplifiedStore = { array, simplifiedIdx, value ->
+                ctx.mkArrayStoreNoSimplify(array, simplifiedIndices[simplifiedIdx], value)
+            }
+        )
+    }
+
+    private fun <D0 : KSort, D1 : KSort, R : KSort> simplifyArrayStore(
+        expr: SimplifierFlatArray2StoreExpr<D0, D1, R>
+    ): KExpr<KArray2Sort<D0, D1, R>> {
+        val indices0 = expr.indices0
+        val indices1 = expr.indices1
+
+        val storedIndices = hashMapOf<KExpr<D0>, MutableMap<KExpr<D1>, Int>>()
+        val simplifiedIndices0 = arrayListOf<KExpr<D0>>()
+        val simplifiedIndices1 = arrayListOf<KExpr<D1>>()
+
+        return simplifyArrayStore(
+            expr = expr,
+            findStoredIndexPosition = { i ->
+                storedIndices[indices0[i]]?.get(indices1[i])
+            },
+            saveStoredIndexPosition = { i, indexPosition ->
+                val index1Map = storedIndices.getOrPut(indices0[i]) { hashMapOf() }
+                index1Map[indices1[i]] = indexPosition
+            },
+            indexIsConstant = { i ->
+                indices0[i].definitelyIsConstant && indices1[i].definitelyIsConstant
+            },
+            addSimplifiedIndex = { i ->
+                simplifiedIndices0.add(indices0[i])
+                simplifiedIndices1.add(indices1[i])
+            },
+            distinctWithSimplifiedIndex = { i, simplifiedIdx ->
+                areDefinitelyDistinct(indices0[i], simplifiedIndices0[simplifiedIdx])
+                    && areDefinitelyDistinct(indices1[i], simplifiedIndices1[simplifiedIdx])
+            },
+            selectIndicesMatch = { select: KArray2Select<D0, D1, R>, i ->
+                indices0[i] == select.index0 && indices1[i] == select.index1
+            },
+            mkSimplifiedStore = { array, simplifiedIdx, value ->
+                ctx.mkArrayStoreNoSimplify(
+                    array,
+                    simplifiedIndices0[simplifiedIdx],
+                    simplifiedIndices1[simplifiedIdx],
+                    value
                 )
             }
         )
+    }
 
-    @Suppress("ComplexMethod", "LoopWithTooManyJumpStatements")
-    private fun <D : KSort, R : KSort> transform(expr: SimplifierFlatArrayStoreExpr<D, R>): KExpr<KArraySort<D, R>> =
-        simplifyExpr(expr, expr.args) { transformedArgs ->
-            val base: KExpr<KArraySort<D, R>> = transformedArgs.first().uncheckedCast()
-            val indices: List<KExpr<D>> = transformedArgs.subList(
-                fromIndex = 1, toIndex = 1 + expr.indices.size
-            ).uncheckedCast()
-            val values: List<KExpr<R>> = transformedArgs.subList(
-                fromIndex = 1 + expr.indices.size, toIndex = transformedArgs.size
-            ).uncheckedCast()
+    private fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> simplifyArrayStore(
+        expr: SimplifierFlatArray3StoreExpr<D0, D1, D2, R>
+    ): KExpr<KArray3Sort<D0, D1, D2, R>> {
+        val indices0 = expr.indices0
+        val indices1 = expr.indices1
+        val indices2 = expr.indices2
+
+        val storedIndices = hashMapOf<KExpr<D0>, MutableMap<KExpr<D1>, MutableMap<KExpr<D2>, Int>>>()
+        val simplifiedIndices0 = arrayListOf<KExpr<D0>>()
+        val simplifiedIndices1 = arrayListOf<KExpr<D1>>()
+        val simplifiedIndices2 = arrayListOf<KExpr<D2>>()
 
-            if (indices.isEmpty()) {
-                return@simplifyExpr base
+        return simplifyArrayStore(
+            expr = expr,
+            findStoredIndexPosition = { i ->
+                storedIndices[indices0[i]]?.get(indices1[i])?.get(indices2[i])
+            },
+            saveStoredIndexPosition = { i, indexPosition ->
+                val index1Map = storedIndices.getOrPut(indices0[i]) { hashMapOf() }
+                val index2Map = index1Map.getOrPut(indices1[i]) { hashMapOf() }
+                index2Map[indices2[i]] = indexPosition
+            },
+            indexIsConstant = { i ->
+                indices0[i].definitelyIsConstant
+                    && indices1[i].definitelyIsConstant
+                    && indices2[i].definitelyIsConstant
+            },
+            addSimplifiedIndex = { i ->
+                simplifiedIndices0.add(indices0[i])
+                simplifiedIndices1.add(indices1[i])
+                simplifiedIndices2.add(indices2[i])
+            },
+            distinctWithSimplifiedIndex = { i, simplifiedIdx ->
+                areDefinitelyDistinct(indices0[i], simplifiedIndices0[simplifiedIdx])
+                    && areDefinitelyDistinct(indices1[i], simplifiedIndices1[simplifiedIdx])
+                    && areDefinitelyDistinct(indices2[i], simplifiedIndices2[simplifiedIdx])
+            },
+            selectIndicesMatch = { select: KArray3Select<D0, D1, D2, R>, i ->
+                indices0[i] == select.index0
+                    && indices1[i] == select.index1
+                    && indices2[i] == select.index2
+            },
+            mkSimplifiedStore = { array, simplifiedIdx, value ->
+                ctx.mkArrayStoreNoSimplify(
+                    array,
+                    simplifiedIndices0[simplifiedIdx],
+                    simplifiedIndices1[simplifiedIdx],
+                    simplifiedIndices2[simplifiedIdx],
+                    value
+                )
             }
+        )
+    }
 
-            val storedIndices = hashMapOf<KExpr<D>, Int>()
-            val simplifiedIndices = arrayListOf<KExpr<D>>()
-            val simplifiedValues = arrayListOf<KExpr<R>>()
-            var lastNonConstantIndex = -1
-
-            for (i in indices.indices.reversed()) {
-                val index = indices[i]
-                val value = values[i]
-
-                val storedIndexPosition = storedIndices[index]
-                if (storedIndexPosition != null) {
-
-                    /** Try push store.
-                     * (store (store a i x) j y), i != j ==> (store (store a j y) i x)
-                     *
-                     * Store can be pushed only if all parent indices are definitely not equal.
-                     * */
-                    val allParentIndicesAreDistinct = allParentSoreIndicesAreDistinct(
-                        index = index,
-                        storedIndexPosition = storedIndexPosition,
-                        lastNonConstantIndex = lastNonConstantIndex,
-                        simplifiedIndices = simplifiedIndices
-                    )
-
-                    if (allParentIndicesAreDistinct) {
-                        simplifiedValues[storedIndexPosition] = value
-                        if (!index.definitelyIsConstant) {
-                            lastNonConstantIndex = maxOf(lastNonConstantIndex, storedIndexPosition)
-                        }
-                        continue
-                    }
-                }
+    private fun <R : KSort> simplifyArrayStore(
+        expr: SimplifierFlatArrayNStoreExpr<R>
+    ): KExpr<KArrayNSort<R>> {
+        val indices = expr.indices
+        val storedIndices = hashMapOf<List<KExpr<*>>, Int>()
+        val simplifiedIndices = arrayListOf<List<KExpr<*>>>()
 
-                // simplify direct store to array
-                if (storedIndices.isEmpty()) {
-                    // (store (const v) i v) ==> (const v)
-                    if (base is KArrayConst<D, R> && base.value == value) {
-                        continue
-                    }
+        return simplifyArrayStore(
+            expr = expr,
+            findStoredIndexPosition = { i ->
+                storedIndices[indices[i]]
+            },
+            saveStoredIndexPosition = { i, indexPosition ->
+                storedIndices[indices[i]] = indexPosition
+            },
+            indexIsConstant = { i ->
+                indices[i].all { it.definitelyIsConstant }
+            },
+            addSimplifiedIndex = { i ->
+                simplifiedIndices.add(indices[i])
+            },
+            distinctWithSimplifiedIndex = { i, simplifiedIdx ->
+                areDefinitelyDistinct(indices[i], simplifiedIndices[simplifiedIdx])
+            },
+            selectIndicesMatch = { select: KArrayNSelect<R>, i ->
+                indices[i] == select.indices
+            },
+            mkSimplifiedStore = { array, simplifiedIdx, value ->
+                ctx.mkArrayNStoreNoSimplify(array, simplifiedIndices[simplifiedIdx], value)
+            }
+        )
+    }
+
+    @Suppress("LongParameterList", "NestedBlockDepth", "ComplexMethod", "LoopWithTooManyJumpStatements")
+    private inline fun <A : KArraySortBase<R>, R : KSort, reified S : KArraySelectBase<out A, R>> simplifyArrayStore(
+        expr: SimplifierFlatArrayStoreBaseExpr<A, R>,
+        findStoredIndexPosition: (Int) -> Int?,
+        saveStoredIndexPosition: (Int, Int) -> Unit,
+        indexIsConstant: (Int) -> Boolean,
+        addSimplifiedIndex: (Int) -> Unit,
+        distinctWithSimplifiedIndex: (Int, Int) -> Boolean,
+        selectIndicesMatch: (S, Int) -> Boolean,
+        mkSimplifiedStore: (KExpr<A>, Int, KExpr<R>) -> KExpr<A>
+    ): KExpr<A> {
+        if (expr.numIndices == 0) {
+            return expr.base
+        }
+
+        val simplifiedValues = arrayListOf<KExpr<R>>()
+        var numSimplifiedIndices = 0
+        var lastNonConstantIndex = -1
+
+        for (i in expr.numIndices - 1 downTo 0) {
+            val value = expr.values[i]
+
+            val storedIndexPosition = findStoredIndexPosition(i)
+            if (storedIndexPosition != null) {
+
+                /** Try push store.
+                 * (store (store a i x) j y), i != j ==> (store (store a j y) i x)
+                 *
+                 * Store can be pushed only if all parent indices are definitely not equal.
+                 * */
+                val allParentIndicesAreDistinct = allParentSoreIndicesAreDistinct(
+                    index = i,
+                    storedIndexPosition = storedIndexPosition,
+                    lastNonConstantIndex = lastNonConstantIndex,
+                    numSimplifiedIndices = numSimplifiedIndices,
+                    indexIsConstant = { x -> indexIsConstant(x) },
+                    distinctWithSimplifiedIndex = { x, y -> distinctWithSimplifiedIndex(x, y) }
+                )
 
-                    // (store a i (select a i)) ==> a
-                    if (value is KArraySelect<*, *> && base == value.array && index == value.index) {
-                        continue
+                if (allParentIndicesAreDistinct) {
+                    simplifiedValues[storedIndexPosition] = value
+                    if (!indexIsConstant(i)) {
+                        lastNonConstantIndex = maxOf(lastNonConstantIndex, storedIndexPosition)
                     }
+                    continue
                 }
+            }
 
-                // store
-                simplifiedIndices.add(index)
-                simplifiedValues.add(value)
-                val indexPosition = simplifiedIndices.lastIndex
-                storedIndices[index] = indexPosition
-                if (!index.definitelyIsConstant) {
-                    lastNonConstantIndex = maxOf(lastNonConstantIndex, indexPosition)
+            // simplify direct store to array
+            if (numSimplifiedIndices == 0) {
+                // (store (const v) i v) ==> (const v)
+                if (expr.base is KArrayConst<A, *> && expr.base.value == expr.values[i]) {
+                    continue
+                }
+
+                // (store a i (select a i)) ==> a
+                if (value is S && expr.base == value.array && selectIndicesMatch(value, i)) {
+                    continue
                 }
             }
 
-            var result = base
-            for (i in simplifiedIndices.indices) {
-                val index = simplifiedIndices[i]
-                val value = simplifiedValues[i]
-                result = mkArrayStoreNoSimplify(result, index, value)
+            // store
+            simplifiedValues.add(value)
+
+            val indexPosition = numSimplifiedIndices++
+            addSimplifiedIndex(i)
+            saveStoredIndexPosition(i, indexPosition)
+
+            if (!indexIsConstant(i)) {
+                lastNonConstantIndex = maxOf(lastNonConstantIndex, indexPosition)
             }
+        }
 
-            return@simplifyExpr result
+        var result = expr.base
+        for (i in 0 until numSimplifiedIndices) {
+            result = mkSimplifiedStore(result, i, simplifiedValues[i])
         }
 
-    private fun <D : KSort> allParentSoreIndicesAreDistinct(
-        index: KExpr<D>,
+        return result
+    }
+
+    @Suppress("LongParameterList")
+    private inline fun allParentSoreIndicesAreDistinct(
+        index: Int,
         storedIndexPosition: Int,
         lastNonConstantIndex: Int,
-        simplifiedIndices: List<KExpr<D>>
+        numSimplifiedIndices: Int,
+        indexIsConstant: (Int) -> Boolean,
+        distinctWithSimplifiedIndex: (Int, Int) -> Boolean
     ): Boolean {
         /**
          * Since all constants are trivially comparable we can guarantee, that
          * all parents are distinct.
          * Otherwise, we need to perform full check of parent indices.
          * */
-        if (index.definitelyIsConstant && storedIndexPosition >= lastNonConstantIndex) return true
+        if (indexIsConstant(index) && storedIndexPosition >= lastNonConstantIndex) return true
 
         /**
          *  If non-constant index is among the indices we need to check,
@@ -288,13 +500,13 @@ interface KArrayExprSimplifier : KExprSimplifierBase {
          *  not definitely distinct, we will not check all other indices.
          * */
         if (lastNonConstantIndex > storedIndexPosition
-            && !areDefinitelyDistinct(index, simplifiedIndices[lastNonConstantIndex])
+            && !distinctWithSimplifiedIndex(index, lastNonConstantIndex)
         ) {
             return false
         }
 
-        for (checkIdx in (storedIndexPosition + 1) until simplifiedIndices.size) {
-            if (!areDefinitelyDistinct(index, simplifiedIndices[checkIdx])) {
+        for (checkIdx in (storedIndexPosition + 1) until numSimplifiedIndices) {
+            if (!distinctWithSimplifiedIndex(index, checkIdx)) {
                 // possibly equal index, we can't squash stores
                 return false
             }
@@ -303,77 +515,276 @@ interface KArrayExprSimplifier : KExprSimplifierBase {
         return true
     }
 
-    /**
-     * Try to simplify only indices first.
-     * Usually this will be enough and we will not produce many irrelevant array store expressions.
-     * */
-    private fun <D : KSort, R : KSort> transform(expr: SimplifierFlatArraySelectExpr<D, R>): KExpr<R> =
-        simplifyExpr(expr, expr.args) { allIndices ->
-            val index = allIndices.first()
-            val arrayIndices = allIndices.subList(fromIndex = 1, toIndex = allIndices.size)
-
-            var arrayStoreIdx = 0
-            while (arrayStoreIdx < arrayIndices.size) {
-                val storeIdx = arrayIndices[arrayStoreIdx]
-
-                // (select (store i v) i) ==> v
-                if (storeIdx == index) {
-                    return@simplifyExpr rewrite(expr.storedValues[arrayStoreIdx])
-                }
+    override fun <D : KSort, R : KSort> transform(expr: KArraySelect<D, R>): KExpr<R> =
+        simplifyExpr(expr, expr.index) { index ->
+            transformSelect(expr.array, index)
+        }
 
-                if (!areDefinitelyDistinct(index, storeIdx)) {
-                    break
-                }
+    override fun <D0 : KSort, D1 : KSort, R : KSort> transform(expr: KArray2Select<D0, D1, R>): KExpr<R> =
+        simplifyExpr(expr, expr.index0, expr.index1) { index0, index1 ->
+            transformSelect(expr.array, index0, index1)
+        }
 
-                // (select (store a i v) j), i != j ==> (select a j)
-                arrayStoreIdx++
-            }
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Select<D0, D1, D2, R>
+    ): KExpr<R> = simplifyExpr(expr, expr.index0, expr.index1, expr.index2) { index0, index1, index2 ->
+        transformSelect(expr.array, index0, index1, index2)
+    }
 
-            if (arrayStoreIdx == arrayIndices.size) {
-                return@simplifyExpr rewrite(SimplifierArraySelectExpr(ctx, expr.baseArray, index))
-            }
+    override fun <R : KSort> transform(expr: KArrayNSelect<R>): KExpr<R> =
+        simplifyExpr(expr, expr.indices) { indices ->
+            transformSelect(expr.array, indices)
+        }
+
+    fun <D : KSort, R : KSort> transformSelect(
+        array: KExpr<KArraySort<D, R>>, index: KExpr<D>
+    ): KExpr<R> = transformSelect(
+        array,
+        selectFromStore = { store: KArrayStore<D, R> -> SelectFromStoreExpr(ctx, store, index) },
+        selectFromFunction = { f -> KFunctionApp(ctx, f, listOf(index).uncheckedCast()) },
+        default = { SimplifierArraySelectExpr(ctx, array, index) }
+    )
+
+    fun <D0 : KSort, D1 : KSort, R : KSort> transformSelect(
+        array: KExpr<KArray2Sort<D0, D1, R>>, index0: KExpr<D0>, index1: KExpr<D1>
+    ): KExpr<R> = transformSelect(
+        array,
+        selectFromStore = { store: KArray2Store<D0, D1, R> -> Select2FromStoreExpr(ctx, store, index0, index1) },
+        selectFromFunction = { f -> KFunctionApp(ctx, f, listOf(index0, index1).uncheckedCast()) },
+        default = { SimplifierArray2SelectExpr(ctx, array, index0, index1) }
+    )
+
+    fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transformSelect(
+        array: KExpr<KArray3Sort<D0, D1, D2, R>>,
+        index0: KExpr<D0>, index1: KExpr<D1>, index2: KExpr<D2>
+    ): KExpr<R> = transformSelect(
+        array,
+        selectFromStore = { store: KArray3Store<D0, D1, D2, R> ->
+            Select3FromStoreExpr(ctx, store, index0, index1, index2)
+        },
+        selectFromFunction = { f -> KFunctionApp(ctx, f, listOf(index0, index1, index2).uncheckedCast()) },
+        default = { SimplifierArray3SelectExpr(ctx, array, index0, index1, index2) }
+    )
 
-            rewrite(SimplifierArraySelectExpr(ctx, expr.original, index))
+    fun <R : KSort> transformSelect(
+        array: KExpr<KArrayNSort<R>>, indices: List<KExpr<KSort>>
+    ): KExpr<R> = transformSelect(
+        array,
+        selectFromStore = { store: KArrayNStore<R> -> SelectNFromStoreExpr(ctx, store, indices) },
+        selectFromFunction = { f -> KFunctionApp(ctx, f, indices) },
+        default = { SimplifierArrayNSelectExpr(ctx, array, indices) }
+    )
+
+    private inline fun <A : KArraySortBase<R>, R : KSort, reified S : KArrayStoreBase<A, R>> transformSelect(
+        array: KExpr<A>,
+        selectFromStore: (S) -> KExpr<R>,
+        selectFromFunction: (KDecl<R>) -> KExpr<R>,
+        default: () -> KExpr<R>
+    ): KExpr<R> = when (array) {
+        is S -> rewrite(selectFromStore(array))
+        is KFunctionAsArray<A, *> -> rewrite(selectFromFunction(array.function.uncheckedCast()))
+        else -> rewrite(default())
+    }
+
+    private fun <D : KSort, R : KSort> transform(expr: SelectFromStoreExpr<D, R>): KExpr<R> =
+        simplifyExpr(expr, expr.array.index) { storeIndex ->
+            transformSelectFromStore(
+                expr = expr,
+                indexMatch = { expr.index == storeIndex },
+                indexDistinct = { areDefinitelyDistinct(expr.index, storeIndex) },
+                transformNested = { transformSelect(expr.array.array, expr.index) },
+                default = { SimplifierArraySelectExpr(ctx, expr.array, expr.index) }
+            )
         }
 
+    private fun <D0 : KSort, D1 : KSort, R : KSort> transform(expr: Select2FromStoreExpr<D0, D1, R>): KExpr<R> =
+        simplifyExpr(expr, expr.array.index0, expr.array.index1) { storeIndex0, storeIndex1 ->
+            transformSelectFromStore(
+                expr = expr,
+                indexMatch = { expr.index0 == storeIndex0 && expr.index1 == storeIndex1 },
+                indexDistinct = {
+                    areDefinitelyDistinct(expr.index0, storeIndex0)
+                        && areDefinitelyDistinct(expr.index1, storeIndex1)
+                },
+                transformNested = { transformSelect(expr.array.array, expr.index0, expr.index1) },
+                default = { SimplifierArray2SelectExpr(ctx, expr.array, expr.index0, expr.index1) }
+            )
+        }
+
+    private fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: Select3FromStoreExpr<D0, D1, D2, R>
+    ): KExpr<R> =
+        simplifyExpr(expr, expr.array.index0, expr.array.index1, expr.array.index2) { si0, si1, si2 ->
+            transformSelectFromStore(
+                expr = expr,
+                indexMatch = { expr.index0 == si0 && expr.index1 == si1 && expr.index2 == si2 },
+                indexDistinct = {
+                    areDefinitelyDistinct(expr.index0, si0)
+                        && areDefinitelyDistinct(expr.index1, si1)
+                        && areDefinitelyDistinct(expr.index2, si2)
+                },
+                transformNested = { transformSelect(expr.array.array, expr.index0, expr.index1, expr.index2) },
+                default = { SimplifierArray3SelectExpr(ctx, expr.array, expr.index0, expr.index1, expr.index2) }
+            )
+        }
+
+    private fun <R : KSort> transform(expr: SelectNFromStoreExpr<R>): KExpr<R> =
+        simplifyExpr(expr, expr.array.indices) { indices ->
+            transformSelectFromStore(
+                expr = expr,
+                indexMatch = { expr.indices == indices },
+                indexDistinct = { areDefinitelyDistinct(expr.indices, indices) },
+                transformNested = { transformSelect(expr.array.array, expr.indices) },
+                default = { SimplifierArrayNSelectExpr(ctx, expr.array, expr.indices) }
+            )
+        }
+
+    private inline fun <A : KArraySortBase<R>, R : KSort> transformSelectFromStore(
+        expr: SelectFromStoreExprBase<A, R>,
+        indexMatch: () -> Boolean,
+        indexDistinct: () -> Boolean,
+        transformNested: () -> KExpr<R>,
+        default: () -> KExpr<R>
+    ): KExpr<R> {
+        // (select (store i v) i) ==> v
+        if (indexMatch()) {
+            return rewrite(expr.storeValue)
+        }
+
+        // (select (store a i v) j), i != j ==> (select a j)
+        if (indexDistinct()) {
+            return transformNested()
+        }
+
+        return rewrite(default())
+    }
+
     private fun <D : KSort, R : KSort> transform(expr: SimplifierArraySelectExpr<D, R>): KExpr<R> =
-        simplifyExpr(expr, expr.array, expr.index) { arrayArg, indexArg ->
-            var array: KExpr<KArraySort<D, R>> = arrayArg.uncheckedCast()
-            val index: KExpr<D> = indexArg.uncheckedCast()
-
-            while (array is KArrayStore<D, R>) {
-                // (select (store i v) i) ==> v
-                if (array.index == index) {
-                    return@simplifyExpr array.value
-                }
+        simplifyExpr(expr, expr.array) { array ->
+            transformSelectFull(
+                expr = array,
+                storeIndexMatch = { store: KArrayStore<D, R> -> expr.index == store.index },
+                storeIndexDistinct = { store: KArrayStore<D, R> -> areDefinitelyDistinct(expr.index, store.index) },
+                mkLambdaSubstitution = { lambda: KArrayLambda<D, R> ->
+                    substitute(mkConstApp(lambda.indexVarDecl), expr.index)
+                },
+                default = { mkArraySelectNoSimplify(it, expr.index) }
+            )
+        }
 
-                // (select (store a i v) j), i != j ==> (select a j)
-                if (areDefinitelyDistinct(index, array.index)) {
-                    array = array.array
-                } else {
-                    // possibly equal index, we can't expand stores
-                    break
-                }
+    private fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+        expr: SimplifierArray2SelectExpr<D0, D1, R>
+    ): KExpr<R> = simplifyExpr(expr, expr.array) { array ->
+        transformSelectFull(
+            expr = array,
+            storeIndexMatch = { store: KArray2Store<D0, D1, R> ->
+                expr.index0 == store.index0 && expr.index1 == store.index1
+            },
+            storeIndexDistinct = { store: KArray2Store<D0, D1, R> ->
+                areDefinitelyDistinct(expr.index0, store.index0)
+                    && areDefinitelyDistinct(expr.index1, store.index1)
+            },
+            mkLambdaSubstitution = { lambda: KArray2Lambda<D0, D1, R> ->
+                substitute(mkConstApp(lambda.indexVar0Decl), expr.index0)
+                substitute(mkConstApp(lambda.indexVar1Decl), expr.index1)
+            },
+            default = { mkArraySelectNoSimplify(it, expr.index0, expr.index1) }
+        )
+    }
+
+    private fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: SimplifierArray3SelectExpr<D0, D1, D2, R>
+    ): KExpr<R> = simplifyExpr(expr, expr.array) { array ->
+        transformSelectFull(
+            expr = array,
+            storeIndexMatch = { store: KArray3Store<D0, D1, D2, R> ->
+                expr.index0 == store.index0
+                    && expr.index1 == store.index1
+                    && expr.index2 == store.index2
+            },
+            storeIndexDistinct = { store: KArray3Store<D0, D1, D2, R> ->
+                areDefinitelyDistinct(expr.index0, store.index0)
+                    && areDefinitelyDistinct(expr.index1, store.index1)
+                    && areDefinitelyDistinct(expr.index2, store.index2)
+            },
+            mkLambdaSubstitution = { lambda: KArray3Lambda<D0, D1, D2, R> ->
+                substitute(mkConstApp(lambda.indexVar0Decl), expr.index0)
+                substitute(mkConstApp(lambda.indexVar1Decl), expr.index1)
+                substitute(mkConstApp(lambda.indexVar2Decl), expr.index2)
+            },
+            default = { mkArraySelectNoSimplify(it, expr.index0, expr.index1, expr.index2) }
+        )
+    }
+
+    private fun <R : KSort> transform(expr: SimplifierArrayNSelectExpr<R>): KExpr<R> =
+        simplifyExpr(expr, expr.array) { array ->
+            transformSelectFull(
+                expr = array,
+                storeIndexMatch = { store: KArrayNStore<R> -> expr.indices == store.indices },
+                storeIndexDistinct = { store: KArrayNStore<R> -> areDefinitelyDistinct(expr.indices, store.indices) },
+                mkLambdaSubstitution = { lambda: KArrayNLambda<R> ->
+                    lambda.indexVarDeclarations.zip(expr.indices) { varDecl, index ->
+                        substitute(mkConstApp(varDecl).uncheckedCast<_, KExpr<KSort>>(), index.uncheckedCast())
+                    }
+                },
+                default = { mkArrayNSelectNoSimplify(it, expr.indices) }
+            )
+        }
+
+    private inline fun <
+        A : KArraySortBase<R>,
+        R : KSort,
+        reified S : KArrayStoreBase<A, R>,
+        reified L : KArrayLambdaBase<A, R>
+    > transformSelectFull(
+        expr: KExpr<A>,
+        storeIndexMatch: (S) -> Boolean,
+        storeIndexDistinct: (S) -> Boolean,
+        mkLambdaSubstitution: KExprSubstitutor.(L) -> Unit,
+        default: (KExpr<A>) -> KExpr<R>
+    ): KExpr<R> {
+        var array: KExpr<A> = expr
+        while (array is S) {
+            // (select (store i v) i) ==> v
+            if (storeIndexMatch(array)) {
+                return array.value
             }
 
-            when (array) {
-                // (select (const v) i) ==> v
-                is KArrayConst<D, R> -> {
-                    array.value
-                }
-                // (select (lambda x body) i) ==> body[i/x]
-                is KArrayLambda<D, R> -> {
-                    val resolvedBody = KExprSubstitutor(ctx).apply {
-                        val indexVarExpr = mkConstApp(array.indexVarDecl)
-                        substitute(indexVarExpr, index)
-                    }.apply(array.body)
-                    rewrite(resolvedBody)
-                }
-                else -> {
-                    mkArraySelectNoSimplify(array, index)
-                }
+            // (select (store a i v) j), i != j ==> (select a j)
+            if (storeIndexDistinct(array)) {
+                array = array.array
+            } else {
+                // possibly equal index, we can't expand stores
+                break
+            }
+        }
+
+        return when (array) {
+            // (select (const v) i) ==> v
+            is KArrayConst<A, *> -> {
+                array.value.uncheckedCast()
             }
+            // (select (lambda x body) i) ==> body[i/x]
+            is L -> {
+                val resolvedBody = KExprSubstitutor(ctx).apply {
+                    mkLambdaSubstitution(array)
+                }.apply(array.body)
+                rewrite(resolvedBody)
+            }
+
+            else -> default(array)
         }
+    }
+
+    @Suppress("USELESS_CAST") // Exhaustive when
+    private fun <A : KArraySortBase<R>, R : KSort> flatStoresGeneric(
+        sort: A, expr: KExpr<A>
+    ): SimplifierFlatArrayStoreBaseExpr<A, R> = when (sort as KArraySortBase<R>) {
+        is KArraySort<*, R> -> flatStores<KSort, R>(expr.uncheckedCast()).uncheckedCast()
+        is KArray2Sort<*, *, R> -> flatStores2<KSort, KSort, R>(expr.uncheckedCast()).uncheckedCast()
+        is KArray3Sort<*, *, *, R> -> flatStores3<KSort, KSort, KSort, R>(expr.uncheckedCast()).uncheckedCast()
+        is KArrayNSort<R> -> flatStoresN<R>(expr.uncheckedCast()).uncheckedCast()
+    }
 
     private fun <D : KSort, R : KSort> flatStores(
         expr: KExpr<KArraySort<D, R>>,
@@ -388,6 +799,76 @@ interface KArrayExprSimplifier : KExprSimplifierBase {
         }
         return SimplifierFlatArrayStoreExpr(
             ctx = ctx,
+            original = expr,
+            base = base,
+            indices = indices,
+            values = values
+        )
+    }
+
+    private fun <D0 : KSort, D1 : KSort, R : KSort> flatStores2(
+        expr: KExpr<KArray2Sort<D0, D1, R>>,
+    ): SimplifierFlatArray2StoreExpr<D0, D1, R> {
+        val indices0 = arrayListOf<KExpr<D0>>()
+        val indices1 = arrayListOf<KExpr<D1>>()
+        val values = arrayListOf<KExpr<R>>()
+        var base = expr
+        while (base is KArray2Store<D0, D1, R>) {
+            indices0.add(base.index0)
+            indices1.add(base.index1)
+            values.add(base.value)
+            base = base.array
+        }
+        return SimplifierFlatArray2StoreExpr(
+            ctx = ctx,
+            original = expr,
+            base = base,
+            indices0 = indices0,
+            indices1 = indices1,
+            values = values
+        )
+    }
+
+    private fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> flatStores3(
+        expr: KExpr<KArray3Sort<D0, D1, D2, R>>,
+    ): SimplifierFlatArray3StoreExpr<D0, D1, D2, R> {
+        val indices0 = arrayListOf<KExpr<D0>>()
+        val indices1 = arrayListOf<KExpr<D1>>()
+        val indices2 = arrayListOf<KExpr<D2>>()
+        val values = arrayListOf<KExpr<R>>()
+        var base = expr
+        while (base is KArray3Store<D0, D1, D2, R>) {
+            indices0.add(base.index0)
+            indices1.add(base.index1)
+            indices2.add(base.index2)
+            values.add(base.value)
+            base = base.array
+        }
+        return SimplifierFlatArray3StoreExpr(
+            ctx = ctx,
+            original = expr,
+            base = base,
+            indices0 = indices0,
+            indices1 = indices1,
+            indices2 = indices2,
+            values = values
+        )
+    }
+
+    private fun <R : KSort> flatStoresN(
+        expr: KExpr<KArrayNSort<R>>,
+    ): SimplifierFlatArrayNStoreExpr<R> {
+        val indices = arrayListOf<List<KExpr<*>>>()
+        val values = arrayListOf<KExpr<R>>()
+        var base = expr
+        while (base is KArrayNStore<R>) {
+            indices.add(base.indices)
+            values.add(base.value)
+            base = base.array
+        }
+        return SimplifierFlatArrayNStoreExpr(
+            ctx = ctx,
+            original = expr,
             base = base,
             indices = indices,
             values = values
@@ -397,54 +878,276 @@ interface KArrayExprSimplifier : KExprSimplifierBase {
     private val KExpr<*>.definitelyIsConstant: Boolean
         get() = this is KInterpretedValue<*>
 
+    private fun areDefinitelyDistinct(left: List<KExpr<*>>, right: List<KExpr<*>>): Boolean {
+        for (i in left.indices) {
+            val lhs: KExpr<KSort> = left[i].uncheckedCast()
+            val rhs: KExpr<KSort> = right[i].uncheckedCast()
+            if (!areDefinitelyDistinct(lhs, rhs)) return false
+        }
+        return true
+    }
+
     /**
      * Auxiliary expression to handle expanded array stores.
      * @see [SimplifierAuxExpression]
      * */
+    private sealed class SimplifierFlatArrayStoreBaseExpr<A : KArraySortBase<R>, R : KSort>(
+        ctx: KContext,
+        val numIndices: Int,
+        val original: KExpr<A>,
+        val base: KExpr<A>,
+        val values: List<KExpr<R>>
+    ) : KExpr<A>(ctx) {
+        override val sort: A
+            get() = base.sort
+
+        override fun internEquals(other: Any): Boolean =
+            error("Interning is not used for Aux expressions")
+
+        override fun internHashCode(): Int =
+            error("Interning is not used for Aux expressions")
+
+        override fun print(printer: ExpressionPrinter) {
+            original.print(printer)
+        }
+
+        abstract fun getStoreIndex(idx: Int): List<KExpr<*>>
+
+        abstract fun selectValue(originalArray: KExpr<A>, index: List<KExpr<*>>): KExpr<R>
+    }
+
     private class SimplifierFlatArrayStoreExpr<D : KSort, R : KSort>(
         ctx: KContext,
-        val base: KExpr<KArraySort<D, R>>,
+        original: KExpr<KArraySort<D, R>>,
+        base: KExpr<KArraySort<D, R>>,
         val indices: List<KExpr<D>>,
-        val values: List<KExpr<R>>,
-    ) : KApp<KArraySort<D, R>, KSort>(ctx) {
+        values: List<KExpr<R>>,
+    ) : SimplifierFlatArrayStoreBaseExpr<KArraySort<D, R>, R>(ctx, indices.size, original, base, values) {
+        override fun accept(transformer: KTransformerBase): KExpr<KArraySort<D, R>> {
+            transformer as KArrayExprSimplifier
+            return transformer.transform(this)
+        }
 
-        override val args: List<KExpr<KSort>> =
-            (listOf(base) + indices + values).uncheckedCast()
+        fun unwrap(): List<KExpr<KSort>> = (listOf(base) + indices + values).uncheckedCast()
+
+        fun wrap(args: List<KExpr<KSort>>) = SimplifierFlatArrayStoreExpr(
+            ctx,
+            original,
+            base = args.first().uncheckedCast(),
+            indices = args.subList(
+                fromIndex = 1, toIndex = 1 + numIndices
+            ).uncheckedCast(),
+            values = args.subList(
+                fromIndex = 1 + numIndices, toIndex = args.size
+            ).uncheckedCast()
+        )
 
-        override val decl: KDecl<KArraySort<D, R>>
-            get() = ctx.mkArrayStoreDecl(base.sort)
+        override fun getStoreIndex(idx: Int): List<KExpr<*>> = listOf(indices[idx])
 
-        override val sort: KArraySort<D, R>
-            get() = base.sort
+        override fun selectValue(originalArray: KExpr<KArraySort<D, R>>, index: List<KExpr<*>>): KExpr<R> =
+            KArraySelect(ctx, originalArray, index.single().uncheckedCast())
+    }
 
-        override fun accept(transformer: KTransformerBase): KExpr<KArraySort<D, R>> {
+    private class SimplifierFlatArray2StoreExpr<D0 : KSort, D1 : KSort, R : KSort>(
+        ctx: KContext,
+        original: KExpr<KArray2Sort<D0, D1, R>>,
+        base: KExpr<KArray2Sort<D0, D1, R>>,
+        val indices0: List<KExpr<D0>>,
+        val indices1: List<KExpr<D1>>,
+        values: List<KExpr<R>>,
+    ) : SimplifierFlatArrayStoreBaseExpr<KArray2Sort<D0, D1, R>, R>(ctx, indices0.size, original, base, values) {
+        override fun accept(transformer: KTransformerBase): KExpr<KArray2Sort<D0, D1, R>> {
+            transformer as KArrayExprSimplifier
+            return transformer.transform(this)
+        }
+
+        fun unwrap(): List<KExpr<KSort>> = buildList {
+            add(base)
+            addAll(indices0)
+            addAll(indices1)
+            addAll(values)
+        }.uncheckedCast()
+
+        fun wrap(args: List<KExpr<KSort>>) = SimplifierFlatArray2StoreExpr(
+            ctx,
+            original,
+            base = args.first().uncheckedCast(),
+            indices0 = args.subList(
+                fromIndex = 1, toIndex = 1 + numIndices
+            ).uncheckedCast(),
+            indices1 = args.subList(
+                fromIndex = 1 + numIndices, toIndex = 1 + 2 * numIndices
+            ).uncheckedCast(),
+            values = args.subList(
+                fromIndex = 1 + 2 * numIndices, toIndex = args.size
+            ).uncheckedCast()
+        )
+
+
+        override fun getStoreIndex(idx: Int): List<KExpr<*>> = listOf(indices0[idx], indices1[idx])
+
+        override fun selectValue(originalArray: KExpr<KArray2Sort<D0, D1, R>>, index: List<KExpr<*>>): KExpr<R> =
+            KArray2Select(ctx, originalArray, index.first().uncheckedCast(), index.last().uncheckedCast())
+    }
+
+    @Suppress("LongParameterList")
+    private class SimplifierFlatArray3StoreExpr<D0 : KSort, D1 : KSort, D2 : KSort, R : KSort>(
+        ctx: KContext,
+        original: KExpr<KArray3Sort<D0, D1, D2, R>>,
+        base: KExpr<KArray3Sort<D0, D1, D2, R>>,
+        val indices0: List<KExpr<D0>>,
+        val indices1: List<KExpr<D1>>,
+        val indices2: List<KExpr<D2>>,
+        values: List<KExpr<R>>,
+    ) : SimplifierFlatArrayStoreBaseExpr<KArray3Sort<D0, D1, D2, R>, R>(ctx, indices0.size, original, base, values) {
+        override fun accept(transformer: KTransformerBase): KExpr<KArray3Sort<D0, D1, D2, R>> {
             transformer as KArrayExprSimplifier
             return transformer.transform(this)
         }
+
+        fun unwrap(): List<KExpr<KSort>> = buildList {
+            add(base)
+            addAll(indices0)
+            addAll(indices1)
+            addAll(indices2)
+            addAll(values)
+        }.uncheckedCast()
+
+        @Suppress("MagicNumber")
+        fun wrap(args: List<KExpr<KSort>>) = SimplifierFlatArray3StoreExpr(
+            ctx,
+            original,
+            base = args.first().uncheckedCast(),
+            indices0 = args.subList(
+                fromIndex = 1, toIndex = 1 + numIndices
+            ).uncheckedCast(),
+            indices1 = args.subList(
+                fromIndex = 1 + numIndices, toIndex = 1 + 2 * numIndices
+            ).uncheckedCast(),
+            indices2 = args.subList(
+                fromIndex = 1 + 2 * numIndices, toIndex = 1 + 3 * numIndices
+            ).uncheckedCast(),
+            values = args.subList(
+                fromIndex = 1 + 3 * numIndices, toIndex = args.size
+            ).uncheckedCast()
+        )
+
+        override fun getStoreIndex(idx: Int): List<KExpr<*>> = listOf(indices0[idx], indices1[idx], indices2[idx])
+
+        override fun selectValue(originalArray: KExpr<KArray3Sort<D0, D1, D2, R>>, index: List<KExpr<*>>): KExpr<R> {
+            val (idx0, idx1, idx2) = index
+            return KArray3Select(
+                ctx,
+                originalArray,
+                idx0.uncheckedCast(),
+                idx1.uncheckedCast(),
+                idx2.uncheckedCast()
+            )
+        }
+    }
+
+    private class SimplifierFlatArrayNStoreExpr<R : KSort>(
+        ctx: KContext,
+        original: KExpr<KArrayNSort<R>>,
+        base: KExpr<KArrayNSort<R>>,
+        val indices: List<List<KExpr<*>>>,
+        values: List<KExpr<R>>,
+    ) : SimplifierFlatArrayStoreBaseExpr<KArrayNSort<R>, R>(ctx, indices.size, original, base, values) {
+        override fun accept(transformer: KTransformerBase): KExpr<KArrayNSort<R>> {
+            transformer as KArrayExprSimplifier
+            return transformer.transform(this)
+        }
+
+        fun unwrap(): List<KExpr<KSort>> = buildList {
+            add(base)
+            addAll(values)
+            this@SimplifierFlatArrayNStoreExpr.indices.forEach {
+                addAll(it)
+            }
+        }.uncheckedCast()
+
+        fun wrap(args: List<KExpr<KSort>>) = SimplifierFlatArrayNStoreExpr(
+            ctx, original,
+            base = args.first().uncheckedCast(),
+            values = args.subList(
+                fromIndex = 1, toIndex = 1 + numIndices
+            ).uncheckedCast(),
+            indices = args.subList(
+                fromIndex = 1 + numIndices, toIndex = args.size
+            ).chunked(numIndices)
+        )
+
+        override fun getStoreIndex(idx: Int): List<KExpr<*>> = indices[idx]
+
+        override fun selectValue(originalArray: KExpr<KArrayNSort<R>>, index: List<KExpr<*>>): KExpr<R> =
+            KArrayNSelect(ctx, originalArray, index.uncheckedCast())
     }
 
     /**
-     * Auxiliary expression to handle select with base array expanded.
+     * Auxiliary expression to handle array select.
      * @see [SimplifierAuxExpression]
      * */
-    private class SimplifierFlatArraySelectExpr<D : KSort, R : KSort>(
+    private sealed class SimplifierArraySelectBaseExpr<A : KArraySortBase<R>, R : KSort>(
         ctx: KContext,
-        val original: KExpr<KArraySort<D, R>>,
-        val baseArray: KExpr<KArraySort<D, R>>,
-        val storedIndices: List<KExpr<D>>,
-        val storedValues: List<KExpr<R>>,
-        val index: KExpr<D>,
-    ) : KApp<R, D>(ctx) {
+        val array: KExpr<A>
+    ) : KExpr<R>(ctx) {
+        override val sort: R
+            get() = array.sort.range
 
-        override val args: List<KExpr<D>> =
-            listOf(index) + storedIndices
+        override fun internEquals(other: Any): Boolean =
+            error("Interning is not used for Aux expressions")
 
-        override val sort: R
-            get() = baseArray.sort.range
+        override fun internHashCode(): Int =
+            error("Interning is not used for Aux expressions")
+
+        override fun print(printer: ExpressionPrinter) {
+            printer.append("(simplifierSelect ")
+            printer.append(array)
+            printer.append(")")
+        }
+    }
+
+    private class SimplifierArraySelectExpr<D : KSort, R : KSort>(
+        ctx: KContext,
+        array: KExpr<KArraySort<D, R>>,
+        val index: KExpr<D>,
+    ) : SimplifierArraySelectBaseExpr<KArraySort<D, R>, R>(ctx, array) {
+        override fun accept(transformer: KTransformerBase): KExpr<R> {
+            transformer as KArrayExprSimplifier
+            return transformer.transform(this)
+        }
+    }
 
-        override val decl: KDecl<R>
-            get() = ctx.mkArraySelectDecl(baseArray.sort)
+    private class SimplifierArray2SelectExpr<D0 : KSort, D1 : KSort, R : KSort>(
+        ctx: KContext,
+        array: KExpr<KArray2Sort<D0, D1, R>>,
+        val index0: KExpr<D0>,
+        val index1: KExpr<D1>
+    ) : SimplifierArraySelectBaseExpr<KArray2Sort<D0, D1, R>, R>(ctx, array) {
+        override fun accept(transformer: KTransformerBase): KExpr<R> {
+            transformer as KArrayExprSimplifier
+            return transformer.transform(this)
+        }
+    }
+
+    private class SimplifierArray3SelectExpr<D0 : KSort, D1 : KSort, D2 : KSort, R : KSort>(
+        ctx: KContext,
+        array: KExpr<KArray3Sort<D0, D1, D2, R>>,
+        val index0: KExpr<D0>,
+        val index1: KExpr<D1>,
+        val index2: KExpr<D2>,
+    ) : SimplifierArraySelectBaseExpr<KArray3Sort<D0, D1, D2, R>, R>(ctx, array) {
+        override fun accept(transformer: KTransformerBase): KExpr<R> {
+            transformer as KArrayExprSimplifier
+            return transformer.transform(this)
+        }
+    }
 
+    private class SimplifierArrayNSelectExpr<R : KSort>(
+        ctx: KContext,
+        array: KExpr<KArrayNSort<R>>,
+        val indices: List<KExpr<*>>,
+    ) : SimplifierArraySelectBaseExpr<KArrayNSort<R>, R>(ctx, array) {
         override fun accept(transformer: KTransformerBase): KExpr<R> {
             transformer as KArrayExprSimplifier
             return transformer.transform(this)
@@ -452,26 +1155,72 @@ interface KArrayExprSimplifier : KExprSimplifierBase {
     }
 
     /**
-     * Auxiliary expression to handle array select.
+     * Auxiliary expression to handle select from array store.
      * @see [SimplifierAuxExpression]
      * */
-    private class SimplifierArraySelectExpr<D : KSort, R : KSort>(
+    private sealed class SelectFromStoreExprBase<A : KArraySortBase<R>, R : KSort>(
         ctx: KContext,
-        val array: KExpr<KArraySort<D, R>>,
-        val index: KExpr<D>,
-    ) : KApp<R, KSort>(ctx) {
-        override val args: List<KExpr<KSort>> = listOf(array, index).uncheckedCast()
+        array: KArrayStoreBase<A, R>
+    ) : KExpr<R>(ctx) {
+        val storeValue: KExpr<R> = array.value
 
-        override val sort: R
-            get() = array.sort.range
+        override val sort: R = storeValue.sort
+
+        override fun print(printer: ExpressionPrinter) {
+            printer.append("(selectFromStore)")
+        }
+
+        override fun internEquals(other: Any): Boolean =
+            error("Interning is not used for Aux expressions")
+
+        override fun internHashCode(): Int =
+            error("Interning is not used for Aux expressions")
+    }
+
+    private class SelectFromStoreExpr<D : KSort, R : KSort>(
+        ctx: KContext,
+        val array: KArrayStore<D, R>,
+        val index: KExpr<D>,
+    ) : SelectFromStoreExprBase<KArraySort<D, R>, R>(ctx, array) {
+        override fun accept(transformer: KTransformerBase): KExpr<R> {
+            transformer as KArrayExprSimplifier
+            return transformer.transform(this)
+        }
+    }
 
-        override val decl: KDecl<R>
-            get() = ctx.mkArraySelectDecl(array.sort)
+    private class Select2FromStoreExpr<D0 : KSort, D1 : KSort, R : KSort>(
+        ctx: KContext,
+        val array: KArray2Store<D0, D1, R>,
+        val index0: KExpr<D0>,
+        val index1: KExpr<D1>
+    ) : SelectFromStoreExprBase<KArray2Sort<D0, D1, R>, R>(ctx, array) {
+        override fun accept(transformer: KTransformerBase): KExpr<R> {
+            transformer as KArrayExprSimplifier
+            return transformer.transform(this)
+        }
+    }
 
+    private class Select3FromStoreExpr<D0 : KSort, D1 : KSort, D2 : KSort, R : KSort>(
+        ctx: KContext,
+        val array: KArray3Store<D0, D1, D2, R>,
+        val index0: KExpr<D0>,
+        val index1: KExpr<D1>,
+        val index2: KExpr<D2>,
+    ) : SelectFromStoreExprBase<KArray3Sort<D0, D1, D2, R>, R>(ctx, array) {
         override fun accept(transformer: KTransformerBase): KExpr<R> {
             transformer as KArrayExprSimplifier
             return transformer.transform(this)
         }
     }
 
+    private class SelectNFromStoreExpr<R : KSort>(
+        ctx: KContext,
+        val array: KArrayNStore<R>,
+        val indices: List<KExpr<KSort>>,
+    ) : SelectFromStoreExprBase<KArrayNSort<R>, R>(ctx, array) {
+        override fun accept(transformer: KTransformerBase): KExpr<R> {
+            transformer as KArrayExprSimplifier
+            return transformer.transform(this)
+        }
+    }
 }
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/KExprSimplifier.kt b/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/KExprSimplifier.kt
index 5c4be2383..1cee9163b 100644
--- a/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/KExprSimplifier.kt
+++ b/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/KExprSimplifier.kt
@@ -3,7 +3,10 @@ package org.ksmt.expr.rewrite.simplify
 import org.ksmt.KContext
 import org.ksmt.decl.KDecl
 import org.ksmt.expr.KApp
+import org.ksmt.expr.KArray2Lambda
+import org.ksmt.expr.KArray3Lambda
 import org.ksmt.expr.KArrayLambda
+import org.ksmt.expr.KArrayNLambda
 import org.ksmt.expr.KDistinctExpr
 import org.ksmt.expr.KEqExpr
 import org.ksmt.expr.KExistentialQuantifier
@@ -12,7 +15,11 @@ import org.ksmt.expr.KInterpretedValue
 import org.ksmt.expr.KUniversalQuantifier
 import org.ksmt.expr.rewrite.KExprUninterpretedDeclCollector
 import org.ksmt.expr.transformer.KNonRecursiveTransformerBase
+import org.ksmt.sort.KArray2Sort
+import org.ksmt.sort.KArray3Sort
+import org.ksmt.sort.KArrayNSort
 import org.ksmt.sort.KArraySort
+import org.ksmt.sort.KArraySortBase
 import org.ksmt.sort.KBoolSort
 import org.ksmt.sort.KBvSort
 import org.ksmt.sort.KFpSort
@@ -41,7 +48,7 @@ open class KExprSimplifier(override val ctx: KContext) :
             realSort -> simplifyEqReal(lhs.uncheckedCast(), rhs.uncheckedCast())
             is KBvSort -> simplifyEqBv(lhs as KExpr<KBvSort>, rhs.uncheckedCast())
             is KFpSort -> simplifyEqFp(lhs as KExpr<KFpSort>, rhs.uncheckedCast())
-            is KArraySort<*, *> -> simplifyEqArray(lhs as KExpr<KArraySort<KSort, KSort>>, rhs.uncheckedCast())
+            is KArraySortBase<*> -> simplifyEqArray(lhs as KExpr<KArraySortBase<KSort>>, rhs.uncheckedCast())
             is KUninterpretedSort -> simplifyEqUninterpreted(lhs.uncheckedCast(), rhs.uncheckedCast())
             else -> mkEqNoSimplify(lhs, rhs)
         }
@@ -120,6 +127,24 @@ open class KExprSimplifier(override val ctx: KContext) :
         simplifyArrayLambda(expr.indexVarDecl, body)
     }
 
+    override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+        expr: KArray2Lambda<D0, D1, R>
+    ): KExpr<KArray2Sort<D0, D1, R>> = simplifyExpr(expr, expr.body) { body ->
+        simplifyArrayLambda(expr.indexVar0Decl, expr.indexVar1Decl, body)
+    }
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Lambda<D0, D1, D2, R>
+    ): KExpr<KArray3Sort<D0, D1, D2, R>> = simplifyExpr(expr, expr.body) { body ->
+        simplifyArrayLambda(expr.indexVar0Decl, expr.indexVar1Decl, expr.indexVar2Decl, body)
+    }
+
+    override fun <R : KSort> transform(
+        expr: KArrayNLambda<R>
+    ): KExpr<KArrayNSort<R>> = simplifyExpr(expr, expr.body) { body ->
+        simplifyArrayLambda(expr.indexVarDeclarations, body)
+    }
+
     override fun transform(expr: KExistentialQuantifier): KExpr<KBoolSort> =
         simplifyExpr(expr, expr.body) { body ->
             simplifyExistentialQuantifier(expr.bounds, body)
@@ -134,7 +159,7 @@ open class KExprSimplifier(override val ctx: KContext) :
         bound: KDecl<D>,
         simplifiedBody: KExpr<R>
     ): KExpr<KArraySort<D, R>> = simplifyQuantifier(
-        bounds = listOf(element = bound),
+        bounds = listOf(bound),
         simplifiedBody = simplifiedBody,
         eliminateQuantifier = { body ->
             val sort = mkArraySort(bound.sort, body.sort)
@@ -143,6 +168,45 @@ open class KExprSimplifier(override val ctx: KContext) :
         buildQuantifier = { _, body -> mkArrayLambda(bound, body) }
     )
 
+    fun <D0 : KSort, D1 : KSort, R : KSort> KContext.simplifyArrayLambda(
+        bound0: KDecl<D0>, bound1: KDecl<D1>,
+        simplifiedBody: KExpr<R>
+    ): KExpr<KArray2Sort<D0, D1, R>> = simplifyQuantifier(
+        bounds = listOf(bound0, bound1),
+        simplifiedBody = simplifiedBody,
+        eliminateQuantifier = { body ->
+            val sort = mkArraySort(bound0.sort, bound1.sort, body.sort)
+            mkArrayConst(sort, body)
+        },
+        buildQuantifier = { _, body -> mkArrayLambda(bound0, bound1, body) }
+    )
+
+    fun <D0 : KSort, D1 : KSort, D2: KSort, R : KSort> KContext.simplifyArrayLambda(
+        bound0: KDecl<D0>, bound1: KDecl<D1>, bound2: KDecl<D2>,
+        simplifiedBody: KExpr<R>
+    ): KExpr<KArray3Sort<D0, D1, D2, R>> = simplifyQuantifier(
+        bounds = listOf(bound0, bound1, bound2),
+        simplifiedBody = simplifiedBody,
+        eliminateQuantifier = { body ->
+            val sort = mkArraySort(bound0.sort, bound1.sort, bound2.sort, body.sort)
+            mkArrayConst(sort, body)
+        },
+        buildQuantifier = { _, body -> mkArrayLambda(bound0, bound1, bound2, body) }
+    )
+
+    fun <R : KSort> KContext.simplifyArrayLambda(
+        bounds: List<KDecl<*>>,
+        simplifiedBody: KExpr<R>
+    ): KExpr<KArrayNSort<R>> = simplifyQuantifier(
+        bounds = bounds,
+        simplifiedBody = simplifiedBody,
+        eliminateQuantifier = { body ->
+            val sort = mkArrayNSort(bounds.map { it.sort }, body.sort)
+            mkArrayConst(sort, body)
+        },
+        buildQuantifier = { _, body -> mkArrayNLambda(bounds, body) }
+    )
+
     fun KContext.simplifyExistentialQuantifier(
         bounds: List<KDecl<*>>,
         simplifiedBody: KExpr<KBoolSort>
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/expr/transformer/KNonRecursiveTransformer.kt b/ksmt-core/src/main/kotlin/org/ksmt/expr/transformer/KNonRecursiveTransformer.kt
index 7af4ecf67..a352d638a 100644
--- a/ksmt-core/src/main/kotlin/org/ksmt/expr/transformer/KNonRecursiveTransformer.kt
+++ b/ksmt-core/src/main/kotlin/org/ksmt/expr/transformer/KNonRecursiveTransformer.kt
@@ -4,8 +4,17 @@ import org.ksmt.KContext
 import org.ksmt.expr.KAddArithExpr
 import org.ksmt.expr.KAndExpr
 import org.ksmt.expr.KApp
+import org.ksmt.expr.KArray2Lambda
+import org.ksmt.expr.KArray2Select
+import org.ksmt.expr.KArray2Store
+import org.ksmt.expr.KArray3Lambda
+import org.ksmt.expr.KArray3Select
+import org.ksmt.expr.KArray3Store
 import org.ksmt.expr.KArrayConst
 import org.ksmt.expr.KArrayLambda
+import org.ksmt.expr.KArrayNLambda
+import org.ksmt.expr.KArrayNSelect
+import org.ksmt.expr.KArrayNStore
 import org.ksmt.expr.KArraySelect
 import org.ksmt.expr.KArrayStore
 import org.ksmt.expr.KBv2IntExpr
@@ -114,7 +123,11 @@ import org.ksmt.expr.KUnaryMinusArithExpr
 import org.ksmt.expr.KUniversalQuantifier
 import org.ksmt.expr.KXorExpr
 import org.ksmt.sort.KArithSort
+import org.ksmt.sort.KArray2Sort
+import org.ksmt.sort.KArray3Sort
+import org.ksmt.sort.KArrayNSort
 import org.ksmt.sort.KArraySort
+import org.ksmt.sort.KArraySortBase
 import org.ksmt.sort.KBoolSort
 import org.ksmt.sort.KBv1Sort
 import org.ksmt.sort.KBvSort
@@ -122,6 +135,7 @@ import org.ksmt.sort.KFpSort
 import org.ksmt.sort.KIntSort
 import org.ksmt.sort.KRealSort
 import org.ksmt.sort.KSort
+import org.ksmt.utils.uncheckedCast
 
 /**
  * Apply specialized non-recursive transformations for all KSMT expressions.
@@ -482,15 +496,99 @@ abstract class KNonRecursiveTransformer(override val ctx: KContext) : KNonRecurs
         ) { rm, value -> mkBvToFpExpr(expr.sort, rm, value, expr.signed) }
 
     // array transformers
-    override fun <D : KSort, R : KSort> transform(expr: KArrayStore<D, R>): KExpr<KArraySort<D, R>> =
-        transformExprAfterTransformedDefault(
-            expr, expr.array, expr.index, expr.value, ::transformApp, KContext::mkArrayStore
+    override fun <D : KSort, R : KSort> transform(
+        expr: KArrayStore<D, R>
+    ): KExpr<KArraySort<D, R>> = transformExprAfterTransformedDefault(
+        expr, expr.array, expr.index, expr.value, ::transformArrayStore, KContext::mkArrayStore
+    )
+
+    override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+        expr: KArray2Store<D0, D1, R>
+    ): KExpr<KArray2Sort<D0, D1, R>> = transformExprAfterTransformedDefault(
+        expr, expr.array, expr.index0, expr.index1, expr.value, ::transformArrayStore, KContext::mkArrayStore
+    )
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Store<D0, D1, D2, R>
+    ): KExpr<KArray3Sort<D0, D1, D2, R>> = transformExprAfterTransformedDefault(
+        expr, expr.array, expr.index0, expr.index1, expr.index2, expr.value,
+        ::transformArrayStore, KContext::mkArrayStore
+    )
+
+    override fun <R : KSort> transform(
+        expr: KArrayNStore<R>
+    ): KExpr<KArrayNSort<R>> = transformExprAfterTransformedDefault(
+        expr, expr.args, ::transformArrayStore
+    ) { args ->
+        mkArrayNStore(
+            array = args.first().uncheckedCast(),
+            indices = args.subList(fromIndex = 1, toIndex = args.size - 1).uncheckedCast(),
+            value = args.last().uncheckedCast()
         )
+    }
+
+    override fun <D : KSort, R : KSort> transform(
+        expr: KArraySelect<D, R>
+    ): KExpr<R> = transformExprAfterTransformedDefault(
+        expr, expr.array, expr.index, ::transformArraySelect, KContext::mkArraySelect
+    )
+
+    override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+        expr: KArray2Select<D0, D1, R>
+    ): KExpr<R> = transformExprAfterTransformedDefault(
+        expr, expr.array, expr.index0, expr.index1, ::transformArraySelect, KContext::mkArraySelect
+    )
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Select<D0, D1, D2, R>
+    ): KExpr<R> = transformExprAfterTransformedDefault(
+        expr, expr.array, expr.index0, expr.index1, expr.index2, ::transformArraySelect, KContext::mkArraySelect
+    )
+
+    override fun <R : KSort> transform(
+        expr: KArrayNSelect<R>
+    ): KExpr<R> = transformExprAfterTransformedDefault(
+        expr, expr.args, ::transformArraySelect
+    ) { args ->
+        mkArrayNSelect(
+            array = args.first().uncheckedCast(),
+            indices = args.drop(1)
+        )
+    }
+
+    override fun <D : KSort, R : KSort> transform(
+        expr: KArrayLambda<D, R>
+    ): KExpr<KArraySort<D, R>> = transformExprAfterTransformedDefault(
+        expr, expr.body, ::transformArrayLambda
+    ) { body ->
+        mkArrayLambda(expr.indexVarDecl, body)
+    }
 
-    override fun <D : KSort, R : KSort> transform(expr: KArraySelect<D, R>): KExpr<R> =
-        transformExprAfterTransformedDefault(expr, expr.array, expr.index, ::transformApp, KContext::mkArraySelect)
+    override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+        expr: KArray2Lambda<D0, D1, R>
+    ): KExpr<KArray2Sort<D0, D1, R>> = transformExprAfterTransformedDefault(
+        expr, expr.body, ::transformArrayLambda
+    ) { body ->
+        mkArrayLambda(expr.indexVar0Decl, expr.indexVar1Decl, body)
+    }
 
-    override fun <D : KSort, R : KSort> transform(expr: KArrayConst<D, R>): KExpr<KArraySort<D, R>> =
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Lambda<D0, D1, D2, R>
+    ): KExpr<KArray3Sort<D0, D1, D2, R>> = transformExprAfterTransformedDefault(
+        expr, expr.body, ::transformArrayLambda
+    ) { body ->
+        mkArrayLambda(expr.indexVar0Decl, expr.indexVar1Decl, expr.indexVar2Decl, body)
+    }
+
+    override fun <R : KSort> transform(
+        expr: KArrayNLambda<R>
+    ): KExpr<KArrayNSort<R>> = transformExprAfterTransformedDefault(
+        expr, expr.body, ::transformArrayLambda
+    ) { body ->
+        mkArrayNLambda(expr.indexVarDeclarations, body)
+    }
+
+    override fun <A : KArraySortBase<R>, R : KSort> transform(expr: KArrayConst<A, R>): KExpr<A> =
         transformExprAfterTransformedDefault(expr, expr.value, ::transformApp) { value ->
             mkArrayConst(expr.sort, value)
         }
@@ -544,12 +642,6 @@ abstract class KNonRecursiveTransformer(override val ctx: KContext) : KNonRecurs
         transformExprAfterTransformedDefault(expr, expr.arg, ::transformApp, KContext::mkRealIsInt)
 
     // quantified expressions
-    override fun <D : KSort, R : KSort> transform(
-        expr: KArrayLambda<D, R>
-    ): KExpr<KArraySort<D, R>> = transformExprAfterTransformedDefault(expr, expr.body, ::transformExpr) { body ->
-        mkArrayLambda(expr.indexVarDecl, body)
-    }
-
     override fun transform(expr: KExistentialQuantifier): KExpr<KBoolSort> =
         transformExprAfterTransformedDefault(expr, expr.body, ::transformExpr) { body ->
             mkExistentialQuantifier(body, expr.bounds)
@@ -649,7 +741,7 @@ abstract class KNonRecursiveTransformer(override val ctx: KContext) : KNonRecurs
     }
 
     /**
-     * Specialized version of [transformExprAfterTransformedDefault] for expression with 4 arguments.
+     * Specialized version of [transformExprAfterTransformedDefault] for expression with four arguments.
      * */
     @Suppress("LongParameterList", "ComplexCondition")
     private inline fun <In : KExpr<T>, Out : KExpr<T>, T : KSort, A0 : KSort, A1 : KSort, A2 : KSort, A3 : KSort>
@@ -672,4 +764,33 @@ abstract class KNonRecursiveTransformer(override val ctx: KContext) : KNonRecurs
             return transformExprDefault(transformedExpr)
         }
 
+    /**
+     * Specialized version of [transformExprAfterTransformedDefault] for expression with five arguments.
+     * */
+    @Suppress("LongParameterList", "ComplexCondition")
+    private inline fun <
+        In : KExpr<T>, Out : KExpr<T>,
+        T : KSort, A0 : KSort, A1 : KSort, A2 : KSort, A3 : KSort, A4 : KSort
+    > transformExprAfterTransformedDefault(
+        expr: In,
+        d0: KExpr<A0>,
+        d1: KExpr<A1>,
+        d2: KExpr<A2>,
+        d3: KExpr<A3>,
+        d4: KExpr<A4>,
+        ifNotTransformed: (In) -> KExpr<T>,
+        transformer: KContext.(KExpr<A0>, KExpr<A1>, KExpr<A2>, KExpr<A3>, KExpr<A4>) -> Out
+    ): KExpr<T> =
+        transformExprAfterTransformed(
+            expr, d0, d1, d2, d3, d4
+        ) { td0, td1, td2, td3, td4 ->
+            if (td0 == d0 && td1 == d1 && td2 == d2 && td3 == d3 && td4 == d4) {
+                return ifNotTransformed(expr)
+            }
+
+            val transformedExpr = ctx.transformer(td0, td1, td2, td3, td4)
+
+            return transformExprDefault(transformedExpr)
+        }
+
 }
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/expr/transformer/KNonRecursiveTransformerBase.kt b/ksmt-core/src/main/kotlin/org/ksmt/expr/transformer/KNonRecursiveTransformerBase.kt
index 341c85757..c230c2861 100644
--- a/ksmt-core/src/main/kotlin/org/ksmt/expr/transformer/KNonRecursiveTransformerBase.kt
+++ b/ksmt-core/src/main/kotlin/org/ksmt/expr/transformer/KNonRecursiveTransformerBase.kt
@@ -1,10 +1,16 @@
 package org.ksmt.expr.transformer
 
 import org.ksmt.expr.KApp
+import org.ksmt.expr.KArray2Lambda
+import org.ksmt.expr.KArray3Lambda
 import org.ksmt.expr.KArrayLambda
+import org.ksmt.expr.KArrayNLambda
 import org.ksmt.expr.KExistentialQuantifier
 import org.ksmt.expr.KExpr
 import org.ksmt.expr.KUniversalQuantifier
+import org.ksmt.sort.KArray2Sort
+import org.ksmt.sort.KArray3Sort
+import org.ksmt.sort.KArrayNSort
 import org.ksmt.sort.KArraySort
 import org.ksmt.sort.KBoolSort
 import org.ksmt.sort.KSort
@@ -60,6 +66,28 @@ abstract class KNonRecursiveTransformerBase: KTransformer {
      * */
     abstract override fun <D : KSort, R : KSort> transform(expr: KArrayLambda<D, R>): KExpr<KArraySort<D, R>>
 
+    /**
+     * Disable [KTransformer] transform KArray2Lambda implementation since it is incorrect
+     * for non-recursive usage.
+     * */
+    abstract override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+        expr: KArray2Lambda<D0, D1, R>
+    ): KExpr<KArray2Sort<D0, D1, R>>
+
+    /**
+     * Disable [KTransformer] transform KArray3Lambda implementation since it is incorrect
+     * for non-recursive usage.
+     * */
+    abstract override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Lambda<D0, D1, D2, R>
+    ): KExpr<KArray3Sort<D0, D1, D2, R>>
+
+    /**
+     * Disable [KTransformer] transform KArrayNLambda implementation since it is incorrect
+     * for non-recursive usage.
+     * */
+    abstract override fun <R : KSort> transform(expr: KArrayNLambda<R>): KExpr<KArrayNSort<R>>
+
     /**
      * Disable [KTransformer] transform KExistentialQuantifier implementation since it is incorrect
      * for non-recursive usage.
@@ -270,4 +298,40 @@ abstract class KNonRecursiveTransformerBase: KTransformer {
 
         return transformer(td0, td1, td2, td3)
     }
+
+    /**
+     * Specialized version of [transformExprAfterTransformed] for expression with five arguments.
+     * */
+    @Suppress("LongParameterList", "ComplexCondition")
+    inline fun <T : KSort, A0 : KSort, A1 : KSort, A2 : KSort, A3 : KSort, A4 : KSort> transformExprAfterTransformed(
+        expr: KExpr<T>,
+        dependency0: KExpr<A0>,
+        dependency1: KExpr<A1>,
+        dependency2: KExpr<A2>,
+        dependency3: KExpr<A3>,
+        dependency4: KExpr<A4>,
+        transformer: (KExpr<A0>, KExpr<A1>, KExpr<A2>, KExpr<A3>, KExpr<A4>) -> KExpr<T>
+    ): KExpr<T> {
+        val td0 = transformedExpr(dependency0)
+        val td1 = transformedExpr(dependency1)
+        val td2 = transformedExpr(dependency2)
+        val td3 = transformedExpr(dependency3)
+        val td4 = transformedExpr(dependency4)
+
+        if (td0 == null || td1 == null || td2 == null || td3 == null || td4 == null) {
+            retryExprTransformation(expr)
+
+            transformExprDependencyIfNeeded(dependency0, td0)
+            transformExprDependencyIfNeeded(dependency1, td1)
+            transformExprDependencyIfNeeded(dependency2, td2)
+            transformExprDependencyIfNeeded(dependency3, td3)
+            transformExprDependencyIfNeeded(dependency4, td4)
+
+            markExpressionAsNotTransformed()
+
+            return expr
+        }
+
+        return transformer(td0, td1, td2, td3, td4)
+    }
 }
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/expr/transformer/KTransformer.kt b/ksmt-core/src/main/kotlin/org/ksmt/expr/transformer/KTransformer.kt
index 2768abcfd..5829dd3ea 100644
--- a/ksmt-core/src/main/kotlin/org/ksmt/expr/transformer/KTransformer.kt
+++ b/ksmt-core/src/main/kotlin/org/ksmt/expr/transformer/KTransformer.kt
@@ -4,10 +4,22 @@ import org.ksmt.KContext
 import org.ksmt.expr.KAddArithExpr
 import org.ksmt.expr.KAndExpr
 import org.ksmt.expr.KApp
+import org.ksmt.expr.KArray2Lambda
+import org.ksmt.expr.KArray2Select
+import org.ksmt.expr.KArray2Store
+import org.ksmt.expr.KArray3Lambda
+import org.ksmt.expr.KArray3Select
+import org.ksmt.expr.KArray3Store
 import org.ksmt.expr.KArrayConst
 import org.ksmt.expr.KArrayLambda
+import org.ksmt.expr.KArrayLambdaBase
+import org.ksmt.expr.KArrayNLambda
+import org.ksmt.expr.KArrayNSelect
+import org.ksmt.expr.KArrayNStore
 import org.ksmt.expr.KArraySelect
+import org.ksmt.expr.KArraySelectBase
 import org.ksmt.expr.KArrayStore
+import org.ksmt.expr.KArrayStoreBase
 import org.ksmt.expr.KBitVec16Value
 import org.ksmt.expr.KBitVec1Value
 import org.ksmt.expr.KBitVec32Value
@@ -136,7 +148,11 @@ import org.ksmt.expr.KUnaryMinusArithExpr
 import org.ksmt.expr.KUniversalQuantifier
 import org.ksmt.expr.KXorExpr
 import org.ksmt.sort.KArithSort
+import org.ksmt.sort.KArray2Sort
+import org.ksmt.sort.KArray3Sort
+import org.ksmt.sort.KArrayNSort
 import org.ksmt.sort.KArraySort
+import org.ksmt.sort.KArraySortBase
 import org.ksmt.sort.KBoolSort
 import org.ksmt.sort.KBv16Sort
 import org.ksmt.sort.KBv1Sort
@@ -294,17 +310,73 @@ interface KTransformer : KTransformerBase {
     override fun <T : KFpSort> transform(expr: KBvToFpExpr<T>): KExpr<T> = transformApp(expr)
 
     // array transformers
-    override fun <D : KSort, R : KSort> transform(expr: KArrayStore<D, R>): KExpr<KArraySort<D, R>> = transformApp(expr)
-    override fun <D : KSort, R : KSort> transform(expr: KArraySelect<D, R>): KExpr<R> = transformApp(expr)
-    override fun <D : KSort, R : KSort> transform(expr: KArrayConst<D, R>): KExpr<KArraySort<D, R>> = transformApp(expr)
+    fun <A : KArraySortBase<R>, R : KSort> transformArrayStore(expr: KArrayStoreBase<A, R>): KExpr<A> =
+        transformApp(expr)
 
-    override fun <D : KSort, R : KSort> transform(expr: KFunctionAsArray<D, R>): KExpr<KArraySort<D, R>> =
+    override fun <D : KSort, R : KSort> transform(expr: KArrayStore<D, R>): KExpr<KArraySort<D, R>> =
+        transformArrayStore(expr)
+
+    override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+        expr: KArray2Store<D0, D1, R>
+    ): KExpr<KArray2Sort<D0, D1, R>> = transformArrayStore(expr)
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Store<D0, D1, D2, R>
+    ): KExpr<KArray3Sort<D0, D1, D2, R>> = transformArrayStore(expr)
+
+    override fun <R : KSort> transform(expr: KArrayNStore<R>): KExpr<KArrayNSort<R>> =
+        transformArrayStore(expr)
+
+    fun <A : KArraySortBase<R>, R : KSort> transformArraySelect(expr: KArraySelectBase<A, R>): KExpr<R> =
+        transformApp(expr)
+
+    override fun <D : KSort, R : KSort> transform(expr: KArraySelect<D, R>): KExpr<R> =
+        transformArraySelect(expr)
+
+    override fun <D0 : KSort, D1 : KSort, R : KSort> transform(expr: KArray2Select<D0, D1, R>): KExpr<R> =
+        transformArraySelect(expr)
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Select<D0, D1, D2, R>
+    ): KExpr<R> = transformArraySelect(expr)
+
+    override fun <R : KSort> transform(expr: KArrayNSelect<R>): KExpr<R> =
+        transformArraySelect(expr)
+
+    override fun <A : KArraySortBase<R>, R : KSort> transform(expr: KArrayConst<A, R>): KExpr<A> = transformApp(expr)
+
+    override fun <A : KArraySortBase<R>, R : KSort> transform(expr: KFunctionAsArray<A, R>): KExpr<A> =
+        transformExpr(expr)
+
+    fun <A : KArraySortBase<R>, R : KSort> transformArrayLambda(expr: KArrayLambdaBase<A, R>): KExpr<A> =
         transformExpr(expr)
 
     override fun <D : KSort, R : KSort> transform(expr: KArrayLambda<D, R>): KExpr<KArraySort<D, R>> = with(ctx) {
         val body = expr.body.accept(this@KTransformer)
-        if (body == expr.body) return transformExpr(expr)
-        return transformExpr(mkArrayLambda(expr.indexVarDecl, body))
+        if (body == expr.body) return transformArrayLambda(expr)
+        return transformArrayLambda(mkArrayLambda(expr.indexVarDecl, body))
+    }
+
+    override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+        expr: KArray2Lambda<D0, D1, R>
+    ): KExpr<KArray2Sort<D0, D1, R>> = with(ctx) {
+        val body = expr.body.accept(this@KTransformer)
+        if (body == expr.body) return transformArrayLambda(expr)
+        return transformArrayLambda(mkArrayLambda(expr.indexVar0Decl, expr.indexVar1Decl, body))
+    }
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Lambda<D0, D1, D2, R>
+    ): KExpr<KArray3Sort<D0, D1, D2, R>> = with(ctx) {
+        val body = expr.body.accept(this@KTransformer)
+        if (body == expr.body) return transformArrayLambda(expr)
+        return transformArrayLambda(mkArrayLambda(expr.indexVar0Decl, expr.indexVar1Decl, expr.indexVar2Decl, body))
+    }
+
+    override fun <R : KSort> transform(expr: KArrayNLambda<R>): KExpr<KArrayNSort<R>> = with(ctx) {
+        val body = expr.body.accept(this@KTransformer)
+        if (body == expr.body) return transformArrayLambda(expr)
+        return transformArrayLambda(mkArrayNLambda(expr.indexVarDeclarations, body))
     }
 
     // arith transformers
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/expr/transformer/KTransformerBase.kt b/ksmt-core/src/main/kotlin/org/ksmt/expr/transformer/KTransformerBase.kt
index 499d3e8a4..0cfa3e45a 100644
--- a/ksmt-core/src/main/kotlin/org/ksmt/expr/transformer/KTransformerBase.kt
+++ b/ksmt-core/src/main/kotlin/org/ksmt/expr/transformer/KTransformerBase.kt
@@ -2,8 +2,17 @@ package org.ksmt.expr.transformer
 
 import org.ksmt.expr.KAddArithExpr
 import org.ksmt.expr.KAndExpr
+import org.ksmt.expr.KArray2Lambda
+import org.ksmt.expr.KArray2Select
+import org.ksmt.expr.KArray2Store
+import org.ksmt.expr.KArray3Lambda
+import org.ksmt.expr.KArray3Select
+import org.ksmt.expr.KArray3Store
 import org.ksmt.expr.KArrayConst
 import org.ksmt.expr.KArrayLambda
+import org.ksmt.expr.KArrayNLambda
+import org.ksmt.expr.KArrayNSelect
+import org.ksmt.expr.KArrayNStore
 import org.ksmt.expr.KArraySelect
 import org.ksmt.expr.KArrayStore
 import org.ksmt.expr.KBitVec16Value
@@ -130,7 +139,11 @@ import org.ksmt.expr.KUnaryMinusArithExpr
 import org.ksmt.expr.KUniversalQuantifier
 import org.ksmt.expr.KXorExpr
 import org.ksmt.sort.KArithSort
+import org.ksmt.sort.KArray2Sort
+import org.ksmt.sort.KArray3Sort
+import org.ksmt.sort.KArrayNSort
 import org.ksmt.sort.KArraySort
+import org.ksmt.sort.KArraySortBase
 import org.ksmt.sort.KBoolSort
 import org.ksmt.sort.KBv16Sort
 import org.ksmt.sort.KBv1Sort
@@ -272,10 +285,30 @@ interface KTransformerBase {
 
     // array transformers
     fun <D : KSort, R : KSort> transform(expr: KArrayStore<D, R>): KExpr<KArraySort<D, R>>
+    fun <D0 : KSort, D1 : KSort, R : KSort> transform(expr: KArray2Store<D0, D1, R>): KExpr<KArray2Sort<D0, D1, R>>
+
+    fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Store<D0, D1, D2, R>
+    ): KExpr<KArray3Sort<D0, D1, D2, R>>
+
+    fun <R : KSort> transform(expr: KArrayNStore<R>): KExpr<KArrayNSort<R>>
+
     fun <D : KSort, R : KSort> transform(expr: KArraySelect<D, R>): KExpr<R>
-    fun <D : KSort, R : KSort> transform(expr: KArrayConst<D, R>): KExpr<KArraySort<D, R>>
-    fun <D : KSort, R : KSort> transform(expr: KFunctionAsArray<D, R>): KExpr<KArraySort<D, R>>
+    fun <D0 : KSort, D1 : KSort, R : KSort> transform(expr: KArray2Select<D0, D1, R>): KExpr<R>
+    fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(expr: KArray3Select<D0, D1, D2, R>): KExpr<R>
+    fun <R : KSort> transform(expr: KArrayNSelect<R>): KExpr<R>
+
+    fun <A : KArraySortBase<R>, R : KSort> transform(expr: KArrayConst<A, R>): KExpr<A>
+    fun <A : KArraySortBase<R>, R : KSort> transform(expr: KFunctionAsArray<A, R>): KExpr<A>
+
     fun <D : KSort, R : KSort> transform(expr: KArrayLambda<D, R>): KExpr<KArraySort<D, R>>
+    fun <D0 : KSort, D1 : KSort, R : KSort> transform(expr: KArray2Lambda<D0, D1, R>): KExpr<KArray2Sort<D0, D1, R>>
+
+    fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Lambda<D0, D1, D2, R>
+    ): KExpr<KArray3Sort<D0, D1, D2, R>>
+
+    fun <R : KSort> transform(expr: KArrayNLambda<R>): KExpr<KArrayNSort<R>>
 
     // arith transformers
     fun <T : KArithSort> transform(expr: KAddArithExpr<T>): KExpr<T>
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/solver/model/DefaultValueSampler.kt b/ksmt-core/src/main/kotlin/org/ksmt/solver/model/DefaultValueSampler.kt
index 3cb03f0d9..e2ca1b119 100644
--- a/ksmt-core/src/main/kotlin/org/ksmt/solver/model/DefaultValueSampler.kt
+++ b/ksmt-core/src/main/kotlin/org/ksmt/solver/model/DefaultValueSampler.kt
@@ -3,7 +3,11 @@ package org.ksmt.solver.model
 import org.ksmt.KContext
 import org.ksmt.expr.KExpr
 import org.ksmt.expr.KFpRoundingMode
+import org.ksmt.sort.KArray2Sort
+import org.ksmt.sort.KArray3Sort
+import org.ksmt.sort.KArrayNSort
 import org.ksmt.sort.KArraySort
+import org.ksmt.sort.KArraySortBase
 import org.ksmt.sort.KBoolSort
 import org.ksmt.sort.KBvSort
 import org.ksmt.sort.KFpRoundingModeSort
@@ -44,9 +48,20 @@ open class DefaultValueSampler<T : KSort> (
         mkFpRoundingModeExpr(defaultRm).asExpr(this@DefaultValueSampler.sort)
     }
 
-    override fun <D : KSort, R : KSort> visit(sort: KArraySort<D, R>): KExpr<T> = with(ctx) {
-        mkArrayConst(sort, sort.range.sampleValue()).asExpr(this@DefaultValueSampler.sort)
-    }
+    private fun <T : KArraySortBase<R>, R: KSort> sampleArrayValue(sort: T): KExpr<T> =
+        ctx.mkArrayConst(sort, sort.range.sampleValue())
+
+    override fun <D : KSort, R : KSort> visit(sort: KArraySort<D, R>): KExpr<T> =
+        sampleArrayValue(sort).asExpr(this@DefaultValueSampler.sort)
+
+    override fun <D0 : KSort, D1 : KSort, R : KSort> visit(sort: KArray2Sort<D0, D1, R>): KExpr<T> =
+        sampleArrayValue(sort).asExpr(this@DefaultValueSampler.sort)
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> visit(sort: KArray3Sort<D0, D1, D2, R>): KExpr<T> =
+        sampleArrayValue(sort).asExpr(this@DefaultValueSampler.sort)
+
+    override fun <R : KSort> visit(sort: KArrayNSort<R>): KExpr<T> =
+        sampleArrayValue(sort).asExpr(this@DefaultValueSampler.sort)
 
     override fun visit(sort: KUninterpretedSort): KExpr<T> =
         ctx.uninterpretedSortDefaultValue(sort).asExpr(this@DefaultValueSampler.sort)
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/solver/model/KModelEvaluator.kt b/ksmt-core/src/main/kotlin/org/ksmt/solver/model/KModelEvaluator.kt
index 5599a754b..d961aa321 100644
--- a/ksmt-core/src/main/kotlin/org/ksmt/solver/model/KModelEvaluator.kt
+++ b/ksmt-core/src/main/kotlin/org/ksmt/solver/model/KModelEvaluator.kt
@@ -2,9 +2,10 @@ package org.ksmt.solver.model
 
 import org.ksmt.KContext
 import org.ksmt.decl.KDecl
+import org.ksmt.expr.KArray2Lambda
+import org.ksmt.expr.KArray3Lambda
 import org.ksmt.expr.KArrayLambda
-import org.ksmt.expr.KArraySelect
-import org.ksmt.expr.KArrayStore
+import org.ksmt.expr.KArrayNLambda
 import org.ksmt.expr.KConst
 import org.ksmt.expr.KExistentialQuantifier
 import org.ksmt.expr.KExpr
@@ -18,7 +19,11 @@ import org.ksmt.expr.rewrite.simplify.KExprSimplifier
 import org.ksmt.expr.rewrite.simplify.simplifyExpr
 import org.ksmt.solver.KModel
 import org.ksmt.solver.model.DefaultValueSampler.Companion.sampleValue
+import org.ksmt.sort.KArray2Sort
+import org.ksmt.sort.KArray3Sort
+import org.ksmt.sort.KArrayNSort
 import org.ksmt.sort.KArraySort
+import org.ksmt.sort.KArraySortBase
 import org.ksmt.sort.KBoolSort
 import org.ksmt.sort.KSort
 import org.ksmt.sort.KUninterpretedSort
@@ -47,20 +52,29 @@ open class KModelEvaluator(
             evalFunction(expr.decl, args).also { rewrite(it) }
         }
 
-    private val rewrittenArraySelects = hashMapOf<KArraySelect<*, *>, KArraySelect<*, *>?>()
-    override fun <D : KSort, R : KSort> transform(expr: KArraySelect<D, R>): KExpr<R> {
-        val rewrittenSelect: KArraySelect<D, R>? = rewrittenArraySelects.getOrPut(expr) {
-            ctx.tryEliminateFunctionAsArray(expr)
-        }?.uncheckedCast()
+    override fun <D : KSort, R : KSort> transformSelect(array: KExpr<KArraySort<D, R>>, index: KExpr<D>): KExpr<R> =
+        super.transformSelect(tryEvalArrayConst(array), index)
 
-        return if (rewrittenSelect == null) {
-            super.transform(expr)
-        } else {
-            simplifyExpr(expr, preprocess = { rewrittenSelect })
-        }
+    override fun <D0 : KSort, D1 : KSort, R : KSort> transformSelect(
+        array: KExpr<KArray2Sort<D0, D1, R>>, index0: KExpr<D0>, index1: KExpr<D1>
+    ): KExpr<R> = super.transformSelect(tryEvalArrayConst(array), index0, index1)
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transformSelect(
+        array: KExpr<KArray3Sort<D0, D1, D2, R>>, index0: KExpr<D0>, index1: KExpr<D1>, index2: KExpr<D2>
+    ): KExpr<R> = super.transformSelect(tryEvalArrayConst(array), index0, index1, index2)
+
+    override fun <R : KSort> transformSelect(array: KExpr<KArrayNSort<R>>, indices: List<KExpr<KSort>>): KExpr<R> =
+        super.transformSelect(tryEvalArrayConst(array), indices)
+
+    // If base array is uninterpreted, try to replace it with model value
+    private fun <A : KArraySortBase<R>, R : KSort> tryEvalArrayConst(array: KExpr<A>): KExpr<A> {
+        if (array !is KConst<A>) return array
+        val interpretation = model.interpretation(array.decl) ?: return array
+        if (interpretation.entries.isNotEmpty()) return array
+        return interpretation.default ?: array
     }
 
-    override fun <D : KSort, R : KSort> transform(expr: KFunctionAsArray<D, R>): KExpr<KArraySort<D, R>> {
+    override fun <A : KArraySortBase<R>, R : KSort> transform(expr: KFunctionAsArray<A, R>): KExpr<A> {
         // No way to evaluate f when it is quantified in (as-array f)
         if (expr.function in quantifiedVars) {
             return expr
@@ -79,15 +93,38 @@ open class KModelEvaluator(
                 return@getOrPut completeModelValue(expr.sort)
             }
 
-            val idxDecl = interpretation.vars.singleOrNull()
-                ?: error("Function ${expr.function} has ${interpretation.vars} vars but used in as-array")
+            val usedDeclarations = interpretation.usedDeclarations()
+
+            // argument value is unused in function interpretation.
+            if (interpretation.vars.all { it !in usedDeclarations }) {
+                return evalArrayInterpretation(expr.sort, interpretation)
+            }
+
+            val evaluated = evalFunction(expr.function, interpretation.vars.map { ctx.mkConstApp(it) })
+
+            @Suppress("USELESS_CAST") // Exhaustive when
+            return when (expr.sort as KArraySortBase<R>) {
+                is KArraySort<*, *> -> ctx.mkArrayLambda(
+                    interpretation.vars.single(),
+                    evaluated
+                ).uncheckedCast()
+
+                is KArray2Sort<*, *, *> -> ctx.mkArrayLambda(
+                    interpretation.vars.first(),
+                    interpretation.vars.last(),
+                    evaluated
+                ).uncheckedCast()
 
-            evalArrayFunction(
-                expr.sort,
-                expr.function,
-                idxDecl.uncheckedCast(),
-                interpretation
-            )
+                is KArray3Sort<*, *, *, *> -> {
+                    val (v0, v1, v2) = interpretation.vars
+                    ctx.mkArrayLambda(v0, v1, v2, evaluated).uncheckedCast()
+                }
+
+                is KArrayNSort<*> -> ctx.mkArrayNLambda(
+                    interpretation.vars,
+                    evaluated
+                ).uncheckedCast()
+            }
         }
         return evaluatedArray.asExpr(expr.sort).also { rewrite(it) }
     }
@@ -97,6 +134,28 @@ open class KModelEvaluator(
             ctx.simplifyArrayLambda(expr.indexVarDecl, body)
         }
 
+    override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+        expr: KArray2Lambda<D0, D1, R>
+    ): KExpr<KArray2Sort<D0, D1, R>> =
+        transformQuantifiedExpression(setOf(expr.indexVar0Decl, expr.indexVar1Decl), expr.body) { body ->
+            ctx.simplifyArrayLambda(expr.indexVar0Decl, expr.indexVar1Decl, body)
+        }
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Lambda<D0, D1, D2, R>
+    ): KExpr<KArray3Sort<D0, D1, D2, R>> =
+        transformQuantifiedExpression(
+            setOf(expr.indexVar0Decl, expr.indexVar1Decl, expr.indexVar2Decl),
+            expr.body
+        ) { body ->
+            ctx.simplifyArrayLambda(expr.indexVar0Decl, expr.indexVar1Decl, expr.indexVar2Decl, body)
+        }
+
+    override fun <R : KSort> transform(expr: KArrayNLambda<R>): KExpr<KArrayNSort<R>> =
+        transformQuantifiedExpression(expr.indexVarDeclarations.toSet(), expr.body) { body ->
+            ctx.simplifyArrayLambda(expr.indexVarDeclarations, body)
+        }
+
     override fun transform(expr: KExistentialQuantifier): KExpr<KBoolSort> =
         transformQuantifiedExpression(expr.bounds.toSet(), expr.body) { body ->
             ctx.simplifyExistentialQuantifier(expr.bounds, body)
@@ -107,7 +166,7 @@ open class KModelEvaluator(
             ctx.simplifyUniversalQuantifier(expr.bounds, body)
         }
 
-    private inline fun <B : KSort, T: KSort> transformQuantifiedExpression(
+    private inline fun <B : KSort, T : KSort> transformQuantifiedExpression(
         quantifiedVars: Set<KDecl<*>>,
         body: KExpr<B>,
         crossinline quantifierBuilder: (KExpr<B>) -> KExpr<T>
@@ -143,34 +202,45 @@ open class KModelEvaluator(
         return expr in sortUniverse
     }
 
-    private fun <D : KSort, R : KSort> evalArrayFunction(
-        sort: KArraySort<D, R>,
-        function: KDecl<R>,
-        indexVar: KDecl<D>,
+    @Suppress("USELESS_CAST") // Exhaustive when
+    private fun <A : KArraySortBase<R>, R : KSort> evalArrayInterpretation(
+        sort: A,
         interpretation: KModel.KFuncInterp<R>
-    ): KExpr<KArraySort<D, R>> {
-        val usedDeclarations = interpretation.usedDeclarations()
+    ): KExpr<A> = when (sort as KArraySortBase<R>) {
+        is KArraySort<*, R> -> sort.evalArrayInterpretation(
+            interpretation
+        ) { array: KExpr<KArraySort<KSort, R>>, args, value ->
+            mkArrayStore(array, args.single(), value)
+        }
+
+        is KArray2Sort<*, *, *> -> sort.evalArrayInterpretation(
+            interpretation
+        ) { array: KExpr<KArray2Sort<KSort, KSort, R>>, (idx0, idx1), value ->
+            mkArrayStore(array, idx0, idx1, value)
+        }
 
-        // argument value is unused in function interpretation.
-        if (indexVar !in usedDeclarations) {
-            return evalArrayInterpretation(sort, interpretation)
+        is KArray3Sort<*, *, *, *> -> sort.evalArrayInterpretation(
+            interpretation
+        ) { array: KExpr<KArray3Sort<KSort, KSort, KSort, R>>, (idx0, idx1, idx2), value ->
+            mkArrayStore(array, idx0, idx1, idx2, value)
         }
 
-        val index = ctx.mkConstApp(indexVar)
-        val evaluated = evalFunction(function, listOf(index))
-        return ctx.mkArrayLambda(index.decl, evaluated)
+        is KArrayNSort<*> -> sort.evalArrayInterpretation(
+            interpretation
+        ) { array: KExpr<KArrayNSort<R>>, args, value ->
+            mkArrayNStore(array, args, value)
+        }
     }
 
-    private fun <D : KSort, R : KSort> evalArrayInterpretation(
-        sort: KArraySort<D, R>,
-        interpretation: KModel.KFuncInterp<R>
-    ): KExpr<KArraySort<D, R>> = with(ctx) {
-        val defaultValue = interpretation.default ?: completeModelValue(sort.range)
-        val defaultArray: KExpr<KArraySort<D, R>> = mkArrayConst(sort, defaultValue)
+    private inline fun <A : KArraySortBase<R>, R : KSort, reified S : KArraySortBase<R>> A.evalArrayInterpretation(
+        interpretation: KModel.KFuncInterp<R>,
+        mkEntryStore: KContext.(KExpr<S>, List<KExpr<KSort>>, KExpr<R>) -> KExpr<S>
+    ): KExpr<A> = with(ctx) {
+        val defaultValue = interpretation.default ?: completeModelValue(range)
+        val defaultArray: KExpr<A> = mkArrayConst(this@evalArrayInterpretation, defaultValue)
 
         interpretation.entries.foldRight(defaultArray) { entry, acc ->
-            val idx = entry.args.single().asExpr(sort.domain)
-            acc.store(idx, entry.value)
+            mkEntryStore(acc.uncheckedCast(), entry.args.uncheckedCast(), entry.value).uncheckedCast()
         }
     }
 
@@ -290,47 +360,6 @@ open class KModelEvaluator(
         )
     }
 
-    /**
-     * Usually, [KFunctionAsArray] will be expanded into large array store chain.
-     * In case of array select, we can avoid such expansion and replace
-     * (select (as-array f) i) with (f i).
-     * */
-    private fun <D : KSort, R : KSort> KContext.tryEliminateFunctionAsArray(
-        expr: KArraySelect<D, R>
-    ): KArraySelect<D, R>? {
-        // Unroll stores until we find some base array
-        val parentStores = arrayListOf<KArrayStore<D, R>>()
-        var base = expr.array
-        while (base is KArrayStore<D, R>) {
-            parentStores += base
-            base = base.array
-        }
-
-        // If base array in uninterpreted, try to replace it with model value
-        if (base is KConst<KArraySort<D, R>>) {
-            val interpretation = model.interpretation(base.decl) ?: return null
-            if (interpretation.entries.isNotEmpty()) return null
-            base = interpretation.default ?: return null
-        }
-
-        if (base !is KFunctionAsArray<D, R>) return null
-
-        /**
-         * Replace as-array with (const (f i)) since:
-         * 1. we may have parent stores here and we need an array expression
-         * 2. (select (const (f i)) i) ==> (f i)
-         * */
-        val defaultSelectValue = base.function.apply(listOf(expr.index))
-        var newArrayBase: KExpr<KArraySort<D, R>> = mkArrayConst(base.sort, defaultSelectValue)
-
-        // Rebuild array
-        for (store in parentStores.asReversed()) {
-            newArrayBase = newArrayBase.store(store.index, store.value)
-        }
-
-        return mkArraySelectNoSimplify(newArrayBase, expr.index)
-    }
-
     private fun <T : KSort> completeModelValue(sort: T): KExpr<T> {
         val value = when (sort) {
             is KUninterpretedSort ->
@@ -338,9 +367,9 @@ open class KModelEvaluator(
                     ?.randomOrNull()
                     ?: sort.sampleValue()
 
-            is KArraySort<*, *> -> {
+            is KArraySortBase<*> -> {
                 val arrayValue = completeModelValue(sort.range)
-                ctx.mkArrayConst(sort, arrayValue)
+                ctx.mkArrayConst(sort.uncheckedCast(), arrayValue)
             }
 
             else -> sort.sampleValue()
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/sort/KSort.kt b/ksmt-core/src/main/kotlin/org/ksmt/sort/KSort.kt
index 511e90740..e336dd2b9 100644
--- a/ksmt-core/src/main/kotlin/org/ksmt/sort/KSort.kt
+++ b/ksmt-core/src/main/kotlin/org/ksmt/sort/KSort.kt
@@ -46,23 +46,102 @@ class KRealSort internal constructor(ctx: KContext) : KArithSort(ctx) {
     override fun equals(other: Any?): Boolean = this === other || other is KRealSort
 }
 
-class KArraySort<out D : KSort, out R : KSort> internal constructor(
-    ctx: KContext, val domain: D, val range: R
-) : KSort(ctx) {
-    override fun <T> accept(visitor: KSortVisitor<T>): T = visitor.visit(this)
+sealed class KArraySortBase<R : KSort>(ctx: KContext) : KSort(ctx) {
+    abstract val domainSorts: List<KSort>
+    abstract val range: R
 
     override fun print(builder: StringBuilder): Unit = with(builder) {
         append("(Array ")
-        domain.print(this)
-        append(' ')
+        domainSorts.forEach {
+            append(it)
+            append(' ')
+        }
         range.print(this)
         append(')')
     }
+}
+
+class KArraySort<D : KSort, R : KSort> internal constructor(
+    ctx: KContext, val domain: D, override val range: R
+) : KArraySortBase<R>(ctx) {
+
+    override val domainSorts: List<KSort>
+        get() = listOf(domain)
+
+    override fun <T> accept(visitor: KSortVisitor<T>): T = visitor.visit(this)
 
     override fun hashCode(): Int = hash(javaClass, domain, range)
 
     override fun equals(other: Any?): Boolean =
         this === other || (other is KArraySort<*, *> && domain == other.domain && range == other.range)
+
+    companion object {
+        const val DOMAIN_SIZE = 1
+    }
+}
+
+class KArray2Sort<D0 : KSort, D1 : KSort, R : KSort> internal constructor(
+    ctx: KContext, val domain0: D0, val domain1: D1, override val range: R
+) : KArraySortBase<R>(ctx) {
+
+    override val domainSorts: List<KSort>
+        get() = listOf(domain0, domain1)
+
+    override fun <T> accept(visitor: KSortVisitor<T>): T = visitor.visit(this)
+
+    override fun hashCode(): Int = hash(javaClass, domain0, domain1, range)
+
+    override fun equals(other: Any?): Boolean {
+        if (this === other) return true
+        if (other !is KArray2Sort<*, *, *>) return false
+        return domain0 == other.domain0 && domain1 == other.domain1 && range == other.range
+    }
+
+    companion object {
+        const val DOMAIN_SIZE = 2
+    }
+}
+
+class KArray3Sort<D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> internal constructor(
+    ctx: KContext, val domain0: D0, val domain1: D1, val domain2: D2, override val range: R
+) : KArraySortBase<R>(ctx) {
+
+    override val domainSorts: List<KSort>
+        get() = listOf(domain0, domain1, domain2)
+
+    override fun <T> accept(visitor: KSortVisitor<T>): T = visitor.visit(this)
+
+    override fun hashCode(): Int = hash(javaClass, domain0, domain1, domain2, range)
+
+    override fun equals(other: Any?): Boolean {
+        if (this === other) return true
+        if (other !is KArray3Sort<*, *, *, *>) return false
+        return domain0 == other.domain0 && domain1 == other.domain1 && domain2 == other.domain2 && range == other.range
+    }
+
+    companion object {
+        const val DOMAIN_SIZE = 3
+    }
+}
+
+class KArrayNSort<R : KSort> internal constructor(
+    ctx: KContext, override val domainSorts: List<KSort>, override val range: R
+) : KArraySortBase<R>(ctx) {
+    init {
+        require(domainSorts.size > KArray3Sort.DOMAIN_SIZE) {
+            "Use specialized Array with domain size ${domainSorts.size}"
+        }
+    }
+
+    override fun <T> accept(visitor: KSortVisitor<T>): T = visitor.visit(this)
+
+    override fun hashCode(): Int = hash(javaClass, domainSorts, range)
+
+    override fun equals(other: Any?): Boolean {
+        if (this === other) return true
+        if (other !is KArrayNSort<*>) return false
+        return domainSorts == other.domainSorts && range == other.range
+    }
 }
 
 abstract class KBvSort(ctx: KContext) : KSort(ctx) {
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/sort/KSortVisitor.kt b/ksmt-core/src/main/kotlin/org/ksmt/sort/KSortVisitor.kt
index f1cec4587..5639148d8 100644
--- a/ksmt-core/src/main/kotlin/org/ksmt/sort/KSortVisitor.kt
+++ b/ksmt-core/src/main/kotlin/org/ksmt/sort/KSortVisitor.kt
@@ -8,6 +8,9 @@ interface KSortVisitor<T> {
     fun <S : KBvSort> visit(sort: S): T
     fun <S : KFpSort> visit(sort: S): T
     fun <D : KSort, R : KSort> visit(sort: KArraySort<D, R>): T
+    fun <D0 : KSort, D1 : KSort, R : KSort> visit(sort: KArray2Sort<D0, D1, R>): T
+    fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> visit(sort: KArray3Sort<D0, D1, D2, R>): T
+    fun <R : KSort> visit(sort: KArrayNSort<R>): T
     fun visit(sort: KFpRoundingModeSort): T
     fun visit(sort: KUninterpretedSort): T
 }
diff --git a/ksmt-core/src/test/kotlin/org/ksmt/ModelEvaluationTest.kt b/ksmt-core/src/test/kotlin/org/ksmt/ModelEvaluationTest.kt
index 2c9cfe686..457ccd6bb 100644
--- a/ksmt-core/src/test/kotlin/org/ksmt/ModelEvaluationTest.kt
+++ b/ksmt-core/src/test/kotlin/org/ksmt/ModelEvaluationTest.kt
@@ -3,7 +3,6 @@ package org.ksmt
 import org.ksmt.solver.KModel
 import org.ksmt.solver.model.DefaultValueSampler.Companion.sampleValue
 import org.ksmt.solver.model.KModelImpl
-import org.ksmt.sort.KBv32Sort
 import org.ksmt.utils.getValue
 import kotlin.test.Test
 import kotlin.test.assertEquals
@@ -62,7 +61,7 @@ class ModelEvaluationTest {
             default = null
         )
 
-        val arrayInterp = mkFunctionAsArray<KBv32Sort, KBv32Sort>(tmpDecl)
+        val arrayInterp = mkFunctionAsArray(arraySort, tmpDecl)
 
 
         val model = KModelImpl(
@@ -121,8 +120,8 @@ class ModelEvaluationTest {
             default = null
         )
 
-        val array1Interp = mkFunctionAsArray<KBv32Sort, KBv32Sort>(tmpDecl1)
-        val array2Interp = mkFunctionAsArray<KBv32Sort, KBv32Sort>(tmpDecl2)
+        val array1Interp = mkFunctionAsArray(arraySort, tmpDecl1)
+        val array2Interp = mkFunctionAsArray(arraySort, tmpDecl2)
 
 
         val model = KModelImpl(
diff --git a/ksmt-runner/src/main/kotlin/org/ksmt/runner/serializer/AstDeserializer.kt b/ksmt-runner/src/main/kotlin/org/ksmt/runner/serializer/AstDeserializer.kt
index 14477943d..dbff73864 100644
--- a/ksmt-runner/src/main/kotlin/org/ksmt/runner/serializer/AstDeserializer.kt
+++ b/ksmt-runner/src/main/kotlin/org/ksmt/runner/serializer/AstDeserializer.kt
@@ -9,10 +9,12 @@ import org.ksmt.expr.KExpr
 import org.ksmt.expr.KIntNumExpr
 import org.ksmt.sort.KArithSort
 import org.ksmt.sort.KArraySort
+import org.ksmt.sort.KArraySortBase
 import org.ksmt.sort.KBoolSort
 import org.ksmt.sort.KFpSort
 import org.ksmt.sort.KIntSort
 import org.ksmt.sort.KSort
+import org.ksmt.utils.uncheckedCast
 
 @OptIn(ExperimentalUnsignedTypes::class)
 class AstDeserializer(
@@ -86,6 +88,9 @@ class AstDeserializer(
             SortKind.Bv -> mkBvSort(readUInt())
             SortKind.Fp -> mkFpSort(readUInt(), readUInt())
             SortKind.Array -> mkArraySort(readSort(), readSort())
+            SortKind.Array2 -> mkArraySort(readSort(), readSort(), readSort())
+            SortKind.Array3 -> mkArraySort(readSort(), readSort(), readSort(), readSort())
+            SortKind.ArrayN -> mkArraySort(readAstArray().uncheckedCast(), readSort())
             SortKind.Uninterpreted -> mkUninterpretedSort(readString())
         }
     }
@@ -201,11 +206,47 @@ class AstDeserializer(
             ExprKind.FpToFpExpr -> mkFpToFpExprNoSimplify(readSort() as KFpSort, readExpr(), readExpr())
             ExprKind.RealToFpExpr -> mkRealToFpExprNoSimplify(readSort() as KFpSort, readExpr(), readExpr())
             ExprKind.BvToFpExpr -> mkBvToFpExprNoSimplify(readSort() as KFpSort, readExpr(), readExpr(), readBoolean())
-            ExprKind.ArrayStore -> deserialize(::mkArrayStoreNoSimplify)
-            ExprKind.ArraySelect -> deserialize(::mkArraySelectNoSimplify)
+            ExprKind.ArrayStore -> mkArrayStoreNoSimplify(
+                readExpr(), readExpr(), readExpr()
+            )
+            ExprKind.Array2Store -> mkArrayStoreNoSimplify(
+                readExpr(), readExpr(), readExpr(), readExpr()
+            )
+            ExprKind.Array3Store -> mkArrayStoreNoSimplify(
+                readExpr(), readExpr(), readExpr(), readExpr(), readExpr()
+            )
+            ExprKind.ArrayNStore -> mkArrayNStoreNoSimplify(
+                readExpr(), readAstArray() as List<KExpr<KSort>>, readExpr()
+            )
+            ExprKind.ArraySelect -> mkArraySelectNoSimplify(
+                readExpr(), readExpr()
+            )
+            ExprKind.Array2Select -> mkArraySelectNoSimplify(
+                readExpr(), readExpr(), readExpr()
+            )
+            ExprKind.Array3Select -> mkArraySelectNoSimplify(
+                readExpr(), readExpr(), readExpr(), readExpr()
+            )
+            ExprKind.ArrayNSelect -> mkArrayNSelectNoSimplify(
+                readExpr(), readAstArray() as List<KExpr<KSort>>
+            )
             ExprKind.ArrayConst -> mkArrayConst(readSort() as KArraySort<KSort, KSort>, readExpr())
-            ExprKind.FunctionAsArray -> mkFunctionAsArray<KSort, KSort>(readDecl() as KFuncDecl<KSort>)
-            ExprKind.ArrayLambda -> mkArrayLambda(readDecl(), readExpr())
+            ExprKind.FunctionAsArray -> mkFunctionAsArray(
+                readSort() as KArraySortBase<KSort>,
+                readDecl() as KFuncDecl<KSort>
+            )
+            ExprKind.ArrayLambda -> mkArrayLambda(
+                readDecl(), readExpr()
+            )
+            ExprKind.Array2Lambda -> mkArrayLambda(
+                readDecl(), readDecl(), readExpr()
+            )
+            ExprKind.Array3Lambda -> mkArrayLambda(
+                readDecl(), readDecl(), readDecl(), readExpr()
+            )
+            ExprKind.ArrayNLambda -> mkArrayNLambda(
+                readAstArray() as List<KDecl<KSort>>, readExpr()
+            )
             ExprKind.AddArithExpr -> mkArithAddNoSimplify(readAstArray() as List<KExpr<KArithSort>>)
             ExprKind.MulArithExpr -> mkArithMulNoSimplify(readAstArray() as List<KExpr<KArithSort>>)
             ExprKind.SubArithExpr -> mkArithSubNoSimplify(readAstArray() as List<KExpr<KArithSort>>)
diff --git a/ksmt-runner/src/main/kotlin/org/ksmt/runner/serializer/AstSerializer.kt b/ksmt-runner/src/main/kotlin/org/ksmt/runner/serializer/AstSerializer.kt
index 2c651994e..889b96889 100644
--- a/ksmt-runner/src/main/kotlin/org/ksmt/runner/serializer/AstSerializer.kt
+++ b/ksmt-runner/src/main/kotlin/org/ksmt/runner/serializer/AstSerializer.kt
@@ -8,8 +8,17 @@ import org.ksmt.decl.KDeclVisitor
 import org.ksmt.decl.KFuncDecl
 import org.ksmt.expr.KAddArithExpr
 import org.ksmt.expr.KAndExpr
+import org.ksmt.expr.KArray2Lambda
+import org.ksmt.expr.KArray2Select
+import org.ksmt.expr.KArray2Store
+import org.ksmt.expr.KArray3Lambda
+import org.ksmt.expr.KArray3Select
+import org.ksmt.expr.KArray3Store
 import org.ksmt.expr.KArrayConst
 import org.ksmt.expr.KArrayLambda
+import org.ksmt.expr.KArrayNLambda
+import org.ksmt.expr.KArrayNSelect
+import org.ksmt.expr.KArrayNStore
 import org.ksmt.expr.KArraySelect
 import org.ksmt.expr.KArrayStore
 import org.ksmt.expr.KBitVec16Value
@@ -137,7 +146,11 @@ import org.ksmt.expr.KUniversalQuantifier
 import org.ksmt.expr.KXorExpr
 import org.ksmt.solver.util.KExprInternalizerBase
 import org.ksmt.sort.KArithSort
+import org.ksmt.sort.KArray2Sort
+import org.ksmt.sort.KArray3Sort
+import org.ksmt.sort.KArrayNSort
 import org.ksmt.sort.KArraySort
+import org.ksmt.sort.KArraySortBase
 import org.ksmt.sort.KBoolSort
 import org.ksmt.sort.KBvSort
 import org.ksmt.sort.KFp128Sort
@@ -152,7 +165,7 @@ import org.ksmt.sort.KSort
 import org.ksmt.sort.KSortVisitor
 import org.ksmt.sort.KUninterpretedSort
 
-@Suppress("ArrayPrimitive")
+@Suppress("ArrayPrimitive", "LargeClass")
 @OptIn(ExperimentalUnsignedTypes::class)
 class AstSerializer(
     private val serializationCtx: AstSerializationCtx,
@@ -223,6 +236,39 @@ class AstSerializer(
             }
         }
 
+        override fun <D0 : KSort, D1 : KSort, R : KSort> visit(sort: KArray2Sort<D0, D1, R>): Int {
+            val domain0 = sort.domain0.serializeSort()
+            val domain1 = sort.domain1.serializeSort()
+            val range = sort.range.serializeSort()
+            return serializeSort(sort, SortKind.Array2) {
+                writeAst(domain0)
+                writeAst(domain1)
+                writeAst(range)
+            }
+        }
+
+        override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> visit(sort: KArray3Sort<D0, D1, D2, R>): Int {
+            val domain0 = sort.domain0.serializeSort()
+            val domain1 = sort.domain1.serializeSort()
+            val domain2 = sort.domain2.serializeSort()
+            val range = sort.range.serializeSort()
+            return serializeSort(sort, SortKind.Array3) {
+                writeAst(domain0)
+                writeAst(domain1)
+                writeAst(domain2)
+                writeAst(range)
+            }
+        }
+
+        override fun <R : KSort> visit(sort: KArrayNSort<R>): Int {
+            val domain = sort.domainSorts.map { it.serializeSort() }
+            val range = sort.range.serializeSort()
+            return serializeSort(sort, SortKind.ArrayN) {
+                writeAstArray(domain)
+                writeAst(range)
+            }
+        }
+
         override fun visit(sort: KFpRoundingModeSort): Int = serializeSort(sort, SortKind.FpRM) {}
 
         override fun visit(sort: KUninterpretedSort): Int = serializeSort(sort, SortKind.Uninterpreted) {
@@ -810,11 +856,82 @@ class AstSerializer(
         serialize(array, index, value)
     }
 
+    override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+        expr: KArray2Store<D0, D1, R>
+    ): KExpr<KArray2Sort<D0, D1, R>> = with(expr) {
+        transform(array, index0, index1, value) { a: Int, i0: Int, i1: Int, v: Int ->
+            writeExpr {
+                writeAst(a)
+                writeAst(i0)
+                writeAst(i1)
+                writeAst(v)
+            }
+        }
+    }
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Store<D0, D1, D2, R>
+    ): KExpr<KArray3Sort<D0, D1, D2, R>> = with(expr) {
+        transformList(listOf(array, index0, index1, index2, value)) { args: Array<Int> ->
+            val (a: Int, i0: Int, i1: Int, i2: Int, v: Int) = args
+            writeExpr {
+                writeAst(a)
+                writeAst(i0)
+                writeAst(i1)
+                writeAst(i2)
+                writeAst(v)
+            }
+        }
+    }
+
+    override fun <R : KSort> transform(expr: KArrayNStore<R>): KExpr<KArrayNSort<R>> = with(expr) {
+        transformList(indices + listOf(array, value)) { args: Array<Int> ->
+            val array = args[args.lastIndex - 1]
+            val value = args[args.lastIndex]
+            val indices = args.dropLast(2)
+            writeExpr {
+                writeAst(array)
+                writeAstArray(indices)
+                writeAst(value)
+            }
+        }
+    }
+
     override fun <D : KSort, R : KSort> transform(expr: KArraySelect<D, R>) = with(expr) {
         serialize(array, index)
     }
 
-    override fun <D : KSort, R : KSort> transform(expr: KArrayConst<D, R>) = with(expr) {
+    override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+        expr: KArray2Select<D0, D1, R>
+    ): KExpr<R> = with(expr) {
+        serialize(array, index0, index1)
+    }
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Select<D0, D1, D2, R>
+    ): KExpr<R> = with(expr) {
+        transform(array, index0, index1, index2) { a: Int, i0: Int, i1: Int, i2: Int ->
+            writeExpr {
+                writeAst(a)
+                writeAst(i0)
+                writeAst(i1)
+                writeAst(i2)
+            }
+        }
+    }
+
+    override fun <R : KSort> transform(expr: KArrayNSelect<R>): KExpr<R> = with(expr) {
+        transformList(indices + array) { args: Array<Int> ->
+            val array = args.last()
+            val indices = args.dropLast(1)
+            writeExpr {
+                writeAst(array)
+                writeAstArray(indices)
+            }
+        }
+    }
+
+    override fun <A: KArraySortBase<R>, R : KSort> transform(expr: KArrayConst<A, R>) = with(expr) {
         transform(value) { value: Int ->
             val sortIdx = sort.serializeSort()
             writeExpr {
@@ -826,9 +943,49 @@ class AstSerializer(
 
     override fun <D : KSort, R : KSort> transform(expr: KArrayLambda<D, R>) = with(expr) {
         transform(body) { body: Int ->
-            val internalizedIndex = indexVarDecl.serializeDecl()
+            val serializedIndex = indexVarDecl.serializeDecl()
+            writeExpr {
+                writeAst(serializedIndex)
+                writeAst(body)
+            }
+        }
+    }
+
+    override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+        expr: KArray2Lambda<D0, D1, R>
+    ): KExpr<KArray2Sort<D0, D1, R>> = with(expr) {
+        transform(body) { body: Int ->
+            val serializedIndex0 = indexVar0Decl.serializeDecl()
+            val serializedIndex1 = indexVar1Decl.serializeDecl()
             writeExpr {
-                writeAst(internalizedIndex)
+                writeAst(serializedIndex0)
+                writeAst(serializedIndex1)
+                writeAst(body)
+            }
+        }
+    }
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Lambda<D0, D1, D2, R>
+    ): KExpr<KArray3Sort<D0, D1, D2, R>> = with(expr) {
+        transform(body) { body: Int ->
+            val serializedIndex0 = indexVar0Decl.serializeDecl()
+            val serializedIndex1 = indexVar1Decl.serializeDecl()
+            val serializedIndex2 = indexVar2Decl.serializeDecl()
+            writeExpr {
+                writeAst(serializedIndex0)
+                writeAst(serializedIndex1)
+                writeAst(serializedIndex2)
+                writeAst(body)
+            }
+        }
+    }
+
+    override fun <R : KSort> transform(expr: KArrayNLambda<R>): KExpr<KArrayNSort<R>> = with(expr) {
+        transform(body) { body: Int ->
+            val serializedIndices = indexVarDeclarations.map { it.serializeDecl() }
+            writeExpr {
+                writeAstArray(serializedIndices)
                 writeAst(body)
             }
         }
@@ -920,10 +1077,12 @@ class AstSerializer(
         }
     }
 
-    override fun <D : KSort, R : KSort> transform(expr: KFunctionAsArray<D, R>) = with(expr) {
+    override fun <A: KArraySortBase<R>, R : KSort> transform(expr: KFunctionAsArray<A, R>) = with(expr) {
         transform {
+            val sortIdx = sort.serializeSort()
             val funcIdx = function.serializeDecl()
             writeExpr {
+                writeAst(sortIdx)
                 writeAst(funcIdx)
             }
         }
diff --git a/ksmt-runner/src/main/kotlin/org/ksmt/runner/serializer/ExprKind.kt b/ksmt-runner/src/main/kotlin/org/ksmt/runner/serializer/ExprKind.kt
index 0e7981f25..b1b7764a8 100644
--- a/ksmt-runner/src/main/kotlin/org/ksmt/runner/serializer/ExprKind.kt
+++ b/ksmt-runner/src/main/kotlin/org/ksmt/runner/serializer/ExprKind.kt
@@ -104,10 +104,19 @@ enum class ExprKind {
     RealToFpExpr,
     BvToFpExpr,
     ArrayStore,
+    Array2Store,
+    Array3Store,
+    ArrayNStore,
     ArraySelect,
+    Array2Select,
+    Array3Select,
+    ArrayNSelect,
     ArrayConst,
     FunctionAsArray,
     ArrayLambda,
+    Array2Lambda,
+    Array3Lambda,
+    ArrayNLambda,
     AddArithExpr,
     MulArithExpr,
     SubArithExpr,
diff --git a/ksmt-runner/src/main/kotlin/org/ksmt/runner/serializer/ExprKindMapper.kt b/ksmt-runner/src/main/kotlin/org/ksmt/runner/serializer/ExprKindMapper.kt
index b1e7a6e4c..e1bb844be 100644
--- a/ksmt-runner/src/main/kotlin/org/ksmt/runner/serializer/ExprKindMapper.kt
+++ b/ksmt-runner/src/main/kotlin/org/ksmt/runner/serializer/ExprKindMapper.kt
@@ -2,8 +2,17 @@ package org.ksmt.runner.serializer
 
 import org.ksmt.expr.KAddArithExpr
 import org.ksmt.expr.KAndExpr
+import org.ksmt.expr.KArray2Lambda
+import org.ksmt.expr.KArray2Select
+import org.ksmt.expr.KArray2Store
+import org.ksmt.expr.KArray3Lambda
+import org.ksmt.expr.KArray3Select
+import org.ksmt.expr.KArray3Store
 import org.ksmt.expr.KArrayConst
 import org.ksmt.expr.KArrayLambda
+import org.ksmt.expr.KArrayNLambda
+import org.ksmt.expr.KArrayNSelect
+import org.ksmt.expr.KArrayNStore
 import org.ksmt.expr.KArraySelect
 import org.ksmt.expr.KArrayStore
 import org.ksmt.expr.KBitVec16Value
@@ -131,7 +140,11 @@ import org.ksmt.expr.KUniversalQuantifier
 import org.ksmt.expr.KXorExpr
 import org.ksmt.expr.transformer.KTransformerBase
 import org.ksmt.sort.KArithSort
+import org.ksmt.sort.KArray2Sort
+import org.ksmt.sort.KArray3Sort
+import org.ksmt.sort.KArrayNSort
 import org.ksmt.sort.KArraySort
+import org.ksmt.sort.KArraySortBase
 import org.ksmt.sort.KBoolSort
 import org.ksmt.sort.KBv16Sort
 import org.ksmt.sort.KBv1Sort
@@ -502,21 +515,49 @@ class ExprKindMapper: KTransformerBase {
     override fun <D : KSort, R : KSort> transform(expr: KArrayStore<D, R>): KExpr<KArraySort<D, R>> =
         expr.kind(ExprKind.ArrayStore)
 
+    override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+        expr: KArray2Store<D0, D1, R>
+    ): KExpr<KArray2Sort<D0, D1, R>> = expr.kind(ExprKind.Array2Store)
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Store<D0, D1, D2, R>
+    ): KExpr<KArray3Sort<D0, D1, D2, R>> = expr.kind(ExprKind.Array3Store)
+
+    override fun <R : KSort> transform(expr: KArrayNStore<R>): KExpr<KArrayNSort<R>> =
+        expr.kind(ExprKind.ArrayNStore)
 
     override fun <D : KSort, R : KSort> transform(expr: KArraySelect<D, R>): KExpr<R> = expr.kind(ExprKind.ArraySelect)
 
+    override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+        expr: KArray2Select<D0, D1, R>
+    ): KExpr<R> = expr.kind(ExprKind.Array2Select)
 
-    override fun <D : KSort, R : KSort> transform(expr: KArrayConst<D, R>): KExpr<KArraySort<D, R>> =
-        expr.kind(ExprKind.ArrayConst)
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Select<D0, D1, D2, R>
+    ): KExpr<R> = expr.kind(ExprKind.Array3Select)
+
+    override fun <R : KSort> transform(expr: KArrayNSelect<R>): KExpr<R> = expr.kind(ExprKind.ArrayNSelect)
 
+    override fun <A : KArraySortBase<R>, R : KSort> transform(expr: KArrayConst<A, R>): KExpr<A> =
+        expr.kind(ExprKind.ArrayConst)
 
-    override fun <D : KSort, R : KSort> transform(expr: KFunctionAsArray<D, R>): KExpr<KArraySort<D, R>> =
+    override fun <A : KArraySortBase<R>, R : KSort> transform(expr: KFunctionAsArray<A, R>): KExpr<A> =
         expr.kind(ExprKind.FunctionAsArray)
 
 
     override fun <D : KSort, R : KSort> transform(expr: KArrayLambda<D, R>): KExpr<KArraySort<D, R>> =
         expr.kind(ExprKind.ArrayLambda)
 
+    override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+        expr: KArray2Lambda<D0, D1, R>
+    ): KExpr<KArray2Sort<D0, D1, R>> = expr.kind(ExprKind.Array2Lambda)
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Lambda<D0, D1, D2, R>
+    ): KExpr<KArray3Sort<D0, D1, D2, R>> = expr.kind(ExprKind.Array3Lambda)
+
+    override fun <R : KSort> transform(expr: KArrayNLambda<R>): KExpr<KArrayNSort<R>> =
+        expr.kind(ExprKind.ArrayLambda)
 
     override fun <T : KArithSort> transform(expr: KAddArithExpr<T>): KExpr<T> = expr.kind(ExprKind.AddArithExpr)
 
diff --git a/ksmt-runner/src/main/kotlin/org/ksmt/runner/serializer/SortKind.kt b/ksmt-runner/src/main/kotlin/org/ksmt/runner/serializer/SortKind.kt
index b4bb1c7de..1ab86960c 100644
--- a/ksmt-runner/src/main/kotlin/org/ksmt/runner/serializer/SortKind.kt
+++ b/ksmt-runner/src/main/kotlin/org/ksmt/runner/serializer/SortKind.kt
@@ -1,5 +1,5 @@
 package org.ksmt.runner.serializer
 
 enum class SortKind {
-    Bool, Int, Real, Bv, Fp, Array, FpRM, Uninterpreted
+    Bool, Int, Real, Bv, Fp, Array, Array2, Array3, ArrayN, FpRM, Uninterpreted
 }
diff --git a/ksmt-test/src/main/kotlin/org/ksmt/test/RandomExpressionGenerator.kt b/ksmt-test/src/main/kotlin/org/ksmt/test/RandomExpressionGenerator.kt
index 0a92893e3..8e5ed54ed 100644
--- a/ksmt-test/src/main/kotlin/org/ksmt/test/RandomExpressionGenerator.kt
+++ b/ksmt-test/src/main/kotlin/org/ksmt/test/RandomExpressionGenerator.kt
@@ -5,7 +5,11 @@ import org.ksmt.KContext
 import org.ksmt.expr.KExpr
 import org.ksmt.expr.KFpRoundingMode
 import org.ksmt.expr.KInterpretedValue
+import org.ksmt.sort.KArray2Sort
+import org.ksmt.sort.KArray3Sort
+import org.ksmt.sort.KArrayNSort
 import org.ksmt.sort.KArraySort
+import org.ksmt.sort.KArraySortBase
 import org.ksmt.sort.KBoolSort
 import org.ksmt.sort.KBvSort
 import org.ksmt.sort.KFpRoundingModeSort
@@ -401,7 +405,7 @@ class RandomExpressionGenerator {
                     args + sortArgument
                 }
 
-            override fun <D : KSort, R : KSort> visit(sort: KArraySort<D, R>): AstGenerator<ExprArgument> {
+            private fun <A : KArraySortBase<R>, R : KSort> generateArray(sort: A): AstGenerator<ExprArgument> {
                 val rangeSortArgument = SortArgument(sort.range, generationContext.findSortIdx(sort.range))
                 val rangeExprGenerator = sort.range.accept(ConstExprGenerator(rangeSortArgument, generationContext))
                 val rangeExpr = rangeExprGenerator.generate(generationContext)
@@ -409,6 +413,20 @@ class RandomExpressionGenerator {
                     listOf(sortArgument, rangeExpr)
                 }
             }
+
+            override fun <D : KSort, R : KSort> visit(sort: KArraySort<D, R>): AstGenerator<ExprArgument> =
+                generateArray(sort)
+
+            override fun <D0 : KSort, D1 : KSort, R : KSort> visit(
+                sort: KArray2Sort<D0, D1, R>
+            ): AstGenerator<ExprArgument> = generateArray(sort)
+
+            override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> visit(
+                sort: KArray3Sort<D0, D1, D2, R>
+            ): AstGenerator<ExprArgument> = generateArray(sort)
+
+            override fun <R : KSort> visit(sort: KArrayNSort<R>): AstGenerator<ExprArgument> =
+                generateArray(sort)
         }
 
         sealed interface Argument {
diff --git a/ksmt-test/src/test/kotlin/org/ksmt/test/BenchmarksBasedTest.kt b/ksmt-test/src/test/kotlin/org/ksmt/test/BenchmarksBasedTest.kt
index 4c1941186..b920c1a31 100644
--- a/ksmt-test/src/test/kotlin/org/ksmt/test/BenchmarksBasedTest.kt
+++ b/ksmt-test/src/test/kotlin/org/ksmt/test/BenchmarksBasedTest.kt
@@ -37,7 +37,7 @@ import org.ksmt.solver.KSolverUnsupportedFeatureException
 import org.ksmt.solver.async.KAsyncSolver
 import org.ksmt.solver.runner.KSolverRunnerManager
 import org.ksmt.sort.KArithSort
-import org.ksmt.sort.KArraySort
+import org.ksmt.sort.KArraySortBase
 import org.ksmt.sort.KBoolSort
 import org.ksmt.sort.KBvSort
 import org.ksmt.sort.KFpSort
@@ -422,7 +422,7 @@ abstract class BenchmarksBasedTest {
     }
 
     class AsArrayDeclChecker(override val ctx: KContext, val model: KModel) : KTransformer {
-        override fun <D : KSort, R : KSort> transform(expr: KFunctionAsArray<D, R>): KExpr<KArraySort<D, R>> {
+        override fun <A : KArraySortBase<R>, R : KSort> transform(expr: KFunctionAsArray<A, R>): KExpr<A> {
             assertNotNull(model.interpretation(expr.function), "no interpretation for as-array: $expr")
             return expr
         }
diff --git a/ksmt-yices/src/main/kotlin/org/ksmt/solver/yices/KYicesExprConverter.kt b/ksmt-yices/src/main/kotlin/org/ksmt/solver/yices/KYicesExprConverter.kt
index 462f68c3f..55c57ae7c 100644
--- a/ksmt-yices/src/main/kotlin/org/ksmt/solver/yices/KYicesExprConverter.kt
+++ b/ksmt-yices/src/main/kotlin/org/ksmt/solver/yices/KYicesExprConverter.kt
@@ -82,13 +82,13 @@ open class KYicesExprConverter(
                         && argType.range is KIntSort
                         && exprSort is KArraySort<*, *>
                         && exprSort.range is KRealSort ->
-                    castArrayRangeToInt(convertedExpr.uncheckedCast<_, KExpr<KArraySort<*, KRealSort>>>())
+                    castArrayRangeToInt(convertedExpr.uncheckedCast<_, KExpr<KArraySort<KSort, KRealSort>>>())
 
                 argType is KArraySort<*, *>
                         && argType.range is KRealSort
                         && exprSort is KArraySort<*, *>
                         && exprSort.range is KIntSort ->
-                    castArrayRangeToReal(convertedExpr.uncheckedCast<_, KExpr<KArraySort<*, KIntSort>>>())
+                    castArrayRangeToReal(convertedExpr.uncheckedCast<_, KExpr<KArraySort<KSort, KIntSort>>>())
 
                 else -> error("Invalid state")
             }
@@ -345,7 +345,9 @@ open class KYicesExprConverter(
 
                 if (convertedExprSort is KArraySort<*, *>) {
                     argTypes.addAll(listOf(convertedExprSort, convertedExprSort.domain))
-                    return expr.convert(yicesArgs, ::mkArraySelect)
+                    return expr.convert(yicesArgs) { array: KExpr<KArraySort<KSort, KSort>>, index: KExpr<KSort> ->
+                        mkArraySelect(array, index)
+                    }
                 }
 
                 if (!Terms.isAtomic(yicesArgs.first())) {
@@ -376,7 +378,11 @@ open class KYicesExprConverter(
                 val rangeType = arrayType.range
                 argTypes.addAll(listOf(arrayType, indexType, rangeType))
 
-                expr.convert(yicesArgs, ::mkArrayStore)
+                expr.convert(
+                    yicesArgs
+                ) { array: KExpr<KArraySort<KSort, KSort>>, index: KExpr<KSort>, value: KExpr<KSort> ->
+                    mkArrayStore(array, index, value)
+                }
             }
             Constructor.EQ_TERM -> {
                 if (Terms.isArithmetic(yicesArgs.first())) {
@@ -413,7 +419,7 @@ open class KYicesExprConverter(
                     if (yicesCtx.findConvertedDecl(yicesArgs.first()) == null) {
                         mkArrayConst(mkArraySort(convertSort(Terms.typeOf(yicesArgs.first())), body.sort), body)
                     } else {
-                        val index = convertDecl(yicesArgs.first())
+                        val index: KDecl<KSort> = convertDecl(yicesArgs.first()).uncheckedCast()
                         mkArrayLambda(index, body)
                     }
                 }
diff --git a/ksmt-yices/src/main/kotlin/org/ksmt/solver/yices/KYicesExprInternalizer.kt b/ksmt-yices/src/main/kotlin/org/ksmt/solver/yices/KYicesExprInternalizer.kt
index bb8cfa58a..5ab206dbc 100644
--- a/ksmt-yices/src/main/kotlin/org/ksmt/solver/yices/KYicesExprInternalizer.kt
+++ b/ksmt-yices/src/main/kotlin/org/ksmt/solver/yices/KYicesExprInternalizer.kt
@@ -4,8 +4,17 @@ import org.ksmt.KContext
 import org.ksmt.decl.KDecl
 import org.ksmt.expr.KAddArithExpr
 import org.ksmt.expr.KAndExpr
+import org.ksmt.expr.KArray2Lambda
+import org.ksmt.expr.KArray2Select
+import org.ksmt.expr.KArray2Store
+import org.ksmt.expr.KArray3Lambda
+import org.ksmt.expr.KArray3Select
+import org.ksmt.expr.KArray3Store
 import org.ksmt.expr.KArrayConst
 import org.ksmt.expr.KArrayLambda
+import org.ksmt.expr.KArrayNLambda
+import org.ksmt.expr.KArrayNSelect
+import org.ksmt.expr.KArrayNStore
 import org.ksmt.expr.KArraySelect
 import org.ksmt.expr.KArrayStore
 import org.ksmt.expr.KBitVec16Value
@@ -147,6 +156,10 @@ import org.ksmt.sort.KFpSort
 import org.ksmt.sort.KRealSort
 import org.ksmt.sort.KSort
 import org.ksmt.solver.KSolverUnsupportedFeatureException
+import org.ksmt.sort.KArray2Sort
+import org.ksmt.sort.KArray3Sort
+import org.ksmt.sort.KArrayNSort
+import org.ksmt.sort.KArraySortBase
 import org.ksmt.sort.KBv16Sort
 import org.ksmt.sort.KBv1Sort
 import org.ksmt.sort.KBv32Sort
@@ -639,19 +652,49 @@ open class KYicesExprInternalizer(
         transform(array, index, value, yicesCtx::functionUpdate1)
     }
 
+    override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+        expr: KArray2Store<D0, D1, R>
+    ): KExpr<KArray2Sort<D0, D1, R>> {
+        TODO("Multi-indexed arrays are not supported")
+    }
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Store<D0, D1, D2, R>
+    ): KExpr<KArray3Sort<D0, D1, D2, R>> {
+        TODO("Multi-indexed arrays are not supported")
+    }
+
+    override fun <R : KSort> transform(expr: KArrayNStore<R>): KExpr<KArrayNSort<R>> {
+        TODO("Multi-indexed arrays are not supported")
+    }
+
     override fun <D : KSort, R : KSort> transform(expr: KArraySelect<D, R>): KExpr<R> = with(expr) {
         transform(array, index) { array: YicesTerm, index: YicesTerm ->
             yicesCtx.funApplication(array, index)
         }
     }
 
-    override fun <D : KSort, R : KSort> transform(expr: KArrayConst<D, R>): KExpr<KArraySort<D, R>> = with(expr) {
+    override fun <D0 : KSort, D1 : KSort, R : KSort> transform(expr: KArray2Select<D0, D1, R>): KExpr<R> {
+        TODO("Multi-indexed arrays are not supported")
+    }
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Select<D0, D1, D2, R>
+    ): KExpr<R> {
+        TODO("Multi-indexed arrays are not supported")
+    }
+
+    override fun <R : KSort> transform(expr: KArrayNSelect<R>): KExpr<R> {
+        TODO("Multi-indexed arrays are not supported")
+    }
+
+    override fun <A: KArraySortBase<R>, R : KSort> transform(expr: KArrayConst<A, R>): KExpr<A> = with(expr) {
         transform(value) { value: YicesTerm ->
             yicesCtx.lambda(listOf(yicesCtx.newVariable(sort.internalizeSort())), value)
         }
     }
 
-    override fun <D : KSort, R : KSort> transform(expr: KFunctionAsArray<D, R>): KExpr<KArraySort<D, R>> = with(expr) {
+    override fun <A : KArraySortBase<R>, R : KSort> transform(expr: KFunctionAsArray<A, R>): KExpr<A> = with(expr) {
         transform { function.internalizeDecl() }
     }
 
@@ -675,6 +718,22 @@ open class KYicesExprInternalizer(
         }
     }
 
+    override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+        expr: KArray2Lambda<D0, D1, R>
+    ): KExpr<KArray2Sort<D0, D1, R>> {
+        TODO("Multi-indexed arrays are not supported")
+    }
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Lambda<D0, D1, D2, R>
+    ): KExpr<KArray3Sort<D0, D1, D2, R>> {
+        TODO("Multi-indexed arrays are not supported")
+    }
+
+    override fun <R : KSort> transform(expr: KArrayNLambda<R>): KExpr<KArrayNSort<R>> {
+        TODO("Multi-indexed arrays are not supported")
+    }
+
     override fun <T : KArithSort> transform(expr: KAddArithExpr<T>): KExpr<T> = with(expr) {
         transformList(args) { args: Array<YicesTerm> -> yicesCtx.add(args.toList()) }
     }
diff --git a/ksmt-yices/src/main/kotlin/org/ksmt/solver/yices/KYicesModel.kt b/ksmt-yices/src/main/kotlin/org/ksmt/solver/yices/KYicesModel.kt
index 34f750ab6..0aa577f8b 100644
--- a/ksmt-yices/src/main/kotlin/org/ksmt/solver/yices/KYicesModel.kt
+++ b/ksmt-yices/src/main/kotlin/org/ksmt/solver/yices/KYicesModel.kt
@@ -70,7 +70,7 @@ class KYicesModel(
 
                 funcInterpretationsToDo.add(Pair(yval, funcDecl))
 
-                mkFunctionAsArray<KSort, KSort>(funcDecl).uncheckedCast()
+                mkFunctionAsArray(sort.uncheckedCast(), funcDecl).uncheckedCast()
             }
             else -> error("Unsupported sort $sort")
         }
diff --git a/ksmt-yices/src/main/kotlin/org/ksmt/solver/yices/KYicesSortInternalizer.kt b/ksmt-yices/src/main/kotlin/org/ksmt/solver/yices/KYicesSortInternalizer.kt
index a5e55ab7a..3190010c3 100644
--- a/ksmt-yices/src/main/kotlin/org/ksmt/solver/yices/KYicesSortInternalizer.kt
+++ b/ksmt-yices/src/main/kotlin/org/ksmt/solver/yices/KYicesSortInternalizer.kt
@@ -1,6 +1,9 @@
 package org.ksmt.solver.yices
 
 import org.ksmt.solver.KSolverUnsupportedFeatureException
+import org.ksmt.sort.KArray2Sort
+import org.ksmt.sort.KArray3Sort
+import org.ksmt.sort.KArrayNSort
 import org.ksmt.sort.KArraySort
 import org.ksmt.sort.KBoolSort
 import org.ksmt.sort.KBvSort
@@ -36,6 +39,18 @@ open class KYicesSortInternalizer(
             yicesCtx.functionType(sort.domain.internalizeYicesSort(), sort.range.internalizeYicesSort())
         }
 
+    override fun <D0 : KSort, D1 : KSort, R : KSort> visit(sort: KArray2Sort<D0, D1, R>): YicesSort {
+        TODO("Multi-indexed arrays are not supported")
+    }
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> visit(sort: KArray3Sort<D0, D1, D2, R>): YicesSort {
+        TODO("Multi-indexed arrays are not supported")
+    }
+
+    override fun <R : KSort> visit(sort: KArrayNSort<R>): YicesSort {
+        TODO("Multi-indexed arrays are not supported")
+    }
+
     override fun visit(sort: KUninterpretedSort): YicesSort = yicesCtx.internalizeSort(sort) {
         yicesCtx.newUninterpretedType(sort.name)
     }
diff --git a/ksmt-z3/src/main/kotlin/com/microsoft/z3/Util.kt b/ksmt-z3/src/main/kotlin/com/microsoft/z3/Util.kt
index 614af8c05..0e92676ce 100644
--- a/ksmt-z3/src/main/kotlin/com/microsoft/z3/Util.kt
+++ b/ksmt-z3/src/main/kotlin/com/microsoft/z3/Util.kt
@@ -1,5 +1,7 @@
 package com.microsoft.z3
 
+import com.microsoft.z3.enumerations.Z3_error_code
+
 fun intOrNull(ctx: Long, expr: Long): Int? {
     val result = Native.IntPtr()
     if (!Native.getNumeralInt(ctx, expr, result)) return null
@@ -46,3 +48,28 @@ fun getAppArgs(ctx: Long, expr: Long): LongArray {
     val size = Native.getAppNumArgs(ctx, expr)
     return LongArray(size) { idx -> Native.getAppArg(ctx, expr, idx) }
 }
+
+/**
+ * We have no way to obtain array sort domain size.
+ * To overcome this we iterate over domain until index is out of bounds.
+ * */
+@Suppress("LoopWithTooManyJumpStatements")
+fun getArraySortDomain(ctx: Long, sort: Long): List<Long> {
+    val domain = arrayListOf<Long>()
+    while (true) {
+        val domainSortI = Native.INTERNALgetArraySortDomainN(ctx, sort, domain.size)
+        when (val errorCode = Z3_error_code.fromInt(Native.INTERNALgetErrorCode(ctx))) {
+            Z3_error_code.Z3_OK -> {
+                domain.add(domainSortI)
+                continue
+            }
+
+            /**
+             * Z3 set [Z3_error_code.Z3_INVALID_ARG] error code when sort domain index is out of bounds.
+             * */
+            Z3_error_code.Z3_INVALID_ARG -> break
+            else -> throw Z3Exception(Native.INTERNALgetErrorMsg(ctx, errorCode.toInt()))
+        }
+    }
+    return domain
+}
diff --git a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3ExprConverter.kt b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3ExprConverter.kt
index 6da2f71c2..2055f002f 100644
--- a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3ExprConverter.kt
+++ b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3ExprConverter.kt
@@ -10,6 +10,7 @@ import com.microsoft.z3.enumerations.Z3_sort_kind
 import com.microsoft.z3.enumerations.Z3_symbol_kind
 import com.microsoft.z3.fpSignOrNull
 import com.microsoft.z3.getAppArgs
+import com.microsoft.z3.getArraySortDomain
 import com.microsoft.z3.intOrNull
 import com.microsoft.z3.longOrNull
 import org.ksmt.KContext
@@ -23,7 +24,11 @@ import org.ksmt.expr.KIntNumExpr
 import org.ksmt.expr.KRealNumExpr
 import org.ksmt.solver.util.KExprConverterBase
 import org.ksmt.sort.KArithSort
+import org.ksmt.sort.KArray2Sort
+import org.ksmt.sort.KArray3Sort
+import org.ksmt.sort.KArrayNSort
 import org.ksmt.sort.KArraySort
+import org.ksmt.sort.KArraySortBase
 import org.ksmt.sort.KBoolSort
 import org.ksmt.sort.KBv1Sort
 import org.ksmt.sort.KBvSort
@@ -31,6 +36,7 @@ import org.ksmt.sort.KFpRoundingModeSort
 import org.ksmt.sort.KFpSort
 import org.ksmt.sort.KRealSort
 import org.ksmt.sort.KSort
+import org.ksmt.utils.uncheckedCast
 
 open class KZ3ExprConverter(
     private val ctx: KContext,
@@ -91,11 +97,7 @@ open class KZ3ExprConverter(
             Z3_sort_kind.Z3_BOOL_SORT -> boolSort
             Z3_sort_kind.Z3_INT_SORT -> intSort
             Z3_sort_kind.Z3_REAL_SORT -> realSort
-            Z3_sort_kind.Z3_ARRAY_SORT -> {
-                val domain = Native.getArraySortDomain(nCtx, sort)
-                val range = Native.getArraySortRange(nCtx, sort)
-                mkArraySort(domain.convertSort(), range.convertSort())
-            }
+            Z3_sort_kind.Z3_ARRAY_SORT -> convertNativeArraySort(sort)
             Z3_sort_kind.Z3_BV_SORT -> mkBvSort(Native.getBvSortSize(nCtx, sort).toUInt())
             Z3_sort_kind.Z3_FLOATING_POINT_SORT ->
                 mkFpSort(Native.fpaGetEbits(nCtx, sort).toUInt(), Native.fpaGetSbits(nCtx, sort).toUInt())
@@ -115,6 +117,22 @@ open class KZ3ExprConverter(
         }
     }
 
+    open fun KContext.convertNativeArraySort(sort: Long): KSort {
+        val domain = getArraySortDomain(nCtx, sort).map { it.convertSort<KSort>() }
+        val range = Native.getArraySortRange(nCtx, sort).convertSort<KSort>()
+
+        return when (domain.size) {
+            KArraySort.DOMAIN_SIZE -> mkArraySort(domain.single(), range)
+            KArray2Sort.DOMAIN_SIZE -> mkArraySort(domain.first(), domain.last(), range)
+            KArray3Sort.DOMAIN_SIZE -> {
+                val (d0, d1, d2) = domain
+                mkArraySort(d0, d1, d2, range)
+            }
+
+            else -> mkArrayNSort(domain, range)
+        }
+    }
+
     /**
      * Convert expression non-recursively.
      * 1. Ensure all expression arguments are already converted and available in [z3Ctx].
@@ -177,11 +195,11 @@ open class KZ3ExprConverter(
             Z3_decl_kind.Z3_OP_TO_REAL -> expr.convert(::mkIntToReal)
             Z3_decl_kind.Z3_OP_TO_INT -> expr.convert(::mkRealToInt)
             Z3_decl_kind.Z3_OP_IS_INT -> expr.convert(::mkRealIsInt)
-            Z3_decl_kind.Z3_OP_STORE -> expr.convert(::mkArrayStore)
-            Z3_decl_kind.Z3_OP_SELECT -> expr.convert(::mkArraySelect)
+            Z3_decl_kind.Z3_OP_STORE -> convertArrayStore(expr)
+            Z3_decl_kind.Z3_OP_SELECT -> convertArraySelect(expr)
             Z3_decl_kind.Z3_OP_CONST_ARRAY -> expr.convert { arg: KExpr<KSort> ->
-                val range = Native.getRange(nCtx, decl).convertSort<KArraySort<*, *>>()
-                mkArrayConst(range, arg)
+                val sort = Native.getRange(nCtx, decl).convertSort<KArraySortBase<KSort>>()
+                mkArrayConst(sort, arg)
             }
             Z3_decl_kind.Z3_OP_BNUM,
             Z3_decl_kind.Z3_OP_BIT1,
@@ -277,9 +295,10 @@ open class KZ3ExprConverter(
 
             Z3_decl_kind.Z3_OP_BSMUL_NO_UDFL -> expr.convert(::mkBvMulNoUnderflowExpr)
             Z3_decl_kind.Z3_OP_AS_ARRAY -> convert {
+                val sort = Native.getRange(nCtx, decl).convertSort<KArraySortBase<KSort>>()
                 val z3Decl = Native.getDeclFuncDeclParameter(nCtx, decl, 0).convertDecl<KSort>()
                 val funDecl = z3Decl as? KFuncDecl<KSort> ?: error("unexpected as-array decl $z3Decl")
-                mkFunctionAsArray<KSort, KSort>(funDecl)
+                mkFunctionAsArray(sort, funDecl)
             }
 
             Z3_decl_kind.Z3_OP_FPA_NEG -> expr.convert(::mkFpNegationExpr)
@@ -495,6 +514,73 @@ open class KZ3ExprConverter(
         mkFpRoundingModeExpr(roundingMode)
     }
 
+    private fun convertArrayStore(expr: Long): ExprConversionResult =
+        when (Native.getAppNumArgs(nCtx, expr)) {
+            KArraySort.DOMAIN_SIZE + 2 -> expr.convert(::mkArray1Store)
+            KArray2Sort.DOMAIN_SIZE + 2 -> expr.convert(::mkArray2Store)
+            KArray3Sort.DOMAIN_SIZE + 2 -> expr.convertList { args: List<KExpr<KSort>> ->
+                val (i0, i1, i2) = args.subList(1, args.lastIndex)
+                mkArray3Store(args.first().uncheckedCast(), i0, i1, i2, args.last())
+            }
+            else -> expr.convertList { args: List<KExpr<KSort>> ->
+                mkArrayNStore(args.first().uncheckedCast(), args.subList(1, args.lastIndex), args.last())
+            }
+        }
+
+    private fun convertArraySelect(expr: Long): ExprConversionResult =
+        when (Native.getAppNumArgs(nCtx, expr)) {
+            KArraySort.DOMAIN_SIZE + 1 -> expr.convert(::mkArray1Select)
+            KArray2Sort.DOMAIN_SIZE + 1 -> expr.convert(::mkArray2Select)
+            KArray3Sort.DOMAIN_SIZE + 1 -> expr.convert(::mkArray3Select)
+            else -> expr.convertList { args: List<KExpr<KSort>> ->
+                mkArrayNSelect(args.first().uncheckedCast(), args.drop(1))
+            }
+        }
+
+    private fun mkArray1Select(
+        array: KExpr<KArraySort<KSort, KSort>>,
+        index: KExpr<KSort>
+    ) = ctx.mkArraySelect(array, index)
+
+    private fun mkArray2Select(
+        array: KExpr<KArray2Sort<KSort, KSort, KSort>>,
+        index0: KExpr<KSort>, index1: KExpr<KSort>
+    ) = ctx.mkArraySelect(array, index0, index1)
+
+    private fun mkArray3Select(
+        array: KExpr<KArray3Sort<KSort, KSort, KSort, KSort>>,
+        index0: KExpr<KSort>, index1: KExpr<KSort>, index2: KExpr<KSort>
+    ) = ctx.mkArraySelect(array, index0, index1, index2)
+
+    private fun mkArrayNSelect(
+        array: KExpr<KArrayNSort<KSort>>,
+        indices: List<KExpr<KSort>>
+    ) = ctx.mkArrayNSelect(array, indices)
+
+    private fun mkArray1Store(
+        array: KExpr<KArraySort<KSort, KSort>>,
+        index: KExpr<KSort>,
+        value: KExpr<KSort>
+    ) = ctx.mkArrayStore(array, index, value)
+
+    private fun mkArray2Store(
+        array: KExpr<KArray2Sort<KSort, KSort, KSort>>,
+        index0: KExpr<KSort>, index1: KExpr<KSort>,
+        value: KExpr<KSort>
+    ) = ctx.mkArrayStore(array, index0, index1, value)
+
+    private fun mkArray3Store(
+        array: KExpr<KArray3Sort<KSort, KSort, KSort, KSort>>,
+        index0: KExpr<KSort>, index1: KExpr<KSort>, index2: KExpr<KSort>,
+        value: KExpr<KSort>
+    ) = ctx.mkArrayStore(array, index0, index1, index2, value)
+
+    private fun mkArrayNStore(
+        array: KExpr<KArrayNSort<KSort>>,
+        indices: List<KExpr<KSort>>,
+        value: KExpr<KSort>
+    ) = ctx.mkArrayNStore(array, indices, value)
+
     open fun convertQuantifier(expr: Long): ExprConversionResult = with(ctx) {
         val numBound = Native.getQuantifierNumBound(nCtx, expr)
         val boundSorts = List(numBound) { idx -> Native.getQuantifierBoundSort(nCtx, expr, idx) }
@@ -530,8 +616,15 @@ open class KZ3ExprConverter(
             Native.isQuantifierForall(nCtx, expr) -> mkUniversalQuantifier(body, bounds)
             Native.isQuantifierExists(nCtx, expr) -> mkExistentialQuantifier(body, bounds)
             Native.isLambda(nCtx, expr) -> {
-                val boundVar = bounds.singleOrNull() ?: TODO("Array lambda with multiple indices")
-                mkArrayLambda(boundVar, body)
+                when (bounds.size) {
+                    KArraySort.DOMAIN_SIZE -> mkArrayLambda(bounds.single(), body)
+                    KArray2Sort.DOMAIN_SIZE -> mkArrayLambda(bounds.first(), bounds.last(), body)
+                    KArray3Sort.DOMAIN_SIZE -> {
+                        val (b0, b1, b2) = bounds
+                        mkArrayLambda(b0, b1, b2, body)
+                    }
+                    else -> mkArrayNLambda(bounds, body)
+                }
             }
             else -> TODO("unexpected quantifier: ${Native.astToString(nCtx, expr)}")
         }
diff --git a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3ExprInternalizer.kt b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3ExprInternalizer.kt
index cb08dbeb6..8cc7f8fef 100644
--- a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3ExprInternalizer.kt
+++ b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3ExprInternalizer.kt
@@ -9,8 +9,17 @@ import org.ksmt.KContext
 import org.ksmt.decl.KDecl
 import org.ksmt.expr.KAddArithExpr
 import org.ksmt.expr.KAndExpr
+import org.ksmt.expr.KArray2Lambda
+import org.ksmt.expr.KArray2Select
+import org.ksmt.expr.KArray2Store
+import org.ksmt.expr.KArray3Lambda
+import org.ksmt.expr.KArray3Select
+import org.ksmt.expr.KArray3Store
 import org.ksmt.expr.KArrayConst
 import org.ksmt.expr.KArrayLambda
+import org.ksmt.expr.KArrayNLambda
+import org.ksmt.expr.KArrayNSelect
+import org.ksmt.expr.KArrayNStore
 import org.ksmt.expr.KArraySelect
 import org.ksmt.expr.KArrayStore
 import org.ksmt.expr.KBitVec16Value
@@ -142,7 +151,11 @@ import org.ksmt.expr.KUniversalQuantifier
 import org.ksmt.expr.KXorExpr
 import org.ksmt.solver.util.KExprInternalizerBase
 import org.ksmt.sort.KArithSort
+import org.ksmt.sort.KArray2Sort
+import org.ksmt.sort.KArray3Sort
+import org.ksmt.sort.KArrayNSort
 import org.ksmt.sort.KArraySort
+import org.ksmt.sort.KArraySortBase
 import org.ksmt.sort.KBoolSort
 import org.ksmt.sort.KBvSort
 import org.ksmt.sort.KFp128Sort
@@ -605,19 +618,113 @@ open class KZ3ExprInternalizer(
         transform(array, index, value, Native::mkStore)
     }
 
+    override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+        expr: KArray2Store<D0, D1, R>
+    ): KExpr<KArray2Sort<D0, D1, R>> = with(expr) {
+        transform(array, index0, index1, value) { array: Long, i0: Long, i1: Long, value: Long ->
+            val indices = longArrayOf(i0, i1)
+            Native.mkStoreN(nCtx, array, indices.size, indices, value)
+        }
+    }
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Store<D0, D1, D2, R>
+    ): KExpr<KArray3Sort<D0, D1, D2, R>> = with(expr) {
+        transformArray(listOf(array, index0, index1, index2, value)) { args ->
+            val (array, i0, i1, i2, value) = args
+            val indices = longArrayOf(i0, i1, i2)
+            Native.mkStoreN(nCtx, array, indices.size, indices, value)
+        }
+    }
+
+    override fun <R : KSort> transform(expr: KArrayNStore<R>): KExpr<KArrayNSort<R>> = with(expr) {
+        transformArray(indices + listOf(array, value)) { args ->
+            val value = args[args.lastIndex]
+            val array = args[args.lastIndex - 1]
+            val indices = args.copyOf(args.size - 2)
+            Native.mkStoreN(nCtx, array, indices.size, indices, value)
+        }
+    }
+
     override fun <D : KSort, R : KSort> transform(expr: KArraySelect<D, R>) = with(expr) {
         transform(array, index, Native::mkSelect)
     }
 
-    override fun <D : KSort, R : KSort> transform(expr: KArrayConst<D, R>) = with(expr) {
-        transform(value) { value: Long -> Native.mkConstArray(nCtx, sort.domain.internalizeSort(), value) }
+    override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+        expr: KArray2Select<D0, D1, R>
+    ): KExpr<R> = with(expr) {
+        transform(array, index0, index1) { array: Long, i0: Long, i1: Long ->
+            val indices = longArrayOf(i0, i1)
+            Native.mkSelectN(nCtx, array, indices.size, indices)
+        }
+    }
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Select<D0, D1, D2, R>
+    ): KExpr<R>  = with(expr) {
+        transform(array, index0, index1, index2) { array: Long, i0: Long, i1: Long, i2: Long ->
+            val indices = longArrayOf(i0, i1, i2)
+            Native.mkSelectN(nCtx, array, indices.size, indices)
+        }
+    }
+
+    override fun <R : KSort> transform(expr: KArrayNSelect<R>): KExpr<R> = with(expr) {
+        transformArray(indices + array) { args ->
+            val array = args.last()
+            val indices = args.copyOf(args.size - 1)
+            Native.mkSelectN(nCtx, array, indices.size, indices)
+        }
     }
 
+    override fun <A: KArraySortBase<R>, R : KSort> transform(expr: KArrayConst<A, R>) = with(expr) {
+        transform(value) { value: Long ->
+            mkConstArray(sort, value)
+        }
+    }
+
+    private fun mkConstArray(sort: KArraySortBase<*>, value: Long): Long =
+        if (sort is KArraySort<*, *>) {
+            Native.mkConstArray(nCtx, sort.domain.internalizeSort(), value)
+        } else {
+            val domain = sort.domainSorts.map { it.internalizeSort() }.toLongArray()
+            val domainNames = LongArray(sort.domainSorts.size) { Native.mkIntSymbol(nCtx, it) }
+            Native.mkLambda(nCtx, domain.size, domain, domainNames, value)
+        }
+
     override fun <D : KSort, R : KSort> transform(expr: KArrayLambda<D, R>) = with(expr) {
-        transform(body) { body: Long ->
-            val indexSort = indexVarDecl.sort.internalizeSort()
-            val indexName = Native.mkStringSymbol(nCtx, indexVarDecl.name)
-            Native.mkLambda(nCtx, 1, longArrayOf(indexSort), longArrayOf(indexName), body)
+        transform(body, ctx.mkConstApp(indexVarDecl)) { body: Long, index: Long ->
+            val indices = longArrayOf(index)
+            Native.mkLambdaConst(nCtx, indices.size, indices, body)
+        }
+    }
+
+    override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+        expr: KArray2Lambda<D0, D1, R>
+    ): KExpr<KArray2Sort<D0, D1, R>> = with(expr) {
+        transform(
+            body, ctx.mkConstApp(indexVar0Decl), ctx.mkConstApp(indexVar1Decl)
+        ) { body: Long, index0: Long, index1: Long ->
+            val indices = longArrayOf(index0, index1)
+            Native.mkLambdaConst(nCtx, indices.size, indices, body)
+        }
+    }
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+        expr: KArray3Lambda<D0, D1, D2, R>
+    ): KExpr<KArray3Sort<D0, D1, D2, R>>  = with(expr) {
+        transform(
+            body, ctx.mkConstApp(indexVar0Decl), ctx.mkConstApp(indexVar1Decl), ctx.mkConstApp(indexVar2Decl)
+        ) { body: Long, index0: Long, index1: Long, index2: Long ->
+            val indices = longArrayOf(index0, index1, index2)
+            Native.mkLambdaConst(nCtx, indices.size, indices, body)
+        }
+    }
+
+    override fun <R : KSort> transform(expr: KArrayNLambda<R>): KExpr<KArrayNSort<R>> = with(expr) {
+        transformArray(indexVarDeclarations.map { ctx.mkConstApp(it) } + body) { args ->
+            val body = args.last()
+            val indices = args.copyOf(args.size - 1)
+            Native.mkLambdaConst(nCtx, indices.size, indices, body)
         }
     }
 
@@ -706,8 +813,8 @@ open class KZ3ExprInternalizer(
 
     override fun transform(expr: KUniversalQuantifier) = transformQuantifier(expr, isUniversal = true)
 
-    override fun <D : KSort, R : KSort> transform(expr: KFunctionAsArray<D, R>): KExpr<KArraySort<D, R>> {
-        TODO("KFunctionAsArray internalization is not implemented in z3")
+    override fun <A : KArraySortBase<R>, R : KSort> transform(expr: KFunctionAsArray<A, R>): KExpr<A> = with(expr) {
+        transform { Native.mkAsArray(nCtx, function.internalizeDecl()) }
     }
 
     inline fun <S : KExpr<*>> S.transform(
diff --git a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3SortInternalizer.kt b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3SortInternalizer.kt
index c449d2dea..2fc609a3d 100644
--- a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3SortInternalizer.kt
+++ b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3SortInternalizer.kt
@@ -1,6 +1,9 @@
 package org.ksmt.solver.z3
 
 import com.microsoft.z3.Native
+import org.ksmt.sort.KArray2Sort
+import org.ksmt.sort.KArray3Sort
+import org.ksmt.sort.KArrayNSort
 import org.ksmt.sort.KArraySort
 import org.ksmt.sort.KBoolSort
 import org.ksmt.sort.KBvSort
@@ -42,6 +45,34 @@ open class KZ3SortInternalizer(
             Native.mkArraySort(nCtx, domain, range)
         }
 
+    override fun <D0 : KSort, D1 : KSort, R : KSort> visit(sort: KArray2Sort<D0, D1, R>): Long =
+        z3Ctx.internalizeSort(sort) {
+            val domain = longArrayOf(
+                sort.domain0.internalizeZ3Sort(),
+                sort.domain1.internalizeZ3Sort()
+            )
+            val range = sort.range.internalizeZ3Sort()
+            Native.mkArraySortN(nCtx, domain.size, domain, range)
+        }
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> visit(sort: KArray3Sort<D0, D1, D2, R>): Long =
+        z3Ctx.internalizeSort(sort) {
+            val domain = longArrayOf(
+                sort.domain0.internalizeZ3Sort(),
+                sort.domain1.internalizeZ3Sort(),
+                sort.domain2.internalizeZ3Sort()
+            )
+            val range = sort.range.internalizeZ3Sort()
+            Native.mkArraySortN(nCtx, domain.size, domain, range)
+        }
+
+    override fun <R : KSort> visit(sort: KArrayNSort<R>): Long =
+        z3Ctx.internalizeSort(sort) {
+            val domain = sort.domainSorts.map { it.internalizeZ3Sort() }.toLongArray()
+            val range = sort.range.internalizeZ3Sort()
+            Native.mkArraySortN(nCtx, domain.size, domain, range)
+        }
+
     override fun visit(sort: KFpRoundingModeSort): Long = z3Ctx.internalizeSort(sort) {
         Native.mkFpaRoundingModeSort(nCtx)
     }
diff --git a/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/ArrayTest.kt b/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/ArrayTest.kt
new file mode 100644
index 000000000..a7249bd81
--- /dev/null
+++ b/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/ArrayTest.kt
@@ -0,0 +1,141 @@
+package org.ksmt.solver.z3
+
+import com.microsoft.z3.Context
+import org.ksmt.KContext
+import org.ksmt.expr.KExpr
+import org.ksmt.sort.KSort
+import org.ksmt.utils.getValue
+import kotlin.test.Test
+import kotlin.test.assertEquals
+
+class ArrayTest {
+
+    @Test
+    fun testArrayConversion(): Unit = with(KContext()) {
+        val sort = mkArraySort(bv32Sort, bv64Sort)
+
+        val array by sort
+        val index by bv32Sort
+        val value by bv64Sort
+        val decl = mkFuncDecl("F", bv64Sort, listOf(bv32Sort))
+
+        testArrayConvert(
+            mkConst = { mkArrayConst(sort, value) },
+            mkSelect = { mkArraySelect(array, index) },
+            mkStore = { mkArrayStore(array, index, value) },
+            mkLambda = { mkArrayLambda(index.decl, mkArraySelect(array, index)) },
+            mkAsArray = { mkFunctionAsArray(sort, decl) }
+        )
+    }
+
+    @Test
+    fun testArray2Conversion(): Unit = with(KContext()) {
+        val sort = mkArraySort(bv32Sort, bv8Sort, bv64Sort)
+
+        val array by sort
+        val index0 by bv32Sort
+        val index1 by bv8Sort
+        val value by bv64Sort
+        val decl = mkFuncDecl("F", bv64Sort, listOf(bv32Sort, bv8Sort))
+
+        testArrayConvert(
+            mkConst = { mkArrayConst(sort, value) },
+            mkSelect = { mkArraySelect(array, index0, index1) },
+            mkStore = { mkArrayStore(array, index0, index1, value) },
+            mkLambda = { mkArrayLambda(index0.decl, index1.decl, mkArraySelect(array, index0, index1)) },
+            mkAsArray = { mkFunctionAsArray(sort, decl) }
+        )
+    }
+
+    @Test
+    fun testArray3Conversion(): Unit = with(KContext()) {
+        val sort = mkArraySort(bv32Sort, bv8Sort, bv16Sort, bv64Sort)
+
+        val array by sort
+        val index0 by bv32Sort
+        val index1 by bv8Sort
+        val index2 by bv16Sort
+        val value by bv64Sort
+        val decl = mkFuncDecl("F", bv64Sort, listOf(bv32Sort, bv8Sort, bv16Sort))
+
+        testArrayConvert(
+            mkConst = { mkArrayConst(sort, value) },
+            mkSelect = { mkArraySelect(array, index0, index1, index2) },
+            mkStore = { mkArrayStore(array, index0, index1, index2, value) },
+            mkLambda = {
+                mkArrayLambda(
+                    index0.decl, index1.decl, index2.decl,
+                    mkArraySelect(array, index0, index1, index2)
+                )
+            },
+            mkAsArray = { mkFunctionAsArray(sort, decl) }
+        )
+    }
+
+    @Test
+    fun testArrayNConversion(): Unit = with(KContext()) {
+        val domain = listOf(bv32Sort, bv8Sort, bv32Sort, bv8Sort, bv32Sort)
+        val sort = mkArrayNSort(domain, bv64Sort)
+
+        val array by sort
+        val indices = domain.mapIndexed { i, s -> mkConst("x$i", s) }
+        val value by bv64Sort
+        val decl = mkFuncDecl("F", bv64Sort, domain)
+
+        testArrayConvert(
+            mkConst = { mkArrayConst(sort, value) },
+            mkSelect = { mkArrayNSelect(array, indices) },
+            mkStore = { mkArrayNStore(array, indices, value) },
+            mkLambda = { mkArrayNLambda(indices.map { it.decl }, mkArrayNSelect(array, indices)) },
+            mkAsArray = { mkFunctionAsArray(sort, decl) }
+        )
+    }
+
+    private inline fun KContext.testArrayConvert(
+        mkConst: KContext.() -> KExpr<*>,
+        mkSelect: KContext.() -> KExpr<*>,
+        mkStore: KContext.() -> KExpr<*>,
+        mkLambda: KContext.() -> KExpr<*>,
+        mkAsArray: KContext.() -> KExpr<*>
+    ) {
+        val const = mkConst()
+        val select = mkSelect()
+        val store = mkStore()
+        val lambda = mkLambda()
+        val asArray = mkAsArray()
+
+        val ctx = this
+        Context().use { z3Native ->
+            val z3InternCtx = KZ3Context(z3Native)
+            val z3ConvertCtx = KZ3Context(z3Native)
+
+            with(KZ3ExprInternalizer(ctx, z3InternCtx)) {
+                val iConst = const.internalizeExprWrapped().simplify()
+                val iSelect = select.internalizeExprWrapped().simplify()
+                val iStore = store.internalizeExprWrapped().simplify()
+                val iLambda = lambda.internalizeExprWrapped().simplify()
+                val iAsArray = asArray.internalizeExprWrapped().simplify()
+
+                with(KZ3ExprConverter(ctx, z3ConvertCtx)) {
+                    val cConst = iConst.convertExprWrapped<KSort>()
+                    val cSelect = iSelect.convertExprWrapped<KSort>()
+                    val cStore = iStore.convertExprWrapped<KSort>()
+                    val cLambda = iLambda.convertExprWrapped<KSort>()
+                    val cAsArray = iAsArray.convertExprWrapped<KSort>()
+
+                    assertEquals(const, cConst)
+                    assertEquals(select, cSelect)
+                    assertEquals(store, cStore)
+                    assertEquals(lambda, cLambda)
+                    assertEquals(asArray, cAsArray)
+                }
+            }
+        }
+    }
+
+    companion object {
+        init {
+            KZ3Solver(KContext()).close()
+        }
+    }
+}