diff --git a/NEWS b/NEWS
index 9a13a567f..a1bf329de 100644
--- a/NEWS
+++ b/NEWS
@@ -33,6 +33,9 @@ New in spot 1.99.5a (not yet released)
     automata already tagged as "deterministic", and "inherently-weak"
     or "weak" even for automata tagged "weak" or "terminal".
 
+  * Renamings:
+    is_guarantee_automaton() -> is_terminal_automaton()
+
   Python:
   * Add bindings for is_unambiguous().
 
diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc
index 445c71025..f3af772c7 100644
--- a/src/bin/ltlfilt.cc
+++ b/src/bin/ltlfilt.cc
@@ -589,7 +589,7 @@ namespace
 	    }
 	  else
 	    {
-	      matched &= !guarantee || is_guarantee_automaton(min);
+	      matched &= !guarantee || is_terminal_automaton(min);
 	      matched &= !safety || is_safety_mwdba(min);
 	    }
 	}
diff --git a/src/tests/ikwiad.cc b/src/tests/ikwiad.cc
index 3818b6832..045846866 100644
--- a/src/tests/ikwiad.cc
+++ b/src/tests/ikwiad.cc
@@ -1432,7 +1432,7 @@ checked_main(int argc, char** argv)
 		}
 	      else
 		{
-		  bool g = is_guarantee_automaton(ensure_digraph(a));
+		  bool g = is_terminal_automaton(ensure_digraph(a));
 		  bool s = is_safety_mwdba(ensure_digraph(a));
 		  if (g && !s)
 		    {
diff --git a/src/twaalgos/minimize.cc b/src/twaalgos/minimize.cc
index 1dc6c2c6f..c98f63845 100644
--- a/src/twaalgos/minimize.cc
+++ b/src/twaalgos/minimize.cc
@@ -590,7 +590,7 @@ namespace spot
     // the case where the input is terminal.  See issue #120.
     // (2) It would be nice to have a more precise detection of
     // terminal automata in the output.  Calling
-    // is_guarantee_automaton() seems overkill here.  But maybe we can
+    // is_terminal_automaton() seems overkill here.  But maybe we can
     // add a quick check inside minimize_dfa.
     if (a->prop_terminal())
       res->prop_terminal(true);
@@ -625,7 +625,7 @@ namespace spot
 
     // If aut_f is a guarantee automaton, the WDBA minimization must be
     // correct.
-    if (is_guarantee_automaton(aut_f))
+    if (is_terminal_automaton(aut_f))
       return min_aut_f;
 
     // Build negation automaton if not supplied.
@@ -654,10 +654,8 @@ namespace spot
 
     // If the negation is a guarantee automaton, then the
     // minimization is correct.
-    if (is_guarantee_automaton(aut_neg_f))
-      {
-	return min_aut_f;
-      }
+    if (is_terminal_automaton(aut_neg_f))
+      return min_aut_f;
 
     bool ok = false;
 
diff --git a/src/twaalgos/safety.cc b/src/twaalgos/safety.cc
index 8c142110e..3038a3288 100644
--- a/src/twaalgos/safety.cc
+++ b/src/twaalgos/safety.cc
@@ -24,8 +24,7 @@
 namespace spot
 {
   bool
-  is_guarantee_automaton(const const_twa_graph_ptr& aut,
-			 scc_info* si)
+  is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* si)
   {
     if (aut->prop_terminal())
       return true;
diff --git a/src/twaalgos/safety.hh b/src/twaalgos/safety.hh
index ee08b0ec5..3ca1ee7c7 100644
--- a/src/twaalgos/safety.hh
+++ b/src/twaalgos/safety.hh
@@ -23,30 +23,18 @@
 
 namespace spot
 {
-  /// \brief Whether an automaton represents a guarantee property.
+  /// \brief Whether an automaton is terminal.
   ///
-  /// A weak deterministic TGBA represents a guarantee property if any
-  /// accepting path ends on an accepting state with only one
-  /// transition that is a self-loop labelled by true.
-  ///
-  /// Note that in the general case, this is only a sufficient
-  /// condition : some guarantee automata might not be recognized with
-  /// this check e.g. because of some non-determinism in the
-  /// automaton.  In that case, you should interpret a \c false return
-  /// value as "I don't know".
-  ///
-  /// If you apply this function on a weak deterministic TGBA
-  /// (e.g. after a successful minimization with
-  /// minimize_obligation()), then the result leaves no doubt: false
-  /// really means that the automaton is not a guarantee property.
+  /// An automaton is terminal if any accepting path ends on an
+  /// accepting state with only one transition that is a self-loop
+  /// labelled by true.
   ///
   /// \param aut the automaton to check
   ///
   /// \param sm an scc_info object for the automaton if available (it
   /// will be built otherwise).
   SPOT_API bool
-  is_guarantee_automaton(const const_twa_graph_ptr& aut,
-			 scc_info* sm = nullptr);
+  is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* sm = nullptr);
 
   /// \brief Whether a minimized WDBA represents a safety property.
   ///
diff --git a/wrap/python/ajax/spotcgi.in b/wrap/python/ajax/spotcgi.in
index 2a1714beb..22dd49269 100755
--- a/wrap/python/ajax/spotcgi.in
+++ b/wrap/python/ajax/spotcgi.in
@@ -516,7 +516,7 @@ if output_type == 'f':
             automaton = spot.ltl_to_tgba_fm(f, dict, False, True)
             minimized = spot.minimize_obligation(automaton, f)
             if minimized != automaton:
-                g = spot.is_guarantee_automaton(minimized)
+                g = spot.is_terminal_automaton(minimized)
                 s = spot.is_safety_mwdba(minimized)
                 if s and not f.is_syntactic_safety():
                     unbufprint('<li>pathologic safety</li>')