diff --git a/ChangeLog b/ChangeLog index 949837c70..7059f134d 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,11 @@ +2011-11-13 Alexandre Duret-Lutz + + Add more nodes when resizing BDD table. + + * src/misc/bddalloc.cc (bdd_allocator::initialize): Call + bdd_setmaxincrease(500000), because the default is 50000, + which cause garbage collection to occur too often. + 2011-11-28 Alexandre Duret-Lutz * NEWS: Mention the Kripke I/O. diff --git a/src/misc/bddalloc.cc b/src/misc/bddalloc.cc index d95f899dd..fd135612a 100644 --- a/src/misc/bddalloc.cc +++ b/src/misc/bddalloc.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2007 Laboratoire de Recherche et Développement +// Copyright (C) 2007, 2011 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2006, 2007 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -56,6 +56,8 @@ namespace spot // done if Buddy is initialized by Spot. Otherwise we prefer not // to overwrite a handler that might have been set by the user.) bdd_gbc_hook(0); + // When the node time is full, add 500000 nodes, i.e., 10MB. + bdd_setmaxincrease(500000); } void