diff --git a/NEWS b/NEWS
index 9b6681ff8..bb9d71103 100644
--- a/NEWS
+++ b/NEWS
@@ -63,6 +63,8 @@ New in spot 1.99.5a (not yet released)
   * Renamings:
     is_guarantee_automaton() -> is_terminal_automaton()
     tgba_run -> twa_run
+    dtgba_sat_synthetize() -> dtwa_sat_synthetize()
+    dtgba_sat_synthetize_dichotomy() -> dtwa_sat_synthetize_dichotomy()
 
   Python:
   * Add bindings for is_unambiguous().
diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc
index 83ec4ad73..2b908a1ef 100644
--- a/src/bin/autfilt.cc
+++ b/src/bin/autfilt.cc
@@ -55,7 +55,7 @@
 #include "twaalgos/stripacc.hh"
 #include "twaalgos/remfin.hh"
 #include "twaalgos/cleanacc.hh"
-#include "twaalgos/dtgbasat.hh"
+#include "twaalgos/dtwasat.hh"
 #include "twaalgos/complement.hh"
 #include "twaalgos/strength.hh"
 
diff --git a/src/tests/ikwiad.cc b/src/tests/ikwiad.cc
index b867e5235..8200665a7 100644
--- a/src/tests/ikwiad.cc
+++ b/src/tests/ikwiad.cc
@@ -62,7 +62,7 @@
 #include "twaalgos/remfin.hh"
 #include "twaalgos/complete.hh"
 #include "twaalgos/dtbasat.hh"
-#include "twaalgos/dtgbasat.hh"
+#include "twaalgos/dtwasat.hh"
 #include "twaalgos/stutter.hh"
 #include "twaalgos/totgba.hh"
 
@@ -367,7 +367,7 @@ checked_main(int argc, char** argv)
   bool cs_oblig = false;
   bool opt_complete = false;
   int opt_dtbasat = -1;
-  int opt_dtgbasat = -1;
+  int opt_dtwasat = -1;
 
   for (;;)
     {
@@ -679,9 +679,9 @@ checked_main(int argc, char** argv)
       else if (!strncmp(argv[formula_index], "-RG", 3))
         {
 	  if (argv[formula_index][3] != 0)
-	    opt_dtgbasat = to_int(argv[formula_index] + 3);
+	    opt_dtwasat = to_int(argv[formula_index] + 3);
 	  else
-	    opt_dtgbasat = 0;
+	    opt_dtwasat = 0;
           //output = -1;
         }
       else if (!strcmp(argv[formula_index], "-Rm"))
@@ -1191,13 +1191,13 @@ checked_main(int argc, char** argv)
 	  if (satminimized)
 	    a = satminimized;
 	}
-      else if (opt_dtgbasat >= 0)
+      else if (opt_dtwasat >= 0)
 	{
-	  tm.start("dtgbasat");
-	  auto satminimized = dtgba_sat_minimize
-	    (ensure_digraph(a), opt_dtgbasat,
-	     spot::acc_cond::generalized_buchi(opt_dtgbasat));
-	  tm.stop("dtgbasat");
+	  tm.start("dtwasat");
+	  auto satminimized = dtwa_sat_minimize
+	    (ensure_digraph(a), opt_dtwasat,
+	     spot::acc_cond::generalized_buchi(opt_dtwasat));
+	  tm.stop("dtwasat");
 	  if (satminimized)
 	    a = satminimized;
 	}
@@ -1210,7 +1210,7 @@ checked_main(int argc, char** argv)
 	}
 
       if (opt_determinize || opt_dtwacomp || opt_dtbasat >= 0
-	  || opt_dtgbasat >= 0)
+	  || opt_dtwasat >= 0)
 	{
 	  if (scc_filter && (reduction_dir_sim || reduction_rev_sim))
 	    {
diff --git a/src/twaalgos/Makefile.am b/src/twaalgos/Makefile.am
index 362c2f014..7f63b4a02 100644
--- a/src/twaalgos/Makefile.am
+++ b/src/twaalgos/Makefile.am
@@ -40,7 +40,7 @@ twaalgos_HEADERS = \
   degen.hh \
   dot.hh \
   dtbasat.hh \
-  dtgbasat.hh \
+  dtwasat.hh \
   emptiness.hh \
   emptiness_stats.hh \
   gv04.hh \
@@ -95,7 +95,7 @@ libtwaalgos_la_SOURCES = \
   degen.cc \
   dot.cc \
   dtbasat.cc \
-  dtgbasat.cc \
+  dtwasat.cc \
   emptiness.cc \
   gv04.cc \
   hoa.cc \
diff --git a/src/twaalgos/dtgbasat.cc b/src/twaalgos/dtwasat.cc
similarity index 95%
rename from src/twaalgos/dtgbasat.cc
rename to src/twaalgos/dtwasat.cc
index 8439ba6e2..bf496752e 100644
--- a/src/twaalgos/dtgbasat.cc
+++ b/src/twaalgos/dtwasat.cc
@@ -20,8 +20,8 @@
 #include <iostream>
 #include <fstream>
 #include <sstream>
-#include "dtgbasat.hh"
-#include "reachiter.hh"
+#include "dtwasat.hh"
+#include "dtbasat.hh"
 #include <map>
 #include <utility>
 #include "sccinfo.hh"
@@ -35,7 +35,6 @@
 #include "dot.hh"
 #include "complete.hh"
 #include "misc/optionmap.hh"
-#include "dtbasat.hh"
 #include "sccfilter.hh"
 #include "sbacc.hh"
 #include "postproc.hh"
@@ -46,7 +45,7 @@
 //
 // Additionally, if the following DEBUG macro is set to 1, the CNF
 // file will be output with a comment before each clause, and an
-// additional output file (dtgba-sat.dbg) will be created with a list
+// additional output file (dtwa-sat.dbg) will be created with a list
 // of all positive variables in the result and their meaning.
 
 #define DEBUG 0
@@ -602,7 +601,7 @@ namespace spot
     typedef std::pair<int, int> sat_stats;
 
     static
-    sat_stats dtgba_to_sat(std::ostream& out, const_twa_graph_ptr ref,
+    sat_stats dtwa_to_sat(std::ostream& out, const_twa_graph_ptr ref,
 			   dict& d, bool state_based, bool colored)
     {
 #if DEBUG
@@ -1037,7 +1036,7 @@ namespace spot
       const transition* last_sat_trans = nullptr;
 
 #if DEBUG
-      std::fstream out("dtgba-sat.dbg",
+      std::fstream out("dtwa-sat.dbg",
 		       std::ios_base::trunc | std::ios_base::out);
       out.exceptions(std::ifstream::failbit | std::ifstream::badbit);
       std::set<int> positive;
@@ -1119,15 +1118,15 @@ namespace spot
   }
 
   twa_graph_ptr
-  dtgba_sat_synthetize(const const_twa_graph_ptr& a,
-		       unsigned target_acc_number,
-		       const acc_cond::acc_code& target_acc,
-		       int target_state_number,
-		       bool state_based, bool colored)
+  dtwa_sat_synthetize(const const_twa_graph_ptr& a,
+		      unsigned target_acc_number,
+		      const acc_cond::acc_code& target_acc,
+		      int target_state_number,
+		      bool state_based, bool colored)
   {
     if (target_state_number == 0)
       return nullptr;
-    trace << "dtgba_sat_synthetize(..., nacc = " << target_acc_number
+    trace << "dtwa_sat_synthetize(..., nacc = " << target_acc_number
 	  << ", acc = \"" << target_acc
 	  << "\", states = " << target_state_number
 	  << ", state_based = " << state_based << ")\n";
@@ -1142,7 +1141,7 @@ namespace spot
 
     timer_map t;
     t.start("encode");
-    sat_stats s = dtgba_to_sat(solver(), a, d, state_based, colored);
+    sat_stats s = dtwa_to_sat(solver(), a, d, state_based, colored);
     t.stop("encode");
     t.start("solve");
     solution = solver.get_solution();
@@ -1186,16 +1185,16 @@ namespace spot
     if (show && res)
       print_dot(std::cout, res);
 
-    trace << "dtgba_sat_synthetize(...) = " << res << '\n';
+    trace << "dtwa_sat_synthetize(...) = " << res << '\n';
     return res;
   }
 
   twa_graph_ptr
-  dtgba_sat_minimize(const const_twa_graph_ptr& a,
-		     unsigned target_acc_number,
-		     const acc_cond::acc_code& target_acc,
-		     bool state_based, int max_states,
-		     bool colored)
+  dtwa_sat_minimize(const const_twa_graph_ptr& a,
+		    unsigned target_acc_number,
+		    const acc_cond::acc_code& target_acc,
+		    bool state_based, int max_states,
+		    bool colored)
   {
     int n_states = (max_states < 0) ?
       stats_reachable(a).states : max_states + 1;
@@ -1204,9 +1203,9 @@ namespace spot
     for (;;)
       {
 	auto next =
-	  dtgba_sat_synthetize(prev ? prev : a, target_acc_number,
-			       target_acc, --n_states,
-			       state_based, colored);
+	  dtwa_sat_synthetize(prev ? prev : a, target_acc_number,
+			      target_acc, --n_states,
+			      state_based, colored);
 	if (!next)
 	  return prev;
 	else
@@ -1217,11 +1216,11 @@ namespace spot
   }
 
   twa_graph_ptr
-  dtgba_sat_minimize_dichotomy(const const_twa_graph_ptr& a,
-			       unsigned target_acc_number,
-			       const acc_cond::acc_code& target_acc,
-			       bool state_based, int max_states,
-			       bool colored)
+  dtwa_sat_minimize_dichotomy(const const_twa_graph_ptr& a,
+			      unsigned target_acc_number,
+			      const acc_cond::acc_code& target_acc,
+			      bool state_based, int max_states,
+			      bool colored)
   {
     if (max_states < 1)
       max_states = stats_reachable(a).states - 1;
@@ -1232,9 +1231,9 @@ namespace spot
       {
 	int target = (max_states + min_states) / 2;
 	auto next =
-	  dtgba_sat_synthetize(prev ? prev : a, target_acc_number,
-			       target_acc, target, state_based,
-			       colored);
+	  dtwa_sat_synthetize(prev ? prev : a, target_acc_number,
+			      target_acc, target, state_based,
+			      colored);
 	if (!next)
 	  {
 	    min_states = target + 1;
@@ -1358,7 +1357,7 @@ namespace spot
       {
 	auto orig = a;
 	if (!target_is_buchi || !a->acc().is_buchi() || colored)
-	  a = (dicho ? dtgba_sat_minimize_dichotomy : dtgba_sat_minimize)
+	  a = (dicho ? dtwa_sat_minimize_dichotomy : dtwa_sat_minimize)
 	    (a, nacc, target_acc, state_based, max_states, colored);
 	else
 	  a = (dicho ? dtba_sat_minimize_dichotomy : dtba_sat_minimize)
@@ -1370,8 +1369,8 @@ namespace spot
     else
       {
 	if (!target_is_buchi || !a->acc().is_buchi() || colored)
-	  a = dtgba_sat_synthetize(a, nacc, target_acc, states,
-				   state_based, colored);
+	  a = dtwa_sat_synthetize(a, nacc, target_acc, states,
+				  state_based, colored);
 	else
 	  a = dtba_sat_synthetize(a, states, state_based);
       }
diff --git a/src/twaalgos/dtgbasat.hh b/src/twaalgos/dtwasat.hh
similarity index 64%
rename from src/twaalgos/dtgbasat.hh
rename to src/twaalgos/dtwasat.hh
index ba04ce1c0..61706f00b 100644
--- a/src/twaalgos/dtgbasat.hh
+++ b/src/twaalgos/dtwasat.hh
@@ -23,10 +23,10 @@
 
 namespace spot
 {
-  /// \brief Attempt to synthetize am equivalent deterministic TGBA
+  /// \brief Attempt to synthetize an equivalent deterministic TωA
   /// with a SAT solver.
   ///
-  /// \param a the input TGBA.  It should be a deterministic TGBA.
+  /// \param a the input TωA.  It should be a deterministic TωA.
   ///
   /// \param target_acc_number is the number of acceptance sets wanted
   /// in the result.
@@ -38,51 +38,50 @@ namespace spot
   /// target_state_number reachable states.
   ///
   /// \param state_based set to true to force all outgoing transitions
-  /// of a state to share the same acceptance conditions, effectively
-  /// turning the TGBA into a TBA.
+  /// of a state to share the same acceptance conditions.
   ///
   /// \param colored if true, force all transitions to belong to
   /// exactly one acceptance set.
   ///
-  /// This functions attempts to find a TGBA with \a target_acc_number
+  /// This functions attempts to find a TωA with \a target_acc_number
   /// acceptance sets and target_state_number states that is
-  /// equivalent to \a a.  If no such TGBA is found, a null pointer is
+  /// equivalent to \a a.  If no such TωA is found, a null pointer is
   /// returned.
   SPOT_API twa_graph_ptr
-  dtgba_sat_synthetize(const const_twa_graph_ptr& a,
-		       unsigned target_acc_number,
-		       const acc_cond::acc_code& target_acc,
-		       int target_state_number,
-		       bool state_based = false,
-		       bool colored = false);
+  dtwa_sat_synthetize(const const_twa_graph_ptr& a,
+		      unsigned target_acc_number,
+		      const acc_cond::acc_code& target_acc,
+		      int target_state_number,
+		      bool state_based = false,
+		      bool colored = false);
 
-  /// \brief Attempt to minimize a deterministic TGBA with a SAT solver.
+  /// \brief Attempt to minimize a deterministic TωA with a SAT solver.
   ///
-  /// This calls dtgba_sat_synthetize() in a loop, with a decreasing
+  /// This calls dtwa_sat_synthetize() in a loop, with a decreasing
   /// number of states, and returns the last successfully built TGBA.
   ///
-  /// If no smaller TGBA exist, this returns a null pointer.
+  /// If no smaller TGBA exists, this returns a null pointer.
   SPOT_API twa_graph_ptr
-  dtgba_sat_minimize(const const_twa_graph_ptr& a,
-		     unsigned target_acc_number,
-		     const acc_cond::acc_code& target_acc,
-		     bool state_based = false,
-		     int max_states = -1,
-		     bool colored = false);
+  dtwa_sat_minimize(const const_twa_graph_ptr& a,
+		    unsigned target_acc_number,
+		    const acc_cond::acc_code& target_acc,
+		    bool state_based = false,
+		    int max_states = -1,
+		    bool colored = false);
 
-  /// \brief Attempt to minimize a deterministic TGBA with a SAT solver.
+  /// \brief Attempt to minimize a deterministic TωA with a SAT solver.
   ///
-  /// This calls dtgba_sat_synthetize() in a loop, but attempting to
+  /// This calls dtwa_sat_synthetize() in a loop, but attempting to
   /// find the minimum number of states using a binary search.
   //
   /// If no smaller TBA exist, this returns a null pointer.
   SPOT_API twa_graph_ptr
-  dtgba_sat_minimize_dichotomy(const const_twa_graph_ptr& a,
-			       unsigned target_acc_number,
-			       const acc_cond::acc_code& target_acc,
-			       bool state_based = false,
-			       int max_states = -1,
-			       bool colored = false);
+  dtwa_sat_minimize_dichotomy(const const_twa_graph_ptr& a,
+			      unsigned target_acc_number,
+			      const acc_cond::acc_code& target_acc,
+			      bool state_based = false,
+			      int max_states = -1,
+			      bool colored = false);
 
   /// \brief High-level interface to SAT-based minimization
   ///
diff --git a/src/twaalgos/postproc.cc b/src/twaalgos/postproc.cc
index 3ae4e344f..06a70a0c2 100644
--- a/src/twaalgos/postproc.cc
+++ b/src/twaalgos/postproc.cc
@@ -28,7 +28,7 @@
 #include "powerset.hh"
 #include "isdet.hh"
 #include "dtbasat.hh"
-#include "dtgbasat.hh"
+#include "dtwasat.hh"
 #include "complete.hh"
 #include "totgba.hh"
 #include "sbacc.hh"
@@ -413,15 +413,15 @@ namespace spot
 	else
 	  {
 	    if (sat_states_ != -1)
-	      res = dtgba_sat_synthetize
+	      res = dtwa_sat_synthetize
 		(res, target_acc, acc_cond::generalized_buchi(target_acc),
 		 sat_states_, state_based_);
 	    else if (sat_minimize_ == 1 || sat_minimize_ == -1)
-	      res = dtgba_sat_minimize
+	      res = dtwa_sat_minimize
 		(res, target_acc, acc_cond::generalized_buchi(target_acc),
 		 state_based_);
 	    else  // sat_minimize_ == 2
-	      res = dtgba_sat_minimize_dichotomy
+	      res = dtwa_sat_minimize_dichotomy
 		(res, target_acc, acc_cond::generalized_buchi(target_acc),
 		 state_based_);
 	  }
diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i
index 02083b497..456158b9a 100644
--- a/wrap/python/spot_impl.i
+++ b/wrap/python/spot_impl.i
@@ -135,7 +135,7 @@
 #include "twaalgos/stutter.hh"
 #include "twaalgos/translate.hh"
 #include "twaalgos/hoa.hh"
-#include "twaalgos/dtgbasat.hh"
+#include "twaalgos/dtwasat.hh"
 #include "twaalgos/relabel.hh"
 
 #include "parseaut/public.hh"
@@ -315,7 +315,7 @@ namespace std {
 %include "twaalgos/stutter.hh"
 %include "twaalgos/translate.hh"
 %include "twaalgos/hoa.hh"
-%include "twaalgos/dtgbasat.hh"
+%include "twaalgos/dtwasat.hh"
 %include "twaalgos/relabel.hh"
 
 %include "parseaut/public.hh"