diff --git a/kex-annotation-processor/src/main/resources/SMTExpr.vm b/kex-annotation-processor/src/main/resources/SMTExpr.vm
index fd8858687..4d804906c 100644
--- a/kex-annotation-processor/src/main/resources/SMTExpr.vm
+++ b/kex-annotation-processor/src/main/resources/SMTExpr.vm
@@ -573,7 +573,7 @@ class Ifer {
             inline fun < reified T : $valexpr > `else`(`false`: T): T {
                 val ctx = cond.ctx
                 val expr = engine().ite(ctx, cond.expr, `true`.expr, `false`.expr)
-                val axiom = spliceAxioms(ctx, `true`.axiom, `false`.axiom)
+                val axiom = spliceAxioms(ctx, cond.axiom, `true`.axiom, `false`.axiom)
                 return ${valexpr}.forceCast< T >($valexpr(ctx, expr, axiom))
             }
             inline fun < reified T : $valexpr > else_(`false`: () -> T) = `else`(`false`())
diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/asm/manager/ClassInstantiationManager.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/asm/manager/ClassInstantiationManager.kt
index 8023c03b9..ec27a729e 100644
--- a/kex-core/src/main/kotlin/org/vorpal/research/kex/asm/manager/ClassInstantiationManager.kt
+++ b/kex-core/src/main/kotlin/org/vorpal/research/kex/asm/manager/ClassInstantiationManager.kt
@@ -39,6 +39,18 @@ interface ClassInstantiationManager {
             else -> type
         }
 
+    fun getAll(type: Type, accessLevel: AccessModifier, excludes: Set<Class>): Set<Type> =
+        when (type) {
+            is ClassType -> getAllConcreteSubtypes(type.klass, accessLevel)
+                .filter { it !in excludes }
+                .mapTo(mutableSetOf()) { it.asType }
+
+            is ArrayType -> getAll(type.component, accessLevel, excludes)
+                .mapTo(mutableSetOf()) { it.asArray }
+
+            else -> setOf(type)
+        }
+
     fun getAllConcreteSubtypes(klass: Class, accessLevel: AccessModifier): Set<Class>
 
     fun getConcreteClass(klass: KexClass, cm: ClassManager, accessLevel: AccessModifier, random: Random): KexClass =
diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/descriptor/converter.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/descriptor/converter.kt
index d66453854..11c599144 100644
--- a/kex-core/src/main/kotlin/org/vorpal/research/kex/descriptor/converter.kt
+++ b/kex-core/src/main/kotlin/org/vorpal/research/kex/descriptor/converter.kt
@@ -64,7 +64,7 @@ class Object2DescriptorConverter : DescriptorBuilder() {
                 is LongArray -> KexLong.asArray()
                 is FloatArray -> KexFloat.asArray()
                 is DoubleArray -> KexDouble.asArray()
-                is Array<*> -> any.javaClass.componentType.kex
+                is Array<*> -> any.javaClass.componentType.kex.asArray()
                 is String -> KexString()
                 else -> any.javaClass.kex
             }
diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/descriptor/descriptor.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/descriptor/descriptor.kt
index f2569e4d8..8e7eaef9d 100644
--- a/kex-core/src/main/kotlin/org/vorpal/research/kex/descriptor/descriptor.kt
+++ b/kex-core/src/main/kotlin/org/vorpal/research/kex/descriptor/descriptor.kt
@@ -54,6 +54,7 @@ sealed class Descriptor(term: Term, type: KexType) {
         }
 
     val query: PredicateState get() = collectQuery(mutableSetOf())
+    val initializerState: PredicateState get() = collectInitializerState(mutableSetOf())
     val depth: Int get() = countDepth(setOf(), mutableMapOf())
 
     val typeInfo: PredicateState get() = generateTypeInfo(mutableSetOf())
@@ -67,6 +68,7 @@ sealed class Descriptor(term: Term, type: KexType) {
     abstract fun print(map: MutableMap<Descriptor, String>): String
     abstract fun structuralEquality(other: Descriptor, map: MutableSet<Pair<Descriptor, Descriptor>>): Boolean
     abstract fun collectQuery(set: MutableSet<Descriptor>): PredicateState
+    abstract fun collectInitializerState(set: MutableSet<Descriptor>): PredicateState
 
     abstract fun countDepth(visited: Set<Descriptor>, cache: MutableMap<Descriptor, Int>): Int
     abstract fun concretize(
@@ -105,6 +107,10 @@ sealed class ConstantDescriptor(term: Term, type: KexType) : Descriptor(term, ty
             require { term equality null }
         }
 
+        override fun collectInitializerState(set: MutableSet<Descriptor>): PredicateState = basic {
+            state { term equality null }
+        }
+
         override fun structuralEquality(other: Descriptor, map: MutableSet<Pair<Descriptor, Descriptor>>) =
             other is Null
     }
@@ -116,6 +122,10 @@ sealed class ConstantDescriptor(term: Term, type: KexType) : Descriptor(term, ty
             require { term equality value }
         }
 
+        override fun collectInitializerState(set: MutableSet<Descriptor>): PredicateState = basic {
+            state { term equality value }
+        }
+
         override fun structuralEquality(other: Descriptor, map: MutableSet<Pair<Descriptor, Descriptor>>): Boolean {
             if (other !is Bool) return false
             return this.value == other.value
@@ -129,6 +139,10 @@ sealed class ConstantDescriptor(term: Term, type: KexType) : Descriptor(term, ty
             require { term equality value }
         }
 
+        override fun collectInitializerState(set: MutableSet<Descriptor>): PredicateState = basic {
+            state { term equality value }
+        }
+
         override fun structuralEquality(other: Descriptor, map: MutableSet<Pair<Descriptor, Descriptor>>): Boolean {
             if (other !is Byte) return false
             return this.value == other.value
@@ -142,6 +156,10 @@ sealed class ConstantDescriptor(term: Term, type: KexType) : Descriptor(term, ty
             require { term equality value }
         }
 
+        override fun collectInitializerState(set: MutableSet<Descriptor>): PredicateState = basic {
+            state { term equality value }
+        }
+
         override fun structuralEquality(other: Descriptor, map: MutableSet<Pair<Descriptor, Descriptor>>): Boolean {
             if (other !is Char) return false
             return this.value == other.value
@@ -155,6 +173,10 @@ sealed class ConstantDescriptor(term: Term, type: KexType) : Descriptor(term, ty
             require { term equality value }
         }
 
+        override fun collectInitializerState(set: MutableSet<Descriptor>): PredicateState = basic {
+            state { term equality value }
+        }
+
         override fun structuralEquality(other: Descriptor, map: MutableSet<Pair<Descriptor, Descriptor>>): Boolean {
             if (other !is Short) return false
             return this.value == other.value
@@ -168,6 +190,10 @@ sealed class ConstantDescriptor(term: Term, type: KexType) : Descriptor(term, ty
             require { term equality value }
         }
 
+        override fun collectInitializerState(set: MutableSet<Descriptor>): PredicateState = basic {
+            state { term equality value }
+        }
+
         override fun structuralEquality(other: Descriptor, map: MutableSet<Pair<Descriptor, Descriptor>>): Boolean {
             if (other !is Int) return false
             return this.value == other.value
@@ -181,6 +207,10 @@ sealed class ConstantDescriptor(term: Term, type: KexType) : Descriptor(term, ty
             require { term equality value }
         }
 
+        override fun collectInitializerState(set: MutableSet<Descriptor>): PredicateState = basic {
+            state { term equality value }
+        }
+
         override fun structuralEquality(other: Descriptor, map: MutableSet<Pair<Descriptor, Descriptor>>): Boolean {
             if (other !is Long) return false
             return this.value == other.value
@@ -194,6 +224,10 @@ sealed class ConstantDescriptor(term: Term, type: KexType) : Descriptor(term, ty
             require { term equality value }
         }
 
+        override fun collectInitializerState(set: MutableSet<Descriptor>): PredicateState = basic {
+            state { term equality value }
+        }
+
         override fun structuralEquality(other: Descriptor, map: MutableSet<Pair<Descriptor, Descriptor>>): Boolean {
             if (other !is Float) return false
             return this.value == other.value
@@ -207,6 +241,10 @@ sealed class ConstantDescriptor(term: Term, type: KexType) : Descriptor(term, ty
             require { term equality value }
         }
 
+        override fun collectInitializerState(set: MutableSet<Descriptor>): PredicateState = basic {
+            state { term equality value }
+        }
+
         override fun structuralEquality(other: Descriptor, map: MutableSet<Pair<Descriptor, Descriptor>>): Boolean {
             if (other !is Double) return false
             return this.value == other.value
@@ -283,6 +321,19 @@ sealed class FieldContainingDescriptor<T : FieldContainingDescriptor<T>>(
         }
     }
 
+    override fun collectInitializerState(set: MutableSet<Descriptor>): PredicateState {
+        if (this in set) return emptyState()
+        set += this
+        return basic {
+            state { term.initializeNew() }
+            for ((field, value) in fields) {
+                val fieldTerm = term.field(field.second, field.first)
+                append(value.collectInitializerState(set))
+                state { fieldTerm.initialize(value.term) }
+            }
+        }
+    }
+
     override fun concretize(
         cm: ClassManager,
         accessLevel: AccessModifier,
@@ -483,6 +534,16 @@ class ArrayDescriptor(val elementType: KexType, val length: Int) :
         }
     }
 
+    override fun collectInitializerState(set: MutableSet<Descriptor>): PredicateState {
+        if (this in set) return emptyState()
+        set += this
+        return basic {
+            val fullElements = (0 until length).map { elements[it] ?: descriptor { default(elementType) } }
+            fullElements.forEach { append(it.collectInitializerState(set)) }
+            state { term.initializeNew(length, fullElements.map { it.term }) }
+        }
+    }
+
 
     override fun concretize(
         cm: ClassManager,
diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt
index f758e2346..7ee5c8231 100644
--- a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt
+++ b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt
@@ -179,6 +179,8 @@ data class PersistentClauseList(
 
     override fun plus(other: ClauseList): PersistentClauseList = PersistentClauseList(state.addAll(other.state))
     override fun plus(other: Clause): PersistentClauseList = PersistentClauseList(state.add(other))
+
+    fun dropLast(n: Int): PersistentClauseList = subState(0, maxOf(0, size - n))
 }
 
 @Serializable
@@ -268,6 +270,8 @@ data class PersistentPathCondition(
 
     override fun plus(other: PathCondition): PersistentPathCondition = PersistentPathCondition(path.addAll(other.path))
     override fun plus(other: PathClause): PersistentPathCondition = PersistentPathCondition(path.add(other))
+
+    fun dropLast(n: Int): PersistentPathCondition = subPath(0, maxOf(0, size - n))
 }
 
 @Serializable
@@ -297,11 +301,29 @@ abstract class SymbolicState {
     abstract operator fun plus(other: PathClause): SymbolicState
     abstract operator fun plus(other: ClauseList): SymbolicState
     abstract operator fun plus(other: PathCondition): SymbolicState
+
+    override fun equals(other: Any?): Boolean {
+        if (this === other) return true
+        if (javaClass != other?.javaClass) return false
+
+        other as SymbolicState
+
+        if (clauses != other.clauses) return false
+        if (path != other.path) return false
+
+        return true
+    }
+
+    override fun hashCode(): Int {
+        var result = clauses.hashCode()
+        result = 31 * result + path.hashCode()
+        return result
+    }
 }
 
 @Serializable
 @SerialName("SymbolicStateImpl")
-internal data class SymbolicStateImpl(
+internal class SymbolicStateImpl(
     override val clauses: ClauseList,
     override val path: PathCondition,
     override val concreteTypes: @Contextual Map<Term, KexType>,
@@ -315,15 +337,19 @@ internal data class SymbolicStateImpl(
         concreteValues = concreteValues + other.concreteValues,
         termMap = termMap + other.termMap
     )
+
     override fun plus(other: StateClause): SymbolicState = copy(
         clauses = clauses + other
     )
+
     override fun plus(other: PathClause): SymbolicState = copy(
         path = path + other,
     )
+
     override fun plus(other: ClauseList): SymbolicState = copy(
         clauses = clauses + other
     )
+
     override fun plus(other: PathCondition): SymbolicState = copy(
         path = path + other,
     )
@@ -331,17 +357,28 @@ internal data class SymbolicStateImpl(
     override fun toString(): String {
         return "SymbolicStateImpl(clauses=$clauses, path=$path)"
     }
+
+    fun copy(
+        clauses: ClauseList = this.clauses,
+        path: PathCondition = this.path,
+        concreteTypes: Map<Term, KexType> = this.concreteTypes,
+        concreteValues: Map<Term, Descriptor> = this.concreteValues,
+        termMap: Map<Term, WrappedValue> = this.termMap,
+    ): SymbolicState = SymbolicStateImpl(
+        clauses, path, concreteTypes, concreteValues, termMap
+    )
 }
 
 @Serializable
 @SerialName("PersistentSymbolicState")
-data class PersistentSymbolicState(
+class PersistentSymbolicState(
     override val clauses: PersistentClauseList,
     override val path: PersistentPathCondition,
     override val concreteTypes: @Contextual PersistentMap<Term, KexType>,
     override val concreteValues: @Contextual PersistentMap<Term, @Contextual Descriptor>,
     override val termMap: @Contextual PersistentMap<Term, @Contextual WrappedValue>,
 ) : SymbolicState() {
+
     override fun toString() = clauses.joinToString("\n") { it.predicate.toString() }
 
     override fun plus(other: SymbolicState): PersistentSymbolicState = PersistentSymbolicState(
@@ -351,18 +388,32 @@ data class PersistentSymbolicState(
         concreteValues = concreteValues.putAll(other.concreteValues),
         termMap = termMap.putAll(other.termMap)
     )
+
     override fun plus(other: StateClause): PersistentSymbolicState = copy(
         clauses = clauses + other
     )
+
     override fun plus(other: PathClause): PersistentSymbolicState = copy(
         path = path + other,
     )
+
     override fun plus(other: ClauseList): PersistentSymbolicState = copy(
         clauses = clauses + other
     )
+
     override fun plus(other: PathCondition): PersistentSymbolicState = copy(
         path = path + other,
     )
+
+    fun copy(
+        clauses: PersistentClauseList = this.clauses,
+        path: PersistentPathCondition = this.path,
+        concreteTypes: PersistentMap<Term, KexType> = this.concreteTypes,
+        concreteValues: PersistentMap<Term, Descriptor> = this.concreteValues,
+        termMap: PersistentMap<Term, WrappedValue> = this.termMap,
+    ): PersistentSymbolicState = PersistentSymbolicState(
+        clauses, path, concreteTypes, concreteValues, termMap
+    )
 }
 
 
diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicTraceBuilder.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicTraceBuilder.kt
index dbfc6eded..79df4b7f5 100644
--- a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicTraceBuilder.kt
+++ b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicTraceBuilder.kt
@@ -449,6 +449,7 @@ class SymbolicTraceBuilder(
             for ((value, term) in method.parameterValues.asList.zip(call.params.asList)) {
                 valueMap[value] = term
             }
+            stateBuilder += StateClause(call.call, state { true equality true })
             lastCall = null
         } else {
             if (!traceCollectingEnabled) return@safeCall
@@ -715,9 +716,10 @@ class SymbolicTraceBuilder(
             predicate
         )
 
-        /**
-         * we do not use 'postProcess' here, because actual call predicate may not end up in the final state
-         */
+//        postProcess(instruction, state { true equality true })
+//        /**
+//         * we do not use 'postProcess' here, because actual call predicate may not end up in the final state
+//         */
         traceBuilder += instruction
         updateCatches(instruction)
     }
@@ -1015,8 +1017,10 @@ class SymbolicTraceBuilder(
          * we do not use 'postProcess' here because jump instruction is not converted into any predicate
          */
         previousBlock = instruction.parent
-        traceBuilder += instruction
-        updateCatches(instruction)
+
+        postProcess(instruction, state { true equality true })
+//        traceBuilder += instruction
+//        updateCatches(instruction)
     }
 
     override fun newArray(
@@ -1125,14 +1129,10 @@ class SymbolicTraceBuilder(
             terms[termReceiver] = kfgReceiver.wrapped()
             concreteTypeMap[termReceiver] = concreteValue.getConcreteType(termReceiver.type)
 
-            stateBuilder += StateClause(instruction, predicate)
+            postProcess(instruction, predicate)
+        } else {
+            postProcess(instruction, state { true equality true })
         }
-
-        /**
-         * we do not use 'postProcess' here because return inst is not always converted into predicate
-         */
-        traceBuilder += instruction
-        updateCatches(instruction)
     }
 
     private fun numericValue(value: Any?): Number = when (value) {
@@ -1297,8 +1297,8 @@ class SymbolicTraceBuilder(
 
         val kfgValue = parseValue(value)
         val termValue = mkValue(kfgValue)
-        val descriptorValue = concreteValue.getAsDescriptor()
-        val kfgType = descriptorValue.type.getKfgType(ctx.types)
+        val concreteType = concreteValue.getConcreteType(termValue.type)
+        val kfgType = concreteType.getKfgType(ctx.types)
         if (termValue in typeChecked) {
             val checkedType = typeChecked.getValue(termValue)
             if (checkedType.isSubtypeOfCached(kfgType)) return@safeCall
@@ -1306,7 +1306,7 @@ class SymbolicTraceBuilder(
         typeChecked[termValue] = kfgType
 
         val predicate = path {
-            (termValue `is` descriptorValue.type) equality true
+            (termValue `is` concreteType) equality true
         }
 
         processPath(PathClauseType.OVERLOAD_CHECK, instruction, predicate)
@@ -1325,8 +1325,7 @@ class SymbolicTraceBuilder(
         val comparisonResult = when (concreteValue) {
             null -> false
             else -> {
-                val descriptorValue = concreteValue.getAsDescriptor()
-                val actualKfgType = descriptorValue.type.getKfgType(ctx.types)
+                val actualKfgType = concreteValue.getConcreteType(termValue.type).getKfgType(ctx.types)
                 actualKfgType.isSubtypeOfCached(expectedKfgType)
             }
         }
diff --git a/kex-ksmt/src/main/kotlin/org/vorpal/research/kex/smt/ksmt/KSMTSolver.kt b/kex-ksmt/src/main/kotlin/org/vorpal/research/kex/smt/ksmt/KSMTSolver.kt
index f49c36eac..b6067bf68 100644
--- a/kex-ksmt/src/main/kotlin/org/vorpal/research/kex/smt/ksmt/KSMTSolver.kt
+++ b/kex-ksmt/src/main/kotlin/org/vorpal/research/kex/smt/ksmt/KSMTSolver.kt
@@ -431,6 +431,7 @@ class KSMTSolver(
         }
 
         val indices = hashSetOf<Term>()
+        val coveredArrays = hashSetOf<Term>()
         for (ptr in ptrs) {
             val memspace = ptr.memspace
 
@@ -550,10 +551,13 @@ class KSMTSolver(
                         val maxLen = maxOf(initialLength, finalLength)
                         properties[memspace]!!["length"]!!.first[modelPtr] = term { const(initialLength) }
                         properties[memspace]!!["length"]!!.second[modelPtr] = term { const(finalLength) }
-                        for (i in 0 until maxLen) {
-                            val indexTerm = term { ptr[i] }
-                            if (indexTerm !in ptrs)
-                                indices += indexTerm
+                        if (modelPtr !in coveredArrays) {
+                            coveredArrays += modelPtr
+                            for (i in 0 until maxLen) {
+                                val indexTerm = term { ptr[i] }
+                                if (indexTerm !in ptrs)
+                                    indices += indexTerm
+                            }
                         }
                     } else if (ptr is ConstClassTerm || ptr is ClassAccessTerm) {
                         properties.recoverBitvectorProperty(
diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/ConcolicPathSelector.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/ConcolicPathSelector.kt
index 1fe041c9a..a9ccc7533 100644
--- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/ConcolicPathSelector.kt
+++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/ConcolicPathSelector.kt
@@ -7,10 +7,16 @@ import org.vorpal.research.kex.trace.symbolic.PersistentSymbolicState
 import org.vorpal.research.kex.trace.symbolic.protocol.ExecutionCompletedResult
 import org.vorpal.research.kfg.ir.Method
 
-interface ConcolicPathSelector : SuspendableIterator<PersistentSymbolicState> {
+interface ConcolicPathSelectorManager {
+    val ctx: ExecutionContext
+    val targets: Set<Method>
+    fun createPathSelectorFor(target: Method): ConcolicPathSelector
+}
+
+interface ConcolicPathSelector : SuspendableIterator<Pair<Method, PersistentSymbolicState>> {
     val ctx: ExecutionContext
 
     suspend fun isEmpty(): Boolean
-    suspend fun addExecutionTrace(method: Method, result: ExecutionCompletedResult)
+    suspend fun addExecutionTrace(method: Method, checkedState: PersistentSymbolicState, result: ExecutionCompletedResult)
     fun reverse(pathClause: PathClause): PathClause?
 }
diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/InstructionConcolicChecker.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/InstructionConcolicChecker.kt
index d3d45a190..055096dde 100644
--- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/InstructionConcolicChecker.kt
+++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/InstructionConcolicChecker.kt
@@ -10,9 +10,9 @@ import kotlinx.coroutines.yield
 import kotlinx.serialization.ExperimentalSerializationApi
 import kotlinx.serialization.InternalSerializationApi
 import org.vorpal.research.kex.ExecutionContext
-import org.vorpal.research.kex.asm.analysis.concolic.bfs.BfsPathSelectorImpl
-import org.vorpal.research.kex.asm.analysis.concolic.cgs.ContextGuidedSelector
-import org.vorpal.research.kex.asm.analysis.concolic.gui.GUIProxySelector
+import org.vorpal.research.kex.asm.analysis.concolic.bfs.BfsPathSelectorManager
+import org.vorpal.research.kex.asm.analysis.concolic.cgs.ContextGuidedSelectorManager
+import org.vorpal.research.kex.asm.analysis.concolic.coverage.CoverageGuidedSelectorManager
 import org.vorpal.research.kex.asm.analysis.util.analyzeOrTimeout
 import org.vorpal.research.kex.asm.analysis.util.checkAsync
 import org.vorpal.research.kex.compile.CompilerHelper
@@ -27,6 +27,7 @@ import org.vorpal.research.kex.trace.runner.SymbolicExternalTracingRunner
 import org.vorpal.research.kex.trace.runner.generateDefaultParameters
 import org.vorpal.research.kex.trace.runner.generateParameters
 import org.vorpal.research.kex.trace.symbolic.SymbolicState
+import org.vorpal.research.kex.trace.symbolic.persistentSymbolicState
 import org.vorpal.research.kex.trace.symbolic.protocol.ExecutionCompletedResult
 import org.vorpal.research.kex.trace.symbolic.protocol.ExecutionResult
 import org.vorpal.research.kex.util.newFixedThreadPoolContextWithMDC
@@ -41,41 +42,73 @@ import java.util.concurrent.atomic.AtomicInteger
 import kotlin.time.Duration.Companion.seconds
 import kotlin.time.ExperimentalTime
 
+interface TestNameGenerator {
+    fun generateName(method: Method, parameters: Parameters<Descriptor>): String
+}
+
+class TestNameGeneratorImpl : TestNameGenerator {
+    private var testIndex = AtomicInteger(0)
+
+    override fun generateName(method: Method, parameters: Parameters<Descriptor>): String =
+        method.klassName + testIndex.getAndIncrement()
+
+}
+
 @ExperimentalSerializationApi
 @InternalSerializationApi
 class InstructionConcolicChecker(
     val ctx: ExecutionContext,
+    private val pathSelector: ConcolicPathSelector,
+    private val testNameGenerator: TestNameGenerator,
 ) {
     val cm: ClassManager
         get() = ctx.cm
 
     private val compilerHelper = CompilerHelper(ctx)
 
-    private val searchStrategy = kexConfig.getStringValue("concolic", "searchStrategy", "bfs")
-    private val guiEnabled = kexConfig.getBooleanValue("gui", "enabled", false)
+    companion object {
 
-    private var testIndex = AtomicInteger(0)
+        private fun buildSelectorManager(
+            ctx: ExecutionContext,
+            targets: Set<Method>,
+            strategyName: String,
+        ): ConcolicPathSelectorManager = when (strategyName) {
+            "bfs" -> BfsPathSelectorManager(ctx, targets)
+            "cgs" -> ContextGuidedSelectorManager(ctx, targets)
+            "coverage" -> CoverageGuidedSelectorManager(ctx, targets)
+            else -> unreachable { log.error("Unknown type of search strategy $strategyName") }
+        }
 
-    companion object {
         @ExperimentalTime
         @DelicateCoroutinesApi
         fun run(context: ExecutionContext, targets: Set<Method>) {
             val executors = kexConfig.getIntValue("concolic", "numberOfExecutors", 8)
             val timeLimit = kexConfig.getIntValue("concolic", "timeLimit", 100)
+            val searchStrategy = kexConfig.getStringValue("concolic", "searchStrategy", "bfs")
 
             val actualNumberOfExecutors = maxOf(1, minOf(executors, targets.size))
             val coroutineContext = newFixedThreadPoolContextWithMDC(actualNumberOfExecutors, "concolic-dispatcher")
+
+            val selectorManager = buildSelectorManager(context, targets, searchStrategy)
+            val testNameGenerator = TestNameGeneratorImpl()
+
             runBlocking(coroutineContext) {
                 withTimeoutOrNull(timeLimit.seconds) {
                     targets.map {
-                        async { InstructionConcolicChecker(context).visit(it) }
+                        async {
+                            InstructionConcolicChecker(
+                                context,
+                                selectorManager.createPathSelectorFor(it),
+                                testNameGenerator
+                            ).start(it)
+                        }
                     }.awaitAll()
                 }
             }
         }
     }
 
-    suspend fun visit(method: Method) {
+    suspend fun start(method: Method) {
         method.analyzeOrTimeout(ctx.accessLevel) {
             processMethod(it)
         }
@@ -101,7 +134,7 @@ class InstructionConcolicChecker(
         collectTrace(method, parameters.asDescriptors)
 
     private suspend fun collectTrace(method: Method, parameters: Parameters<Descriptor>): ExecutionResult? = tryOrNull {
-        val generator = UnsafeGenerator(ctx, method, method.klassName + testIndex.getAndIncrement())
+        val generator = UnsafeGenerator(ctx, method, testNameGenerator.generateName(method, parameters))
         generator.generate(parameters)
         val testFile = generator.emit()
 
@@ -123,41 +156,31 @@ class InstructionConcolicChecker(
         null
     }
 
-    private fun buildPathSelector(): ConcolicPathSelector {
-        val pathSelector = when (searchStrategy) {
-            "bfs" -> BfsPathSelectorImpl(ctx)
-            "cgs" -> ContextGuidedSelector(ctx)
-            else -> unreachable { log.error("Unknown type of search strategy $searchStrategy") }
-        }
-
-        return if (guiEnabled) GUIProxySelector(pathSelector) else pathSelector
-    }
-
-    private suspend fun handleStartingTrace(
+    private suspend fun initializeExecutionGraph(
         method: Method,
-        pathIterator: ConcolicPathSelector,
-        executionResult: ExecutionResult?
+        pathIterator: ConcolicPathSelector
     ) {
-        executionResult?.let {
-            when (it) {
-                is ExecutionCompletedResult -> pathIterator.addExecutionTrace(method, it)
-                else -> log.warn("Failed to generate random trace: $it")
+        val initialExecution = when (val randomTrace = getRandomTrace(method)) {
+            is ExecutionCompletedResult -> randomTrace
+            else -> getDefaultTrace(method)
+        }
+        when (initialExecution) {
+            is ExecutionCompletedResult -> {
+                pathIterator.addExecutionTrace(method, persistentSymbolicState(), initialExecution)
+            }
+
+            else -> {
+                log.warn("Failed to generate random trace for method $method: $initialExecution")
             }
         }
     }
 
-    private suspend fun processMethod(method: Method) {
-        testIndex = AtomicInteger(0)
-        val pathIterator = buildPathSelector()
-
-        handleStartingTrace(method, pathIterator, getRandomTrace(method))
-        if (pathIterator.isEmpty()) {
-            handleStartingTrace(method, pathIterator, getDefaultTrace(method))
-        }
+    private suspend fun processMethod(startingMethod: Method) {
+        initializeExecutionGraph(startingMethod, pathSelector)
         yield()
 
-        while (pathIterator.hasNext()) {
-            val state = pathIterator.next()
+        while (pathSelector.hasNext()) {
+            val (method, state) = pathSelector.next()
             log.debug { "Checking state: $state" }
             log.debug { "Path:\n${state.path.asState()}" }
             yield()
@@ -166,7 +189,7 @@ class InstructionConcolicChecker(
             when (newState) {
                 is ExecutionCompletedResult -> when {
                     newState.trace.isEmpty() -> log.warn { "Collected empty state from $state" }
-                    else -> pathIterator.addExecutionTrace(method, newState)
+                    else -> pathSelector.addExecutionTrace(method, state, newState)
                 }
 
                 else -> log.warn("Failure during execution: $newState")
diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/bfs/BfsPathSelector.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/bfs/BfsPathSelector.kt
index b58be5a80..e0a76427f 100644
--- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/bfs/BfsPathSelector.kt
+++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/bfs/BfsPathSelector.kt
@@ -2,6 +2,7 @@ package org.vorpal.research.kex.asm.analysis.concolic.bfs
 
 import org.vorpal.research.kex.ExecutionContext
 import org.vorpal.research.kex.asm.analysis.concolic.ConcolicPathSelector
+import org.vorpal.research.kex.asm.analysis.concolic.ConcolicPathSelectorManager
 import org.vorpal.research.kex.state.predicate.DefaultSwitchPredicate
 import org.vorpal.research.kex.state.predicate.EqualityPredicate
 import org.vorpal.research.kex.state.predicate.InequalityPredicate
@@ -25,9 +26,17 @@ import org.vorpal.research.kthelper.assert.unreachable
 import org.vorpal.research.kthelper.collection.dequeOf
 import org.vorpal.research.kthelper.logging.log
 
+class BfsPathSelectorManager(
+    override val ctx: ExecutionContext,
+    override val targets: Set<Method>
+) : ConcolicPathSelectorManager {
+    override fun createPathSelectorFor(target: Method): ConcolicPathSelector =
+        BfsPathSelectorImpl(ctx, target)
+}
 
 class BfsPathSelectorImpl(
     override val ctx: ExecutionContext,
+    val method: Method
 ) : ConcolicPathSelector {
     private val coveredPaths = mutableSetOf<PersistentPathCondition>()
     private val candidates = mutableSetOf<PersistentPathCondition>()
@@ -36,14 +45,18 @@ class BfsPathSelectorImpl(
     override suspend fun isEmpty(): Boolean = deque.isEmpty()
     override suspend fun hasNext(): Boolean = deque.isNotEmpty()
 
-    override suspend fun addExecutionTrace(method: Method, result: ExecutionCompletedResult) {
+    override suspend fun addExecutionTrace(
+        method: Method,
+        checkedState: PersistentSymbolicState,
+        result: ExecutionCompletedResult
+    ) {
         val persistentResult = result.symbolicState.toPersistentState()
         if (persistentResult.path in coveredPaths) return
         coveredPaths += persistentResult.path
         addCandidates(persistentResult)
     }
 
-    override suspend fun next(): PersistentSymbolicState = deque.pollFirst()
+    override suspend fun next(): Pair<Method, PersistentSymbolicState> = method to deque.pollFirst()
 
     override fun reverse(pathClause: PathClause): PathClause? = pathClause.reversed()
 
@@ -85,6 +98,7 @@ class BfsPathSelectorImpl(
             if (coveredPaths.any { reversed in it }) null
             else reversed
         }
+
         is SwitchInst -> when (predicate) {
             is DefaultSwitchPredicate -> {
                 val defaultSwitch = predicate as DefaultSwitchPredicate
@@ -100,6 +114,7 @@ class BfsPathSelectorImpl(
                 }
                 result
             }
+
             is EqualityPredicate -> {
                 val equalityPredicate = predicate as EqualityPredicate
                 val switchInst = instruction as SwitchInst
@@ -120,8 +135,10 @@ class BfsPathSelectorImpl(
                     if (coveredPaths.any { mutated in it }) mutated else null
                 }
             }
+
             else -> unreachable { log.error("Unexpected predicate in switch clause: $predicate") }
         }
+
         is TableSwitchInst -> when (predicate) {
             is DefaultSwitchPredicate -> {
                 val defaultSwitch = predicate as DefaultSwitchPredicate
@@ -137,6 +154,7 @@ class BfsPathSelectorImpl(
                 }
                 result
             }
+
             is EqualityPredicate -> {
                 val equalityPredicate = predicate as EqualityPredicate
                 val switchInst = instruction as TableSwitchInst
@@ -157,8 +175,10 @@ class BfsPathSelectorImpl(
                     if (coveredPaths.any { mutated in it }) null else mutated
                 }
             }
+
             else -> unreachable { log.error("Unexpected predicate in switch clause: $predicate") }
         }
+
         else -> when (val pred = predicate) {
             is EqualityPredicate -> {
                 val (lhv, rhv) = pred.lhv to pred.rhv
@@ -166,21 +186,26 @@ class BfsPathSelectorImpl(
                     is NullTerm -> copy(predicate = path(instruction.location) {
                         lhv inequality null
                     })
+
                     is ConstBoolTerm -> copy(predicate = path(instruction.location) {
                         lhv equality !rhv.value
                     })
+
                     else -> log.warn("Unknown clause $this").let { null }
                 }
             }
+
             is InequalityPredicate -> {
                 val (lhv, rhv) = pred.lhv to pred.rhv
                 when (rhv) {
                     is NullTerm -> copy(predicate = path(instruction.location) {
                         lhv equality null
                     })
+
                     else -> log.warn("Unknown clause $this").let { null }
                 }
             }
+
             else -> null
         }
     }
diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/cgs/ContextGuidedSelector.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/cgs/ContextGuidedSelector.kt
index c3f134b7b..9af59e619 100644
--- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/cgs/ContextGuidedSelector.kt
+++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/cgs/ContextGuidedSelector.kt
@@ -3,6 +3,7 @@ package org.vorpal.research.kex.asm.analysis.concolic.cgs
 import kotlinx.coroutines.yield
 import org.vorpal.research.kex.ExecutionContext
 import org.vorpal.research.kex.asm.analysis.concolic.ConcolicPathSelector
+import org.vorpal.research.kex.asm.analysis.concolic.ConcolicPathSelectorManager
 import org.vorpal.research.kex.asm.manager.NoConcreteInstanceException
 import org.vorpal.research.kex.asm.manager.instantiationManager
 import org.vorpal.research.kex.ktype.kexType
@@ -37,8 +38,18 @@ import org.vorpal.research.kthelper.collection.dequeOf
 import org.vorpal.research.kthelper.logging.log
 import org.vorpal.research.kthelper.`try`
 
+
+class ContextGuidedSelectorManager(
+    override val ctx: ExecutionContext,
+    override val targets: Set<Method>
+) : ConcolicPathSelectorManager {
+    override fun createPathSelectorFor(target: Method): ConcolicPathSelector =
+        ContextGuidedSelector(ctx, target)
+}
+
 class ContextGuidedSelector(
     override val ctx: ExecutionContext,
+    val method: Method
 ) : ConcolicPathSelector {
     private val executionTree = ExecutionTree(ctx)
     private var currentDepth = 0
@@ -77,7 +88,7 @@ class ContextGuidedSelector(
         false
     }.getOrElse { false }
 
-    override suspend fun next(): PersistentSymbolicState {
+    override suspend fun next(): Pair<Method, PersistentSymbolicState> {
         val currentState = states.pollFirst()!!
         visitedContexts += currentState.context
 
@@ -85,7 +96,7 @@ class ContextGuidedSelector(
         val stateSize = currentStateState.clauses.indexOf(currentState.activeClause)
         val state = currentStateState.clauses.subState(0, stateSize)
 
-        return persistentSymbolicState(
+        return method to persistentSymbolicState(
             state,
             currentState.path + currentState.revertedClause,
             currentStateState.concreteTypes,
@@ -115,7 +126,11 @@ class ContextGuidedSelector(
         branchIterator = executionTree.getBranches(currentDepth).shuffled(ctx.random).iterator()
     }
 
-    override suspend fun addExecutionTrace(method: Method, result: ExecutionCompletedResult) {
+    override suspend fun addExecutionTrace(
+        method: Method,
+        checkedState: PersistentSymbolicState,
+        result: ExecutionCompletedResult
+    ) {
         executionTree.addTrace(result.symbolicState.toPersistentState())
     }
 
diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/CoverageGuidedSelector.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/CoverageGuidedSelector.kt
new file mode 100644
index 000000000..92525a1c5
--- /dev/null
+++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/CoverageGuidedSelector.kt
@@ -0,0 +1,61 @@
+package org.vorpal.research.kex.asm.analysis.concolic.coverage
+
+import org.vorpal.research.kex.ExecutionContext
+import org.vorpal.research.kex.asm.analysis.concolic.ConcolicPathSelector
+import org.vorpal.research.kex.asm.analysis.concolic.ConcolicPathSelectorManager
+import org.vorpal.research.kex.trace.symbolic.PathClause
+import org.vorpal.research.kex.trace.symbolic.PersistentSymbolicState
+import org.vorpal.research.kex.trace.symbolic.protocol.ExecutionCompletedResult
+import org.vorpal.research.kfg.ir.Method
+import org.vorpal.research.kfg.ir.value.instruction.Instruction
+
+class CoverageGuidedSelectorManager(
+    override val ctx: ExecutionContext,
+    override val targets: Set<Method>
+) : ConcolicPathSelectorManager {
+    val executionGraph = ExecutionGraph(ctx, targets)
+
+    override fun createPathSelectorFor(target: Method): ConcolicPathSelector =
+        CoverageGuidedSelector(this)
+
+    private val targetInstructions = targets.flatMapTo(mutableSetOf()) { it.body.flatten() }
+    private val coveredInstructions = mutableSetOf<Instruction>()
+
+    fun addCoverage(trace: List<Instruction>) {
+        coveredInstructions += trace
+    }
+
+    fun isCovered(): Boolean = coveredInstructions.containsAll(targetInstructions)
+    fun isCovered(instruction: Instruction): Boolean = instruction in coveredInstructions
+}
+
+class CoverageGuidedSelector(
+    private val manager: CoverageGuidedSelectorManager
+) : ConcolicPathSelector {
+    override val ctx: ExecutionContext
+        get() = manager.ctx
+    private val executionGraph get() = manager.executionGraph
+    private val candidates = mutableMapOf<PersistentSymbolicState, CandidateState>()
+
+    override suspend fun isEmpty(): Boolean = manager.isCovered() || executionGraph.candidates.isEmpty()
+
+    override suspend fun hasNext(): Boolean = !isEmpty()
+
+    override suspend fun next(): Pair<Method, PersistentSymbolicState> {
+        val candidate = executionGraph.candidates.nextCandidate()
+        candidates[candidate.state] = candidate
+        return candidate.method to candidate.state
+    }
+
+    override suspend fun addExecutionTrace(
+        method: Method,
+        checkedState: PersistentSymbolicState,
+        result: ExecutionCompletedResult
+    ) {
+        manager.addCoverage(result.trace)
+        executionGraph.addTrace(method, candidates[checkedState], result)
+    }
+
+    override fun reverse(pathClause: PathClause): PathClause = TODO() //pathClause.reversed()
+
+}
diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/ExecutionGraph.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/ExecutionGraph.kt
new file mode 100644
index 000000000..fccde853b
--- /dev/null
+++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/ExecutionGraph.kt
@@ -0,0 +1,534 @@
+package org.vorpal.research.kex.asm.analysis.concolic.coverage
+
+import kotlinx.collections.immutable.PersistentList
+import kotlinx.collections.immutable.toPersistentList
+import org.vorpal.research.kex.ExecutionContext
+import org.vorpal.research.kex.asm.manager.NoConcreteInstanceException
+import org.vorpal.research.kex.asm.manager.instantiationManager
+import org.vorpal.research.kex.ktype.KexRtManager.isKexRt
+import org.vorpal.research.kex.ktype.kexType
+import org.vorpal.research.kex.state.predicate.DefaultSwitchPredicate
+import org.vorpal.research.kex.state.predicate.EqualityPredicate
+import org.vorpal.research.kex.state.predicate.InequalityPredicate
+import org.vorpal.research.kex.state.predicate.Predicate
+import org.vorpal.research.kex.state.predicate.path
+import org.vorpal.research.kex.state.predicate.predicate
+import org.vorpal.research.kex.state.term.ConstBoolTerm
+import org.vorpal.research.kex.state.term.InstanceOfTerm
+import org.vorpal.research.kex.state.term.boolValue
+import org.vorpal.research.kex.state.term.numericValue
+import org.vorpal.research.kex.state.transformer.TermCollector
+import org.vorpal.research.kex.trace.symbolic.PathClause
+import org.vorpal.research.kex.trace.symbolic.PathClauseType
+import org.vorpal.research.kex.trace.symbolic.PersistentClauseList
+import org.vorpal.research.kex.trace.symbolic.PersistentSymbolicState
+import org.vorpal.research.kex.trace.symbolic.persistentSymbolicState
+import org.vorpal.research.kex.trace.symbolic.protocol.ExecutionCompletedResult
+import org.vorpal.research.kex.trace.symbolic.toPersistentState
+import org.vorpal.research.kex.util.isSubtypeOfCached
+import org.vorpal.research.kex.util.next
+import org.vorpal.research.kfg.arrayIndexOOBClass
+import org.vorpal.research.kfg.classCastClass
+import org.vorpal.research.kfg.ir.BasicBlock
+import org.vorpal.research.kfg.ir.Method
+import org.vorpal.research.kfg.ir.value.EmptyUsageContext
+import org.vorpal.research.kfg.ir.value.IntConstant
+import org.vorpal.research.kfg.ir.value.Value
+import org.vorpal.research.kfg.ir.value.instruction.BranchInst
+import org.vorpal.research.kfg.ir.value.instruction.CallInst
+import org.vorpal.research.kfg.ir.value.instruction.CatchInst
+import org.vorpal.research.kfg.ir.value.instruction.Instruction
+import org.vorpal.research.kfg.ir.value.instruction.ReturnInst
+import org.vorpal.research.kfg.ir.value.instruction.SwitchInst
+import org.vorpal.research.kfg.ir.value.instruction.TableSwitchInst
+import org.vorpal.research.kfg.nullptrClass
+import org.vorpal.research.kfg.type.ClassType
+import org.vorpal.research.kfg.type.Type
+import org.vorpal.research.kthelper.assert.unreachable
+import org.vorpal.research.kthelper.graph.GraphView
+import org.vorpal.research.kthelper.graph.PredecessorGraph
+import org.vorpal.research.kthelper.graph.Viewable
+import org.vorpal.research.kthelper.logging.log
+import kotlin.math.exp
+import kotlin.math.pow
+
+fun Predicate.reverseBoolCond() = when (this) {
+    is EqualityPredicate -> predicate(this.type, this.location) {
+        lhv equality !(rhv as ConstBoolTerm).value
+    }
+
+    is InequalityPredicate -> predicate(this.type, this.location) {
+        lhv inequality !(rhv as ConstBoolTerm).value
+    }
+
+    else -> unreachable { log.error("Unexpected predicate in bool cond: $this") }
+}
+
+fun Predicate.reverseSwitchCond(
+    predecessors: Set<PersistentSymbolicState>,
+    branches: Map<Value, BasicBlock>
+): List<Predicate> = when (this) {
+    is DefaultSwitchPredicate -> branches.keys
+        .mapTo(mutableSetOf()) { (it as IntConstant).value }
+        .map {
+            predicate(this.type, this.location) {
+                cond equality it
+            }
+        }
+
+    is EqualityPredicate -> {
+        val outgoingPaths = branches.toList()
+            .groupBy({ it.second }, { it.first })
+            .map { it.value.mapTo(mutableSetOf()) { const -> (const as IntConstant).value } }
+
+        val equivalencePaths = mutableMapOf<Int, Set<Int>>()
+        for (set in outgoingPaths) {
+            for (value in set) {
+                equivalencePaths[value] = set
+            }
+        }
+
+        val visitedCandidates = predecessors
+            .map { it.path.last().predicate }
+            .filterIsInstance<EqualityPredicate>()
+            .mapTo(mutableSetOf()) { it.rhv.numericValue }
+
+        val candidates = run {
+            val currentRange = branches.keys.map { (it as IntConstant).value }.toMutableSet()
+            for (candidate in visitedCandidates) {
+                val visited: Set<Int> = equivalencePaths[candidate] ?: emptySet()
+                currentRange.removeAll(visited)
+            }
+            currentRange
+        }
+
+        candidates.map {
+            predicate(type, location) {
+                lhv equality it
+            }
+        }
+    }
+
+    else -> unreachable { log.error("Unexpected predicate in switch clause: $this") }
+}
+
+
+sealed class Vertex(
+    val type: String,
+    val instruction: Instruction
+) : PredecessorGraph.PredecessorVertex<Vertex> {
+    companion object {
+        const val STATE = "STATE"
+    }
+
+    private val _predecessors = mutableSetOf<Vertex>()
+    private val _successors = mutableSetOf<Vertex>()
+
+    override val predecessors: Set<Vertex>
+        get() = _predecessors
+    override val successors: Set<Vertex>
+        get() = _successors
+
+    fun linkDown(other: Vertex) {
+        _successors += other
+        other._predecessors += this
+    }
+
+    override fun toString(): String {
+        return "Vertex($type, ${instruction.print()})"
+    }
+}
+
+class StateVertex(
+    instruction: Instruction
+) : Vertex(STATE, instruction)
+
+class PathVertex(
+    pathType: PathClauseType,
+    instruction: Instruction
+) : Vertex(pathType.name, instruction) {
+    private val states = hashMapOf<PersistentClauseList, MutableSet<PersistentSymbolicState>>()
+    private val visitedPrefixes = hashSetOf<PersistentClauseList>()
+
+    fun addStateAndProduceCandidates(
+        ctx: ExecutionContext,
+        state: PersistentSymbolicState
+    ): List<PersistentSymbolicState> {
+        val prefix = state.clauses.dropLast(1)
+        val condition = state.path.last()
+        val prefixStates = states.getOrPut(prefix, ::hashSetOf).also {
+            it += state
+        }
+        return when (prefix) {
+            in visitedPrefixes -> emptyList()
+            else -> {
+                visitedPrefixes += prefix
+                val reversedConditions = when (condition.type) {
+                    PathClauseType.NULL_CHECK -> listOf(condition.copy(predicate = condition.predicate.reverseBoolCond()))
+                    PathClauseType.TYPE_CHECK -> listOf(condition.copy(predicate = condition.predicate.reverseBoolCond()))
+                    PathClauseType.BOUNDS_CHECK -> listOf(condition.copy(predicate = condition.predicate.reverseBoolCond()))
+                    PathClauseType.CONDITION_CHECK -> when (val inst = condition.instruction) {
+                        is BranchInst -> listOf(condition.copy(predicate = condition.predicate.reverseBoolCond()))
+                        is SwitchInst -> condition.predicate.reverseSwitchCond(prefixStates, inst.branches).map {
+                            condition.copy(predicate = it)
+                        }
+
+                        is TableSwitchInst -> {
+                            val branches = inst.range.let { range ->
+                                range.associateWith { inst.branches[it - range.first] }
+                                    .mapKeys { ctx.values.getInt(it.key) }
+                            }
+                            condition.predicate.reverseSwitchCond(prefixStates, branches).map {
+                                condition.copy(predicate = it)
+                            }
+                        }
+
+                        else -> unreachable { log.error("Unexpected predicate in clause $inst") }
+                    }
+
+                    PathClauseType.OVERLOAD_CHECK -> {
+                        val excludeClasses = prefixStates
+                            .asSequence()
+                            .map { it.path.last().predicate }
+                            .flatMap { TermCollector.getFullTermSet(it).filterIsInstance<InstanceOfTerm>() }
+                            .map { it.checkedType.getKfgType(ctx.types) }
+                            .filterIsInstance<ClassType>()
+                            .mapTo(mutableSetOf()) { it.klass }
+
+                        try {
+                            val lhv = condition.predicate.operands[0] as InstanceOfTerm
+                            val termType = lhv.operand.type.getKfgType(ctx.types)
+                            val allCandidates = instantiationManager.getAll(termType, ctx.accessLevel, excludeClasses)
+                                .filterNot { it.isKexRt }
+                            // TODO: add proper prioritization
+                            val prioritizedCandidates = allCandidates.shuffled(ctx.random).take(5)
+                            prioritizedCandidates.map {
+                                condition.copy(predicate = path(instruction.location) {
+                                    (lhv.operand `is` it.kexType) equality true
+                                })
+                            }
+                        } catch (e: NoConcreteInstanceException) {
+                            emptyList()
+                        }
+                    }
+                }
+                reversedConditions.map {
+                    persistentSymbolicState(
+                        prefix,
+                        state.path.dropLast(1) + it,
+                        state.concreteTypes,
+                        state.concreteValues,
+                        state.termMap
+                    )
+                }
+            }
+        }
+    }
+}
+
+private fun PersistentSymbolicState.findExceptionHandlerInst(
+    type: Type,
+    stateStackTrace: PersistentList<Pair<Instruction?, Method>>
+): Instruction? {
+    val currentClause = path.last()
+    val stackTrace = stateStackTrace.mapNotNullTo(mutableListOf()) { it.first }
+    stackTrace.add(currentClause.instruction)
+    var result: Instruction? = null
+    stackTrace@ for (inst in stackTrace.asReversed()) {
+        for (handler in inst.parent.handlers) {
+            if (type.isSubtypeOfCached(handler.exception)) {
+                result = handler.first()
+                break@stackTrace
+            }
+        }
+    }
+    return result
+}
+
+class CandidateState(
+    val method: Method,
+    val state: PersistentSymbolicState,
+    val stackTrace: PersistentList<Pair<Instruction?, Method>>
+) {
+    val nextInstruction: Instruction?
+    var score: Long = 0L
+
+    init {
+        val cm = method.cm
+        val currentClause = state.path.last()
+        nextInstruction = when (currentClause.type) {
+            PathClauseType.NULL_CHECK -> when (currentClause.predicate.operands[1].boolValue) {
+                true -> state.findExceptionHandlerInst(cm.nullptrClass.asType, stackTrace)
+                false -> currentClause.instruction.next
+            }
+
+            PathClauseType.TYPE_CHECK -> when (currentClause.predicate.operands[1].boolValue) {
+                true -> currentClause.instruction.next
+                false -> state.findExceptionHandlerInst(cm.classCastClass.asType, stackTrace)
+            }
+
+            PathClauseType.BOUNDS_CHECK -> when (currentClause.predicate.operands[1].boolValue) {
+                true -> currentClause.instruction.next
+                false -> state.findExceptionHandlerInst(cm.arrayIndexOOBClass.asType, stackTrace)
+            }
+
+            PathClauseType.OVERLOAD_CHECK -> {
+                val checkedType =
+                    (currentClause.predicate.operands[0] as InstanceOfTerm).checkedType.getKfgType(cm.type)
+                val callInst = currentClause.instruction as CallInst
+                when (checkedType) {
+                    is ClassType -> {
+                        val calledMethod = checkedType.klass.getMethod(
+                            callInst.method.name,
+                            callInst.method.returnType,
+                            *callInst.method.argTypes.toTypedArray()
+                        )
+                        when {
+                            calledMethod.hasBody -> calledMethod.body.entry.first()
+                            else -> callInst.next
+                        }
+                    }
+
+                    else -> callInst.next
+                }
+            }
+
+            PathClauseType.CONDITION_CHECK -> when (val inst = currentClause.instruction) {
+                is BranchInst -> when (currentClause.predicate.operands[1].boolValue) {
+                    true -> inst.trueSuccessor.first()
+                    false -> inst.falseSuccessor.first()
+                }
+
+                is SwitchInst -> {
+                    val numericValue = currentClause.predicate.operands[1].numericValue
+                    var result: Instruction? = null
+                    for ((key, branch) in inst.branches) {
+                        if (numericValue == (key as IntConstant).value) {
+                            result = branch.first()
+                        }
+                    }
+                    if (result == null) {
+                        result = inst.default.first()
+                    }
+                    result
+                }
+
+                is TableSwitchInst -> {
+                    val numericValue = currentClause.predicate.operands[1].numericValue
+                    var result: Instruction? = null
+                    for (key in inst.range) {
+                        if (numericValue == key) {
+                            result = inst.branches[key - inst.range.first].first()
+                        }
+                    }
+                    if (result == null) {
+                        result = inst.default.first()
+                    }
+                    result
+                }
+
+                else -> unreachable { log.error("Unexpected instruction in condition check: $inst") }
+            }
+        }
+    }
+
+    override fun equals(other: Any?): Boolean {
+        if (this === other) return true
+        if (javaClass != other?.javaClass) return false
+
+        other as CandidateState
+
+        return state == other.state
+    }
+
+    override fun hashCode(): Int {
+        return state.hashCode()
+    }
+}
+
+
+// TODO: add concurrency support
+class ExecutionGraph(
+    val ctx: ExecutionContext,
+    private val targets: Set<Method>
+) : PredecessorGraph<Vertex>, Viewable {
+
+    companion object {
+        const val DEFAULT_SCORE = 10_000L
+        const val SIGMA = 10.0
+    }
+
+    private val root: Vertex = StateVertex(ctx.cm.instruction.getUnreachable(EmptyUsageContext))
+    private val innerNodes = hashMapOf<Pair<String, Instruction>, Vertex>().also {
+        it["STATE" to root.instruction] = root
+    }
+    private val instructionGraph = InstructionGraph(targets)
+    val candidates = CandidateSet(ctx)
+
+    override val entry: Vertex
+        get() = root
+
+    override val nodes: Set<Vertex>
+        get() = innerNodes.values.toSet()
+
+    inner class CandidateSet(val ctx: ExecutionContext) : Iterable<CandidateState> {
+        private var isValid = false
+        private var totalScore: Long = 0L
+        private val candidates = hashSetOf<CandidateState>()
+
+        override fun iterator(): Iterator<CandidateState> = candidates.iterator()
+
+        fun isEmpty() = candidates.isEmpty()
+
+        fun addAll(newCandidates: Collection<CandidateState>) {
+            candidates.addAll(newCandidates)
+            newCandidates.forEach { totalScore += it.score }
+        }
+
+        private fun remove(candidateState: CandidateState) {
+            if (candidates.remove(candidateState)) {
+                totalScore -= candidateState.score
+            }
+        }
+
+        fun invalidate() {
+            isValid = false
+        }
+
+        private fun recomputeScores() {
+            totalScore = 0L
+            candidates.forEach {
+                it.recomputeScore()
+                totalScore += it.score
+            }
+            isValid = true
+        }
+
+        fun nextCandidate(): CandidateState {
+            if (!isValid) recomputeScores()
+            if (totalScore == 0L) {
+                return candidates.first().also { remove(it) }
+            }
+
+            val random = ctx.random.nextLong(totalScore)
+            var current = 0L
+            for (state in candidates) {
+                current += state.score
+                if (random < current) {
+                    remove(state)
+                    return state
+                }
+            }
+            return unreachable { log.error("Unexpected error") }
+        }
+    }
+
+    private fun CandidateState.recomputeScore() {
+        var newScore = 0L
+        if (nextInstruction != null) {
+            newScore += 1L
+
+            val scaleDistance = { distance: Int ->
+                val normalizedDistance = exp(-0.5 * (distance.toDouble() / SIGMA).pow(2))
+                (normalizedDistance * DEFAULT_SCORE).toLong()
+            }
+
+            val (targetDistance, _) = instructionGraph.getVertex(nextInstruction)
+                .distanceToUncovered(targets, stackTrace)
+            newScore += scaleDistance(targetDistance)
+//            newScore += scaleDistance(uncoveredDistance) / 10L
+        }
+        score = newScore
+    }
+
+    @Suppress("UNUSED_PARAMETER")
+    fun addTrace(method: Method, candidate: CandidateState?, executionResult: ExecutionCompletedResult) {
+        instructionGraph.addTrace(executionResult.trace)
+        var prevVertex = root
+        var clauseIndex = 0
+        var pathIndex = 0
+        val symbolicState = executionResult.symbolicState.toPersistentState()
+
+        var previousInstruction: Instruction? = null
+        val stackTrace = mutableListOf<Pair<Instruction?, Method>>()
+
+        for (clause in symbolicState.clauses) {
+            // stack trace building part
+            val currentInstruction = clause.instruction
+            val currentMethod = currentInstruction.parent.method
+            when (currentInstruction) {
+                currentMethod.body.entry.first() -> {
+                    stackTrace += previousInstruction to currentMethod
+                }
+
+                is CallInst -> {
+                    previousInstruction = currentInstruction
+                }
+
+                is ReturnInst -> stackTrace.removeLast()
+                is CatchInst -> while (stackTrace.last().second != currentMethod) {
+                    stackTrace.removeLast()
+                }
+            }
+
+            // candidate states calculation part
+            ++clauseIndex
+            // TODO: limit number of states
+//                if (clauseIndex > 10_000) break
+            if (clause is PathClause) ++pathIndex
+
+            val type = when (clause) {
+                is PathClause -> clause.type.toString()
+                else -> Vertex.STATE
+            }
+            val currentVertex = innerNodes.getOrPut(type to clause.instruction) {
+                candidates.invalidate()
+                when (clause) {
+                    is PathClause -> PathVertex(clause.type, clause.instruction)
+                    else -> StateVertex(clause.instruction)
+                }
+            }
+
+            if (clause is PathClause) {
+                currentVertex as PathVertex
+                val currentStackTrace = stackTrace.toPersistentList()
+
+                candidates.addAll(
+                    currentVertex.addStateAndProduceCandidates(
+                        ctx, persistentSymbolicState(
+                            symbolicState.clauses.subState(0, clauseIndex),
+                            symbolicState.path.subPath(0, pathIndex),
+                            symbolicState.concreteTypes,
+                            symbolicState.concreteValues,
+                            symbolicState.termMap
+                        )
+                    ).mapTo(mutableSetOf()) { CandidateState(method, it, currentStackTrace) }
+                )
+            }
+
+            prevVertex.linkDown(currentVertex)
+            prevVertex = currentVertex
+        }
+    }
+
+    override val graphView: List<GraphView>
+        get() {
+            val graphNodes = mutableMapOf<Vertex, GraphView>()
+
+            var i = 0
+            for (vertex in nodes) {
+                graphNodes[vertex] = GraphView("${i++}", "$vertex".replace("\"", "\\\"")) {
+                    it.setColor(info.leadinglight.jdot.enums.Color.X11.black)
+                }
+            }
+
+            for (vertex in nodes) {
+                val current = graphNodes.getValue(vertex)
+                for (child in vertex.successors) {
+                    current.addSuccessor(graphNodes.getValue(child))
+                }
+            }
+
+            return graphNodes.values.toList()
+        }
+}
diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/InstructionGraph.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/InstructionGraph.kt
new file mode 100644
index 000000000..52e5be1b8
--- /dev/null
+++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/InstructionGraph.kt
@@ -0,0 +1,244 @@
+package org.vorpal.research.kex.asm.analysis.concolic.coverage
+
+import info.leadinglight.jdot.enums.Color
+import kotlinx.collections.immutable.PersistentList
+import org.vorpal.research.kex.asm.manager.instantiationManager
+import org.vorpal.research.kex.asm.util.AccessModifier
+import org.vorpal.research.kex.ktype.KexRtManager.isKexRt
+import org.vorpal.research.kex.ktype.KexRtManager.rtMapped
+import org.vorpal.research.kex.ktype.KexRtManager.rtUnmapped
+import org.vorpal.research.kfg.ir.BasicBlock
+import org.vorpal.research.kfg.ir.Method
+import org.vorpal.research.kfg.ir.value.instruction.ArrayLoadInst
+import org.vorpal.research.kfg.ir.value.instruction.ArrayStoreInst
+import org.vorpal.research.kfg.ir.value.instruction.BranchInst
+import org.vorpal.research.kfg.ir.value.instruction.CallInst
+import org.vorpal.research.kfg.ir.value.instruction.CallOpcode
+import org.vorpal.research.kfg.ir.value.instruction.FieldLoadInst
+import org.vorpal.research.kfg.ir.value.instruction.FieldStoreInst
+import org.vorpal.research.kfg.ir.value.instruction.Instruction
+import org.vorpal.research.kfg.ir.value.instruction.ReturnInst
+import org.vorpal.research.kfg.ir.value.instruction.TerminateInst
+import org.vorpal.research.kthelper.assert.ktassert
+import org.vorpal.research.kthelper.collection.mapToArray
+import org.vorpal.research.kthelper.collection.queueOf
+import org.vorpal.research.kthelper.graph.GraphView
+import org.vorpal.research.kthelper.graph.Viewable
+import org.vorpal.research.kthelper.tryOrNull
+
+
+@Suppress("MemberVisibilityCanBePrivate")
+class InstructionGraph(
+    val targets: Set<Method>
+) : Viewable {
+    private val nodes = mutableMapOf<Instruction, Vertex>()
+
+    var covered = 0
+
+    inner class Vertex(val instruction: Instruction) {
+        var covered = false
+        val upEdges = mutableSetOf<Vertex>()
+        val downEdges = mutableSetOf<Vertex>()
+
+        override fun toString(): String = instruction.print()
+
+        override fun equals(other: Any?): Boolean {
+            if (this === other) return true
+            if (javaClass != other?.javaClass) return false
+
+            other as Vertex
+
+            return instruction == other.instruction
+        }
+
+        override fun hashCode(): Int {
+            return instruction.hashCode()
+        }
+
+        fun linkDown(other: Vertex) {
+            downEdges += other
+            other.upEdges += this
+        }
+
+        fun distanceToUncovered(
+            targets: Set<Method>,
+            initialStackTrace: PersistentList<Pair<Instruction?, Method>>
+        ): Pair<Int, Int> {
+            var minTargetDistance = Int.MAX_VALUE
+            var minUncoveredDistance = Int.MAX_VALUE
+
+            val distances = mutableMapOf<Vertex, Int>()
+            distances[this] = 0
+            val queue = queueOf(this to initialStackTrace)
+            while (queue.isNotEmpty()) {
+                val (current, stackTrace) = queue.poll()
+                val currentDistance = distances[current]!!
+
+                if (!current.covered) {
+                    if (currentDistance < minUncoveredDistance) {
+                        minUncoveredDistance = currentDistance
+                    }
+                    if (current.instruction.parent.method in targets && currentDistance < minTargetDistance) {
+                        minTargetDistance = currentDistance
+                    }
+                    continue
+                }
+
+                val edges = when (current.instruction) {
+                    is ReturnInst -> {
+                        val newStackTrace = stackTrace.removeAt(stackTrace.size - 1)
+                        if (newStackTrace.isEmpty()) continue
+                        current.downEdges.filter { it.instruction.parent.method == newStackTrace.last().second }
+                            .map { it to newStackTrace }
+                    }
+
+                    is CallInst -> {
+                        current.downEdges.map {
+                            if (it.instruction.parent.method != current.instruction.parent.method) {
+                                it to stackTrace.add(it.instruction to it.instruction.parent.method)
+                            } else {
+                                it to stackTrace
+                            }
+                        }
+                    }
+
+                    else -> current.downEdges.map { it to stackTrace }
+                }
+
+                for ((edge, edgeStackTrace) in edges) {
+                    val distance = distances.getOrDefault(edge, Int.MAX_VALUE)
+                    val stepValue = when (current.instruction) {
+                        is CallInst -> 2
+                        is FieldLoadInst, is FieldStoreInst -> 1
+                        is ArrayLoadInst, is ArrayStoreInst -> 1
+                        is BranchInst -> 1
+                        else -> 0
+                    }
+                    if (distance > (currentDistance + stepValue)) {
+                        distances[edge] = currentDistance + stepValue
+                        queue += edge to edgeStackTrace
+                    }
+                }
+            }
+            return minTargetDistance to minUncoveredDistance
+        }
+    }
+
+    fun getVertex(instruction: Instruction): Vertex {
+        if (instruction in nodes) {
+            return nodes[instruction]!!
+        } else {
+            val method = instruction.parent.method
+            ktassert(instruction == method.body.entry.first())
+
+            val queue = queueOf<Triple<Vertex?, BasicBlock, Int>>()
+            queue += Triple(null, method.body.entry, 0)
+            queue.addAll(method.body.catchEntries.map { Triple(null, it, 0) })
+            val visited = mutableSetOf<Pair<Instruction?, Instruction>>()
+            val resolves = mutableMapOf<Instruction, List<Method>>()
+
+            while (queue.isNotEmpty()) {
+                val (prev, block, index) = queue.poll()
+                val current = block.instructions[index]
+                if (prev?.instruction to current in visited) continue
+                visited += prev?.instruction to current
+
+                val vertex = nodes.getOrPut(current) { Vertex(current) }
+                prev?.linkDown(vertex)
+
+                when (current) {
+                    is CallInst -> {
+                        val resolvedMethods = resolves.getOrPut(current) {
+                            when (current.opcode) {
+                                CallOpcode.STATIC -> listOf(current.method)
+                                CallOpcode.SPECIAL -> listOf(current.method)
+                                CallOpcode.INTERFACE, CallOpcode.VIRTUAL -> {
+                                    val currentMethod = current.method
+
+                                    val targetPackages = targets.map { it.klass.pkg }.toSet()
+
+                                    val retTypeMapped = currentMethod.returnType.rtMapped
+                                    val argTypesMapped = currentMethod.argTypes.mapToArray { it.rtMapped }
+                                    val retTypeUnmapped = currentMethod.returnType.rtUnmapped
+                                    val argTypesUnmapped = currentMethod.argTypes.mapToArray { it.rtUnmapped }
+                                    instantiationManager.getAllConcreteSubtypes(
+                                        currentMethod.klass,
+                                        AccessModifier.Private
+                                    )
+                                        .filter { klass -> targetPackages.any { it.isParent(klass.pkg) } }
+                                        .mapNotNullTo(mutableSetOf()) {
+                                            tryOrNull {
+                                                if (it.isKexRt) {
+                                                    it.getMethod(currentMethod.name, retTypeMapped, *argTypesMapped)
+                                                } else {
+                                                    it.getMethod(currentMethod.name, retTypeUnmapped, *argTypesUnmapped)
+                                                }
+                                            }
+                                        }
+                                        .filter { it.hasBody }
+                                }
+                            }.filter { it.hasBody }
+                        }
+                        for (candidate in resolvedMethods) {
+                            queue += Triple(vertex, candidate.body.entry, 0)
+                            queue.addAll(candidate.body.catchEntries.map { Triple(null, it, 0) })
+
+                            candidate.body.flatten().filterIsInstance<ReturnInst>().forEach {
+                                val returnVertex = nodes.getOrPut(it) { Vertex(it) }
+                                queue += Triple(returnVertex, block, index + 1)
+                            }
+                        }
+                        if (resolvedMethods.isEmpty()) {
+                            queue += Triple(vertex, block, index + 1)
+                        }
+                    }
+
+                    is TerminateInst -> current.successors.forEach {
+                        queue += Triple(vertex, it, 0)
+                    }
+
+                    else -> queue += Triple(vertex, block, index + 1)
+                }
+            }
+
+            return nodes.getOrPut(instruction) { Vertex(instruction) }
+        }
+    }
+
+    fun addTrace(trace: List<Instruction>) {
+        var prev: Vertex? = null
+        for (inst in trace) {
+            val current = getVertex(inst)
+            if (!current.covered) ++covered
+
+            current.covered = true
+            prev?.linkDown(current)
+            prev = current
+        }
+    }
+
+    override val graphView: List<GraphView>
+        get() {
+            val graphNodes = mutableMapOf<Vertex, GraphView>()
+
+            var i = 0
+            for (vertex in nodes.values) {
+                graphNodes[vertex] = GraphView("${i++}", "$vertex".replace("\"", "\\\"")) {
+                    val color = when {
+                        vertex.covered -> Color.X11.green
+                        else -> Color.X11.red
+                    }
+                    it.setColor(color)
+                }
+            }
+
+            for (vertex in nodes.values) {
+                val current = graphNodes.getValue(vertex)
+                for (child in vertex.downEdges) {
+                    current.addSuccessor(graphNodes.getValue(child))
+                }
+            }
+
+            return graphNodes.values.toList()
+        }
+}
diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/gui/GUIProxySelector.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/gui/GUIProxySelector.kt
index 4ffa3a7e6..5f02557d8 100644
--- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/gui/GUIProxySelector.kt
+++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/gui/GUIProxySelector.kt
@@ -40,16 +40,20 @@ class GUIProxySelector(private val concolicPathSelector: ConcolicPathSelector) :
 
     override suspend fun isEmpty(): Boolean = concolicPathSelector.isEmpty()
 
-    override suspend fun addExecutionTrace(method: Method, result: ExecutionCompletedResult) {
+    override suspend fun addExecutionTrace(
+        method: Method,
+        checkedState: PersistentSymbolicState,
+        result: ExecutionCompletedResult
+    ) {
         val vertices = graph.addTrace(result.symbolicState.toPersistentState())
         val json = Json.encodeToString(vertices)
         log.debug("Vertices trace: $json")
         log.debug(graph)
         client.send(json)
-        concolicPathSelector.addExecutionTrace(method, result)
+        concolicPathSelector.addExecutionTrace(method, checkedState, result)
     }
 
-    override suspend fun next(): PersistentSymbolicState {
+    override suspend fun next(): Pair<Method, PersistentSymbolicState> {
         log.debug("Waiting for client decision")
         val received = client.receive()
 
@@ -61,7 +65,8 @@ class GUIProxySelector(private val concolicPathSelector: ConcolicPathSelector) :
         val vertex: Vertex = Json.decodeFromString(received)
         log.debug("Received vertex: {}", vertex)
 
-        return interactiveNext(vertex) ?: concolicPathSelector.next()
+        return interactiveNext(vertex)?.let { it.clauses.first().instruction.parent.method to it }
+            ?: concolicPathSelector.next()
     }
 
     private fun interactiveNext(vertex: Vertex): PersistentSymbolicState? {
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 c5faf9224..cc75aba54 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
@@ -31,6 +31,7 @@ import org.vorpal.research.kex.state.transformer.Optimizer
 import org.vorpal.research.kex.state.transformer.RecursiveInliner
 import org.vorpal.research.kex.state.transformer.ReflectionInfoAdapter
 import org.vorpal.research.kex.state.transformer.Slicer
+import org.vorpal.research.kex.state.transformer.StaticFieldWDescriptorInliner
 import org.vorpal.research.kex.state.transformer.StensgaardAA
 import org.vorpal.research.kex.state.transformer.StringMethodAdapter
 import org.vorpal.research.kex.state.transformer.TermCollector
@@ -52,6 +53,7 @@ class AsyncChecker(
 ) {
     private val isSlicingEnabled = kexConfig.getBooleanValue("smt", "slicing", false)
     private val logQuery = kexConfig.getBooleanValue("smt", "logQuery", false)
+    private val useADSolver = kexConfig.getBooleanValue("smt", "useADSolver", false)
     private val psa = PredicateStateAnalysis(ctx.cm)
 
     lateinit var state: PredicateState
@@ -100,6 +102,7 @@ class AsyncChecker(
         +BoolTypeAdapter(method.cm.type)
         +ClassMethodAdapter(method.cm)
         +ConstEnumAdapter(ctx)
+        +StaticFieldWDescriptorInliner(ctx)
         +ConstStringAdapter(method.cm.type)
         +StringMethodAdapter(ctx.cm)
         +ConcolicArrayLengthAdapter()
@@ -158,9 +161,11 @@ class AsyncChecker(
             log.debug("Query size: {}", query.size)
         }
 
-        tryAbstractDomainSolve(ctx, state, query)?.let {
-            log.debug("Constant solver acquired {}", it)
-            return it
+        if (useADSolver) {
+            tryAbstractDomainSolve(ctx, state, query)?.let {
+                log.debug("Constant solver acquired {}", it)
+                return it
+            }
         }
 
         val result = AsyncSMTProxySolver(ctx).use {
diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/AsyncIncrementalChecker.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/AsyncIncrementalChecker.kt
index cd7b68a51..70b475c2d 100644
--- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/AsyncIncrementalChecker.kt
+++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/AsyncIncrementalChecker.kt
@@ -24,6 +24,7 @@ import org.vorpal.research.kex.state.transformer.KexRtAdapter
 import org.vorpal.research.kex.state.transformer.NewFieldInitializer
 import org.vorpal.research.kex.state.transformer.Optimizer
 import org.vorpal.research.kex.state.transformer.RecursiveInliner
+import org.vorpal.research.kex.state.transformer.StaticFieldWDescriptorInliner
 import org.vorpal.research.kex.state.transformer.StringMethodAdapter
 import org.vorpal.research.kex.state.transformer.TypeInfoMap
 import org.vorpal.research.kex.state.transformer.TypeNameAdapter
@@ -84,6 +85,7 @@ class AsyncIncrementalChecker(
         +BoolTypeAdapter(method.cm.type)
         +ClassMethodAdapter(method.cm)
         +ConstEnumAdapter(ctx)
+        +StaticFieldWDescriptorInliner(ctx)
         +ConstStringAdapter(method.cm.type)
         +StringMethodAdapter(ctx.cm)
         +ConcolicArrayLengthAdapter()
diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/state/transformer/StaticFieldInliner.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/state/transformer/StaticFieldInliner.kt
index 8abb5570e..380f6887c 100644
--- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/state/transformer/StaticFieldInliner.kt
+++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/state/transformer/StaticFieldInliner.kt
@@ -6,19 +6,27 @@ import org.vorpal.research.kex.asm.state.PredicateStateAnalysis
 import org.vorpal.research.kex.config.kexConfig
 import org.vorpal.research.kex.descriptor.ClassDescriptor
 import org.vorpal.research.kex.descriptor.Descriptor
+import org.vorpal.research.kex.descriptor.Object2DescriptorConverter
 import org.vorpal.research.kex.descriptor.descriptor
 import org.vorpal.research.kex.ktype.kexType
 import org.vorpal.research.kex.smt.Checker
 import org.vorpal.research.kex.smt.Result
+import org.vorpal.research.kex.state.IncrementalPredicateState
 import org.vorpal.research.kex.state.PredicateState
 import org.vorpal.research.kex.state.StateBuilder
+import org.vorpal.research.kex.state.predicate.state
 import org.vorpal.research.kex.state.term.FieldLoadTerm
 import org.vorpal.research.kex.state.term.FieldTerm
 import org.vorpal.research.kex.state.term.Term
 import org.vorpal.research.kex.util.KfgTargetFilter
+import org.vorpal.research.kex.util.allFields
+import org.vorpal.research.kex.util.isFinal
+import org.vorpal.research.kex.util.isStatic
+import org.vorpal.research.kex.util.loadClass
 import org.vorpal.research.kfg.ir.Class
 import org.vorpal.research.kfg.ir.Field
 import org.vorpal.research.kfg.ir.Method
+import org.vorpal.research.kfg.type.ClassType
 import org.vorpal.research.kthelper.collection.dequeOf
 import org.vorpal.research.kthelper.logging.log
 import org.vorpal.research.kthelper.`try`
@@ -160,3 +168,69 @@ class StaticFieldInliner(
         ps
     }
 }
+
+
+class StaticFieldWDescriptorInliner(
+    val ctx: ExecutionContext
+) : RecollectingTransformer<StaticFieldWDescriptorInliner>, IncrementalTransformer {
+    override val builders = dequeOf(StateBuilder())
+
+    companion object {
+        private val objectConverter = Object2DescriptorConverter()
+        private val staticFields = mutableMapOf<Class, MutableMap<String, Descriptor>>()
+
+        private fun getStaticField(ctx: ExecutionContext, field: Field): Descriptor? = when (field.klass) {
+            in staticFields -> staticFields[field.klass]!![field.name]
+            else -> {
+                val loadedKlass = ctx.loader.loadClass(field.klass)
+                val fields = mutableMapOf<String, Descriptor>()
+                staticFields[field.klass] = fields
+                for (fieldReflection in loadedKlass.allFields) {
+                    if (fieldReflection.isStatic && fieldReflection.isFinal) {
+                        fields[fieldReflection.name] = tryOrNull {
+                            objectConverter.convert(fieldReflection.get(null))
+                        } ?: continue
+                    }
+                }
+                fields[field.name]
+            }
+        }
+    }
+
+    private val Term.isEnum get() = (this.type.getKfgType(ctx.cm.type) as? ClassType)?.klass?.isEnum ?: false
+
+    override fun apply(ps: PredicateState): PredicateState = `try` {
+        val staticFields = TermCollector.getFullTermSet(ps)
+            .asSequence()
+            .filterIsInstance<FieldLoadTerm>()
+            .mapNotNullTo(mutableSetOf()) {
+                val field = it.field as FieldTerm
+                tryOrNull { field.unmappedKfgField(ctx.cm) }?.let { kfgField ->
+                    if (kfgField.isStatic && kfgField.isFinal && !field.isEnum) {
+                        kfgField
+                    } else {
+                        null
+                    }
+                }
+            }
+            .filterNotTo(mutableSetOf()) { field -> ignores.any { filter -> filter.matches(field.klass) } }
+        for (field in staticFields) {
+            val descriptor = getStaticField(ctx, field) ?: continue
+            currentBuilder += descriptor.initializerState
+            currentBuilder += state {
+                staticRef(field.klass).field(field.type.kexType, field.name).initialize(descriptor.term)
+            }
+        }
+        super.apply(ps)
+    }.getOrElse {
+        log.error("Failed to inline static fields in $ps")
+        ps
+    }
+
+    override fun apply(state: IncrementalPredicateState): IncrementalPredicateState {
+        return IncrementalPredicateState(
+            apply(state.state),
+            state.queries
+        )
+    }
+}
diff --git a/kex-test.ini b/kex-test.ini
index 33efafbe2..131d89212 100644
--- a/kex-test.ini
+++ b/kex-test.ini
@@ -63,7 +63,7 @@ numberOfConcreteMethods = 5
 [concolic]
 timeLimit = 300
 numberOfExecutors = 1
-searchStrategy = cgs
+searchStrategy = coverage
 
 [crash]
 timeLimit = 100
diff --git a/kex-test/src/main/kotlin/org/vorpal/research/kex/test/javadebug/JavaTest.java b/kex-test/src/main/kotlin/org/vorpal/research/kex/test/javadebug/JavaTest.java
index 8c0259474..29215ff6b 100644
--- a/kex-test/src/main/kotlin/org/vorpal/research/kex/test/javadebug/JavaTest.java
+++ b/kex-test/src/main/kotlin/org/vorpal/research/kex/test/javadebug/JavaTest.java
@@ -1,33 +1,49 @@
 package org.vorpal.research.kex.test.javadebug;
 
-import java.util.ArrayList;
+import org.vorpal.research.kex.test.concolic.Point;
 
 @SuppressWarnings("ALL")
 public class JavaTest {
-//    public int foo(Point a, Point b) {
-//        int ax = a.getX();
-//        int bx = b.getX();
-//        int mx = Math.max(ax, bx);
-//
-//        int ay = a.getY();
-//        int by = b.getY();
-//        int my = Math.min(ay, by);
-//        int res;
-//        if (mx < my) {
-//            System.out.println("success");
-//            res = mx - my;
-//        } else {
-//            System.out.println("fail");
-//            res = my - mx;
+    public int foo(Point a, Point b) {
+        int ax = a.getX();
+        int bx = b.getX();
+        int mx = Math.max(ax, bx);
+
+        int ay = a.getY();
+        int by = b.getY();
+        int my = Math.min(ay, by);
+        int res;
+        if (mx < my) {
+            System.out.println("success");
+            res = mx - my;
+        } else if (mx > my) {
+            System.out.println("fail");
+            res = my - mx;
+        } else {
+            throw new IllegalArgumentException();
+        }
+        return res;
+    }
+
+//    public int testWrapper(ArrayList<Integer> b) {
+//        if (b.get(0) < 0) {
+//            throw new IllegalArgumentException();
 //        }
-//        return res;
+//        return b.size();
 //    }
 
-    public int testWrapper(ArrayList<Integer> b) {
-        if (b.get(0) < 0) {
-            throw new IllegalArgumentException();
+    public boolean testFoo(boolean b) {
+        if (b) {
+            foo(new Point(100, 100), new Point(0, 0));
+            return false;
+        } else {
+            try {
+                foo(new Point(0, 0), new Point(0, 0));
+            } catch (IllegalArgumentException e) {
+                System.err.println("asdsad");
+            }
+            return true;
         }
-        return b.size();
     }
 }
 
diff --git a/kex.ini b/kex.ini
index c92029b98..5e8b1cee2 100644
--- a/kex.ini
+++ b/kex.ini
@@ -78,7 +78,7 @@ numberOfConcreteMethods = 3
 [concolic]
 timeLimit = 120
 numberOfExecutors = 1
-searchStrategy = cgs
+searchStrategy = coverage
 
 [crash]
 timeLimit = 600
@@ -122,6 +122,8 @@ logSMTLib = false
 
 simplifyFormulae = false
 
+useADSolver = false
+
 [ksmt]
 solver = z3
 solver = cvc5