From 7f1d5f597c38a6ae2191bb1549c78ed244ef3274 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 17 May 2004 13:17:13 +0000
Subject: [PATCH] * src/misc/bddalloc.cc (bdd_allocator::varnum): Suppress.
 (bdd_allocator::bdd_allocator): Adjust. (bdd_allocator::extvarnum): Always
 call bdd_varnum(), so that it doesn't matter if the number of variable has
 been augmented externally. * src/misc/bddalloc.hh (bdd_allocator::varnum):
 Suppress.

---
 ChangeLog            |  7 +++++++
 src/misc/bddalloc.cc | 10 +++++-----
 src/misc/bddalloc.hh |  1 -
 3 files changed, 12 insertions(+), 6 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 02cc1a160..f35fbe549 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,12 @@
 2004-05-17  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* src/misc/bddalloc.cc (bdd_allocator::varnum): Suppress.
+	(bdd_allocator::bdd_allocator): Adjust.
+	(bdd_allocator::extvarnum): Always call bdd_varnum(), so that
+	it doesn't matter if the number of variable has been augmented
+	externally.
+	* src/misc/bddalloc.hh (bdd_allocator::varnum): Suppress.
+
 	* src/ltlvisit/formlength.cc: Fix style to please sanity checks.
 
 	* src/ltlvisit/lunabbrev.cc: Fix style to please sanity checks.
diff --git a/src/misc/bddalloc.cc b/src/misc/bddalloc.cc
index 9ffd54669..476eedf95 100644
--- a/src/misc/bddalloc.cc
+++ b/src/misc/bddalloc.cc
@@ -26,10 +26,9 @@
 namespace spot
 {
   bool bdd_allocator::initialized = false;
-  int bdd_allocator::varnum = 2;
 
   bdd_allocator::bdd_allocator()
-    : lvarnum(varnum)
+    : lvarnum(bdd_varnum())
   {
     initialize();
     fl.push_front(pos_lenght_pair(0, lvarnum));
@@ -46,14 +45,15 @@ namespace spot
     // to tune this.  By the meantime, we take the typical values
     // for large examples advocated by the BuDDy manual.
     bdd_init(1000000, 10000);
-    bdd_setvarnum(varnum);
+    bdd_setvarnum(2);
   }
 
   void
   bdd_allocator::extvarnum(int more)
   {
-    // If varnum has been extended from another allocator, use
-    // the new variables.
+    int varnum = bdd_varnum();
+    // If varnum has been extended from another allocator (or
+    // externally), use the new variables.
     if (lvarnum < varnum)
       {
 	more -= varnum - lvarnum;
diff --git a/src/misc/bddalloc.hh b/src/misc/bddalloc.hh
index ba3abed98..c2d145139 100644
--- a/src/misc/bddalloc.hh
+++ b/src/misc/bddalloc.hh
@@ -44,7 +44,6 @@ namespace spot
     using free_list::dump_free_list;
   protected:
     static bool initialized; ///< Whether the BDD library has been initialized.
-    static int varnum; ///< number of variables in use in the BDD library.
     int lvarnum; ///< number of variables in use in this allocator.
   private:
     /// Require more variables.