diff --git a/README.md b/README.md
index 9d31e14a0..66b014e5f 100644
--- a/README.md
+++ b/README.md
@@ -14,9 +14,9 @@ repositories {
 }
 
 // core 
-implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.4")
+implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.5")
 // z3 solver
-implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.4")
+implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.5")
 ```
 
 ## Usage
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 84f026226..bc51e1a49 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.4"
+version = "0.4.5"
 
 repositories {
     mavenCentral()
diff --git a/docs/getting-started.md b/docs/getting-started.md
index 087dbc06c..07adf1cea 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.4")    
+    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.5")    
 }
 ```
 
@@ -26,9 +26,9 @@ dependencies {
 ```kotlin
 dependencies {
     // z3 
-    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.4")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.5")
     // bitwuzla
-    implementation("com.github.UnitTestBot.ksmt:ksmt-bitwuzla:0.4.4")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-bitwuzla:0.4.5")
 }
 ```
 SMT solver specific packages are provided with solver native binaries. 
diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts
index 34769886f..5aacab819 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.4")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.5")
     // z3 solver
-    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.4")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.5")
 }
 
 java {
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/KContext.kt b/ksmt-core/src/main/kotlin/org/ksmt/KContext.kt
index 8c05ed1c1..7c3452912 100644
--- a/ksmt-core/src/main/kotlin/org/ksmt/KContext.kt
+++ b/ksmt-core/src/main/kotlin/org/ksmt/KContext.kt
@@ -291,7 +291,6 @@ import org.ksmt.expr.KUnaryMinusArithExpr
 import org.ksmt.expr.KUniversalQuantifier
 import org.ksmt.expr.KXorExpr
 import org.ksmt.expr.rewrite.simplify.simplifyAnd
-import org.ksmt.expr.rewrite.simplify.simplifyAndNoFlat
 import org.ksmt.expr.rewrite.simplify.simplifyArithAdd
 import org.ksmt.expr.rewrite.simplify.simplifyArithDiv
 import org.ksmt.expr.rewrite.simplify.simplifyArithGe
@@ -392,7 +391,6 @@ import org.ksmt.expr.rewrite.simplify.simplifyIntToReal
 import org.ksmt.expr.rewrite.simplify.simplifyIte
 import org.ksmt.expr.rewrite.simplify.simplifyNot
 import org.ksmt.expr.rewrite.simplify.simplifyOr
-import org.ksmt.expr.rewrite.simplify.simplifyOrNoFlat
 import org.ksmt.expr.rewrite.simplify.simplifyRealIsInt
 import org.ksmt.expr.rewrite.simplify.simplifyRealToFpExpr
 import org.ksmt.expr.rewrite.simplify.simplifyRealToInt
@@ -666,17 +664,56 @@ open class KContext(
     private val andNaryCache = mkAstInterner<KAndNaryExpr>()
     private val andBinaryCache = mkAstInterner<KAndBinaryExpr>()
 
-    open fun mkAnd(args: List<KExpr<KBoolSort>>): KExpr<KBoolSort> =
-        mkSimplified(args, KContext::simplifyAnd, ::mkAndNoSimplify)
+    /**
+     * Create boolean AND expression.
+     *
+     * @param flat flat nested AND expressions
+     * @param order reorder arguments to ensure that (and a b) == (and b a)
+     * */
+    @JvmOverloads
+    open fun mkAnd(
+        args: List<KExpr<KBoolSort>>,
+        flat: Boolean = true,
+        order: Boolean = true
+    ): KExpr<KBoolSort> = mkSimplified(
+        args,
+        simplifier = { exprArgs -> simplifyAnd(exprArgs, flat, order) },
+        createNoSimplify = ::mkAndNoSimplify
+    )
 
+    @Deprecated(
+        "NoFlat builders are deprecated",
+        replaceWith = ReplaceWith("mkAnd(args, flat = false)"),
+        level = DeprecationLevel.ERROR
+    )
     open fun mkAndNoFlat(args: List<KExpr<KBoolSort>>): KExpr<KBoolSort> =
-        mkSimplified(args, KContext::simplifyAndNoFlat, ::mkAndNoSimplify)
+        mkAnd(args, flat = false)
 
-    open fun mkAnd(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>): KExpr<KBoolSort> =
-        mkSimplified(lhs, rhs, KContext::simplifyAnd, ::mkAndNoSimplify)
+    /**
+     * Create boolean binary AND expression.
+     *
+     * @param flat flat nested AND expressions
+     * @param order reorder arguments to ensure that (and a b) == (and b a)
+     * */
+    @JvmOverloads
+    open fun mkAnd(
+        lhs: KExpr<KBoolSort>,
+        rhs: KExpr<KBoolSort>,
+        flat: Boolean = true,
+        order: Boolean = true
+    ): KExpr<KBoolSort> = mkSimplified(
+        lhs, rhs,
+        simplifier = { a, b -> simplifyAnd(a, b, flat, order) },
+        createNoSimplify = ::mkAndNoSimplify
+    )
 
+    @Deprecated(
+        "NoFlat builders are deprecated",
+        replaceWith = ReplaceWith("mkAnd(lhs, rhs, flat = false)"),
+        level = DeprecationLevel.ERROR
+    )
     open fun mkAndNoFlat(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>): KExpr<KBoolSort> =
-        mkSimplified(lhs, rhs, KContext::simplifyAndNoFlat, ::mkAndNoSimplify)
+        mkAnd(lhs, rhs, flat = false)
 
     open fun mkAndNoSimplify(args: List<KExpr<KBoolSort>>): KAndExpr =
         if (args.size == 2) {
@@ -697,17 +734,56 @@ open class KContext(
     private val orNaryCache = mkAstInterner<KOrNaryExpr>()
     private val orBinaryCache = mkAstInterner<KOrBinaryExpr>()
 
-    open fun mkOr(args: List<KExpr<KBoolSort>>): KExpr<KBoolSort> =
-        mkSimplified(args, KContext::simplifyOr, ::mkOrNoSimplify)
+    /**
+     * Create boolean OR expression.
+     *
+     * @param flat flat nested OR expressions
+     * @param order reorder arguments to ensure that (or a b) == (or b a)
+     * */
+    @JvmOverloads
+    open fun mkOr(
+        args: List<KExpr<KBoolSort>>,
+        flat: Boolean = true,
+        order: Boolean = true
+    ): KExpr<KBoolSort> = mkSimplified(
+        args,
+        simplifier = { exprArgs -> simplifyOr(exprArgs, flat, order) },
+        createNoSimplify = ::mkOrNoSimplify
+    )
 
+    @Deprecated(
+        "NoFlat builders are deprecated",
+        replaceWith = ReplaceWith("mkOr(args, flat = false)"),
+        level = DeprecationLevel.ERROR
+    )
     open fun mkOrNoFlat(args: List<KExpr<KBoolSort>>): KExpr<KBoolSort> =
-        mkSimplified(args, KContext::simplifyOrNoFlat, ::mkOrNoSimplify)
+        mkOr(args, flat = false)
 
-    open fun mkOr(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>): KExpr<KBoolSort> =
-        mkSimplified(lhs, rhs, KContext::simplifyOr, ::mkOrNoSimplify)
+    /**
+     * Create boolean binary OR expression.
+     *
+     * @param flat flat nested OR expressions
+     * @param order reorder arguments to ensure that (or a b) == (or b a)
+     * */
+    @JvmOverloads
+    open fun mkOr(
+        lhs: KExpr<KBoolSort>,
+        rhs: KExpr<KBoolSort>,
+        flat: Boolean = true,
+        order: Boolean = true
+    ): KExpr<KBoolSort> = mkSimplified(
+        lhs, rhs,
+        simplifier = { a, b -> simplifyOr(a, b, flat, order) },
+        createNoSimplify = ::mkOrNoSimplify
+    )
 
+    @Deprecated(
+        "NoFlat builders are deprecated",
+        replaceWith = ReplaceWith("mkOr(lhs, rhs, flat = false)"),
+        level = DeprecationLevel.ERROR
+    )
     open fun mkOrNoFlat(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>): KExpr<KBoolSort> =
-        mkSimplified(lhs, rhs, KContext::simplifyOrNoFlat, ::mkOrNoSimplify)
+        mkOr(lhs, rhs, flat = false)
 
     open fun mkOrNoSimplify(args: List<KExpr<KBoolSort>>): KOrExpr =
         if (args.size == 2) {
@@ -767,8 +843,21 @@ open class KContext(
 
     private val eqCache = mkAstInterner<KEqExpr<out KSort>>()
 
-    open fun <T : KSort> mkEq(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort> =
-        mkSimplified(lhs, rhs, KContext::simplifyEq, ::mkEqNoSimplify)
+    /**
+     * Create EQ expression.
+     *
+     * @param order reorder arguments to ensure that (= a b) == (= b a)
+     * */
+    @JvmOverloads
+    open fun <T : KSort> mkEq(
+        lhs: KExpr<T>,
+        rhs: KExpr<T>,
+        order: Boolean = true
+    ): KExpr<KBoolSort> = mkSimplified(
+        lhs, rhs,
+        simplifier = { l, r -> simplifyEq(l, r, order) },
+        createNoSimplify = ::mkEqNoSimplify
+    )
 
     open fun <T : KSort> mkEqNoSimplify(lhs: KExpr<T>, rhs: KExpr<T>): KEqExpr<T> =
         eqCache.createIfContextActive {
@@ -778,8 +867,20 @@ open class KContext(
 
     private val distinctCache = mkAstInterner<KDistinctExpr<out KSort>>()
 
-    open fun <T : KSort> mkDistinct(args: List<KExpr<T>>): KExpr<KBoolSort> =
-        mkSimplified(args, KContext::simplifyDistinct, ::mkDistinctNoSimplify)
+    /**
+     * Create DISTINCT expression.
+     *
+     * @param order reorder arguments to ensure that (distinct a b) == (distinct b a)
+     * */
+    @JvmOverloads
+    open fun <T : KSort> mkDistinct(
+        args: List<KExpr<T>>,
+        order: Boolean = true
+    ): KExpr<KBoolSort> = mkSimplified(
+        args,
+        simplifier = { exprArgs -> simplifyDistinct(exprArgs, order) },
+        createNoSimplify = ::mkDistinctNoSimplify
+    )
 
     open fun <T : KSort> mkDistinctNoSimplify(args: List<KExpr<T>>): KDistinctExpr<T> =
         distinctCache.createIfContextActive {
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/BoolSimplification.kt b/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/BoolSimplification.kt
index 6c92555fa..eb345977e 100644
--- a/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/BoolSimplification.kt
+++ b/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/BoolSimplification.kt
@@ -20,48 +20,32 @@ fun KContext.simplifyNot(arg: KExpr<KBoolSort>): KExpr<KBoolSort> = when (arg) {
     else -> mkNotNoSimplify(arg)
 }
 
-fun KContext.simplifyAnd(args: List<KExpr<KBoolSort>>): KExpr<KBoolSort> =
-    simplifyAndCore(args, flat = true)
-
-fun KContext.simplifyOr(args: List<KExpr<KBoolSort>>): KExpr<KBoolSort> =
-    simplifyOrCore(args, flat = true)
-
-fun KContext.simplifyAndNoFlat(args: List<KExpr<KBoolSort>>): KExpr<KBoolSort> =
-    simplifyAndCore(args, flat = false)
-
-fun KContext.simplifyOrNoFlat(args: List<KExpr<KBoolSort>>): KExpr<KBoolSort> =
-    simplifyOrCore(args, flat = false)
-
-fun KContext.simplifyAnd(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>): KExpr<KBoolSort> =
-    simplifyAndCore(lhs, rhs, flat = true)
-
-fun KContext.simplifyOr(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>): KExpr<KBoolSort> =
-    simplifyOrCore(lhs, rhs, flat = true)
-
-fun KContext.simplifyAndNoFlat(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>): KExpr<KBoolSort> =
-    simplifyAndCore(lhs, rhs, flat = false)
-
-fun KContext.simplifyOrNoFlat(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>): KExpr<KBoolSort> =
-    simplifyOrCore(lhs, rhs, flat = false)
-
 fun KContext.simplifyImplies(p: KExpr<KBoolSort>, q: KExpr<KBoolSort>): KExpr<KBoolSort> =
     simplifyOr(simplifyNot(p), q)
 
 fun KContext.simplifyXor(a: KExpr<KBoolSort>, b: KExpr<KBoolSort>): KExpr<KBoolSort> =
     simplifyEq(simplifyNot(a), b)
 
-fun <T : KSort> KContext.simplifyEq(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort> = when {
+fun <T : KSort> KContext.simplifyEq(
+    lhs: KExpr<T>,
+    rhs: KExpr<T>,
+    order: Boolean = true
+): KExpr<KBoolSort> = when {
     lhs == rhs -> trueExpr
     lhs is KInterpretedValue<T> && rhs is KInterpretedValue<T> && lhs != rhs -> falseExpr
-    lhs.sort == boolSort -> simplifyEqBool(lhs.uncheckedCast(), rhs.uncheckedCast())
+    lhs.sort == boolSort -> simplifyEqBool(lhs.uncheckedCast(), rhs.uncheckedCast(), order)
+    order -> withExpressionsOrdered(lhs, rhs, ::mkEqNoSimplify)
     else -> mkEqNoSimplify(lhs, rhs)
 }
 
-fun <T : KSort> KContext.simplifyDistinct(args: List<KExpr<T>>): KExpr<KBoolSort> {
+fun <T : KSort> KContext.simplifyDistinct(
+    args: List<KExpr<T>>,
+    order: Boolean = true
+): KExpr<KBoolSort> {
     if (args.isEmpty() || args.size == 1) return trueExpr
 
     // (distinct a b) ==> (not (= a b))
-    if (args.size == 2) return simplifyNot(simplifyEq(args[0], args[1]))
+    if (args.size == 2) return simplifyNot(simplifyEq(args[0], args[1], order))
 
     // (distinct a b a) ==> false
     val distinctArgs = args.toSet()
@@ -70,7 +54,14 @@ fun <T : KSort> KContext.simplifyDistinct(args: List<KExpr<T>>): KExpr<KBoolSort
     // All arguments are not equal and all are interpreted values ==> all are distinct
     if (args.all { it is KInterpretedValue<*> }) return trueExpr
 
-    return mkDistinctNoSimplify(args)
+    return if (order) {
+        val orderedArgs = args.toMutableList().apply {
+            ensureExpressionsOrder()
+        }
+        mkDistinctNoSimplify(orderedArgs)
+    } else {
+        mkDistinctNoSimplify(args)
+    }
 }
 
 fun <T : KSort> KContext.simplifyIte(
@@ -129,10 +120,14 @@ fun <T : KSort> KContext.simplifyIte(
 }
 
 
-fun KContext.simplifyEqBool(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>): KExpr<KBoolSort> {
+fun KContext.simplifyEqBool(
+    lhs: KExpr<KBoolSort>,
+    rhs: KExpr<KBoolSort>,
+    order: Boolean = true
+): KExpr<KBoolSort> {
     // (= (not a) (not b)) ==> (= a b)
     if (lhs is KNotExpr && rhs is KNotExpr) {
-        return simplifyEq(lhs.arg, rhs.arg)
+        return simplifyEq(lhs.arg, rhs.arg, order)
     }
 
     when (lhs) {
@@ -150,7 +145,11 @@ fun KContext.simplifyEqBool(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>): KExpr
         return falseExpr
     }
 
-    return mkEqNoSimplify(lhs, rhs)
+    return if (order) {
+        withExpressionsOrdered(lhs, rhs, ::mkEqNoSimplify)
+    } else {
+        mkEqNoSimplify(lhs, rhs)
+    }
 }
 
 fun KExpr<KBoolSort>.isComplement(other: KExpr<KBoolSort>) =
@@ -159,57 +158,72 @@ fun KExpr<KBoolSort>.isComplement(other: KExpr<KBoolSort>) =
 private fun KContext.isComplementCore(a: KExpr<KBoolSort>, b: KExpr<KBoolSort>) =
     (a == trueExpr && b == falseExpr) || (a is KNotExpr && a.arg == b)
 
-fun KContext.simplifyAndCore(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>, flat: Boolean): KExpr<KBoolSort> =
-    simplifyAndOr<KAndExpr>(
-        flat = flat,
-        lhs = lhs, rhs = rhs,
-        // (and a b true) ==> (and a b)
-        neutralElement = trueExpr,
-        // (and a b false) ==> false
-        zeroElement = falseExpr,
-        buildResultBinaryExpr = { simplifiedLhs, simplifiedRhs -> mkAndNoSimplify(simplifiedLhs, simplifiedRhs) },
-        buildResultFlatExpr = { simplifiedArgs -> mkAndNoSimplify(simplifiedArgs) }
-    )
-
-fun KContext.simplifyAndCore(args: List<KExpr<KBoolSort>>, flat: Boolean): KExpr<KBoolSort> =
-    simplifyAndOr<KAndExpr>(
-        flat = flat,
-        args = args,
-        // (and a b true) ==> (and a b)
-        neutralElement = trueExpr,
-        // (and a b false) ==> false
-        zeroElement = falseExpr,
-        buildResultBinaryExpr = { simplifiedLhs, simplifiedRhs -> mkAndNoSimplify(simplifiedLhs, simplifiedRhs) },
-        buildResultFlatExpr = { simplifiedArgs -> mkAndNoSimplify(simplifiedArgs) }
-    )
-
-fun KContext.simplifyOrCore(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>, flat: Boolean): KExpr<KBoolSort> =
-    simplifyAndOr<KOrExpr>(
-        flat = flat,
-        lhs = lhs, rhs = rhs,
-        // (or a b false) ==> (or a b)
-        neutralElement = falseExpr,
-        // (or a b true) ==> true
-        zeroElement = trueExpr,
-        buildResultBinaryExpr = { simplifiedLhs, simplifiedRhs -> mkOrNoSimplify(simplifiedLhs, simplifiedRhs) },
-        buildResultFlatExpr = { simplifiedArgs -> mkOrNoSimplify(simplifiedArgs) }
-    )
-
-fun KContext.simplifyOrCore(args: List<KExpr<KBoolSort>>, flat: Boolean): KExpr<KBoolSort> =
-    simplifyAndOr<KOrExpr>(
-        flat = flat,
-        args = args,
-        // (or a b false) ==> (or a b)
-        neutralElement = falseExpr,
-        // (or a b true) ==> true
-        zeroElement = trueExpr,
-        buildResultBinaryExpr = { simplifiedLhs, simplifiedRhs -> mkOrNoSimplify(simplifiedLhs, simplifiedRhs) },
-        buildResultFlatExpr = { simplifiedArgs -> mkOrNoSimplify(simplifiedArgs) }
-    )
+fun KContext.simplifyAnd(
+    lhs: KExpr<KBoolSort>,
+    rhs: KExpr<KBoolSort>,
+    flat: Boolean = true,
+    order: Boolean = true
+): KExpr<KBoolSort> = simplifyAndOr<KAndExpr>(
+    flat = flat, order = order,
+    lhs = lhs, rhs = rhs,
+    // (and a b true) ==> (and a b)
+    neutralElement = trueExpr,
+    // (and a b false) ==> false
+    zeroElement = falseExpr,
+    buildResultBinaryExpr = { simplifiedLhs, simplifiedRhs -> mkAndNoSimplify(simplifiedLhs, simplifiedRhs) },
+    buildResultFlatExpr = { simplifiedArgs -> mkAndNoSimplify(simplifiedArgs) }
+)
+
+fun KContext.simplifyAnd(
+    args: List<KExpr<KBoolSort>>,
+    flat: Boolean = true,
+    order: Boolean = true
+): KExpr<KBoolSort> = simplifyAndOr<KAndExpr>(
+    flat = flat, order = order,
+    args = args,
+    // (and a b true) ==> (and a b)
+    neutralElement = trueExpr,
+    // (and a b false) ==> false
+    zeroElement = falseExpr,
+    buildResultBinaryExpr = { simplifiedLhs, simplifiedRhs -> mkAndNoSimplify(simplifiedLhs, simplifiedRhs) },
+    buildResultFlatExpr = { simplifiedArgs -> mkAndNoSimplify(simplifiedArgs) }
+)
+
+fun KContext.simplifyOr(
+    lhs: KExpr<KBoolSort>,
+    rhs: KExpr<KBoolSort>,
+    flat: Boolean = true,
+    order: Boolean = true
+): KExpr<KBoolSort> = simplifyAndOr<KOrExpr>(
+    flat = flat, order = order,
+    lhs = lhs, rhs = rhs,
+    // (or a b false) ==> (or a b)
+    neutralElement = falseExpr,
+    // (or a b true) ==> true
+    zeroElement = trueExpr,
+    buildResultBinaryExpr = { simplifiedLhs, simplifiedRhs -> mkOrNoSimplify(simplifiedLhs, simplifiedRhs) },
+    buildResultFlatExpr = { simplifiedArgs -> mkOrNoSimplify(simplifiedArgs) }
+)
+
+fun KContext.simplifyOr(
+    args: List<KExpr<KBoolSort>>,
+    flat: Boolean = true,
+    order: Boolean = true
+): KExpr<KBoolSort> = simplifyAndOr<KOrExpr>(
+    flat = flat, order = order,
+    args = args,
+    // (or a b false) ==> (or a b)
+    neutralElement = falseExpr,
+    // (or a b true) ==> true
+    zeroElement = trueExpr,
+    buildResultBinaryExpr = { simplifiedLhs, simplifiedRhs -> mkOrNoSimplify(simplifiedLhs, simplifiedRhs) },
+    buildResultFlatExpr = { simplifiedArgs -> mkOrNoSimplify(simplifiedArgs) }
+)
 
 @Suppress("LongParameterList")
 private inline fun <reified T : KApp<KBoolSort, KBoolSort>> simplifyAndOr(
     flat: Boolean,
+    order: Boolean,
     args: List<KExpr<KBoolSort>>,
     neutralElement: KExpr<KBoolSort>,
     zeroElement: KExpr<KBoolSort>,
@@ -219,7 +233,7 @@ private inline fun <reified T : KApp<KBoolSort, KBoolSort>> simplifyAndOr(
     0 -> neutralElement
     1 -> args.single()
     2 -> simplifyAndOr(
-        flat = flat,
+        flat = flat, order = order,
         lhs = args.first(), rhs = args.last(),
         neutralElement = neutralElement,
         zeroElement = zeroElement,
@@ -227,7 +241,7 @@ private inline fun <reified T : KApp<KBoolSort, KBoolSort>> simplifyAndOr(
         buildResultFlatExpr = buildResultFlatExpr
     )
     else -> simplifyAndOr(
-        flat = flat,
+        flat = flat, order = order,
         args = args,
         neutralElement = neutralElement,
         zeroElement = zeroElement,
@@ -238,6 +252,7 @@ private inline fun <reified T : KApp<KBoolSort, KBoolSort>> simplifyAndOr(
 @Suppress("LongParameterList")
 private inline fun <reified T : KApp<KBoolSort, KBoolSort>> simplifyAndOr(
     flat: Boolean,
+    order: Boolean,
     lhs: KExpr<KBoolSort>,
     rhs: KExpr<KBoolSort>,
     neutralElement: KExpr<KBoolSort>,
@@ -247,7 +262,7 @@ private inline fun <reified T : KApp<KBoolSort, KBoolSort>> simplifyAndOr(
 ): KExpr<KBoolSort> {
     if (flat && (lhs is T || rhs is T)) {
         return simplifyAndOr(
-            flat = true,
+            flat = true, order = order,
             args = listOf(lhs, rhs),
             neutralElement = neutralElement,
             zeroElement = zeroElement
@@ -260,13 +275,15 @@ private inline fun <reified T : KApp<KBoolSort, KBoolSort>> simplifyAndOr(
         lhs == neutralElement -> rhs
         rhs == neutralElement -> lhs
         lhs.isComplement(rhs) -> zeroElement
+        order -> withExpressionsOrdered(lhs, rhs) { l, r -> buildResultBinaryExpr(l, r) }
         else -> buildResultBinaryExpr(lhs, rhs)
     }
 }
 
-@Suppress("NestedBlockDepth")
+@Suppress("NestedBlockDepth", "LongParameterList")
 private inline fun <reified T : KApp<KBoolSort, KBoolSort>> simplifyAndOr(
     flat: Boolean,
+    order: Boolean,
     args: List<KExpr<KBoolSort>>,
     neutralElement: KExpr<KBoolSort>,
     zeroElement: KExpr<KBoolSort>,
@@ -292,7 +309,12 @@ private inline fun <reified T : KApp<KBoolSort, KBoolSort>> simplifyAndOr(
     return when (resultArgs.size) {
         0 -> neutralElement
         1 -> resultArgs.single()
-        else -> buildResultExpr(resultArgs)
+        else -> {
+            if (order) {
+                resultArgs.ensureExpressionsOrder()
+            }
+            buildResultExpr(resultArgs)
+        }
     }
 }
 
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/ExpressionOrdering.kt b/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/ExpressionOrdering.kt
new file mode 100644
index 000000000..66a4d4e6d
--- /dev/null
+++ b/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/ExpressionOrdering.kt
@@ -0,0 +1,41 @@
+package org.ksmt.expr.rewrite.simplify
+
+import org.ksmt.expr.KConst
+import org.ksmt.expr.KExpr
+import org.ksmt.expr.KInterpretedValue
+import org.ksmt.sort.KSort
+
+object ExpressionOrdering : Comparator<KExpr<*>> {
+    override fun compare(left: KExpr<*>, right: KExpr<*>): Int = when (left) {
+        is KInterpretedValue<*> -> when (right) {
+            is KInterpretedValue<*> -> compareDefault(left, right)
+            else -> -1
+        }
+
+        is KConst<*> -> when (right) {
+            is KInterpretedValue<*> -> 1
+            is KConst<*> -> compareDefault(left, right)
+            else -> -1
+        }
+
+        else -> compareDefault(left, right)
+    }
+
+    @JvmStatic
+    private fun compareDefault(left: KExpr<*>?, right: KExpr<*>?): Int =
+        System.identityHashCode(left).compareTo(System.identityHashCode(right))
+}
+
+inline fun <T : KSort, R> withExpressionsOrdered(
+    lhs: KExpr<T>,
+    rhs: KExpr<T>,
+    body: (KExpr<T>, KExpr<T>) -> R
+): R = if (ExpressionOrdering.compare(lhs, rhs) <= 0) {
+    body(lhs, rhs)
+} else {
+    body(rhs, lhs)
+}
+
+fun <T : KSort> MutableList<KExpr<T>>.ensureExpressionsOrder() {
+    sortWith(ExpressionOrdering)
+}
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/KArithExprSimplifier.kt b/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/KArithExprSimplifier.kt
index e55362b1b..5d901f015 100644
--- a/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/KArithExprSimplifier.kt
+++ b/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/KArithExprSimplifier.kt
@@ -34,7 +34,7 @@ interface KArithExprSimplifier : KExprSimplifierBase {
             return (lhs.compareTo(rhs) == 0).expr
         }
 
-        return mkEqNoSimplify(lhs, rhs)
+        withExpressionsOrdered(lhs, rhs, ::mkEqNoSimplify)
     }
 
     fun areDefinitelyDistinctInt(lhs: KExpr<KIntSort>, rhs: KExpr<KIntSort>): Boolean {
@@ -51,7 +51,7 @@ interface KArithExprSimplifier : KExprSimplifierBase {
             return (lhs.toRealValue().compareTo(rhs.toRealValue()) == 0).expr
         }
 
-        return mkEqNoSimplify(lhs, rhs)
+        return withExpressionsOrdered(lhs, rhs, ::mkEqNoSimplify)
     }
 
     fun areDefinitelyDistinctReal(lhs: KExpr<KRealSort>, rhs: KExpr<KRealSort>): Boolean {
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 241d8ff97..474c4f66b 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
@@ -62,7 +62,7 @@ interface KArrayExprSimplifier : KExprSimplifierBase {
             return rewrite(simplifiedExpr)
         }
 
-        return mkEqNoSimplify(lhs, rhs)
+        return withExpressionsOrdered(lhs, rhs, ::mkEqNoSimplify)
     }
 
     /**
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/KBoolExprSimplifier.kt b/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/KBoolExprSimplifier.kt
index e3017b404..8a9384281 100644
--- a/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/KBoolExprSimplifier.kt
+++ b/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/KBoolExprSimplifier.kt
@@ -152,32 +152,11 @@ interface KBoolExprSimplifier : KExprSimplifierBase {
     )
 
     fun simplifyEqBool(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>): KExpr<KBoolSort> =
-        ctx.simplifyEqBool(lhs, rhs)
+        ctx.simplifyEqBool(lhs, rhs, order = true)
 
     fun areDefinitelyDistinctBool(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>): Boolean =
         lhs.isComplement(rhs)
 
-    private fun flatAnd(expr: KAndExpr) = flatExpr<KAndExpr>(expr) { it.args }
-    private fun flatOr(expr: KOrExpr) = flatExpr<KOrExpr>(expr) { it.args }
-
-    private inline fun <reified T> flatExpr(
-        initial: KExpr<KBoolSort>,
-        getArgs: (T) -> List<KExpr<KBoolSort>>,
-    ): List<KExpr<KBoolSort>> {
-        val flatten = arrayListOf<KExpr<KBoolSort>>()
-        val unprocessed = arrayListOf<KExpr<KBoolSort>>()
-        unprocessed += initial
-        while (unprocessed.isNotEmpty()) {
-            val e = unprocessed.removeLast()
-            if (e !is T) {
-                flatten += e
-                continue
-            }
-            unprocessed += getArgs(e).asReversed()
-        }
-        return flatten
-    }
-
     /**
      * Auxiliary expression to perform ite condition (1) simplification stage.
      * Check out [KIteExpr] simplification.
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/KBvExprSimplifier.kt b/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/KBvExprSimplifier.kt
index fd5db58e0..3d960b428 100644
--- a/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/KBvExprSimplifier.kt
+++ b/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/KBvExprSimplifier.kt
@@ -104,7 +104,7 @@ interface KBvExprSimplifier : KExprSimplifierBase {
             return rewrite(simplifyBvConcatEq(lhs, rhs))
         }
 
-        mkEqNoSimplify(lhs, rhs)
+        withExpressionsOrdered(lhs, rhs, ::mkEqNoSimplify)
     }
 
     fun <T : KBvSort> areDefinitelyDistinctBv(lhs: KExpr<T>, rhs: KExpr<T>): Boolean {
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 1cee9163b..7eac5e6df 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
@@ -43,14 +43,14 @@ open class KExprSimplifier(override val ctx: KContext) :
     ) { lhs, rhs ->
         if (lhs == rhs) return@simplifyExpr trueExpr
         when (lhs.sort) {
-            boolSort -> simplifyEqBool(lhs.uncheckedCast(), rhs.uncheckedCast())
+            boolSort -> this@KExprSimplifier.simplifyEqBool(lhs.uncheckedCast(), rhs.uncheckedCast())
             intSort -> simplifyEqInt(lhs.uncheckedCast(), rhs.uncheckedCast())
             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 KArraySortBase<*> -> simplifyEqArray(lhs as KExpr<KArraySortBase<KSort>>, rhs.uncheckedCast())
             is KUninterpretedSort -> simplifyEqUninterpreted(lhs.uncheckedCast(), rhs.uncheckedCast())
-            else -> mkEqNoSimplify(lhs, rhs)
+            else -> withExpressionsOrdered(lhs, rhs, ::mkEqNoSimplify)
         }
     }
 
@@ -252,7 +252,7 @@ open class KExprSimplifier(override val ctx: KContext) :
     open fun simplifyEqUninterpreted(
         lhs: KExpr<KUninterpretedSort>,
         rhs: KExpr<KUninterpretedSort>
-    ): KExpr<KBoolSort> = ctx.mkEqNoSimplify(lhs, rhs)
+    ): KExpr<KBoolSort> = withExpressionsOrdered(lhs, rhs, ctx::mkEqNoSimplify)
 
     open fun areDefinitelyDistinctUninterpreted(
         lhs: KExpr<KUninterpretedSort>,
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/KFpExprSimplifier.kt b/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/KFpExprSimplifier.kt
index 52875ee4f..10f4f7025 100644
--- a/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/KFpExprSimplifier.kt
+++ b/ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/KFpExprSimplifier.kt
@@ -53,7 +53,7 @@ interface KFpExprSimplifier : KExprSimplifierBase {
             return fpStructurallyEqual(lhs, rhs).expr
         }
 
-        return mkEqNoSimplify(lhs, rhs)
+        return withExpressionsOrdered(lhs, rhs, ::mkEqNoSimplify)
     }
 
     fun <T : KFpSort> areDefinitelyDistinctFp(lhs: KExpr<T>, rhs: KExpr<T>): Boolean {
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 9a41efcd0..8f5c26b20 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
@@ -157,16 +157,24 @@ abstract class KNonRecursiveTransformer(override val ctx: KContext) : KNonRecurs
 
     // bool transformers
     override fun transform(expr: KAndExpr): KExpr<KBoolSort> =
-        transformExprAfterTransformedDefault(expr, expr.args, ::transformApp, KContext::mkAnd)
+        transformExprAfterTransformedDefault(
+            expr, expr.args, ::transformApp
+        ) { args -> mkAnd(args, flat = false, order = false) }
 
     override fun transform(expr: KAndBinaryExpr): KExpr<KBoolSort> =
-        transformExprAfterTransformedDefault(expr, expr.lhs, expr.rhs, ::transformApp, KContext::mkAnd)
+        transformExprAfterTransformedDefault(
+            expr, expr.lhs, expr.rhs, ::transformApp
+        ) { l, r -> mkAnd(l, r, flat = false, order = false) }
 
     override fun transform(expr: KOrExpr): KExpr<KBoolSort> =
-        transformExprAfterTransformedDefault(expr, expr.args, ::transformApp, KContext::mkOr)
+        transformExprAfterTransformedDefault(
+            expr, expr.args, ::transformApp
+        ) { args -> mkOr(args, flat = false) }
 
     override fun transform(expr: KOrBinaryExpr): KExpr<KBoolSort> =
-        transformExprAfterTransformedDefault(expr, expr.lhs, expr.rhs, ::transformApp, KContext::mkOr)
+        transformExprAfterTransformedDefault(
+            expr, expr.lhs, expr.rhs, ::transformApp
+        ) { l, r -> mkOr(l, r, flat = false, order = false) }
 
     override fun transform(expr: KNotExpr): KExpr<KBoolSort> =
         transformExprAfterTransformedDefault(expr, expr.arg, ::transformApp, KContext::mkNot)
@@ -178,10 +186,14 @@ abstract class KNonRecursiveTransformer(override val ctx: KContext) : KNonRecurs
         transformExprAfterTransformedDefault(expr, expr.a, expr.b, ::transformApp, KContext::mkXor)
 
     override fun <T : KSort> transform(expr: KEqExpr<T>): KExpr<KBoolSort> =
-        transformExprAfterTransformedDefault(expr, expr.lhs, expr.rhs, ::transformApp, KContext::mkEq)
+        transformExprAfterTransformedDefault(
+            expr, expr.lhs, expr.rhs, ::transformApp
+        ) { l, r -> mkEq(l, r, order = false) }
 
     override fun <T : KSort> transform(expr: KDistinctExpr<T>): KExpr<KBoolSort> =
-        transformExprAfterTransformedDefault(expr, expr.args, ::transformApp, KContext::mkDistinct)
+        transformExprAfterTransformedDefault(
+            expr, expr.args, ::transformApp
+        ) { args -> mkDistinct(args, order = false) }
 
     override fun <T : KSort> transform(expr: KIteExpr<T>): KExpr<T> =
         transformExprAfterTransformedDefault(
diff --git a/ksmt-core/src/test/kotlin/org/ksmt/SimplifierTest.kt b/ksmt-core/src/test/kotlin/org/ksmt/SimplifierTest.kt
index 80612148c..0c4b0f930 100644
--- a/ksmt-core/src/test/kotlin/org/ksmt/SimplifierTest.kt
+++ b/ksmt-core/src/test/kotlin/org/ksmt/SimplifierTest.kt
@@ -3,6 +3,7 @@ package org.ksmt
 import org.ksmt.KContext.SimplificationMode.NO_SIMPLIFY
 import org.ksmt.expr.KAndExpr
 import org.ksmt.expr.KBitVecValue
+import org.ksmt.expr.KEqExpr
 import org.ksmt.expr.KExpr
 import org.ksmt.expr.rewrite.simplify.KExprSimplifier
 import org.ksmt.sort.KArraySort
@@ -50,8 +51,9 @@ class SimplifierTest {
         val simplifiedEq = KExprSimplifier(this).apply(arrayEq)
         val simplifiedSelects = KExprSimplifier(this).apply(allSelectsEq)
 
-        val simplifiedEqParts = (simplifiedEq as KAndExpr).args
-        val simplifiedAllSelectsParts = (simplifiedSelects as KAndExpr).args
+        // Compare sets of Eq expressions
+        val simplifiedEqParts = (simplifiedEq as KAndExpr).args.map { (it as KEqExpr<*>).args.toSet() }
+        val simplifiedAllSelectsParts = (simplifiedSelects as KAndExpr).args.map { (it as KEqExpr<*>).args.toSet() }
         assertEquals(simplifiedAllSelectsParts.toSet(), simplifiedEqParts.toSet())
     }
 
@@ -197,7 +199,7 @@ class SimplifierTest {
         val simplifiedExpr = KExprSimplifier(this).apply(expr)
 
         assertTrue(simplifiedExpr is KAndExpr)
-        assertEquals(usedVars, simplifiedExpr.args)
+        assertEquals(usedVars.toSet(), simplifiedExpr.args.toSet())
     }
 
 }