diff --git a/spot/gen/Makefile.am b/spot/gen/Makefile.am
index ed668cfd4..b8249f1e5 100644
--- a/spot/gen/Makefile.am
+++ b/spot/gen/Makefile.am
@@ -1,6 +1,6 @@
 ## -*- coding: utf-8 -*-
-## Copyright (C) 2017 Laboratoire de Recherche et Développement de l'Epita
-## (LRDE).
+## Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement
+## de l'Epita (LRDE).
 ##
 ## This file is part of Spot, a model checking library.
 ##
@@ -17,7 +17,8 @@
 ## You should have received a copy of the GNU General Public License
 ## along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
-AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS)
+AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) \
+              -I$(top_builddir)/lib -I$(top_srcdir)/lib
 AM_CXXFLAGS = $(WARNING_CXXFLAGS)
 
 spotgendir = $(pkgincludedir)/gen
diff --git a/spot/gen/automata.cc b/spot/gen/automata.cc
index e634d4e8a..bf1785dd3 100644
--- a/spot/gen/automata.cc
+++ b/spot/gen/automata.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2017 Laboratoire de Recherche et Developpement de
-// l'EPITA (LRDE).
+// Copyright (C) 2017-2018 Laboratoire de Recherche et Developpement
+// de l'EPITA (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twa/twagraph.hh>
 #include <spot/gen/automata.hh>
 #include <spot/tl/parse.hh>
diff --git a/spot/gen/formulas.cc b/spot/gen/formulas.cc
index d9dd5eab9..b50062252 100644
--- a/spot/gen/formulas.cc
+++ b/spot/gen/formulas.cc
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <cmath>
 
 #include <spot/gen/formulas.hh>
diff --git a/spot/graph/Makefile.am b/spot/graph/Makefile.am
index 9af6d639c..87723057a 100644
--- a/spot/graph/Makefile.am
+++ b/spot/graph/Makefile.am
@@ -1,5 +1,5 @@
 ## -*- coding: utf-8 -*-
-## Copyright (C) 2014 Laboratoire de Recherche et Développement de
+## Copyright (C) 2014, 2018 Laboratoire de Recherche et Développement de
 ## l'Epita (LRDE).
 ##
 ## This file is part of Spot, a model checking library.
@@ -18,7 +18,8 @@
 ## along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 
-AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir)
+AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) \
+              -I$(top_builddir)/lib -I$(top_srcdir)/lib
 AM_CXXFLAGS = $(WARNING_CXXFLAGS)
 
 graphdir = $(pkgincludedir)/graph
diff --git a/spot/kripke/Makefile.am b/spot/kripke/Makefile.am
index 2b8d80a8f..90161378e 100644
--- a/spot/kripke/Makefile.am
+++ b/spot/kripke/Makefile.am
@@ -1,5 +1,5 @@
 ## -*- coding: utf-8 -*-
-## Copyright (C) 2009, 2011, 2013, 2014, 2015 Laboratoire de Recherche
+## Copyright (C) 2009, 2011, 2013-2015, 2018 Laboratoire de Recherche
 ## et Developpement de l'Epita (LRDE).
 ##
 ## This file is part of Spot, a model checking library.
@@ -17,7 +17,8 @@
 ## You should have received a copy of the GNU General Public License
 ## along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
-AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS)
+AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) \
+              -I$(top_builddir)/lib -I$(top_srcdir)/lib
 AM_CXXFLAGS = $(WARNING_CXXFLAGS)
 
 kripkedir = $(pkgincludedir)/kripke
diff --git a/spot/kripke/fairkripke.cc b/spot/kripke/fairkripke.cc
index 5d8c059cc..70d44a2b4 100644
--- a/spot/kripke/fairkripke.cc
+++ b/spot/kripke/fairkripke.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2010, 2014, 2016 Laboratoire de Recherche et
-// Developpement de l'Epita
+// Copyright (C) 2009, 2010, 2014, 2016, 2018 Laboratoire de Recherche
+// et Developpement de l'Epita
 //
 // This file is part of Spot, a model checking library.
 //
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/kripke/fairkripke.hh>
 
 namespace spot
diff --git a/spot/kripke/kripke.cc b/spot/kripke/kripke.cc
index cbec796fa..07beb6b10 100644
--- a/spot/kripke/kripke.cc
+++ b/spot/kripke/kripke.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2010, 2014, 2016 Laboratoire de Recherche et
-// Developpement de l'Epita
+// Copyright (C) 2009, 2010, 2014, 2016, 2018 Laboratoire de Recherche
+// et Developpement de l'Epita
 //
 // This file is part of Spot, a model checking library.
 //
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/kripke/kripke.hh>
 
 namespace spot
diff --git a/spot/ltsmin/Makefile.am b/spot/ltsmin/Makefile.am
index 3204ba4c9..6f3b6ae3d 100644
--- a/spot/ltsmin/Makefile.am
+++ b/spot/ltsmin/Makefile.am
@@ -1,5 +1,5 @@
 ## -*- coding: utf-8 -*-
-## Copyright (C) 2011, 2013, 2014, 2015, 2016, 2017 Laboratoire de
+## Copyright (C) 2011, 2013, 2014, 2015, 2016, 2017, 2018 Laboratoire de
 ## Recherche et Developpement de l'Epita (LRDE).
 ##
 ## This file is part of Spot, a model checking library.
@@ -18,7 +18,8 @@
 ## along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) \
-              $(BUDDY_CPPFLAGS) $(LTDLINCL)
+              $(BUDDY_CPPFLAGS) $(LTDLINCL) \
+              -I$(top_builddir)/lib -I$(top_srcdir)/lib
 AM_CXXFLAGS = $(WARNING_CXXFLAGS)
 
 ltsmindir = $(pkgincludedir)/ltsmin
@@ -29,10 +30,12 @@ lib_LTLIBRARIES = libspotltsmin.la
 libspotltsmin_la_DEPENDENCIES = \
   $(top_builddir)/spot/libspot.la \
   $(top_builddir)/buddy/src/libbddx.la \
+  $(top_builddir)/lib/libgnu.la \
   $(LTDLDEPS)
 libspotltsmin_la_LIBADD = \
   $(top_builddir)/spot/libspot.la \
   $(top_builddir)/buddy/src/libbddx.la \
+  $(top_builddir)/lib/libgnu.la \
   $(LIBLTDL) -lpthread
 libspotltsmin_la_LDFLAGS = -no-undefined $(SYMBOLIC_LDFLAGS)
 libspotltsmin_la_SOURCES = ltsmin.cc
diff --git a/spot/ltsmin/ltsmin.cc b/spot/ltsmin/ltsmin.cc
index 7757f554a..c893793b7 100644
--- a/spot/ltsmin/ltsmin.cc
+++ b/spot/ltsmin/ltsmin.cc
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <ltdl.h>
 #include <cstring>
 #include <cstdlib>
diff --git a/spot/misc/game.cc b/spot/misc/game.cc
index b8c51587c..ea897d5e5 100644
--- a/spot/misc/game.cc
+++ b/spot/misc/game.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,10 +17,10 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
-#include <config.h>
+#include "config.h"
 
 #include <cmath>
-#include "spot/misc/game.hh"
+#include <spot/misc/game.hh>
 
 namespace spot
 {
diff --git a/spot/parseaut/Makefile.am b/spot/parseaut/Makefile.am
index 56d56fa4b..8d34c5605 100644
--- a/spot/parseaut/Makefile.am
+++ b/spot/parseaut/Makefile.am
@@ -1,6 +1,6 @@
 ## -*- coding: utf-8 -*-
-## Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement de
-## l'Epita (LRDE).
+## Copyright (C) 2013, 2014, 2018 Laboratoire de Recherche et
+## Développement de l'Epita (LRDE).
 ##
 ## This file is part of Spot, a model checking library.
 ##
@@ -17,7 +17,8 @@
 ## You should have received a copy of the GNU General Public License
 ## along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
-AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) -DYY_NO_INPUT
+AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) \
+              -DYY_NO_INPUT -I$(top_builddir)/lib -I$(top_srcdir)/lib
 # Disable -Werror because too many versions of flex yield warnings.
 AM_CXXFLAGS = $(WARNING_CXXFLAGS:-Werror=)
 
diff --git a/spot/parseaut/fmterror.cc b/spot/parseaut/fmterror.cc
index 9175a263e..49db70b41 100644
--- a/spot/parseaut/fmterror.cc
+++ b/spot/parseaut/fmterror.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
+// Copyright (C) 2013-2015, 2018 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <ostream>
 #include <spot/parseaut/public.hh>
 
diff --git a/spot/parseaut/scanaut.ll b/spot/parseaut/scanaut.ll
index aef870ae5..728404c3d 100644
--- a/spot/parseaut/scanaut.ll
+++ b/spot/parseaut/scanaut.ll
@@ -1,5 +1,5 @@
 /* -*- coding: utf-8 -*-
-** Copyright (C) 2014-2017 Laboratoire de Recherche et Développement
+** Copyright (C) 2014-2018 Laboratoire de Recherche et Développement
 ** de l'Epita (LRDE).
 **
 ** This file is part of Spot, a model checking library.
@@ -24,7 +24,9 @@
 %option extra-type="struct extra_data*"
 
 /* %option debug */
-
+%top{
+#include "config.h"
+}
 %{
 #include <string>
 #include <sys/stat.h>
diff --git a/spot/parsetl/Makefile.am b/spot/parsetl/Makefile.am
index 3a8edf31e..d98c9ebab 100644
--- a/spot/parsetl/Makefile.am
+++ b/spot/parsetl/Makefile.am
@@ -1,6 +1,6 @@
 ## -*- coding: utf-8 -*-
-## Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015
-## Laboratoire de Recherche et Développement de l'Epita (LRDE).
+## Copyright (C) 2008-2015, 2018 Laboratoire de Recherche et
+## Développement de l'Epita (LRDE).
 ## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris
 ## 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 ## Université Pierre et Marie Curie.
@@ -20,7 +20,8 @@
 ## You should have received a copy of the GNU General Public License
 ## along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
-AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) -DYY_NO_INPUT
+AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) -DYY_NO_INPUT \
+              -I$(top_builddir)/lib -I$(top_srcdir)/lib
 # Disable -Werror because too many versions of flex yield warnings.
 AM_CXXFLAGS = $(WARNING_CXXFLAGS:-Werror=)
 
diff --git a/spot/parsetl/fmterror.cc b/spot/parsetl/fmterror.cc
index a8b262874..eb13c9459 100644
--- a/spot/parsetl/fmterror.cc
+++ b/spot/parsetl/fmterror.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2012, 2013, 2015, 2016 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2010, 2012-2013, 2015-2016, 2018 Laboratoire de
+// Recherche et Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris
 // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 // Université Pierre et Marie Curie.
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/tl/parse.hh>
 #include <ostream>
 #include <iterator>
diff --git a/spot/parsetl/parsetl.yy b/spot/parsetl/parsetl.yy
index 69b619252..369204f18 100644
--- a/spot/parsetl/parsetl.yy
+++ b/spot/parsetl/parsetl.yy
@@ -1,6 +1,6 @@
 /* -*- coding: utf-8 -*-
 
-** Copyright (C) 2009-2017 Laboratoire de Recherche et Développement
+** Copyright (C) 2009-2018 Laboratoire de Recherche et Développement
 ** de l'Epita (LRDE).
 ** Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6
 ** (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@@ -33,6 +33,7 @@
 
 %code requires
 {
+#include "config.h"
 #include <string>
 #include <sstream>
 #include <spot/tl/parse.hh>
diff --git a/spot/parsetl/scantl.ll b/spot/parsetl/scantl.ll
index 256543726..4f2c53512 100644
--- a/spot/parsetl/scantl.ll
+++ b/spot/parsetl/scantl.ll
@@ -1,5 +1,5 @@
 /* -*- coding: utf-8 -*-
-** Copyright (C) 2010-2015, 2017, Laboratoire de Recherche et
+** Copyright (C) 2010-2015, 2017, 2018, Laboratoire de Recherche et
 ** Développement de l'Epita (LRDE).
 ** Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
 ** département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -26,6 +26,9 @@
 %option stack
 %option never-interactive
 
+%top{
+#include "config.h"
+}
 %{
 #include <cstdlib>
 #include <string>
diff --git a/spot/priv/Makefile.am b/spot/priv/Makefile.am
index 09c35cb1c..13317e41d 100644
--- a/spot/priv/Makefile.am
+++ b/spot/priv/Makefile.am
@@ -1,6 +1,6 @@
 ## -*- coding: utf-8 -*-
-## Copyright (C) 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche
-## et Développement de l'Epita (LRDE).
+## Copyright (C) 2013-2018 Laboratoire de Recherche et Développement
+## de l'Epita (LRDE).
 ##
 ## This file is part of Spot, a model checking library.
 ##
@@ -17,7 +17,8 @@
 ## You should have received a copy of the GNU General Public License
 ## along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
-AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS)
+AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) \
+	      -I$(top_builddir)/lib -I$(top_srcdir)/lib
 AM_CXXFLAGS = $(WARNING_CXXFLAGS)
 
 noinst_LTLIBRARIES = libpriv.la
diff --git a/spot/priv/bddalloc.cc b/spot/priv/bddalloc.cc
index 7ee299714..3ce691c0f 100644
--- a/spot/priv/bddalloc.cc
+++ b/spot/priv/bddalloc.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2007, 2011, 2014, 2015, 2017 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2007, 2011, 2014, 2015, 2017, 2018 Laboratoire de
+// Recherche et Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2006, 2007 Laboratoire d'Informatique de
 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 // Université Pierre et Marie Curie.
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <bddx.h>
 #include <cassert>
 #include <cstdlib>
diff --git a/spot/priv/freelist.cc b/spot/priv/freelist.cc
index 4b806afc9..f93c9428f 100644
--- a/spot/priv/freelist.cc
+++ b/spot/priv/freelist.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014 Laboratoire de Recherche et Développement de
+// Copyright (C) 2014, 2018 Laboratoire de Recherche et Développement de
 // l'Epita.
 // Copyright (C) 2004, 2006  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include "spot/priv/freelist.hh"
 #include <cassert>
 #include <iostream>
diff --git a/spot/priv/satcommon.cc b/spot/priv/satcommon.cc
index 999086616..6d9e0a675 100644
--- a/spot/priv/satcommon.cc
+++ b/spot/priv/satcommon.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013-2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -18,6 +18,7 @@
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 
+#include "config.h"
 #include <fstream>
 #include <set>
 #include <cassert>
diff --git a/spot/priv/trim.cc b/spot/priv/trim.cc
index 12b3c95e6..ad8dbbf64 100644
--- a/spot/priv/trim.cc
+++ b/spot/priv/trim.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015  Laboratoire de Recherche et Developpement de
-// l'Epita (LRDE).
+// Copyright (C) 2015, 2018 Laboratoire de Recherche et Developpement
+// de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/priv/trim.hh>
 #include <algorithm>
 #include <functional>
diff --git a/spot/priv/weight.cc b/spot/priv/weight.cc
index 18f0009d5..ec3e02baf 100644
--- a/spot/priv/weight.cc
+++ b/spot/priv/weight.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2014, 2016, 2017 Laboratoire de Recherche et
-// Developpement de l'Epita.
+// Copyright (C) 2011, 2014, 2016, 2017, 2018 Laboratoire de Recherche
+// et Developpement de l'Epita.
 // Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <cassert>
 #include <ostream>
 #include <spot/priv/weight.hh>
diff --git a/spot/ta/Makefile.am b/spot/ta/Makefile.am
index 3498fc64f..12f7196b1 100644
--- a/spot/ta/Makefile.am
+++ b/spot/ta/Makefile.am
@@ -1,6 +1,6 @@
 ## -*- coding: utf-8 -*-
-## Copyright (C) 2010, 2012, 2013, 2015 Laboratoire de Recherche et
-## Développement de l'Epita (LRDE).
+## Copyright (C) 2010, 2012, 2013, 2015, 2018 Laboratoire de Recherche
+## et Développement de l'Epita (LRDE).
 ##
 ## This file is part of Spot, a model checking library.
 ##
@@ -17,7 +17,8 @@
 ## You should have received a copy of the GNU General Public License
 ## along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
-AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS)
+AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) \
+              -I$(top_builddir)/lib -I$(top_srcdir)/lib
 AM_CXXFLAGS = $(WARNING_CXXFLAGS)
 
 tadir = $(pkgincludedir)/ta
diff --git a/spot/ta/ta.cc b/spot/ta/ta.cc
index f371beca9..84d3db390 100644
--- a/spot/ta/ta.cc
+++ b/spot/ta/ta.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2014 Laboratoire de Recherche et
+// Copyright (C) 2010, 2011, 2014, 2018 Laboratoire de Recherche et
 // Developpement de l Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -18,6 +18,7 @@
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 
+#include "config.h"
 #include <spot/ta/ta.hh>
 
 namespace spot
diff --git a/spot/ta/taexplicit.cc b/spot/ta/taexplicit.cc
index 075f725ed..457bf0ff8 100644
--- a/spot/ta/taexplicit.cc
+++ b/spot/ta/taexplicit.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010-2017 Laboratoire de Recherche et Développement de
+// Copyright (C) 2010-2018 Laboratoire de Recherche et Développement de
 // l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -19,6 +19,7 @@
 
 //#define TRACE
 
+#include "config.h"
 #include <iostream>
 #ifdef TRACE
 #define trace std::clog
diff --git a/spot/ta/taproduct.cc b/spot/ta/taproduct.cc
index d6975d293..f5728560d 100644
--- a/spot/ta/taproduct.cc
+++ b/spot/ta/taproduct.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012, 2014-2017 Laboratoire de Recherche et
+// Copyright (C) 2011, 2012, 2014-2018 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 //
@@ -18,6 +18,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/ta/taproduct.hh>
 #include <cassert>
 #include <spot/misc/hashfunc.hh>
diff --git a/spot/ta/tgtaexplicit.cc b/spot/ta/tgtaexplicit.cc
index 40af1632e..694636583 100644
--- a/spot/ta/tgtaexplicit.cc
+++ b/spot/ta/tgtaexplicit.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2012, 2014, 2015, 2016 Laboratoire de
+// Copyright (C) 2010-2012, 2014-2016, 2018 Laboratoire de
 // Recherche et Developpement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/ta/tgtaexplicit.hh>
 #include <spot/twa/formula2bdd.hh>
 #include <spot/twa/bddprint.hh>
diff --git a/spot/ta/tgtaproduct.cc b/spot/ta/tgtaproduct.cc
index e49c6d629..f073fbdbd 100644
--- a/spot/ta/tgtaproduct.cc
+++ b/spot/ta/tgtaproduct.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2014-2017 Laboratoire de Recherche et Développement de
+// Copyright (C) 2012, 2014-2018 Laboratoire de Recherche et Développement de
 // l Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -20,6 +20,7 @@
 
 //#define TRACE
 
+#include "config.h"
 #include <iostream>
 #ifdef TRACE
 #define trace std::clog
diff --git a/spot/taalgos/Makefile.am b/spot/taalgos/Makefile.am
index 29d15f4a8..958900947 100644
--- a/spot/taalgos/Makefile.am
+++ b/spot/taalgos/Makefile.am
@@ -1,6 +1,6 @@
 ## -*- coding: utf-8 -*-
-## Copyright (C) 2010, 2012, 2013, 2015 Laboratoire de Recherche et
-## Développement de l'Epita (LRDE).
+## Copyright (C) 2010, 2012, 2013, 2015, 2018 Laboratoire de Recherche
+## et Développement de l'Epita (LRDE).
 ##
 ## This file is part of Spot, a model checking library.
 ##
@@ -18,7 +18,8 @@
 ## along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 
-AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) -I.. $(BUDDY_CPPFLAGS)
+AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) -I.. $(BUDDY_CPPFLAGS) \
+              -I$(top_builddir)/lib -I$(top_srcdir)/lib
 AM_CXXFLAGS = $(WARNING_CXXFLAGS)
 
 taalgosdir = $(pkgincludedir)/taalgos
diff --git a/spot/taalgos/dot.cc b/spot/taalgos/dot.cc
index c6a612218..39e69e683 100644
--- a/spot/taalgos/dot.cc
+++ b/spot/taalgos/dot.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2012, 2014, 2015, 2016 Laboratoire de Recherche
+// Copyright (C) 2010, 2012, 2014-2016, 2018 Laboratoire de Recherche
 // et Developpement de l Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <ostream>
 #include <spot/taalgos/dot.hh>
 #include <spot/twa/bddprint.hh>
diff --git a/spot/taalgos/emptinessta.cc b/spot/taalgos/emptinessta.cc
index 952e54073..152afc110 100644
--- a/spot/taalgos/emptinessta.cc
+++ b/spot/taalgos/emptinessta.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire
-// de Recherche et Développement de l'Epita (LRDE).
+// Copyright (C) 2010-2016, 2018 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -19,6 +19,7 @@
 
 //#define TRACE
 
+#include "config.h"
 #include <iostream>
 #ifdef TRACE
 #define trace std::clog
diff --git a/spot/taalgos/minimize.cc b/spot/taalgos/minimize.cc
index bea3fd2e6..b2b12cb12 100644
--- a/spot/taalgos/minimize.cc
+++ b/spot/taalgos/minimize.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire
-// de Recherche et Développement de l'Epita (LRDE).
+// Copyright (C) 2010-2016, 2018 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -20,6 +20,7 @@
 
 //#define TRACE
 
+#include "config.h"
 #ifdef TRACE
 #  define trace std::cerr
 #else
diff --git a/spot/taalgos/reachiter.cc b/spot/taalgos/reachiter.cc
index f60e504dd..44f52e4d0 100644
--- a/spot/taalgos/reachiter.cc
+++ b/spot/taalgos/reachiter.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2012, 2014, 2015, 2016 Laboratoire de Recherche
+// Copyright (C) 2010, 2012, 2014-2016, 2018 Laboratoire de Recherche
 // et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <cassert>
 #include <spot/taalgos/reachiter.hh>
 
diff --git a/spot/taalgos/statessetbuilder.cc b/spot/taalgos/statessetbuilder.cc
index 7e1a611d2..68c4046fa 100644
--- a/spot/taalgos/statessetbuilder.cc
+++ b/spot/taalgos/statessetbuilder.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2014, 2016 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2010, 2014, 2016, 2018 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <iostream>
 #include <spot/ta/ta.hh>
 #include <spot/taalgos/statessetbuilder.hh>
diff --git a/spot/taalgos/stats.cc b/spot/taalgos/stats.cc
index f7851834c..1787f6a27 100644
--- a/spot/taalgos/stats.cc
+++ b/spot/taalgos/stats.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2014, 2015, 2016 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2008, 2014, 2015, 2016, 2018 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
 // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <iostream>
 #include <spot/ta/ta.hh>
 #include <spot/taalgos/stats.hh>
diff --git a/spot/taalgos/tgba2ta.cc b/spot/taalgos/tgba2ta.cc
index 434d47a46..e088ffa18 100644
--- a/spot/taalgos/tgba2ta.cc
+++ b/spot/taalgos/tgba2ta.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010-2017 Laboratoire de Recherche et Développement de
+// Copyright (C) 2010-2018 Laboratoire de Recherche et Développement de
 // l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -19,6 +19,7 @@
 
 //#define TRACE
 
+#include "config.h"
 #include <iostream>
 #ifdef TRACE
 #define trace std::clog
diff --git a/spot/tl/Makefile.am b/spot/tl/Makefile.am
index e997811b5..b7362ae99 100644
--- a/spot/tl/Makefile.am
+++ b/spot/tl/Makefile.am
@@ -1,5 +1,5 @@
 ## -*- coding: utf-8 -*-
-## Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et
+## Copyright (C) 2015-2018 Laboratoire de Recherche et
 ## Développement de l'Epita (LRDE).
 ##
 ## This file is part of Spot, a model checking library.
@@ -17,7 +17,8 @@
 ## You should have received a copy of the GNU General Public License
 ## along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
-AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS)
+AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) \
+              -I$(top_builddir)/lib -I$(top_srcdir)/lib
 AM_CXXFLAGS = $(WARNING_CXXFLAGS)
 
 tldir = $(pkgincludedir)/tl
diff --git a/spot/tl/apcollect.cc b/spot/tl/apcollect.cc
index 65b092470..e1f11372d 100644
--- a/spot/tl/apcollect.cc
+++ b/spot/tl/apcollect.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2014, 2015 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2012, 2014, 2015, 2018 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 // Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/tl/apcollect.hh>
 #include <spot/twa/twa.hh>
 #include <spot/twa/bdddict.hh>
diff --git a/spot/tl/contain.cc b/spot/tl/contain.cc
index a60a7ac3b..19c3b7158 100644
--- a/spot/tl/contain.cc
+++ b/spot/tl/contain.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2010, 2011, 2012, 2014, 2015, 2016 Laboratoire de
-// Recherche et Développement de l'Epita (LRDE).
+// Copyright (C) 2009-2012, 2014-2016, 2018 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
 // Copyright (C) 2006, 2007 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/tl/contain.hh>
 #include <spot/tl/simplify.hh>
 #include <spot/tl/formula.hh>
diff --git a/spot/tl/declenv.cc b/spot/tl/declenv.cc
index b044bc522..cad6466cd 100644
--- a/spot/tl/declenv.cc
+++ b/spot/tl/declenv.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2012, 2014, 2015 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2009, 2012, 2014, 2015, 2018 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
 // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/tl/declenv.hh>
 
 namespace spot
diff --git a/spot/tl/defaultenv.cc b/spot/tl/defaultenv.cc
index cbf817283..ae3c22643 100644
--- a/spot/tl/defaultenv.cc
+++ b/spot/tl/defaultenv.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2014, 2015 Laboratoire de Recherche et
+// Copyright (C) 2012, 2014, 2015, 2018 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 // Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/tl/defaultenv.hh>
 
 namespace spot
diff --git a/spot/tl/dot.cc b/spot/tl/dot.cc
index 1f8dbf157..be6e2ac6b 100644
--- a/spot/tl/dot.cc
+++ b/spot/tl/dot.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire
-// de Recherche et Développement de l'Epita (LRDE).
+// Copyright (C) 2009-2015, 2018 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6
 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
 // Pierre et Marie Curie.
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/tl/dot.hh>
 #include <spot/tl/formula.hh>
 #include <unordered_map>
diff --git a/spot/tl/exclusive.cc b/spot/tl/exclusive.cc
index 35e70c020..979b8fe94 100644
--- a/spot/tl/exclusive.cc
+++ b/spot/tl/exclusive.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015-2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/tl/exclusive.hh>
 #include <spot/twaalgos/mask.hh>
 #include <spot/misc/casts.hh>
@@ -154,7 +155,7 @@ namespace spot
           support &= bdd_support(t.cond);
     }
 
-    bdd restrict = bddtrue;
+    bdd restrict_ = bddtrue;
     auto d = aut->get_dict();
 
     std::vector<bdd> group;
@@ -172,7 +173,7 @@ namespace spot
         unsigned s = group.size();
         for (unsigned j = 0; j < s; ++j)
           for (unsigned k = j + 1; k < s; ++k)
-            restrict &= group[j] | group[k];
+            restrict_ &= group[j] | group[k];
       }
 
     twa_graph_ptr res = make_twa_graph(aut->get_dict());
@@ -184,8 +185,8 @@ namespace spot
         transform_accessible(aut, res, [&](unsigned, bdd& cond,
                                            acc_cond::mark_t&, unsigned)
                              {
-                               minato_isop isop(cond & restrict,
-                                                cond | !restrict,
+                               minato_isop isop(cond & restrict_,
+                                                cond | !restrict_,
                                                 true);
                                bdd res = bddfalse;
                                bdd cube = bddfalse;
@@ -200,7 +201,7 @@ namespace spot
         transform_accessible(aut, res, [&](unsigned, bdd& cond,
                                            acc_cond::mark_t&, unsigned)
                              {
-                               cond &= restrict;
+                               cond &= restrict_;
                              });
       }
     return res;
diff --git a/spot/tl/hierarchy.cc b/spot/tl/hierarchy.cc
index 4f042799a..7b9716f5a 100644
--- a/spot/tl/hierarchy.cc
+++ b/spot/tl/hierarchy.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2017 Laboratoire de Recherche et Développement de
+// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de
 // l'Epita (LRDE)
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <sstream>
 #include <spot/tl/formula.hh>
 #include <spot/tl/hierarchy.hh>
diff --git a/spot/tl/length.cc b/spot/tl/length.cc
index 789df65b2..2793a6af5 100644
--- a/spot/tl/length.cc
+++ b/spot/tl/length.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2012, 2014, 2015 Laboratoire de Recherche et
+// Copyright (C) 2010, 2012, 2014, 2015, 2018 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 // Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/tl/length.hh>
 #include <spot/tl/formula.hh>
 
diff --git a/spot/tl/ltlf.cc b/spot/tl/ltlf.cc
index 74532eabb..a6a61fe96 100644
--- a/spot/tl/ltlf.cc
+++ b/spot/tl/ltlf.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2016 Laboratoire de Recherche et Développement de
-// l'Epita (LRDE).
+// Copyright (C) 2016, 2018 Laboratoire de Recherche et Développement
+// de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/tl/ltlf.hh>
 
 namespace spot
diff --git a/spot/tl/mark.cc b/spot/tl/mark.cc
index b6e83ccca..ec17d78d3 100644
--- a/spot/tl/mark.cc
+++ b/spot/tl/mark.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2012, 2014, 2015 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2010, 2012, 2014, 2015, 2018 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/tl/mark.hh>
 #include <cassert>
 #include <algorithm>
diff --git a/spot/tl/mutation.cc b/spot/tl/mutation.cc
index 6bee8e1e8..7c704dba5 100644
--- a/spot/tl/mutation.cc
+++ b/spot/tl/mutation.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et
+// Copyright (C) 2014-2016, 2018 Laboratoire de Recherche et
 // Developpement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <set>
 #include <algorithm>
 
diff --git a/spot/tl/nenoform.cc b/spot/tl/nenoform.cc
index 7283080c8..8705960df 100644
--- a/spot/tl/nenoform.cc
+++ b/spot/tl/nenoform.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2015 Laboratoire de
+// Copyright (C) 2009-2013, 2015, 2018 Laboratoire de
 // Recherche et Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/tl/nenoform.hh>
 #include <spot/tl/simplify.hh>
 
diff --git a/spot/tl/print.cc b/spot/tl/print.cc
index f46dc4976..5bbb0cf98 100644
--- a/spot/tl/print.cc
+++ b/spot/tl/print.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2010, 2012, 2013, 2014, 2015, 2016 Laboratoire de
+// Copyright (C) 2008, 2010, 2012-2016, 2018 Laboratoire de
 // Recherche et Développement de l'Epita (LRDE)
 // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <cassert>
 #include <sstream>
 #include <ctype.h>
diff --git a/spot/tl/randomltl.cc b/spot/tl/randomltl.cc
index f7ff25162..a284b0690 100644
--- a/spot/tl/randomltl.cc
+++ b/spot/tl/randomltl.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015, 2016
-// Laboratoire de Recherche et Développement de l'Epita (LRDE).
+// Copyright (C) 2008-2012, 2014-2016, 2018 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
 // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6
 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
 // Pierre et Marie Curie.
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <cassert>
 #include <algorithm>
 #include <spot/tl/randomltl.hh>
diff --git a/spot/tl/relabel.cc b/spot/tl/relabel.cc
index 838fe19c5..383f559c1 100644
--- a/spot/tl/relabel.cc
+++ b/spot/tl/relabel.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
-// et Développement de l'Epita (LRDE).
+// Copyright (C) 2012-2016, 2018 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/tl/relabel.hh>
 #include <sstream>
 #include <spot/misc/hash.hh>
diff --git a/spot/tl/remove_x.cc b/spot/tl/remove_x.cc
index 582036103..4ab27d1d7 100644
--- a/spot/tl/remove_x.cc
+++ b/spot/tl/remove_x.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
+// Copyright (C) 2013, 2014, 2015, 2018 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/tl/simplify.hh>
 #include <spot/tl/apcollect.hh>
 #include <spot/tl/remove_x.hh>
diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc
index 8c4e82bb9..1332d24dc 100644
--- a/spot/tl/simplify.cc
+++ b/spot/tl/simplify.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011-2017 Laboratoire de Recherche et Developpement
+// Copyright (C) 2011-2018 Laboratoire de Recherche et Developpement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <iostream>
 //#define TRACE
 #ifdef TRACE
diff --git a/spot/tl/snf.cc b/spot/tl/snf.cc
index e234a44d2..e525fe6df 100644
--- a/spot/tl/snf.cc
+++ b/spot/tl/snf.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2014, 2015, 2016 Laboratoire de Recherche et
-// Developpement de l'Epita (LRDE).
+// Copyright (C) 2012, 2014, 2015, 2016, 2018 Laboratoire de Recherche
+// et Developpement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/tl/snf.hh>
 
 #if defined __clang__
diff --git a/spot/tl/unabbrev.cc b/spot/tl/unabbrev.cc
index b5daa5d7c..e0164a5ce 100644
--- a/spot/tl/unabbrev.cc
+++ b/spot/tl/unabbrev.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015 Laboratoire de Recherche et Développement
+// Copyright (C) 2015, 2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -18,6 +18,7 @@
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 
+#include "config.h"
 #include <spot/tl/unabbrev.hh>
 
 namespace spot
diff --git a/spot/twa/Makefile.am b/spot/twa/Makefile.am
index f0dde7983..f99598a8f 100644
--- a/spot/twa/Makefile.am
+++ b/spot/twa/Makefile.am
@@ -1,6 +1,6 @@
 ## -*- coding: utf-8 -*-
-## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire
-## de Recherche et Développement de l'Epita (LRDE).
+## Copyright (C) 2009-2016, 2018 Laboratoire de Recherche et
+## Développement de l'Epita (LRDE).
 ## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 ## département Systèmes Répartis Coopératifs (SRC), Université Pierre
 ## et Marie Curie.
@@ -20,7 +20,8 @@
 ## You should have received a copy of the GNU General Public License
 ## along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
-AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS)
+AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) \
+              -I$(top_builddir)/lib -I$(top_srcdir)/lib
 AM_CXXFLAGS = $(WARNING_CXXFLAGS)
 
 twadir = $(pkgincludedir)/twa
diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc
index 0c36625b5..c6df13210 100644
--- a/spot/twa/acc.cc
+++ b/spot/twa/acc.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et
-// Développement de l'Epita.
+// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement
+// de l'Epita.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -18,6 +18,7 @@
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 
+#include "config.h"
 #include <iostream>
 #include <sstream>
 #include <set>
diff --git a/spot/twa/bdddict.cc b/spot/twa/bdddict.cc
index 58d7185c3..1d83e37d5 100644
--- a/spot/twa/bdddict.cc
+++ b/spot/twa/bdddict.cc
@@ -1,9 +1,9 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2012-2017 Laboratoire de Recherche et
+// Copyright (C) 2009, 2012-2018 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
-// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
-// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
-// Université Pierre et Marie Curie.
+// Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6
+// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
+// Pierre et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <ostream>
 #include <sstream>
 #include <cassert>
diff --git a/spot/twa/bddprint.cc b/spot/twa/bddprint.cc
index 79c89d1f2..a0d4b3625 100644
--- a/spot/twa/bddprint.cc
+++ b/spot/twa/bddprint.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2012, 2014, 2015 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2009, 2012, 2014, 2015, 2018 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6
 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
 // Pierre et Marie Curie.
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <sstream>
 #include <cassert>
 #include <ostream>
diff --git a/spot/twa/formula2bdd.cc b/spot/twa/formula2bdd.cc
index f10f53ad4..d93e1ecf6 100644
--- a/spot/twa/formula2bdd.cc
+++ b/spot/twa/formula2bdd.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009-2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2009-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris
 // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <cassert>
 #include <spot/twa/formula2bdd.hh>
 #include <spot/misc/minato.hh>
diff --git a/spot/twa/taatgba.cc b/spot/twa/taatgba.cc
index 5cdab01d3..27f15edcc 100644
--- a/spot/twa/taatgba.cc
+++ b/spot/twa/taatgba.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009-2017 Laboratoire de Recherche et Développement de
+// Copyright (C) 2009-2018 Laboratoire de Recherche et Développement de
 // l'Epita (LRDE)
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <map>
 #include <algorithm>
 #include <iterator>
diff --git a/spot/twa/twa.cc b/spot/twa/twa.cc
index cdbb033d1..19fd494a0 100644
--- a/spot/twa/twa.cc
+++ b/spot/twa/twa.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2014-2017 Laboratoire de Recherche et Developpement de
+// Copyright (C) 2011, 2014-2018 Laboratoire de Recherche et Developpement de
 // l'EPITA (LRDE).
 // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twa/twa.hh>
 #include <spot/twa/twagraph.hh>
 #include <spot/twaalgos/couvreurnew.hh>
diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc
index f43b1b48d..c3d2671d7 100644
--- a/spot/twa/twagraph.cc
+++ b/spot/twa/twagraph.cc
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twa/twagraph.hh>
 #include <spot/tl/print.hh>
 #include <spot/misc/bddlt.hh>
diff --git a/spot/twa/twaproduct.cc b/spot/twa/twaproduct.cc
index 29328355c..d1ff07b17 100644
--- a/spot/twa/twaproduct.cc
+++ b/spot/twa/twaproduct.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2011, 2012, 2014, 2015, 2016, 2017 Laboratoire
-// de Recherche et Développement de l'Epita (LRDE).
+// Copyright (C) 2009, 2011-2012, 2014-2018 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de
 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 // Université Pierre et Marie Curie.
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twa/twaproduct.hh>
 #include <string>
 #include <cassert>
diff --git a/spot/twaalgos/Makefile.am b/spot/twaalgos/Makefile.am
index 5d1d7fa3b..500115a51 100644
--- a/spot/twaalgos/Makefile.am
+++ b/spot/twaalgos/Makefile.am
@@ -1,5 +1,5 @@
 ## -*- coding: utf-8 -*-
-## Copyright (C) 2008-2017 Laboratoire de Recherche et Développement
+## Copyright (C) 2008-2018 Laboratoire de Recherche et Développement
 ## de l'Epita (LRDE).
 ## Copyright (C) 2003-2005 Laboratoire d'Informatique de Paris 6
 ## (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@@ -22,7 +22,8 @@
 
 SUBDIRS = gtec
 
-AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS)
+AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) \
+              -I$(top_builddir)/lib -I$(top_srcdir)/lib
 AM_CXXFLAGS = $(WARNING_CXXFLAGS)
 
 twaalgosdir = $(pkgincludedir)/twaalgos
diff --git a/spot/twaalgos/aiger.cc b/spot/twaalgos/aiger.cc
index 26344ce68..8cf2f1c82 100644
--- a/spot/twaalgos/aiger.cc
+++ b/spot/twaalgos/aiger.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/aiger.hh>
 
 #include <cmath>
diff --git a/spot/twaalgos/alternation.cc b/spot/twaalgos/alternation.cc
index eed14cedd..0ebbb1667 100644
--- a/spot/twaalgos/alternation.cc
+++ b/spot/twaalgos/alternation.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2016-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <algorithm>
 #include <sstream>
 #include <spot/twaalgos/alternation.hh>
diff --git a/spot/twaalgos/are_isomorphic.cc b/spot/twaalgos/are_isomorphic.cc
index 773e640d3..77fb95741 100644
--- a/spot/twaalgos/are_isomorphic.cc
+++ b/spot/twaalgos/are_isomorphic.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twa/twagraph.hh>
 #include <spot/twaalgos/are_isomorphic.hh>
 #include <spot/twaalgos/canonicalize.hh>
diff --git a/spot/twaalgos/bfssteps.cc b/spot/twaalgos/bfssteps.cc
index 082c815fd..131596117 100644
--- a/spot/twaalgos/bfssteps.cc
+++ b/spot/twaalgos/bfssteps.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE)
+// Copyright (C) 2014, 2015, 2018 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE)
 // Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <deque>
 #include <utility>
 #include <spot/twa/twa.hh>
diff --git a/spot/twaalgos/canonicalize.cc b/spot/twaalgos/canonicalize.cc
index 9b3cbaa39..1feca0113 100644
--- a/spot/twaalgos/canonicalize.cc
+++ b/spot/twaalgos/canonicalize.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/canonicalize.hh>
 #include <spot/twa/twagraph.hh>
 #include <set>
diff --git a/spot/twaalgos/cleanacc.cc b/spot/twaalgos/cleanacc.cc
index 74d4c5692..a672f1cb5 100644
--- a/spot/twaalgos/cleanacc.cc
+++ b/spot/twaalgos/cleanacc.cc
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/cleanacc.hh>
 
 namespace spot
diff --git a/spot/twaalgos/cobuchi.cc b/spot/twaalgos/cobuchi.cc
index 73d0f5661..32129a196 100644
--- a/spot/twaalgos/cobuchi.cc
+++ b/spot/twaalgos/cobuchi.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement
+// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/cobuchi.hh>
 
 #include <spot/misc/bddlt.hh>
@@ -35,11 +36,11 @@
 #include <stack>
 #include <unordered_map>
 
-#define DEBUG 0
-#if DEBUG
-#define debug std::cerr
+#define TRACE 0
+#if TRACE
+#define trace std::cerr
 #else
-#define debug while (0) std::cout
+#define trace while (0) std::cout
 #endif
 
 namespace spot
@@ -461,7 +462,7 @@ namespace spot
                     }
                 }
             }
-          debug << "All_states:\n" << *bv_aut_trans_ << '\n';
+          trace << "All_states:\n" << *bv_aut_trans_ << '\n';
 
           twa_graph_ptr res = make_twa_graph(aut_->get_dict());
           res->copy_ap_of(aut_);
@@ -548,14 +549,14 @@ namespace spot
                       bv_trans_mark->at(l) |= bv_aut_trans_->at(s * nc + l);
               toclean_.push_back(bv_trans_mark);
 
-              debug << "src:" << top.second;
+              trace << "src:" << top.second;
               if (named_states)
-                debug << ' ' << (*state_name)[top.second];
-              debug << '\n';
+                trace << ' ' << (*state_name)[top.second];
+              trace << '\n';
 
               for (unsigned l = 0; l < nc; ++l)
                 {
-                  debug << "l: "
+                  trace << "l: "
                         << bdd_format_formula(aut_->get_dict(), num2bdd_[l])
                         << '\n';
 
@@ -582,12 +583,12 @@ namespace spot
                                 (top.first.first + 1) % (nb_copy_ + 1)
                               : top.first.first;
 
-                  debug << "dest\n" << *bv_res << "i: " << i << '\n';
+                  trace << "dest\n" << *bv_res << "i: " << i << '\n';
                   res->new_edge(top.second,
                                 new_state(std::make_pair(i, bv_res)),
                                 num2bdd_[l]);
                 }
-              debug << '\n';
+              trace << '\n';
             }
 
           // Set rejecting states.
@@ -617,7 +618,7 @@ namespace spot
   twa_graph_ptr
   nsa_to_dca(const_twa_graph_ptr aut, bool named_states)
   {
-    debug << "NSA_to_dca\n";
+    trace << "NSA_to_dca\n";
     std::vector<acc_cond::rs_pair> pairs;
     if (!aut->acc().is_streett_like(pairs) && !aut->acc().is_parity())
       throw std::runtime_error("nsa_to_dca() only works with Streett-like or "
@@ -632,10 +633,10 @@ namespace spot
     vect_nca_info nca_info;
     nsa_to_nca(aut, named_states, &nca_info);
 
-#if DEBUG
-    debug << "PRINTING INFO\n";
+#if TRACE
+    trace << "PRINTING INFO\n";
     for (unsigned i = 0; i < nca_info.size(); ++i)
-      debug << '<' << nca_info[i]->clause_num << ',' << nca_info[i]->state_num
+      trace << '<' << nca_info[i]->clause_num << ',' << nca_info[i]->state_num
             << ',' << *nca_info[i]->all_dst << ">\n";
 #endif
 
@@ -647,7 +648,7 @@ namespace spot
   twa_graph_ptr
   dnf_to_dca(const_twa_graph_ptr aut, bool named_states)
   {
-    debug << "DNF_to_dca\n";
+    trace << "DNF_to_dca\n";
     const acc_cond::acc_code& code = aut->get_acceptance();
     if (!code.is_dnf())
       throw std::runtime_error("dnf_to_dca() only works with DNF (Rabin-like "
@@ -662,10 +663,10 @@ namespace spot
     vect_nca_info nca_info;
     dnf_to_nca(aut, false, &nca_info);
 
-#if DEBUG
-    debug << "PRINTING INFO\n";
+#if TRACE
+    trace << "PRINTING INFO\n";
     for (unsigned i = 0; i < nca_info.size(); ++i)
-      debug << '<' << nca_info[i]->clause_num << ',' << nca_info[i]->state_num
+      trace << '<' << nca_info[i]->clause_num << ',' << nca_info[i]->state_num
             << ',' << *nca_info[i]->all_dst << ">\n";
 #endif
 
diff --git a/spot/twaalgos/complement.cc b/spot/twaalgos/complement.cc
index 2ac33d058..446052b44 100644
--- a/spot/twaalgos/complement.cc
+++ b/spot/twaalgos/complement.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013-2015, 2017 Laboratoire de Recherche et
+// Copyright (C) 2013-2015, 2017-2018 Laboratoire de Recherche et
 // Développement de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/complement.hh>
 #include <spot/twaalgos/dualize.hh>
 #include <spot/twaalgos/isdet.hh>
diff --git a/spot/twaalgos/complete.cc b/spot/twaalgos/complete.cc
index 71426c795..78ac48b7b 100644
--- a/spot/twaalgos/complete.cc
+++ b/spot/twaalgos/complete.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013-2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement
 // de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/complete.hh>
 
 namespace spot
diff --git a/spot/twaalgos/compsusp.cc b/spot/twaalgos/compsusp.cc
index ae9b6a68f..36dbeb008 100644
--- a/spot/twaalgos/compsusp.cc
+++ b/spot/twaalgos/compsusp.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
+// Copyright (C) 2012-2015, 2018 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/compsusp.hh>
 #include <spot/twaalgos/sccfilter.hh>
 #include <spot/twaalgos/sccinfo.hh>
diff --git a/spot/twaalgos/couvreurnew.cc b/spot/twaalgos/couvreurnew.cc
index 3f9fcc780..103431ec9 100644
--- a/spot/twaalgos/couvreurnew.cc
+++ b/spot/twaalgos/couvreurnew.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2016-2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2016-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/couvreurnew.hh>
 
 #include <spot/twa/twa.hh>
diff --git a/spot/twaalgos/cycles.cc b/spot/twaalgos/cycles.cc
index 90deed5b3..51b528584 100644
--- a/spot/twaalgos/cycles.cc
+++ b/spot/twaalgos/cycles.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2014-2017 Laboratoire de Recherche et
+// Copyright (C) 2012, 2014-2018 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <iostream>
 #include <spot/twaalgos/cycles.hh>
 
diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc
index 77ff75a2d..d1dbdc633 100644
--- a/spot/twaalgos/degen.cc
+++ b/spot/twaalgos/degen.cc
@@ -17,7 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
-
+#include "config.h"
 #include <spot/twaalgos/degen.hh>
 #include <spot/twa/twagraph.hh>
 #include <spot/misc/hash.hh>
diff --git a/spot/twaalgos/determinize.cc b/spot/twaalgos/determinize.cc
index bfb2bc9e3..323a5ad0d 100644
--- a/spot/twaalgos/determinize.cc
+++ b/spot/twaalgos/determinize.cc
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <algorithm>
 #include <deque>
 #include <stack>
diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc
index cb8efa123..39fbc87d5 100644
--- a/spot/twaalgos/dot.cc
+++ b/spot/twaalgos/dot.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012, 2014-2017 Laboratoire de Recherche
+// Copyright (C) 2011, 2012, 2014-2018 Laboratoire de Recherche
 // et Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <ostream>
 #include <sstream>
 #include <stdexcept>
diff --git a/spot/twaalgos/dtbasat.cc b/spot/twaalgos/dtbasat.cc
index f945bd2ef..e765fae3d 100644
--- a/spot/twaalgos/dtbasat.cc
+++ b/spot/twaalgos/dtbasat.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche
+// Copyright (C) 2013-2018 Laboratoire de Recherche
 // et Développement de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <fstream>
 #include <sstream>
 #include <map>
@@ -33,14 +34,14 @@
 // file used to communicate with the sat solver will be left in
 // the current directory.
 //
-// Additionally, if the following DEBUG macro is set to 1, the CNF
+// Additionally, if the following TRACE macro is set to 1, the CNF
 // file will be output with a comment before each clause, and an
 // additional output file (dtba-sat.dbg) will be created with a list
 // of all positive variables in the result and their meaning.
 
-#define DEBUG 0
+#define TRACE 0
 
-#if DEBUG
+#if TRACE
 #define dout out << "c "
 #define cnf_comment(...) solver.comment(__VA_ARGS__)
 #define trace std::cerr
@@ -105,7 +106,7 @@ namespace spot
       int
       transid(unsigned src, bdd& cond, unsigned dst)
       {
-#if DEBUG
+#if TRACE
         try
         {
           return helper.get_t(src, alpha_map.at(cond), dst);
@@ -130,7 +131,7 @@ namespace spot
       int
       transacc(unsigned src, bdd& cond, unsigned dst)
       {
-#if DEBUG
+#if TRACE
         try
         {
           return helper.get_ta(src, alpha_map.at(cond), dst);
@@ -150,7 +151,7 @@ namespace spot
       pathid_ref(unsigned src_cand, unsigned src_ref, unsigned dst_cand,
           unsigned dst_ref)
       {
-#if DEBUG
+#if TRACE
         try
         {
           return helper.get_prc(
@@ -169,7 +170,7 @@ namespace spot
 #endif
       }
 
-#if DEBUG
+#if TRACE
       int
       pathid_ref(unsigned path, unsigned src_cand, unsigned dst_cand)
       {
@@ -187,7 +188,7 @@ namespace spot
       pathid_cand(unsigned src_cand, unsigned src_ref, unsigned dst_cand,
           unsigned dst_ref)
       {
-#if DEBUG
+#if TRACE
         try
         {
           return helper.get_prc(
@@ -330,7 +331,7 @@ namespace spot
       // Empty automaton is impossible.
       assert(d.cand_size > 0);
 
-#if DEBUG
+#if TRACE
       debug_dict = ref->get_dict();
       solver.comment("d.ref_size", d.ref_size, '\n');
       solver.comment("d.cand_size", d.cand_size, '\n');
@@ -353,7 +354,7 @@ namespace spot
       for (unsigned q1 = 0; q1 < d.cand_size; ++q1)
         for (unsigned l = 0; l < alpha_size; ++l)
           {
-#if DEBUG
+#if TRACE
             solver.comment("");
             for (unsigned q2 = 0; q2 < d.cand_size; q2++)
               {
@@ -457,7 +458,7 @@ namespace spot
                                   {
                                     bdd s = bdd_satoneset(all, ap, bddfalse);
                                     all -= s;
-#if DEBUG
+#if TRACE
                                     std::string f_t = d.fmt_t(q2, s, q1);
                                     cnf_comment(f_p, "R ∧", f_t, "δ → ¬", f_t,
                                                 "F\n");
@@ -544,7 +545,7 @@ namespace spot
                                   {
                                     bdd s = bdd_satoneset(all, ap, bddfalse);
                                     all -= s;
-#if DEBUG
+#if TRACE
                                     std::string f_t = d.fmt_t(q2, s, q1);
                                     cnf_comment(f_p, "C ∧", f_t, "δ →", f_t,
                                                 "F\n");
@@ -566,7 +567,7 @@ namespace spot
                                   {
                                     bdd s = bdd_satoneset(all, ap, bddfalse);
                                     all -= s;
-#if DEBUG
+#if TRACE
                                     std::string f_t = d.fmt_t(q2, s, q3);
                                     cnf_comment(f_p, "C ∧", f_t, "δ ∧ ¬", f_t,
                                                 "F →", d.fmt_p(q1, q1p, q3, dp),
@@ -602,7 +603,7 @@ namespace spot
       a->prop_universal(true);
       a->new_states(satdict.cand_size);
 
-#if DEBUG
+#if TRACE
       std::fstream out("dtba-sat.dbg",
                        std::ios_base::trunc | std::ios_base::out);
       out.exceptions(std::ifstream::failbit | std::ifstream::badbit);
@@ -638,7 +639,7 @@ namespace spot
               }
             }
           }
-#if DEBUG
+#if TRACE
       dout << "--- transition variables ---\n";
       for (unsigned i = 0; i < cand_size; ++i)
         for (unsigned j = 0; j < alpha_size; ++j)
diff --git a/spot/twaalgos/dtwasat.cc b/spot/twaalgos/dtwasat.cc
index a66197ecc..b1fd22b4b 100644
--- a/spot/twaalgos/dtwasat.cc
+++ b/spot/twaalgos/dtwasat.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche
+// Copyright (C) 2013-2018 Laboratoire de Recherche
 // et Développement de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <fstream>
 #include <sstream>
 #include <map>
@@ -41,14 +42,14 @@
 // file used to communicate with the sat solver will be left in
 // the current directory.
 //
-// Additionally, if the following DEBUG macro is set to 1, the CNF
+// Additionally, if the following TRACE macro is set to 1, the CNF
 // file will be output with a comment before each clause, and an
 // 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
+#define TRACE 0
 
-#if DEBUG
+#if TRACE
 #define dout out << "c "
 #define cnf_comment(...)  solver.comment(__VA_ARGS__)
 #define trace std::cerr
@@ -247,7 +248,7 @@ namespace spot
       int
       transid(unsigned src, bdd& cond, unsigned dst)
       {
-#if DEBUG
+#if TRACE
         try
         {
           return helper.get_t(src, alpha_map.at(cond), dst);
@@ -272,7 +273,7 @@ namespace spot
       int
       transacc(unsigned src, bdd& cond, unsigned dst, unsigned nacc)
       {
-#if DEBUG
+#if TRACE
         try
         {
           return helper.get_ta(src, alpha_map.at(cond), dst, nacc);
@@ -293,7 +294,7 @@ namespace spot
           unsigned dst_ref, acc_cond::mark_t acc_cand = 0U,
           acc_cond::mark_t acc_ref = 0U)
       {
-#if DEBUG
+#if TRACE
         try
         {
           return helper.get_p(
@@ -315,7 +316,7 @@ namespace spot
 #endif
       }
 
-#if DEBUG
+#if TRACE
       int
       pathid(unsigned path, unsigned src_cand, unsigned dst_cand)
       {
@@ -539,7 +540,7 @@ namespace spot
                           bool state_based,
                           bool colored)
     {
-#if DEBUG
+#if TRACE
       debug_dict = ref->get_dict();
 #endif
       // Compute the AP used.
@@ -572,7 +573,7 @@ namespace spot
       // Empty automaton is impossible.
       assert(d.cand_size > 0);
 
-#if DEBUG
+#if TRACE
       debug_ref_acc = &ref->acc();
       debug_cand_acc = &d.cacc;
       solver.comment("d.ref_size:", d.ref_size, '\n');
@@ -597,7 +598,7 @@ namespace spot
       for (unsigned q1 = 0; q1 < d.cand_size; ++q1)
         for (unsigned l = 0; l < alpha_size; ++l)
           {
-#if DEBUG
+#if TRACE
             solver.comment("");
             for (unsigned q2 = 0; q2 < d.cand_size; ++q2)
               {
@@ -768,7 +769,7 @@ namespace spot
 
                                           for (auto& v: missing)
                                             {
-#if DEBUG
+#if TRACE
                                               solver.comment((rejloop ?
                                                        "(11) " : "(12) "), f_p,
                                                   " ∧ ", d.fmt_t(q2, l, q3),
@@ -787,7 +788,7 @@ namespace spot
                                                   orsep = " ∨ ";
                                                 }
                                               solver.comment_rec(")\n");
-#endif // DEBUG
+#endif // TRACE
                                               solver.add({-pid, -ti});
                                               for (int s: v)
                                                 if (s < 0)
@@ -825,7 +826,7 @@ namespace spot
                                                 q1, q1p, q3, dp, f2, f2p);
                                             if (pid == p2id)
                                               continue;
-#if DEBUG
+#if TRACE
                                             solver.comment("(13) ", f_p, " ∧ ",
                                                  d.fmt_t(q1, l, q3), "δ ");
 
@@ -883,7 +884,7 @@ namespace spot
       a->set_acceptance(satdict.cand_nacc, satdict.cand_acc);
       a->new_states(satdict.cand_size);
 
-#if DEBUG
+#if TRACE
       std::fstream out("dtwa-sat.dbg",
                        std::ios_base::trunc | std::ios_base::out);
       out.exceptions(std::ifstream::failbit | std::ifstream::badbit);
@@ -922,7 +923,7 @@ namespace spot
             }
           }
 
-#if DEBUG
+#if TRACE
       dout << "--- transition variables ---\n";
       for (unsigned i = 0; i < satdict.cand_size; ++i)
         for (unsigned j = 0; j < alpha_size; ++j)
diff --git a/spot/twaalgos/dualize.cc b/spot/twaalgos/dualize.cc
index 73d762728..1f8a436cf 100644
--- a/spot/twaalgos/dualize.cc
+++ b/spot/twaalgos/dualize.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/misc/minato.hh>
 #include <spot/twa/twagraph.hh>
 #include <spot/twaalgos/alternation.hh>
@@ -180,8 +181,8 @@ namespace spot
       }
 
       // Handles the dualization of a universal initial transition.
-      // In theory the transition would be split into several existential 
-      // initial transitions, but since spot does not allow multiple initial 
+      // In theory the transition would be split into several existential
+      // initial transitions, but since spot does not allow multiple initial
       // states, we rather use a trick: We add a new initial state, and then
       // copy all exiting transitions from each of the state of the universal
       // initial transition.
@@ -251,9 +252,9 @@ namespace spot
       }
 
       // Given the bdd representation b of a transition, adds destination states
-      // to s, and returns the marks on the transition. s being empty means the 
+      // to s, and returns the marks on the transition. s being empty means the
       // transition goes toward a "forever true" state. s with size one
-      // represents an existential transition, while size over one represents 
+      // represents an existential transition, while size over one represents
       // a universal transition.
       acc_cond::mark_t bdd_to_state(bdd b, std::vector<unsigned>& s)
       {
diff --git a/spot/twaalgos/emptiness.cc b/spot/twaalgos/emptiness.cc
index 606c6d3ab..f9b91f1a7 100644
--- a/spot/twaalgos/emptiness.cc
+++ b/spot/twaalgos/emptiness.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2011-2017 Laboratoire de Recherche et
+// Copyright (C) 2009, 2011-2018 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <sstream>
 #include <memory>
 #include <spot/twaalgos/emptiness.hh>
diff --git a/spot/twaalgos/gtec/Makefile.am b/spot/twaalgos/gtec/Makefile.am
index 14f6dc92f..98198e6ef 100644
--- a/spot/twaalgos/gtec/Makefile.am
+++ b/spot/twaalgos/gtec/Makefile.am
@@ -1,6 +1,6 @@
 ## -*- coding: utf-8 -*-
-## Copyright (C) 2011, 2013, 2014, 2016 Laboratoire de Recherche et
-## Developpement de l'Epita (LRDE).
+## Copyright (C) 2011, 2013, 2014, 2016, 2018 Laboratoire de Recherche
+## et Developpement de l'Epita (LRDE).
 ## Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
 ## département Systèmes Répartis Coopératifs (SRC), Université Pierre
 ## et Marie Curie.
@@ -20,7 +20,8 @@
 ## You should have received a copy of the GNU General Public License
 ## along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
-AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS)
+AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) \
+              -I$(top_builddir)/lib -I$(top_srcdir)/lib
 AM_CXXFLAGS = $(WARNING_CXXFLAGS)
 
 gtecdir = $(pkgincludedir)/twaalgos/gtec
diff --git a/spot/twaalgos/gtec/ce.cc b/spot/twaalgos/gtec/ce.cc
index 66aae9b9d..c44bb3ebe 100644
--- a/spot/twaalgos/gtec/ce.cc
+++ b/spot/twaalgos/gtec/ce.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2013, 2014, 2015, 2016 Laboratoire de
+// Copyright (C) 2010-2011, 2013-2016, 2018 Laboratoire de
 // Recherche et Développement de l'Epita (LRDE).
 // Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/gtec/ce.hh>
 #include <spot/twaalgos/bfssteps.hh>
 #include <spot/misc/hash.hh>
diff --git a/spot/twaalgos/gtec/gtec.cc b/spot/twaalgos/gtec/gtec.cc
index 8aece6ad5..243ad8c91 100644
--- a/spot/twaalgos/gtec/gtec.cc
+++ b/spot/twaalgos/gtec/gtec.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2011, 2014, 2015, 2016 Laboratoire de Recherche
+// Copyright (C) 2008, 2011, 2014-2016, 2018 Laboratoire de Recherche
 // et Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -22,6 +22,7 @@
 
 // #define TRACE
 
+#include "config.h"
 #include <iostream>
 #ifdef TRACE
 #define trace std::cerr
diff --git a/spot/twaalgos/gtec/sccstack.cc b/spot/twaalgos/gtec/sccstack.cc
index d953fff45..34ec7493b 100644
--- a/spot/twaalgos/gtec/sccstack.cc
+++ b/spot/twaalgos/gtec/sccstack.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014 Laboratoire de Recherche et Developpement de
+// Copyright (C) 2014, 2018 Laboratoire de Recherche et Developpement de
 // l'Epita (LRDE).
 // Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/gtec/sccstack.hh>
 
 namespace spot
diff --git a/spot/twaalgos/gtec/status.cc b/spot/twaalgos/gtec/status.cc
index 0c5862408..d9b6d8fc8 100644
--- a/spot/twaalgos/gtec/status.cc
+++ b/spot/twaalgos/gtec/status.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014, 2016 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2014, 2016, 2018 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 // Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <ostream>
 #include <spot/twaalgos/gtec/status.hh>
 
diff --git a/spot/twaalgos/gv04.cc b/spot/twaalgos/gv04.cc
index 45e496954..a6e7e6b64 100644
--- a/spot/twaalgos/gv04.cc
+++ b/spot/twaalgos/gv04.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2010, 2011, 2013-2017 Laboratoire de
+// Copyright (C) 2008, 2010, 2011, 2013-2018 Laboratoire de
 // recherche et développement de l'Epita (LRDE).
 // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6
 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@@ -22,6 +22,7 @@
 
 //#define TRACE
 
+#include "config.h"
 #include <iostream>
 #ifdef TRACE
 #define trace std::cerr
diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc
index 51d45e6a7..e70bf4d18 100644
--- a/spot/twaalgos/hoa.cc
+++ b/spot/twaalgos/hoa.cc
@@ -1,9 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012, 2014, 2015, 2016, 2017 Laboratoire de Recherche et
+// Copyright (C) 2014-2018 Laboratoire de Recherche et
 // Developpement de l'Epita (LRDE).
-// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
-// et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -20,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <ostream>
 #include <sstream>
 #include <cstring>
diff --git a/spot/twaalgos/iscolored.cc b/spot/twaalgos/iscolored.cc
index 871ab6bc4..d38a36ee8 100644
--- a/spot/twaalgos/iscolored.cc
+++ b/spot/twaalgos/iscolored.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2017 Laboratoire de Recherche et Développement de l'Epita
-// (LRDE).
+// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement
+// de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/iscolored.hh>
 
 namespace spot
diff --git a/spot/twaalgos/isdet.cc b/spot/twaalgos/isdet.cc
index 50cdcde2b..51a43661c 100644
--- a/spot/twaalgos/isdet.cc
+++ b/spot/twaalgos/isdet.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/isdet.hh>
 #include <spot/twaalgos/sccinfo.hh>
 
diff --git a/spot/twaalgos/isunamb.cc b/spot/twaalgos/isunamb.cc
index e0f8af6a0..3adb787bd 100644
--- a/spot/twaalgos/isunamb.cc
+++ b/spot/twaalgos/isunamb.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013, 2015-2017 Laboratoire de Recherche et
+// Copyright (C) 2013, 2015-2018 Laboratoire de Recherche et
 // Developpement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/isunamb.hh>
 #include <spot/twaalgos/product.hh>
 #include <spot/twaalgos/sccinfo.hh>
diff --git a/spot/twaalgos/isweakscc.cc b/spot/twaalgos/isweakscc.cc
index 5bd292e5e..04a9f07db 100644
--- a/spot/twaalgos/isweakscc.cc
+++ b/spot/twaalgos/isweakscc.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/tl/formula.hh>
 #include <spot/twaalgos/isweakscc.hh>
 #include <spot/twaalgos/mask.hh>
diff --git a/spot/twaalgos/langmap.cc b/spot/twaalgos/langmap.cc
index a49386717..3ba6b3b23 100644
--- a/spot/twaalgos/langmap.cc
+++ b/spot/twaalgos/langmap.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2016-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <numeric>
 #include <spot/twa/twa.hh>
 #include <spot/twaalgos/dualize.hh>
diff --git a/spot/twaalgos/lbtt.cc b/spot/twaalgos/lbtt.cc
index c96c599c7..c56f4a0f9 100644
--- a/spot/twaalgos/lbtt.cc
+++ b/spot/twaalgos/lbtt.cc
@@ -1,9 +1,9 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de
-// Recherche et Développement de l'Epita (LRDE).
-// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris
-// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
-// Université Pierre et Marie Curie.
+// Copyright (C) 2011-2016, 2018 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
+// Copyright (C) 2003-2005 Laboratoire d'Informatique de Paris 6
+// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
+// Pierre et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/lbtt.hh>
 #include <map>
 #include <string>
diff --git a/spot/twaalgos/ltl2taa.cc b/spot/twaalgos/ltl2taa.cc
index 2a06fcd02..8b02d7c9e 100644
--- a/spot/twaalgos/ltl2taa.cc
+++ b/spot/twaalgos/ltl2taa.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2010, 2012, 2013, 2014, 2015, 2016 Laboratoire
-// de Recherche et Développement de l'Epita (LRDE).
+// Copyright (C) 2009-2010, 2012-2016, 2018 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <utility>
 #include <algorithm>
 #include <spot/tl/unabbrev.hh>
diff --git a/spot/twaalgos/ltl2tgba_fm.cc b/spot/twaalgos/ltl2tgba_fm.cc
index 62d039748..648c03b08 100644
--- a/spot/twaalgos/ltl2tgba_fm.cc
+++ b/spot/twaalgos/ltl2tgba_fm.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008-2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2008-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6
 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/misc/hash.hh>
 #include <spot/misc/bddlt.hh>
 #include <spot/misc/minato.hh>
diff --git a/spot/twaalgos/magic.cc b/spot/twaalgos/magic.cc
index 24820aac4..ac3a5bd37 100644
--- a/spot/twaalgos/magic.cc
+++ b/spot/twaalgos/magic.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2013-2017  Laboratoire de recherche et
+// Copyright (C) 2011, 2013-2018  Laboratoire de recherche et
 // développement de l'Epita (LRDE).
 // Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -22,6 +22,7 @@
 
 //#define TRACE
 
+#include "config.h"
 #include <iostream>
 #ifdef TRACE
 #define trace std::cerr
diff --git a/spot/twaalgos/mask.cc b/spot/twaalgos/mask.cc
index 70fbb22e5..5a6e6a6aa 100644
--- a/spot/twaalgos/mask.cc
+++ b/spot/twaalgos/mask.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/mask.hh>
 
 namespace spot
diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc
index fcab083f7..db5ad9c63 100644
--- a/spot/twaalgos/minimize.cc
+++ b/spot/twaalgos/minimize.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010-2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2010-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -19,13 +19,13 @@
 
 
 //#define TRACE
-
 #ifdef TRACE
 #  define trace std::cerr
 #else
 #  define trace while (0) std::cerr
 #endif
 
+#include "config.h"
 #include <queue>
 #include <deque>
 #include <set>
diff --git a/spot/twaalgos/neverclaim.cc b/spot/twaalgos/neverclaim.cc
index 296f02344..c24fc8948 100644
--- a/spot/twaalgos/neverclaim.cc
+++ b/spot/twaalgos/neverclaim.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2011, 2012, 2014, 2015, 2016 Laboratoire de
-// Recherche et Développement de l'Epita (LRDE).
+// Copyright (C) 2009, 2011, 2012, 2014-2016, 2018 Laboratoire
+// de Recherche et Développement de l'Epita (LRDE).
 // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <ostream>
 #include <sstream>
 #include <spot/twaalgos/neverclaim.hh>
diff --git a/spot/twaalgos/parity.cc b/spot/twaalgos/parity.cc
index 5908baf10..81b67024b 100644
--- a/spot/twaalgos/parity.cc
+++ b/spot/twaalgos/parity.cc
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/parity.hh>
 #include <spot/twa/twagraph.hh>
 #include <spot/twaalgos/product.hh>
diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc
index 4203e5b57..b443481df 100644
--- a/spot/twaalgos/postproc.cc
+++ b/spot/twaalgos/postproc.cc
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/postproc.hh>
 #include <spot/twaalgos/minimize.hh>
 #include <spot/twaalgos/simulation.hh>
diff --git a/spot/twaalgos/powerset.cc b/spot/twaalgos/powerset.cc
index 516945841..8ed37fbc1 100644
--- a/spot/twaalgos/powerset.cc
+++ b/spot/twaalgos/powerset.cc
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <set>
 #include <iterator>
 #include <vector>
diff --git a/spot/twaalgos/product.cc b/spot/twaalgos/product.cc
index ab0aa13df..df32d2c8b 100644
--- a/spot/twaalgos/product.cc
+++ b/spot/twaalgos/product.cc
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/product.hh>
 #include <spot/twa/twagraph.hh>
 #include <spot/twaalgos/complete.hh>
diff --git a/spot/twaalgos/rabin2parity.cc b/spot/twaalgos/rabin2parity.cc
index c41638c63..178981cad 100644
--- a/spot/twaalgos/rabin2parity.cc
+++ b/spot/twaalgos/rabin2parity.cc
@@ -1,5 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement de l'Epita.
+// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement
+// de l'Epita.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -16,10 +17,9 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <deque>
-
 #include <spot/twaalgos/rabin2parity.hh>
-
 #include <spot/twaalgos/sccinfo.hh>
 
 namespace spot
diff --git a/spot/twaalgos/randomgraph.cc b/spot/twaalgos/randomgraph.cc
index 1452ffd7c..59e1c6bdf 100644
--- a/spot/twaalgos/randomgraph.cc
+++ b/spot/twaalgos/randomgraph.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008-2010, 2012-2017 Laboratoire de Recherche et
+// Copyright (C) 2008-2010, 2012-2018 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 // Copyright (C) 2004, 2005, 2007 Laboratoire d'Informatique de
 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/randomgraph.hh>
 #include <spot/twa/twagraph.hh>
 #include <spot/misc/random.hh>
diff --git a/spot/twaalgos/randomize.cc b/spot/twaalgos/randomize.cc
index a38435ba9..c3b09a004 100644
--- a/spot/twaalgos/randomize.cc
+++ b/spot/twaalgos/randomize.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <algorithm>
 #include <numeric>
 #include <random>
diff --git a/spot/twaalgos/reachiter.cc b/spot/twaalgos/reachiter.cc
index 33ece2d65..a85c20005 100644
--- a/spot/twaalgos/reachiter.cc
+++ b/spot/twaalgos/reachiter.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2011, 2013, 2014, 2015, 2016 Laboratoire de Recherche
+// Copyright (C) 2009, 2011, 2013-2016, 2018 Laboratoire de Recherche
 // et Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <cassert>
 #include <spot/twaalgos/reachiter.hh>
 
diff --git a/spot/twaalgos/relabel.cc b/spot/twaalgos/relabel.cc
index 72884400d..3d09136bc 100644
--- a/spot/twaalgos/relabel.cc
+++ b/spot/twaalgos/relabel.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/relabel.hh>
 #include <spot/twa/formula2bdd.hh>
 
diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc
index 682bddc40..07b496dfe 100644
--- a/spot/twaalgos/remfin.cc
+++ b/spot/twaalgos/remfin.cc
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/remfin.hh>
 #include <spot/twaalgos/sccinfo.hh>
 #include <iostream>
diff --git a/spot/twaalgos/remprop.cc b/spot/twaalgos/remprop.cc
index 32e32bfdb..bdd5a842c 100644
--- a/spot/twaalgos/remprop.cc
+++ b/spot/twaalgos/remprop.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015-2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/remprop.hh>
 #include <spot/twaalgos/mask.hh>
 #include <spot/misc/casts.hh>
@@ -124,7 +125,7 @@ namespace spot
 
   twa_graph_ptr remove_ap::strip(const_twa_graph_ptr aut) const
   {
-    bdd restrict = bddtrue;
+    bdd restrict_ = bddtrue;
     bdd exist = bddtrue;
     auto d = aut->get_dict();
 
@@ -147,7 +148,7 @@ namespace spot
         int v = d->has_registered_proposition(ap, aut);
         if (v >= 0)
           {
-            restrict &= bdd_ithvar(v);
+            restrict_ &= bdd_ithvar(v);
             res->unregister_ap(v);
           }
       }
@@ -156,7 +157,7 @@ namespace spot
         int v = d->has_registered_proposition(ap, aut);
         if (v >= 0)
           {
-            restrict &= bdd_nithvar(v);
+            restrict_ &= bdd_nithvar(v);
             res->unregister_ap(v);
           }
       }
@@ -165,7 +166,7 @@ namespace spot
                                        acc_cond::mark_t&, unsigned)
                          {
                            cond = bdd_restrict(bdd_exist(cond, exist),
-                                               restrict);
+                                               restrict_);
                          });
     return res;
   }
diff --git a/spot/twaalgos/sbacc.cc b/spot/twaalgos/sbacc.cc
index 3cff71f1a..fe55d5fb8 100644
--- a/spot/twaalgos/sbacc.cc
+++ b/spot/twaalgos/sbacc.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015-2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <vector>
 #include <map>
 #include <utility>
diff --git a/spot/twaalgos/sccfilter.cc b/spot/twaalgos/sccfilter.cc
index 34bbd92ca..d73e67b26 100644
--- a/spot/twaalgos/sccfilter.cc
+++ b/spot/twaalgos/sccfilter.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009-2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2009-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/sccfilter.hh>
 #include <spot/twaalgos/reachiter.hh>
 #include <spot/twaalgos/sccinfo.hh>
diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc
index 567b9f1bd..9f77bb313 100644
--- a/spot/twaalgos/sccinfo.cc
+++ b/spot/twaalgos/sccinfo.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/sccinfo.hh>
 #include <stack>
 #include <algorithm>
diff --git a/spot/twaalgos/se05.cc b/spot/twaalgos/se05.cc
index ec24263b7..89032f289 100644
--- a/spot/twaalgos/se05.cc
+++ b/spot/twaalgos/se05.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2013-2017  Laboratoire de Recherche et
+// Copyright (C) 2011, 2013-2018  Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 // Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -22,6 +22,7 @@
 
 //#define TRACE
 
+#include "config.h"
 #include <iostream>
 #ifdef TRACE
 #define trace std::cerr
diff --git a/spot/twaalgos/sepsets.cc b/spot/twaalgos/sepsets.cc
index 2e9f95f42..2b246a06d 100644
--- a/spot/twaalgos/sepsets.cc
+++ b/spot/twaalgos/sepsets.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et
+// Copyright (C) 2015-2018 Laboratoire de Recherche et
 // Développement de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/sepsets.hh>
 #include <spot/twaalgos/sccinfo.hh>
 
diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc
index e7b8979ed..724510d84 100644
--- a/spot/twaalgos/simulation.cc
+++ b/spot/twaalgos/simulation.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <queue>
 #include <map>
 #include <utility>
diff --git a/spot/twaalgos/split.cc b/spot/twaalgos/split.cc
index 70d63f405..f2d1bae92 100644
--- a/spot/twaalgos/split.cc
+++ b/spot/twaalgos/split.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement
 // de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/split.hh>
 
 namespace spot
diff --git a/spot/twaalgos/stats.cc b/spot/twaalgos/stats.cc
index cfcdd51c5..2d0a7a849 100644
--- a/spot/twaalgos/stats.cc
+++ b/spot/twaalgos/stats.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2011, 2012, 2013, 2014, 2015, 2016, 2017
-// Laboratoire de Recherche et Développement de l'Epita (LRDE).
+// Copyright (C) 2008, 2011-2018 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <iostream>
 #include <sstream>
 #include <spot/twa/twa.hh>
diff --git a/spot/twaalgos/strength.cc b/spot/twaalgos/strength.cc
index 24578f268..36821c91e 100644
--- a/spot/twaalgos/strength.cc
+++ b/spot/twaalgos/strength.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2013, 2014, 2015, 2016, 2017 Laboratoire
-// de Recherche et Développement de l'Epita (LRDE)
+// Copyright (C) 2010-2011, 2013-2018 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE)
 //
 // This file is part of Spot, a model checking library.
 //
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/strength.hh>
 #include <spot/misc/hash.hh>
 #include <spot/twaalgos/isweakscc.hh>
diff --git a/spot/twaalgos/stripacc.cc b/spot/twaalgos/stripacc.cc
index a4018035a..41634b409 100644
--- a/spot/twaalgos/stripacc.cc
+++ b/spot/twaalgos/stripacc.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2014, 2015, 2017 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2012, 2014-2015, 2017-2018 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/stripacc.hh>
 #include <spot/twaalgos/reachiter.hh>
 
diff --git a/spot/twaalgos/stutter.cc b/spot/twaalgos/stutter.cc
index 8fd9cbd48..b2f2cbedb 100644
--- a/spot/twaalgos/stutter.cc
+++ b/spot/twaalgos/stutter.cc
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/stutter.hh>
 #include <spot/twa/twa.hh>
 #include <spot/misc/hash.hh>
diff --git a/spot/twaalgos/sum.cc b/spot/twaalgos/sum.cc
index f175d7de5..85e579471 100644
--- a/spot/twaalgos/sum.cc
+++ b/spot/twaalgos/sum.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/alternation.hh>
 #include <spot/twaalgos/sum.hh>
 #include <spot/twa/twagraph.hh>
@@ -76,7 +77,7 @@ namespace spot
         }
     }
 
-    // Helper function that perform the sum of the automaton in left and the 
+    // Helper function that perform the sum of the automaton in left and the
     // automaton in right, using is_sum true for sum_or and is_sum false
     // as sum_and
     static
diff --git a/spot/twaalgos/tau03.cc b/spot/twaalgos/tau03.cc
index 8e07a2fac..ec7396949 100644
--- a/spot/twaalgos/tau03.cc
+++ b/spot/twaalgos/tau03.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2013-2017  Laboratoire de Recherche et
+// Copyright (C) 2011, 2013-2018  Laboratoire de Recherche et
 // Developpement de l'Epita (LRDE).
 // Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -25,6 +25,7 @@
 
 //#define TRACE
 
+#include "config.h"
 #include <iostream>
 #ifdef TRACE
 #define trace std::cerr
diff --git a/spot/twaalgos/tau03opt.cc b/spot/twaalgos/tau03opt.cc
index 9b9907605..51f988854 100644
--- a/spot/twaalgos/tau03opt.cc
+++ b/spot/twaalgos/tau03opt.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2013-2017  Laboratoire de Recherche et
+// Copyright (C) 2011, 2013-2018  Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 // Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -34,6 +34,7 @@
 
 //#define TRACE
 
+#include "config.h"
 #include <iostream>
 #ifdef TRACE
 #define trace std::cerr
diff --git a/spot/twaalgos/totgba.cc b/spot/twaalgos/totgba.cc
index bac6fad04..e9440f22e 100644
--- a/spot/twaalgos/totgba.cc
+++ b/spot/twaalgos/totgba.cc
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/totgba.hh>
 #include <spot/twaalgos/remfin.hh>
 #include <spot/twaalgos/cleanacc.hh>
@@ -25,11 +26,11 @@
 #include <deque>
 #include <tuple>
 
-#define DEBUG 0
-#if DEBUG
-#define debug std::cerr
+#define TRACE 0
+#if TRACE
+#define trace std::cerr
 #else
-#define debug while (0) std::cerr
+#define trace while (0) std::cerr
 #endif
 
 namespace spot
@@ -121,11 +122,11 @@ namespace spot
                 SPOT_UNREACHABLE();
               }
           }
-#if DEBUG
-        debug << "\nPrinting all clauses\n";
+#if TRACE
+        trace << "\nPrinting all clauses\n";
         for (unsigned i = 0; i < all_clauses_.size(); ++i)
           {
-            debug << i << " Fin:" << all_clauses_[i].first << " Inf:"
+            trace << i << " Fin:" << all_clauses_[i].first << " Inf:"
                   << all_clauses_[i].second << '\n';
           }
 #endif
@@ -238,16 +239,16 @@ namespace spot
                   res[scc].push_back(clause);
               }
           }
-#if DEBUG
-        debug << "accepting clauses\n";
+#if TRACE
+        trace << "accepting clauses\n";
         for (unsigned i = 0; i < res.size(); ++i)
           {
-            debug << "scc(" << i << ") --> ";
+            trace << "scc(" << i << ") --> ";
             for (auto elt : res[i])
-              debug << elt << ',';
-            debug << '\n'
+              trace << elt << ',';
+            trace << '\n'
           }
-        debug << '\n';
+        trace << '\n';
 #endif
       }
 
@@ -257,7 +258,7 @@ namespace spot
       void
       add_state(unsigned st)
       {
-        debug << "add_state(" << st << ")\n";
+        trace << "add_state(" << st << ")\n";
         if (st_repr_[st].empty())
           {
             unsigned st_scc = si_.scc_of(st);
@@ -270,7 +271,7 @@ namespace spot
 
             else
               st_repr_[st].emplace_back(-1U, res_->new_state());
-            debug << "added\n";
+            trace << "added\n";
           }
       }
 
@@ -317,7 +318,7 @@ namespace spot
           init_st_in_(in->get_init_state_number()),
           init_reachable_(is_init_reachable())
       {
-        debug << "State based ? " << state_based_ << '\n';
+        trace << "State based ? " << state_based_ << '\n';
         std::tie(all_inf_, all_fin_) = code.used_inf_fin_sets();
         split_dnf_clauses(code);
         find_set_to_add();
@@ -346,7 +347,7 @@ namespace spot
                 add_state(st);
                 for (const auto& e : in_->out(st))
                   {
-                    debug << "working_on_edge(" << st << ',' << e.dst << ")\n";
+                    trace << "working_on_edge(" << st << ',' << e.dst << ")\n";
 
                     unsigned dst_scc = si_.scc_of(e.dst);
                     if (!si_.is_useful_scc(dst_scc))
@@ -366,7 +367,7 @@ namespace spot
                       for (const auto& p_src : st_repr_[st])
                         for (const auto& p_dst : st_repr_[e.dst])
                           {
-                            debug << "repr(" << p_src.second << ','
+                            trace << "repr(" << p_src.second << ','
                                   << p_dst.second << ")\n";
 
                             if (same_scc && p_src.first == p_dst.first)
diff --git a/spot/twaalgos/toweak.cc b/spot/twaalgos/toweak.cc
index efebee736..f734ecfc2 100644
--- a/spot/twaalgos/toweak.cc
+++ b/spot/twaalgos/toweak.cc
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/misc/bddlt.hh>
 #include <spot/misc/minato.hh>
 #include <spot/twa/twagraph.hh>
diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc
index c7de29be9..d8fb14f3e 100644
--- a/spot/twaalgos/translate.cc
+++ b/spot/twaalgos/translate.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013-2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/translate.hh>
 #include <spot/twaalgos/ltl2tgba_fm.hh>
 #include <spot/twaalgos/compsusp.hh>
diff --git a/spot/twaalgos/word.cc b/spot/twaalgos/word.cc
index a5bad2812..cd117d898 100644
--- a/spot/twaalgos/word.cc
+++ b/spot/twaalgos/word.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013-2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/twaalgos/word.hh>
 #include <spot/twa/bddprint.hh>
 #include <spot/twa/bdddict.hh>
diff --git a/tests/Makefile.am b/tests/Makefile.am
index 5c4f4b1ba..4e25ec2a1 100644
--- a/tests/Makefile.am
+++ b/tests/Makefile.am
@@ -22,7 +22,8 @@
 ## along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 AUTOMAKE_OPTIONS = subdir-objects
-AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS)
+AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) \
+              -I$(top_builddir)/lib -I$(top_srcdir)/lib
 AM_CXXFLAGS = $(WARNING_CXXFLAGS)
 LDADD = $(top_builddir)/spot/libspot.la $(top_builddir)/buddy/src/libbddx.la
 
diff --git a/tests/core/acc.cc b/tests/core/acc.cc
index 6c534c751..40059d8c2 100644
--- a/tests/core/acc.cc
+++ b/tests/core/acc.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-x
-// Copyright (C) 2014, 2015, 2017 Laboratoire de Recherche et
+// Copyright (C) 2014, 2015, 2017, 2018 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <iostream>
 #include <iterator>
 #include <vector>
diff --git a/tests/core/bitvect.cc b/tests/core/bitvect.cc
index 32a2f6d52..d8b0750d5 100644
--- a/tests/core/bitvect.cc
+++ b/tests/core/bitvect.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et
+// Copyright (C) 2013-2016, 2018 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <iostream>
 #include <spot/misc/bitvect.hh>
 
diff --git a/tests/core/checkpsl.cc b/tests/core/checkpsl.cc
index 09a473f88..b9cb6e746 100644
--- a/tests/core/checkpsl.cc
+++ b/tests/core/checkpsl.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2014-2016, 2018 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <iostream>
 #include <fstream>
 #include <cassert>
diff --git a/tests/core/checkta.cc b/tests/core/checkta.cc
index f8482c09e..5750d5516 100644
--- a/tests/core/checkta.cc
+++ b/tests/core/checkta.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et
+// Copyright (C) 2014-2016, 2018 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <iostream>
 #include <iomanip>
 #include <fstream>
diff --git a/tests/core/consterm.cc b/tests/core/consterm.cc
index 75904b31b..dedb2479a 100644
--- a/tests/core/consterm.cc
+++ b/tests/core/consterm.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2012, 2015, 2016 Laboratoire de Recherche
+// Copyright (C) 2010-2012, 2015-2016, 2018 Laboratoire de Recherche
 // et Dévelopement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <iostream>
 #include <fstream>
 #include <sstream>
diff --git a/tests/core/emptchk.cc b/tests/core/emptchk.cc
index 12c573652..171036d55 100644
--- a/tests/core/emptchk.cc
+++ b/tests/core/emptchk.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et
+// Copyright (C) 2014-2016, 2018 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <iostream>
 #include <fstream>
 #include <cassert>
diff --git a/tests/core/equalsf.cc b/tests/core/equalsf.cc
index 3761d25ab..692ddc167 100644
--- a/tests/core/equalsf.cc
+++ b/tests/core/equalsf.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015, 2016 Laboratoire de
+// Copyright (C) 2008-2012, 2014-2016, 2018 Laboratoire de
 // Recherche et Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de
 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <iostream>
 #include <fstream>
 #include <sstream>
diff --git a/tests/core/graph.cc b/tests/core/graph.cc
index 3de1d51f0..caaf073c0 100644
--- a/tests/core/graph.cc
+++ b/tests/core/graph.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014, 2015, 2016, 2017 Laboratoire de Recherche et
+// Copyright (C) 2014-2018 Laboratoire de Recherche et
 // Développement de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -17,7 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
-
+#include "config.h"
 #include <iostream>
 #include <spot/graph/graph.hh>
 
diff --git a/tests/core/ikwiad.cc b/tests/core/ikwiad.cc
index b60aa72f9..c85d44f80 100644
--- a/tests/core/ikwiad.cc
+++ b/tests/core/ikwiad.cc
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <iostream>
 #include <iomanip>
 #include <cassert>
diff --git a/tests/core/intvcmp2.cc b/tests/core/intvcmp2.cc
index ad4d07dc5..8024673af 100644
--- a/tests/core/intvcmp2.cc
+++ b/tests/core/intvcmp2.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2014, 2015 Laboratoire de Recherche et Developpement
-// de l'Epita (LRDE).
+// Copyright (C) 2011, 2014, 2015, 2018 Laboratoire de Recherche et
+// Developpement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <iostream>
 #include <spot/misc/intvcmp2.hh>
 #include <cstring>
diff --git a/tests/core/intvcomp.cc b/tests/core/intvcomp.cc
index c5b709678..b4d61de76 100644
--- a/tests/core/intvcomp.cc
+++ b/tests/core/intvcomp.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2014, 2015 Laboratoire de Recherche et
+// Copyright (C) 2011, 2014, 2015, 2018 Laboratoire de Recherche et
 // Developpement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <iostream>
 #include <spot/misc/intvcomp.hh>
 #include <cstring>
diff --git a/tests/core/kind.cc b/tests/core/kind.cc
index 37e9499a0..35c69c48e 100644
--- a/tests/core/kind.cc
+++ b/tests/core/kind.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2012, 2015, 2016 Laboratoire de Recherche et
-// Developement de l'Epita (LRDE).
+// Copyright (C) 2010, 2012, 2015, 2016, 2018 Laboratoire de Recherche
+// et Developement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <iostream>
 #include <fstream>
 #include <sstream>
diff --git a/tests/core/kripkecat.cc b/tests/core/kripkecat.cc
index b780c2f8e..d3ea0fd86 100644
--- a/tests/core/kripkecat.cc
+++ b/tests/core/kripkecat.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2014, 2015 Laboratoire de Recherche et
+// Copyright (C) 2011, 2014, 2015, 2018 Laboratoire de Recherche et
 // Developpement de l'Epita (LRDE)
 //
 // This file is part of Spot, a model checking library.
@@ -17,7 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
-
+#include "config.h"
 #include <spot/parseaut/public.hh>
 #include <spot/twaalgos/hoa.hh>
 
diff --git a/tests/core/length.cc b/tests/core/length.cc
index 2df3ed530..7d99186e4 100644
--- a/tests/core/length.cc
+++ b/tests/core/length.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2015, 2016 Laboratoire de Recherche et
+// Copyright (C) 2012, 2015, 2016, 2018 Laboratoire de Recherche et
 // Developement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <iostream>
 #include <cassert>
 #include <cstdlib>
diff --git a/tests/core/ltlrel.cc b/tests/core/ltlrel.cc
index 3beb53d38..82e001464 100644
--- a/tests/core/ltlrel.cc
+++ b/tests/core/ltlrel.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et Developement
-// de l'Epita (LRDE).
+// Copyright (C) 2013-2016, 2018 Laboratoire de Recherche et
+// Developement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <iostream>
 #include <cassert>
 #include <cstdlib>
diff --git a/tests/core/ngraph.cc b/tests/core/ngraph.cc
index 6de093314..0c0db715e 100644
--- a/tests/core/ngraph.cc
+++ b/tests/core/ngraph.cc
@@ -17,7 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
-
+#include "config.h"
 #include <iostream>
 #include <spot/graph/ngraph.hh>
 #include <spot/twa/twa.hh>
diff --git a/tests/core/parity.cc b/tests/core/parity.cc
index 61983f8e4..64b5f18a2 100644
--- a/tests/core/parity.cc
+++ b/tests/core/parity.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2016 Laboratoire de Recherche et Développement
+// Copyright (C) 2016, 2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <cassert>
 #include <ctime>
 #include <vector>
diff --git a/tests/core/randtgba.cc b/tests/core/randtgba.cc
index 3bc655f78..15039c1ba 100644
--- a/tests/core/randtgba.cc
+++ b/tests/core/randtgba.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008-2012, 2014-2017 Laboratoire de Recherche et
+// Copyright (C) 2008-2012, 2014-2018 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris
 // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <cassert>
 #include <cstdlib>
 #include <iostream>
diff --git a/tests/core/readltl.cc b/tests/core/readltl.cc
index 747c68fe6..6e445bd1a 100644
--- a/tests/core/readltl.cc
+++ b/tests/core/readltl.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2009, 2012, 2015, 2016 Laboratoire de Recherche
-// et Développement de l'Epita (LRDE).
+// Copyright (C) 2008, 2009, 2012, 2015, 2016, 2018 Laboratoire de
+// Recherche et Développement de l'Epita (LRDE).
 // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6
 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
 // Pierre et Marie Curie.
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <iostream>
 #include <fstream>
 #include <cassert>
diff --git a/tests/core/reduc.cc b/tests/core/reduc.cc
index 5e6be26be..d6b5a9067 100644
--- a/tests/core/reduc.cc
+++ b/tests/core/reduc.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*_
-// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015, 2016 Laboratoire
+// Copyright (C) 2008-2012, 2014-2016, 2018 Laboratoire
 // de Recherche et Développement de l'Epita (LRDE).
 // Copyright (C) 2004, 2006, 2007 Laboratoire d'Informatique de Paris
 // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <iostream>
 #include <fstream>
 #include <cassert>
diff --git a/tests/core/safra.cc b/tests/core/safra.cc
index 53f91642d..ca4591559 100644
--- a/tests/core/safra.cc
+++ b/tests/core/safra.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2015, 2016, 2018 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <iostream>
 #include <cstring>
 
diff --git a/tests/core/sccif.cc b/tests/core/sccif.cc
index 4947e9da9..96f289936 100644
--- a/tests/core/sccif.cc
+++ b/tests/core/sccif.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -18,6 +18,7 @@
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 
+#include "config.h"
 #include <iostream>
 #include <spot/twa/twagraph.hh>
 #include <spot/twaalgos/sccinfo.hh>
diff --git a/tests/core/syntimpl.cc b/tests/core/syntimpl.cc
index 2c08a248d..d5037c183 100644
--- a/tests/core/syntimpl.cc
+++ b/tests/core/syntimpl.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015, 2016
-// Laboratoire de Recherche et Développement de l'Epita (LRDE).
+// Copyright (C) 2008-2012, 2014-2016, 2018 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
 // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6
 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
 // Pierre et Marie Curie.
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <iostream>
 #include <cassert>
 #include <cstdlib>
diff --git a/tests/core/taatgba.cc b/tests/core/taatgba.cc
index 8ebf4f1f6..beba2d3de 100644
--- a/tests/core/taatgba.cc
+++ b/tests/core/taatgba.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2014, 2015 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2009, 2014, 2015, 2018 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <iostream>
 #include <cassert>
 #include <spot/misc/hash.hh>
diff --git a/tests/core/tostring.cc b/tests/core/tostring.cc
index 411c1271c..895c1a490 100644
--- a/tests/core/tostring.cc
+++ b/tests/core/tostring.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2009, 2012, 2015, 2016 Laboratoire de Recherche
-// et Développement de l'Epita (LRDE).
+// Copyright (C) 2008, 2009, 2012, 2015, 2016, 2018 Laboratoire de
+// Recherche et Développement de l'Epita (LRDE).
 // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -20,6 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <iostream>
 #include <cassert>
 #include <spot/tl/parse.hh>
diff --git a/tests/core/trival.cc b/tests/core/trival.cc
index 74a643d0e..203bf8177 100644
--- a/tests/core/trival.cc
+++ b/tests/core/trival.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2016 Laboratoire de Recherche et Developpement de
-// l'Epita (LRDE).
+// Copyright (C) 2016, 2018 Laboratoire de Recherche et Developpement
+// de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -18,6 +18,7 @@
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 #undef NDEBUG
+#include "config.h"
 #include <spot/misc/trival.hh>
 #include <cassert>
 
diff --git a/tests/core/twagraph.cc b/tests/core/twagraph.cc
index c3cf98b20..4a34535f0 100644
--- a/tests/core/twagraph.cc
+++ b/tests/core/twagraph.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -17,7 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
-
+#include "config.h"
 #include <iostream>
 #include <spot/twa/twagraph.hh>
 #include <spot/twaalgos/dot.hh>
diff --git a/tests/ltsmin/modelcheck.cc b/tests/ltsmin/modelcheck.cc
index 7a5cc9f7e..8c3770c0a 100644
--- a/tests/ltsmin/modelcheck.cc
+++ b/tests/ltsmin/modelcheck.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016, 2017 Laboratoire de
-// Recherche et Developpement de l'Epita (LRDE)
+// Copyright (C) 2011-2018 Laboratoire de Recherche et Developpement
+// de l'Epita (LRDE)
 //
 // This file is part of Spot, a model checking library.
 //
@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include <spot/ltsmin/ltsmin.hh>
 #include <spot/twaalgos/dot.hh>
 #include <spot/tl/defaultenv.hh>
diff --git a/tests/sanity/includes.test b/tests/sanity/includes.test
index bbcf29b89..32732bc63 100755
--- a/tests/sanity/includes.test
+++ b/tests/sanity/includes.test
@@ -1,6 +1,6 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2008, 2011, 2012, 2016 Laboratoire de Recherche et
+# Copyright (C) 2008, 2011, 2012, 2016, 2018 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 # Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6
 # (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@@ -24,6 +24,7 @@
 # Check that each header is self contained and generates no warning.
 
 set -e
+set +x
 
 rm -f failures.inc
 
@@ -39,21 +40,19 @@ for file in `find "$INCDIR" \( -name "${1-*}.hh" \
      # Those are not public headers, so we do not care
      continue
    else
-     echo "Missing, or incorrect include guard." >&2
-     echo "FAIL: $file"
-     echo "  $file" >> failures.inc
+     echo "FAIL: $file (missing #pragma once)"
+     echo "  $file (missing #pragma once)" >> failures.inc
      continue
    fi
 
    echo "#include <spot/$file>" >incltest.cc
-
    if $CXX $CPPFLAGS -DSKIP_DEPRECATED_WARNING $CXXFLAGS \
            -I$top_builddir -I$top_srcdir -I$top_srcdir/buddy/src \
            -c incltest.cc; then
       echo "PASS: $file"
    else
-      echo "FAIL: $file"
-      echo "  $file" >> failures.inc
+      echo "FAIL: $file (not self-contained)"
+      echo "  $file (not self-contained)" >> failures.inc
    fi
 done
 
diff --git a/tests/sanity/style.test b/tests/sanity/style.test
index bcf29fea8..131d049bb 100755
--- a/tests/sanity/style.test
+++ b/tests/sanity/style.test
@@ -1,6 +1,6 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2009-2017 Laboratoire de Recherche et Développement de
+# Copyright (C) 2009-2018 Laboratoire de Recherche et Développement de
 # l'Epita (LRDE).
 # Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6
 # (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@@ -306,11 +306,16 @@ for dir in "$TOP/spot" "$TOP/bin" "$TOP/tests"; do
 	    *)
 	      $GREP '#.*include.*priv/' $tmp &&
 		diag 'Do not include private headers in public headers.'
-        $GREP '^[^#]*[^#_]assert[	 ]*(.*)' $tmp &&
-          diag 'Use SPOT_ASSERT() instead of assert() in public headers.'
+              $GREP '^[^#]*[^#_]assert[	 ]*(.*)' $tmp &&
+                diag 'Use SPOT_ASSERT() instead of assert() in public headers.'
 	      ;;
-
 	  esac
+          case $file in
+              */bin/*);;
+              *.hh)
+                  $GREP '#.*include.*[<"]config.h[">]' $tmp &&
+                      diag 'Do not include config.h in header files.'
+          esac
 	  ;;
 	*.cc)
 	  if $GREP 'namespace$' $tmp >/dev/null; then
@@ -322,7 +327,15 @@ for dir in "$TOP/spot" "$TOP/bin" "$TOP/tests"; do
 	  fi
           e$GREP '	' $tmp &&
 	      diag 'Use spaces instead of tabs.'
-	  ;;
+          case $file in
+              */bin/*) ;;
+              *)
+                  if $GREP -q '#.*include.*"config.h"' $tmp; then
+                      :
+                  else
+                      diag "*.cc files should include "'"config.h"'
+                  fi;;
+          esac;;
       esac
       case $file in
 	*/bin/*|*.cc);;