From 27398b9806b9cb2017813e9da2c9f9f5d19f2860 Mon Sep 17 00:00:00 2001 From: RipplB Date: Thu, 18 Jul 2024 13:05:35 +0200 Subject: [PATCH] Change big multi test CFA encoding to LBE This really broad functional test ran for way too long. Turns out, the issue was the encoding, as SBE led to pretty big state spaces. --- .../kotlin/multi/MultiNondetDiningPhilosophersTest.kt | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/subprojects/common/multi-tests/src/test/kotlin/multi/MultiNondetDiningPhilosophersTest.kt b/subprojects/common/multi-tests/src/test/kotlin/multi/MultiNondetDiningPhilosophersTest.kt index 3234b6a198..ce30555dea 100644 --- a/subprojects/common/multi-tests/src/test/kotlin/multi/MultiNondetDiningPhilosophersTest.kt +++ b/subprojects/common/multi-tests/src/test/kotlin/multi/MultiNondetDiningPhilosophersTest.kt @@ -75,19 +75,19 @@ class MultiNondetDiningPhilosophersTest { val cfa1ConfigBuilder = CfaConfigBuilder(CfaConfigBuilder.Domain.EXPL, CfaConfigBuilder.Refinement.SEQ_ITP, Z3LegacySolverFactory.getInstance()) - cfa1ConfigBuilder.encoding(CfaConfigBuilder.Encoding.SBE) + cfa1ConfigBuilder.encoding(CfaConfigBuilder.Encoding.LBE) val cfa1ExplBuilder = cfa1ConfigBuilder.ExplStrategy(phil1cfa) val cfa2ConfigBuilder = CfaConfigBuilder(CfaConfigBuilder.Domain.EXPL, CfaConfigBuilder.Refinement.SEQ_ITP, Z3LegacySolverFactory.getInstance()) - cfa2ConfigBuilder.encoding(CfaConfigBuilder.Encoding.SBE) + cfa2ConfigBuilder.encoding(CfaConfigBuilder.Encoding.LBE) val cfa2ExplBuilder = cfa1ConfigBuilder.ExplStrategy(phil2cfa) val cfa3ConfigBuilder = CfaConfigBuilder(CfaConfigBuilder.Domain.EXPL, CfaConfigBuilder.Refinement.SEQ_ITP, Z3LegacySolverFactory.getInstance()) - cfa3ConfigBuilder.encoding(CfaConfigBuilder.Encoding.SBE) + cfa3ConfigBuilder.encoding(CfaConfigBuilder.Encoding.LBE) val cfa3ExplBuilder = cfa1ConfigBuilder.ExplStrategy(phil3cfa) val cfa4ConfigBuilder = CfaConfigBuilder(CfaConfigBuilder.Domain.EXPL, CfaConfigBuilder.Refinement.SEQ_ITP, Z3LegacySolverFactory.getInstance()) - cfa4ConfigBuilder.encoding(CfaConfigBuilder.Encoding.SBE) + cfa4ConfigBuilder.encoding(CfaConfigBuilder.Encoding.LBE) val cfa4ExplBuilder = cfa1ConfigBuilder.ExplStrategy(phil4cfa) val cfaRefToPrec = RefutationToGlobalCfaPrec(ItpRefToExplPrec(), phil1cfa.initLoc)