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 1707be9ba..9dea3848e 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
@@ -66,6 +66,12 @@ val AbstractDomainValue.isTrue: Boolean
 val AbstractDomainValue.isFalse: Boolean
     get() = this == DomainStorage.falseDomain
 
+val AbstractDomainValue.isNull: Boolean
+    get() = this is NullDomainValue
+
+val AbstractDomainValue.isConstant: Boolean
+    get() = this is IntervalDomainValue<*> && this.isConstant
+
 class DomainStorage(value: AbstractDomainValue) {
 
     var value = value
@@ -559,12 +565,16 @@ data class TypeDomainValue(val type: Type) : AbstractDomainValue {
         else -> unreachable { log.error("Attempting to meet $this and $other") }
     }
 
-    override fun assign(other: AbstractDomainValue): AbstractDomainValue = other
+    override fun assign(other: AbstractDomainValue): AbstractDomainValue = when (other) {
+        is TypeDomainValue -> if (other.type.isSubtypeOfCached(type)) other else this
+        else -> other
+    }
 
     override fun cast(type: Type): AbstractDomainValue = when {
         type.isSubtypeOfCached(this.type) -> TypeDomainValue(type)
         else -> this
     }
+
     override fun satisfiesType(type: Type): AbstractDomainValue = when {
         type.isSubtypeOfCached(this.type) -> DomainStorage.trueDomain
         this.type.isSubtypeOfCached(type) -> DomainStorage.trueDomain
@@ -609,6 +619,7 @@ data class PtrDomainValue(
         is Bottom -> other
         is NullityAbstractDomainValue -> PtrDomainValue(nullity.join(other), type)
         is PtrDomainValue -> PtrDomainValue(nullity.join(other.nullity), type.join(other.type))
+        is ArrayDomainValue -> PtrDomainValue(nullity.join(other.nullity), type.join(other.type))
         else -> unreachable { log.error("Attempting to join $this and $other") }
     }
 
@@ -621,7 +632,12 @@ data class PtrDomainValue(
     }
 
     override fun assign(other: AbstractDomainValue): AbstractDomainValue = when (other) {
-        is NullityAbstractDomainValue -> PtrDomainValue(other, type)
+        is NullityAbstractDomainValue -> PtrDomainValue(nullity.assign(other), type)
+        is TypeDomainValue -> when {
+            other.type is ArrayType -> ArrayDomainValue(nullity, type.assign(other), ArrayDomainValue.TOP_LENGTH)
+            else -> PtrDomainValue(nullity, type.assign(other))
+        }
+
         else -> other
     }
 
@@ -644,6 +660,10 @@ data class ArrayDomainValue(
         is Top -> Top
         is Bottom -> this
         is NullityAbstractDomainValue -> ArrayDomainValue(nullity.join(other), type, length)
+        is PtrDomainValue -> PtrDomainValue(
+            nullity.join(other.nullity),
+            type.join(other.type)
+        )
         is ArrayDomainValue -> ArrayDomainValue(
             nullity.join(other.nullity),
             type.join(other.type),
@@ -667,8 +687,15 @@ data class ArrayDomainValue(
     }
 
     override fun assign(other: AbstractDomainValue): AbstractDomainValue = when (other) {
-        is NullityAbstractDomainValue -> PtrDomainValue(other, type)
-        is PtrDomainValue -> ArrayDomainValue(other.nullity, other.type, length)
+        is NullityAbstractDomainValue -> PtrDomainValue(nullity.assign(other), type)
+        is PtrDomainValue -> ArrayDomainValue(nullity.assign(other.nullity), type.assign(other.type), length)
+        is ArrayDomainValue -> ArrayDomainValue(
+            nullity.assign(other.nullity),
+            type.assign(other.type),
+            length.assign(other.length)
+        )
+
+        is TypeDomainValue -> ArrayDomainValue(nullity, type.assign(other), length)
         else -> other
     }
 
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 ac9ccf2d5..efdd6f984 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
@@ -4,6 +4,17 @@ import kotlinx.collections.immutable.PersistentMap
 import kotlinx.collections.immutable.persistentMapOf
 import kotlinx.collections.immutable.toPersistentList
 import org.vorpal.research.kex.ExecutionContext
+import org.vorpal.research.kex.ktype.KexBool
+import org.vorpal.research.kex.ktype.KexByte
+import org.vorpal.research.kex.ktype.KexChar
+import org.vorpal.research.kex.ktype.KexDouble
+import org.vorpal.research.kex.ktype.KexFloat
+import org.vorpal.research.kex.ktype.KexInt
+import org.vorpal.research.kex.ktype.KexInteger
+import org.vorpal.research.kex.ktype.KexLong
+import org.vorpal.research.kex.ktype.KexPointer
+import org.vorpal.research.kex.ktype.KexShort
+import org.vorpal.research.kex.ktype.KexType
 import org.vorpal.research.kex.smt.Result
 import org.vorpal.research.kex.state.ChoiceState
 import org.vorpal.research.kex.state.IncrementalPredicateState
@@ -24,10 +35,17 @@ 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
 import org.vorpal.research.kex.state.transformer.Transformer
+import org.vorpal.research.kfg.ir.value.instruction.CmpOpcode
 import org.vorpal.research.kfg.ir.value.instruction.UnaryOpcode
+import org.vorpal.research.kthelper.assert.unreachable
+import org.vorpal.research.kthelper.logging.log
+import org.vorpal.research.kthelper.maxOf
+import org.vorpal.research.kthelper.minOf
 
 class AbstractDomainSolver(val ctx: ExecutionContext) : Transformer<AbstractDomainSolver>, IncrementalTransformer {
     private var abstractDomainValues = persistentMapOf<Term, DomainStorage>()
@@ -191,13 +209,28 @@ class AbstractDomainSolver(val ctx: ExecutionContext) : Transformer<AbstractDoma
             is PredicateType.State -> {
                 val rhv = domainValue(predicate.rhv)
                 storageValue(predicate.lhv).value = rhv
-                equalities = equalities.put(predicate.lhv, predicate.rhv)
+                equalities = equalities.put(predicate.lhv, equalities[predicate.rhv] ?: predicate.rhv)
             }
 
             else -> {
                 val lhv = domainValue(predicate.lhv)
                 val rhv = domainValue(predicate.rhv)
                 satisfiabilityDomainValue = satisfiabilityDomainValue.meet(lhv.satisfiesEquality(rhv))
+                if (satisfiabilityDomainValue.isSat) {
+                    val condition = equalities[predicate.lhv] ?: predicate.lhv
+                    when (condition) {
+                        is CmpTerm -> when {
+                            rhv.isTrue -> propagateCmpCondition(condition)
+                            rhv.isFalse -> propagateCmpCondition(condition.reversed())
+                        }
+
+                        is InstanceOfTerm -> when {
+                            rhv.isTrue -> propagateInstanceOfCondition(condition, true)
+                            rhv.isFalse -> propagateInstanceOfCondition(condition, false)
+                        }
+                        is ValueTerm -> propagateCondition(condition)
+                    }
+                }
             }
         }
         return predicate
@@ -214,6 +247,119 @@ class AbstractDomainSolver(val ctx: ExecutionContext) : Transformer<AbstractDoma
         }
         return predicate
     }
+
+    private fun CmpTerm.reversed(): CmpTerm = term {
+        when (opcode) {
+            CmpOpcode.EQ -> lhv neq rhv
+            CmpOpcode.NEQ -> lhv eq rhv
+            CmpOpcode.LT -> lhv ge rhv
+            CmpOpcode.GT -> lhv le rhv
+            CmpOpcode.LE -> lhv gt rhv
+            CmpOpcode.GE -> lhv lt rhv
+            CmpOpcode.CMP -> rhv cmp lhv
+            CmpOpcode.CMPG -> rhv cmpg lhv
+            CmpOpcode.CMPL -> rhv cmpl lhv
+        }
+    } 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)
+        when {
+            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}")
+                }
+            }
+
+            term.lhv.type is KexInteger && rhv.value.isConstant -> when (term.opcode) {
+                CmpOpcode.EQ -> lhv.value.assign(rhv.value)
+                CmpOpcode.NEQ -> {} // nothing
+                CmpOpcode.LT, CmpOpcode.LE -> when (val lhvValue = lhv.value) {
+                    is IntervalDomainValue<*> -> lhv.value.assign(
+                        IntervalDomainValue(
+                            lhvValue.min,
+                            minOf(lhvValue.max, (rhv.value as IntervalDomainValue<*>).min)
+                        )
+                    )
+
+                    is Top -> lhv.value.assign(
+                        IntervalDomainValue(
+                            lowerBound(term.lhv.type),
+                            (rhv.value as IntervalDomainValue<*>).min
+                        )
+                    )
+
+                    else -> {
+                        log.error("Could not propagate cmp condition $term for ${lhv.value} and ${rhv.value}")
+                    }
+                }
+
+                CmpOpcode.GT, CmpOpcode.GE -> when (val lhvValue = lhv.value) {
+                    is IntervalDomainValue<*> -> lhv.value.assign(
+                        IntervalDomainValue(
+                            maxOf(lhvValue.min, (rhv.value as IntervalDomainValue<*>).min),
+                            lhvValue.max
+                        )
+                    )
+
+                    is Top -> lhv.value.assign(
+                        IntervalDomainValue(
+                            (rhv.value as IntervalDomainValue<*>).min,
+                            upperBound(term.lhv.type)
+                        )
+                    )
+
+                    else -> {
+                        log.error("Could not propagate cmp condition $term for ${lhv.value} and ${rhv.value}")
+                    }
+                }
+
+                else -> {
+                    log.error("Could not propagate cmp condition $term for ${lhv.value} and ${rhv.value}")
+                }
+            }
+        }
+    }
+
+    private fun propagateInstanceOfCondition(term: InstanceOfTerm, positive: Boolean) {
+        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}")
+        }
+    }
+
+    private fun lowerBound(type: KexType): Number = when (type) {
+        is KexBool -> 0
+        is KexByte -> Byte.MAX_VALUE
+        is KexChar -> Char.MIN_VALUE.code
+        is KexShort -> Short.MIN_VALUE
+        is KexInt -> Int.MIN_VALUE
+        is KexLong -> Long.MIN_VALUE
+        is KexFloat -> Float.NEGATIVE_INFINITY
+        is KexDouble -> Double.NEGATIVE_INFINITY
+        else -> unreachable { log.error("Unknown type $type for lower bound") }
+    }
+
+    private fun upperBound(type: KexType): Number = when (type) {
+        is KexBool -> 1
+        is KexByte -> Byte.MAX_VALUE
+        is KexChar -> Char.MAX_VALUE.code
+        is KexShort -> Short.MAX_VALUE
+        is KexInt -> Int.MAX_VALUE
+        is KexLong -> Long.MAX_VALUE
+        is KexFloat -> Float.POSITIVE_INFINITY
+        is KexDouble -> Double.POSITIVE_INFINITY
+        else -> unreachable { log.error("Unknown type $type for lower bound") }
+    }
 }