diff --git a/src/tgba/bdddict.cc b/src/tgba/bdddict.cc
index 8130e8d9b..4d5f558f9 100644
--- a/src/tgba/bdddict.cc
+++ b/src/tgba/bdddict.cc
@@ -159,7 +159,6 @@ namespace spot
     register_acceptance_variables(bdd_low(f), for_me);
   }
 
-
   int
   bdd_dict::register_clone_acc(int v, const void* for_me)
   {
@@ -178,6 +177,26 @@ namespace spot
     return res;
   }
 
+  const ltl::formula*
+  bdd_dict::oneacc_to_formula(int var) const
+  {
+    assert(unsigned(var) < bdd_map.size());
+    const bdd_info& i = bdd_map[var];
+    assert(i.type == acc);
+    return i.f;
+  }
+
+  const ltl::formula*
+  bdd_dict::oneacc_to_formula(bdd oneacc) const
+  {
+    assert(oneacc != bddfalse);
+    while (bdd_high(oneacc) == bddfalse)
+      {
+	oneacc = bdd_low(oneacc);
+	assert(oneacc != bddfalse);
+      }
+    return oneacc_to_formula(bdd_var(oneacc));
+  }
 
   int
   bdd_dict::register_anonymous_variables(int n, const void* for_me)
diff --git a/src/tgba/bdddict.hh b/src/tgba/bdddict.hh
index a33f9ba42..17600aeaa 100644
--- a/src/tgba/bdddict.hh
+++ b/src/tgba/bdddict.hh
@@ -148,6 +148,27 @@ namespace spot
     /// automaton).
     void register_acceptance_variables(bdd f, const void* for_me);
 
+    /// \brief Convert one acceptance condition into the associated
+    /// formula.
+    ///
+    /// This version accepts a conjunction of Acc variables, in which
+    /// only one must be positive.  This positive variable will be
+    /// converted back into the associated formula.
+    ///
+    /// The returned formula is not cloned, and is valid until the BDD
+    /// variable used in \a oneacc are unregistered.
+    const ltl::formula* oneacc_to_formula(bdd oneacc) const;
+
+    /// \brief Convert one acceptance condition into the associated
+    /// formula.
+    ///
+    /// This version takes the number of a BDD variable that must has
+    /// been returned by a call to register_acceptance_variable().
+    ///
+    /// The returned formula is not cloned, and is valid until the BDD
+    /// variable \a var is unregistered.
+    const ltl::formula* oneacc_to_formula(int var) const;
+
     /// \brief Register anonymous BDD variables.
     ///
     /// Return (and maybe allocate) \a n consecutive BDD variables which
diff --git a/src/tgbaalgos/save.cc b/src/tgbaalgos/save.cc
index f2eaa491e..320cebfaf 100644
--- a/src/tgbaalgos/save.cc
+++ b/src/tgbaalgos/save.cc
@@ -77,29 +77,16 @@ namespace spot
 	  {
 	    bdd cube = bdd_satone(acc);
 	    acc -= cube;
-	    while (cube != bddtrue)
+	    const ltl::formula* f = d->oneacc_to_formula(cube);
+	    std::string s = ltl::to_string(f);
+	    if (is_atomic_prop(f) && s[0] == '"')
 	      {
-		assert(cube != bddfalse);
-		// Display the first variable that is positive.
-		// There should be only one per satisfaction.
-		if (bdd_high(cube) != bddfalse)
-		  {
-		    int v = bdd_var(cube);
-		    const bdd_dict::bdd_info& i = d->bdd_map[v];
-		    assert(i.type == bdd_dict::acc);
-		    std::string s = ltl::to_string(i.f);
-		    if (is_atomic_prop(i.f) && s[0] == '"')
-		      {
-			// Unquote atomic propositions.
-			s.erase(s.begin());
-			s.resize(s.size() - 1);
-		      }
-		    os_ << " \"";
-		    escape_str(os_, s) << "\"";
-		    break;
-		  }
-		cube = bdd_low(cube);
+		// Unquote atomic propositions.
+		s.erase(s.begin());
+		s.resize(s.size() - 1);
 	      }
+	    os_ << " \"";
+	    escape_str(os_, s) << "\"";
 	  }
 	return os_;
       }