diff --git a/spot/twaalgos/dtbasat.cc b/spot/twaalgos/dtbasat.cc
index b3b31e195..e9b2e029e 100644
--- a/spot/twaalgos/dtbasat.cc
+++ b/spot/twaalgos/dtbasat.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
-// Développement de l'Epita.
+// Copyright (C) 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche
+// et Développement de l'Epita.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -715,9 +715,12 @@ namespace spot
   dtba_sat_synthetize(const const_twa_graph_ptr& a,
                       int target_state_number, bool state_based)
   {
+    if (a->is_alternating())
+      throw std::runtime_error
+        ("dtba_sat_synthetize() does not support alternating automata");
     if (!a->acc().is_buchi())
       throw std::runtime_error
-        ("dtba_sat() can only work with Büchi acceptance");
+        ("dtba_sat_synthetize() can only work with Büchi acceptance");
     if (target_state_number == 0)
       return nullptr;
     trace << "dtba_sat_synthetize(..., states = " << target_state_number
diff --git a/spot/twaalgos/dtwasat.cc b/spot/twaalgos/dtwasat.cc
index bcbf1171d..38547ebbf 100644
--- a/spot/twaalgos/dtwasat.cc
+++ b/spot/twaalgos/dtwasat.cc
@@ -992,6 +992,9 @@ namespace spot
                       int target_state_number,
                       bool state_based, bool colored)
   {
+    if (a->is_alternating())
+      throw std::runtime_error
+        ("dtwa_sat_synthetize() does not support alternating automata");
     if (target_state_number == 0)
       return nullptr;
     trace << "dtwa_sat_synthetize(..., nacc = " << target_acc_number