diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/bounded25.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/bounded25.kt
index 3d532f2b9b..5b8d481b8b 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/bounded25.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/bounded25.kt
@@ -15,9 +15,11 @@
  */
 package hu.bme.mit.theta.xcfa.cli.portfolio
 
+import hu.bme.mit.theta.analysis.algorithm.mdd.MddChecker
 import hu.bme.mit.theta.common.logging.Logger
 import hu.bme.mit.theta.frontend.ParseContext
 import hu.bme.mit.theta.frontend.transformation.ArchitectureConfig
+import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.ArithmeticTrait
 import hu.bme.mit.theta.graphsolver.patterns.constraints.MCM
 import hu.bme.mit.theta.xcfa.analysis.isInlined
 import hu.bme.mit.theta.xcfa.cli.params.*
@@ -38,7 +40,7 @@ fun boundedPortfolio25(
 
   val checker = { config: XcfaConfig<*, *> -> runConfig(config, logger, uniqueLogger, true) }
 
-  var baseConfig =
+  var boundedBaseConfig =
     XcfaConfig(
       inputConfig =
         InputConfig(
@@ -84,6 +86,29 @@ fun boundedPortfolio25(
       debugConfig = portfolioConfig.debugConfig,
     )
 
+  val mddBaseConfig =
+    XcfaConfig(
+      inputConfig = boundedBaseConfig.inputConfig,
+      frontendConfig = boundedBaseConfig.frontendConfig,
+      backendConfig =
+        BackendConfig(
+          backend = Backend.MDD,
+          solverHome = portfolioConfig.backendConfig.solverHome,
+          timeoutMs = 0,
+          specConfig =
+            MddConfig(
+              solver = "Z3",
+              validateSolver = false,
+              iterationStrategy = MddChecker.IterationStrategy.GSAT,
+              reversed = false,
+              cegar = false,
+              initPrec = InitPrec.EMPTY,
+            ),
+        ),
+      outputConfig = boundedBaseConfig.outputConfig,
+      debugConfig = boundedBaseConfig.debugConfig,
+    )
+
   if (parseContext.multiThreading) {
     throw UnsupportedOperationException("Multithreading for bounded checkers not supported")
   }
@@ -113,7 +138,7 @@ fun boundedPortfolio25(
 
   val anyError = ExceptionTrigger(label = "Anything")
 
-  fun XcfaConfig<*, BoundedConfig>.adaptConfig(
+  fun XcfaConfig<CFrontendConfig, BoundedConfig>.adaptConfig(
     bmcEnabled: Boolean = false,
     indEnabled: Boolean = false,
     itpEnabled: Boolean = false,
@@ -122,6 +147,9 @@ fun boundedPortfolio25(
     itpSolver: String = "cvc5:1.0.8",
     timeoutMs: Long = 0,
     inProcess: Boolean = this.backendConfig.inProcess,
+    reversed: Boolean = false,
+    cegar: Boolean = false,
+    initprec: InitPrec = InitPrec.EMPTY,
   ): XcfaConfig<*, BoundedConfig> {
     return copy(
       backendConfig =
@@ -130,6 +158,9 @@ fun boundedPortfolio25(
           inProcess = inProcess,
           specConfig =
             backendConfig.specConfig!!.copy(
+              reversed = reversed,
+              cegar = cegar,
+              initPrec = initprec,
               bmcConfig =
                 backendConfig.specConfig!!
                   .bmcConfig
@@ -147,95 +178,204 @@ fun boundedPortfolio25(
     )
   }
 
-  fun getStm(inProcess: Boolean): STM {
+  fun XcfaConfig<CFrontendConfig, MddConfig>.adaptConfig(
+    timeoutMs: Long = 0,
+    inProcess: Boolean = this.backendConfig.inProcess,
+  ): XcfaConfig<*, MddConfig> {
+    return copy(backendConfig = backendConfig.copy(timeoutMs = timeoutMs, inProcess = inProcess))
+  }
+
+  val canUseMathsat = !parseContext.arithmeticTraits.contains(ArithmeticTrait.FLOAT)
+
+  fun getMddConfig(inProcess: Boolean): Node =
+    ConfigNode(
+      "MddZ3-GSAT-$inProcess",
+      mddBaseConfig.adaptConfig(inProcess = inProcess, timeoutMs = 180_000),
+      checker,
+    )
+
+  fun getBmcConfig(inProcess: Boolean): Node {
     val edges = LinkedHashSet<Edge>()
+    lateinit var lastNode: ConfigNode
+
     val configBmcZ3 =
       ConfigNode(
         "BmcZ3-$inProcess",
-        baseConfig.adaptConfig(inProcess = inProcess, bmcEnabled = true, timeoutMs = 30000),
+        boundedBaseConfig.adaptConfig(inProcess = inProcess, bmcEnabled = true, timeoutMs = 30_000),
         checker,
       )
-    val configBmcMathsat =
+    lastNode = configBmcZ3
+    if (canUseMathsat) {
+      val configBmcMathsat =
+        ConfigNode(
+          "BmcMathsat-$inProcess",
+          boundedBaseConfig.adaptConfig(
+            inProcess = inProcess,
+            bmcSolver = "mathsat:5.6.10",
+            bmcEnabled = true,
+            timeoutMs = 30_000,
+          ),
+          checker,
+        )
+      edges.add(Edge(lastNode, configBmcMathsat, solverError))
+      lastNode = configBmcMathsat
+    }
+    val configBmcCvc5 =
       ConfigNode(
-        "BmcMathsat-$inProcess",
-        baseConfig.adaptConfig(
+        "BmcCvc5-$inProcess",
+        boundedBaseConfig.adaptConfig(
           inProcess = inProcess,
-          bmcSolver = "mathsat:5.6.10",
+          bmcSolver = "cvc5:1.0.8",
           bmcEnabled = true,
-          timeoutMs = 30000,
+          timeoutMs = 30_000,
         ),
         checker,
       )
-    val configIndZ3 =
+    edges.add(Edge(lastNode, configBmcCvc5, solverError))
+    lastNode = configBmcCvc5
+
+    return HierarchicalNode("BMC_$inProcess", STM(configBmcZ3, edges))
+  }
+
+  fun getKindConfig(inProcess: Boolean): Node {
+    val edges = LinkedHashSet<Edge>()
+    lateinit var lastNode: ConfigNode
+
+    val configKindZ3 =
       ConfigNode(
-        "IndZ3-$inProcess",
-        baseConfig.adaptConfig(
+        "KindZ3-$inProcess",
+        boundedBaseConfig.adaptConfig(
           inProcess = inProcess,
           bmcEnabled = true,
           indEnabled = true,
-          timeoutMs = 300000,
+          timeoutMs = 300_000,
         ),
         checker,
       )
-    val configIndMathsat =
+    lastNode = configKindZ3
+
+    val configKindCvc5 =
       ConfigNode(
-        "IndMathsat-$inProcess",
-        baseConfig.adaptConfig(
+        "KindCvc5-$inProcess",
+        boundedBaseConfig.adaptConfig(
           inProcess = inProcess,
-          bmcSolver = "mathsat:5.6.10",
-          indSolver = "mathsat:5.6.10",
           bmcEnabled = true,
           indEnabled = true,
-          timeoutMs = 300000,
+          bmcSolver = "cvc5:1.0.8",
+          indSolver = "cvc5:1.0.8",
+          timeoutMs = 300_000,
         ),
         checker,
       )
-    val configItpCvc5 =
+    edges.add(Edge(lastNode, configKindCvc5, solverError))
+    lastNode = configKindCvc5
+
+    if (canUseMathsat) {
+      val configKindMathsat =
+        ConfigNode(
+          "KindMathsat-$inProcess",
+          boundedBaseConfig.adaptConfig(
+            inProcess = inProcess,
+            bmcEnabled = true,
+            indEnabled = true,
+            bmcSolver = "mathsat:5.6.10",
+            indSolver = "mathsat:5.6.10",
+            timeoutMs = 300_000,
+          ),
+          checker,
+        )
+      edges.add(Edge(lastNode, configKindMathsat, solverError))
+      lastNode = configKindMathsat
+    }
+
+    return HierarchicalNode("KIND_$inProcess", STM(configKindZ3, edges))
+  }
+
+  fun getIMCConfig(inProcess: Boolean): Node {
+    val edges = LinkedHashSet<Edge>()
+    lateinit var lastNode: ConfigNode
+
+    val configIMCZ3abstract =
       ConfigNode(
-        "ItpCvc5-$inProcess",
-        baseConfig.adaptConfig(
+        "IMCZ3-abstract-$inProcess",
+        boundedBaseConfig.adaptConfig(
           inProcess = inProcess,
-          itpEnabled = true,
-          itpSolver = "cvc5:1.0.8",
-          timeoutMs = 0,
+          bmcEnabled = true,
+          indEnabled = true,
+          cegar = true,
+          timeoutMs = 300_000,
         ),
         checker,
       )
-    val configItpMathsat =
+    lastNode = configIMCZ3abstract
+
+    val configRIMCZ3 =
       ConfigNode(
-        "ItpMathsat-$inProcess",
-        baseConfig.adaptConfig(
+        "RIMCZ3-$inProcess",
+        boundedBaseConfig.adaptConfig(
           inProcess = inProcess,
-          itpSolver = "mathsat:5.6.10",
-          itpEnabled = true,
-          timeoutMs = 0,
+          bmcEnabled = true,
+          indEnabled = true,
+          reversed = true,
+          timeoutMs = 300_000,
         ),
         checker,
       )
+    edges.add(Edge(lastNode, configRIMCZ3, solverError))
+    lastNode = configRIMCZ3
 
-    edges.add(Edge(configBmcZ3, configBmcMathsat, solverError))
-    edges.add(
-      Edge(configBmcZ3, configIndZ3, if (inProcess) timeoutOrNotSolvableError else anyError)
-    )
-    edges.add(
-      Edge(
-        configBmcMathsat,
-        configIndMathsat,
-        if (inProcess) timeoutOrNotSolvableError else anyError,
+    val configRIMCCvc5 =
+      ConfigNode(
+        "RIMCCvc5-$inProcess",
+        boundedBaseConfig.adaptConfig(
+          inProcess = inProcess,
+          bmcEnabled = true,
+          indEnabled = true,
+          reversed = true,
+          bmcSolver = "cvc5:1.0.8",
+          indSolver = "cvc5:1.0.8",
+          timeoutMs = 300_000,
+        ),
+        checker,
       )
-    )
+    edges.add(Edge(lastNode, configRIMCCvc5, solverError))
+    lastNode = configRIMCCvc5
 
-    edges.add(Edge(configIndZ3, configIndMathsat, solverError))
-    edges.add(
-      Edge(configIndZ3, configItpCvc5, if (inProcess) timeoutOrNotSolvableError else anyError)
-    )
-    edges.add(
-      Edge(configIndMathsat, configItpCvc5, if (inProcess) timeoutOrNotSolvableError else anyError)
-    )
+    if (canUseMathsat) {
+      val configRIMCMathsat =
+        ConfigNode(
+          "RIMCMathsat-$inProcess",
+          boundedBaseConfig.adaptConfig(
+            inProcess = inProcess,
+            bmcEnabled = true,
+            indEnabled = true,
+            reversed = true,
+            bmcSolver = "mathsat:5.6.10",
+            indSolver = "mathsat:5.6.10",
+            timeoutMs = 300_000,
+          ),
+          checker,
+        )
+      edges.add(Edge(lastNode, configRIMCMathsat, solverError))
+      lastNode = configRIMCMathsat
+    }
+
+    return HierarchicalNode("IMC_$inProcess", STM(configIMCZ3abstract, edges))
+  }
+
+  fun getStm(inProcess: Boolean): STM {
+    val edges = LinkedHashSet<Edge>()
+
+    val mddConfig = getMddConfig(inProcess)
+    val bmcConfig = getBmcConfig(inProcess)
+    val indConfig = getKindConfig(inProcess)
+    val imcConfig = getIMCConfig(inProcess)
 
-    edges.add(Edge(configItpCvc5, configItpMathsat, anyError))
+    edges.add(Edge(mddConfig, bmcConfig, if (inProcess) timeoutOrNotSolvableError else anyError))
+    edges.add(Edge(bmcConfig, indConfig, if (inProcess) timeoutOrNotSolvableError else anyError))
+    edges.add(Edge(indConfig, imcConfig, if (inProcess) timeoutOrNotSolvableError else anyError))
 
-    return STM(configBmcZ3, edges)
+    return STM(mddConfig, edges)
   }
 
   logger.write(Logger.Level.RESULT, "Using bounded portfolio\n")
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/stm.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/stm.kt
index a68572f6a2..b8b33c9c21 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/stm.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/stm.kt
@@ -16,6 +16,8 @@
 package hu.bme.mit.theta.xcfa.cli.portfolio
 
 import hu.bme.mit.theta.analysis.algorithm.SafetyResult
+import hu.bme.mit.theta.xcfa.cli.params.Backend
+import hu.bme.mit.theta.xcfa.cli.params.BoundedConfig
 import hu.bme.mit.theta.xcfa.cli.params.XcfaConfig
 
 abstract class Node(val name: String) {
@@ -28,7 +30,7 @@ abstract class Node(val name: String) {
   abstract fun visualize(): String
 }
 
-class HierarchicalNode(name: String, private val innerSTM: STM) : Node(name) {
+class HierarchicalNode(name: String, val innerSTM: STM) : Node(name) {
 
   override fun execute(): Pair<Any, Any> = innerSTM.execute()
 
@@ -39,6 +41,24 @@ ${innerSTM.visualize()}
       .trimIndent()
 }
 
+fun XcfaConfig<*, *>.visualize(): String =
+  if (backendConfig.backend == Backend.BOUNDED) {
+    val specConfig = backendConfig.specConfig as BoundedConfig
+    """
+      reversed: ${specConfig.reversed}
+      abstract: ${specConfig.cegar}
+      bmc: ${!specConfig.bmcConfig.disable}
+      bmcSolver: ${specConfig.bmcConfig.bmcSolver}
+      kind: ${!specConfig.indConfig.disable}
+      kindSolver: ${specConfig.indConfig.indSolver}
+      imc: ${!specConfig.itpConfig.disable}
+      imcSolver: ${specConfig.itpConfig.itpSolver}
+    """
+      .trimIndent()
+  } else {
+    ""
+  }
+
 class ConfigNode(
   name: String,
   private val config: XcfaConfig<*, *>,
@@ -52,7 +72,7 @@ class ConfigNode(
 
   override fun visualize(): String =
     config
-      .toString()
+      .visualize()
       .lines() // TODO: reintroduce visualize()
       .map { "state ${name.replace(Regex("[:\\.-]+"), "_")}: $it" }
       .reduce { a, b -> "$a\n$b" }
@@ -108,13 +128,15 @@ data class STM(val initNode: Node, val edges: Set<Edge>) {
     }
   }
 
-  private fun visualizeNodes(): String =
-    edges
-      .map { listOf(it.source, it.target) }
-      .flatten()
-      .toSet()
-      .map { it.visualize() }
-      .reduce { a, b -> "$a\n$b" }
+  private fun visualizeNodes(): String {
+    val lastNodes = mutableSetOf<Node>()
+    val nodes = mutableSetOf(initNode)
+    while (!lastNodes.containsAll(nodes)) {
+      lastNodes.addAll(nodes)
+      nodes.addAll(nodes.flatMap { it.outEdges.map { it.target } })
+    }
+    return nodes.map { it.visualize() }.reduce { a, b -> "$a\n$b" }
+  }
 
   fun visualize(): String =
     """
diff --git a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliPortfolioTest.kt b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliPortfolioTest.kt
index bcd0d3c02b..a21bf274a3 100644
--- a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliPortfolioTest.kt
+++ b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliPortfolioTest.kt
@@ -18,7 +18,6 @@ package hu.bme.mit.theta.xcfa.cli
 import hu.bme.mit.theta.common.logging.Logger
 import hu.bme.mit.theta.common.logging.NullLogger
 import hu.bme.mit.theta.frontend.ParseContext
-import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.ArithmeticTrait
 import hu.bme.mit.theta.graphsolver.patterns.constraints.MCM
 import hu.bme.mit.theta.xcfa.cli.params.SpecBackendConfig
 import hu.bme.mit.theta.xcfa.cli.params.SpecFrontendConfig
@@ -108,20 +107,18 @@ class XcfaCliPortfolioTest {
         uniqueLogger: Logger,
       ) -> STM
   ) {
+    val stm =
+      portfolio(
+        XCFA("name", setOf()),
+        emptySet(),
+        ParseContext(),
+        XcfaConfig<SpecFrontendConfig, SpecBackendConfig>(),
+        NullLogger.getInstance(),
+        NullLogger.getInstance(),
+      )
 
-    for (value in ArithmeticTrait.values()) {
-
-      val stm =
-        portfolio(
-          XCFA("name", setOf()),
-          emptySet(),
-          ParseContext(),
-          XcfaConfig<SpecFrontendConfig, SpecBackendConfig>(),
-          NullLogger.getInstance(),
-          NullLogger.getInstance(),
-        )
-
-      Assertions.assertTrue(stm.visualize().isNotEmpty())
-    }
+    val vis = stm.visualize()
+    System.err.println(vis)
+    Assertions.assertTrue(vis.isNotEmpty())
   }
 }