diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/AsyncChecker.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/AsyncChecker.kt
index cf83219a7..c5faf9224 100644
--- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/AsyncChecker.kt
+++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/AsyncChecker.kt
@@ -166,11 +166,6 @@ class AsyncChecker(
         val result = AsyncSMTProxySolver(ctx).use {
             it.isPathPossibleAsync(state, query)
         }
-//        val aiResult = tryAbstractDomainSolve(state, query)
-//        if (aiResult is Result.UnsatResult && result !is Result.UnsatResult) {
-//            val a = tryAbstractDomainSolve(state, query)
-//            log.error("AAAAAAAAAAAA")
-//        }
         log.debug("Acquired {}", result)
         return result
     }
diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/state/transformer/domain/AbstractDomain.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/state/transformer/domain/AbstractDomain.kt
index 9dea3848e..0cf299856 100644
--- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/state/transformer/domain/AbstractDomain.kt
+++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/state/transformer/domain/AbstractDomain.kt
@@ -69,6 +69,14 @@ val AbstractDomainValue.isFalse: Boolean
 val AbstractDomainValue.isNull: Boolean
     get() = this is NullDomainValue
 
+val AbstractDomainValue.canBeNull: Boolean
+    get() = when (this) {
+        is NullDomainValue -> true
+        is NullableDomainValue -> true
+        is Top -> true
+        else -> false
+    }
+
 val AbstractDomainValue.isConstant: Boolean
     get() = this is IntervalDomainValue<*> && this.isConstant
 
@@ -233,21 +241,71 @@ data class IntervalDomainValue<T : Number>(val min: T, val max: T) : NumberAbstr
 
     override fun assign(other: AbstractDomainValue): AbstractDomainValue = other
 
+    @Suppress("UNCHECKED_CAST")
+    private fun <T : Number> lowerBound(num: T): T = when (num) {
+        is Byte -> Byte.MIN_VALUE
+        is Short -> Short.MIN_VALUE
+        is Int -> Int.MIN_VALUE
+        is Long -> Long.MIN_VALUE
+        is Float -> Float.NEGATIVE_INFINITY
+        is Double -> Double.NEGATIVE_INFINITY
+        else -> unreachable { log.error("Unknown number impl $num") }
+    } as T
+
+    @Suppress("UNCHECKED_CAST")
+    private fun <T : Number> upperBound(num: T) = when (num) {
+        is Byte -> Byte.MAX_VALUE
+        is Short -> Short.MAX_VALUE
+        is Int -> Int.MAX_VALUE
+        is Long -> Long.MAX_VALUE
+        is Float -> Float.POSITIVE_INFINITY
+        is Double -> Double.POSITIVE_INFINITY
+        else -> unreachable { log.error("Unknown number impl $num") }
+    } as T
+
     override fun apply(opcode: BinaryOpcode, other: AbstractDomainValue): AbstractDomainValue = when (other) {
         is Top -> Top
 
         is IntervalDomainValue<*> -> when (opcode) {
-            BinaryOpcode.ADD -> IntervalDomainValue(other.min + other.min, max + other.max)
-            BinaryOpcode.SUB -> IntervalDomainValue(min - other.max, max + other.min)
-            BinaryOpcode.MUL -> IntervalDomainValue(
-                minOf(min * other.min, max * other.min, min * other.max, max * other.max),
-                maxOf(min * other.min, max * other.min, min * other.max, max * other.max)
-            )
-
-            BinaryOpcode.DIV -> IntervalDomainValue(
-                minOf(min / other.min, max / other.min, min / other.max, max / other.max),
-                maxOf(min / other.min, max / other.min, min / other.max, max / other.max)
-            )
+            BinaryOpcode.ADD -> {
+                val lb = min + other.min
+                val ub = max + other.max
+                when {
+                    lb < min || lb < other.min -> IntervalDomainValue(lowerBound(min), upperBound(max))
+                    ub < max || ub < other.max -> IntervalDomainValue(lowerBound(min), upperBound(max))
+                    else -> IntervalDomainValue(lb, ub)
+                }
+            }
+
+            BinaryOpcode.SUB -> {
+                val lb = min - other.max
+                val ub = max - other.min
+                when {
+                    lb > min -> IntervalDomainValue(lowerBound(min), upperBound(max))
+                    ub < max -> IntervalDomainValue(lowerBound(min), upperBound(max))
+                    else -> IntervalDomainValue(lb, ub)
+                }
+            }
+
+            BinaryOpcode.MUL -> {
+                val lb = minOf(min * other.min, max * other.min, min * other.max, max * other.max)
+                val ub = maxOf(min * other.min, max * other.min, min * other.max, max * other.max)
+                when {
+                    lb > min -> IntervalDomainValue(lowerBound(min), upperBound(max))
+                    ub < max -> IntervalDomainValue(lowerBound(min), upperBound(max))
+                    else -> IntervalDomainValue(lb, ub)
+                }
+            }
+
+            BinaryOpcode.DIV -> {
+                val lb = minOf(min / other.min, max / other.min, min / other.max, max / other.max)
+                val ub = maxOf(min / other.min, max / other.min, min / other.max, max / other.max)
+                when {
+                    lb > min -> IntervalDomainValue(lowerBound(min), upperBound(max))
+                    ub < max -> IntervalDomainValue(lowerBound(min), upperBound(max))
+                    else -> IntervalDomainValue(lb, ub)
+                }
+            }
 
             BinaryOpcode.REM -> when {
                 this.isConstant && other.isConstant -> IntervalDomainValue(min % other.min)
@@ -607,7 +665,11 @@ sealed interface TermDomainValue : AbstractDomainValue {
         else -> unreachable { log.error("$this == $other is unexpected satisfiability check") }
     }
 
-    override fun satisfiesType(type: Type): AbstractDomainValue = this.type.satisfiesType(type)
+    override fun satisfiesType(type: Type): AbstractDomainValue = when {
+        nullity.isNull -> DomainStorage.falseDomain
+        nullity.canBeNull -> Top
+        else -> this.type.satisfiesType(type)
+    }
 }
 
 data class PtrDomainValue(
@@ -664,6 +726,7 @@ data class ArrayDomainValue(
             nullity.join(other.nullity),
             type.join(other.type)
         )
+
         is ArrayDomainValue -> ArrayDomainValue(
             nullity.join(other.nullity),
             type.join(other.type),
diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/state/transformer/domain/AbstractDomainSolver.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/state/transformer/domain/AbstractDomainSolver.kt
index efdd6f984..1877dd83b 100644
--- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/state/transformer/domain/AbstractDomainSolver.kt
+++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/state/transformer/domain/AbstractDomainSolver.kt
@@ -35,7 +35,6 @@ import org.vorpal.research.kex.state.term.CmpTerm
 import org.vorpal.research.kex.state.term.InstanceOfTerm
 import org.vorpal.research.kex.state.term.NegTerm
 import org.vorpal.research.kex.state.term.Term
-import org.vorpal.research.kex.state.term.ValueTerm
 import org.vorpal.research.kex.state.term.term
 import org.vorpal.research.kex.state.transformer.ConstantPropagator
 import org.vorpal.research.kex.state.transformer.IncrementalTransformer
@@ -228,7 +227,6 @@ class AbstractDomainSolver(val ctx: ExecutionContext) : Transformer<AbstractDoma
                             rhv.isTrue -> propagateInstanceOfCondition(condition, true)
                             rhv.isFalse -> propagateInstanceOfCondition(condition, false)
                         }
-                        is ValueTerm -> propagateCondition(condition)
                     }
                 }
             }
@@ -243,6 +241,9 @@ class AbstractDomainSolver(val ctx: ExecutionContext) : Transformer<AbstractDoma
                 val lhv = domainValue(predicate.lhv)
                 val rhv = domainValue(predicate.rhv)
                 satisfiabilityDomainValue = satisfiabilityDomainValue.meet(lhv.satisfiesInequality(rhv))
+                if (satisfiabilityDomainValue.isSat) {
+                    propagateCmpCondition(term { predicate.lhv neq predicate.rhv } as CmpTerm)
+                }
             }
         }
         return predicate
@@ -262,10 +263,6 @@ class AbstractDomainSolver(val ctx: ExecutionContext) : Transformer<AbstractDoma
         }
     } as CmpTerm
 
-    private fun propagateCondition(term: Term) {
-        System.err.println(term)
-    }
-
     private fun propagateCmpCondition(term: CmpTerm) {
         val lhv = storageValue(term.lhv)
         val rhv = storageValue(term.rhv)
@@ -273,9 +270,7 @@ class AbstractDomainSolver(val ctx: ExecutionContext) : Transformer<AbstractDoma
             term.lhv.type is KexPointer && rhv.value.isNull -> when (term.opcode) {
                 CmpOpcode.EQ -> lhv.value.assign(NullDomainValue)
                 CmpOpcode.NEQ -> lhv.value.assign(NonNullableDomainValue)
-                else -> {
-                    log.error("Could not propagate cmp condition $term for ${lhv.value} and ${rhv.value}")
-                }
+                else -> {}
             }
 
             term.lhv.type is KexInteger && rhv.value.isConstant -> when (term.opcode) {
@@ -296,9 +291,7 @@ class AbstractDomainSolver(val ctx: ExecutionContext) : Transformer<AbstractDoma
                         )
                     )
 
-                    else -> {
-                        log.error("Could not propagate cmp condition $term for ${lhv.value} and ${rhv.value}")
-                    }
+                    else -> {}
                 }
 
                 CmpOpcode.GT, CmpOpcode.GE -> when (val lhvValue = lhv.value) {
@@ -316,14 +309,10 @@ class AbstractDomainSolver(val ctx: ExecutionContext) : Transformer<AbstractDoma
                         )
                     )
 
-                    else -> {
-                        log.error("Could not propagate cmp condition $term for ${lhv.value} and ${rhv.value}")
-                    }
+                    else -> {}
                 }
 
-                else -> {
-                    log.error("Could not propagate cmp condition $term for ${lhv.value} and ${rhv.value}")
-                }
+                else -> {}
             }
         }
     }
@@ -332,8 +321,6 @@ class AbstractDomainSolver(val ctx: ExecutionContext) : Transformer<AbstractDoma
         val operand = storageValue(term.operand)
         if (positive) {
             operand.value.assign(TypeDomainValue(term.checkedType.getKfgType(ctx.types)))
-        } else {
-            log.error("Could not propagate cmp condition $term for ${operand.value}")
         }
     }