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 acbc09b188..469e6b3a26 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
@@ -18,11 +18,12 @@
 import hu.bme.mit.theta.analysis.Analysis;
 import hu.bme.mit.theta.analysis.LTS;
 import hu.bme.mit.theta.analysis.State;
-import hu.bme.mit.theta.analysis.algorithm.ARG;
-import hu.bme.mit.theta.analysis.algorithm.ArgBuilder;
-import hu.bme.mit.theta.analysis.algorithm.ArgNodeComparators;
-import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
+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.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;
@@ -56,7 +57,7 @@
 import java.util.Collections;
 import java.util.function.Predicate;
 
-import static hu.bme.mit.theta.analysis.algorithm.ArgUtils.isWellLabeled;
+import static hu.bme.mit.theta.analysis.algorithm.arg.ArgUtils.isWellLabeled;
 import static hu.bme.mit.theta.core.decl.Decls.Var;
 import static hu.bme.mit.theta.core.type.anytype.Exprs.Prime;
 import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And;
@@ -115,11 +116,11 @@ public void test() {
 		final SingleExprTraceRefiner<ExplState, StsAction, ExplPrec, VarsRefutation> refiner = SingleExprTraceRefiner
 				.create(exprTraceChecker, JoiningPrecRefiner.create(new VarsRefToExplPrec()), PruneStrategy.LAZY, logger);
 
-		final SafetyChecker<ExplState, StsAction, ExplPrec> checker = CegarChecker.create(abstractor, refiner, logger);
+		final SafetyChecker<ARG<ExplState, StsAction>, Trace<ExplState, StsAction>, ExplPrec> checker = CegarChecker.create(abstractor, refiner, logger);
 
-		final SafetyResult<ExplState, StsAction> safetyStatus = checker.check(prec);
+		final SafetyResult<ARG<ExplState, StsAction>, Trace<ExplState, StsAction>> safetyStatus = checker.check(prec);
 
-		final ARG<ExplState, StsAction> arg = safetyStatus.getArg();
+		final ARG<ExplState, StsAction> arg = safetyStatus.getWitness();
 		assertTrue(isWellLabeled(arg, abstractionSolver));
 
 		// System.out.println(new
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 2712527c1b..256fe294e3 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
@@ -15,7 +15,7 @@
  */
 package hu.bme.mit.theta.sts.analysis;
 
-import static hu.bme.mit.theta.analysis.algorithm.ArgUtils.isWellLabeled;
+import static hu.bme.mit.theta.analysis.algorithm.arg.ArgUtils.isWellLabeled;
 import static hu.bme.mit.theta.core.decl.Decls.Var;
 import static hu.bme.mit.theta.core.type.anytype.Exprs.Prime;
 import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And;
@@ -30,6 +30,8 @@
 
 import java.util.function.Predicate;
 
+import hu.bme.mit.theta.analysis.Trace;
+import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
 import hu.bme.mit.theta.analysis.expr.refinement.*;
 import hu.bme.mit.theta.solver.ItpSolver;
 import hu.bme.mit.theta.solver.Solver;
@@ -39,10 +41,9 @@
 import hu.bme.mit.theta.analysis.Analysis;
 import hu.bme.mit.theta.analysis.LTS;
 import hu.bme.mit.theta.analysis.State;
-import hu.bme.mit.theta.analysis.algorithm.ARG;
-import hu.bme.mit.theta.analysis.algorithm.ArgBuilder;
+import hu.bme.mit.theta.analysis.algorithm.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.SafetyResult;
 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;
@@ -109,12 +110,12 @@ public void testPredPrec() {
 				.create(exprTraceChecker, JoiningPrecRefiner.create(new ItpRefToPredPrec(ExprSplitters.atoms())),
 						PruneStrategy.LAZY, logger);
 
-		final SafetyChecker<PredState, StsAction, PredPrec> checker = CegarChecker.create(abstractor, refiner, logger);
+		final SafetyChecker<ARG<PredState, StsAction>, Trace<PredState, StsAction>, PredPrec> checker = CegarChecker.create(abstractor, refiner, logger);
 
-		final SafetyResult<PredState, StsAction> safetyStatus = checker.check(prec);
+		final SafetyResult<ARG<PredState, StsAction>, Trace<PredState, StsAction>> safetyStatus = checker.check(prec);
 		System.out.println(safetyStatus);
 
-		final ARG<PredState, StsAction> arg = safetyStatus.getArg();
+		final ARG<PredState, StsAction> arg = safetyStatus.getWitness();
 		assertTrue(isWellLabeled(arg, abstractionSolver));
 
 		// System.out.println(new