MDD should not cause more OOMs

ftsrg · Nov 14, 2024 · 208ff04 · 208ff04
1 parent 86e630f
commit 208ff04
Showing 1 changed file with 3 additions and 2 deletions.
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
@@ -94,7 +94,7 @@ fun boundedPortfolio25(
       backendConfig =
         BackendConfig(
           backend = Backend.MDD,
-          memlimit = portfolioConfig.backendConfig.memlimit,
+          memlimit = portfolioConfig.backendConfig.memlimit / 5 * 4,
           solverHome = portfolioConfig.backendConfig.solverHome,
           timeoutMs = 0,
           specConfig =
@@ -377,7 +377,8 @@ fun boundedPortfolio25(
     edges.add(Edge(bmcConfig, indConfig, if (inProcess) timeoutOrNotSolvableError else anyError))
     edges.add(Edge(indConfig, imcConfig, if (inProcess) timeoutOrNotSolvableError else anyError))
 
-    return STM(mddConfig, edges)
+    return if (inProcess) STM(mddConfig, edges)
+    else STM(bmcConfig, edges) // mdd should not be run not-in-proc
   }
 
   logger.write(Logger.Level.RESULT, "Using bounded portfolio\n")