diff --git a/build.gradle.kts b/build.gradle.kts
index b76fd9f7ff..06036a38d7 100644
--- a/build.gradle.kts
+++ b/build.gradle.kts
@@ -29,7 +29,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "6.6.3"
+    version = "6.6.4"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }
diff --git a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java
index 7427f38b20..37c30260ea 100644
--- a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java
+++ b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java
@@ -15,16 +15,19 @@
  */
 package hu.bme.mit.theta.cfa.analysis.config;
 
+import static com.google.common.base.Preconditions.checkState;
+import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True;
+
 import hu.bme.mit.theta.analysis.*;
+import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
 import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder;
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgNodeComparators;
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgNodeComparators.ArgNodeComparator;
-import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
-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.CegarChecker;
-import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner;
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgAbstractor;
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgCegarChecker;
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgRefiner;
+import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor;
 import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterion;
 import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterions;
 import hu.bme.mit.theta.analysis.expl.*;
@@ -52,14 +55,10 @@
 import hu.bme.mit.theta.common.logging.NullLogger;
 import hu.bme.mit.theta.solver.Solver;
 import hu.bme.mit.theta.solver.SolverFactory;
-
 import java.util.Set;
 import java.util.function.Function;
 import java.util.function.Predicate;
 
-import static com.google.common.base.Preconditions.checkState;
-import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True;
-
 public class CfaConfigBuilder {
 
     private final SolverFactory abstractionSolverFactory;
@@ -75,16 +74,19 @@ public class CfaConfigBuilder {
     private InitPrec initPrec = InitPrec.EMPTY;
     private PruneStrategy pruneStrategy = PruneStrategy.LAZY;
 
-    public CfaConfigBuilder(final Domain domain, final Refinement refinement,
-                            final SolverFactory solverFactory) {
+    public CfaConfigBuilder(
+            final Domain domain, final Refinement refinement, final SolverFactory solverFactory) {
         this.domain = domain;
         this.refinement = refinement;
         this.abstractionSolverFactory = solverFactory;
         this.refinementSolverFactory = solverFactory;
     }
 
-    public CfaConfigBuilder(final Domain domain, final Refinement refinement,
-                            final SolverFactory abstractionSolverFactory, final SolverFactory refinementSolverFactory) {
+    public CfaConfigBuilder(
+            final Domain domain,
+            final Refinement refinement,
+            final SolverFactory abstractionSolverFactory,
+            final SolverFactory refinementSolverFactory) {
         this.domain = domain;
         this.refinement = refinement;
         this.abstractionSolverFactory = abstractionSolverFactory;
@@ -131,12 +133,13 @@ public CfaConfigBuilder pruneStrategy(final PruneStrategy pruneStrategy) {
         return this;
     }
 
-    public CfaConfig<? extends State, ? extends Action, ? extends Prec> build(final CFA cfa,
-                                                                              final CFA.Loc errLoc) {
+    public CfaConfig<? extends State, ? extends Action, ? extends Prec> build(
+            final CFA cfa, final CFA.Loc errLoc) {
         if (domain == Domain.EXPL) {
             return (new ExplStrategy(cfa)).buildConfig(errLoc);
         }
-        if (domain == Domain.PRED_BOOL || domain == Domain.PRED_CART
+        if (domain == Domain.PRED_BOOL
+                || domain == Domain.PRED_CART
                 || domain == Domain.PRED_SPLIT) {
             return (new PredStrategy(cfa)).buildConfig(errLoc);
         }
@@ -166,18 +169,53 @@ public enum Domain {
     public enum Refinement {
         FW_BIN_ITP {
             @Override
-            public <S extends ExprState, P extends Prec> Refiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(BuilderStrategy<S, P> builderStrategy) {
-                return SingleExprTraceRefiner.create(ExprTraceFwBinItpChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createItpSolver()), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger());
+            public <S extends ExprState, P extends Prec>
+                    ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
+                            BuilderStrategy<S, P> builderStrategy) {
+                return SingleExprTraceRefiner.create(
+                        ExprTraceFwBinItpChecker.create(
+                                True(),
+                                True(),
+                                builderStrategy.getRefinementSolverFactory().createItpSolver()),
+                        builderStrategy
+                                .getPrecGranularity()
+                                .createRefiner(builderStrategy.getItpRefToPrec()),
+                        builderStrategy.getPruneStrategy(),
+                        builderStrategy.getLogger());
             }
-        }, BW_BIN_ITP {
+        },
+        BW_BIN_ITP {
             @Override
-            public <S extends ExprState, P extends Prec> Refiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(BuilderStrategy<S, P> builderStrategy) {
-                return SingleExprTraceRefiner.create(ExprTraceBwBinItpChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createItpSolver()), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger());
+            public <S extends ExprState, P extends Prec>
+                    ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
+                            BuilderStrategy<S, P> builderStrategy) {
+                return SingleExprTraceRefiner.create(
+                        ExprTraceBwBinItpChecker.create(
+                                True(),
+                                True(),
+                                builderStrategy.getRefinementSolverFactory().createItpSolver()),
+                        builderStrategy
+                                .getPrecGranularity()
+                                .createRefiner(builderStrategy.getItpRefToPrec()),
+                        builderStrategy.getPruneStrategy(),
+                        builderStrategy.getLogger());
             }
-        }, SEQ_ITP {
+        },
+        SEQ_ITP {
             @Override
-            public <S extends ExprState, P extends Prec> Refiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(BuilderStrategy<S, P> builderStrategy) {
-                return SingleExprTraceRefiner.create(ExprTraceSeqItpChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createItpSolver()), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger());
+            public <S extends ExprState, P extends Prec>
+                    ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
+                            BuilderStrategy<S, P> builderStrategy) {
+                return SingleExprTraceRefiner.create(
+                        ExprTraceSeqItpChecker.create(
+                                True(),
+                                True(),
+                                builderStrategy.getRefinementSolverFactory().createItpSolver()),
+                        builderStrategy
+                                .getPrecGranularity()
+                                .createRefiner(builderStrategy.getItpRefToPrec()),
+                        builderStrategy.getPruneStrategy(),
+                        builderStrategy.getLogger());
             }
         },
         MULTI_SEQ {
@@ -187,60 +225,229 @@ public <S extends ExprState> StopCriterion<S, CfaAction> getStopCriterion() {
             }
 
             @Override
-            public <S extends ExprState, P extends Prec> Refiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(BuilderStrategy<S, P> builderStrategy) {
-                return MultiExprTraceRefiner.create(ExprTraceSeqItpChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createItpSolver()), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger());
+            public <S extends ExprState, P extends Prec>
+                    ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
+                            BuilderStrategy<S, P> builderStrategy) {
+                return MultiExprTraceRefiner.create(
+                        ExprTraceSeqItpChecker.create(
+                                True(),
+                                True(),
+                                builderStrategy.getRefinementSolverFactory().createItpSolver()),
+                        builderStrategy
+                                .getPrecGranularity()
+                                .createRefiner(builderStrategy.getItpRefToPrec()),
+                        builderStrategy.getPruneStrategy(),
+                        builderStrategy.getLogger());
             }
         },
         UNSAT_CORE {
             @Override
-            public <S extends ExprState, P extends Prec> Refiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(BuilderStrategy<S, P> builderStrategy) {
-                return SingleExprTraceRefiner.create(ExprTraceUnsatCoreChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getVarsRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger());
+            public <S extends ExprState, P extends Prec>
+                    ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
+                            BuilderStrategy<S, P> builderStrategy) {
+                return SingleExprTraceRefiner.create(
+                        ExprTraceUnsatCoreChecker.create(
+                                True(),
+                                True(),
+                                builderStrategy.getRefinementSolverFactory().createUCSolver()),
+                        builderStrategy
+                                .getPrecGranularity()
+                                .createRefiner(builderStrategy.getVarsRefToPrec()),
+                        builderStrategy.getPruneStrategy(),
+                        builderStrategy.getLogger());
             }
-        }, UCB {
+        },
+        UCB {
             @Override
-            public <S extends ExprState, P extends Prec> Refiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(BuilderStrategy<S, P> builderStrategy) {
-                return SingleExprTraceRefiner.create(ExprTraceUCBChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger());
+            public <S extends ExprState, P extends Prec>
+                    ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
+                            BuilderStrategy<S, P> builderStrategy) {
+                return SingleExprTraceRefiner.create(
+                        ExprTraceUCBChecker.create(
+                                True(),
+                                True(),
+                                builderStrategy.getRefinementSolverFactory().createUCSolver()),
+                        builderStrategy
+                                .getPrecGranularity()
+                                .createRefiner(builderStrategy.getItpRefToPrec()),
+                        builderStrategy.getPruneStrategy(),
+                        builderStrategy.getLogger());
             }
         },
         NWT_WP {
             @Override
-            public <S extends ExprState, P extends Prec> Refiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(BuilderStrategy<S, P> builderStrategy) {
-                return SingleExprTraceRefiner.create(ExprTraceNewtonChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()).withoutIT().withSP().withoutLV(), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger());
+            public <S extends ExprState, P extends Prec>
+                    ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
+                            BuilderStrategy<S, P> builderStrategy) {
+                return SingleExprTraceRefiner.create(
+                        ExprTraceNewtonChecker.create(
+                                        True(),
+                                        True(),
+                                        builderStrategy
+                                                .getRefinementSolverFactory()
+                                                .createUCSolver())
+                                .withoutIT()
+                                .withSP()
+                                .withoutLV(),
+                        builderStrategy
+                                .getPrecGranularity()
+                                .createRefiner(builderStrategy.getItpRefToPrec()),
+                        builderStrategy.getPruneStrategy(),
+                        builderStrategy.getLogger());
             }
-        }, NWT_SP {
+        },
+        NWT_SP {
             @Override
-            public <S extends ExprState, P extends Prec> Refiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(BuilderStrategy<S, P> builderStrategy) {
-                return SingleExprTraceRefiner.create(ExprTraceNewtonChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()).withoutIT().withWP().withoutLV(), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger());
+            public <S extends ExprState, P extends Prec>
+                    ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
+                            BuilderStrategy<S, P> builderStrategy) {
+                return SingleExprTraceRefiner.create(
+                        ExprTraceNewtonChecker.create(
+                                        True(),
+                                        True(),
+                                        builderStrategy
+                                                .getRefinementSolverFactory()
+                                                .createUCSolver())
+                                .withoutIT()
+                                .withWP()
+                                .withoutLV(),
+                        builderStrategy
+                                .getPrecGranularity()
+                                .createRefiner(builderStrategy.getItpRefToPrec()),
+                        builderStrategy.getPruneStrategy(),
+                        builderStrategy.getLogger());
             }
-        }, NWT_WP_LV {
+        },
+        NWT_WP_LV {
             @Override
-            public <S extends ExprState, P extends Prec> Refiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(BuilderStrategy<S, P> builderStrategy) {
-                return SingleExprTraceRefiner.create(ExprTraceNewtonChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()).withoutIT().withWP().withLV(), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger());
+            public <S extends ExprState, P extends Prec>
+                    ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
+                            BuilderStrategy<S, P> builderStrategy) {
+                return SingleExprTraceRefiner.create(
+                        ExprTraceNewtonChecker.create(
+                                        True(),
+                                        True(),
+                                        builderStrategy
+                                                .getRefinementSolverFactory()
+                                                .createUCSolver())
+                                .withoutIT()
+                                .withWP()
+                                .withLV(),
+                        builderStrategy
+                                .getPrecGranularity()
+                                .createRefiner(builderStrategy.getItpRefToPrec()),
+                        builderStrategy.getPruneStrategy(),
+                        builderStrategy.getLogger());
             }
-        }, NWT_SP_LV {
+        },
+        NWT_SP_LV {
             @Override
-            public <S extends ExprState, P extends Prec> Refiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(BuilderStrategy<S, P> builderStrategy) {
-                return SingleExprTraceRefiner.create(ExprTraceNewtonChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()).withoutIT().withSP().withLV(), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger());
+            public <S extends ExprState, P extends Prec>
+                    ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
+                            BuilderStrategy<S, P> builderStrategy) {
+                return SingleExprTraceRefiner.create(
+                        ExprTraceNewtonChecker.create(
+                                        True(),
+                                        True(),
+                                        builderStrategy
+                                                .getRefinementSolverFactory()
+                                                .createUCSolver())
+                                .withoutIT()
+                                .withSP()
+                                .withLV(),
+                        builderStrategy
+                                .getPrecGranularity()
+                                .createRefiner(builderStrategy.getItpRefToPrec()),
+                        builderStrategy.getPruneStrategy(),
+                        builderStrategy.getLogger());
             }
-        }, NWT_IT_WP {
+        },
+        NWT_IT_WP {
             @Override
-            public <S extends ExprState, P extends Prec> Refiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(BuilderStrategy<S, P> builderStrategy) {
-                return SingleExprTraceRefiner.create(ExprTraceNewtonChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()).withIT().withWP().withoutLV(), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger());
+            public <S extends ExprState, P extends Prec>
+                    ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
+                            BuilderStrategy<S, P> builderStrategy) {
+                return SingleExprTraceRefiner.create(
+                        ExprTraceNewtonChecker.create(
+                                        True(),
+                                        True(),
+                                        builderStrategy
+                                                .getRefinementSolverFactory()
+                                                .createUCSolver())
+                                .withIT()
+                                .withWP()
+                                .withoutLV(),
+                        builderStrategy
+                                .getPrecGranularity()
+                                .createRefiner(builderStrategy.getItpRefToPrec()),
+                        builderStrategy.getPruneStrategy(),
+                        builderStrategy.getLogger());
             }
-        }, NWT_IT_SP {
+        },
+        NWT_IT_SP {
             @Override
-            public <S extends ExprState, P extends Prec> Refiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(BuilderStrategy<S, P> builderStrategy) {
-                return SingleExprTraceRefiner.create(ExprTraceNewtonChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()).withIT().withSP().withoutLV(), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger());
+            public <S extends ExprState, P extends Prec>
+                    ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
+                            BuilderStrategy<S, P> builderStrategy) {
+                return SingleExprTraceRefiner.create(
+                        ExprTraceNewtonChecker.create(
+                                        True(),
+                                        True(),
+                                        builderStrategy
+                                                .getRefinementSolverFactory()
+                                                .createUCSolver())
+                                .withIT()
+                                .withSP()
+                                .withoutLV(),
+                        builderStrategy
+                                .getPrecGranularity()
+                                .createRefiner(builderStrategy.getItpRefToPrec()),
+                        builderStrategy.getPruneStrategy(),
+                        builderStrategy.getLogger());
             }
-        }, NWT_IT_WP_LV {
+        },
+        NWT_IT_WP_LV {
             @Override
-            public <S extends ExprState, P extends Prec> Refiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(BuilderStrategy<S, P> builderStrategy) {
-                return SingleExprTraceRefiner.create(ExprTraceNewtonChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()).withIT().withWP().withLV(), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger());
+            public <S extends ExprState, P extends Prec>
+                    ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
+                            BuilderStrategy<S, P> builderStrategy) {
+                return SingleExprTraceRefiner.create(
+                        ExprTraceNewtonChecker.create(
+                                        True(),
+                                        True(),
+                                        builderStrategy
+                                                .getRefinementSolverFactory()
+                                                .createUCSolver())
+                                .withIT()
+                                .withWP()
+                                .withLV(),
+                        builderStrategy
+                                .getPrecGranularity()
+                                .createRefiner(builderStrategy.getItpRefToPrec()),
+                        builderStrategy.getPruneStrategy(),
+                        builderStrategy.getLogger());
             }
-        }, NWT_IT_SP_LV {
+        },
+        NWT_IT_SP_LV {
             @Override
-            public <S extends ExprState, P extends Prec> Refiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(BuilderStrategy<S, P> builderStrategy) {
-                return SingleExprTraceRefiner.create(ExprTraceNewtonChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()).withIT().withSP().withLV(), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger());
+            public <S extends ExprState, P extends Prec>
+                    ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
+                            BuilderStrategy<S, P> builderStrategy) {
+                return SingleExprTraceRefiner.create(
+                        ExprTraceNewtonChecker.create(
+                                        True(),
+                                        True(),
+                                        builderStrategy
+                                                .getRefinementSolverFactory()
+                                                .createUCSolver())
+                                .withIT()
+                                .withSP()
+                                .withLV(),
+                        builderStrategy
+                                .getPrecGranularity()
+                                .createRefiner(builderStrategy.getItpRefToPrec()),
+                        builderStrategy.getPruneStrategy(),
+                        builderStrategy.getLogger());
             }
         };
 
@@ -248,24 +455,25 @@ public <S extends ExprState> StopCriterion<S, CfaAction> getStopCriterion() {
             return StopCriterions.firstCex();
         }
 
-        public abstract <S extends ExprState, P extends Prec> Refiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(BuilderStrategy<S, P> builderStrategy);
-
+        public abstract <S extends ExprState, P extends Prec>
+                ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
+                        BuilderStrategy<S, P> builderStrategy);
     }
 
     public enum Search {
         BFS {
             @Override
             public ArgNodeComparator getComp(final CFA cfa, final CFA.Loc errLoc) {
-                return ArgNodeComparators.combine(ArgNodeComparators.targetFirst(),
-                        ArgNodeComparators.bfs());
+                return ArgNodeComparators.combine(
+                        ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs());
             }
         },
 
         DFS {
             @Override
             public ArgNodeComparator getComp(final CFA cfa, final CFA.Loc errLoc) {
-                return ArgNodeComparators.combine(ArgNodeComparators.targetFirst(),
-                        ArgNodeComparators.dfs());
+                return ArgNodeComparators.combine(
+                        ArgNodeComparators.targetFirst(), ArgNodeComparators.dfs());
             }
         },
 
@@ -277,7 +485,6 @@ public ArgNodeComparator getComp(final CFA cfa, final CFA.Loc errLoc) {
         };
 
         public abstract ArgNodeComparator getComp(CFA cfa, CFA.Loc errLoc);
-
     }
 
     public enum PredSplit {
@@ -302,8 +509,9 @@ public <P extends Prec> CfaPrec<P> createPrec(final P innerPrec) {
             }
 
             @Override
-            public <S extends ExprState, A extends Action, P extends Prec, R extends Refutation> PrecRefiner<CfaState<S>, A, CfaPrec<P>, R> createRefiner(
-                    final RefutationToPrec<P, R> refToPrec) {
+            public <S extends ExprState, A extends Action, P extends Prec, R extends Refutation>
+                    PrecRefiner<CfaState<S>, A, CfaPrec<P>, R> createRefiner(
+                            final RefutationToPrec<P, R> refToPrec) {
                 return GlobalCfaPrecRefiner.create(refToPrec);
             }
 
@@ -320,8 +528,9 @@ public <P extends Prec> CfaPrec<P> createPrec(final P innerPrec) {
             }
 
             @Override
-            public <S extends ExprState, A extends Action, P extends Prec, R extends Refutation> PrecRefiner<CfaState<S>, A, CfaPrec<P>, R> createRefiner(
-                    final RefutationToPrec<P, R> refToPrec) {
+            public <S extends ExprState, A extends Action, P extends Prec, R extends Refutation>
+                    PrecRefiner<CfaState<S>, A, CfaPrec<P>, R> createRefiner(
+                            final RefutationToPrec<P, R> refToPrec) {
                 return LocalCfaPrecRefiner.create(refToPrec);
             }
 
@@ -333,8 +542,10 @@ public CfaPrec<PredPrec> assumePrecs(CFA cfa) {
 
         public abstract <P extends Prec> CfaPrec<P> createPrec(P innerPrec);
 
-        public abstract <S extends ExprState, A extends Action, P extends Prec, R extends Refutation> PrecRefiner<CfaState<S>, A, CfaPrec<P>, R> createRefiner(
-                RefutationToPrec<P, R> refToPrec);
+        public abstract <
+                        S extends ExprState, A extends Action, P extends Prec, R extends Refutation>
+                PrecRefiner<CfaState<S>, A, CfaPrec<P>, R> createRefiner(
+                        RefutationToPrec<P, R> refToPrec);
 
         public abstract CfaPrec<PredPrec> assumePrecs(CFA cfa);
     }
@@ -358,19 +569,37 @@ public CfaLts getLts(CFA.Loc errorLoc) {
     }
 
     public enum InitPrec {
-        EMPTY, ALLVARS, ALLASSUMES
+        EMPTY,
+        ALLVARS,
+        ALLASSUMES
     }
 
     public abstract class BuilderStrategy<S extends ExprState, P extends Prec> {
 
-        protected static final String UNSUPPORTED_CONFIG_VALUE = "Builder strategy %s does not support configuration value %s as %s";
+        protected static final String UNSUPPORTED_CONFIG_VALUE =
+                "Builder strategy %s does not support configuration value %s as %s";
         protected final CFA cfa;
 
         @SuppressWarnings("java:S1699")
         protected BuilderStrategy(CFA cfa) {
-            checkState(getSupportedDomains().contains(domain), UNSUPPORTED_CONFIG_VALUE, getClass().getSimpleName(), domain, "domain");
-            checkState(getSupportedRefinements().contains(refinement), UNSUPPORTED_CONFIG_VALUE, getClass().getSimpleName(), refinement, "refinement");
-            checkState(getSupportedInitPrecs().contains(initPrec), UNSUPPORTED_CONFIG_VALUE, getClass().getSimpleName(), initPrec, "initial precision");
+            checkState(
+                    getSupportedDomains().contains(domain),
+                    UNSUPPORTED_CONFIG_VALUE,
+                    getClass().getSimpleName(),
+                    domain,
+                    "domain");
+            checkState(
+                    getSupportedRefinements().contains(refinement),
+                    UNSUPPORTED_CONFIG_VALUE,
+                    getClass().getSimpleName(),
+                    refinement,
+                    "refinement");
+            checkState(
+                    getSupportedInitPrecs().contains(initPrec),
+                    UNSUPPORTED_CONFIG_VALUE,
+                    getClass().getSimpleName(),
+                    initPrec,
+                    "initial precision");
             this.cfa = cfa;
         }
 
@@ -389,7 +618,10 @@ public CfaAnalysis<S, P> getAnalysis() {
         public abstract RefutationToPrec<P, ItpRefutation> getItpRefToPrec();
 
         public RefutationToPrec<P, VarsRefutation> getVarsRefToPrec() {
-            throw new UnsupportedOperationException(String.format("Builder strategy %s can not provide Vars refutation to precision", getClass().getSimpleName()));
+            throw new UnsupportedOperationException(
+                    String.format(
+                            "Builder strategy %s can not provide Vars refutation to precision",
+                            getClass().getSimpleName()));
         }
 
         protected SolverFactory getRefinementSolverFactory() {
@@ -421,22 +653,30 @@ public CfaLts getLts() {
         public CfaConfig<CfaState<S>, CfaAction, CfaPrec<P>> buildConfig(CFA.Loc errLoc) {
             final Predicate<CfaState<S>> target = new CfaErrorlocPredicate<>(errLoc);
             final Analysis<CfaState<S>, CfaAction, CfaPrec<P>> analysis = getAnalysis();
-            final ArgBuilder<CfaState<S>, CfaAction, CfaPrec<P>> argBuilder = ArgBuilder.create(
-                    getLts(errLoc), analysis, target,
-                    true);
-            final Abstractor<CfaState<S>, CfaAction, CfaPrec<P>> abstractor = BasicAbstractor.builder(
-                            argBuilder)
-                    .waitlist(PriorityWaitlist.create(search.getComp(cfa, errLoc)))
-                    .stopCriterion(refinement.getStopCriterion())
-                    .logger(logger).build();
-            final Refiner<CfaState<S>, CfaAction, CfaPrec<P>> refiner = refinement.getRefiner(this);
-            final SafetyChecker<ARG<CfaState<S>, CfaAction>, Trace<CfaState<S>, CfaAction>, CfaPrec<P>> checker = CegarChecker.create(
-                    abstractor, refiner,
-                    logger);
+            final ArgBuilder<CfaState<S>, CfaAction, CfaPrec<P>> argBuilder =
+                    ArgBuilder.create(getLts(errLoc), analysis, target, true);
+            final ArgAbstractor<CfaState<S>, CfaAction, CfaPrec<P>> abstractor =
+                    BasicArgAbstractor.builder(argBuilder)
+                            .waitlist(PriorityWaitlist.create(search.getComp(cfa, errLoc)))
+                            .stopCriterion(refinement.getStopCriterion())
+                            .logger(logger)
+                            .build();
+            final ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> refiner =
+                    refinement.getRefiner(this);
+            final SafetyChecker<
+                            ARG<CfaState<S>, CfaAction>, Trace<CfaState<S>, CfaAction>, CfaPrec<P>>
+                    checker = ArgCegarChecker.create(abstractor, refiner, logger);
             return CfaConfig.create(checker, createInitPrec());
         }
 
-        public MultiAnalysisSide<CfaState<S>, S, CfaState<UnitState>, CfaAction, CfaPrec<P>, CfaPrec<UnitPrec>> getMultiSide() {
+        public MultiAnalysisSide<
+                        CfaState<S>,
+                        S,
+                        CfaState<UnitState>,
+                        CfaAction,
+                        CfaPrec<P>,
+                        CfaPrec<UnitPrec>>
+                getMultiSide() {
             return new MultiAnalysisSide<>(
                     getAnalysis(),
                     CfaControlInitFuncKt.cfaControlInitFunc(cfa.getInitLoc()),
@@ -470,7 +710,8 @@ public Set<InitPrec> getSupportedInitPrecs() {
 
         @Override
         public Analysis<ExplState, StmtAction, ? super ExplPrec> getDataAnalysis() {
-            return ExplStmtAnalysis.create(abstractionSolverFactory.createSolver(), True(), maxEnum);
+            return ExplStmtAnalysis.create(
+                    abstractionSolverFactory.createSolver(), True(), maxEnum);
         }
 
         @Override
@@ -489,7 +730,12 @@ public CfaPrec<ExplPrec> createInitPrec() {
                 case EMPTY -> precGranularity.createPrec(ExplPrec.empty());
                 case ALLVARS -> precGranularity.createPrec(ExplPrec.of(cfa.getVars()));
                 default ->
-                        throw new UnsupportedOperationException(String.format(UNSUPPORTED_CONFIG_VALUE, getClass().getSimpleName(), initPrec, "initial precision"));
+                        throw new UnsupportedOperationException(
+                                String.format(
+                                        UNSUPPORTED_CONFIG_VALUE,
+                                        getClass().getSimpleName(),
+                                        initPrec,
+                                        "initial precision"));
             };
         }
     }
@@ -520,8 +766,7 @@ public Set<Refinement> getSupportedRefinements() {
                     Refinement.NWT_IT_SP,
                     Refinement.NWT_IT_WP,
                     Refinement.NWT_IT_SP_LV,
-                    Refinement.NWT_IT_WP_LV
-            );
+                    Refinement.NWT_IT_WP_LV);
         }
 
         @Override
@@ -546,9 +791,13 @@ public CfaPrec<PredPrec> createInitPrec() {
                 case EMPTY -> precGranularity.createPrec(PredPrec.of());
                 case ALLASSUMES -> precGranularity.assumePrecs(cfa);
                 default ->
-                        throw new UnsupportedOperationException(String.format(UNSUPPORTED_CONFIG_VALUE, getClass().getSimpleName(), initPrec, "initial precision"));
+                        throw new UnsupportedOperationException(
+                                String.format(
+                                        UNSUPPORTED_CONFIG_VALUE,
+                                        getClass().getSimpleName(),
+                                        initPrec,
+                                        "initial precision"));
             };
         }
     }
-
 }
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/Abstractor.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/Abstractor.java
index a7eb473efd..a6cb49bb43 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/Abstractor.java
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/Abstractor.java
@@ -15,31 +15,23 @@
  */
 package hu.bme.mit.theta.analysis.algorithm.cegar;
 
-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.ARG;
+import hu.bme.mit.theta.analysis.algorithm.Witness;
 
 /**
- * Common interface for the abstractor component. It can create an initial ARG and check an ARG with
+ * Common interface for the abstractor component. It can create an initial witness and check a witness with
  * a given precision.
  */
-public interface Abstractor<S extends State, A extends Action, P extends Prec> {
+public interface Abstractor<P extends Prec, W extends Witness> {
 
     /**
-     * Create initial ARG.
-     *
-     * @return
+     * Create initial witness
      */
-    ARG<S, A> createArg();
+    W createWitness();
 
     /**
-     * Check ARG with given precision.
-     *
-     * @param arg
-     * @param prec
-     * @return
+     * Check witness with given precision
      */
-    AbstractorResult check(ARG<S, A> arg, P prec);
+    AbstractorResult check(W witness, P prec);
 
 }
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgAbstractor.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgAbstractor.java
new file mode 100644
index 0000000000..67890b8a3a
--- /dev/null
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgAbstractor.java
@@ -0,0 +1,28 @@
+/*
+ *  Copyright 2024 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.analysis.algorithm.cegar;
+
+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.ARG;
+
+/**
+ * Common interface for the abstractor component. It can create an initial ARG and check an ARG with
+ * a given precision.
+ */
+public interface ArgAbstractor<S extends State, A extends Action, P extends Prec>
+        extends Abstractor<P, ARG<S, A>> {}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgCegarChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgCegarChecker.java
new file mode 100644
index 0000000000..06260c732c
--- /dev/null
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgCegarChecker.java
@@ -0,0 +1,48 @@
+/*
+ *  Copyright 2024 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.analysis.algorithm.cegar;
+
+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.Trace;
+import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
+import hu.bme.mit.theta.analysis.utils.ArgVisualizer;
+import hu.bme.mit.theta.common.logging.Logger;
+import hu.bme.mit.theta.common.logging.NullLogger;
+
+/**
+ * Counterexample-Guided Abstraction Refinement (CEGAR) loop implementation,
+ * that uses an Abstractor to explore the abstract state space and a Refiner to
+ * check counterexamples and refine them if needed. It also provides certain
+ * statistics about its execution.
+ */
+public final class ArgCegarChecker {
+
+    private ArgCegarChecker() {
+    }
+
+    public static <S extends State, A extends Action, P extends Prec> CegarChecker<S, A, P, ARG<S, A>, Trace<S, A>> create(
+            final ArgAbstractor<S, A, P> abstractor, final ArgRefiner<S, A, P> refiner) {
+        return create(abstractor, refiner, NullLogger.getInstance());
+    }
+
+    public static <S extends State, A extends Action, P extends Prec> CegarChecker<S, A, P, ARG<S, A>, Trace<S, A>> create(
+            final ArgAbstractor<S, A, P> abstractor, final ArgRefiner<S, A, P> refiner, final Logger logger) {
+        return CegarChecker.create(abstractor, refiner, logger, ArgVisualizer.getDefault());
+    }
+
+}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgRefiner.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgRefiner.java
new file mode 100644
index 0000000000..2683a2fd0f
--- /dev/null
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgRefiner.java
@@ -0,0 +1,29 @@
+/*
+ *  Copyright 2024 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.analysis.algorithm.cegar;
+
+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.Trace;
+import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
+
+/**
+ * Common interface for refiners. It takes an ARG and a precision, checks if the counterexample in
+ * the ARG is feasible and if not, it refines the precision and may also prune the ARG.
+ */
+public interface ArgRefiner<S extends State, A extends Action, P extends Prec> extends Refiner<S, A, P, ARG<S, A>, Trace<S, A>> {
+}
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/BasicArgAbstractor.java
similarity index 91%
rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicAbstractor.java
rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicArgAbstractor.java
index 42eb1487e1..050ae32ce3 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/BasicArgAbstractor.java
@@ -41,7 +41,7 @@
 /**
  * Basic implementation for the abstractor, relying on an ArgBuilder.
  */
-public class BasicAbstractor<S extends State, A extends Action, P extends Prec> implements Abstractor<S, A, P> {
+public class BasicArgAbstractor<S extends State, A extends Action, P extends Prec> implements ArgAbstractor<S, A, P> {
 
     protected final ArgBuilder<S, A, P> argBuilder;
     protected final Function<? super S, ?> projection;
@@ -49,8 +49,8 @@ public class BasicAbstractor<S extends State, A extends Action, P extends Prec>
     protected final StopCriterion<S, A> stopCriterion;
     protected 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) {
+    protected BasicArgAbstractor(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);
@@ -64,7 +64,7 @@ public static <S extends State, A extends Action, P extends Prec> Builder<S, A,
     }
 
     @Override
-    public ARG<S, A> createArg() {
+    public ARG<S, A> createWitness() {
         return argBuilder.createArg();
     }
 
@@ -174,8 +174,8 @@ public Builder<S, A, P> logger(final Logger logger) {
             return this;
         }
 
-        public BasicAbstractor<S, A, P> build() {
-            return new BasicAbstractor<>(argBuilder, projection, waitlist, stopCriterion, logger);
+        public BasicArgAbstractor<S, A, P> build() {
+            return new BasicArgAbstractor<>(argBuilder, projection, waitlist, stopCriterion, logger);
         }
     }
 
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java
index af69cd7121..fa811afc42 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java
@@ -17,19 +17,18 @@
 
 import com.google.common.base.Stopwatch;
 import hu.bme.mit.theta.analysis.Action;
+import hu.bme.mit.theta.analysis.Cex;
 import hu.bme.mit.theta.analysis.Prec;
 import hu.bme.mit.theta.analysis.State;
-import hu.bme.mit.theta.analysis.Trace;
-import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
-import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
 import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
+import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
+import hu.bme.mit.theta.analysis.algorithm.Witness;
 import hu.bme.mit.theta.analysis.runtimemonitor.MonitorCheckpoint;
-import hu.bme.mit.theta.analysis.utils.ArgVisualizer;
+import hu.bme.mit.theta.analysis.utils.WitnessVisualizer;
 import hu.bme.mit.theta.common.Utils;
 import hu.bme.mit.theta.common.logging.Logger;
 import hu.bme.mit.theta.common.logging.Logger.Level;
 import hu.bme.mit.theta.common.logging.NullLogger;
-
 import hu.bme.mit.theta.common.visualization.writer.JSONWriter;
 import hu.bme.mit.theta.common.visualization.writer.WebDebuggerLogger;
 
@@ -43,42 +42,44 @@
  * check counterexamples and refine them if needed. It also provides certain
  * statistics about its execution.
  */
-public final class CegarChecker<S extends State, A extends Action, P extends Prec> implements SafetyChecker<ARG<S, A>, Trace<S, A>, P> {
+public final class CegarChecker<S extends State, A extends Action, P extends Prec, W extends Witness, C extends Cex> implements SafetyChecker<W, C, P> {
 
-    private final Abstractor<S, A, P> abstractor;
-    private final Refiner<S, A, P> refiner;
+    private final Abstractor<P, W> abstractor;
+    private final Refiner<S, A, P, W, C> refiner;
     private final Logger logger;
-    private final ARG<S, A> arg; // TODO I don't think putting the ARG up here from check below causes any issues, but keep it in mind, that it might
+    private final W witness;
+    private final WitnessVisualizer<? super W> witnessVisualizer;
 
-    private CegarChecker(final Abstractor<S, A, P> abstractor, final Refiner<S, A, P> refiner, final Logger logger) {
+    private CegarChecker(final Abstractor<P, W> abstractor, final Refiner<S, A, P, W, C> refiner, final Logger logger, final WitnessVisualizer<? super W> witnessVisualizer) {
         this.abstractor = checkNotNull(abstractor);
         this.refiner = checkNotNull(refiner);
         this.logger = checkNotNull(logger);
-        arg = abstractor.createArg();
+        witness = abstractor.createWitness();
+        this.witnessVisualizer = checkNotNull(witnessVisualizer);
     }
 
-    public static <S extends State, A extends Action, P extends Prec> CegarChecker<S, A, P> create(
-            final Abstractor<S, A, P> abstractor, final Refiner<S, A, P> refiner) {
-        return new CegarChecker<>(abstractor, refiner, NullLogger.getInstance());
+    public static <S extends State, A extends Action, P extends Prec, W extends Witness, C extends Cex> CegarChecker<S, A, P, W, C> create(
+            final Abstractor<P, W> abstractor, final Refiner<S, A, P, W, C> refiner, final WitnessVisualizer<W> witnessVisualizer) {
+        return create(abstractor, refiner, NullLogger.getInstance(), witnessVisualizer);
     }
 
-    public static <S extends State, A extends Action, P extends Prec> CegarChecker<S, A, P> create(
-            final Abstractor<S, A, P> abstractor, final Refiner<S, A, P> refiner, final Logger logger) {
-        return new CegarChecker<>(abstractor, refiner, logger);
+    public static <S extends State, A extends Action, P extends Prec, W extends Witness, C extends Cex> CegarChecker<S, A, P, W, C> create(
+            final Abstractor<P, W> abstractor, final Refiner<S, A, P, W, C> refiner, final Logger logger, final WitnessVisualizer<? super W> witnessVisualizer) {
+        return new CegarChecker<>(abstractor, refiner, logger, witnessVisualizer);
     }
 
-    public ARG<S, A> getArg() {
-        return arg;
+    public W getWitness() {
+        return witness;
     }
 
     @Override
-    public SafetyResult<ARG<S, A>, Trace<S, A>> check(final P initPrec) {
+    public SafetyResult<W, C> check(final P initPrec) {
         logger.write(Level.INFO, "Configuration: %s%n", this);
         final Stopwatch stopwatch = Stopwatch.createStarted();
         long abstractorTime = 0;
         long refinerTime = 0;
-        RefinerResult<S, A, P> refinerResult = null;
-        AbstractorResult abstractorResult = null;
+        RefinerResult<S, A, P, C> refinerResult = null;
+        AbstractorResult abstractorResult;
         P prec = initPrec;
         int iteration = 0;
         WebDebuggerLogger wdl = WebDebuggerLogger.getInstance();
@@ -88,12 +89,12 @@ public SafetyResult<ARG<S, A>, Trace<S, A>> check(final P initPrec) {
             logger.write(Level.MAINSTEP, "Iteration %d%n", iteration);
             logger.write(Level.MAINSTEP, "| Checking abstraction...%n");
             final long abstractorStartTime = stopwatch.elapsed(TimeUnit.MILLISECONDS);
-            abstractorResult = abstractor.check(arg, prec);
+            abstractorResult = abstractor.check(witness, prec);
             abstractorTime += stopwatch.elapsed(TimeUnit.MILLISECONDS) - abstractorStartTime;
             logger.write(Level.MAINSTEP, "| Checking abstraction done, result: %s%n", abstractorResult);
 
             if (WebDebuggerLogger.enabled()) {
-                String argGraph = JSONWriter.getInstance().writeString(ArgVisualizer.getDefault().visualize(arg));
+                String argGraph = JSONWriter.getInstance().writeString(witnessVisualizer.visualize(witness));
                 String precString = prec.toString();
                 wdl.addIteration(iteration, argGraph, precString);
             }
@@ -104,7 +105,7 @@ public SafetyResult<ARG<S, A>, Trace<S, A>> check(final P initPrec) {
                 P lastPrec = prec;
                 logger.write(Level.MAINSTEP, "| Refining abstraction...%n");
                 final long refinerStartTime = stopwatch.elapsed(TimeUnit.MILLISECONDS);
-                refinerResult = refiner.refine(arg, prec);
+                refinerResult = refiner.refine(witness, prec);
                 refinerTime += stopwatch.elapsed(TimeUnit.MILLISECONDS) - refinerStartTime;
                 logger.write(Level.MAINSTEP, "Refining abstraction done, result: %s%n", refinerResult);
 
@@ -123,16 +124,16 @@ public SafetyResult<ARG<S, A>, Trace<S, A>> check(final P initPrec) {
         } while (!abstractorResult.isSafe() && !refinerResult.isUnsafe());
 
         stopwatch.stop();
-        SafetyResult<ARG<S, A>, Trace<S, A>> cegarResult = null;
+        SafetyResult<W, C> cegarResult = null;
         final CegarStatistics stats = new CegarStatistics(stopwatch.elapsed(TimeUnit.MILLISECONDS), abstractorTime,
                 refinerTime, iteration);
 
-        assert abstractorResult.isSafe() || (refinerResult != null && refinerResult.isUnsafe());
+        assert abstractorResult.isSafe() || refinerResult.isUnsafe();
 
         if (abstractorResult.isSafe()) {
-            cegarResult = SafetyResult.safe(arg, stats);
+            cegarResult = SafetyResult.safe(witness, stats);
         } else if (refinerResult.isUnsafe()) {
-            cegarResult = SafetyResult.unsafe(refinerResult.asUnsafe().getCex(), arg, stats);
+            cegarResult = SafetyResult.unsafe(refinerResult.asUnsafe().getCex(), witness, stats);
         }
 
         assert cegarResult != null;
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/Refiner.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/Refiner.java
index 0bbfe07f1d..6eca5d7c21 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/Refiner.java
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/Refiner.java
@@ -16,23 +16,19 @@
 package hu.bme.mit.theta.analysis.algorithm.cegar;
 
 import hu.bme.mit.theta.analysis.Action;
+import hu.bme.mit.theta.analysis.Cex;
 import hu.bme.mit.theta.analysis.Prec;
 import hu.bme.mit.theta.analysis.State;
-import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
+import hu.bme.mit.theta.analysis.algorithm.Witness;
 
 /**
- * Common interface for refiners. It takes an ARG and a precision, checks if the counterexample in
- * the ARG is feasible and if not, it refines the precision and may also prune the ARG.
+ * Common interface for refiners. It takes a witness and a precision, checks if the counterexample in
+ * the witness is feasible and if not, it refines the precision
  */
-public interface Refiner<S extends State, A extends Action, P extends Prec> {
+public interface Refiner<S extends State, A extends Action, P extends Prec, W extends Witness, C extends Cex> {
 
     /**
-     * Checks if the counterexample in the ARG is feasible. If not, refines the precision and prunes
-     * the ARG.
-     *
-     * @param arg
-     * @param prec
-     * @return
+     * Checks if the counterexample in the witness is feasible. If not, refines the precision
      */
-    RefinerResult<S, A, P> refine(ARG<S, A> arg, P prec);
+    RefinerResult<S, A, P, C> refine(W witness, P prec);
 }
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/RefinerResult.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/RefinerResult.java
index bbce8b5451..a4be30781e 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/RefinerResult.java
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/RefinerResult.java
@@ -15,30 +15,29 @@
  */
 package hu.bme.mit.theta.analysis.algorithm.cegar;
 
-import static com.google.common.base.Preconditions.checkNotNull;
-
 import hu.bme.mit.theta.analysis.Action;
+import hu.bme.mit.theta.analysis.Cex;
 import hu.bme.mit.theta.analysis.Prec;
 import hu.bme.mit.theta.analysis.State;
-import hu.bme.mit.theta.analysis.Trace;
 import hu.bme.mit.theta.common.Utils;
 
+import static com.google.common.base.Preconditions.checkNotNull;
+
 /**
  * Represents the result of the Refiner class that can be either spurious or unsafe. In the former
  * case it also contains the refined precision and in the latter case the feasible counterexample.
  */
-public abstract class RefinerResult<S extends State, A extends Action, P extends Prec> {
+public abstract class RefinerResult<S extends State, A extends Action, P extends Prec, C extends Cex> {
 
-    private RefinerResult() {
+    protected RefinerResult() {
     }
 
     /**
      * Create a new spurious result.
      *
      * @param refinedPrec Refined precision
-     * @return
      */
-    public static <S extends State, A extends Action, P extends Prec> Spurious<S, A, P> spurious(
+    public static <S extends State, A extends Action, P extends Prec, C extends Cex> Spurious<S, A, P, C> spurious(
             final P refinedPrec) {
         return new Spurious<>(refinedPrec);
     }
@@ -47,10 +46,9 @@ public static <S extends State, A extends Action, P extends Prec> Spurious<S, A,
      * Creates a new unsafe result.
      *
      * @param cex Feasible counterexample
-     * @return
      */
-    public static <S extends State, A extends Action, P extends Prec> Unsafe<S, A, P> unsafe(
-            final Trace<S, A> cex) {
+    public static <S extends State, A extends Action, P extends Prec, C extends Cex> Unsafe<S, A, P, C> unsafe(
+            final C cex) {
         return new Unsafe<>(cex);
     }
 
@@ -58,15 +56,15 @@ public static <S extends State, A extends Action, P extends Prec> Unsafe<S, A, P
 
     public abstract boolean isUnsafe();
 
-    public abstract Spurious<S, A, P> asSpurious();
+    public abstract Spurious<S, A, P, C> asSpurious();
 
-    public abstract Unsafe<S, A, P> asUnsafe();
+    public abstract Unsafe<S, A, P, C> asUnsafe();
 
     /**
      * Represents the spurious result with a refined precision.
      */
-    public static final class Spurious<S extends State, A extends Action, P extends Prec>
-            extends RefinerResult<S, A, P> {
+    public static final class Spurious<S extends State, A extends Action, P extends Prec, C extends Cex>
+            extends RefinerResult<S, A, P, C> {
 
         private final P refinedPrec;
 
@@ -89,12 +87,12 @@ public boolean isUnsafe() {
         }
 
         @Override
-        public Spurious<S, A, P> asSpurious() {
+        public Spurious<S, A, P, C> asSpurious() {
             return this;
         }
 
         @Override
-        public Unsafe<S, A, P> asUnsafe() {
+        public Unsafe<S, A, P, C> asUnsafe() {
             throw new ClassCastException(
                     "Cannot cast " + Spurious.class.getSimpleName() + " to "
                             + Unsafe.class.getSimpleName());
@@ -111,16 +109,16 @@ public String toString() {
     /**
      * Represents the unsafe result with a feasible counterexample.
      */
-    public static final class Unsafe<S extends State, A extends Action, P extends Prec> extends
-            RefinerResult<S, A, P> {
+    public static final class Unsafe<S extends State, A extends Action, P extends Prec, C extends Cex> extends
+            RefinerResult<S, A, P, C> {
 
-        private final Trace<S, A> cex;
+        private final C cex;
 
-        private Unsafe(final Trace<S, A> cex) {
+        private Unsafe(final C cex) {
             this.cex = checkNotNull(cex);
         }
 
-        public Trace<S, A> getCex() {
+        public C getCex() {
             return cex;
         }
 
@@ -135,14 +133,14 @@ public boolean isUnsafe() {
         }
 
         @Override
-        public Spurious<S, A, P> asSpurious() {
+        public Spurious<S, A, P, C> asSpurious() {
             throw new ClassCastException(
                     "Cannot cast " + Unsafe.class.getSimpleName() + " to "
                             + Spurious.class.getSimpleName());
         }
 
         @Override
-        public Unsafe<S, A, P> asUnsafe() {
+        public Unsafe<S, A, P, C> asUnsafe() {
             return this;
         }
 
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/AasporRefiner.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/AasporRefiner.java
index 8f2f499547..f1f7430241 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/AasporRefiner.java
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/AasporRefiner.java
@@ -16,9 +16,10 @@
 package hu.bme.mit.theta.analysis.expr.refinement;
 
 import hu.bme.mit.theta.analysis.Prec;
+import hu.bme.mit.theta.analysis.Trace;
 import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode;
-import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner;
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgRefiner;
 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;
@@ -29,15 +30,15 @@
 import java.util.Set;
 import java.util.stream.Collectors;
 
-public final class AasporRefiner<S extends ExprState, A extends ExprAction, P extends Prec> implements Refiner<S, A, P> {
+public final class AasporRefiner<S extends ExprState, A extends ExprAction, P extends Prec> implements ArgRefiner<S, A, P> {
 
-    private final Refiner<S, A, P> refiner;
+    private final ArgRefiner<S, A, P> refiner;
 
     private final PruneStrategy pruneStrategy;
 
     private final Map<VarDecl<?>, Set<S>> ignoredVarRegistry;
 
-    private AasporRefiner(final Refiner<S, A, P> refiner,
+    private AasporRefiner(final ArgRefiner<S, A, P> refiner,
                           final PruneStrategy pruneStrategy,
                           final Map<VarDecl<?>, Set<S>> ignoredVarRegistry) {
         this.refiner = refiner;
@@ -46,14 +47,14 @@ private AasporRefiner(final Refiner<S, A, P> refiner,
     }
 
     public static <S extends ExprState, A extends ExprAction, P extends Prec> AasporRefiner<S, A, P> create(
-            final Refiner<S, A, P> refiner, final PruneStrategy pruneStrategy,
+            final ArgRefiner<S, A, P> refiner, final PruneStrategy pruneStrategy,
             final Map<VarDecl<?>, Set<S>> ignoredVarRegistry) {
         return new AasporRefiner<>(refiner, pruneStrategy, ignoredVarRegistry);
     }
 
     @Override
-    public RefinerResult<S, A, P> refine(final ARG<S, A> arg, final P prec) {
-        final RefinerResult<S, A, P> result = refiner.refine(arg, prec);
+    public RefinerResult<S, A, P, Trace<S, A>> refine(final ARG<S, A> arg, final P prec) {
+        final RefinerResult<S, A, P, Trace<S, A>> result = refiner.refine(arg, prec);
         if (result.isUnsafe() || pruneStrategy != PruneStrategy.LAZY) return result;
 
         final P newPrec = result.asSpurious().getRefinedPrec();
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/MultiExprTraceRefiner.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/MultiExprTraceRefiner.java
index 72c516adef..b2cee796d0 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/MultiExprTraceRefiner.java
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/MultiExprTraceRefiner.java
@@ -20,7 +20,7 @@
 import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode;
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgTrace;
-import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner;
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgRefiner;
 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;
@@ -34,7 +34,7 @@
 import static com.google.common.base.Preconditions.checkNotNull;
 
 public final class MultiExprTraceRefiner<S extends ExprState, A extends ExprAction, P extends Prec, R extends Refutation>
-        implements Refiner<S, A, P> {
+        implements ArgRefiner<S, A, P> {
 
     private final ExprTraceChecker<R> exprTraceChecker;
     private final PrecRefiner<S, A, P, R> precRefiner;
@@ -76,17 +76,17 @@ public static <S extends ExprState, A extends ExprAction, P extends Prec, R exte
     }
 
     @Override
-    public RefinerResult<S, A, P> refine(final ARG<S, A> arg, final P prec) {
+    public RefinerResult<S, A, P, Trace<S, A>> refine(final ARG<S, A> arg, final P prec) {
         checkNotNull(arg);
         checkNotNull(prec);
         assert !arg.isSafe() : "ARG must be unsafe";
 
-        final List<ArgTrace<S, A>> cexs = arg.getCexs().collect(Collectors.toList());
-        final List<Trace<S, A>> traces = arg.getCexs().map(ArgTrace::toTrace).collect(Collectors.toList());
+        final List<ArgTrace<S, A>> cexs = arg.getCexs().toList();
+        final List<Trace<S, A>> traces = arg.getCexs().map(ArgTrace::toTrace).toList();
         assert traces.size() == cexs.size();
 
         logger.write(Level.INFO, "|  |  Number of traces: %d%n", traces.size());
-        assert traces.size() > 0 : "No counterexample in ARG";
+        assert !traces.isEmpty() : "No counterexample in ARG";
 
         logger.write(Level.SUBSTEP, "|  |  Checking traces...");
         final List<ExprTraceStatus<R>> cexStatuses = new ArrayList<>(traces.size());
@@ -106,7 +106,7 @@ public RefinerResult<S, A, P> refine(final ARG<S, A> arg, final P prec) {
             assert cexStatuses.size() == cexs.size();
             logger.write(Level.SUBSTEP, "done, result: all infeasible%n");
             final List<R> refutations = cexStatuses.stream().map(s -> s.asInfeasible().getRefutation())
-                    .collect(Collectors.toList());
+                    .toList();
             assert refutations.size() == cexs.size();
 
             final List<ArgNode<S, A>> nodesToPrune = new ArrayList<>(traces.size());
@@ -120,7 +120,7 @@ public RefinerResult<S, A, P> refine(final ARG<S, A> arg, final P prec) {
 
             for (int i = 0; i < nodesToPrune.size(); ++i) {
                 final ArgNode<S, A> node = nodesToPrune.get(i);
-                if (node.properAncestors().anyMatch(a -> nodesToPrune.contains(a))) {
+                if (node.properAncestors().anyMatch(nodesToPrune::contains)) {
                     skip.set(i, true);
                 }
             }
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 ac06cf2a87..126f4212f4 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
@@ -20,7 +20,7 @@
 import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode;
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgTrace;
-import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner;
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgRefiner;
 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;
@@ -37,7 +37,7 @@
  * ExprActions) using an ExprTraceChecker and a PrecRefiner.
  */
 public class SingleExprTraceRefiner<S extends ExprState, A extends ExprAction, P extends Prec, R extends Refutation>
-        implements Refiner<S, A, P> {
+        implements ArgRefiner<S, A, P> {
     protected final ExprTraceChecker<R> exprTraceChecker;
     protected final PrecRefiner<S, A, P, R> precRefiner;
     protected final PruneStrategy pruneStrategy;
@@ -78,7 +78,7 @@ public static <S extends ExprState, A extends ExprAction, P extends Prec, R exte
     }
 
     @Override
-    public RefinerResult<S, A, P> refine(final ARG<S, A> arg, final P prec) {
+    public RefinerResult<S, A, P, Trace<S, A>> refine(final ARG<S, A> arg, final P prec) {
         checkNotNull(arg);
         checkNotNull(prec);
         assert !arg.isSafe() : "ARG must be unsafe";
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/ArgVisualizer.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/ArgVisualizer.java
index 9992e5a3e7..c4c82eeb74 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/ArgVisualizer.java
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/ArgVisualizer.java
@@ -36,7 +36,7 @@
 import hu.bme.mit.theta.common.visualization.LineStyle;
 import hu.bme.mit.theta.common.visualization.NodeAttributes;
 
-public final class ArgVisualizer<S extends State, A extends Action> {
+public final class ArgVisualizer<S extends State, A extends Action> implements WitnessVisualizer<ARG<? extends S, ? extends A>> {
 
     private static final LineStyle COVER_EDGE_STYLE = LineStyle.DASHED;
     private static final LineStyle SUCC_EDGE_STYLE = LineStyle.NORMAL;
@@ -53,8 +53,8 @@ public final class ArgVisualizer<S extends State, A extends Action> {
 
     private static class LazyHolderDefault {
 
-        static final ArgVisualizer<State, Action> INSTANCE = new ArgVisualizer<>(s -> s.toString(),
-                a -> a.toString());
+        static final ArgVisualizer<State, Action> INSTANCE = new ArgVisualizer<>(Object::toString,
+                Object::toString);
     }
 
     private static class LazyHolderStructureOnly {
@@ -81,6 +81,7 @@ public static ArgVisualizer<State, Action> getStructureOnly() {
         return LazyHolderStructureOnly.INSTANCE;
     }
 
+    @Override
     public Graph visualize(final ARG<? extends S, ? extends A> arg) {
         final Graph graph = new Graph(ARG_ID, ARG_LABEL);
 
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/WitnessVisualizer.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/WitnessVisualizer.java
new file mode 100644
index 0000000000..bd1a9d8234
--- /dev/null
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/WitnessVisualizer.java
@@ -0,0 +1,26 @@
+/*
+ *  Copyright 2024 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.analysis.utils;
+
+import hu.bme.mit.theta.analysis.algorithm.Witness;
+import hu.bme.mit.theta.common.visualization.Graph;
+
+public interface WitnessVisualizer<W extends Witness> {
+
+    Graph visualize(W witness);
+
+}
diff --git a/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/config/StmtMultiConfigBuilder.kt b/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/config/StmtMultiConfigBuilder.kt
index 2e7f57a91a..e0d8173455 100644
--- a/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/config/StmtMultiConfigBuilder.kt
+++ b/subprojects/common/analysis/src/main/kotlin/hu/bme/mit/theta/analysis/multi/config/StmtMultiConfigBuilder.kt
@@ -13,13 +13,12 @@
  *  See the License for the specific language governing permissions and
  *  limitations under the License.
  */
-
 package hu.bme.mit.theta.analysis.multi.config
 
 import hu.bme.mit.theta.analysis.Prec
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder
-import hu.bme.mit.theta.analysis.algorithm.cegar.BasicAbstractor
-import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgCegarChecker
+import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor
 import hu.bme.mit.theta.analysis.expr.ExprState
 import hu.bme.mit.theta.analysis.expr.StmtAction
 import hu.bme.mit.theta.analysis.expr.refinement.*
@@ -39,117 +38,264 @@ import hu.bme.mit.theta.solver.SolverFactory
 import hu.bme.mit.theta.solver.UCSolver
 import java.util.function.Predicate
 
-sealed class StmtMultiConfigBuilder<LState : ExprState, RState : ExprState, DataState : ExprState, LControl : ExprState, RControl : ExprState, LAction : StmtAction, RAction : StmtAction, R : Refutation, LPrec : Prec, RPrec : Prec, DataPrec : Prec, LControlPrec : Prec, RControlPrec : Prec>(
-    private val product: MultiBuilderResultPOJO<LState, RState, DataState, LControl, RControl, LAction, RAction, LPrec, RPrec, DataPrec, LControlPrec, RControlPrec, ExprMultiState<LControl, RControl, DataState>, ExprMultiState<LControl, RControl, UnitState>, StmtMultiAction<LAction, RAction>, StmtMultiLts<LState, RState, DataState, LControl, RControl, LAction, RAction>>,
-    val prop: Expr<BoolType>,
-    val target: Predicate<ExprMultiState<LControl, RControl, DataState>>,
-    private val lRefToPrec: RefutationToPrec<LPrec, R>,
-    private val rRefToPrec: RefutationToPrec<RPrec, R>,
-    private val dRefToPrec: RefutationToPrec<DataPrec, R>,
-    private val lInitPrec: LPrec,
-    private val rInitPrec: RPrec,
-    private val dInitPrec: DataPrec,
-    val solverFactory: SolverFactory,
-    val logger: Logger,
-    val pruneStrategy: PruneStrategy = PruneStrategy.FULL
+sealed class StmtMultiConfigBuilder<
+  LState : ExprState,
+  RState : ExprState,
+  DataState : ExprState,
+  LControl : ExprState,
+  RControl : ExprState,
+  LAction : StmtAction,
+  RAction : StmtAction,
+  R : Refutation,
+  LPrec : Prec,
+  RPrec : Prec,
+  DataPrec : Prec,
+  LControlPrec : Prec,
+  RControlPrec : Prec,
+>(
+  private val product:
+    MultiBuilderResultPOJO<
+      LState,
+      RState,
+      DataState,
+      LControl,
+      RControl,
+      LAction,
+      RAction,
+      LPrec,
+      RPrec,
+      DataPrec,
+      LControlPrec,
+      RControlPrec,
+      ExprMultiState<LControl, RControl, DataState>,
+      ExprMultiState<LControl, RControl, UnitState>,
+      StmtMultiAction<LAction, RAction>,
+      StmtMultiLts<LState, RState, DataState, LControl, RControl, LAction, RAction>,
+    >,
+  val prop: Expr<BoolType>,
+  val target: Predicate<ExprMultiState<LControl, RControl, DataState>>,
+  private val lRefToPrec: RefutationToPrec<LPrec, R>,
+  private val rRefToPrec: RefutationToPrec<RPrec, R>,
+  private val dRefToPrec: RefutationToPrec<DataPrec, R>,
+  private val lInitPrec: LPrec,
+  private val rInitPrec: RPrec,
+  private val dInitPrec: DataPrec,
+  val solverFactory: SolverFactory,
+  val logger: Logger,
+  val pruneStrategy: PruneStrategy = PruneStrategy.FULL,
 ) {
 
-    abstract fun getTraceChecker(): ExprTraceChecker<R>
+  abstract fun getTraceChecker(): ExprTraceChecker<R>
 
-    fun build(): MultiConfig<DataState, LControl, RControl, LAction, RAction, LPrec, RPrec, DataPrec, ExprMultiState<LControl, RControl, DataState>, StmtMultiAction<LAction, RAction>> {
-        val argBuilder = ArgBuilder.create(product.lts, product.side.analysis, target)
-        val abstractor = BasicAbstractor.builder(argBuilder).build()
-        val traceChecker = getTraceChecker()
-        val precRefiner =
-            JoiningPrecRefiner.create<ExprMultiState<LControl, RControl, DataState>, StmtMultiAction<LAction, RAction>, MultiPrec<LPrec, RPrec, DataPrec>, R>(
-                RefToMultiPrec(lRefToPrec, rRefToPrec, dRefToPrec)
-            )
-        val refiner = SingleExprTraceRefiner.create(traceChecker, precRefiner, pruneStrategy, logger)
-        return MultiConfig(CegarChecker.create(abstractor, refiner), MultiPrec(lInitPrec, rInitPrec, dInitPrec))
-    }
+  fun build():
+    MultiConfig<
+      DataState,
+      LControl,
+      RControl,
+      LAction,
+      RAction,
+      LPrec,
+      RPrec,
+      DataPrec,
+      ExprMultiState<LControl, RControl, DataState>,
+      StmtMultiAction<LAction, RAction>,
+    > {
+    val argBuilder = ArgBuilder.create(product.lts, product.side.analysis, target)
+    val abstractor = BasicArgAbstractor.builder(argBuilder).build()
+    val traceChecker = getTraceChecker()
+    val precRefiner =
+      JoiningPrecRefiner.create<
+        ExprMultiState<LControl, RControl, DataState>,
+        StmtMultiAction<LAction, RAction>,
+        MultiPrec<LPrec, RPrec, DataPrec>,
+        R,
+      >(
+        RefToMultiPrec(lRefToPrec, rRefToPrec, dRefToPrec)
+      )
+    val refiner = SingleExprTraceRefiner.create(traceChecker, precRefiner, pruneStrategy, logger)
+    return MultiConfig(
+      ArgCegarChecker.create(abstractor, refiner),
+      MultiPrec(lInitPrec, rInitPrec, dInitPrec),
+    )
+  }
 
-    class ItpStmtMultiConfigBuilder<LState : ExprState, RState : ExprState, DataState : ExprState, LControl : ExprState, RControl : ExprState, LAction : StmtAction, RAction : StmtAction, LPrec : Prec, RPrec : Prec, DataPrec : Prec, LControlPrec : Prec, RControlPrec : Prec>(
-        product: MultiBuilderResultPOJO<LState, RState, DataState, LControl, RControl, LAction, RAction, LPrec, RPrec, DataPrec, LControlPrec, RControlPrec, ExprMultiState<LControl, RControl, DataState>, ExprMultiState<LControl, RControl, UnitState>, StmtMultiAction<LAction, RAction>, StmtMultiLts<LState, RState, DataState, LControl, RControl, LAction, RAction>>,
-        prop: Expr<BoolType>,
-        target: Predicate<ExprMultiState<LControl, RControl, DataState>>,
-        lRefToPrec: RefutationToPrec<LPrec, ItpRefutation>,
-        rRefToPrec: RefutationToPrec<RPrec, ItpRefutation>,
-        dRefToPrec: RefutationToPrec<DataPrec, ItpRefutation>,
-        lInitPrec: LPrec,
-        rInitPrec: RPrec,
-        dInitPrec: DataPrec,
-        solverFactory: SolverFactory,
-        logger: Logger,
-        pruneStrategy: PruneStrategy = PruneStrategy.FULL,
-        private val traceCheckerType: TraceCheckerType = TraceCheckerType.SEQ_ITP
-    ) : StmtMultiConfigBuilder<LState, RState, DataState, LControl, RControl, LAction, RAction, ItpRefutation, LPrec, RPrec, DataPrec, LControlPrec, RControlPrec>(
-        product,
-        prop,
-        target,
-        lRefToPrec,
-        rRefToPrec,
-        dRefToPrec,
-        lInitPrec,
-        rInitPrec,
-        dInitPrec,
-        solverFactory,
-        logger,
-        pruneStrategy
+  class ItpStmtMultiConfigBuilder<
+    LState : ExprState,
+    RState : ExprState,
+    DataState : ExprState,
+    LControl : ExprState,
+    RControl : ExprState,
+    LAction : StmtAction,
+    RAction : StmtAction,
+    LPrec : Prec,
+    RPrec : Prec,
+    DataPrec : Prec,
+    LControlPrec : Prec,
+    RControlPrec : Prec,
+  >(
+    product:
+      MultiBuilderResultPOJO<
+        LState,
+        RState,
+        DataState,
+        LControl,
+        RControl,
+        LAction,
+        RAction,
+        LPrec,
+        RPrec,
+        DataPrec,
+        LControlPrec,
+        RControlPrec,
+        ExprMultiState<LControl, RControl, DataState>,
+        ExprMultiState<LControl, RControl, UnitState>,
+        StmtMultiAction<LAction, RAction>,
+        StmtMultiLts<LState, RState, DataState, LControl, RControl, LAction, RAction>,
+      >,
+    prop: Expr<BoolType>,
+    target: Predicate<ExprMultiState<LControl, RControl, DataState>>,
+    lRefToPrec: RefutationToPrec<LPrec, ItpRefutation>,
+    rRefToPrec: RefutationToPrec<RPrec, ItpRefutation>,
+    dRefToPrec: RefutationToPrec<DataPrec, ItpRefutation>,
+    lInitPrec: LPrec,
+    rInitPrec: RPrec,
+    dInitPrec: DataPrec,
+    solverFactory: SolverFactory,
+    logger: Logger,
+    pruneStrategy: PruneStrategy = PruneStrategy.FULL,
+    private val traceCheckerType: TraceCheckerType = TraceCheckerType.SEQ_ITP,
+  ) :
+    StmtMultiConfigBuilder<
+      LState,
+      RState,
+      DataState,
+      LControl,
+      RControl,
+      LAction,
+      RAction,
+      ItpRefutation,
+      LPrec,
+      RPrec,
+      DataPrec,
+      LControlPrec,
+      RControlPrec,
+    >(
+      product,
+      prop,
+      target,
+      lRefToPrec,
+      rRefToPrec,
+      dRefToPrec,
+      lInitPrec,
+      rInitPrec,
+      dInitPrec,
+      solverFactory,
+      logger,
+      pruneStrategy,
     ) {
 
-        enum class TraceCheckerType(
-            val generator: (init: Expr<BoolType>, target: Expr<BoolType>, solver: ItpSolver) -> ExprTraceChecker<ItpRefutation>
-        ) {
-
-            SEQ_ITP(ExprTraceSeqItpChecker::create), FW_BIN(ExprTraceFwBinItpChecker::create), BW_BIN(
-                ExprTraceBwBinItpChecker::create
-            )
-        }
+    enum class TraceCheckerType(
+      val generator:
+        (init: Expr<BoolType>, target: Expr<BoolType>, solver: ItpSolver) -> ExprTraceChecker<
+            ItpRefutation
+          >
+    ) {
 
-        override fun getTraceChecker(): ExprTraceChecker<ItpRefutation> = traceCheckerType.generator(
-            BoolExprs.True(), prop, solverFactory.createItpSolver()
-        )
+      SEQ_ITP(ExprTraceSeqItpChecker::create),
+      FW_BIN(ExprTraceFwBinItpChecker::create),
+      BW_BIN(ExprTraceBwBinItpChecker::create),
     }
 
-    class VarsStmtMultiConfigBuilder<LState : ExprState, RState : ExprState, DataState : ExprState, LControl : ExprState, RControl : ExprState, LAction : StmtAction, RAction : StmtAction, LPrec : Prec, RPrec : Prec, DataPrec : Prec, LControlPrec : Prec, RControlPrec : Prec>(
-        product: MultiBuilderResultPOJO<LState, RState, DataState, LControl, RControl, LAction, RAction, LPrec, RPrec, DataPrec, LControlPrec, RControlPrec, ExprMultiState<LControl, RControl, DataState>, ExprMultiState<LControl, RControl, UnitState>, StmtMultiAction<LAction, RAction>, StmtMultiLts<LState, RState, DataState, LControl, RControl, LAction, RAction>>,
-        prop: Expr<BoolType>,
-        target: Predicate<ExprMultiState<LControl, RControl, DataState>>,
-        lRefToPrec: RefutationToPrec<LPrec, VarsRefutation>,
-        rRefToPrec: RefutationToPrec<RPrec, VarsRefutation>,
-        dRefToPrec: RefutationToPrec<DataPrec, VarsRefutation>,
-        lInitPrec: LPrec,
-        rInitPrec: RPrec,
-        dInitPrec: DataPrec,
-        solverFactory: SolverFactory,
-        logger: Logger,
-        pruneStrategy: PruneStrategy = PruneStrategy.FULL,
-        private val traceCheckerType: TraceCheckerType = TraceCheckerType.UNSAT_CORE
-    ) : StmtMultiConfigBuilder<LState, RState, DataState, LControl, RControl, LAction, RAction, VarsRefutation, LPrec, RPrec, DataPrec, LControlPrec, RControlPrec>(
-        product,
-        prop,
-        target,
-        lRefToPrec,
-        rRefToPrec,
-        dRefToPrec,
-        lInitPrec,
-        rInitPrec,
-        dInitPrec,
-        solverFactory,
-        logger,
-        pruneStrategy
-    ) {
+    override fun getTraceChecker(): ExprTraceChecker<ItpRefutation> =
+      traceCheckerType.generator(BoolExprs.True(), prop, solverFactory.createItpSolver())
+  }
 
-        enum class TraceCheckerType(
-            val generator: (init: Expr<BoolType>, target: Expr<BoolType>, solver: UCSolver) -> ExprTraceChecker<VarsRefutation>
-        ) {
+  class VarsStmtMultiConfigBuilder<
+    LState : ExprState,
+    RState : ExprState,
+    DataState : ExprState,
+    LControl : ExprState,
+    RControl : ExprState,
+    LAction : StmtAction,
+    RAction : StmtAction,
+    LPrec : Prec,
+    RPrec : Prec,
+    DataPrec : Prec,
+    LControlPrec : Prec,
+    RControlPrec : Prec,
+  >(
+    product:
+      MultiBuilderResultPOJO<
+        LState,
+        RState,
+        DataState,
+        LControl,
+        RControl,
+        LAction,
+        RAction,
+        LPrec,
+        RPrec,
+        DataPrec,
+        LControlPrec,
+        RControlPrec,
+        ExprMultiState<LControl, RControl, DataState>,
+        ExprMultiState<LControl, RControl, UnitState>,
+        StmtMultiAction<LAction, RAction>,
+        StmtMultiLts<LState, RState, DataState, LControl, RControl, LAction, RAction>,
+      >,
+    prop: Expr<BoolType>,
+    target: Predicate<ExprMultiState<LControl, RControl, DataState>>,
+    lRefToPrec: RefutationToPrec<LPrec, VarsRefutation>,
+    rRefToPrec: RefutationToPrec<RPrec, VarsRefutation>,
+    dRefToPrec: RefutationToPrec<DataPrec, VarsRefutation>,
+    lInitPrec: LPrec,
+    rInitPrec: RPrec,
+    dInitPrec: DataPrec,
+    solverFactory: SolverFactory,
+    logger: Logger,
+    pruneStrategy: PruneStrategy = PruneStrategy.FULL,
+    private val traceCheckerType: TraceCheckerType = TraceCheckerType.UNSAT_CORE,
+  ) :
+    StmtMultiConfigBuilder<
+      LState,
+      RState,
+      DataState,
+      LControl,
+      RControl,
+      LAction,
+      RAction,
+      VarsRefutation,
+      LPrec,
+      RPrec,
+      DataPrec,
+      LControlPrec,
+      RControlPrec,
+    >(
+      product,
+      prop,
+      target,
+      lRefToPrec,
+      rRefToPrec,
+      dRefToPrec,
+      lInitPrec,
+      rInitPrec,
+      dInitPrec,
+      solverFactory,
+      logger,
+      pruneStrategy,
+    ) {
 
-            UNSAT_CORE(ExprTraceUnsatCoreChecker::create)
-        }
+    enum class TraceCheckerType(
+      val generator:
+        (init: Expr<BoolType>, target: Expr<BoolType>, solver: UCSolver) -> ExprTraceChecker<
+            VarsRefutation
+          >
+    ) {
 
-        override fun getTraceChecker(): ExprTraceChecker<VarsRefutation> = traceCheckerType.generator(
-            BoolExprs.True(), prop, solverFactory.createUCSolver()
-        )
+      UNSAT_CORE(ExprTraceUnsatCoreChecker::create)
     }
 
+    override fun getTraceChecker(): ExprTraceChecker<VarsRefutation> =
+      traceCheckerType.generator(BoolExprs.True(), prop, solverFactory.createUCSolver())
+  }
 }
diff --git a/subprojects/sts/sts-analysis/src/main/java/hu/bme/mit/theta/sts/analysis/config/StsConfigBuilder.java b/subprojects/sts/sts-analysis/src/main/java/hu/bme/mit/theta/sts/analysis/config/StsConfigBuilder.java
index 397a4a4ef8..7e946253e9 100644
--- a/subprojects/sts/sts-analysis/src/main/java/hu/bme/mit/theta/sts/analysis/config/StsConfigBuilder.java
+++ b/subprojects/sts/sts-analysis/src/main/java/hu/bme/mit/theta/sts/analysis/config/StsConfigBuilder.java
@@ -15,16 +15,18 @@
  */
 package hu.bme.mit.theta.sts.analysis.config;
 
+import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Not;
+
 import hu.bme.mit.theta.analysis.*;
+import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
 import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder;
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgNodeComparators;
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgNodeComparators.ArgNodeComparator;
-import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
-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.CegarChecker;
-import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner;
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgAbstractor;
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgCegarChecker;
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgRefiner;
+import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor;
 import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterions;
 import hu.bme.mit.theta.analysis.expl.ExplAnalysis;
 import hu.bme.mit.theta.analysis.expl.ExplPrec;
@@ -66,19 +68,23 @@
 import hu.bme.mit.theta.sts.analysis.initprec.StsEmptyInitPrec;
 import hu.bme.mit.theta.sts.analysis.initprec.StsInitPrec;
 import hu.bme.mit.theta.sts.analysis.initprec.StsPropInitPrec;
-
 import java.util.function.Predicate;
 
-import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Not;
-
 public final class StsConfigBuilder {
 
     public enum Domain {
-        EXPL, PRED_BOOL, PRED_CART, PRED_SPLIT
+        EXPL,
+        PRED_BOOL,
+        PRED_CART,
+        PRED_SPLIT
     }
 
     public enum Refinement {
-        FW_BIN_ITP, BW_BIN_ITP, SEQ_ITP, MULTI_SEQ, UNSAT_CORE
+        FW_BIN_ITP,
+        BW_BIN_ITP,
+        SEQ_ITP,
+        MULTI_SEQ,
+        UNSAT_CORE
     }
 
     public enum Search {
@@ -91,7 +97,6 @@ public enum Search {
         private Search(final ArgNodeComparator comparator) {
             this.comparator = comparator;
         }
-
     }
 
     public enum PredSplit {
@@ -109,14 +114,14 @@ private PredSplit(final ExprSplitter splitter) {
     }
 
     public enum InitPrec {
-        EMPTY(new StsEmptyInitPrec()), PROP(new StsPropInitPrec());
+        EMPTY(new StsEmptyInitPrec()),
+        PROP(new StsPropInitPrec());
 
         public final StsInitPrec builder;
 
         private InitPrec(final StsInitPrec builder) {
             this.builder = builder;
         }
-
     }
 
     private Logger logger = NullLogger.getInstance();
@@ -128,8 +133,8 @@ private InitPrec(final StsInitPrec builder) {
     private InitPrec initPrec = InitPrec.EMPTY;
     private PruneStrategy pruneStrategy = PruneStrategy.LAZY;
 
-    public StsConfigBuilder(final Domain domain, final Refinement refinement,
-                            final SolverFactory solverFactory) {
+    public StsConfigBuilder(
+            final Domain domain, final Refinement refinement, final SolverFactory solverFactory) {
         this.domain = domain;
         this.refinement = refinement;
         this.solverFactory = solverFactory;
@@ -168,63 +173,80 @@ public StsConfigBuilder pruneStrategy(final PruneStrategy pruneStrategy) {
         if (domain == Domain.EXPL) {
             final Solver analysisSolver = solverFactory.createSolver();
             final Predicate<ExplState> target = new ExplStatePredicate(negProp, analysisSolver);
-            final Analysis<ExplState, ExprAction, ExplPrec> analysis = ExplAnalysis.create(
-                    analysisSolver, init);
-            final ArgBuilder<ExplState, StsAction, ExplPrec> argBuilder = ArgBuilder.create(lts,
-                    analysis, target,
-                    true);
-            final Abstractor<ExplState, StsAction, ExplPrec> abstractor = BasicAbstractor.builder(
-                            argBuilder)
-                    .waitlist(PriorityWaitlist.create(search.comparator))
-                    .stopCriterion(refinement == Refinement.MULTI_SEQ ? StopCriterions.fullExploration()
-                            : StopCriterions.firstCex())
-                    .logger(logger).build();
-
-            Refiner<ExplState, StsAction, ExplPrec> refiner = null;
+            final Analysis<ExplState, ExprAction, ExplPrec> analysis =
+                    ExplAnalysis.create(analysisSolver, init);
+            final ArgBuilder<ExplState, StsAction, ExplPrec> argBuilder =
+                    ArgBuilder.create(lts, analysis, target, true);
+            final ArgAbstractor<ExplState, StsAction, ExplPrec> abstractor =
+                    BasicArgAbstractor.builder(argBuilder)
+                            .waitlist(PriorityWaitlist.create(search.comparator))
+                            .stopCriterion(
+                                    refinement == Refinement.MULTI_SEQ
+                                            ? StopCriterions.fullExploration()
+                                            : StopCriterions.firstCex())
+                            .logger(logger)
+                            .build();
+
+            ArgRefiner<ExplState, StsAction, ExplPrec> refiner = null;
 
             switch (refinement) {
                 case FW_BIN_ITP:
-                    refiner = SingleExprTraceRefiner.create(
-                            ExprTraceFwBinItpChecker.create(init, negProp,
-                                    solverFactory.createItpSolver()),
-                            JoiningPrecRefiner.create(new ItpRefToExplPrec()), pruneStrategy, logger);
+                    refiner =
+                            SingleExprTraceRefiner.create(
+                                    ExprTraceFwBinItpChecker.create(
+                                            init, negProp, solverFactory.createItpSolver()),
+                                    JoiningPrecRefiner.create(new ItpRefToExplPrec()),
+                                    pruneStrategy,
+                                    logger);
                     break;
                 case BW_BIN_ITP:
-                    refiner = SingleExprTraceRefiner.create(
-                            ExprTraceBwBinItpChecker.create(init, negProp,
-                                    solverFactory.createItpSolver()),
-                            JoiningPrecRefiner.create(new ItpRefToExplPrec()), pruneStrategy, logger);
+                    refiner =
+                            SingleExprTraceRefiner.create(
+                                    ExprTraceBwBinItpChecker.create(
+                                            init, negProp, solverFactory.createItpSolver()),
+                                    JoiningPrecRefiner.create(new ItpRefToExplPrec()),
+                                    pruneStrategy,
+                                    logger);
                     break;
                 case SEQ_ITP:
-                    refiner = SingleExprTraceRefiner.create(
-                            ExprTraceSeqItpChecker.create(init, negProp,
-                                    solverFactory.createItpSolver()),
-                            JoiningPrecRefiner.create(new ItpRefToExplPrec()), pruneStrategy, logger);
+                    refiner =
+                            SingleExprTraceRefiner.create(
+                                    ExprTraceSeqItpChecker.create(
+                                            init, negProp, solverFactory.createItpSolver()),
+                                    JoiningPrecRefiner.create(new ItpRefToExplPrec()),
+                                    pruneStrategy,
+                                    logger);
                     break;
                 case MULTI_SEQ:
-                    refiner = MultiExprTraceRefiner.create(
-                            ExprTraceSeqItpChecker.create(init, negProp,
-                                    solverFactory.createItpSolver()),
-                            JoiningPrecRefiner.create(new ItpRefToExplPrec()), pruneStrategy, logger);
+                    refiner =
+                            MultiExprTraceRefiner.create(
+                                    ExprTraceSeqItpChecker.create(
+                                            init, negProp, solverFactory.createItpSolver()),
+                                    JoiningPrecRefiner.create(new ItpRefToExplPrec()),
+                                    pruneStrategy,
+                                    logger);
                     break;
                 case UNSAT_CORE:
-                    refiner = SingleExprTraceRefiner.create(
-                            ExprTraceUnsatCoreChecker.create(init, negProp,
-                                    solverFactory.createUCSolver()),
-                            JoiningPrecRefiner.create(new VarsRefToExplPrec()), pruneStrategy, logger);
+                    refiner =
+                            SingleExprTraceRefiner.create(
+                                    ExprTraceUnsatCoreChecker.create(
+                                            init, negProp, solverFactory.createUCSolver()),
+                                    JoiningPrecRefiner.create(new VarsRefToExplPrec()),
+                                    pruneStrategy,
+                                    logger);
                     break;
                 default:
                     throw new UnsupportedOperationException(
                             domain + " domain does not support " + refinement + " refinement.");
             }
 
-            final SafetyChecker<ARG<ExplState, StsAction>, Trace<ExplState, StsAction>, ExplPrec> checker = CegarChecker.create(
-                    abstractor, refiner,
-                    logger);
+            final SafetyChecker<ARG<ExplState, StsAction>, Trace<ExplState, StsAction>, ExplPrec>
+                    checker = ArgCegarChecker.create(abstractor, refiner, logger);
             final ExplPrec prec = initPrec.builder.createExpl(sts);
             return StsConfig.create(checker, prec);
 
-        } else if (domain == Domain.PRED_BOOL || domain == Domain.PRED_CART
+        } else if (domain == Domain.PRED_BOOL
+                || domain == Domain.PRED_CART
                 || domain == Domain.PRED_SPLIT) {
             final Solver analysisSolver = solverFactory.createSolver();
             PredAbstractor predAbstractor = null;
@@ -242,55 +264,65 @@ public StsConfigBuilder pruneStrategy(final PruneStrategy pruneStrategy) {
                     throw new UnsupportedOperationException(domain + " domain is not supported.");
             }
             final Predicate<ExprState> target = new ExprStatePredicate(negProp, analysisSolver);
-            final Analysis<PredState, ExprAction, PredPrec> analysis = PredAnalysis.create(
-                    analysisSolver, predAbstractor,
-                    init);
-            final ArgBuilder<PredState, StsAction, PredPrec> argBuilder = ArgBuilder.create(lts,
-                    analysis, target,
-                    true);
-            final Abstractor<PredState, StsAction, PredPrec> abstractor = BasicAbstractor.builder(
-                            argBuilder)
-                    .waitlist(PriorityWaitlist.create(search.comparator))
-                    .stopCriterion(refinement == Refinement.MULTI_SEQ ? StopCriterions.fullExploration()
-                            : StopCriterions.firstCex())
-                    .logger(logger).build();
+            final Analysis<PredState, ExprAction, PredPrec> analysis =
+                    PredAnalysis.create(analysisSolver, predAbstractor, init);
+            final ArgBuilder<PredState, StsAction, PredPrec> argBuilder =
+                    ArgBuilder.create(lts, analysis, target, true);
+            final ArgAbstractor<PredState, StsAction, PredPrec> abstractor =
+                    BasicArgAbstractor.builder(argBuilder)
+                            .waitlist(PriorityWaitlist.create(search.comparator))
+                            .stopCriterion(
+                                    refinement == Refinement.MULTI_SEQ
+                                            ? StopCriterions.fullExploration()
+                                            : StopCriterions.firstCex())
+                            .logger(logger)
+                            .build();
 
             ExprTraceChecker<ItpRefutation> exprTraceChecker = null;
             switch (refinement) {
                 case FW_BIN_ITP:
-                    exprTraceChecker = ExprTraceFwBinItpChecker.create(init, negProp,
-                            solverFactory.createItpSolver());
+                    exprTraceChecker =
+                            ExprTraceFwBinItpChecker.create(
+                                    init, negProp, solverFactory.createItpSolver());
                     break;
                 case BW_BIN_ITP:
-                    exprTraceChecker = ExprTraceBwBinItpChecker.create(init, negProp,
-                            solverFactory.createItpSolver());
+                    exprTraceChecker =
+                            ExprTraceBwBinItpChecker.create(
+                                    init, negProp, solverFactory.createItpSolver());
                     break;
                 case SEQ_ITP:
-                    exprTraceChecker = ExprTraceSeqItpChecker.create(init, negProp,
-                            solverFactory.createItpSolver());
+                    exprTraceChecker =
+                            ExprTraceSeqItpChecker.create(
+                                    init, negProp, solverFactory.createItpSolver());
                     break;
                 case MULTI_SEQ:
-                    exprTraceChecker = ExprTraceSeqItpChecker.create(init, negProp,
-                            solverFactory.createItpSolver());
+                    exprTraceChecker =
+                            ExprTraceSeqItpChecker.create(
+                                    init, negProp, solverFactory.createItpSolver());
                     break;
                 default:
                     throw new UnsupportedOperationException(
                             domain + " domain does not support " + refinement + " refinement.");
             }
-            Refiner<PredState, StsAction, PredPrec> refiner;
+            ArgRefiner<PredState, StsAction, PredPrec> refiner;
             if (refinement == Refinement.MULTI_SEQ) {
-                refiner = MultiExprTraceRefiner.create(exprTraceChecker,
-                        JoiningPrecRefiner.create(new ItpRefToPredPrec(predSplit.splitter)),
-                        pruneStrategy, logger);
+                refiner =
+                        MultiExprTraceRefiner.create(
+                                exprTraceChecker,
+                                JoiningPrecRefiner.create(new ItpRefToPredPrec(predSplit.splitter)),
+                                pruneStrategy,
+                                logger);
             } else {
-                refiner = SingleExprTraceRefiner.create(exprTraceChecker,
-                        JoiningPrecRefiner.create(new ItpRefToPredPrec(predSplit.splitter)),
-                        pruneStrategy, logger);
+                refiner =
+                        SingleExprTraceRefiner.create(
+                                exprTraceChecker,
+                                JoiningPrecRefiner.create(new ItpRefToPredPrec(predSplit.splitter)),
+                                pruneStrategy,
+                                logger);
             }
 
-            final SafetyChecker<ARG<PredState, StsAction>, Trace<PredState, StsAction>, PredPrec> checker = CegarChecker.create(
-                    abstractor, refiner,
-                    logger);
+            final SafetyChecker<ARG<PredState, StsAction>, Trace<PredState, StsAction>, PredPrec>
+                    checker = ArgCegarChecker.create(abstractor, refiner, logger);
 
             final PredPrec prec = initPrec.builder.createPred(sts);
             return StsConfig.create(checker, prec);
diff --git a/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsExplTest.java b/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsExplTest.java
index db171f2718..4f2f998af5 100644
--- a/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsExplTest.java
+++ b/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsExplTest.java
@@ -24,9 +24,9 @@
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder;
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgNodeComparators;
 import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
-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.CegarChecker;
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgAbstractor;
+import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor;
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgCegarChecker;
 import hu.bme.mit.theta.analysis.expl.ExplAnalysis;
 import hu.bme.mit.theta.analysis.expl.ExplPrec;
 import hu.bme.mit.theta.analysis.expl.ExplState;
@@ -110,7 +110,7 @@ public void test() {
         final ArgBuilder<ExplState, StsAction, ExplPrec> argBuilder = ArgBuilder.create(lts,
                 analysis, target);
 
-        final Abstractor<ExplState, StsAction, ExplPrec> abstractor = BasicAbstractor.builder(
+        final ArgAbstractor<ExplState, StsAction, ExplPrec> abstractor = BasicArgAbstractor.builder(
                         argBuilder)
                 .waitlist(PriorityWaitlist.create(ArgNodeComparators.bfs())).logger(logger).build();
 
@@ -122,7 +122,7 @@ public void test() {
                 .create(exprTraceChecker, JoiningPrecRefiner.create(new VarsRefToExplPrec()),
                         PruneStrategy.LAZY, logger);
 
-        final SafetyChecker<ARG<ExplState, StsAction>, Trace<ExplState, StsAction>, ExplPrec> checker = CegarChecker.create(
+        final SafetyChecker<ARG<ExplState, StsAction>, Trace<ExplState, StsAction>, ExplPrec> checker = ArgCegarChecker.create(
                 abstractor, refiner, logger);
 
         final SafetyResult<ARG<ExplState, StsAction>, Trace<ExplState, StsAction>> safetyStatus = checker.check(prec);
diff --git a/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsPredTest.java b/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsPredTest.java
index 5eea722540..bed9497f54 100644
--- a/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsPredTest.java
+++ b/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsPredTest.java
@@ -44,9 +44,9 @@
 import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder;
 import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
-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.CegarChecker;
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgAbstractor;
+import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor;
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgCegarChecker;
 import hu.bme.mit.theta.analysis.expr.ExprAction;
 import hu.bme.mit.theta.analysis.expr.ExprState;
 import hu.bme.mit.theta.analysis.expr.ExprStatePredicate;
@@ -104,7 +104,7 @@ public void testPredPrec() {
         final ArgBuilder<PredState, StsAction, PredPrec> argBuilder = ArgBuilder.create(lts,
                 analysis, target);
 
-        final Abstractor<PredState, StsAction, PredPrec> abstractor = BasicAbstractor.builder(
+        final ArgAbstractor<PredState, StsAction, PredPrec> abstractor = BasicArgAbstractor.builder(
                         argBuilder).logger(logger)
                 .build();
 
@@ -117,7 +117,7 @@ public void testPredPrec() {
                         JoiningPrecRefiner.create(new ItpRefToPredPrec(ExprSplitters.atoms())),
                         PruneStrategy.LAZY, logger);
 
-        final SafetyChecker<ARG<PredState, StsAction>, Trace<PredState, StsAction>, PredPrec> checker = CegarChecker.create(
+        final SafetyChecker<ARG<PredState, StsAction>, Trace<PredState, StsAction>, PredPrec> checker = ArgCegarChecker.create(
                 abstractor, refiner, logger);
 
         final SafetyResult<ARG<PredState, StsAction>, Trace<PredState, StsAction>> safetyStatus = checker.check(prec);
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
deleted file mode 100644
index d17f15fda1..0000000000
--- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAbstractor.kt
+++ /dev/null
@@ -1,137 +0,0 @@
-/*
- *  Copyright 2024 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.ARG
-import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder
-import hu.bme.mit.theta.analysis.algorithm.arg.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 64bd2e3d62..f923d0e6f0 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
@@ -13,13 +13,12 @@
  *  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.*
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode
-import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgAbstractor
 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
@@ -54,251 +53,364 @@ import java.util.*
 import java.util.function.Predicate
 
 open class XcfaAnalysis<S : ExprState, P : Prec>(
-    private val corePartialOrd: PartialOrd<XcfaState<PtrState<S>>>,
-    private val coreInitFunc: InitFunc<XcfaState<PtrState<S>>, XcfaPrec<P>>,
-    private var coreTransFunc: TransFunc<XcfaState<PtrState<S>>, XcfaAction, XcfaPrec<P>>,
+  private val corePartialOrd: PartialOrd<XcfaState<PtrState<S>>>,
+  private val coreInitFunc: InitFunc<XcfaState<PtrState<S>>, XcfaPrec<P>>,
+  private var coreTransFunc: TransFunc<XcfaState<PtrState<S>>, XcfaAction, XcfaPrec<P>>,
 ) : Analysis<XcfaState<PtrState<S>>, XcfaAction, XcfaPrec<P>> {
 
-    init {
-        ConeOfInfluence.coreTransFunc = transFunc as TransFunc<XcfaState<out PtrState<out ExprState>>, XcfaAction, XcfaPrec<out Prec>>
-        coreTransFunc = ConeOfInfluence.transFunc as TransFunc<XcfaState<PtrState<S>>, XcfaAction, XcfaPrec<P>>
-    }
+  init {
+    ConeOfInfluence.coreTransFunc =
+      transFunc as TransFunc<XcfaState<out PtrState<out ExprState>>, XcfaAction, XcfaPrec<out Prec>>
+    coreTransFunc =
+      ConeOfInfluence.transFunc as TransFunc<XcfaState<PtrState<S>>, XcfaAction, XcfaPrec<P>>
+  }
+
+  override fun getPartialOrd(): PartialOrd<XcfaState<PtrState<S>>> = corePartialOrd
+
+  override fun getInitFunc(): InitFunc<XcfaState<PtrState<S>>, XcfaPrec<P>> = coreInitFunc
 
-    override fun getPartialOrd(): PartialOrd<XcfaState<PtrState<S>>> = corePartialOrd
-    override fun getInitFunc(): InitFunc<XcfaState<PtrState<S>>, XcfaPrec<P>> = coreInitFunc
-    override fun getTransFunc(): TransFunc<XcfaState<PtrState<S>>, XcfaAction, XcfaPrec<P>> = coreTransFunc
+  override fun getTransFunc(): TransFunc<XcfaState<PtrState<S>>, XcfaAction, XcfaPrec<P>> =
+    coreTransFunc
 }
 
 /// Common
 private var tempCnt: Int = 0
-fun getCoreXcfaLts() = LTS<XcfaState<out PtrState<out ExprState>>, XcfaAction> { s ->
-    s.processes.map { proc ->
+
+fun getCoreXcfaLts() =
+  LTS<XcfaState<out PtrState<out ExprState>>, XcfaAction> { s ->
+    s.processes
+      .map { proc ->
         if (proc.value.locs.peek().final) {
-            listOf(XcfaAction(proc.key,
-                XcfaEdge(proc.value.locs.peek(), proc.value.locs.peek(), SequenceLabel(listOf(
+          listOf(
+            XcfaAction(
+              proc.key,
+              XcfaEdge(
+                proc.value.locs.peek(),
+                proc.value.locs.peek(),
+                SequenceLabel(
+                  listOf(
                     proc.value.paramStmts.peek().second,
                     ReturnLabel(proc.value.returnStmts.peek()),
-                ))), nextCnt = s.sGlobal.nextCnt))
+                  )
+                ),
+              ),
+              nextCnt = s.sGlobal.nextCnt,
+            )
+          )
         } else if (!proc.value.paramsInitialized) {
-            listOf(XcfaAction(proc.key, XcfaEdge(proc.value.locs.peek(), proc.value.locs.peek(),
-                proc.value.paramStmts.peek().first), nextCnt = s.sGlobal.nextCnt))
+          listOf(
+            XcfaAction(
+              proc.key,
+              XcfaEdge(
+                proc.value.locs.peek(),
+                proc.value.locs.peek(),
+                proc.value.paramStmts.peek().first,
+              ),
+              nextCnt = s.sGlobal.nextCnt,
+            )
+          )
         } else {
-            proc.value.locs.peek().outgoingEdges.map { edge ->
-                val newLabel = edge.label.changeVars(proc.value.varLookup.peek())
-                val flatLabels = newLabel.getFlatLabels()
-                if (flatLabels.any { it is InvokeLabel || it is StartLabel }) {
-                    val newNewLabel = SequenceLabel(flatLabels.map { label ->
-                        if (label is InvokeLabel) {
-                            val procedure = s.xcfa?.procedures?.find { proc -> proc.name == label.name }
-                                ?: error("No such method ${label.name}.")
-                            val lookup: MutableMap<VarDecl<*>, VarDecl<*>> = LinkedHashMap()
-                            SequenceLabel(listOf(procedure.params.withIndex()
-                                .filter { it.value.second != ParamDirection.OUT }.map { iVal ->
-                                    val originalVar = iVal.value.first
-                                    val tempVar = Var("tmp${tempCnt++}_" + originalVar.name,
-                                        originalVar.type)
-                                    lookup[originalVar] = tempVar
+          proc.value.locs.peek().outgoingEdges.map { edge ->
+            val newLabel = edge.label.changeVars(proc.value.varLookup.peek())
+            val flatLabels = newLabel.getFlatLabels()
+            if (flatLabels.any { it is InvokeLabel || it is StartLabel }) {
+              val newNewLabel =
+                SequenceLabel(
+                  flatLabels.map { label ->
+                    if (label is InvokeLabel) {
+                      val procedure =
+                        s.xcfa?.procedures?.find { proc -> proc.name == label.name }
+                          ?: error("No such method ${label.name}.")
+                      val lookup: MutableMap<VarDecl<*>, VarDecl<*>> = LinkedHashMap()
+                      SequenceLabel(
+                        listOf(
+                            procedure.params
+                              .withIndex()
+                              .filter { it.value.second != ParamDirection.OUT }
+                              .map { iVal ->
+                                val originalVar = iVal.value.first
+                                val tempVar =
+                                  Var("tmp${tempCnt++}_" + originalVar.name, originalVar.type)
+                                lookup[originalVar] = tempVar
+                                StmtLabel(
+                                  Stmts.Assign(
+                                    TypeUtils.cast(tempVar, tempVar.type),
+                                    TypeUtils.cast(label.params[iVal.index], tempVar.type),
+                                  ),
+                                  metadata = label.metadata,
+                                )
+                              },
+                            listOf(label.copy(tempLookup = lookup)),
+                          )
+                          .flatten()
+                      )
+                    } else if (label is StartLabel) {
+                      val procedure =
+                        s.xcfa?.procedures?.find { proc -> proc.name == label.name }
+                          ?: error("No such method ${label.name}.")
+                      val lookup: MutableMap<VarDecl<*>, VarDecl<*>> = LinkedHashMap()
+                      SequenceLabel(
+                        listOf(
+                            procedure.params
+                              .withIndex()
+                              .filter { it.value.second != ParamDirection.OUT }
+                              .mapNotNull { iVal ->
+                                val originalVar = iVal.value.first
+                                val tempVar =
+                                  Var("tmp${tempCnt++}_" + originalVar.name, originalVar.type)
+                                lookup[originalVar] = tempVar
+                                val trial =
+                                  Try.attempt {
                                     StmtLabel(
-                                        Stmts.Assign(
-                                            TypeUtils.cast(tempVar, tempVar.type),
-                                            TypeUtils.cast(label.params[iVal.index], tempVar.type)),
-                                        metadata = label.metadata)
-                                }, listOf(label.copy(tempLookup = lookup))).flatten())
-                        } else if (label is StartLabel) {
-                            val procedure = s.xcfa?.procedures?.find { proc -> proc.name == label.name }
-                                ?: error("No such method ${label.name}.")
-                            val lookup: MutableMap<VarDecl<*>, VarDecl<*>> = LinkedHashMap()
-                            SequenceLabel(listOf(procedure.params.withIndex()
-                                .filter { it.value.second != ParamDirection.OUT }.mapNotNull { iVal ->
-                                    val originalVar = iVal.value.first
-                                    val tempVar = Var("tmp${tempCnt++}_" + originalVar.name,
-                                        originalVar.type)
-                                    lookup[originalVar] = tempVar
-                                    val trial = Try.attempt {
-                                        StmtLabel(
-                                            Stmts.Assign(
-                                                TypeUtils.cast(tempVar, tempVar.type),
-                                                TypeUtils.cast(label.params[iVal.index], tempVar.type)),
-                                            metadata = label.metadata)
-                                    }
-                                    if (trial.isSuccess) {
-                                        trial.asSuccess().value
-                                    } else {
-                                        null
-                                    }
-                                }, listOf(label.copy(tempLookup = lookup))).flatten())
-                        } else label
-                    })
-                    XcfaAction(proc.key, edge.withLabel(newNewLabel), nextCnt = s.sGlobal.nextCnt)
-                } else
-                    XcfaAction(proc.key, edge.withLabel(newLabel), nextCnt = s.sGlobal.nextCnt)
-            }
+                                      Stmts.Assign(
+                                        TypeUtils.cast(tempVar, tempVar.type),
+                                        TypeUtils.cast(label.params[iVal.index], tempVar.type),
+                                      ),
+                                      metadata = label.metadata,
+                                    )
+                                  }
+                                if (trial.isSuccess) {
+                                  trial.asSuccess().value
+                                } else {
+                                  null
+                                }
+                              },
+                            listOf(label.copy(tempLookup = lookup)),
+                          )
+                          .flatten()
+                      )
+                    } else label
+                  }
+                )
+              XcfaAction(proc.key, edge.withLabel(newNewLabel), nextCnt = s.sGlobal.nextCnt)
+            } else XcfaAction(proc.key, edge.withLabel(newLabel), nextCnt = s.sGlobal.nextCnt)
+          }
         }
-    }.flatten().toSet()
-}
+      }
+      .flatten()
+      .toSet()
+  }
 
 fun getXcfaLts(): LTS<XcfaState<out PtrState<out ExprState>>, XcfaAction> {
-    val lts = getCoreXcfaLts()
-    return LTS<XcfaState<out PtrState<out ExprState>>, XcfaAction> { s ->
-        lts.getEnabledActionsFor(s).filter { !s.apply(it).first.bottom }.toSet()
-    }
+  val lts = getCoreXcfaLts()
+  return LTS<XcfaState<out PtrState<out ExprState>>, XcfaAction> { s ->
+    lts.getEnabledActionsFor(s).filter { !s.apply(it).first.bottom }.toSet()
+  }
 }
 
 enum class ErrorDetection {
-    ERROR_LOCATION,
-    DATA_RACE,
-    OVERFLOW,
-    NO_ERROR
+  ERROR_LOCATION,
+  DATA_RACE,
+  OVERFLOW,
+  NO_ERROR,
 }
 
 fun getXcfaErrorPredicate(
-    errorDetection: ErrorDetection): Predicate<XcfaState<out PtrState<out ExprState>>> = when (errorDetection) {
+  errorDetection: ErrorDetection
+): Predicate<XcfaState<out PtrState<out ExprState>>> =
+  when (errorDetection) {
     ErrorDetection.ERROR_LOCATION ->
-        Predicate<XcfaState<out PtrState<out ExprState>>> { s -> s.processes.any { it.value.locs.peek().error } }
+      Predicate<XcfaState<out PtrState<out ExprState>>> { s ->
+        s.processes.any { it.value.locs.peek().error }
+      }
 
     ErrorDetection.DATA_RACE -> {
-        Predicate<XcfaState<out PtrState<out ExprState>>> { s ->
-            val xcfa = s.xcfa!!
-            for (process1 in s.processes)
-                for (process2 in s.processes)
-                    if (process1.key != process2.key)
-                        for (edge1 in process1.value.locs.peek().outgoingEdges)
-                            for (edge2 in process2.value.locs.peek().outgoingEdges) {
-                                val mutexes1 = s.mutexes.filterValues { it == process1.key }.keys
-                                val mutexes2 = s.mutexes.filterValues { it == process2.key }.keys
-                                val globalVars1 = edge1.getGlobalVarsWithNeededMutexes(xcfa, mutexes1)
-                                val globalVars2 = edge2.getGlobalVarsWithNeededMutexes(xcfa, mutexes2)
-                                for (v1 in globalVars1)
-                                    for (v2 in globalVars2)
-                                        if (v1.varDecl == v2.varDecl)
-                                            if (v1.access.isWritten || v2.access.isWritten)
-                                                if ((v1.mutexes intersect v2.mutexes).isEmpty())
-                                                    return@Predicate true
-                            }
-            false
-        }
+      Predicate<XcfaState<out PtrState<out ExprState>>> { s ->
+        val xcfa = s.xcfa!!
+        for (process1 in s.processes) for (process2 in s.processes) if (
+          process1.key != process2.key
+        )
+          for (edge1 in process1.value.locs.peek().outgoingEdges) for (edge2 in
+            process2.value.locs.peek().outgoingEdges) {
+            val mutexes1 = s.mutexes.filterValues { it == process1.key }.keys
+            val mutexes2 = s.mutexes.filterValues { it == process2.key }.keys
+            val globalVars1 = edge1.getGlobalVarsWithNeededMutexes(xcfa, mutexes1)
+            val globalVars2 = edge2.getGlobalVarsWithNeededMutexes(xcfa, mutexes2)
+            for (v1 in globalVars1) for (v2 in globalVars2) if (v1.varDecl == v2.varDecl)
+              if (v1.access.isWritten || v2.access.isWritten)
+                if ((v1.mutexes intersect v2.mutexes).isEmpty()) return@Predicate true
+          }
+        false
+      }
     }
 
-    ErrorDetection.NO_ERROR, ErrorDetection.OVERFLOW -> Predicate<XcfaState<out PtrState<out ExprState>>> { false }
-}
+    ErrorDetection.NO_ERROR,
+    ErrorDetection.OVERFLOW -> Predicate<XcfaState<out PtrState<out ExprState>>> { false }
+  }
 
 fun <S : ExprState> getPartialOrder(partialOrd: PartialOrd<PtrState<S>>) =
-    PartialOrd<XcfaState<PtrState<S>>> { s1, s2 ->
-        s1.processes == s2.processes && s1.bottom == s2.bottom && s1.mutexes == s2.mutexes && partialOrd.isLeq(
-            s1.sGlobal, s2.sGlobal)
-    }
+  PartialOrd<XcfaState<PtrState<S>>> { s1, s2 ->
+    s1.processes == s2.processes &&
+      s1.bottom == s2.bottom &&
+      s1.mutexes == s2.mutexes &&
+      partialOrd.isLeq(s1.sGlobal, s2.sGlobal)
+  }
 
-private fun <S : ExprState> stackIsLeq(s1: XcfaState<PtrState<S>>,
-    s2: XcfaState<PtrState<S>>) = s2.processes.keys.all { pid ->
+private fun <S : ExprState> stackIsLeq(s1: XcfaState<PtrState<S>>, s2: XcfaState<PtrState<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
+      val ps2 = s2.processes.getValue(pid)
+      ps1.locs.peek() == ps2.locs.peek() && ps1.paramsInitialized && ps2.paramsInitialized
     } ?: false
-}
+  }
 
 fun <S : ExprState> getStackPartialOrder(partialOrd: PartialOrd<PtrState<S>>) =
-    PartialOrd<XcfaState<PtrState<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())
-    }
+  PartialOrd<XcfaState<PtrState<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 PtrState<out ExprState>>, P : XcfaPrec<out Prec>> getXcfaArgBuilder(
-    analysis: Analysis<S, XcfaAction, P>,
-    lts: LTS<XcfaState<out PtrState<out ExprState>>, XcfaAction>,
-    errorDetection: ErrorDetection)
-    : ArgBuilder<S, XcfaAction, P> =
-    ArgBuilder.create(
-        lts,
-        analysis,
-        getXcfaErrorPredicate(errorDetection)
-    )
+  analysis: Analysis<S, XcfaAction, P>,
+  lts: LTS<XcfaState<out PtrState<out ExprState>>, XcfaAction>,
+  errorDetection: ErrorDetection,
+): ArgBuilder<S, XcfaAction, P> =
+  ArgBuilder.create(lts, analysis, getXcfaErrorPredicate(errorDetection))
 
 fun <S : XcfaState<out PtrState<out ExprState>>, P : XcfaPrec<out Prec>> getXcfaAbstractor(
-    analysis: Analysis<S, XcfaAction, P>,
-    waitlist: Waitlist<*>,
-    stopCriterion: StopCriterion<*, *>,
-    logger: Logger,
-    lts: LTS<XcfaState<out PtrState<out ExprState>>, XcfaAction>,
-    errorDetection: ErrorDetection
-): Abstractor<out XcfaState<out PtrState<out ExprState>>, XcfaAction, out XcfaPrec<out Prec>> =
-    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 {
-            if (it.xcfa!!.isInlined) it.processes
-            else it.processes.map { (_, p) -> p.locs.peek() }
-        }
-        .build() // TODO: can we do this nicely?
+  analysis: Analysis<S, XcfaAction, P>,
+  waitlist: Waitlist<*>,
+  stopCriterion: StopCriterion<*, *>,
+  logger: Logger,
+  lts: LTS<XcfaState<out PtrState<out ExprState>>, XcfaAction>,
+  errorDetection: ErrorDetection,
+): ArgAbstractor<out XcfaState<out PtrState<out ExprState>>, XcfaAction, out XcfaPrec<out Prec>> =
+  XcfaArgAbstractor.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 {
+      if (it.xcfa!!.isInlined) it.processes else it.processes.map { (_, p) -> p.locs.peek() }
+    }
+    .build() // TODO: can we do this nicely?
 
 /// EXPL
 
-private fun getExplXcfaInitFunc(xcfa: XCFA,
-    solver: Solver): (XcfaPrec<PtrPrec<ExplPrec>>) -> List<XcfaState<PtrState<ExplState>>> {
-    val processInitState = xcfa.initProcedures.mapIndexed { i, it ->
+private fun getExplXcfaInitFunc(
+  xcfa: XCFA,
+  solver: Solver,
+): (XcfaPrec<PtrPrec<ExplPrec>>) -> List<XcfaState<PtrState<ExplState>>> {
+  val processInitState =
+    xcfa.initProcedures
+      .mapIndexed { i, it ->
         val initLocStack: LinkedList<XcfaLocation> = LinkedList()
         initLocStack.add(it.first.initLoc)
-        Pair(i, XcfaProcessState(initLocStack, prefix = "T$i",
-            varLookup = LinkedList(listOf(createLookup(it.first, "T$i", "")))))
-    }.toMap()
-    return { p ->
-        ExplInitFunc.create(solver, True()).getPtrInitFunc().getInitStates(p.p)
-            .map { XcfaState(xcfa, processInitState, it) }
+        Pair(
+          i,
+          XcfaProcessState(
+            initLocStack,
+            prefix = "T$i",
+            varLookup = LinkedList(listOf(createLookup(it.first, "T$i", ""))),
+          ),
+        )
+      }
+      .toMap()
+  return { p ->
+    ExplInitFunc.create(solver, True()).getPtrInitFunc().getInitStates(p.p).map {
+      XcfaState(xcfa, processInitState, it)
     }
+  }
 }
 
-private fun getExplXcfaTransFunc(solver: Solver, maxEnum: Int, isHavoc: Boolean):
-    (XcfaState<PtrState<ExplState>>, XcfaAction, XcfaPrec<PtrPrec<ExplPrec>>) -> List<XcfaState<PtrState<ExplState>>> {
-    val explTransFunc = (ExplStmtTransFunc.create(solver,
-        maxEnum) as TransFunc<ExplState, ExprAction, ExplPrec>).getPtrTransFunc(isHavoc)
-    return { s, a, p ->
-        val (newSt, newAct) = s.apply(a)
-        explTransFunc.getSuccStates(newSt.sGlobal, newAct, p.p.addVars(
-            listOf(s.processes.map { it.value.varLookup }.flatten(),
-                listOf(getTempLookup(a.label))).flatten())).map { newSt.withState(it) }
-    }
+private fun getExplXcfaTransFunc(
+  solver: Solver,
+  maxEnum: Int,
+  isHavoc: Boolean,
+): (XcfaState<PtrState<ExplState>>, XcfaAction, XcfaPrec<PtrPrec<ExplPrec>>) -> List<
+    XcfaState<PtrState<ExplState>>
+  > {
+  val explTransFunc =
+    (ExplStmtTransFunc.create(solver, maxEnum) as TransFunc<ExplState, ExprAction, ExplPrec>)
+      .getPtrTransFunc(isHavoc)
+  return { s, a, p ->
+    val (newSt, newAct) = s.apply(a)
+    explTransFunc
+      .getSuccStates(
+        newSt.sGlobal,
+        newAct,
+        p.p.addVars(
+          listOf(s.processes.map { it.value.varLookup }.flatten(), listOf(getTempLookup(a.label)))
+            .flatten()
+        ),
+      )
+      .map { newSt.withState(it) }
+  }
 }
 
-class ExplXcfaAnalysis(xcfa: XCFA, solver: Solver, maxEnum: Int,
-    partialOrd: PartialOrd<XcfaState<PtrState<ExplState>>>, isHavoc: Boolean) :
-    XcfaAnalysis<ExplState, PtrPrec<ExplPrec>>(
-        corePartialOrd = partialOrd,
-        coreInitFunc = getExplXcfaInitFunc(xcfa, solver),
-        coreTransFunc = getExplXcfaTransFunc(solver, maxEnum, isHavoc)
-    )
+class ExplXcfaAnalysis(
+  xcfa: XCFA,
+  solver: Solver,
+  maxEnum: Int,
+  partialOrd: PartialOrd<XcfaState<PtrState<ExplState>>>,
+  isHavoc: Boolean,
+) :
+  XcfaAnalysis<ExplState, PtrPrec<ExplPrec>>(
+    corePartialOrd = partialOrd,
+    coreInitFunc = getExplXcfaInitFunc(xcfa, solver),
+    coreTransFunc = getExplXcfaTransFunc(solver, maxEnum, isHavoc),
+  )
 
 /// PRED
 
-private fun getPredXcfaInitFunc(xcfa: XCFA,
-    predAbstractor: PredAbstractor): (XcfaPrec<PtrPrec<PredPrec>>) -> List<XcfaState<PtrState<PredState>>> {
-    val processInitState = xcfa.initProcedures.mapIndexed { i, it ->
+private fun getPredXcfaInitFunc(
+  xcfa: XCFA,
+  predAbstractor: PredAbstractor,
+): (XcfaPrec<PtrPrec<PredPrec>>) -> List<XcfaState<PtrState<PredState>>> {
+  val processInitState =
+    xcfa.initProcedures
+      .mapIndexed { i, it ->
         val initLocStack: LinkedList<XcfaLocation> = LinkedList()
         initLocStack.add(it.first.initLoc)
-        Pair(i, XcfaProcessState(initLocStack, prefix = "T$i",
-            varLookup = LinkedList(listOf(createLookup(it.first, "T$i", "")))))
-    }.toMap()
-    return { p ->
-        PredInitFunc.create(predAbstractor, True()).getPtrInitFunc().getInitStates(p.p)
-            .map { XcfaState(xcfa, processInitState, it) }
+        Pair(
+          i,
+          XcfaProcessState(
+            initLocStack,
+            prefix = "T$i",
+            varLookup = LinkedList(listOf(createLookup(it.first, "T$i", ""))),
+          ),
+        )
+      }
+      .toMap()
+  return { p ->
+    PredInitFunc.create(predAbstractor, True()).getPtrInitFunc().getInitStates(p.p).map {
+      XcfaState(xcfa, processInitState, it)
     }
+  }
 }
 
-private fun getPredXcfaTransFunc(predAbstractor: PredAbstractors.PredAbstractor, isHavoc: Boolean):
-    (XcfaState<PtrState<PredState>>, XcfaAction, XcfaPrec<PtrPrec<PredPrec>>) -> List<XcfaState<PtrState<PredState>>> {
-    val predTransFunc = (PredTransFunc.create<StmtAction>(
-        predAbstractor) as TransFunc<PredState, ExprAction, PredPrec>).getPtrTransFunc(isHavoc)
-    return { s, a, p ->
-        val (newSt, newAct) = s.apply(a)
-        predTransFunc.getSuccStates(newSt.sGlobal, newAct, p.p.addVars(
-            s.processes.map { it.value.foldVarLookup() + getTempLookup(a.label) }
-        )).map { newSt.withState(it) }
-    }
+private fun getPredXcfaTransFunc(
+  predAbstractor: PredAbstractors.PredAbstractor,
+  isHavoc: Boolean,
+): (XcfaState<PtrState<PredState>>, XcfaAction, XcfaPrec<PtrPrec<PredPrec>>) -> List<
+    XcfaState<PtrState<PredState>>
+  > {
+  val predTransFunc =
+    (PredTransFunc.create<StmtAction>(predAbstractor) as TransFunc<PredState, ExprAction, PredPrec>)
+      .getPtrTransFunc(isHavoc)
+  return { s, a, p ->
+    val (newSt, newAct) = s.apply(a)
+    predTransFunc
+      .getSuccStates(
+        newSt.sGlobal,
+        newAct,
+        p.p.addVars(s.processes.map { it.value.foldVarLookup() + getTempLookup(a.label) }),
+      )
+      .map { newSt.withState(it) }
+  }
 }
 
-class PredXcfaAnalysis(xcfa: XCFA, solver: Solver, predAbstractor: PredAbstractor,
-    partialOrd: PartialOrd<XcfaState<PtrState<PredState>>>, isHavoc: Boolean) :
-    XcfaAnalysis<PredState, PtrPrec<PredPrec>>(
-        corePartialOrd = partialOrd,
-        coreInitFunc = getPredXcfaInitFunc(xcfa, predAbstractor),
-        coreTransFunc = getPredXcfaTransFunc(predAbstractor, isHavoc)
-    )
+class PredXcfaAnalysis(
+  xcfa: XCFA,
+  solver: Solver,
+  predAbstractor: PredAbstractor,
+  partialOrd: PartialOrd<XcfaState<PtrState<PredState>>>,
+  isHavoc: Boolean,
+) :
+  XcfaAnalysis<PredState, PtrPrec<PredPrec>>(
+    corePartialOrd = partialOrd,
+    coreInitFunc = getPredXcfaInitFunc(xcfa, predAbstractor),
+    coreTransFunc = getPredXcfaTransFunc(predAbstractor, isHavoc),
+  )
diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaArgAbstractor.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaArgAbstractor.kt
new file mode 100644
index 0000000000..bc2d2b816c
--- /dev/null
+++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaArgAbstractor.kt
@@ -0,0 +1,143 @@
+/*
+ *  Copyright 2024 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.ARG
+import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder
+import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode
+import hu.bme.mit.theta.analysis.algorithm.cegar.AbstractorResult
+import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor
+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 XcfaArgAbstractor<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,
+) : BasicArgAbstractor<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>
+    ): BasicArgAbstractor.Builder<S, A, P> {
+      return Builder(argBuilder)
+    }
+  }
+
+  class Builder<S : State, A : Action, P : Prec>(argBuilder: ArgBuilder<S, A, P>) :
+    BasicArgAbstractor.Builder<S, A, P>(argBuilder) {
+
+    override fun build(): BasicArgAbstractor<S, A, P> {
+      return XcfaArgAbstractor(argBuilder, projection, waitlist, stopCriterion, logger)
+    }
+  }
+}
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
index ad0a385e5d..93410e0641 100644
--- 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
@@ -64,7 +64,7 @@ class XcfaSingleExprTraceRefiner<S : ExprState, A : ExprAction, P : Prec, R : Re
         return null
     }
 
-    fun refineTemp(arg: ARG<S, A>, prec: P?): RefinerResult<S, A, P?> {
+    fun refineTemp(arg: ARG<S, A>, prec: P?): RefinerResult<S, A, P?, Trace<S, A>> {
         Preconditions.checkNotNull(arg)
         Preconditions.checkNotNull(prec)
         assert(!arg.isSafe) { "ARG must be unsafe" }
@@ -118,7 +118,7 @@ class XcfaSingleExprTraceRefiner<S : ExprState, A : ExprAction, P : Prec, R : Re
         }
     }
 
-    override fun refine(arg: ARG<S, A>, prec: P?): RefinerResult<S, A, P?> {
+    override fun refine(arg: ARG<S, A>, prec: P?): RefinerResult<S, A, P?, Trace<S, A>> {
         Preconditions.checkNotNull(arg)
         Preconditions.checkNotNull<P>(prec)
         assert(!arg.isSafe) { "ARG must be unsafe" }
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 b4aa758303..a04508f9cf 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
@@ -13,14 +13,13 @@
  *  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.algorithm.arg.ArgNodeComparators
 import hu.bme.mit.theta.analysis.algorithm.SafetyResult
-import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor
-import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker
-import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner
+import hu.bme.mit.theta.analysis.algorithm.arg.ArgNodeComparators
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgAbstractor
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgCegarChecker
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgRefiner
 import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterions
 import hu.bme.mit.theta.analysis.expl.*
 import hu.bme.mit.theta.analysis.expr.refinement.*
@@ -39,255 +38,309 @@ import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory
 import hu.bme.mit.theta.xcfa.analysis.coi.ConeOfInfluence
 import hu.bme.mit.theta.xcfa.analysis.coi.XcfaCoiMultiThread
 import hu.bme.mit.theta.xcfa.analysis.por.*
+import java.util.*
+import kotlin.random.Random
 import org.junit.jupiter.api.Assertions
 import org.junit.jupiter.params.ParameterizedTest
 import org.junit.jupiter.params.provider.MethodSource
-import java.util.*
-import kotlin.random.Random
-
 
 class XcfaExplAnalysisTest {
 
+  companion object {
 
-    companion object {
-
-        private val seed = 1001
-
-        @JvmStatic
-        fun data(): Collection<Array<Any>> {
-            return listOf(
-                arrayOf("/00assignment.c", SafetyResult<*, *>::isUnsafe),
-                arrayOf("/01function.c", SafetyResult<*, *>::isUnsafe),
-                arrayOf("/02functionparam.c", SafetyResult<*, *>::isSafe),
-                arrayOf("/03nondetfunction.c", SafetyResult<*, *>::isUnsafe),
-                arrayOf("/04multithread.c", SafetyResult<*, *>::isUnsafe),
-            )
-        }
-    }
-
-    @ParameterizedTest
-    @MethodSource("data")
-    fun testNoporExpl(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) {
-        println("Testing NOPOR on $filepath...")
-        val stream = javaClass.getResourceAsStream(filepath)
-        val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first
-        ConeOfInfluence = XcfaCoiMultiThread(xcfa)
-
-        val analysis = ExplXcfaAnalysis(
-            xcfa,
-            Z3LegacySolverFactory.getInstance().createSolver(),
-            1,
-            getPartialOrder(ExplOrd.getInstance().getPtrPartialOrd()), false
-        )
-
-        val lts = getXcfaLts()
-
-        val abstractor = getXcfaAbstractor(analysis,
-            PriorityWaitlist.create(
-                ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs())),
-            StopCriterions.firstCex<XcfaState<PtrState<ExplState>>, XcfaAction>(),
-            ConsoleLogger(Logger.Level.DETAIL),
-            lts,
-            ErrorDetection.ERROR_LOCATION) as Abstractor<XcfaState<PtrState<ExplState>>, XcfaAction, XcfaPrec<PtrPrec<ExplPrec>>>
-
-        val precRefiner = XcfaPrecRefiner<XcfaState<PtrState<ExplState>>, ExplPrec, ItpRefutation>(
-            ItpRefToPtrPrec(ItpRefToExplPrec()))
-
-        val refiner =
-            XcfaSingleExprTraceRefiner.create(
-                ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(),
-                    Z3LegacySolverFactory.getInstance().createItpSolver()),
-                precRefiner, PruneStrategy.FULL,
-                NullLogger.getInstance()) as Refiner<XcfaState<PtrState<ExplState>>, XcfaAction, XcfaPrec<PtrPrec<ExplPrec>>>
-
-        val cegarChecker =
-            CegarChecker.create(abstractor, refiner)
-
-        val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(ExplPrec.empty(), emptySet())))
-
-
-
-        Assertions.assertTrue(verdict(safetyResult))
-    }
-
-    @ParameterizedTest
-    @MethodSource("data")
-    fun testSporExpl(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) {
-        println("Testing SPOR on $filepath...")
-        val stream = javaClass.getResourceAsStream(filepath)
-        val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first
-        ConeOfInfluence = XcfaCoiMultiThread(xcfa)
-
-        val analysis = ExplXcfaAnalysis(
-            xcfa,
-            Z3LegacySolverFactory.getInstance().createSolver(),
-            1,
-            getPartialOrder(ExplOrd.getInstance().getPtrPartialOrd()), false
-        )
-
-        val lts = XcfaSporLts(xcfa)
-
-        val abstractor = getXcfaAbstractor(analysis,
-            PriorityWaitlist.create(
-                ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs())),
-            StopCriterions.firstCex<XcfaState<PtrState<ExplState>>, XcfaAction>(),
-            ConsoleLogger(Logger.Level.DETAIL),
-            lts,
-            ErrorDetection.ERROR_LOCATION) as Abstractor<XcfaState<PtrState<ExplState>>, XcfaAction, XcfaPrec<PtrPrec<ExplPrec>>>
-
-        val precRefiner = XcfaPrecRefiner<XcfaState<PtrState<ExplState>>, ExplPrec, ItpRefutation>(
-            ItpRefToPtrPrec(ItpRefToExplPrec()))
-
-        val refiner =
-            XcfaSingleExprTraceRefiner.create(
-                ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(),
-                    Z3LegacySolverFactory.getInstance().createItpSolver()),
-                precRefiner, PruneStrategy.FULL,
-                NullLogger.getInstance()) as Refiner<XcfaState<PtrState<ExplState>>, XcfaAction, XcfaPrec<PtrPrec<ExplPrec>>>
-
-        val cegarChecker =
-            CegarChecker.create(abstractor, refiner)
-
-        val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(ExplPrec.empty(), emptySet())))
-
-
-
-        Assertions.assertTrue(verdict(safetyResult))
-    }
-
-    @ParameterizedTest
-    @MethodSource("data")
-    fun testDporExpl(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) {
-        XcfaDporLts.random = Random(seed)
-        println("Testing DPOR on $filepath...")
-        val stream = javaClass.getResourceAsStream(filepath)
-        val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first
-        ConeOfInfluence = XcfaCoiMultiThread(xcfa)
-
-        val analysis = ExplXcfaAnalysis(
-            xcfa,
-            Z3LegacySolverFactory.getInstance().createSolver(),
-            1,
-            XcfaDporLts.getPartialOrder(getPartialOrder(ExplOrd.getInstance().getPtrPartialOrd())), false
-        )
-
-        val lts = XcfaDporLts(xcfa)
-
-        val abstractor = getXcfaAbstractor(analysis,
-            lts.waitlist,
-            StopCriterions.firstCex<XcfaState<PtrState<ExplState>>, XcfaAction>(),
-            ConsoleLogger(Logger.Level.DETAIL),
-            lts,
-            ErrorDetection.ERROR_LOCATION) as Abstractor<XcfaState<PtrState<ExplState>>, XcfaAction, XcfaPrec<PtrPrec<ExplPrec>>>
-
-        val precRefiner = XcfaPrecRefiner<XcfaState<PtrState<ExplState>>, ExplPrec, ItpRefutation>(
-            ItpRefToPtrPrec(ItpRefToExplPrec()))
-
-        val refiner =
-            XcfaSingleExprTraceRefiner.create(
-                ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(),
-                    Z3LegacySolverFactory.getInstance().createItpSolver()),
-                precRefiner, PruneStrategy.FULL,
-                ConsoleLogger(
-                    Logger.Level.DETAIL)) as Refiner<XcfaState<PtrState<ExplState>>, XcfaAction, XcfaPrec<PtrPrec<ExplPrec>>>
-
-        val cegarChecker =
-            CegarChecker.create(abstractor, refiner)
-
-        val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(ExplPrec.empty(), emptySet())))
-
-
-
-        Assertions.assertTrue(verdict(safetyResult))
-    }
-
-    @ParameterizedTest
-    @MethodSource("data")
-    fun testAasporExpl(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) {
-        println("Testing AASPOR on $filepath...")
-        val stream = javaClass.getResourceAsStream(filepath)
-        val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first
-        ConeOfInfluence = XcfaCoiMultiThread(xcfa)
-
-        val analysis = ExplXcfaAnalysis(
-            xcfa,
-            Z3LegacySolverFactory.getInstance().createSolver(),
-            1,
-            getPartialOrder(ExplOrd.getInstance().getPtrPartialOrd()), false
-        )
-
-        val lts = XcfaAasporLts(xcfa, mutableMapOf())
-
-        val abstractor = getXcfaAbstractor(analysis,
-            PriorityWaitlist.create(
-                ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs())),
-            StopCriterions.firstCex<XcfaState<PtrState<ExplState>>, XcfaAction>(),
-            ConsoleLogger(Logger.Level.DETAIL),
-            lts,
-            ErrorDetection.ERROR_LOCATION) as Abstractor<XcfaState<PtrState<ExplState>>, XcfaAction, XcfaPrec<PtrPrec<ExplPrec>>>
-
-        val precRefiner = XcfaPrecRefiner<PtrState<ExplState>, ExplPrec, ItpRefutation>(
-            ItpRefToPtrPrec(ItpRefToExplPrec()))
-        val atomicNodePruner = AtomicNodePruner<XcfaState<PtrState<ExplState>>, XcfaAction>()
-
-        val refiner =
-            XcfaSingleExprTraceRefiner.create(
-                ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(),
-                    Z3LegacySolverFactory.getInstance().createItpSolver()),
-                precRefiner, PruneStrategy.FULL, NullLogger.getInstance(),
-                atomicNodePruner) as Refiner<XcfaState<PtrState<ExplState>>, XcfaAction, XcfaPrec<PtrPrec<ExplPrec>>>
-
-        val cegarChecker =
-            CegarChecker.create(abstractor, AasporRefiner.create(refiner, PruneStrategy.FULL, mutableMapOf()))
-
-        val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(ExplPrec.empty(), emptySet())))
-
-
-
-        Assertions.assertTrue(verdict(safetyResult))
-    }
-
-    @ParameterizedTest
-    @MethodSource("data")
-    fun testAadporExpl(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) {
-        XcfaDporLts.random = Random(seed)
-        println("Testing AADPOR on $filepath...")
-        val stream = javaClass.getResourceAsStream(filepath)
-        val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first
-        ConeOfInfluence = XcfaCoiMultiThread(xcfa)
-
-        val analysis = ExplXcfaAnalysis(
-            xcfa,
-            Z3LegacySolverFactory.getInstance().createSolver(),
-            1,
-            XcfaDporLts.getPartialOrder(getPartialOrder(ExplOrd.getInstance().getPtrPartialOrd())), false
-        )
-
-        val lts = XcfaAadporLts(xcfa)
-
-        val abstractor = getXcfaAbstractor(analysis,
-            lts.waitlist,
-            StopCriterions.firstCex<XcfaState<PtrState<ExplState>>, XcfaAction>(),
-            ConsoleLogger(Logger.Level.DETAIL),
-            lts,
-            ErrorDetection.ERROR_LOCATION) as Abstractor<XcfaState<PtrState<ExplState>>, XcfaAction, XcfaPrec<PtrPrec<ExplPrec>>>
-
-        val precRefiner = XcfaPrecRefiner<ExplState, ExplPrec, ItpRefutation>(ItpRefToPtrPrec(ItpRefToExplPrec()))
-
-        val refiner =
-            XcfaSingleExprTraceRefiner.create(
-                ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(),
-                    Z3LegacySolverFactory.getInstance().createItpSolver()),
-                precRefiner, PruneStrategy.FULL,
-                NullLogger.getInstance()) as Refiner<XcfaState<PtrState<ExplState>>, XcfaAction, XcfaPrec<PtrPrec<ExplPrec>>>
-
-        val cegarChecker =
-            CegarChecker.create(abstractor, refiner)
-
-        val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(ExplPrec.empty(), emptySet())))
-
-
+    private val seed = 1001
 
-        Assertions.assertTrue(verdict(safetyResult))
+    @JvmStatic
+    fun data(): Collection<Array<Any>> {
+      return listOf(
+        arrayOf("/00assignment.c", SafetyResult<*, *>::isUnsafe),
+        arrayOf("/01function.c", SafetyResult<*, *>::isUnsafe),
+        arrayOf("/02functionparam.c", SafetyResult<*, *>::isSafe),
+        arrayOf("/03nondetfunction.c", SafetyResult<*, *>::isUnsafe),
+        arrayOf("/04multithread.c", SafetyResult<*, *>::isUnsafe),
+      )
     }
-}
\ No newline at end of file
+  }
+
+  @ParameterizedTest
+  @MethodSource("data")
+  fun testNoporExpl(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) {
+    println("Testing NOPOR on $filepath...")
+    val stream = javaClass.getResourceAsStream(filepath)
+    val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first
+    ConeOfInfluence = XcfaCoiMultiThread(xcfa)
+
+    val analysis =
+      ExplXcfaAnalysis(
+        xcfa,
+        Z3LegacySolverFactory.getInstance().createSolver(),
+        1,
+        getPartialOrder(ExplOrd.getInstance().getPtrPartialOrd()),
+        false,
+      )
+
+    val lts = getXcfaLts()
+
+    val abstractor =
+      getXcfaAbstractor(
+        analysis,
+        PriorityWaitlist.create(
+          ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs())
+        ),
+        StopCriterions.firstCex<XcfaState<PtrState<ExplState>>, XcfaAction>(),
+        ConsoleLogger(Logger.Level.DETAIL),
+        lts,
+        ErrorDetection.ERROR_LOCATION,
+      )
+        as ArgAbstractor<XcfaState<PtrState<ExplState>>, XcfaAction, XcfaPrec<PtrPrec<ExplPrec>>>
+
+    val precRefiner =
+      XcfaPrecRefiner<XcfaState<PtrState<ExplState>>, ExplPrec, ItpRefutation>(
+        ItpRefToPtrPrec(ItpRefToExplPrec())
+      )
+
+    val refiner =
+      XcfaSingleExprTraceRefiner.create(
+        ExprTraceBwBinItpChecker.create(
+          BoolExprs.True(),
+          BoolExprs.True(),
+          Z3LegacySolverFactory.getInstance().createItpSolver(),
+        ),
+        precRefiner,
+        PruneStrategy.FULL,
+        NullLogger.getInstance(),
+      ) as ArgRefiner<XcfaState<PtrState<ExplState>>, XcfaAction, XcfaPrec<PtrPrec<ExplPrec>>>
+
+    val cegarChecker = ArgCegarChecker.create(abstractor, refiner)
+
+    val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(ExplPrec.empty(), emptySet())))
+
+    Assertions.assertTrue(verdict(safetyResult))
+  }
+
+  @ParameterizedTest
+  @MethodSource("data")
+  fun testSporExpl(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) {
+    println("Testing SPOR on $filepath...")
+    val stream = javaClass.getResourceAsStream(filepath)
+    val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first
+    ConeOfInfluence = XcfaCoiMultiThread(xcfa)
+
+    val analysis =
+      ExplXcfaAnalysis(
+        xcfa,
+        Z3LegacySolverFactory.getInstance().createSolver(),
+        1,
+        getPartialOrder(ExplOrd.getInstance().getPtrPartialOrd()),
+        false,
+      )
+
+    val lts = XcfaSporLts(xcfa)
+
+    val abstractor =
+      getXcfaAbstractor(
+        analysis,
+        PriorityWaitlist.create(
+          ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs())
+        ),
+        StopCriterions.firstCex<XcfaState<PtrState<ExplState>>, XcfaAction>(),
+        ConsoleLogger(Logger.Level.DETAIL),
+        lts,
+        ErrorDetection.ERROR_LOCATION,
+      )
+        as ArgAbstractor<XcfaState<PtrState<ExplState>>, XcfaAction, XcfaPrec<PtrPrec<ExplPrec>>>
+
+    val precRefiner =
+      XcfaPrecRefiner<XcfaState<PtrState<ExplState>>, ExplPrec, ItpRefutation>(
+        ItpRefToPtrPrec(ItpRefToExplPrec())
+      )
+
+    val refiner =
+      XcfaSingleExprTraceRefiner.create(
+        ExprTraceBwBinItpChecker.create(
+          BoolExprs.True(),
+          BoolExprs.True(),
+          Z3LegacySolverFactory.getInstance().createItpSolver(),
+        ),
+        precRefiner,
+        PruneStrategy.FULL,
+        NullLogger.getInstance(),
+      ) as ArgRefiner<XcfaState<PtrState<ExplState>>, XcfaAction, XcfaPrec<PtrPrec<ExplPrec>>>
+
+    val cegarChecker = ArgCegarChecker.create(abstractor, refiner)
+
+    val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(ExplPrec.empty(), emptySet())))
+
+    Assertions.assertTrue(verdict(safetyResult))
+  }
+
+  @ParameterizedTest
+  @MethodSource("data")
+  fun testDporExpl(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) {
+    XcfaDporLts.random = Random(seed)
+    println("Testing DPOR on $filepath...")
+    val stream = javaClass.getResourceAsStream(filepath)
+    val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first
+    ConeOfInfluence = XcfaCoiMultiThread(xcfa)
+
+    val analysis =
+      ExplXcfaAnalysis(
+        xcfa,
+        Z3LegacySolverFactory.getInstance().createSolver(),
+        1,
+        XcfaDporLts.getPartialOrder(getPartialOrder(ExplOrd.getInstance().getPtrPartialOrd())),
+        false,
+      )
+
+    val lts = XcfaDporLts(xcfa)
+
+    val abstractor =
+      getXcfaAbstractor(
+        analysis,
+        lts.waitlist,
+        StopCriterions.firstCex<XcfaState<PtrState<ExplState>>, XcfaAction>(),
+        ConsoleLogger(Logger.Level.DETAIL),
+        lts,
+        ErrorDetection.ERROR_LOCATION,
+      )
+        as ArgAbstractor<XcfaState<PtrState<ExplState>>, XcfaAction, XcfaPrec<PtrPrec<ExplPrec>>>
+
+    val precRefiner =
+      XcfaPrecRefiner<XcfaState<PtrState<ExplState>>, ExplPrec, ItpRefutation>(
+        ItpRefToPtrPrec(ItpRefToExplPrec())
+      )
+
+    val refiner =
+      XcfaSingleExprTraceRefiner.create(
+        ExprTraceBwBinItpChecker.create(
+          BoolExprs.True(),
+          BoolExprs.True(),
+          Z3LegacySolverFactory.getInstance().createItpSolver(),
+        ),
+        precRefiner,
+        PruneStrategy.FULL,
+        ConsoleLogger(Logger.Level.DETAIL),
+      ) as ArgRefiner<XcfaState<PtrState<ExplState>>, XcfaAction, XcfaPrec<PtrPrec<ExplPrec>>>
+
+    val cegarChecker = ArgCegarChecker.create(abstractor, refiner)
+
+    val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(ExplPrec.empty(), emptySet())))
+
+    Assertions.assertTrue(verdict(safetyResult))
+  }
+
+  @ParameterizedTest
+  @MethodSource("data")
+  fun testAasporExpl(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) {
+    println("Testing AASPOR on $filepath...")
+    val stream = javaClass.getResourceAsStream(filepath)
+    val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first
+    ConeOfInfluence = XcfaCoiMultiThread(xcfa)
+
+    val analysis =
+      ExplXcfaAnalysis(
+        xcfa,
+        Z3LegacySolverFactory.getInstance().createSolver(),
+        1,
+        getPartialOrder(ExplOrd.getInstance().getPtrPartialOrd()),
+        false,
+      )
+
+    val lts = XcfaAasporLts(xcfa, mutableMapOf())
+
+    val abstractor =
+      getXcfaAbstractor(
+        analysis,
+        PriorityWaitlist.create(
+          ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs())
+        ),
+        StopCriterions.firstCex<XcfaState<PtrState<ExplState>>, XcfaAction>(),
+        ConsoleLogger(Logger.Level.DETAIL),
+        lts,
+        ErrorDetection.ERROR_LOCATION,
+      )
+        as ArgAbstractor<XcfaState<PtrState<ExplState>>, XcfaAction, XcfaPrec<PtrPrec<ExplPrec>>>
+
+    val precRefiner =
+      XcfaPrecRefiner<PtrState<ExplState>, ExplPrec, ItpRefutation>(
+        ItpRefToPtrPrec(ItpRefToExplPrec())
+      )
+    val atomicNodePruner = AtomicNodePruner<XcfaState<PtrState<ExplState>>, XcfaAction>()
+
+    val refiner =
+      XcfaSingleExprTraceRefiner.create(
+        ExprTraceBwBinItpChecker.create(
+          BoolExprs.True(),
+          BoolExprs.True(),
+          Z3LegacySolverFactory.getInstance().createItpSolver(),
+        ),
+        precRefiner,
+        PruneStrategy.FULL,
+        NullLogger.getInstance(),
+        atomicNodePruner,
+      ) as ArgRefiner<XcfaState<PtrState<ExplState>>, XcfaAction, XcfaPrec<PtrPrec<ExplPrec>>>
+
+    val cegarChecker =
+      ArgCegarChecker.create(
+        abstractor,
+        AasporRefiner.create(refiner, PruneStrategy.FULL, mutableMapOf()),
+      )
+
+    val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(ExplPrec.empty(), emptySet())))
+
+    Assertions.assertTrue(verdict(safetyResult))
+  }
+
+  @ParameterizedTest
+  @MethodSource("data")
+  fun testAadporExpl(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) {
+    XcfaDporLts.random = Random(seed)
+    println("Testing AADPOR on $filepath...")
+    val stream = javaClass.getResourceAsStream(filepath)
+    val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first
+    ConeOfInfluence = XcfaCoiMultiThread(xcfa)
+
+    val analysis =
+      ExplXcfaAnalysis(
+        xcfa,
+        Z3LegacySolverFactory.getInstance().createSolver(),
+        1,
+        XcfaDporLts.getPartialOrder(getPartialOrder(ExplOrd.getInstance().getPtrPartialOrd())),
+        false,
+      )
+
+    val lts = XcfaAadporLts(xcfa)
+
+    val abstractor =
+      getXcfaAbstractor(
+        analysis,
+        lts.waitlist,
+        StopCriterions.firstCex<XcfaState<PtrState<ExplState>>, XcfaAction>(),
+        ConsoleLogger(Logger.Level.DETAIL),
+        lts,
+        ErrorDetection.ERROR_LOCATION,
+      )
+        as ArgAbstractor<XcfaState<PtrState<ExplState>>, XcfaAction, XcfaPrec<PtrPrec<ExplPrec>>>
+
+    val precRefiner =
+      XcfaPrecRefiner<ExplState, ExplPrec, ItpRefutation>(ItpRefToPtrPrec(ItpRefToExplPrec()))
+
+    val refiner =
+      XcfaSingleExprTraceRefiner.create(
+        ExprTraceBwBinItpChecker.create(
+          BoolExprs.True(),
+          BoolExprs.True(),
+          Z3LegacySolverFactory.getInstance().createItpSolver(),
+        ),
+        precRefiner,
+        PruneStrategy.FULL,
+        NullLogger.getInstance(),
+      ) as ArgRefiner<XcfaState<PtrState<ExplState>>, XcfaAction, XcfaPrec<PtrPrec<ExplPrec>>>
+
+    val cegarChecker = ArgCegarChecker.create(abstractor, refiner)
+
+    val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(ExplPrec.empty(), emptySet())))
+
+    Assertions.assertTrue(verdict(safetyResult))
+  }
+}
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 e398b5ed07..a10e82f096 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
@@ -13,14 +13,13 @@
  *  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.algorithm.arg.ArgNodeComparators
 import hu.bme.mit.theta.analysis.algorithm.SafetyResult
-import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor
-import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker
-import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner
+import hu.bme.mit.theta.analysis.algorithm.arg.ArgNodeComparators
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgAbstractor
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgCegarChecker
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgRefiner
 import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterions
 import hu.bme.mit.theta.analysis.expr.refinement.*
 import hu.bme.mit.theta.analysis.pred.*
@@ -39,262 +38,316 @@ import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory
 import hu.bme.mit.theta.xcfa.analysis.coi.ConeOfInfluence
 import hu.bme.mit.theta.xcfa.analysis.coi.XcfaCoiMultiThread
 import hu.bme.mit.theta.xcfa.analysis.por.*
+import java.util.*
+import kotlin.random.Random
 import org.junit.jupiter.api.Assertions
 import org.junit.jupiter.params.ParameterizedTest
 import org.junit.jupiter.params.provider.MethodSource
-import java.util.*
-import kotlin.random.Random
-
 
 class XcfaPredAnalysisTest {
 
+  companion object {
 
-    companion object {
-
-        private val seed = 1001;
-
-        @JvmStatic
-        fun data(): Collection<Array<Any>> {
-            return listOf(
-                arrayOf("/00assignment.c", SafetyResult<*, *>::isUnsafe),
-                arrayOf("/01function.c", SafetyResult<*, *>::isUnsafe),
-                arrayOf("/02functionparam.c", SafetyResult<*, *>::isSafe),
-                arrayOf("/03nondetfunction.c", SafetyResult<*, *>::isUnsafe),
-                arrayOf("/04multithread.c", SafetyResult<*, *>::isUnsafe),
-            )
-        }
-    }
-
-    @ParameterizedTest
-    @MethodSource("data")
-    fun testNoporPred(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) {
-        println("Testing NOPOR on $filepath...")
-        val stream = javaClass.getResourceAsStream(filepath)
-        val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first
-        ConeOfInfluence = XcfaCoiMultiThread(xcfa)
-
-        val solver = Z3LegacySolverFactory.getInstance().createSolver()
-        val analysis = PredXcfaAnalysis(
-            xcfa,
-            solver,
-            PredAbstractors.cartesianAbstractor(solver),
-            getPartialOrder(PredOrd.create(solver).getPtrPartialOrd()),
-            false
-        )
-
-        val lts = getXcfaLts()
-
-        val abstractor = getXcfaAbstractor(analysis,
-            PriorityWaitlist.create(
-                ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs())),
-            StopCriterions.firstCex<XcfaState<PtrState<PredState>>, XcfaAction>(),
-            ConsoleLogger(Logger.Level.DETAIL),
-            lts,
-            ErrorDetection.ERROR_LOCATION) as Abstractor<XcfaState<PtrState<PredState>>, XcfaAction, XcfaPrec<PtrPrec<PredPrec>>>
-
-        val precRefiner = XcfaPrecRefiner<XcfaState<PtrState<PredState>>, PredPrec, ItpRefutation>(
-            ItpRefToPtrPrec(ItpRefToPredPrec(ExprSplitters.whole())))
-
-        val refiner =
-            XcfaSingleExprTraceRefiner.create(
-                ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(),
-                    Z3LegacySolverFactory.getInstance().createItpSolver()),
-                precRefiner, PruneStrategy.FULL,
-                NullLogger.getInstance()) as Refiner<XcfaState<PtrState<PredState>>, XcfaAction, XcfaPrec<PtrPrec<PredPrec>>>
-
-        val cegarChecker =
-            CegarChecker.create(abstractor, refiner)
-
-        val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(PredPrec.of(), emptySet())))
-
-
-
-        Assertions.assertTrue(verdict(safetyResult))
-    }
-
-    @ParameterizedTest
-    @MethodSource("data")
-    fun testSporPred(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) {
-        println("Testing SPOR on $filepath...")
-        val stream = javaClass.getResourceAsStream(filepath)
-        val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first
-        ConeOfInfluence = XcfaCoiMultiThread(xcfa)
-
-        val solver = Z3LegacySolverFactory.getInstance().createSolver()
-        val analysis = PredXcfaAnalysis(
-            xcfa,
-            solver,
-            PredAbstractors.cartesianAbstractor(solver),
-            getPartialOrder(PredOrd.create(solver).getPtrPartialOrd()), false
-        )
-
-        val lts = XcfaSporLts(xcfa)
-
-        val abstractor = getXcfaAbstractor(analysis,
-            PriorityWaitlist.create(
-                ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs())),
-            StopCriterions.firstCex<XcfaState<PtrState<PredState>>, XcfaAction>(),
-            ConsoleLogger(Logger.Level.DETAIL),
-            lts,
-            ErrorDetection.ERROR_LOCATION) as Abstractor<XcfaState<PtrState<PredState>>, XcfaAction, XcfaPrec<PtrPrec<PredPrec>>>
-
-        val precRefiner = XcfaPrecRefiner<XcfaState<PtrState<PredState>>, PredPrec, ItpRefutation>(
-            ItpRefToPtrPrec(ItpRefToPredPrec(ExprSplitters.whole())))
-
-        val refiner =
-            XcfaSingleExprTraceRefiner.create(
-                ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(),
-                    Z3LegacySolverFactory.getInstance().createItpSolver()),
-                precRefiner, PruneStrategy.FULL,
-                NullLogger.getInstance()) as Refiner<XcfaState<PtrState<PredState>>, XcfaAction, XcfaPrec<PtrPrec<PredPrec>>>
-
-        val cegarChecker =
-            CegarChecker.create(abstractor, refiner)
-
-        val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(PredPrec.of(), emptySet())))
-
-
-
-        Assertions.assertTrue(verdict(safetyResult))
-    }
-
-    @ParameterizedTest
-    @MethodSource("data")
-    fun testDporPred(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) {
-        XcfaDporLts.random = Random(seed)
-        println("Testing DPOR on $filepath...")
-        val stream = javaClass.getResourceAsStream(filepath)
-        val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first
-        ConeOfInfluence = XcfaCoiMultiThread(xcfa)
-
-        val solver = Z3LegacySolverFactory.getInstance().createSolver()
-        val analysis = PredXcfaAnalysis(
-            xcfa,
-            solver,
-            PredAbstractors.cartesianAbstractor(solver),
-            XcfaDporLts.getPartialOrder(getPartialOrder(PredOrd.create(solver).getPtrPartialOrd())), false
-        )
-
-        val lts = XcfaDporLts(xcfa)
-
-        val abstractor = getXcfaAbstractor(analysis,
-            lts.waitlist,
-            StopCriterions.firstCex<XcfaState<PtrState<PredState>>, XcfaAction>(),
-            ConsoleLogger(Logger.Level.DETAIL),
-            lts,
-            ErrorDetection.ERROR_LOCATION) as Abstractor<XcfaState<PtrState<PredState>>, XcfaAction, XcfaPrec<PtrPrec<PredPrec>>>
-
-        val precRefiner = XcfaPrecRefiner<XcfaState<PtrState<PredState>>, PredPrec, ItpRefutation>(
-            ItpRefToPtrPrec(ItpRefToPredPrec(ExprSplitters.whole())))
-
-        val refiner =
-            XcfaSingleExprTraceRefiner.create(
-                ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(),
-                    Z3LegacySolverFactory.getInstance().createItpSolver()),
-                precRefiner, PruneStrategy.FULL,
-                ConsoleLogger(
-                    Logger.Level.DETAIL)) as Refiner<XcfaState<PtrState<PredState>>, XcfaAction, XcfaPrec<PtrPrec<PredPrec>>>
-
-        val cegarChecker =
-            CegarChecker.create(abstractor, refiner)
-
-        val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(PredPrec.of(), emptySet())))
-
-
-
-        Assertions.assertTrue(verdict(safetyResult))
-    }
-
-    @ParameterizedTest
-    @MethodSource("data")
-    fun testAasporPred(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) {
-        println("Testing AASPOR on $filepath...")
-        val stream = javaClass.getResourceAsStream(filepath)
-        val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first
-        ConeOfInfluence = XcfaCoiMultiThread(xcfa)
-
-        val solver = Z3LegacySolverFactory.getInstance().createSolver()
-        val analysis = PredXcfaAnalysis(
-            xcfa,
-            solver,
-            PredAbstractors.cartesianAbstractor(solver),
-            getPartialOrder(PredOrd.create(solver).getPtrPartialOrd()), false
-        )
-
-        val lts = XcfaAasporLts(xcfa, mutableMapOf())
-
-        val abstractor = getXcfaAbstractor(analysis,
-            PriorityWaitlist.create(
-                ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs())),
-            StopCriterions.firstCex<XcfaState<PtrState<PredState>>, XcfaAction>(),
-            ConsoleLogger(Logger.Level.DETAIL),
-            lts,
-            ErrorDetection.ERROR_LOCATION) as Abstractor<XcfaState<PtrState<PredState>>, XcfaAction, XcfaPrec<PtrPrec<PredPrec>>>
-
-        val precRefiner = XcfaPrecRefiner<PtrState<PredState>, PredPrec, ItpRefutation>(
-            ItpRefToPtrPrec(ItpRefToPredPrec(ExprSplitters.whole())))
-        val atomicNodePruner = AtomicNodePruner<XcfaState<PtrState<PredState>>, XcfaAction>()
-
-        val refiner =
-            XcfaSingleExprTraceRefiner.create(
-                ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(),
-                    Z3LegacySolverFactory.getInstance().createItpSolver()),
-                precRefiner, PruneStrategy.FULL, NullLogger.getInstance(),
-                atomicNodePruner) as Refiner<XcfaState<PtrState<PredState>>, XcfaAction, XcfaPrec<PtrPrec<PredPrec>>>
-
-        val cegarChecker =
-            CegarChecker.create(abstractor, AasporRefiner.create(refiner, PruneStrategy.FULL, mutableMapOf()))
-
-        val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(PredPrec.of(), emptySet())))
-
-
-
-        Assertions.assertTrue(verdict(safetyResult))
-    }
-
-    @ParameterizedTest
-    @MethodSource("data")
-    fun testAadporPred(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) {
-        XcfaDporLts.random = Random(seed)
-        println("Testing AADPOR on $filepath...")
-        val stream = javaClass.getResourceAsStream(filepath)
-        val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first
-        ConeOfInfluence = XcfaCoiMultiThread(xcfa)
-
-        val solver = Z3LegacySolverFactory.getInstance().createSolver()
-        val analysis = PredXcfaAnalysis(
-            xcfa,
-            solver,
-            PredAbstractors.cartesianAbstractor(solver),
-            XcfaDporLts.getPartialOrder(getPartialOrder(PredOrd.create(solver).getPtrPartialOrd())), false
-        )
-
-        val lts = XcfaAadporLts(xcfa)
-
-        val abstractor = getXcfaAbstractor(analysis,
-            lts.waitlist,
-            StopCriterions.firstCex<XcfaState<PtrState<PredState>>, XcfaAction>(),
-            ConsoleLogger(Logger.Level.DETAIL),
-            lts,
-            ErrorDetection.ERROR_LOCATION) as Abstractor<XcfaState<PtrState<PredState>>, XcfaAction, XcfaPrec<PtrPrec<PredPrec>>>
-
-        val precRefiner = XcfaPrecRefiner<PredState, PredPrec, ItpRefutation>(
-            ItpRefToPtrPrec(ItpRefToPredPrec(ExprSplitters.whole())))
-
-        val refiner =
-            XcfaSingleExprTraceRefiner.create(
-                ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(),
-                    Z3LegacySolverFactory.getInstance().createItpSolver()),
-                precRefiner, PruneStrategy.FULL,
-                NullLogger.getInstance()) as Refiner<XcfaState<PtrState<PredState>>, XcfaAction, XcfaPrec<PtrPrec<PredPrec>>>
-
-        val cegarChecker =
-            CegarChecker.create(abstractor, refiner)
-
-        val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(PredPrec.of(), emptySet())))
-
-
+    private val seed = 1001
 
-        Assertions.assertTrue(verdict(safetyResult))
+    @JvmStatic
+    fun data(): Collection<Array<Any>> {
+      return listOf(
+        arrayOf("/00assignment.c", SafetyResult<*, *>::isUnsafe),
+        arrayOf("/01function.c", SafetyResult<*, *>::isUnsafe),
+        arrayOf("/02functionparam.c", SafetyResult<*, *>::isSafe),
+        arrayOf("/03nondetfunction.c", SafetyResult<*, *>::isUnsafe),
+        arrayOf("/04multithread.c", SafetyResult<*, *>::isUnsafe),
+      )
     }
-}
\ No newline at end of file
+  }
+
+  @ParameterizedTest
+  @MethodSource("data")
+  fun testNoporPred(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) {
+    println("Testing NOPOR on $filepath...")
+    val stream = javaClass.getResourceAsStream(filepath)
+    val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first
+    ConeOfInfluence = XcfaCoiMultiThread(xcfa)
+
+    val solver = Z3LegacySolverFactory.getInstance().createSolver()
+    val analysis =
+      PredXcfaAnalysis(
+        xcfa,
+        solver,
+        PredAbstractors.cartesianAbstractor(solver),
+        getPartialOrder(PredOrd.create(solver).getPtrPartialOrd()),
+        false,
+      )
+
+    val lts = getXcfaLts()
+
+    val abstractor =
+      getXcfaAbstractor(
+        analysis,
+        PriorityWaitlist.create(
+          ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs())
+        ),
+        StopCriterions.firstCex<XcfaState<PtrState<PredState>>, XcfaAction>(),
+        ConsoleLogger(Logger.Level.DETAIL),
+        lts,
+        ErrorDetection.ERROR_LOCATION,
+      )
+        as ArgAbstractor<XcfaState<PtrState<PredState>>, XcfaAction, XcfaPrec<PtrPrec<PredPrec>>>
+
+    val precRefiner =
+      XcfaPrecRefiner<XcfaState<PtrState<PredState>>, PredPrec, ItpRefutation>(
+        ItpRefToPtrPrec(ItpRefToPredPrec(ExprSplitters.whole()))
+      )
+
+    val refiner =
+      XcfaSingleExprTraceRefiner.create(
+        ExprTraceBwBinItpChecker.create(
+          BoolExprs.True(),
+          BoolExprs.True(),
+          Z3LegacySolverFactory.getInstance().createItpSolver(),
+        ),
+        precRefiner,
+        PruneStrategy.FULL,
+        NullLogger.getInstance(),
+      ) as ArgRefiner<XcfaState<PtrState<PredState>>, XcfaAction, XcfaPrec<PtrPrec<PredPrec>>>
+
+    val cegarChecker = ArgCegarChecker.create(abstractor, refiner)
+
+    val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(PredPrec.of(), emptySet())))
+
+    Assertions.assertTrue(verdict(safetyResult))
+  }
+
+  @ParameterizedTest
+  @MethodSource("data")
+  fun testSporPred(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) {
+    println("Testing SPOR on $filepath...")
+    val stream = javaClass.getResourceAsStream(filepath)
+    val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first
+    ConeOfInfluence = XcfaCoiMultiThread(xcfa)
+
+    val solver = Z3LegacySolverFactory.getInstance().createSolver()
+    val analysis =
+      PredXcfaAnalysis(
+        xcfa,
+        solver,
+        PredAbstractors.cartesianAbstractor(solver),
+        getPartialOrder(PredOrd.create(solver).getPtrPartialOrd()),
+        false,
+      )
+
+    val lts = XcfaSporLts(xcfa)
+
+    val abstractor =
+      getXcfaAbstractor(
+        analysis,
+        PriorityWaitlist.create(
+          ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs())
+        ),
+        StopCriterions.firstCex<XcfaState<PtrState<PredState>>, XcfaAction>(),
+        ConsoleLogger(Logger.Level.DETAIL),
+        lts,
+        ErrorDetection.ERROR_LOCATION,
+      )
+        as ArgAbstractor<XcfaState<PtrState<PredState>>, XcfaAction, XcfaPrec<PtrPrec<PredPrec>>>
+
+    val precRefiner =
+      XcfaPrecRefiner<XcfaState<PtrState<PredState>>, PredPrec, ItpRefutation>(
+        ItpRefToPtrPrec(ItpRefToPredPrec(ExprSplitters.whole()))
+      )
+
+    val refiner =
+      XcfaSingleExprTraceRefiner.create(
+        ExprTraceBwBinItpChecker.create(
+          BoolExprs.True(),
+          BoolExprs.True(),
+          Z3LegacySolverFactory.getInstance().createItpSolver(),
+        ),
+        precRefiner,
+        PruneStrategy.FULL,
+        NullLogger.getInstance(),
+      ) as ArgRefiner<XcfaState<PtrState<PredState>>, XcfaAction, XcfaPrec<PtrPrec<PredPrec>>>
+
+    val cegarChecker = ArgCegarChecker.create(abstractor, refiner)
+
+    val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(PredPrec.of(), emptySet())))
+
+    Assertions.assertTrue(verdict(safetyResult))
+  }
+
+  @ParameterizedTest
+  @MethodSource("data")
+  fun testDporPred(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) {
+    XcfaDporLts.random = Random(seed)
+    println("Testing DPOR on $filepath...")
+    val stream = javaClass.getResourceAsStream(filepath)
+    val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first
+    ConeOfInfluence = XcfaCoiMultiThread(xcfa)
+
+    val solver = Z3LegacySolverFactory.getInstance().createSolver()
+    val analysis =
+      PredXcfaAnalysis(
+        xcfa,
+        solver,
+        PredAbstractors.cartesianAbstractor(solver),
+        XcfaDporLts.getPartialOrder(getPartialOrder(PredOrd.create(solver).getPtrPartialOrd())),
+        false,
+      )
+
+    val lts = XcfaDporLts(xcfa)
+
+    val abstractor =
+      getXcfaAbstractor(
+        analysis,
+        lts.waitlist,
+        StopCriterions.firstCex<XcfaState<PtrState<PredState>>, XcfaAction>(),
+        ConsoleLogger(Logger.Level.DETAIL),
+        lts,
+        ErrorDetection.ERROR_LOCATION,
+      )
+        as ArgAbstractor<XcfaState<PtrState<PredState>>, XcfaAction, XcfaPrec<PtrPrec<PredPrec>>>
+
+    val precRefiner =
+      XcfaPrecRefiner<XcfaState<PtrState<PredState>>, PredPrec, ItpRefutation>(
+        ItpRefToPtrPrec(ItpRefToPredPrec(ExprSplitters.whole()))
+      )
+
+    val refiner =
+      XcfaSingleExprTraceRefiner.create(
+        ExprTraceBwBinItpChecker.create(
+          BoolExprs.True(),
+          BoolExprs.True(),
+          Z3LegacySolverFactory.getInstance().createItpSolver(),
+        ),
+        precRefiner,
+        PruneStrategy.FULL,
+        ConsoleLogger(Logger.Level.DETAIL),
+      ) as ArgRefiner<XcfaState<PtrState<PredState>>, XcfaAction, XcfaPrec<PtrPrec<PredPrec>>>
+
+    val cegarChecker = ArgCegarChecker.create(abstractor, refiner)
+
+    val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(PredPrec.of(), emptySet())))
+
+    Assertions.assertTrue(verdict(safetyResult))
+  }
+
+  @ParameterizedTest
+  @MethodSource("data")
+  fun testAasporPred(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) {
+    println("Testing AASPOR on $filepath...")
+    val stream = javaClass.getResourceAsStream(filepath)
+    val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first
+    ConeOfInfluence = XcfaCoiMultiThread(xcfa)
+
+    val solver = Z3LegacySolverFactory.getInstance().createSolver()
+    val analysis =
+      PredXcfaAnalysis(
+        xcfa,
+        solver,
+        PredAbstractors.cartesianAbstractor(solver),
+        getPartialOrder(PredOrd.create(solver).getPtrPartialOrd()),
+        false,
+      )
+
+    val lts = XcfaAasporLts(xcfa, mutableMapOf())
+
+    val abstractor =
+      getXcfaAbstractor(
+        analysis,
+        PriorityWaitlist.create(
+          ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs())
+        ),
+        StopCriterions.firstCex<XcfaState<PtrState<PredState>>, XcfaAction>(),
+        ConsoleLogger(Logger.Level.DETAIL),
+        lts,
+        ErrorDetection.ERROR_LOCATION,
+      )
+        as ArgAbstractor<XcfaState<PtrState<PredState>>, XcfaAction, XcfaPrec<PtrPrec<PredPrec>>>
+
+    val precRefiner =
+      XcfaPrecRefiner<PtrState<PredState>, PredPrec, ItpRefutation>(
+        ItpRefToPtrPrec(ItpRefToPredPrec(ExprSplitters.whole()))
+      )
+    val atomicNodePruner = AtomicNodePruner<XcfaState<PtrState<PredState>>, XcfaAction>()
+
+    val refiner =
+      XcfaSingleExprTraceRefiner.create(
+        ExprTraceBwBinItpChecker.create(
+          BoolExprs.True(),
+          BoolExprs.True(),
+          Z3LegacySolverFactory.getInstance().createItpSolver(),
+        ),
+        precRefiner,
+        PruneStrategy.FULL,
+        NullLogger.getInstance(),
+        atomicNodePruner,
+      ) as ArgRefiner<XcfaState<PtrState<PredState>>, XcfaAction, XcfaPrec<PtrPrec<PredPrec>>>
+
+    val cegarChecker =
+      ArgCegarChecker.create(
+        abstractor,
+        AasporRefiner.create(refiner, PruneStrategy.FULL, mutableMapOf()),
+      )
+
+    val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(PredPrec.of(), emptySet())))
+
+    Assertions.assertTrue(verdict(safetyResult))
+  }
+
+  @ParameterizedTest
+  @MethodSource("data")
+  fun testAadporPred(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) {
+    XcfaDporLts.random = Random(seed)
+    println("Testing AADPOR on $filepath...")
+    val stream = javaClass.getResourceAsStream(filepath)
+    val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first
+    ConeOfInfluence = XcfaCoiMultiThread(xcfa)
+
+    val solver = Z3LegacySolverFactory.getInstance().createSolver()
+    val analysis =
+      PredXcfaAnalysis(
+        xcfa,
+        solver,
+        PredAbstractors.cartesianAbstractor(solver),
+        XcfaDporLts.getPartialOrder(getPartialOrder(PredOrd.create(solver).getPtrPartialOrd())),
+        false,
+      )
+
+    val lts = XcfaAadporLts(xcfa)
+
+    val abstractor =
+      getXcfaAbstractor(
+        analysis,
+        lts.waitlist,
+        StopCriterions.firstCex<XcfaState<PtrState<PredState>>, XcfaAction>(),
+        ConsoleLogger(Logger.Level.DETAIL),
+        lts,
+        ErrorDetection.ERROR_LOCATION,
+      )
+        as ArgAbstractor<XcfaState<PtrState<PredState>>, XcfaAction, XcfaPrec<PtrPrec<PredPrec>>>
+
+    val precRefiner =
+      XcfaPrecRefiner<PredState, PredPrec, ItpRefutation>(
+        ItpRefToPtrPrec(ItpRefToPredPrec(ExprSplitters.whole()))
+      )
+
+    val refiner =
+      XcfaSingleExprTraceRefiner.create(
+        ExprTraceBwBinItpChecker.create(
+          BoolExprs.True(),
+          BoolExprs.True(),
+          Z3LegacySolverFactory.getInstance().createItpSolver(),
+        ),
+        precRefiner,
+        PruneStrategy.FULL,
+        NullLogger.getInstance(),
+      ) as ArgRefiner<XcfaState<PtrState<PredState>>, XcfaAction, XcfaPrec<PtrPrec<PredPrec>>>
+
+    val cegarChecker = ArgCegarChecker.create(abstractor, refiner)
+
+    val safetyResult = cegarChecker.check(XcfaPrec(PtrPrec(PredPrec.of(), emptySet())))
+
+    Assertions.assertTrue(verdict(safetyResult))
+  }
+}
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt
index 8c39486021..f8bf86f8d2 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt
@@ -23,9 +23,9 @@ import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode
 import hu.bme.mit.theta.analysis.algorithm.SafetyChecker
 import hu.bme.mit.theta.analysis.algorithm.SafetyResult
 import hu.bme.mit.theta.analysis.algorithm.arg.ARG
-import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor
-import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker
-import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgAbstractor
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgCegarChecker
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgRefiner
 import hu.bme.mit.theta.analysis.expr.ExprAction
 import hu.bme.mit.theta.analysis.expr.ExprState
 import hu.bme.mit.theta.analysis.expr.refinement.*
@@ -43,14 +43,20 @@ import hu.bme.mit.theta.xcfa.cli.params.*
 import hu.bme.mit.theta.xcfa.cli.utils.getSolver
 import hu.bme.mit.theta.xcfa.model.XCFA
 
-fun getCegarChecker(xcfa: XCFA, mcm: MCM,
+fun getCegarChecker(
+    xcfa: XCFA, mcm: MCM,
     config: XcfaConfig<*, *>,
-    logger: Logger): SafetyChecker<ARG<XcfaState<*>, XcfaAction>, Trace<XcfaState<PtrState<*>>, XcfaAction>, XcfaPrec<*>> {
+    logger: Logger
+): SafetyChecker<ARG<XcfaState<*>, XcfaAction>, Trace<XcfaState<PtrState<*>>, XcfaAction>, XcfaPrec<*>> {
     val cegarConfig = config.backendConfig.specConfig as CegarConfig
-    val abstractionSolverFactory: SolverFactory = getSolver(cegarConfig.abstractorConfig.abstractionSolver,
-        cegarConfig.abstractorConfig.validateAbstractionSolver)
-    val refinementSolverFactory: SolverFactory = getSolver(cegarConfig.refinerConfig.refinementSolver,
-        cegarConfig.refinerConfig.validateRefinementSolver)
+    val abstractionSolverFactory: SolverFactory = getSolver(
+        cegarConfig.abstractorConfig.abstractionSolver,
+        cegarConfig.abstractorConfig.validateAbstractionSolver
+    )
+    val refinementSolverFactory: SolverFactory = getSolver(
+        cegarConfig.refinerConfig.refinementSolver,
+        cegarConfig.refinerConfig.validateRefinementSolver
+    )
 
     val ignoredVarRegistry = mutableMapOf<VarDecl<*>, MutableSet<ExprState>>()
 
@@ -59,16 +65,18 @@ fun getCegarChecker(xcfa: XCFA, mcm: MCM,
         (cegarConfig.coi.porLts as XcfaDporLts).waitlist
     } else {
         PriorityWaitlist.create<ArgNode<out XcfaState<PtrState<ExprState>>, XcfaAction>>(
-            cegarConfig.abstractorConfig.search.getComp(xcfa))
+            cegarConfig.abstractorConfig.search.getComp(xcfa)
+        )
     }
 
     val abstractionSolverInstance = abstractionSolverFactory.createSolver()
     val globalStatePartialOrd: PartialOrd<PtrState<ExprState>> = cegarConfig.abstractorConfig.domain.partialOrd(
-        abstractionSolverInstance) as PartialOrd<PtrState<ExprState>>
+        abstractionSolverInstance
+    ) as PartialOrd<PtrState<ExprState>>
     val corePartialOrd: PartialOrd<XcfaState<PtrState<ExprState>>> =
         if (xcfa.isInlined) getPartialOrder(globalStatePartialOrd)
         else getStackPartialOrder(globalStatePartialOrd)
-    val abstractor: Abstractor<ExprState, ExprAction, Prec> = cegarConfig.abstractorConfig.domain.abstractor(
+    val abstractor: ArgAbstractor<ExprState, ExprAction, Prec> = cegarConfig.abstractorConfig.domain.abstractor(
         xcfa,
         abstractionSolverInstance,
         cegarConfig.abstractorConfig.maxEnum,
@@ -83,7 +91,7 @@ fun getCegarChecker(xcfa: XCFA, mcm: MCM,
             corePartialOrd
         },
         cegarConfig.abstractorConfig.havocMemory
-    ) as Abstractor<ExprState, ExprAction, Prec>
+    ) as ArgAbstractor<ExprState, ExprAction, Prec>
 
     val ref: ExprTraceChecker<Refutation> =
         cegarConfig.refinerConfig.refinement.refiner(refinementSolverFactory, cegarConfig.cexMonitor)
@@ -91,43 +99,50 @@ fun getCegarChecker(xcfa: XCFA, mcm: MCM,
     val precRefiner: PrecRefiner<ExprState, ExprAction, Prec, Refutation> =
         cegarConfig.abstractorConfig.domain.itpPrecRefiner(cegarConfig.refinerConfig.exprSplitter.exprSplitter)
             as PrecRefiner<ExprState, ExprAction, Prec, Refutation>
-    val atomicNodePruner: NodePruner<ExprState, ExprAction> = cegarConfig.abstractorConfig.domain.nodePruner as NodePruner<ExprState, ExprAction>
-    val refiner: Refiner<ExprState, ExprAction, Prec> =
+    val atomicNodePruner: NodePruner<ExprState, ExprAction> =
+        cegarConfig.abstractorConfig.domain.nodePruner as NodePruner<ExprState, ExprAction>
+    val refiner: ArgRefiner<ExprState, ExprAction, Prec> =
         if (cegarConfig.refinerConfig.refinement == Refinement.MULTI_SEQ)
             if (cegarConfig.porLevel == POR.AASPOR)
-                MultiExprTraceRefiner.create(ref, precRefiner, cegarConfig.refinerConfig.pruneStrategy, logger,
-                    atomicNodePruner)
+                MultiExprTraceRefiner.create(
+                    ref, precRefiner, cegarConfig.refinerConfig.pruneStrategy, logger,
+                    atomicNodePruner
+                )
             else
                 MultiExprTraceRefiner.create(ref, precRefiner, cegarConfig.refinerConfig.pruneStrategy, logger)
         else
             if (cegarConfig.porLevel == POR.AASPOR)
-                XcfaSingleExprTraceRefiner.create(ref, precRefiner, cegarConfig.refinerConfig.pruneStrategy, logger,
-                    atomicNodePruner)
+                XcfaSingleExprTraceRefiner.create(
+                    ref, precRefiner, cegarConfig.refinerConfig.pruneStrategy, logger,
+                    atomicNodePruner
+                )
             else
                 XcfaSingleExprTraceRefiner.create(ref, precRefiner, cegarConfig.refinerConfig.pruneStrategy, logger)
 
     val cegarChecker = if (cegarConfig.porLevel == POR.AASPOR)
-        CegarChecker.create(
+        ArgCegarChecker.create(
             abstractor,
             AasporRefiner.create(refiner, cegarConfig.refinerConfig.pruneStrategy, ignoredVarRegistry),
             logger
         )
     else
-        CegarChecker.create(abstractor, refiner, logger)
+        ArgCegarChecker.create(abstractor, refiner, logger)
 
     // initialize monitors
     MonitorCheckpoint.reset()
     if (cegarConfig.cexMonitor == CexMonitorOptions.CHECK) {
-        val cm = CexMonitor(logger, cegarChecker.arg)
+        val cm = CexMonitor(logger, cegarChecker.witness)
         MonitorCheckpoint.register(cm, "CegarChecker.unsafeARG")
     }
 
     return object :
         SafetyChecker<ARG<XcfaState<*>, XcfaAction>, Trace<XcfaState<PtrState<*>>, XcfaAction>, XcfaPrec<*>> {
         override fun check(
-            prec: XcfaPrec<*>?): SafetyResult<ARG<XcfaState<*>, XcfaAction>, Trace<XcfaState<PtrState<*>>, XcfaAction>> {
+            prec: XcfaPrec<*>?
+        ): SafetyResult<ARG<XcfaState<*>, XcfaAction>, Trace<XcfaState<PtrState<*>>, XcfaAction>> {
             return cegarChecker.check(
-                prec) as SafetyResult<ARG<XcfaState<*>, XcfaAction>, Trace<XcfaState<PtrState<*>>, XcfaAction>>
+                prec
+            ) as SafetyResult<ARG<XcfaState<*>, XcfaAction>, Trace<XcfaState<PtrState<*>>, XcfaAction>>
         }
 
         override fun check(): SafetyResult<ARG<XcfaState<*>, XcfaAction>, Trace<XcfaState<PtrState<*>>, XcfaAction>> {
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt
index ac5b3d3236..8f1695855c 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt
@@ -13,7 +13,6 @@
  *  See the License for the specific language governing permissions and
  *  limitations under the License.
  */
-
 package hu.bme.mit.theta.xcfa.cli.params
 
 import com.google.gson.reflect.TypeToken
@@ -23,7 +22,7 @@ import hu.bme.mit.theta.analysis.Prec
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgNodeComparators
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgNodeComparators.ArgNodeComparator
-import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgAbstractor
 import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterion
 import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterions
 import hu.bme.mit.theta.analysis.expl.ExplPrec
@@ -55,309 +54,386 @@ import hu.bme.mit.theta.xcfa.model.XCFA
 import java.lang.reflect.Type
 
 enum class InputType {
-    C,
-    LLVM,
-    JSON,
-    DSL,
-    CHC,
-    LITMUS,
+  C,
+  LLVM,
+  JSON,
+  DSL,
+  CHC,
+  LITMUS,
 }
 
 enum class Backend {
-    CEGAR,
-    BOUNDED,
-    CHC,
-    OC,
-    LAZY,
-    PORTFOLIO,
-    NONE,
+  CEGAR,
+  BOUNDED,
+  CHC,
+  OC,
+  LAZY,
+  PORTFOLIO,
+  NONE,
 }
 
 enum class POR(
-    val getLts: (XCFA, MutableMap<VarDecl<*>, MutableSet<ExprState>>) -> LTS<XcfaState<out PtrState<out ExprState>>, XcfaAction>,
-    val isDynamic: Boolean,
-    val isAbstractionAware: Boolean
+  val getLts:
+    (XCFA, MutableMap<VarDecl<*>, MutableSet<ExprState>>) -> LTS<
+        XcfaState<out PtrState<out ExprState>>,
+        XcfaAction,
+      >,
+  val isDynamic: Boolean,
+  val isAbstractionAware: Boolean,
 ) {
 
-    NOPOR({ _, _ -> getXcfaLts() }, false, false),
-    SPOR({ xcfa, _ -> XcfaSporLts(xcfa) }, false, false),
-    AASPOR({ xcfa, registry -> XcfaAasporLts(xcfa, registry) }, false, true),
-    DPOR({ xcfa, _ -> XcfaDporLts(xcfa) }, true, false),
-    AADPOR({ xcfa, _ -> XcfaAadporLts(xcfa) }, true, true)
+  NOPOR({ _, _ -> getXcfaLts() }, false, false),
+  SPOR({ xcfa, _ -> XcfaSporLts(xcfa) }, false, false),
+  AASPOR({ xcfa, registry -> XcfaAasporLts(xcfa, registry) }, false, true),
+  DPOR({ xcfa, _ -> XcfaDporLts(xcfa) }, true, false),
+  AADPOR({ xcfa, _ -> XcfaAadporLts(xcfa) }, true, true),
 }
 
 enum class Strategy {
-    DIRECT,
-    SERVER,
-    SERVER_DEBUG,
-    PORTFOLIO
+  DIRECT,
+  SERVER,
+  SERVER_DEBUG,
+  PORTFOLIO,
 }
 
 // TODO partial orders nicely
 enum class Domain(
-    val abstractor: (
-        xcfa: XCFA,
-        solver: Solver,
-        maxEnum: Int,
-        waitlist: Waitlist<out ArgNode<out XcfaState<out PtrState<out ExprState>>, XcfaAction>>,
-        stopCriterion: StopCriterion<out XcfaState<out PtrState<out ExprState>>, XcfaAction>,
-        logger: Logger,
-        lts: LTS<XcfaState<out PtrState<out ExprState>>, XcfaAction>,
-        errorDetectionType: ErrorDetection,
-        partialOrd: PartialOrd<out XcfaState<out PtrState<out ExprState>>>,
-        isHavoc: Boolean
-    ) -> 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<out PtrPrec<*>>,
-    val partialOrd: (Solver) -> PartialOrd<out PtrState<out ExprState>>,
-    val nodePruner: NodePruner<out ExprState, out ExprAction>,
-    val stateType: Type
+  val abstractor:
+    (
+      xcfa: XCFA,
+      solver: Solver,
+      maxEnum: Int,
+      waitlist: Waitlist<out ArgNode<out XcfaState<out PtrState<out ExprState>>, XcfaAction>>,
+      stopCriterion: StopCriterion<out XcfaState<out PtrState<out ExprState>>, XcfaAction>,
+      logger: Logger,
+      lts: LTS<XcfaState<out PtrState<out ExprState>>, XcfaAction>,
+      errorDetectionType: ErrorDetection,
+      partialOrd: PartialOrd<out XcfaState<out PtrState<out ExprState>>>,
+      isHavoc: Boolean,
+    ) -> ArgAbstractor<out ExprState, out ExprAction, out Prec>,
+  val itpPrecRefiner:
+    (exprSplitter: ExprSplitter) -> PrecRefiner<
+        out ExprState,
+        out ExprAction,
+        out Prec,
+        out Refutation,
+      >,
+  val initPrec: (XCFA, InitPrec) -> XcfaPrec<out PtrPrec<*>>,
+  val partialOrd: (Solver) -> PartialOrd<out PtrState<out ExprState>>,
+  val nodePruner: NodePruner<out ExprState, out ExprAction>,
+  val stateType: Type,
 ) {
 
-    EXPL(
-        abstractor = { a, b, c, d, e, f, g, h, i, j ->
-            getXcfaAbstractor(ExplXcfaAnalysis(a, b, c, i as PartialOrd<XcfaState<PtrState<ExplState>>>, j), d,
-                e, f, g, h)
-        },
-        itpPrecRefiner = {
-            XcfaPrecRefiner<PtrState<ExplState>, ExplPrec, ItpRefutation>(ItpRefToPtrPrec(ItpRefToExplPrec()))
-        },
-        initPrec = { x, ip -> ip.explPrec(x) },
-        partialOrd = { PartialOrd<ExplState> { s1, s2 -> s1.isLeq(s2) }.getPtrPartialOrd() },
-        nodePruner = AtomicNodePruner<XcfaState<PtrState<ExplState>>, XcfaAction>(),
-        stateType = TypeToken.get(ExplState::class.java).type
-    ),
-    PRED_BOOL(
-        abstractor = { a, b, c, d, e, f, g, h, i, j ->
-            getXcfaAbstractor(PredXcfaAnalysis(a, b, PredAbstractors.booleanAbstractor(b),
-                i as PartialOrd<XcfaState<PtrState<PredState>>>, j), d, e, f, g, h)
-        },
-        itpPrecRefiner = { a ->
-            XcfaPrecRefiner<PtrState<PredState>, PredPrec, ItpRefutation>(ItpRefToPtrPrec(ItpRefToPredPrec(a)))
-        },
-        initPrec = { x, ip -> ip.predPrec(x) },
-        partialOrd = { solver -> PredOrd.create(solver).getPtrPartialOrd() },
-        nodePruner = AtomicNodePruner<XcfaState<PtrState<PredState>>, XcfaAction>(),
-        stateType = TypeToken.get(PredState::class.java).type
-    ),
-    PRED_CART(
-        abstractor = { a, b, c, d, e, f, g, h, i, j ->
-            getXcfaAbstractor(PredXcfaAnalysis(a, b, PredAbstractors.cartesianAbstractor(b),
-                i as PartialOrd<XcfaState<PtrState<PredState>>>, j), d, e, f, g, h)
-        },
-        itpPrecRefiner = { a ->
-            XcfaPrecRefiner<PtrState<PredState>, PredPrec, ItpRefutation>(ItpRefToPtrPrec(ItpRefToPredPrec(a)))
-        },
-        initPrec = { x, ip -> ip.predPrec(x) },
-        partialOrd = { solver -> PredOrd.create(solver).getPtrPartialOrd() },
-        nodePruner = AtomicNodePruner<XcfaState<PtrState<PredState>>, XcfaAction>(),
-        stateType = TypeToken.get(PredState::class.java).type
-    ),
-    PRED_SPLIT(
-        abstractor = { a, b, c, d, e, f, g, h, i, j ->
-            getXcfaAbstractor(PredXcfaAnalysis(a, b, PredAbstractors.booleanSplitAbstractor(b),
-                i as PartialOrd<XcfaState<PtrState<PredState>>>, j), d, e, f, g, h)
-        },
-        itpPrecRefiner = { a ->
-            XcfaPrecRefiner<PtrState<PredState>, PredPrec, ItpRefutation>(ItpRefToPtrPrec(ItpRefToPredPrec(a)))
-        },
-        initPrec = { x, ip -> ip.predPrec(x) },
-        partialOrd = { solver -> PredOrd.create(solver).getPtrPartialOrd() },
-        nodePruner = AtomicNodePruner<XcfaState<PtrState<PredState>>, XcfaAction>(),
-        stateType = TypeToken.get(PredState::class.java).type
-    ),
+  EXPL(
+    abstractor = { a, b, c, d, e, f, g, h, i, j ->
+      getXcfaAbstractor(
+        ExplXcfaAnalysis(a, b, c, i as PartialOrd<XcfaState<PtrState<ExplState>>>, j),
+        d,
+        e,
+        f,
+        g,
+        h,
+      )
+    },
+    itpPrecRefiner = {
+      XcfaPrecRefiner<PtrState<ExplState>, ExplPrec, ItpRefutation>(
+        ItpRefToPtrPrec(ItpRefToExplPrec())
+      )
+    },
+    initPrec = { x, ip -> ip.explPrec(x) },
+    partialOrd = { PartialOrd<ExplState> { s1, s2 -> s1.isLeq(s2) }.getPtrPartialOrd() },
+    nodePruner = AtomicNodePruner<XcfaState<PtrState<ExplState>>, XcfaAction>(),
+    stateType = TypeToken.get(ExplState::class.java).type,
+  ),
+  PRED_BOOL(
+    abstractor = { a, b, c, d, e, f, g, h, i, j ->
+      getXcfaAbstractor(
+        PredXcfaAnalysis(
+          a,
+          b,
+          PredAbstractors.booleanAbstractor(b),
+          i as PartialOrd<XcfaState<PtrState<PredState>>>,
+          j,
+        ),
+        d,
+        e,
+        f,
+        g,
+        h,
+      )
+    },
+    itpPrecRefiner = { a ->
+      XcfaPrecRefiner<PtrState<PredState>, PredPrec, ItpRefutation>(
+        ItpRefToPtrPrec(ItpRefToPredPrec(a))
+      )
+    },
+    initPrec = { x, ip -> ip.predPrec(x) },
+    partialOrd = { solver -> PredOrd.create(solver).getPtrPartialOrd() },
+    nodePruner = AtomicNodePruner<XcfaState<PtrState<PredState>>, XcfaAction>(),
+    stateType = TypeToken.get(PredState::class.java).type,
+  ),
+  PRED_CART(
+    abstractor = { a, b, c, d, e, f, g, h, i, j ->
+      getXcfaAbstractor(
+        PredXcfaAnalysis(
+          a,
+          b,
+          PredAbstractors.cartesianAbstractor(b),
+          i as PartialOrd<XcfaState<PtrState<PredState>>>,
+          j,
+        ),
+        d,
+        e,
+        f,
+        g,
+        h,
+      )
+    },
+    itpPrecRefiner = { a ->
+      XcfaPrecRefiner<PtrState<PredState>, PredPrec, ItpRefutation>(
+        ItpRefToPtrPrec(ItpRefToPredPrec(a))
+      )
+    },
+    initPrec = { x, ip -> ip.predPrec(x) },
+    partialOrd = { solver -> PredOrd.create(solver).getPtrPartialOrd() },
+    nodePruner = AtomicNodePruner<XcfaState<PtrState<PredState>>, XcfaAction>(),
+    stateType = TypeToken.get(PredState::class.java).type,
+  ),
+  PRED_SPLIT(
+    abstractor = { a, b, c, d, e, f, g, h, i, j ->
+      getXcfaAbstractor(
+        PredXcfaAnalysis(
+          a,
+          b,
+          PredAbstractors.booleanSplitAbstractor(b),
+          i as PartialOrd<XcfaState<PtrState<PredState>>>,
+          j,
+        ),
+        d,
+        e,
+        f,
+        g,
+        h,
+      )
+    },
+    itpPrecRefiner = { a ->
+      XcfaPrecRefiner<PtrState<PredState>, PredPrec, ItpRefutation>(
+        ItpRefToPtrPrec(ItpRefToPredPrec(a))
+      )
+    },
+    initPrec = { x, ip -> ip.predPrec(x) },
+    partialOrd = { solver -> PredOrd.create(solver).getPtrPartialOrd() },
+    nodePruner = AtomicNodePruner<XcfaState<PtrState<PredState>>, XcfaAction>(),
+    stateType = TypeToken.get(PredState::class.java).type,
+  ),
 }
 
 enum class Refinement(
-    val refiner: (solverFactory: SolverFactory, monitorOption: CexMonitorOptions) -> ExprTraceChecker<out Refutation>,
-    val stopCriterion: StopCriterion<XcfaState<PtrState<ExprState>>, XcfaAction>,
+  val refiner:
+    (solverFactory: SolverFactory, monitorOption: CexMonitorOptions) -> ExprTraceChecker<
+        out Refutation
+      >,
+  val stopCriterion: StopCriterion<XcfaState<PtrState<ExprState>>, XcfaAction>,
 ) {
 
-    FW_BIN_ITP(
-        refiner = { s, _ ->
-            ExprTraceFwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(), s.createItpSolver())
-        },
-        stopCriterion = StopCriterions.firstCex(),
-    ),
-    BW_BIN_ITP(
-        refiner = { s, _ ->
-            ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(), s.createItpSolver())
-        },
-        stopCriterion = StopCriterions.firstCex()
-    ),
-    SEQ_ITP(
-        refiner = { s, _ ->
-            ExprTraceSeqItpChecker.create(BoolExprs.True(), BoolExprs.True(), s.createItpSolver())
-        },
-        stopCriterion = StopCriterions.firstCex()
-    ),
-    MULTI_SEQ(
-        refiner = { s, m ->
-            if (m == CexMonitorOptions.CHECK) error("CexMonitor is not implemented for MULTI_SEQ")
-            ExprTraceSeqItpChecker.create(BoolExprs.True(), BoolExprs.True(), s.createItpSolver())
-        },
-        stopCriterion = StopCriterions.fullExploration()
-    ),
-    UNSAT_CORE(
-        refiner = { s, _ ->
-            ExprTraceUnsatCoreChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
-        },
-        stopCriterion = StopCriterions.firstCex()
-    ),
-    UCB(
-        refiner = { s, _ ->
-            ExprTraceUCBChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
-        },
-        stopCriterion = StopCriterions.firstCex()
-    ),
-
-    NWT_SP(
-        refiner = { s, _ ->
-            ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
-                .withoutIT().withSP().withoutLV()
-        },
-        stopCriterion = StopCriterions.firstCex()
-    ),
-    NWT_WP(
-        refiner = { s, _ ->
-            ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
-                .withoutIT().withWP().withoutLV()
-        },
-        stopCriterion = StopCriterions.firstCex()
-    ),
-    NWT_SP_LV(
-        refiner = { s, _ ->
-            ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
-                .withoutIT().withSP().withLV()
-        },
-        stopCriterion = StopCriterions.firstCex()
-    ),
-    NWT_WP_LV(
-        refiner = { s, _ ->
-            ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
-                .withoutIT().withWP().withLV()
-        },
-        stopCriterion = StopCriterions.firstCex()
-    ),
-    NWT_IT_WP(
-        refiner = { s, _ ->
-            ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
-                .withIT().withWP().withoutLV()
-        },
-        stopCriterion = StopCriterions.firstCex()
-    ),
-    NWT_IT_SP(
-        refiner = { s, _ ->
-            ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
-                .withIT().withSP().withoutLV()
-        },
-        stopCriterion = StopCriterions.firstCex()
-    ),
-    NWT_IT_WP_LV(
-        refiner = { s, _ ->
-            ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
-                .withIT().withWP().withLV()
-        },
-        stopCriterion = StopCriterions.firstCex()
-    ),
-    NWT_IT_SP_LV(
-        refiner = { s, _ ->
-            ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
-                .withIT().withSP().withLV()
-        },
-        stopCriterion = StopCriterions.firstCex()
-    )
+  FW_BIN_ITP(
+    refiner = { s, _ ->
+      ExprTraceFwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(), s.createItpSolver())
+    },
+    stopCriterion = StopCriterions.firstCex(),
+  ),
+  BW_BIN_ITP(
+    refiner = { s, _ ->
+      ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(), s.createItpSolver())
+    },
+    stopCriterion = StopCriterions.firstCex(),
+  ),
+  SEQ_ITP(
+    refiner = { s, _ ->
+      ExprTraceSeqItpChecker.create(BoolExprs.True(), BoolExprs.True(), s.createItpSolver())
+    },
+    stopCriterion = StopCriterions.firstCex(),
+  ),
+  MULTI_SEQ(
+    refiner = { s, m ->
+      if (m == CexMonitorOptions.CHECK) error("CexMonitor is not implemented for MULTI_SEQ")
+      ExprTraceSeqItpChecker.create(BoolExprs.True(), BoolExprs.True(), s.createItpSolver())
+    },
+    stopCriterion = StopCriterions.fullExploration(),
+  ),
+  UNSAT_CORE(
+    refiner = { s, _ ->
+      ExprTraceUnsatCoreChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
+    },
+    stopCriterion = StopCriterions.firstCex(),
+  ),
+  UCB(
+    refiner = { s, _ ->
+      ExprTraceUCBChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
+    },
+    stopCriterion = StopCriterions.firstCex(),
+  ),
+  NWT_SP(
+    refiner = { s, _ ->
+      ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
+        .withoutIT()
+        .withSP()
+        .withoutLV()
+    },
+    stopCriterion = StopCriterions.firstCex(),
+  ),
+  NWT_WP(
+    refiner = { s, _ ->
+      ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
+        .withoutIT()
+        .withWP()
+        .withoutLV()
+    },
+    stopCriterion = StopCriterions.firstCex(),
+  ),
+  NWT_SP_LV(
+    refiner = { s, _ ->
+      ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
+        .withoutIT()
+        .withSP()
+        .withLV()
+    },
+    stopCriterion = StopCriterions.firstCex(),
+  ),
+  NWT_WP_LV(
+    refiner = { s, _ ->
+      ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
+        .withoutIT()
+        .withWP()
+        .withLV()
+    },
+    stopCriterion = StopCriterions.firstCex(),
+  ),
+  NWT_IT_WP(
+    refiner = { s, _ ->
+      ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
+        .withIT()
+        .withWP()
+        .withoutLV()
+    },
+    stopCriterion = StopCriterions.firstCex(),
+  ),
+  NWT_IT_SP(
+    refiner = { s, _ ->
+      ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
+        .withIT()
+        .withSP()
+        .withoutLV()
+    },
+    stopCriterion = StopCriterions.firstCex(),
+  ),
+  NWT_IT_WP_LV(
+    refiner = { s, _ ->
+      ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
+        .withIT()
+        .withWP()
+        .withLV()
+    },
+    stopCriterion = StopCriterions.firstCex(),
+  ),
+  NWT_IT_SP_LV(
+    refiner = { s, _ ->
+      ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
+        .withIT()
+        .withSP()
+        .withLV()
+    },
+    stopCriterion = StopCriterions.firstCex(),
+  ),
 }
 
-
 enum class ExprSplitterOptions(val exprSplitter: ExprSplitter) {
-    WHOLE(ExprSplitters.whole()),
-    CONJUNCTS(ExprSplitters.conjuncts()),
-    ATOMS(ExprSplitters.atoms());
+  WHOLE(ExprSplitters.whole()),
+  CONJUNCTS(ExprSplitters.conjuncts()),
+  ATOMS(ExprSplitters.atoms()),
 }
 
 enum class Search {
-    BFS {
+  BFS {
 
-        override fun getComp(cfa: XCFA): ArgNodeComparator {
-            return ArgNodeComparators.combine(ArgNodeComparators.targetFirst(),
-                ArgNodeComparators.bfs())
-        }
-    },
-    DFS {
+    override fun getComp(cfa: XCFA): ArgNodeComparator {
+      return ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs())
+    }
+  },
+  DFS {
 
-        override fun getComp(cfa: XCFA): ArgNodeComparator {
-            return ArgNodeComparators.combine(ArgNodeComparators.targetFirst(),
-                ArgNodeComparators.dfs())
-        }
-    },
-    ERR {
+    override fun getComp(cfa: XCFA): ArgNodeComparator {
+      return ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.dfs())
+    }
+  },
+  ERR {
 
-        override fun getComp(cfa: XCFA): ArgNodeComparator {
-            return XcfaDistToErrComparator(cfa)
-        }
-    };
+    override fun getComp(cfa: XCFA): ArgNodeComparator {
+      return XcfaDistToErrComparator(cfa)
+    }
+  };
 
-    abstract fun getComp(cfa: XCFA): ArgNodeComparator
+  abstract fun getComp(cfa: XCFA): ArgNodeComparator
 }
 
 enum class InitPrec(
-    val explPrec: (xcfa: XCFA) -> XcfaPrec<PtrPrec<ExplPrec>>,
-    val predPrec: (xcfa: XCFA) -> XcfaPrec<PtrPrec<PredPrec>>,
+  val explPrec: (xcfa: XCFA) -> XcfaPrec<PtrPrec<ExplPrec>>,
+  val predPrec: (xcfa: XCFA) -> XcfaPrec<PtrPrec<PredPrec>>,
 ) {
 
-    EMPTY(
-        explPrec = { XcfaPrec(PtrPrec(ExplPrec.empty(), emptySet())) },
-        predPrec = { XcfaPrec(PtrPrec(PredPrec.of(), emptySet())) }
-    ),
-    ALLVARS(
-        explPrec = { xcfa -> XcfaPrec(PtrPrec(ExplPrec.of(xcfa.collectVars()), emptySet())) },
-        predPrec = { error("ALLVARS is not interpreted for the predicate domain.") }
-    ),
-    ALLGLOBALS(
-        explPrec = { xcfa -> XcfaPrec(PtrPrec(ExplPrec.of(xcfa.vars.map { it.wrappedVar }), emptySet())) },
-        predPrec = { error("ALLGLOBALS is not interpreted for the predicate domain.") }
-    ),
-    ALLASSUMES(
-        explPrec = { xcfa ->
-            XcfaPrec(
-                PtrPrec(ExplPrec.of(xcfa.collectAssumes().flatMap(ExprUtils::getVars)), emptySet()))
-        },
-        predPrec = { xcfa -> XcfaPrec(PtrPrec(PredPrec.of(xcfa.collectAssumes()), emptySet())) },
-    ),
-
+  EMPTY(
+    explPrec = { XcfaPrec(PtrPrec(ExplPrec.empty(), emptySet())) },
+    predPrec = { XcfaPrec(PtrPrec(PredPrec.of(), emptySet())) },
+  ),
+  ALLVARS(
+    explPrec = { xcfa -> XcfaPrec(PtrPrec(ExplPrec.of(xcfa.collectVars()), emptySet())) },
+    predPrec = { error("ALLVARS is not interpreted for the predicate domain.") },
+  ),
+  ALLGLOBALS(
+    explPrec = { xcfa ->
+      XcfaPrec(PtrPrec(ExplPrec.of(xcfa.vars.map { it.wrappedVar }), emptySet()))
+    },
+    predPrec = { error("ALLGLOBALS is not interpreted for the predicate domain.") },
+  ),
+  ALLASSUMES(
+    explPrec = { xcfa ->
+      XcfaPrec(PtrPrec(ExplPrec.of(xcfa.collectAssumes().flatMap(ExprUtils::getVars)), emptySet()))
+    },
+    predPrec = { xcfa -> XcfaPrec(PtrPrec(PredPrec.of(xcfa.collectAssumes()), emptySet())) },
+  ),
 }
 
 enum class ConeOfInfluenceMode(
-    val getLts: (XCFA, MutableMap<VarDecl<*>, MutableSet<ExprState>>, POR) -> LTS<XcfaState<out PtrState<out ExprState>>, XcfaAction>
+  val getLts:
+    (XCFA, MutableMap<VarDecl<*>, MutableSet<ExprState>>, POR) -> LTS<
+        XcfaState<out PtrState<out ExprState>>,
+        XcfaAction,
+      >
 ) {
 
-    NO_COI({ xcfa, ivr, por ->
-        por.getLts(xcfa, ivr).also { NO_COI.porLts = it }
-    }),
-    COI({ xcfa, ivr, por ->
-        ConeOfInfluence.coreLts = por.getLts(xcfa, ivr).also { COI.porLts = it }
-        ConeOfInfluence.lts
-    }),
-    POR_COI({ xcfa, ivr, por ->
-        ConeOfInfluence.coreLts = getXcfaLts()
-        if (por.isAbstractionAware) XcfaAasporCoiLts(xcfa, ivr, ConeOfInfluence.lts)
-        else XcfaSporCoiLts(xcfa, ConeOfInfluence.lts)
-    }),
-    POR_COI_POR({ xcfa, ivr, por ->
-        ConeOfInfluence.coreLts = por.getLts(xcfa, ivr).also { POR_COI_POR.porLts = it }
-        if (por.isAbstractionAware) XcfaAasporCoiLts(xcfa, ivr, ConeOfInfluence.lts)
-        else XcfaSporCoiLts(xcfa, ConeOfInfluence.lts)
-    })
-    ;
+  NO_COI({ xcfa, ivr, por -> por.getLts(xcfa, ivr).also { NO_COI.porLts = it } }),
+  COI({ xcfa, ivr, por ->
+    ConeOfInfluence.coreLts = por.getLts(xcfa, ivr).also { COI.porLts = it }
+    ConeOfInfluence.lts
+  }),
+  POR_COI({ xcfa, ivr, por ->
+    ConeOfInfluence.coreLts = getXcfaLts()
+    if (por.isAbstractionAware) XcfaAasporCoiLts(xcfa, ivr, ConeOfInfluence.lts)
+    else XcfaSporCoiLts(xcfa, ConeOfInfluence.lts)
+  }),
+  POR_COI_POR({ xcfa, ivr, por ->
+    ConeOfInfluence.coreLts = por.getLts(xcfa, ivr).also { POR_COI_POR.porLts = it }
+    if (por.isAbstractionAware) XcfaAasporCoiLts(xcfa, ivr, ConeOfInfluence.lts)
+    else XcfaSporCoiLts(xcfa, ConeOfInfluence.lts)
+  });
 
-    var porLts: LTS<XcfaState<out PtrState<out ExprState>>, XcfaAction>? = null
+  var porLts: LTS<XcfaState<out PtrState<out ExprState>>, XcfaAction>? = null
 }
 
 // TODO CexMonitor: disable for multi_seq
 // TODO add new monitor to xsts cli
 enum class CexMonitorOptions {
 
-    CHECK,
-    DISABLE
+  CHECK,
+  DISABLE,
 }
diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java
index 35b38b2a27..016d828fcb 100644
--- a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java
+++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java
@@ -13,18 +13,20 @@
  *  See the License for the specific language governing permissions and
  *  limitations under the License.
  */
-
 package hu.bme.mit.theta.xsts.analysis.config;
 
+import static com.google.common.base.Preconditions.checkState;
+import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Not;
+
 import hu.bme.mit.theta.analysis.*;
+import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
 import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder;
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgNodeComparators;
-import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
-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.CegarChecker;
-import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner;
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgAbstractor;
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgCegarChecker;
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgRefiner;
+import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor;
 import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterion;
 import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterions;
 import hu.bme.mit.theta.analysis.expl.*;
@@ -60,16 +62,12 @@
 import hu.bme.mit.theta.xsts.analysis.initprec.*;
 import hu.bme.mit.theta.xsts.analysis.util.XstsCombineExtractUtilsKt;
 import hu.bme.mit.theta.xsts.analysis.util.XstsControlInitFuncKt;
-
 import java.util.HashSet;
 import java.util.List;
 import java.util.Set;
 import java.util.function.Function;
 import java.util.function.Predicate;
 
-import static com.google.common.base.Preconditions.checkState;
-import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Not;
-
 public class XstsConfigBuilder {
 
     //////////// CEGAR configuration ////////////
@@ -94,20 +92,26 @@ public enum Domain {
     public enum Refinement {
         FW_BIN_ITP {
             @Override
-            public ExprTraceChecker<ItpRefutation> getItpExprTraceChecker(Expr<BoolType> init, Expr<BoolType> target, ItpSolver solver) {
+            public ExprTraceChecker<ItpRefutation> getItpExprTraceChecker(
+                    Expr<BoolType> init, Expr<BoolType> target, ItpSolver solver) {
                 return ExprTraceFwBinItpChecker.create(init, target, solver);
             }
-        }, BW_BIN_ITP {
+        },
+        BW_BIN_ITP {
             @Override
-            public ExprTraceChecker<ItpRefutation> getItpExprTraceChecker(Expr<BoolType> init, Expr<BoolType> target, ItpSolver solver) {
+            public ExprTraceChecker<ItpRefutation> getItpExprTraceChecker(
+                    Expr<BoolType> init, Expr<BoolType> target, ItpSolver solver) {
                 return ExprTraceBwBinItpChecker.create(init, target, solver);
             }
-        }, SEQ_ITP {
+        },
+        SEQ_ITP {
             @Override
-            public ExprTraceChecker<ItpRefutation> getItpExprTraceChecker(Expr<BoolType> init, Expr<BoolType> target, ItpSolver solver) {
+            public ExprTraceChecker<ItpRefutation> getItpExprTraceChecker(
+                    Expr<BoolType> init, Expr<BoolType> target, ItpSolver solver) {
                 return ExprTraceSeqItpChecker.create(init, target, solver);
             }
-        }, UNSAT_CORE,
+        },
+        UNSAT_CORE,
         MULTI_SEQ {
             @Override
             public <S extends ExprState> StopCriterion<S, XstsAction> getStopCriterion() {
@@ -115,19 +119,20 @@ public <S extends ExprState> StopCriterion<S, XstsAction> getStopCriterion() {
             }
 
             @Override
-            public ExprTraceChecker<ItpRefutation> getItpExprTraceChecker(Expr<BoolType> init, Expr<BoolType> target, ItpSolver solver) {
+            public ExprTraceChecker<ItpRefutation> getItpExprTraceChecker(
+                    Expr<BoolType> init, Expr<BoolType> target, ItpSolver solver) {
                 return ExprTraceSeqItpChecker.create(init, target, solver);
             }
 
             @Override
-            public <S extends ExprState, P extends Prec, R extends Refutation> Refiner<XstsState<S>, XstsAction, P>
-            createRefiner(
-                    ExprTraceChecker<R> traceChecker,
-                    RefutationToPrec<P, R> refToPrec,
-                    PruneStrategy pruneStrategy,
-                    Logger logger
-            ) {
-                return MultiExprTraceRefiner.create(traceChecker, JoiningPrecRefiner.create(refToPrec), pruneStrategy, logger);
+            public <S extends ExprState, P extends Prec, R extends Refutation>
+                    ArgRefiner<XstsState<S>, XstsAction, P> createRefiner(
+                            ExprTraceChecker<R> traceChecker,
+                            RefutationToPrec<P, R> refToPrec,
+                            PruneStrategy pruneStrategy,
+                            Logger logger) {
+                return MultiExprTraceRefiner.create(
+                        traceChecker, JoiningPrecRefiner.create(refToPrec), pruneStrategy, logger);
             }
         };
 
@@ -136,23 +141,22 @@ public <S extends ExprState> StopCriterion<S, XstsAction> getStopCriterion() {
         }
 
         public ExprTraceChecker<ItpRefutation> getItpExprTraceChecker(
-                final Expr<BoolType> init,
-                final Expr<BoolType> target,
-                final ItpSolver solver
-        ) {
-            throw new UnsupportedOperationException(String.format("%s domain can't provide trace checker of ItpRefutation", this.getClass().getSimpleName()));
+                final Expr<BoolType> init, final Expr<BoolType> target, final ItpSolver solver) {
+            throw new UnsupportedOperationException(
+                    String.format(
+                            "%s domain can't provide trace checker of ItpRefutation",
+                            this.getClass().getSimpleName()));
+        }
+
+        public <S extends ExprState, P extends Prec, R extends Refutation>
+                ArgRefiner<XstsState<S>, XstsAction, P> createRefiner(
+                        ExprTraceChecker<R> traceChecker,
+                        RefutationToPrec<P, R> refToPrec,
+                        PruneStrategy pruneStrategy,
+                        Logger logger) {
+            return SingleExprTraceRefiner.create(
+                    traceChecker, JoiningPrecRefiner.create(refToPrec), pruneStrategy, logger);
         }
-
-        public <S extends ExprState, P extends Prec, R extends Refutation> Refiner<XstsState<S>, XstsAction, P>
-        createRefiner(
-                ExprTraceChecker<R> traceChecker,
-                RefutationToPrec<P, R> refToPrec,
-                PruneStrategy pruneStrategy,
-                Logger logger
-        ) {
-            return SingleExprTraceRefiner.create(traceChecker, JoiningPrecRefiner.create(refToPrec), pruneStrategy, logger);
-        }
-
     }
 
     public enum Search {
@@ -165,7 +169,6 @@ public enum Search {
         Search(final ArgNodeComparators.ArgNodeComparator comparator) {
             this.comparator = comparator;
         }
-
     }
 
     public enum PredSplit {
@@ -196,7 +199,6 @@ public enum InitPrec {
         InitPrec(final XstsInitPrec builder) {
             this.builder = builder;
         }
-
     }
 
     public enum AutoExpl {
@@ -214,7 +216,8 @@ public enum AutoExpl {
     }
 
     public enum OptimizeStmts {
-        ON, OFF
+        ON,
+        OFF
     }
 
     private Logger logger = NullLogger.getInstance();
@@ -230,8 +233,11 @@ public enum OptimizeStmts {
     private OptimizeStmts optimizeStmts = OptimizeStmts.ON;
     private AutoExpl autoExpl = AutoExpl.NEWOPERANDS;
 
-    public XstsConfigBuilder(final Domain domain, final Refinement refinement,
-                             final SolverFactory abstractionSolverFactory, final SolverFactory refinementSolverFactory) {
+    public XstsConfigBuilder(
+            final Domain domain,
+            final Refinement refinement,
+            final SolverFactory abstractionSolverFactory,
+            final SolverFactory refinementSolverFactory) {
         this.domain = domain;
         this.refinement = refinement;
         this.abstractionSolverFactory = abstractionSolverFactory;
@@ -282,12 +288,15 @@ public XstsConfigBuilder autoExpl(final AutoExpl autoExpl) {
         if (domain == Domain.EXPL) {
             return (new ExplStrategy(xsts)).buildConfig();
         }
-        if (domain == Domain.PRED_BOOL || domain == Domain.PRED_CART
+        if (domain == Domain.PRED_BOOL
+                || domain == Domain.PRED_CART
                 || domain == Domain.PRED_SPLIT) {
             return (new PredStrategy(xsts)).buildConfig();
         }
-        if (domain == Domain.EXPL_PRED_BOOL || domain == Domain.EXPL_PRED_CART
-                || domain == Domain.EXPL_PRED_SPLIT || domain == Domain.EXPL_PRED_COMBINED) {
+        if (domain == Domain.EXPL_PRED_BOOL
+                || domain == Domain.EXPL_PRED_CART
+                || domain == Domain.EXPL_PRED_SPLIT
+                || domain == Domain.EXPL_PRED_COMBINED) {
             return (new ProdStrategy(xsts)).buildConfig();
         }
         throw new UnsupportedOperationException(domain + " domain is not supported.");
@@ -295,15 +304,26 @@ public XstsConfigBuilder autoExpl(final AutoExpl autoExpl) {
 
     public abstract class BuilderStrategy<S extends ExprState, P extends Prec> {
 
-        protected static final String UNSUPPORTED_CONFIG_VALUE = "Builder strategy %s does not support configuration value %s as %s";
+        protected static final String UNSUPPORTED_CONFIG_VALUE =
+                "Builder strategy %s does not support configuration value %s as %s";
         protected final XSTS xsts;
         protected final Solver abstractionSolver;
         protected final Expr<BoolType> negProp;
 
         @SuppressWarnings("java:S1699")
         protected BuilderStrategy(XSTS xsts) {
-            checkState(getSupportedDomains().contains(domain), UNSUPPORTED_CONFIG_VALUE, getClass().getSimpleName(), domain, "domain");
-            checkState(getSupportedRefinements().contains(refinement), UNSUPPORTED_CONFIG_VALUE, getClass().getSimpleName(), refinement, "refinement");
+            checkState(
+                    getSupportedDomains().contains(domain),
+                    UNSUPPORTED_CONFIG_VALUE,
+                    getClass().getSimpleName(),
+                    domain,
+                    "domain");
+            checkState(
+                    getSupportedRefinements().contains(refinement),
+                    UNSUPPORTED_CONFIG_VALUE,
+                    getClass().getSimpleName(),
+                    refinement,
+                    "refinement");
             this.xsts = xsts;
             abstractionSolver = abstractionSolverFactory.createSolver();
             negProp = Not(xsts.getProp());
@@ -336,7 +356,7 @@ public XstsAnalysis<S, P> getAnalysis() {
 
         public abstract RefutationToPrec<P, ItpRefutation> getItpRefToPrec();
 
-        public Refiner<XstsState<S>, XstsAction, P> getRefiner() {
+        public ArgRefiner<XstsState<S>, XstsAction, P> getRefiner() {
             return refinement.createRefiner(
                     refinement.getItpExprTraceChecker(
                             xsts.getInitFormula(),
@@ -353,22 +373,22 @@ XstsConfig<XstsState<S>, XstsAction, P> buildConfig() {
             final LTS<XstsState<S>, XstsAction> lts = getLts();
             final Predicate<XstsState<S>> target = getPredicate();
             final Analysis<XstsState<S>, XstsAction, P> analysis = getAnalysis();
-            final ArgBuilder<XstsState<S>, XstsAction, P> argBuilder = ArgBuilder.create(
-                    lts, analysis, target,
-                    true);
-            final Abstractor<XstsState<S>, XstsAction, P> abstractor = BasicAbstractor.builder(
-                            argBuilder)
-                    .waitlist(PriorityWaitlist.create(search.comparator))
-                    .stopCriterion(refinement.getStopCriterion())
-                    .logger(logger).build();
-            final Refiner<XstsState<S>, XstsAction, P> refiner = getRefiner();
-            final SafetyChecker<ARG<XstsState<S>, XstsAction>, Trace<XstsState<S>, XstsAction>, P> checker = CegarChecker.create(
-                    abstractor, refiner,
-                    logger);
+            final ArgBuilder<XstsState<S>, XstsAction, P> argBuilder =
+                    ArgBuilder.create(lts, analysis, target, true);
+            final ArgAbstractor<XstsState<S>, XstsAction, P> abstractor =
+                    BasicArgAbstractor.builder(argBuilder)
+                            .waitlist(PriorityWaitlist.create(search.comparator))
+                            .stopCriterion(refinement.getStopCriterion())
+                            .logger(logger)
+                            .build();
+            final ArgRefiner<XstsState<S>, XstsAction, P> refiner = getRefiner();
+            final SafetyChecker<ARG<XstsState<S>, XstsAction>, Trace<XstsState<S>, XstsAction>, P>
+                    checker = ArgCegarChecker.create(abstractor, refiner, logger);
             return XstsConfig.create(checker, getInitPrec());
         }
 
-        public MultiAnalysisSide<XstsState<S>, S, XstsState<UnitState>, XstsAction, P, UnitPrec> getMultiSide() {
+        public MultiAnalysisSide<XstsState<S>, S, XstsState<UnitState>, XstsAction, P, UnitPrec>
+                getMultiSide() {
             return new MultiAnalysisSide<>(
                     getAnalysis(),
                     XstsControlInitFuncKt.xstsControlInitFunc(),
@@ -377,7 +397,6 @@ public MultiAnalysisSide<XstsState<S>, S, XstsState<UnitState>, XstsAction, P, U
                     XstsCombineExtractUtilsKt::xstsExtractDataState,
                     XstsCombineExtractUtilsKt::xstsExtractControlPrec);
         }
-
     }
 
     public class ExplStrategy extends BuilderStrategy<ExplState, ExplPrec> {
@@ -394,8 +413,12 @@ Set<Refinement> getSupportedRefinements() {
 
         public ExplStrategy(XSTS xsts) {
             super(xsts);
-            checkState(domain == Domain.EXPL,
-                    UNSUPPORTED_CONFIG_VALUE, this.getClass().getSimpleName(), domain, "domain");
+            checkState(
+                    domain == Domain.EXPL,
+                    UNSUPPORTED_CONFIG_VALUE,
+                    this.getClass().getSimpleName(),
+                    domain,
+                    "domain");
         }
 
         @Override
@@ -419,12 +442,16 @@ public RefutationToPrec<ExplPrec, ItpRefutation> getItpRefToPrec() {
         }
 
         @Override
-        public Refiner<XstsState<ExplState>, XstsAction, ExplPrec> getRefiner() {
+        public ArgRefiner<XstsState<ExplState>, XstsAction, ExplPrec> getRefiner() {
             if (refinement == Refinement.UNSAT_CORE) {
                 return SingleExprTraceRefiner.create(
-                        ExprTraceUnsatCoreChecker.create(xsts.getInitFormula(), negProp,
+                        ExprTraceUnsatCoreChecker.create(
+                                xsts.getInitFormula(),
+                                negProp,
                                 refinementSolverFactory.createUCSolver()),
-                        JoiningPrecRefiner.create(new VarsRefToExplPrec()), pruneStrategy, logger);
+                        JoiningPrecRefiner.create(new VarsRefToExplPrec()),
+                        pruneStrategy,
+                        logger);
             }
             return super.getRefiner();
         }
@@ -433,7 +460,6 @@ public Refiner<XstsState<ExplState>, XstsAction, ExplPrec> getRefiner() {
         public ExplPrec getInitPrec() {
             return initPrec.builder.createExpl(xsts);
         }
-
     }
 
     public class PredStrategy extends BuilderStrategy<PredState, PredPrec> {
@@ -444,13 +470,24 @@ Set<Domain> getSupportedDomains() {
 
         @Override
         Set<Refinement> getSupportedRefinements() {
-            return new HashSet<>(List.of(Refinement.FW_BIN_ITP, Refinement.BW_BIN_ITP, Refinement.SEQ_ITP, Refinement.MULTI_SEQ));
+            return new HashSet<>(
+                    List.of(
+                            Refinement.FW_BIN_ITP,
+                            Refinement.BW_BIN_ITP,
+                            Refinement.SEQ_ITP,
+                            Refinement.MULTI_SEQ));
         }
 
         public PredStrategy(XSTS xsts) {
             super(xsts);
-            checkState(domain == Domain.PRED_BOOL || domain == Domain.PRED_SPLIT || domain == Domain.PRED_CART,
-                    UNSUPPORTED_CONFIG_VALUE, this.getClass().getSimpleName(), domain, "domain");
+            checkState(
+                    domain == Domain.PRED_BOOL
+                            || domain == Domain.PRED_SPLIT
+                            || domain == Domain.PRED_CART,
+                    UNSUPPORTED_CONFIG_VALUE,
+                    this.getClass().getSimpleName(),
+                    domain,
+                    "domain");
         }
 
         @Override
@@ -482,55 +519,80 @@ public PredPrec getInitPrec() {
         }
     }
 
-    public class ProdStrategy extends BuilderStrategy<Prod2State<ExplState, PredState>, Prod2Prec<ExplPrec, PredPrec>> {
+    public class ProdStrategy
+            extends BuilderStrategy<
+                    Prod2State<ExplState, PredState>, Prod2Prec<ExplPrec, PredPrec>> {
 
         @Override
         Set<Domain> getSupportedDomains() {
-            return new HashSet<>(List.of(Domain.EXPL_PRED_BOOL, Domain.EXPL_PRED_CART, Domain.EXPL_PRED_SPLIT, Domain.EXPL_PRED_COMBINED));
+            return new HashSet<>(
+                    List.of(
+                            Domain.EXPL_PRED_BOOL,
+                            Domain.EXPL_PRED_CART,
+                            Domain.EXPL_PRED_SPLIT,
+                            Domain.EXPL_PRED_COMBINED));
         }
 
         @Override
         Set<Refinement> getSupportedRefinements() {
-            return new HashSet<>(List.of(Refinement.FW_BIN_ITP, Refinement.BW_BIN_ITP, Refinement.SEQ_ITP, Refinement.MULTI_SEQ));
+            return new HashSet<>(
+                    List.of(
+                            Refinement.FW_BIN_ITP,
+                            Refinement.BW_BIN_ITP,
+                            Refinement.SEQ_ITP,
+                            Refinement.MULTI_SEQ));
         }
 
         public ProdStrategy(XSTS xsts) {
             super(xsts);
-            checkState(domain == Domain.EXPL_PRED_BOOL || domain == Domain.EXPL_PRED_SPLIT
-                            || domain == Domain.EXPL_PRED_CART || domain == Domain.EXPL_PRED_COMBINED,
-                    UNSUPPORTED_CONFIG_VALUE, this.getClass().getSimpleName(), domain, "domain");
-            checkState(refinement != Refinement.UNSAT_CORE, UNSUPPORTED_CONFIG_VALUE, getClass().getSimpleName(), refinement, "refinement");
+            checkState(
+                    domain == Domain.EXPL_PRED_BOOL
+                            || domain == Domain.EXPL_PRED_SPLIT
+                            || domain == Domain.EXPL_PRED_CART
+                            || domain == Domain.EXPL_PRED_COMBINED,
+                    UNSUPPORTED_CONFIG_VALUE,
+                    this.getClass().getSimpleName(),
+                    domain,
+                    "domain");
+            checkState(
+                    refinement != Refinement.UNSAT_CORE,
+                    UNSUPPORTED_CONFIG_VALUE,
+                    getClass().getSimpleName(),
+                    refinement,
+                    "refinement");
         }
 
         @Override
         StmtOptimizer<Prod2State<ExplState, PredState>> getLtsOptimizer() {
-            return Prod2ExplPredStmtOptimizer.create(
-                    ExplStmtOptimizer.getInstance()
-            );
+            return Prod2ExplPredStmtOptimizer.create(ExplStmtOptimizer.getInstance());
         }
 
         @Override
         public Predicate<XstsState<Prod2State<ExplState, PredState>>> getPredicate() {
-            return new XstsStatePredicate<>(
-                    new ExprStatePredicate(negProp, abstractionSolver));
+            return new XstsStatePredicate<>(new ExprStatePredicate(negProp, abstractionSolver));
         }
 
         @Override
-        public Analysis<Prod2State<ExplState, PredState>, StmtAction, Prod2Prec<ExplPrec, PredPrec>> getDataAnalysis() {
-            if (domain == Domain.EXPL_PRED_BOOL || domain == Domain.EXPL_PRED_CART
+        public Analysis<Prod2State<ExplState, PredState>, StmtAction, Prod2Prec<ExplPrec, PredPrec>>
+                getDataAnalysis() {
+            if (domain == Domain.EXPL_PRED_BOOL
+                    || domain == Domain.EXPL_PRED_CART
                     || domain == Domain.EXPL_PRED_SPLIT) {
-                final PredAbstractors.PredAbstractor predAbstractor = domain.predAbstractorFunction.apply(abstractionSolver);
+                final PredAbstractors.PredAbstractor predAbstractor =
+                        domain.predAbstractorFunction.apply(abstractionSolver);
                 return Prod2Analysis.create(
                         ExplStmtAnalysis.create(abstractionSolver, xsts.getInitFormula(), maxEnum),
-                        PredAnalysis.create(abstractionSolver, predAbstractor, xsts.getInitFormula()),
+                        PredAnalysis.create(
+                                abstractionSolver, predAbstractor, xsts.getInitFormula()),
                         Prod2ExplPredPreStrengtheningOperator.create(),
                         Prod2ExplPredStrengtheningOperator.create(abstractionSolver));
             } else {
-                final Prod2ExplPredAbstractors.Prod2ExplPredAbstractor prodAbstractor = Prod2ExplPredAbstractors.booleanAbstractor(
-                        abstractionSolver);
+                final Prod2ExplPredAbstractors.Prod2ExplPredAbstractor prodAbstractor =
+                        Prod2ExplPredAbstractors.booleanAbstractor(abstractionSolver);
                 return Prod2ExplPredAnalysis.create(
                         ExplAnalysis.create(abstractionSolver, xsts.getInitFormula()),
-                        PredAnalysis.create(abstractionSolver,
+                        PredAnalysis.create(
+                                abstractionSolver,
                                 PredAbstractors.booleanAbstractor(abstractionSolver),
                                 xsts.getInitFormula()),
                         Prod2ExplPredStrengtheningOperator.create(abstractionSolver),
@@ -548,7 +610,5 @@ public RefutationToPrec<Prod2Prec<ExplPrec, PredPrec>, ItpRefutation> getItpRefT
         public Prod2Prec<ExplPrec, PredPrec> getInitPrec() {
             return initPrec.builder.createProd2ExplPred(xsts);
         }
-
     }
-
-}
\ No newline at end of file
+}
diff --git a/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/XtaAnalysisTest.java b/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/XtaAnalysisTest.java
index 592abd7ad5..6bbc845a97 100644
--- a/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/XtaAnalysisTest.java
+++ b/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/XtaAnalysisTest.java
@@ -31,8 +31,8 @@
 import hu.bme.mit.theta.analysis.LTS;
 import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder;
-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.ArgAbstractor;
+import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor;
 import hu.bme.mit.theta.analysis.unit.UnitAnalysis;
 import hu.bme.mit.theta.analysis.unit.UnitPrec;
 import hu.bme.mit.theta.analysis.unit.UnitState;
@@ -79,11 +79,11 @@ public void test() throws FileNotFoundException, IOException {
                 lts, analysis,
                 s -> false);
 
-        final Abstractor<XtaState<UnitState>, XtaAction, UnitPrec> abstractor = BasicAbstractor.builder(
+        final ArgAbstractor<XtaState<UnitState>, XtaAction, UnitPrec> abstractor = BasicArgAbstractor.builder(
                         argBuilder)
                 .projection(s -> s.getLocs()).build();
 
-        final ARG<XtaState<UnitState>, XtaAction> arg = abstractor.createArg();
+        final ARG<XtaState<UnitState>, XtaAction> arg = abstractor.createWitness();
         abstractor.check(arg, UnitPrec.getInstance());
 
         System.out.println(
diff --git a/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/XtaZoneAnalysisTest.java b/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/XtaZoneAnalysisTest.java
index 437049b128..111e451934 100644
--- a/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/XtaZoneAnalysisTest.java
+++ b/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/XtaZoneAnalysisTest.java
@@ -32,8 +32,8 @@
 import hu.bme.mit.theta.analysis.LTS;
 import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder;
-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.ArgAbstractor;
+import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor;
 import hu.bme.mit.theta.analysis.expl.ExplState;
 import hu.bme.mit.theta.analysis.impl.PrecMappingAnalysis;
 import hu.bme.mit.theta.analysis.prod2.Prod2Analysis;
@@ -91,10 +91,10 @@ public void test() throws FileNotFoundException, IOException {
         final ArgBuilder<XtaState<Prod2State<ExplState, ZoneState>>, XtaAction, ZonePrec> argBuilder = ArgBuilder
                 .create(lts, analysis, s -> false);
 
-        final Abstractor<XtaState<Prod2State<ExplState, ZoneState>>, XtaAction, ZonePrec> abstractor = BasicAbstractor
+        final ArgAbstractor<XtaState<Prod2State<ExplState, ZoneState>>, XtaAction, ZonePrec> abstractor = BasicArgAbstractor
                 .builder(argBuilder).projection(s -> s.getLocs()).build();
 
-        final ARG<XtaState<Prod2State<ExplState, ZoneState>>, XtaAction> arg = abstractor.createArg();
+        final ARG<XtaState<Prod2State<ExplState, ZoneState>>, XtaAction> arg = abstractor.createWitness();
         abstractor.check(arg, prec);
 
         System.out.println(arg.getNodes().collect(Collectors.toSet()));