diff --git a/ChangeLog b/ChangeLog index 1bd4c7d75..a6a535ea8 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,7 @@ 2003-07-10 Alexandre Duret-Lutz + * src/tgbatest/spotlbtt.test: Make 100 rounds. + * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next): Fix so that !p.!Acc[g].Acc[f] + p.!Acc[g].Acc[f] + p.Acc[g].!Acc[f] is factored as !p.!Acc[g].Acc[f] + p.(!Acc[g].Acc[f] + Acc[g].!Acc[f]), diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test index 30beefbf6..15510624e 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -14,13 +14,15 @@ Algorithm GlobalOptions { - Rounds = 1 + Rounds = 100 Interactive = Never # Verbosity = 5 } FormulaOptions { + Size = 1...13 + Propositions = 6 AbbreviatedOperators = Yes GenerateMode = Normal @@ -32,7 +34,7 @@ FormulaOptions AndPriority = 10 OrPriority = 10 - + BeforePriority = 0 StrongReleasePriority = 0 WeakUntilPriority = 0