diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicAbstractor.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicAbstractor.java
index 6c55d2ff79..f731a7cd70 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicAbstractor.java
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicAbstractor.java
@@ -41,16 +41,16 @@
 /**
  * Basic implementation for the abstractor, relying on an ArgBuilder.
  */
-public final class BasicAbstractor<S extends State, A extends Action, P extends Prec> implements Abstractor<S, A, P> {
+public class BasicAbstractor<S extends State, A extends Action, P extends Prec> implements Abstractor<S, A, P> {
 
-    private final ArgBuilder<S, A, P> argBuilder;
-    private final Function<? super S, ?> projection;
-    private final Waitlist<ArgNode<S, A>> waitlist;
-    private final StopCriterion<S, A> stopCriterion;
-    private final Logger logger;
+    protected final ArgBuilder<S, A, P> argBuilder;
+    protected final Function<? super S, ?> projection;
+    protected final Waitlist<ArgNode<S, A>> waitlist;
+    protected final StopCriterion<S, A> stopCriterion;
+    protected final Logger logger;
 
-    private BasicAbstractor(final ArgBuilder<S, A, P> argBuilder, final Function<? super S, ?> projection,
-                            final Waitlist<ArgNode<S, A>> waitlist, final StopCriterion<S, A> stopCriterion, final Logger logger) {
+    protected BasicAbstractor(final ArgBuilder<S, A, P> argBuilder, final Function<? super S, ?> projection,
+                              final Waitlist<ArgNode<S, A>> waitlist, final StopCriterion<S, A> stopCriterion, final Logger logger) {
         this.argBuilder = checkNotNull(argBuilder);
         this.projection = checkNotNull(projection);
         this.waitlist = checkNotNull(waitlist);
@@ -122,7 +122,7 @@ public AbstractorResult check(final ARG<S, A> arg, final P prec) {
         }
     }
 
-    private void close(final ArgNode<S, A> node, final Collection<ArgNode<S, A>> candidates) {
+    protected void close(final ArgNode<S, A> node, final Collection<ArgNode<S, A>> candidates) {
         if (!node.isLeaf()) {
             return;
         }
@@ -139,14 +139,14 @@ public String toString() {
         return Utils.lispStringBuilder(getClass().getSimpleName()).add(waitlist).toString();
     }
 
-    public static final class Builder<S extends State, A extends Action, P extends Prec> {
-        private final ArgBuilder<S, A, P> argBuilder;
-        private Function<? super S, ?> projection;
-        private Waitlist<ArgNode<S, A>> waitlist;
-        private StopCriterion<S, A> stopCriterion;
-        private Logger logger;
+    public static class Builder<S extends State, A extends Action, P extends Prec> {
+        protected final ArgBuilder<S, A, P> argBuilder;
+        protected Function<? super S, ?> projection;
+        protected Waitlist<ArgNode<S, A>> waitlist;
+        protected StopCriterion<S, A> stopCriterion;
+        protected Logger logger;
 
-        private Builder(final ArgBuilder<S, A, P> argBuilder) {
+        protected Builder(final ArgBuilder<S, A, P> argBuilder) {
             this.argBuilder = argBuilder;
             this.projection = s -> 0;
             this.waitlist = FifoWaitlist.create();
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/SingleExprTraceRefiner.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/SingleExprTraceRefiner.java
index 3a873a48fa..8594753d9f 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/SingleExprTraceRefiner.java
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/SingleExprTraceRefiner.java
@@ -36,17 +36,17 @@
  * A Refiner implementation that can refine a single trace (of ExprStates and
  * ExprActions) using an ExprTraceChecker and a PrecRefiner.
  */
-public final class SingleExprTraceRefiner<S extends ExprState, A extends ExprAction, P extends Prec, R extends Refutation>
+public class SingleExprTraceRefiner<S extends ExprState, A extends ExprAction, P extends Prec, R extends Refutation>
         implements Refiner<S, A, P> {
-    private final ExprTraceChecker<R> exprTraceChecker;
-    private final PrecRefiner<S, A, P, R> precRefiner;
-    private final PruneStrategy pruneStrategy;
-    private final NodePruner<S, A> nodePruner;
-    private final Logger logger;
-
-    private SingleExprTraceRefiner(final ExprTraceChecker<R> exprTraceChecker,
-                                   final PrecRefiner<S, A, P, R> precRefiner,
-                                   final PruneStrategy pruneStrategy, final Logger logger) {
+    protected final ExprTraceChecker<R> exprTraceChecker;
+    protected final PrecRefiner<S, A, P, R> precRefiner;
+    protected final PruneStrategy pruneStrategy;
+    protected final NodePruner<S, A> nodePruner;
+    protected final Logger logger;
+
+    protected SingleExprTraceRefiner(final ExprTraceChecker<R> exprTraceChecker,
+                                     final PrecRefiner<S, A, P, R> precRefiner,
+                                     final PruneStrategy pruneStrategy, final Logger logger) {
         this.exprTraceChecker = checkNotNull(exprTraceChecker);
         this.precRefiner = checkNotNull(precRefiner);
         this.pruneStrategy = checkNotNull(pruneStrategy);
@@ -54,10 +54,10 @@ private SingleExprTraceRefiner(final ExprTraceChecker<R> exprTraceChecker,
         this.logger = checkNotNull(logger);
     }
 
-    private SingleExprTraceRefiner(final ExprTraceChecker<R> exprTraceChecker,
-                                   final PrecRefiner<S, A, P, R> precRefiner,
-                                   final PruneStrategy pruneStrategy, final Logger logger,
-                                   final NodePruner<S, A> nodePruner) {
+    protected SingleExprTraceRefiner(final ExprTraceChecker<R> exprTraceChecker,
+                                     final PrecRefiner<S, A, P, R> precRefiner,
+                                     final PruneStrategy pruneStrategy, final Logger logger,
+                                     final NodePruner<S, A> nodePruner) {
         this.exprTraceChecker = checkNotNull(exprTraceChecker);
         this.precRefiner = checkNotNull(precRefiner);
         this.pruneStrategy = checkNotNull(pruneStrategy);
diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/Utils.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/Utils.kt
new file mode 100644
index 0000000000..b16cacd6c6
--- /dev/null
+++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/Utils.kt
@@ -0,0 +1,75 @@
+/*
+ *  Copyright 2023 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.xcfa.analysis
+
+import hu.bme.mit.theta.analysis.expl.ExplState
+import hu.bme.mit.theta.analysis.expr.ExprState
+import hu.bme.mit.theta.analysis.pred.PredState
+import hu.bme.mit.theta.core.decl.Decl
+import hu.bme.mit.theta.core.decl.VarDecl
+import hu.bme.mit.theta.core.model.ImmutableValuation
+import hu.bme.mit.theta.core.model.Valuation
+import hu.bme.mit.theta.xcfa.getFlatLabels
+import hu.bme.mit.theta.xcfa.model.InvokeLabel
+import hu.bme.mit.theta.xcfa.model.XCFA
+import hu.bme.mit.theta.xcfa.passes.changeVars
+import kotlin.reflect.KProperty
+
+fun <K, V> Map<K, V>.reverseMapping() = this.entries.associate { it.value to it.key }
+
+fun Valuation.changeVars(varLut: Map<out Decl<*>, VarDecl<*>>): Valuation {
+    val builder = ImmutableValuation.builder()
+    for (decl in this.decls) {
+        builder.put(decl.changeVars(varLut), this.eval(decl).get())
+    }
+    return builder.build()
+}
+
+internal fun <S : ExprState> XcfaState<S>.withGeneralizedVars(): S {
+    val varLookup = processes.mapNotNull { (_, process) -> process.varLookup.peek()?.reverseMapping() }
+        .reduceOrNull(Map<VarDecl<*>, VarDecl<*>>::plus) ?: mapOf()
+    return if (sGlobal.isBottom) sGlobal
+    else when (sGlobal) {
+        is ExplState -> ExplState.of(sGlobal.getVal().changeVars(varLookup))
+        is PredState -> PredState.of(sGlobal.preds.map { p -> p.changeVars(varLookup) })
+        else -> throw NotImplementedError(
+            "Generalizing variable instances is not implemented for data states that are not explicit or predicate.")
+    } as S
+}
+
+class LazyDelegate<T, P : Any>(val getProperty: T.() -> P) {
+
+    private var calculated = false
+    private lateinit var property: P
+
+    operator fun getValue(thisRef: T, property: KProperty<*>): P {
+        return if (calculated) this.property
+        else thisRef.getProperty().also {
+            this.property = it
+            this.calculated = true
+        }
+    }
+}
+
+val XCFA.isInlined: Boolean by LazyDelegate {
+    !this.procedures.any { p ->
+        p.edges.any { e ->
+            e.getFlatLabels().any { l ->
+                l is InvokeLabel && this.procedures.any { it.name == l.name }
+            }
+        }
+    }
+}
\ No newline at end of file
diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAbstractor.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAbstractor.kt
new file mode 100644
index 0000000000..3d0f25823b
--- /dev/null
+++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAbstractor.kt
@@ -0,0 +1,137 @@
+/*
+ *  Copyright 2023 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.xcfa.analysis
+
+import com.google.common.base.Preconditions
+import hu.bme.mit.theta.analysis.Action
+import hu.bme.mit.theta.analysis.Prec
+import hu.bme.mit.theta.analysis.State
+import hu.bme.mit.theta.analysis.algorithm.ARG
+import hu.bme.mit.theta.analysis.algorithm.ArgBuilder
+import hu.bme.mit.theta.analysis.algorithm.ArgNode
+import hu.bme.mit.theta.analysis.algorithm.cegar.AbstractorResult
+import hu.bme.mit.theta.analysis.algorithm.cegar.BasicAbstractor
+import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterion
+import hu.bme.mit.theta.analysis.reachedset.Partition
+import hu.bme.mit.theta.analysis.waitlist.Waitlist
+import hu.bme.mit.theta.common.logging.Logger
+import java.util.function.Function
+
+class XcfaAbstractor<S : State, A : Action, P : Prec>(
+    argBuilder: ArgBuilder<S, A, P>,
+    projection: Function<in S?, *>?,
+    waitlist: Waitlist<ArgNode<S, A>>,
+    stopCriterion: StopCriterion<S, A>,
+    logger: Logger,
+) : BasicAbstractor<S, A, P>(argBuilder, projection, waitlist, stopCriterion, logger) {
+
+    override fun check(arg: ARG<S, A>, prec: P): AbstractorResult {
+        logger.write(Logger.Level.DETAIL, "|  |  Precision: %s%n", prec)
+
+        if (!arg.isInitialized) {
+            logger.write(Logger.Level.SUBSTEP, "|  |  (Re)initializing ARG...")
+            argBuilder.init(arg, prec)
+            logger.write(Logger.Level.SUBSTEP, "done%n")
+        }
+
+        assert(arg.isInitialized)
+
+        logger.write(
+            Logger.Level.INFO, "|  |  Starting ARG: %d nodes, %d incomplete, %d unsafe%n", arg.nodes.count(),
+            arg.incompleteNodes.count(), arg.unsafeNodes.count()
+        )
+        logger.write(Logger.Level.SUBSTEP, "|  |  Building ARG...")
+
+        val reachedSet: Partition<ArgNode<S, A>, *> = Partition.of { n: ArgNode<S, A> ->
+            projection.apply(n.state)
+        }
+        waitlist.clear()
+
+        reachedSet.addAll(arg.nodes)
+        waitlist.addAll(arg.incompleteNodes)
+
+        if (!stopCriterion.canStop(arg)) {
+            while (!waitlist.isEmpty) {
+                val node = waitlist.remove()
+                var newNodes: Collection<ArgNode<S, A>>? = emptyList()
+                if ((node.state as XcfaState<*>).xcfa!!.isInlined) {
+                    close(node, reachedSet[node])
+                } else {
+                    val expandProcedureCall = (node.state as XcfaState<*>) in (prec as XcfaPrec<P>).noPop
+                    closePop(node, reachedSet[node], !expandProcedureCall)
+                }
+                if (!node.isSubsumed && !node.isTarget) {
+                    newNodes = argBuilder.expand(node, prec)
+                    reachedSet.addAll(newNodes)
+                    waitlist.addAll(newNodes)
+                }
+                if (stopCriterion.canStop(arg, newNodes)) break
+            }
+        }
+
+        logger.write(Logger.Level.SUBSTEP, "done%n")
+        logger.write(
+            Logger.Level.INFO, "|  |  Finished ARG: %d nodes, %d incomplete, %d unsafe%n", arg.nodes.count(),
+            arg.incompleteNodes.count(), arg.unsafeNodes.count()
+        )
+
+        waitlist.clear() // Optimization
+
+        return if (arg.isSafe) {
+            Preconditions.checkState(arg.isComplete, "Returning incomplete ARG as safe")
+            AbstractorResult.safe()
+        } else {
+            AbstractorResult.unsafe()
+        }
+    }
+
+    fun closePop(node: ArgNode<S, A>, candidates: Collection<ArgNode<S, A>>, popCovered: Boolean) {
+        if (!node.isLeaf) {
+            return
+        }
+        for (candidate in candidates) {
+            if (candidate.mayCover(node)) {
+                var onlyStackCovers = false
+                (node.state as XcfaState<*>).processes.forEach { (pid: Int, proc: XcfaProcessState) ->
+                    if (proc != (candidate.state as XcfaState<*>).processes[pid]) {
+                        if (popCovered) proc.popped = proc.locs.pop()
+                        onlyStackCovers = true
+                    }
+                }
+                if (!onlyStackCovers) {
+                    node.cover(candidate)
+                }
+                return
+            }
+        }
+    }
+
+    companion object {
+
+        fun <S : State, A : Action, P : Prec> builder(
+            argBuilder: ArgBuilder<S, A, P>): BasicAbstractor.Builder<S, A, P> {
+            return Builder(argBuilder)
+        }
+    }
+
+    class Builder<S : State, A : Action, P : Prec>(argBuilder: ArgBuilder<S, A, P>)
+        : BasicAbstractor.Builder<S, A, P>(argBuilder) {
+
+        override fun build(): BasicAbstractor<S, A, P> {
+            return XcfaAbstractor(argBuilder, projection, waitlist, stopCriterion, logger)
+        }
+    }
+}
diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt
index 2fffa458cb..a662316543 100644
--- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt
+++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt
@@ -20,7 +20,6 @@ import hu.bme.mit.theta.analysis.*
 import hu.bme.mit.theta.analysis.algorithm.ArgBuilder
 import hu.bme.mit.theta.analysis.algorithm.ArgNode
 import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor
-import hu.bme.mit.theta.analysis.algorithm.cegar.BasicAbstractor
 import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterion
 import hu.bme.mit.theta.analysis.expl.ExplInitFunc
 import hu.bme.mit.theta.analysis.expl.ExplPrec
@@ -174,6 +173,20 @@ fun <S : ExprState> getPartialOrder(partialOrd: PartialOrd<S>) =
             s1.sGlobal, s2.sGlobal)
     }
 
+private fun <S : ExprState> stackIsLeq(s1: XcfaState<S>, s2: XcfaState<S>) = s2.processes.keys.all { pid ->
+    s1.processes[pid]?.let { ps1 ->
+        val ps2 = s2.processes.getValue(pid)
+        ps1.locs.peek() == ps2.locs.peek() && ps1.paramsInitialized && ps2.paramsInitialized
+    } ?: false
+}
+
+fun <S : ExprState> getStackPartialOrder(partialOrd: PartialOrd<S>) =
+    PartialOrd<XcfaState<S>> { s1, s2 ->
+        s1.processes.size == s2.processes.size && stackIsLeq(s1,
+            s2) && s1.bottom == s2.bottom && s1.mutexes == s2.mutexes
+            && partialOrd.isLeq(s1.withGeneralizedVars(), s2.withGeneralizedVars())
+    }
+
 private fun <S : XcfaState<out ExprState>, P : XcfaPrec<out Prec>> getXcfaArgBuilder(
     analysis: Analysis<S, XcfaAction, P>,
     lts: LTS<XcfaState<out ExprState>, XcfaAction>,
@@ -193,10 +206,13 @@ fun <S : XcfaState<out ExprState>, P : XcfaPrec<out Prec>> getXcfaAbstractor(
     lts: LTS<XcfaState<out ExprState>, XcfaAction>,
     errorDetection: ErrorDetection
 ): Abstractor<out XcfaState<out ExprState>, XcfaAction, out XcfaPrec<out Prec>> =
-    BasicAbstractor.builder(getXcfaArgBuilder(analysis, lts, errorDetection))
+    XcfaAbstractor.builder(getXcfaArgBuilder(analysis, lts, errorDetection))
         .waitlist(waitlist as Waitlist<ArgNode<S, XcfaAction>>) // TODO: can we do this nicely?
         .stopCriterion(stopCriterion as StopCriterion<S, XcfaAction>).logger(logger)
-        .projection { it.processes }
+        .projection {
+            if (it.xcfa!!.isInlined) it.processes
+            else it.processes.map { (_, p) -> p.locs.peek() }
+        }
         .build() // TODO: can we do this nicely?
 
 /// EXPL
diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaPrec.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaPrec.kt
index c912925c73..b267bf5f51 100644
--- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaPrec.kt
+++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaPrec.kt
@@ -19,7 +19,7 @@ package hu.bme.mit.theta.xcfa.analysis
 import hu.bme.mit.theta.analysis.Prec
 import hu.bme.mit.theta.core.decl.VarDecl
 
-data class XcfaPrec<P : Prec>(val p: P) : Prec {
+data class XcfaPrec<P : Prec>(val p: P, val noPop: MutableList<XcfaState<*>> = mutableListOf()) : Prec {
 
     override fun getUsedVars(): Collection<VarDecl<*>> {
         return p.usedVars
diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaPrecRefiner.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaPrecRefiner.kt
index 48a4df6a05..ea5eea4307 100644
--- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaPrecRefiner.kt
+++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaPrecRefiner.kt
@@ -39,6 +39,7 @@ class XcfaPrecRefiner<S : ExprState, P : Prec, R : Refutation>(refToPrec: Refuta
         Preconditions.checkNotNull(trace)
         Preconditions.checkNotNull<Any>(prec)
         Preconditions.checkNotNull<R>(refutation)
+        val checkForPop = !(trace.states.first() as XcfaState<*>).xcfa!!.isInlined
         var runningPrec: P = prec.p
         for (i in trace.states.indices) {
             val reverseLookup = trace.states[i].processes.values.map {
@@ -51,8 +52,8 @@ class XcfaPrecRefiner<S : ExprState, P : Prec, R : Refutation>(refToPrec: Refuta
             val additionalLookup = if (i > 0) getTempLookup(
                 trace.actions[i - 1].edge.label).entries.associateBy(
                 { it.value }) { it.key } else emptyMap()
-            val precFromRef = refToPrec.toPrec(refutation, i)
-                .changeVars(reverseLookup + additionalLookup)
+            val varLookup = if (checkForPop) additionalLookup else (reverseLookup + additionalLookup)
+            val precFromRef = refToPrec.toPrec(refutation, i).changeVars(varLookup)
             runningPrec = refToPrec.join(runningPrec, precFromRef)
         }
         return prec.refine(runningPrec)
diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaSingeExprTraceRefiner.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaSingeExprTraceRefiner.kt
new file mode 100644
index 0000000000..432e88a0e9
--- /dev/null
+++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaSingeExprTraceRefiner.kt
@@ -0,0 +1,114 @@
+/*
+ *  Copyright 2023 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.xcfa.analysis
+
+import com.google.common.base.Preconditions
+import hu.bme.mit.theta.analysis.Prec
+import hu.bme.mit.theta.analysis.Trace
+import hu.bme.mit.theta.analysis.algorithm.ARG
+import hu.bme.mit.theta.analysis.algorithm.cegar.RefinerResult
+import hu.bme.mit.theta.analysis.expr.ExprAction
+import hu.bme.mit.theta.analysis.expr.ExprState
+import hu.bme.mit.theta.analysis.expr.refinement.*
+import hu.bme.mit.theta.common.logging.Logger
+import java.util.LinkedList
+
+
+class XcfaSingleExprTraceRefiner<S : ExprState, A : ExprAction, P : Prec, R : Refutation> :
+    SingleExprTraceRefiner<S, A, P, R> {
+
+    private constructor(
+        exprTraceChecker: ExprTraceChecker<R>,
+        precRefiner: PrecRefiner<S, A, P, R>,
+        pruneStrategy: PruneStrategy,
+        logger: Logger
+    ) : super(exprTraceChecker, precRefiner, pruneStrategy, logger)
+
+    private constructor(
+        exprTraceChecker: ExprTraceChecker<R>,
+        precRefiner: PrecRefiner<S, A, P, R>,
+        pruneStrategy: PruneStrategy,
+        logger: Logger,
+        nodePruner: NodePruner<S, A>
+    ) : super(exprTraceChecker, precRefiner, pruneStrategy, logger, nodePruner)
+
+    private fun findPoppedState(trace: Trace<S, A>): Pair<Int, XcfaState<S>>? {
+        trace.states.forEachIndexed { i, s ->
+            val state = s as XcfaState<S>
+            state.processes.entries.find { (_, processState) -> processState.popped != null }
+                ?.let { (pid, processState) ->
+                    val stackBeforePop = LinkedList(processState.locs)
+                    stackBeforePop.push(processState.popped)
+                    val processesBeforePop = state.processes.toMutableMap()
+                    processesBeforePop[pid] = processState.copy(locs = stackBeforePop)
+                    val stateBeforePop = state.copy(processes = processesBeforePop)
+                    return Pair(i, stateBeforePop)
+                }
+        }
+        return null
+    }
+
+    override fun refine(arg: ARG<S, A>, prec: P?): RefinerResult<S, A, P?> {
+        Preconditions.checkNotNull(arg)
+        Preconditions.checkNotNull<P>(prec)
+        assert(!arg.isSafe) { "ARG must be unsafe" }
+
+        val optionalNewCex = arg.cexs.findFirst()
+        val cexToConcretize = optionalNewCex.get()
+        val traceToConcretize = cexToConcretize.toTrace()
+
+        val refinerResult = super.refine(arg, prec)
+        val checkForPop = !(traceToConcretize.states.first() as XcfaState<*>).xcfa!!.isInlined
+
+        return if (checkForPop && refinerResult.isUnsafe) findPoppedState(traceToConcretize)?.let { (i, state) ->
+            when (pruneStrategy) {
+                PruneStrategy.LAZY -> {
+                    logger.write(Logger.Level.SUBSTEP, "|  |  Pruning from index %d...", i)
+                    val nodeToPrune = cexToConcretize.node(i)
+                    nodePruner.prune(arg, nodeToPrune)
+                }
+
+                PruneStrategy.FULL -> {
+                    logger.write(Logger.Level.SUBSTEP, "|  |  Pruning whole ARG", i)
+                    arg.pruneAll()
+                }
+
+                else -> throw UnsupportedOperationException("Unsupported pruning strategy")
+            }
+
+            val refinedPrec = (prec as XcfaPrec<P>).copy()
+            refinedPrec.noPop.add(state)
+            RefinerResult.spurious(refinedPrec as P?)
+        } ?: refinerResult else refinerResult
+    }
+
+    companion object {
+
+        fun <S : ExprState, A : ExprAction, P : Prec, R : Refutation> create(
+            exprTraceChecker: ExprTraceChecker<R>, precRefiner: PrecRefiner<S, A, P, R>,
+            pruneStrategy: PruneStrategy, logger: Logger
+        ): XcfaSingleExprTraceRefiner<S, A, P, R> {
+            return XcfaSingleExprTraceRefiner(exprTraceChecker, precRefiner, pruneStrategy, logger)
+        }
+
+        fun <S : ExprState, A : ExprAction, P : Prec, R : Refutation> create(
+            exprTraceChecker: ExprTraceChecker<R>, precRefiner: PrecRefiner<S, A, P, R>,
+            pruneStrategy: PruneStrategy, logger: Logger, nodePruner: NodePruner<S, A>
+        ): XcfaSingleExprTraceRefiner<S, A, P, R> {
+            return XcfaSingleExprTraceRefiner(exprTraceChecker, precRefiner, pruneStrategy, logger, nodePruner)
+        }
+    }
+}
diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaState.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaState.kt
index 3fd40864b9..7cf2a87b26 100644
--- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaState.kt
+++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaState.kt
@@ -235,6 +235,8 @@ data class XcfaProcessState(val locs: LinkedList<XcfaLocation>, val varLookup: L
     val paramStmts: LinkedList<Pair<XcfaLabel, XcfaLabel>> = LinkedList(listOf(Pair(NopLabel, NopLabel))),
     val paramsInitialized: Boolean = false, val prefix: String = "") {
 
+    internal var popped: XcfaLocation? = null // stores if the stack was popped due to abstract stack covering
+
     fun withNewLoc(l: XcfaLocation): XcfaProcessState {
         val deque: LinkedList<XcfaLocation> = LinkedList(locs)
         deque.pop()
diff --git a/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaExplAnalysisTest.kt b/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaExplAnalysisTest.kt
index 290a49d345..6b89916d1e 100644
--- a/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaExplAnalysisTest.kt
+++ b/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaExplAnalysisTest.kt
@@ -89,7 +89,7 @@ class XcfaExplAnalysisTest {
         val precRefiner = XcfaPrecRefiner<XcfaState<ExplState>, ExplPrec, ItpRefutation>(ItpRefToExplPrec())
 
         val refiner =
-            SingleExprTraceRefiner.create(
+            XcfaSingleExprTraceRefiner.create(
                 ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(),
                     Z3SolverFactory.getInstance().createItpSolver()),
                 precRefiner, PruneStrategy.FULL,
@@ -133,7 +133,7 @@ class XcfaExplAnalysisTest {
         val precRefiner = XcfaPrecRefiner<XcfaState<ExplState>, ExplPrec, ItpRefutation>(ItpRefToExplPrec())
 
         val refiner =
-            SingleExprTraceRefiner.create(
+            XcfaSingleExprTraceRefiner.create(
                 ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(),
                     Z3SolverFactory.getInstance().createItpSolver()),
                 precRefiner, PruneStrategy.FULL,
@@ -177,7 +177,7 @@ class XcfaExplAnalysisTest {
         val precRefiner = XcfaPrecRefiner<XcfaState<ExplState>, ExplPrec, ItpRefutation>(ItpRefToExplPrec())
 
         val refiner =
-            SingleExprTraceRefiner.create(
+            XcfaSingleExprTraceRefiner.create(
                 ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(),
                     Z3SolverFactory.getInstance().createItpSolver()),
                 precRefiner, PruneStrategy.FULL,
@@ -222,7 +222,7 @@ class XcfaExplAnalysisTest {
         val atomicNodePruner = AtomicNodePruner<XcfaState<ExplState>, XcfaAction>()
 
         val refiner =
-            SingleExprTraceRefiner.create(
+            XcfaSingleExprTraceRefiner.create(
                 ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(),
                     Z3SolverFactory.getInstance().createItpSolver()),
                 precRefiner, PruneStrategy.FULL, NullLogger.getInstance(),
@@ -266,7 +266,7 @@ class XcfaExplAnalysisTest {
         val precRefiner = XcfaPrecRefiner<ExplState, ExplPrec, ItpRefutation>(ItpRefToExplPrec())
 
         val refiner =
-            SingleExprTraceRefiner.create(
+            XcfaSingleExprTraceRefiner.create(
                 ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(),
                     Z3SolverFactory.getInstance().createItpSolver()),
                 precRefiner, PruneStrategy.FULL,
diff --git a/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaPredAnalysisTest.kt b/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaPredAnalysisTest.kt
index 67cd2afe5a..f18d9f3cba 100644
--- a/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaPredAnalysisTest.kt
+++ b/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaPredAnalysisTest.kt
@@ -91,7 +91,7 @@ class XcfaPredAnalysisTest {
             ItpRefToPredPrec(ExprSplitters.whole()))
 
         val refiner =
-            SingleExprTraceRefiner.create(
+            XcfaSingleExprTraceRefiner.create(
                 ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(),
                     Z3SolverFactory.getInstance().createItpSolver()),
                 precRefiner, PruneStrategy.FULL,
@@ -137,7 +137,7 @@ class XcfaPredAnalysisTest {
             ItpRefToPredPrec(ExprSplitters.whole()))
 
         val refiner =
-            SingleExprTraceRefiner.create(
+            XcfaSingleExprTraceRefiner.create(
                 ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(),
                     Z3SolverFactory.getInstance().createItpSolver()),
                 precRefiner, PruneStrategy.FULL,
@@ -183,7 +183,7 @@ class XcfaPredAnalysisTest {
             ItpRefToPredPrec(ExprSplitters.whole()))
 
         val refiner =
-            SingleExprTraceRefiner.create(
+            XcfaSingleExprTraceRefiner.create(
                 ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(),
                     Z3SolverFactory.getInstance().createItpSolver()),
                 precRefiner, PruneStrategy.FULL,
@@ -229,7 +229,7 @@ class XcfaPredAnalysisTest {
         val atomicNodePruner = AtomicNodePruner<XcfaState<PredState>, XcfaAction>()
 
         val refiner =
-            SingleExprTraceRefiner.create(
+            XcfaSingleExprTraceRefiner.create(
                 ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(),
                     Z3SolverFactory.getInstance().createItpSolver()),
                 precRefiner, PruneStrategy.FULL, NullLogger.getInstance(),
@@ -274,7 +274,7 @@ class XcfaPredAnalysisTest {
         val precRefiner = XcfaPrecRefiner<PredState, PredPrec, ItpRefutation>(ItpRefToPredPrec(ExprSplitters.whole()))
 
         val refiner =
-            SingleExprTraceRefiner.create(
+            XcfaSingleExprTraceRefiner.create(
                 ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(),
                     Z3SolverFactory.getInstance().createItpSolver()),
                 precRefiner, PruneStrategy.FULL,
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt
index 43b75bfd49..90efc96b98 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt
@@ -99,7 +99,7 @@ enum class Domain(
     ) -> Abstractor<out ExprState, out ExprAction, out Prec>,
     val itpPrecRefiner: (exprSplitter: ExprSplitter) -> PrecRefiner<out ExprState, out ExprAction, out Prec, out Refutation>,
     val initPrec: (XCFA, InitPrec) -> XcfaPrec<*>,
-    val partialOrd: (Solver) -> PartialOrd<out XcfaState<out ExprState>>,
+    val partialOrd: (Solver) -> PartialOrd<out ExprState>,
     val nodePruner: NodePruner<out ExprState, out ExprAction>,
     val stateType: Type
 ) {
@@ -113,7 +113,7 @@ enum class Domain(
             XcfaPrecRefiner<ExplState, ExplPrec, ItpRefutation>(ItpRefToExplPrec())
         },
         initPrec = { x, ip -> ip.explPrec(x) },
-        partialOrd = { getPartialOrder<ExplState> { s1, s2 -> s1.isLeq(s2) } },
+        partialOrd = { PartialOrd<ExplState> { s1, s2 -> s1.isLeq(s2) } },
         nodePruner = AtomicNodePruner<XcfaState<ExplState>, XcfaAction>(),
         stateType = TypeToken.get(ExplState::class.java).type
     ),
@@ -126,7 +126,7 @@ enum class Domain(
             XcfaPrecRefiner<PredState, PredPrec, ItpRefutation>(ItpRefToPredPrec(a))
         },
         initPrec = { x, ip -> ip.predPrec(x) },
-        partialOrd = { solver -> getPartialOrder<PredState>(PredOrd.create(solver)) },
+        partialOrd = { solver -> PredOrd.create(solver) },
         nodePruner = AtomicNodePruner<XcfaState<PredState>, XcfaAction>(),
         stateType = TypeToken.get(PredState::class.java).type
     ),
@@ -139,7 +139,7 @@ enum class Domain(
             XcfaPrecRefiner<PredState, PredPrec, ItpRefutation>(ItpRefToPredPrec(a))
         },
         initPrec = { x, ip -> ip.predPrec(x) },
-        partialOrd = { solver -> getPartialOrder<PredState>(PredOrd.create(solver)) },
+        partialOrd = { solver -> PredOrd.create(solver) },
         nodePruner = AtomicNodePruner<XcfaState<PredState>, XcfaAction>(),
         stateType = TypeToken.get(PredState::class.java).type
     ),
@@ -152,7 +152,7 @@ enum class Domain(
             XcfaPrecRefiner<PredState, PredPrec, ItpRefutation>(ItpRefToPredPrec(a))
         },
         initPrec = { x, ip -> ip.predPrec(x) },
-        partialOrd = { solver -> getPartialOrder<PredState>(PredOrd.create(solver)) },
+        partialOrd = { solver -> PredOrd.create(solver) },
         nodePruner = AtomicNodePruner<XcfaState<PredState>, XcfaAction>(),
         stateType = TypeToken.get(PredState::class.java).type
     ),
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt
index 936912b3ea..a6867a7e4f 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt
@@ -43,9 +43,7 @@ import hu.bme.mit.theta.core.decl.Decl
 import hu.bme.mit.theta.core.type.Type
 import hu.bme.mit.theta.frontend.ParseContext
 import hu.bme.mit.theta.solver.SolverFactory
-import hu.bme.mit.theta.xcfa.analysis.ErrorDetection
-import hu.bme.mit.theta.xcfa.analysis.XcfaAction
-import hu.bme.mit.theta.xcfa.analysis.XcfaState
+import hu.bme.mit.theta.xcfa.analysis.*
 import hu.bme.mit.theta.xcfa.analysis.por.XcfaDporLts
 import hu.bme.mit.theta.xcfa.model.XCFA
 import java.io.BufferedReader
@@ -122,8 +120,10 @@ data class XcfaCegarConfig(
         }
 
         val abstractionSolverInstance = abstractionSolverFactory.createSolver()
-        val corePartialOrd: PartialOrd<out XcfaState<out ExprState>> = domain.partialOrd(
-            abstractionSolverInstance)
+        val globalStatePartialOrd: PartialOrd<out ExprState> = domain.partialOrd(abstractionSolverInstance)
+        val corePartialOrd: PartialOrd<out XcfaState<out ExprState>> =
+            if (xcfa.isInlined) getPartialOrder(globalStatePartialOrd)
+            else getStackPartialOrder(globalStatePartialOrd)
         val abstractor: Abstractor<ExprState, ExprAction, Prec> = domain.abstractor(
             xcfa,
             abstractionSolverInstance,
@@ -156,10 +156,10 @@ data class XcfaCegarConfig(
                     MultiExprTraceRefiner.create(ref, precRefiner, pruneStrategy, logger)
             else
                 if (porLevel == POR.AASPOR)
-                    SingleExprTraceRefiner.create(ref, precRefiner, pruneStrategy, logger,
+                    XcfaSingleExprTraceRefiner.create(ref, precRefiner, pruneStrategy, logger,
                         atomicNodePruner)
                 else
-                    SingleExprTraceRefiner.create(ref, precRefiner, pruneStrategy, logger)
+                    XcfaSingleExprTraceRefiner.create(ref, precRefiner, pruneStrategy, logger)
 
         val cegarChecker = if (porLevel == POR.AASPOR)
             CegarChecker.create(
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex24.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex24.kt
index f7285486ed..5eb22a47e3 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex24.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex24.kt
@@ -21,6 +21,7 @@ import hu.bme.mit.theta.common.logging.Logger
 import hu.bme.mit.theta.frontend.ParseContext
 import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.ArithmeticTrait
 import hu.bme.mit.theta.xcfa.analysis.ErrorDetection
+import hu.bme.mit.theta.xcfa.analysis.isInlined
 import hu.bme.mit.theta.xcfa.cli.*
 import hu.bme.mit.theta.xcfa.model.XCFA
 
@@ -61,6 +62,9 @@ fun complexPortfolio24(
         timeoutMs = 0
     )
 
+    if (!xcfaTyped.isInlined) {
+        baseConfig = baseConfig.copy(search = Search.BFS, pruneStrategy = PruneStrategy.LAZY)
+    }
     if (traitsTyped.multithreaded) {
         baseConfig = baseConfig.copy(search = Search.DFS, porLevel = POR.AASPOR, pruneStrategy = PruneStrategy.FULL,
             coi = ConeOfInfluenceMode.COI)