From 006bd6b9302dbe181c224cc34b65c2a6a9df1558 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 10 Jul 2003 12:01:41 +0000 Subject: [PATCH] * src/tgbatest/spotlbtt.test: Make 100 rounds. --- ChangeLog | 2 ++ src/tgbatest/spotlbtt.test | 6 ++++-- 2 files changed, 6 insertions(+), 2 deletions(-) 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