From 208ff040fe41904402dda45e46b637025ad26954 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Thu, 14 Nov 2024 22:38:57 +0100 Subject: [PATCH] MDD should not cause more OOMs --- .../java/hu/bme/mit/theta/xcfa/cli/portfolio/bounded25.kt | 5 +++-- 1 file changed, 3 insertions(+), 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 index 97f345f7d8..044f6c5db4 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 @@ -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")