From 6e32b658758c5166a57faae8f3eb10565dd47d9a Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 27 Apr 2015 14:23:19 +0200
Subject: [PATCH] * src/twa/acc.cc: Fix BDD conversion in case of unused sets.

---
 src/twa/acc.cc | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/twa/acc.cc b/src/twa/acc.cc
index 295b603fa..b07f25db1 100644
--- a/src/twa/acc.cc
+++ b/src/twa/acc.cc
@@ -412,13 +412,14 @@ namespace spot
 
     auto used = acc_cond::acc_code::used_sets();
     unsigned c = used.count();
+    unsigned max = used.max_set();
 
     bdd_allocator ba;
     int base = ba.allocate_variables(c);
     assert(base == 0);
     std::vector<bdd> r;
     std::vector<unsigned> sets(c);
-    for (unsigned i = 0; r.size() < c; ++i)
+    for (unsigned i = 0; r.size() < max; ++i)
       {
 	if (used.has(i))
 	  {
@@ -473,6 +474,7 @@ namespace spot
 	c.append_or(std::move(rescode));
 	std::swap(c, rescode);
       }
+
     return rescode;
   }
 
@@ -483,13 +485,14 @@ namespace spot
 
     auto used = acc_cond::acc_code::used_sets();
     unsigned c = used.count();
+    unsigned max = used.max_set();
 
     bdd_allocator ba;
     int base = ba.allocate_variables(c);
     assert(base == 0);
     std::vector<bdd> r;
     std::vector<unsigned> sets(c);
-    for (unsigned i = 0; r.size() < c; ++i)
+    for (unsigned i = 0; r.size() < max; ++i)
       {
 	if (used.has(i))
 	  {
@@ -555,13 +558,14 @@ namespace spot
 
     auto used = acc_cond::acc_code::used_sets();
     unsigned c = used.count();
+    unsigned max = used.max_set();
 
     bdd_allocator ba;
     int base = ba.allocate_variables(c);
     assert(base == 0);
     std::vector<bdd> r;
     std::vector<unsigned> sets(c);
-    for (unsigned i = 0; r.size() < c; ++i)
+    for (unsigned i = 0; r.size() < max; ++i)
       {
 	if (used.has(i))
 	  {
@@ -616,6 +620,7 @@ namespace spot
       }
     auto used = acc_cond::acc_code::used_sets();
     unsigned c = used.count();
+    unsigned max = used.max_set();
 
     bdd_allocator ba;
     int base = ba.allocate_variables(c);
@@ -623,7 +628,7 @@ namespace spot
     std::vector<bdd> r;
     std::vector<unsigned> sets(c);
     bdd known = bddtrue;
-    for (unsigned i = 0; r.size() < c; ++i)
+    for (unsigned i = 0; r.size() < max; ++i)
       {
 	if (used.has(i))
 	  {