Skip to content

Commit

Permalink
Change big multi test CFA encoding to LBE
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
RipplB committed Jul 23, 2024
1 parent d3c45ff commit 27398b9
Showing 1 changed file with 4 additions and 4 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down

0 comments on commit 27398b9

Please sign in to comment.