diff --git a/Makefile.am b/Makefile.am
index c73c7360e..26b3818db 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -1,5 +1,5 @@
 ## -*- coding: utf-8 -*-
-## Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et Développement
+## Copyright (C) 2011, 2012, 2013, 2014 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
@@ -20,9 +20,6 @@
 ## You should have received a copy of the GNU General Public License
 ## along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
-if WITH_INCLUDED_BUDDY
-  MAYBE_BUDDY = buddy
-endif WITH_INCLUDED_BUDDY
 if NEVER
   # For Automake a conditional directory
   # is conditionally built, but unconditionally distributed.
@@ -31,7 +28,7 @@ if NEVER
   NEVER_BENCH = bench
 endif
 
-SUBDIRS = $(MAYBE_BUDDY) $(NEVER_BENCH) lib src wrap ltdl iface doc
+SUBDIRS = buddy lib src wrap ltdl iface doc $(NEVER_BENCH)
 
 UTF8 = utf8/doc/ReleaseNotes utf8/doc/utf8cpp.html utf8/utf8.h	\
   utf8/utf8/checked.h utf8/utf8/core.h utf8/utf8/unchecked.h
diff --git a/NEWS b/NEWS
index 21713e170..10cfd3c5a 100644
--- a/NEWS
+++ b/NEWS
@@ -2,6 +2,10 @@ New in spot 1.99a (not yet released)
 
   * Major changes (including backward incompatible changes):
 
+    - The curstomized version of BuDDy (libbdd) used by Spot has be
+      renamed as (libbddx) to avoid issues with copies of BuDDy
+      already installed on the system.
+
     - ltlgrind is a new tool that mutates LTL or PSL formulas.  If you
       have a tool that is bogus on some formula that is tool large to
       debug, you can use ltlgrind to generate smaller derived formulas
diff --git a/README b/README
index e3abbbac7..53a53e167 100644
--- a/README
+++ b/README
@@ -28,18 +28,21 @@ Installation
 Requirements
 ------------
 
-Spot requires a complete installation of Python (version 2.0 or
-later).  Especially, Python's headers files should be installed.  If
-you don't have Python installed, you should run configure with
-the --disable-python option (see below).
+Spot requires a C++11-compliant compiler.
+
+Spot expects a complete installation of Python (version 2.0 or later).
+Especially, Python's headers files should be installed.  If you don't
+have Python installed, and do NOT want to install it, you should run
+configure with the --disable-python option (see below).
+
+Optional third-party dependencies
+----------------------------------
 
 
-Third-party dependencies
-------------------------
 
-Spot also uses a modified version of BuDDy (a binary decision diagram
-library), that is already included in the buddy/ directory.  So you
-do not need to install it yourself.
+If the SAT-solver glucose is found on your system, it will
+be used by our test suite to test our SAT-based minimization
+algorithm.
 
 Spot used to distribute a modified version of LBTT (an LTL to Büchi
 test bench), mostly fixing errors reported by recent compilers.
@@ -61,15 +64,6 @@ should read the file INSTALL for generic instructions.
 In addition to its usual options, ./configure will accept some
 flags specific to Spot:
 
-  --with-included-buddy
-    After you have installed Spot the first time, a modified version
-    of BuDDy will be installed.  The next time you reconfigure Spot,
-    configure will detect that this version is already installed, and
-    will attempt to use it directly (this is in case you had to modify
-    one of these yourself for another purpose).  This option will
-    *force* the use, build, and installation of the included version
-    of BuDDy, even when a compatible version is already installed.
-
   --disable-python
     Turn off the compilation of Python bindings.  These bindings are
     currently used to run a couple of tests, and to build the CGI
@@ -190,7 +184,7 @@ iface/            Interfaces to other libraries.
 Third party software
 --------------------
 
-buddy/            A patched version of BuDDy 2.3 (a BDD library).
+buddy/            A customized version of BuDDy 2.3 (a BDD library).
 ltdl/             Libtool's portable dlopen() wrapper library.
 lib/              Gnulib's portability modules.
 utf8/             Nemanja Trifunovic's utf-8 routines.
diff --git a/buddy/examples/Makefile.def b/buddy/examples/Makefile.def
index 921754045..078000469 100644
--- a/buddy/examples/Makefile.def
+++ b/buddy/examples/Makefile.def
@@ -1,2 +1,2 @@
 AM_CPPFLAGS = -I$(top_srcdir)/src -I$(srcdir)
-LDADD = $(top_builddir)/src/libbdd.la
+LDADD = $(top_builddir)/src/libbddx.la
diff --git a/buddy/examples/adder/adder.cxx b/buddy/examples/adder/adder.cxx
index 1ce547300..d601437b2 100644
--- a/buddy/examples/adder/adder.cxx
+++ b/buddy/examples/adder/adder.cxx
@@ -8,7 +8,7 @@
 #include <string.h>
 #include <time.h>
 #include <iostream>
-#include "bdd.h"
+#include "bddx.h"
 
 using namespace std;
 
diff --git a/buddy/examples/bddcalc/parser_.h b/buddy/examples/bddcalc/parser_.h
index 568d7c5e6..cc9d56669 100644
--- a/buddy/examples/bddcalc/parser_.h
+++ b/buddy/examples/bddcalc/parser_.h
@@ -9,7 +9,7 @@
 #define _PARSER_H
 
 #include <stdio.h>
-#include "bdd.h"
+#include "bddx.h"
 
 #define MAXIDLEN 32  /* Max. number of allowed characters in an identifier */
 
diff --git a/buddy/examples/bddtest/bddtest.cxx b/buddy/examples/bddtest/bddtest.cxx
index 4056cc0db..3e1444e24 100644
--- a/buddy/examples/bddtest/bddtest.cxx
+++ b/buddy/examples/bddtest/bddtest.cxx
@@ -1,6 +1,6 @@
 #include <iomanip>
 #include <stdlib.h>
-#include <bdd.h>
+#include <bddx.h>
 
 static const int varnum = 5;
 
@@ -47,9 +47,9 @@ void test1_check(bdd x)
 {
   using namespace std ;
   double anum = bdd_satcount(x);
-  
+
   cout << "Checking bdd with " << setw(4) << anum << " assignments: ";
-  
+
   allsatBDD = x;
   allsatSumBDD = bddfalse;
 
@@ -107,7 +107,7 @@ void test1()
     int v = rand() % varnum;
     int s = rand() % 2;
     int o = rand() % 2;
-    
+
     if (o == 0)
     {
       if (s == 0)
@@ -136,10 +136,10 @@ int main()
 {
   bdd_init(1000,1000);
   bdd_setvarnum(varnum);
-  
+
   test1();
-  
+
   bdd_done();
-  
+
   return 0;
 }
diff --git a/buddy/examples/cmilner/cmilner.c b/buddy/examples/cmilner/cmilner.c
index ae5558c66..ba6dafa3f 100644
--- a/buddy/examples/cmilner/cmilner.c
+++ b/buddy/examples/cmilner/cmilner.c
@@ -1,7 +1,7 @@
 #include <stdio.h>
 #include <stdlib.h>
 #include <math.h>
-#include "bdd.h"
+#include "bddx.h"
 
 int N;          /* Number of cyclers */
 int *normvar;   /* Current state variables */
@@ -289,4 +289,3 @@ int main(int argc, char** argv)
 
    return 0;
 }
-
diff --git a/buddy/examples/fdd/fdd.cxx b/buddy/examples/fdd/fdd.cxx
index 7abdb32f3..206c5e7b4 100644
--- a/buddy/examples/fdd/fdd.cxx
+++ b/buddy/examples/fdd/fdd.cxx
@@ -6,7 +6,7 @@
  *    0 -> 1 -> 2 -> 3 -> 4 -> 5 -> -> 7 -> 0
  */
 
-#include "fdd.h"
+#include "fddx.h"
 
 /* Use the transition relation "transRel" to iterate through the statespace
  */
@@ -63,7 +63,7 @@ int main() {
    {
          /* Set the current state to be state 'i' */
       bdd current = fdd_ithvar(0,i);
-      
+
          /* Set the next state to be state 'i+1' */
       bdd next = fdd_ithvar(1, (i+1) % 8);
 
diff --git a/buddy/examples/milner/milner.cxx b/buddy/examples/milner/milner.cxx
index 808604050..e8653f259 100644
--- a/buddy/examples/milner/milner.cxx
+++ b/buddy/examples/milner/milner.cxx
@@ -1,7 +1,7 @@
 #include <stdio.h>
 #include <stdlib.h>
 #include <math.h>
-#include "bdd.h"
+#include "bddx.h"
 #include <iostream>
 using namespace std;
 
@@ -17,11 +17,11 @@ bdd A(bdd* x, bdd* y, int z)
 {
    bdd res = bddtrue;
    int i;
-   
+
    for(i=0 ; i<N ; i++)
       if(i != z)
 	 res &= bdd_apply(x[i],y[i],bddop_biimp);
-   
+
    return res;
 }
 
@@ -35,19 +35,19 @@ bdd transitions(bdd* t, bdd* tp, bdd* h, bdd* hp, bdd* c, bdd* cp)
    bdd P;            // Cycler i's handling of the token
    bdd E;            // Cycler i's handling of it's task
    bdd T = bddfalse; // The monolithic transition relation
-   
+
    for(i=0 ; i<N ; i++)
    {
       P = ((c[i]>cp[i]) & (tp[i]>t[i]) & hp[i] & A(c,cp,i)
 	   & A(t,tp,i) & A(h,hp,i))
 	 | ((h[i]>hp[i]) & cp[(i+1)%N] & A(c,cp,(i+1)%N) & A(h,hp,i)
 	    & A(t,tp,N));
-      
+
       E = t[i] & !tp[i] & A(t,tp,i) & A(h,hp,N) & A(c,cp,N);
-      
+
       T |= P | E;
    }
-   
+
    return T;
 }
 
@@ -58,10 +58,10 @@ bdd initial_state(bdd* t, bdd* h, bdd* c)
 {
    int i;
    bdd I = c[0] & !h[0] & !t[0];
-   
+
    for(i=1; i<N; i++)
       I &= !c[i] & !h[i] & !t[i];
-   
+
    return I;
 }
 
@@ -90,7 +90,7 @@ bdd reachable_states(bdd I, bdd T)
       R |= tmp;
    }
    while(prevR != R);
-   
+
    return R;
 }
 
@@ -105,38 +105,38 @@ int main(int argc, char** argv)
       cerr << "       N  number of cyclers\n";
       exit(1);
    }
-   
+
    N = atoi(argv[1]);
    if (N <= 0)
    {
       cerr << "The number of cyclers must be more than zero\n";
       exit(2);
    }
-   
+
    bdd_init(500000, 50000);
    bdd_setvarnum(N*6);
-   
+
    bdd* c  = new bdd[N];
    bdd* cp = new bdd[N];
    bdd* t  = new bdd[N];
    bdd* tp = new bdd[N];
    bdd* h  = new bdd[N];
    bdd* hp = new bdd[N];
-   
+
    int *nvar = new int[N*3];
    int *pvar = new int[N*3];
-   
+
    for (n=0 ; n<N*3 ; n++)
    {
       nvar[n] = n*2;
       pvar[n] = n*2+1;
    }
-   
+
    normvar = bdd_makeset(nvar, N*3);
    primvar = bdd_makeset(pvar, N*3);
    renamepair = bdd_newpair();
    bdd_setpairs(renamepair, pvar, nvar, N*3);
-   
+
    for (n=0 ; n<N ; n++)
    {
       c[n]  = bdd_ithvar(n*6);
@@ -161,7 +161,7 @@ int main(int argc, char** argv)
    bdd I = initial_state(t,h,c);
    bdd T = transitions(t,tp,h,hp,c,cp);
    bdd R = reachable_states(I,T);
-   
+
    bddStat s;
    bdd_stats(&s);
 
@@ -176,4 +176,3 @@ int main(int argc, char** argv)
    bdd_done();
    return 0;
 }
-
diff --git a/buddy/examples/money/money.cxx b/buddy/examples/money/money.cxx
index 650f22e49..58bdfeef5 100644
--- a/buddy/examples/money/money.cxx
+++ b/buddy/examples/money/money.cxx
@@ -1,4 +1,4 @@
-#include "bvec.h"
+#include "bvecx.h"
 #include <iostream>
 using namespace std;
 
@@ -16,15 +16,15 @@ using namespace std;
 
 int main(void)
 {
-   using namespace std ;	
+   using namespace std ;
    // Allocate 11 domains with room for up to 3*10
    static int dom[11] = {30,30,30,30,30,30,30,30,30,30,30};
-   
+
    bdd_init(10000,10000);
    fdd_extdomain(dom,11);
 
       // Assign binary vectors (expressions) to the digits
-   
+
    bvec s = bvec_varfdd(0);  // The 's' digit
    bvec e = bvec_varfdd(1);  // The 'e' digit
    bvec n = bvec_varfdd(2);  // ...
@@ -50,7 +50,7 @@ int main(void)
 
    // The use of "m1*10" instead of "m1*c10" avoids a bitnum mismatch since
    // "m1*10" results in 5 bits but "m1*c10" results in 10 bits!
-   
+
       // And so on ...
    bdd  t2 = (n + r + m1  ==  e + m2*10) & n<c10 & r<c10 & m2<c2;
    bdd  t3 = (e + o + m2  ==  n + m3*10) & o<c10 & m3<c2;
@@ -71,6 +71,6 @@ int main(void)
 
       // Print result
    cout << fddset << t << endl;
-   
+
    return 0;
 }
diff --git a/buddy/examples/queen/queen.cxx b/buddy/examples/queen/queen.cxx
index 3498116fc..7e980159c 100644
--- a/buddy/examples/queen/queen.cxx
+++ b/buddy/examples/queen/queen.cxx
@@ -23,11 +23,11 @@
      . . . X
      X . . .
      . . X .
-     
+
 **************************************************************************/
 #include <stdlib.h>
 #include <iostream>
-#include "bdd.h"
+#include "bddx.h"
 using namespace std;
 
 int N;                /* Size of the chess board */
@@ -41,7 +41,7 @@ void build(int i, int j)
 {
    bdd a=bddtrue, b=bddtrue, c=bddtrue, d=bddtrue;
    int k,l;
-   
+
       /* No one in the same column */
    for (l=0 ; l<N ; l++)
       if (l != j)
@@ -78,7 +78,7 @@ int main(int ac, char **av)
 {
    using namespace std ;
    int n,i,j;
-   
+
    if (ac != 2)
    {
       fprintf(stderr, "USAGE:  queen N\n");
@@ -97,7 +97,7 @@ int main(int ac, char **av)
    bdd_setvarnum(N*N);
 
    queen = bddtrue;
-   
+
       /* Build variable array */
    X = new bdd*[N];
    for (n=0 ; n<N ; n++)
@@ -115,7 +115,7 @@ int main(int ac, char **av)
 	 e |= X[i][j];
       queen &= e;
    }
-   
+
       /* Build requirements for each variable(field) */
    for (i=0 ; i<N ; i++)
       for (j=0 ; j<N ; j++)
@@ -131,6 +131,6 @@ int main(int ac, char **av)
    cout << bddset << solution << endl;
 
    bdd_done();
-   
+
    return 0;
 }
diff --git a/buddy/examples/solitare/solitare.cxx b/buddy/examples/solitare/solitare.cxx
index 4f6829dc1..52d8fec5b 100644
--- a/buddy/examples/solitare/solitare.cxx
+++ b/buddy/examples/solitare/solitare.cxx
@@ -2,7 +2,7 @@
 #include <unistd.h>
 #include <stdlib.h>
 #include <iostream>
-#include "bdd.h"
+#include "bddx.h"
 using std::cout;
 using std::endl;
 using std::flush;
@@ -23,7 +23,7 @@ bddPair *pair;        // Renaming pair
 
 
    // All the possible moves. Note that the numbering starts from '1'
-int moves[][3] = 
+int moves[][3] =
 { {1,4,9}, {1,2,3},
   {2,5,10},
   {3,2,1}, {3,6,11},
@@ -68,7 +68,7 @@ int moves[][3] =
 void make_board(void)
 {
    bdd_setvarnum(SIZE*2);
-   
+
    for (int n=0 ; n<SIZE ; n++)
    {
       boardC[n] = bdd_ithvar(n*2);
@@ -81,7 +81,7 @@ void make_board(void)
 void make_initial_state(void)
 {
    I = bddtrue;
-   
+
    for (int n=0 ; n<SIZE ; n++)
       if (n == CENTER)
 	 I &= !boardC[n];
@@ -95,7 +95,7 @@ void make_initial_state(void)
 bdd all_other_idle(int src, int tmp, int dst)
 {
    bdd idle = bddtrue;
-   
+
    for (int n=0 ; n<SIZE ; n++)
    {
       if (n != src  &&  n != tmp  &&  n != dst)
@@ -113,7 +113,7 @@ bdd make_move(int src, int tmp, int dst)
               !boardN[src] & !boardN[tmp] & boardN[dst];
 
    move &= all_other_idle(src, tmp, dst);
-   
+
    return move;
 }
 
@@ -122,7 +122,7 @@ void make_transition_relation(void)
 {
    using namespace std ;
    T = bddfalse;
-   
+
    for (int n=0 ; moves[n][0]!=moves[n][1] ; n++)
       T |= make_move(moves[n][0]-1, moves[n][1]-1, moves[n][2]-1);
 
@@ -137,7 +137,7 @@ void make_itedata(void)
    pair = bdd_newpair();
    for (int n=0 ; n<SIZE ; n++)
       bdd_setpair(pair, n*2+1, n*2);
-   
+
    currentvar = bddtrue;
    for (int n=0 ; n<SIZE ; n++)
       currentvar &= boardC[n];
@@ -152,7 +152,7 @@ void iterate(void)
    int cou = 1;
 
    make_itedata();
-   
+
    do
    {
       tmp = reachable;
@@ -177,7 +177,7 @@ void iterate_front(void)
    int cou = 1;
 
    make_itedata();
-   
+
    do
    {
       tmp = reachable;
@@ -201,7 +201,7 @@ void setup(void)
    bdd_init(100000,1000);
    bdd_setcacheratio(64);
    bdd_setmaxincrease(500000);
-   
+
    dummyStateNum = pow(2.0, SIZE);
 
    make_board();
@@ -217,4 +217,3 @@ int main(void)
 
    system("ps aux | grep \"./solitare\" | grep -v \"grep\"");
 }
-
diff --git a/buddy/src/Makefile.am b/buddy/src/Makefile.am
index 40538b9fa..de770944d 100644
--- a/buddy/src/Makefile.am
+++ b/buddy/src/Makefile.am
@@ -1,14 +1,13 @@
-
-include_HEADERS = bdd.h fdd.h bvec.h
+include_HEADERS = bddx.h fddx.h bvecx.h
 
 BUDDY_FLAGS = -I$(top_builddir) -DVERSION=23 -DBUDDY_DLL_EXPORTS -DBUDDY_DLL
 
-lib_LTLIBRARIES = libbdd.la
+lib_LTLIBRARIES = libbddx.la
 # See the `Updating version info' node of the Libtool manual before
 # changing this.
-libbdd_la_LDFLAGS = -no-undefined -version-info 0:0:0
-libbdd_la_CPPFLAGS = $(BUDDY_FLAGS)
-libbdd_la_SOURCES = \
+libbddx_la_LDFLAGS = -no-undefined -version-info 0:0:0
+libbddx_la_CPPFLAGS = $(BUDDY_FLAGS)
+libbddx_la_SOURCES = \
  bddio.c \
  bddop.c \
  bddtree.h \
@@ -30,4 +29,4 @@ libbdd_la_SOURCES = \
 check_PROGRAMS = bddtest
 bddtest_SOURCES = bddtest.cxx
 bddtest_CPPFLAGS = -I$(top_builddir)
-bddtest_LDADD = ./libbdd.la
+bddtest_LDADD = ./libbddx.la
diff --git a/buddy/src/bddtest.cxx b/buddy/src/bddtest.cxx
index 9a06ff68d..78b6bd064 100644
--- a/buddy/src/bddtest.cxx
+++ b/buddy/src/bddtest.cxx
@@ -29,8 +29,8 @@
 
 #include <string>
 #include <cstdlib>
-#include "bdd.h"
-#include "bvec.h"
+#include "bddx.h"
+#include "bvecx.h"
 
 using namespace std;
 
diff --git a/buddy/src/bdd.h b/buddy/src/bddx.h
similarity index 99%
rename from buddy/src/bdd.h
rename to buddy/src/bddx.h
index 405f3fd0a..03c7f1cc2 100644
--- a/buddy/src/bdd.h
+++ b/buddy/src/bddx.h
@@ -35,8 +35,8 @@
   DATE:  (C) feb 1997
 *************************************************************************/
 
-#ifndef _BDD_H
-#define _BDD_H
+#ifndef _BDDX_H
+#define _BDDX_H
 
 #if __GNUC__ >= 3
 #define __purefn __attribute__((__pure__))
@@ -1046,6 +1046,6 @@ BUDDY_API bddstrmhandler bdd_strm_hook(bddstrmhandler);
 
 #endif /* CPLUSPLUS */
 
-#endif /* _BDD_H */
+#endif /* _BDDX_H */
 
 /* EOF */
diff --git a/buddy/src/bvec.c b/buddy/src/bvec.c
index 937fefb37..b11af23d1 100644
--- a/buddy/src/bvec.c
+++ b/buddy/src/bvec.c
@@ -1,5 +1,5 @@
 /*========================================================================
-               Copyright (C) 1996-2002 by Jorn Lind-Nielsen
+               Copyright (C) 1996-2002, 2014 by Jorn Lind-Nielsen
                             All rights reserved
 
     Permission is hereby granted, without written agreement and without
@@ -36,7 +36,7 @@
 *************************************************************************/
 #include <stdlib.h>
 #include "kernel.h"
-#include "bvec.h"
+#include "bvecx.h"
 
 #define DEFAULT(v) { v.bitnum=0; v.bitvec=NULL; }
 
@@ -47,7 +47,7 @@ static bvec bvec_build(int bitnum, int isTrue)
 {
    bvec vec;
    int n;
-   
+
    vec.bitvec = NEW(BDD,bitnum);
    vec.bitnum = bitnum;
    if (!vec.bitvec)
@@ -94,7 +94,7 @@ bvec bvec_copy(bvec src)
 {
    bvec dst;
    int n;
-   
+
    if (src.bitnum == 0)
    {
       DEFAULT(dst);
@@ -102,7 +102,7 @@ bvec bvec_copy(bvec src)
    }
 
    dst = bvec_build(src.bitnum,0);
-   
+
    for (n=0 ; n<src.bitnum ; n++)
       dst.bitvec[n] = bdd_addref( src.bitvec[n] );
    dst.bitnum = src.bitnum;
@@ -191,7 +191,7 @@ bvec bvec_var(int bitnum, int offset, int step)
    int n;
 
    v = bvec_build(bitnum,0);
-   
+
    for (n=0 ; n<bitnum ; n++)
       v.bitvec[n] = bdd_ithvar(offset+n*step);
 
@@ -222,9 +222,9 @@ bvec bvec_varfdd(int var)
       DEFAULT(v);
       return v;
    }
-   
+
    v = bvec_build(varbitnum,0);
-   
+
    for (n=0 ; n<v.bitnum ; n++)
       v.bitvec[n] = bdd_ithvar(bddvar[n]);
 
@@ -248,7 +248,7 @@ bvec bvec_varvec(int bitnum, int *var)
    int n;
 
    v = bvec_build(bitnum,0);
-   
+
    for (n=0 ; n<bitnum ; n++)
       v.bitvec[n] = bdd_ithvar(var[n]);
 
@@ -413,7 +413,7 @@ bvec bvec_map1(bvec a, BDD (*fun)(BDD))
 {
    bvec res;
    int n;
-   
+
    res = bvec_build(a.bitnum,0);
    for (n=0 ; n < a.bitnum ; n++)
       res.bitvec[n] = bdd_addref( fun(a.bitvec[n]) );
@@ -450,7 +450,7 @@ bvec bvec_map2(bvec a, bvec b, BDD (*fun)(BDD,BDD))
       bdd_error(BVEC_SIZE);
       return res;
    }
-   
+
    res = bvec_build(a.bitnum,0);
    for (n=0 ; n < a.bitnum ; n++)
       res.bitvec[n] = bdd_addref( fun(a.bitvec[n], b.bitvec[n]) );
@@ -487,7 +487,7 @@ bvec bvec_map3(bvec a, bvec b, bvec c, BDD (*fun)(BDD,BDD,BDD))
       bdd_error(BVEC_SIZE);
       return res;
    }
-   
+
    res = bvec_build(a.bitnum,0);
    for (n=0 ; n < a.bitnum ; n++)
       res.bitvec[n] = bdd_addref( fun(a.bitvec[n], b.bitvec[n], c.bitvec[n]) );
@@ -527,16 +527,16 @@ bvec bvec_add(bvec l, bvec r)
       DEFAULT(res);
       return res;
    }
-   
+
    if (l.bitnum != r.bitnum)
    {
       bdd_error(BVEC_SIZE);
       DEFAULT(res);
       return res;
    }
-   
+
    res = bvec_build(l.bitnum,0);
-   
+
    for (n=0 ; n<res.bitnum ; n++)
    {
       BDD tmp1, tmp2, tmp3;
@@ -551,18 +551,18 @@ bvec bvec_add(bvec l, bvec r)
       tmp1 = bdd_addref( bdd_apply(l.bitvec[n], r.bitvec[n], bddop_or) );
       tmp2 = bdd_addref( bdd_apply(c, tmp1, bddop_and) );
       bdd_delref(tmp1);
-      
+
       tmp1 = bdd_addref( bdd_apply(l.bitvec[n], r.bitvec[n], bddop_and) );
       tmp3 = bdd_addref( bdd_apply(tmp1, tmp2, bddop_or) );
       bdd_delref(tmp1);
       bdd_delref(tmp2);
-      
+
       bdd_delref(c);
       c = tmp3;
    }
 
    bdd_delref(c);
-   
+
    return res;
 }
 
@@ -596,16 +596,16 @@ bvec bvec_sub(bvec l, bvec r)
       DEFAULT(res);
       return res;
    }
-   
+
    if (l.bitnum != r.bitnum)
    {
       bdd_error(BVEC_SIZE);
       DEFAULT(res);
       return res;
    }
-   
+
    res = bvec_build(l.bitnum,0);
-   
+
    for (n=0 ; n<res.bitnum ; n++)
    {
       BDD tmp1, tmp2, tmp3;
@@ -620,7 +620,7 @@ bvec bvec_sub(bvec l, bvec r)
       tmp1 = bdd_addref( bdd_apply(r.bitvec[n], c, bddop_or) );
       tmp2 = bdd_addref( bdd_apply(l.bitvec[n], tmp1, bddop_less) );
       bdd_delref(tmp1);
-      
+
       tmp1 = bdd_addref( bdd_apply(l.bitvec[n], r.bitvec[n], bddop_and) );
       tmp3 = bdd_addref( bdd_apply(tmp1, c, bddop_and) );
       bdd_delref(tmp1);
@@ -628,13 +628,13 @@ bvec bvec_sub(bvec l, bvec r)
       tmp1 = bdd_addref( bdd_apply(tmp3, tmp2, bddop_or) );
       bdd_delref(tmp2);
       bdd_delref(tmp3);
-      
+
       bdd_delref(c);
       c = tmp1;
    }
 
    bdd_delref(c);
-   
+
    return res;
 }
 
@@ -659,17 +659,17 @@ bvec bvec_mulfixed(bvec e, int c)
       DEFAULT(res);
       return res;
    }
-   
+
    if (c == 0)
       return bvec_build(e.bitnum,0);  /* return false array (base case) */
 
    next = bvec_build(e.bitnum,0);
    for (n=1 ; n<e.bitnum ; n++)
          /* e[] is never deleted, so no ref.cou. */
-      next.bitvec[n] = e.bitvec[n-1];    
-      
+      next.bitvec[n] = e.bitvec[n-1];
+
    rest = bvec_mulfixed(next, c>>1);
-   
+
    if (c & 0x1)
    {
       res = bvec_add(e, rest);
@@ -711,10 +711,10 @@ bvec bvec_mul(bvec left, bvec right)
    res = bvec_false(bitnum);
    leftshifttmp = bvec_copy(left);
    leftshift = bvec_coerce(bitnum, leftshifttmp);
-   
+
    /*bvec_delref(leftshifttmp);*/
    bvec_free(leftshifttmp);
-   
+
    for (n=0 ; n<right.bitnum ; n++)
    {
       bvec added = bvec_add(res, leftshift);
@@ -733,14 +733,14 @@ bvec bvec_mul(bvec left, bvec right)
       for (m=bitnum-1 ; m>=1 ; m--)
 	 leftshift.bitvec[m] = leftshift.bitvec[m-1];
       leftshift.bitvec[0] = bddfalse;
-      
+
       /*bvec_delref(added);*/
       bvec_free(added);
    }
 
    /*bvec_delref(leftshift);*/
    bvec_free(leftshift);
-   
+
    return res;
 }
 
@@ -760,12 +760,12 @@ static void bvec_div_rec(bvec divisor, bvec *remainder, bvec *result, int step)
 
    if (step > 1)
       bvec_div_rec( divisor, &newRemainder, &newResult, step-1 );
-   
+
    bvec_free(tmp);
    bvec_free(sub);
    bvec_free(zero);
    bdd_delref(isSmaller);
-   
+
    bvec_free(*remainder);
    bvec_free(*result);
    *result = newResult;
@@ -796,17 +796,17 @@ int bvec_divfixed(bvec e, int c, bvec *res, bvec *rem)
       bvec tmpremainder = bvec_shlfixed(tmp, 1, e.bitvec[e.bitnum-1]);
       bvec result = bvec_shlfixed(e, 1, bddfalse);
       bvec remainder;
-      
+
       bvec_div_rec(divisor, &tmpremainder, &result, divisor.bitnum);
       remainder = bvec_shrfixed(tmpremainder, 1, bddfalse);
 
       bvec_free(tmp);
       bvec_free(tmpremainder);
       bvec_free(divisor);
-      
+
       *res = result;
       *rem = remainder;
-      
+
       return 0;
    }
 
@@ -899,7 +899,7 @@ int bvec_div(bvec left, bvec right, bvec *result, bvec *remainder)
 
    /*bvec_delref(rem);*/
    bvec_free(rem);
-   
+
    return 0;
 }
 
@@ -931,7 +931,7 @@ bvec bvec_ite(bdd a, bvec b, bvec c)
   }
 
   res = bvec_build(b.bitnum, 0);
-  
+
   for (n=0 ; n<b.bitnum ; ++n)
   {
     res.bitvec[n] = bdd_addref( bdd_ite(a, b.bitvec[n], c.bitvec[n]) );
@@ -963,21 +963,21 @@ bvec bvec_shlfixed(bvec e, int pos, BDD c)
       DEFAULT(res);
       return res;
    }
-   
+
    if (e.bitnum == 0)
    {
       DEFAULT(res);
       return res;
    }
-   
+
    res = bvec_build(e.bitnum,0);
 
    for (n=0 ; n<minnum ; n++)
       res.bitvec[n] = bdd_addref(c);
-   
+
    for (n=minnum ; n<e.bitnum ; n++)
       res.bitvec[n] = bdd_addref(e.bitvec[n-pos]);
-   
+
    return res;
 }
 
@@ -1005,14 +1005,14 @@ BVEC bvec_shl(BVEC l, BVEC r, BDD c)
       DEFAULT(res);
       return res;
    }
-   
+
    res = bvec_build(l.bitnum, 0);
 
    for (n=0 ; n<=l.bitnum ; n++)
    {
       val = bvec_con(r.bitnum, n);
       rEquN = bdd_addref( bvec_equ(r, val) );
-      
+
       for (m=0 ; m<l.bitnum ; m++)
       {
    	    /* Set the m'th new location to be the (m+n)'th old location */
@@ -1040,7 +1040,7 @@ BVEC bvec_shl(BVEC l, BVEC r, BDD c)
    for (m=0 ; m<l.bitnum ; m++)
    {
       tmp2 = bdd_addref( bdd_or(res.bitvec[m], tmp1) );
-      
+
       bdd_delref(res.bitvec[m]);
       res.bitvec[m] = tmp2;
    }
@@ -1049,7 +1049,7 @@ BVEC bvec_shl(BVEC l, BVEC r, BDD c)
    bdd_delref(rEquN);
    /*bvec_delref(val);*/
    bvec_free(val);
-   
+
    return res;
 }
 
@@ -1068,25 +1068,25 @@ bvec bvec_shrfixed(bvec e, int pos, BDD c)
 {
    bvec res;
    int n, maxnum = MAX(0,e.bitnum-pos);
-   
+
    if (pos < 0)
    {
       bdd_error(BVEC_SHIFT);
       DEFAULT(res);
       return res;
    }
-   
+
    if (e.bitnum == 0)
    {
       DEFAULT(res);
       return res;
    }
-   
+
    res = bvec_build(e.bitnum,0);
 
    for (n=maxnum ; n<e.bitnum ; n++)
       res.bitvec[n] = bdd_addref(c);
-   
+
    for (n=0 ; n<maxnum ; n++)
       res.bitvec[n] = bdd_addref(e.bitvec[n+pos]);
 
@@ -1117,14 +1117,14 @@ BVEC bvec_shr(BVEC l, BVEC r, BDD c)
       DEFAULT(res);
       return res;
    }
-   
+
    res = bvec_build(l.bitnum, 0);
 
    for (n=0 ; n<=l.bitnum ; n++)
    {
       val = bvec_con(r.bitnum, n);
       rEquN = bdd_addref( bvec_equ(r, val) );
-      
+
       for (m=0 ; m<l.bitnum ; m++)
       {
    	    /* Set the m'th new location to be the (m+n)'th old location */
@@ -1152,7 +1152,7 @@ BVEC bvec_shr(BVEC l, BVEC r, BDD c)
    for (m=0 ; m<l.bitnum ; m++)
    {
       tmp2 = bdd_addref( bdd_or(res.bitvec[m], tmp1) );
-      
+
       bdd_delref(res.bitvec[m]);
       res.bitvec[m] = tmp2;
    }
@@ -1161,7 +1161,7 @@ BVEC bvec_shr(BVEC l, BVEC r, BDD c)
    bdd_delref(rEquN);
    /*bvec_delref(val);*/
    bvec_free(val);
-   
+
    return res;
 }
 
@@ -1180,21 +1180,21 @@ bdd bvec_lth(bvec l, bvec r)
 {
    BDD p = bddfalse;
    int n;
-   
+
    if (l.bitnum == 0  ||  r.bitnum == 0)
       return bddfalse;
-   
+
    if (l.bitnum != r.bitnum)
    {
       bdd_error(BVEC_SIZE);
       return p;
    }
-   
+
    for (n=0 ; n<l.bitnum ; n++)
    {
       /* p = (!l[n] & r[n]) |
        *     bdd_apply(l[n], r[n], bddop_biimp) & p; */
-      
+
       BDD tmp1 = bdd_addref(bdd_apply(l.bitvec[n],r.bitvec[n],bddop_less));
       BDD tmp2 = bdd_addref(bdd_apply(l.bitvec[n],r.bitvec[n],bddop_biimp));
       BDD tmp3 = bdd_addref( bdd_apply(tmp2, p, bddop_and) );
@@ -1224,21 +1224,21 @@ bdd bvec_lte(bvec l, bvec r)
 {
    BDD p = bddtrue;
    int n;
-   
+
    if (l.bitnum == 0  ||  r.bitnum == 0)
       return bddfalse;
-   
+
    if (l.bitnum != r.bitnum)
    {
       bdd_error(BVEC_SIZE);
       return p;
    }
-   
+
    for (n=0 ; n<l.bitnum ; n++)
    {
       /* p = (!l[n] & r[n]) |
        *     bdd_apply(l[n], r[n], bddop_biimp) & p; */
-      
+
       BDD tmp1 = bdd_addref( bdd_apply(l.bitvec[n], r.bitvec[n], bddop_less) );
       BDD tmp2 = bdd_addref( bdd_apply(l.bitvec[n], r.bitvec[n], bddop_biimp) );
       BDD tmp3 = bdd_addref( bdd_apply(tmp2, p, bddop_and) );
@@ -1306,16 +1306,16 @@ bdd bvec_equ(bvec l, bvec r)
 {
    BDD p = bddtrue;
    int n;
-   
+
    if (l.bitnum == 0  ||  r.bitnum == 0)
       return bddfalse;
-   
+
    if (l.bitnum != r.bitnum)
    {
       bdd_error(BVEC_SIZE);
       return p;
    }
-   
+
    for (n=0 ; n<l.bitnum ; n++)
    {
       BDD tmp1, tmp2;
diff --git a/buddy/src/bvec.h b/buddy/src/bvecx.h
similarity index 99%
rename from buddy/src/bvec.h
rename to buddy/src/bvecx.h
index baa2dd522..7c08469ce 100644
--- a/buddy/src/bvec.h
+++ b/buddy/src/bvecx.h
@@ -35,10 +35,10 @@
   DATE:  (C) may 1999
 *************************************************************************/
 
-#ifndef _BVEC_H
-#define _BVEC_H
+#ifndef _BVECX_H
+#define _BVECX_H
 
-#include "fdd.h"
+#include "fddx.h"
 
    /* Boolean (BDD) vector */
 /*
@@ -295,6 +295,6 @@ inline bdd  bvec_neq(const bvec &left, const bvec &right)
 
 #endif /* CPLUSPLUS */
 
-#endif /* _BVEC_H */
+#endif /* _BVECX_H */
 
 /* EOF */
diff --git a/buddy/src/cppext.cxx b/buddy/src/cppext.cxx
index 5c879b69b..0a26d8e38 100644
--- a/buddy/src/cppext.cxx
+++ b/buddy/src/cppext.cxx
@@ -38,7 +38,7 @@
 #include <stdlib.h>
 #include <iomanip>
 #include "kernel.h"
-#include "bvec.h"
+#include "bvecx.h"
 
 using namespace std;
 
diff --git a/buddy/src/fdd.c b/buddy/src/fdd.c
index 639622bd4..1c108548d 100644
--- a/buddy/src/fdd.c
+++ b/buddy/src/fdd.c
@@ -39,7 +39,7 @@
 #include <stdlib.h>
 #include <string.h>
 #include "kernel.h"
-#include "fdd.h"
+#include "fddx.h"
 
 
 static void fdd_printset_rec(FILE *, int, int *);
@@ -83,7 +83,7 @@ void bdd_fdd_init(void)
 void bdd_fdd_done(void)
 {
    int n;
-   
+
    if (domain != NULL)
    {
       for (n=0 ; n<fdvarnum ; n++)
@@ -129,7 +129,7 @@ int fdd_extdomain(int *dom, int num)
 
    if (!bddrunning)
       return bdd_error(BDD_RUNNING);
-   
+
       /* Build domain table */
    if (domain == NULL)  /* First time */
    {
@@ -142,7 +142,7 @@ int fdd_extdomain(int *dom, int num)
       if (fdvarnum + num > fdvaralloc)
       {
          fdvaralloc += (num > fdvaralloc) ? num : fdvaralloc;
-	 
+
 	 domain = (Domain*)realloc(domain, sizeof(Domain)*fdvaralloc);
 	 if (domain == NULL)
 	    return bdd_error(BDD_MEMORY);
@@ -182,7 +182,7 @@ int fdd_extdomain(int *dom, int num)
 
    fdvarnum += num;
    firstbddvar += extravars;
-   
+
    return offset;
 }
 
@@ -208,17 +208,17 @@ int fdd_overlapdomain(int v1, int v2)
 {
    Domain *d;
    int n;
-   
+
    if (!bddrunning)
       return bdd_error(BDD_RUNNING);
-   
+
    if (v1 < 0  ||  v1 >= fdvarnum  ||  v2 < 0  ||  v2 >= fdvarnum)
       return bdd_error(BDD_VAR);
 
    if (fdvarnum + 1 > fdvaralloc)
    {
       fdvaralloc += fdvaralloc;
-      
+
       domain = (Domain*)realloc(domain, sizeof(Domain)*fdvaralloc);
       if (domain == NULL)
 	 return bdd_error(BDD_MEMORY);
@@ -233,10 +233,10 @@ int fdd_overlapdomain(int v1, int v2)
       d->ivar[n] = domain[v1].ivar[n];
    for (n=0 ; n<domain[v2].binsize ; n++)
       d->ivar[domain[v1].binsize+n] = domain[v2].ivar[n];
-	 
+
    d->var = bdd_makeset(d->ivar, d->binsize);
    bdd_addref(d->var);
-   
+
    return fdvarnum++;
 }
 
@@ -275,7 +275,7 @@ int fdd_domainnum(void)
 {
    if (!bddrunning)
       return bdd_error(BDD_RUNNING);
-   
+
    return fdvarnum;
 }
 
@@ -294,7 +294,7 @@ int fdd_domainsize(int v)
 {
    if (!bddrunning)
       return bdd_error(BDD_RUNNING);
-   
+
    if (v < 0  ||  v >= fdvarnum)
       return bdd_error(BDD_VAR);
    return domain[v].realsize;
@@ -315,7 +315,7 @@ int fdd_varnum(int v)
 {
    if (!bddrunning)
       return bdd_error(BDD_RUNNING);
-   
+
    if (v >= fdvarnum  ||  v < 0)
       return bdd_error(BDD_VAR);
    return domain[v].binsize;
@@ -343,7 +343,7 @@ int *fdd_vars(int v)
       bdd_error(BDD_RUNNING);
       return NULL;
    }
-   
+
    if (v >= fdvarnum  ||  v < 0)
    {
       bdd_error(BDD_VAR);
@@ -378,13 +378,13 @@ BDD fdd_ithvar(int var, int val)
 {
    int n;
    int v=1, tmp;
-   
+
    if (!bddrunning)
    {
       bdd_error(BDD_RUNNING);
       return bddfalse;
    }
-   
+
    if (var < 0  ||  var >= fdvarnum)
    {
       bdd_error(BDD_VAR);
@@ -400,7 +400,7 @@ BDD fdd_ithvar(int var, int val)
    for (n=0 ; n<domain[var].binsize ; n++)
    {
       bdd_addref(v);
-      
+
       if (val & 0x1)
 	 tmp = bdd_apply(bdd_ithvar(domain[var].ivar[n]), v, bddop_and);
       else
@@ -465,11 +465,11 @@ int* fdd_scanallvar(BDD r)
    char *store;
    int *res;
    BDD p = r;
-   
+
    CHECKa(r,NULL);
    if (r == bddfalse)
       return NULL;
-   
+
    store = NEW(char,bddvarnum);
    for (n=0 ; n<bddvarnum ; n++)
       store[n] = 0;
@@ -494,21 +494,21 @@ int* fdd_scanallvar(BDD r)
    {
       int m;
       int val=0;
-      
+
       for (m=domain[n].binsize-1 ; m>=0 ; m--)
 	 if ( store[domain[n].ivar[m]] )
 	    val = val*2 + 1;
          else
 	    val = val*2;
-      
+
       res[n] = val;
    }
-   
+
    free(store);
-   
+
    return res;
 }
-   
+
 /*
 NAME    {* fdd\_ithset *}
 SECTION {* fdd *}
@@ -526,7 +526,7 @@ BDD fdd_ithset(int var)
       bdd_error(BDD_RUNNING);
       return bddfalse;
    }
-   
+
    if (var < 0  ||  var >= fdvarnum)
    {
       bdd_error(BDD_VAR);
@@ -553,13 +553,13 @@ BDD fdd_domain(int var)
    int n,val;
    Domain *dom;
    BDD d;
-      
+
    if (!bddrunning)
    {
       bdd_error(BDD_RUNNING);
       return bddfalse;
    }
-   
+
    if (var < 0  ||  var >= fdvarnum)
    {
       bdd_error(BDD_VAR);
@@ -567,15 +567,15 @@ BDD fdd_domain(int var)
    }
 
       /* Encode V<=X-1. V is the variables in 'var' and X is the domain size */
-   
+
    dom = &domain[var];
    val = dom->realsize-1;
    d = bddtrue;
-   
+
    for (n=0 ; n<dom->binsize ; n++)
    {
       BDD tmp;
-      
+
       if (val & 0x1)
 	 tmp = bdd_apply( bdd_nithvar(dom->ivar[n]), d, bddop_or );
       else
@@ -607,13 +607,13 @@ BDD fdd_equals(int left, int right)
 {
    BDD e = bddtrue, tmp1, tmp2;
    int n;
-   
+
    if (!bddrunning)
    {
       bdd_error(BDD_RUNNING);
       return bddfalse;
    }
-   
+
    if (left < 0  ||  left >= fdvarnum  ||  right < 0  ||  right >= fdvarnum)
    {
       bdd_error(BDD_VAR);
@@ -624,13 +624,13 @@ BDD fdd_equals(int left, int right)
       bdd_error(BDD_RANGE);
       return bddfalse;
    }
-   
+
    for (n=0 ; n<domain[left].binsize ; n++)
    {
       tmp1 = bdd_addref( bdd_apply(bdd_ithvar(domain[left].ivar[n]),
 				   bdd_ithvar(domain[right].ivar[n]),
 				   bddop_biimp) );
-      
+
       tmp2 = bdd_addref( bdd_apply(e, tmp1, bddop_and) );
       bdd_delref(tmp1);
       bdd_delref(e);
@@ -704,13 +704,13 @@ void fdd_printset(BDD r)
 void fdd_fprintset(FILE *ofile, BDD r)
 {
    int *set;
-   
+
    if (!bddrunning)
    {
       bdd_error(BDD_RUNNING);
       return;
    }
-   
+
    if (r < 2)
    {
       fprintf(ofile, "%s", r == 0 ? "F" : "T");
@@ -723,7 +723,7 @@ void fdd_fprintset(FILE *ofile, BDD r)
       bdd_error(BDD_MEMORY);
       return;
    }
-   
+
    memset(set, 0, sizeof(int) * bddvarnum);
    fdd_printset_rec(ofile, r, set);
    free(set);
@@ -737,7 +737,7 @@ static void fdd_printset_rec(FILE *ofile, int r, int *set)
    int *var;
    int *binval;
    int ok, first;
-   
+
    if (r == 0)
       return;
    else
@@ -754,7 +754,7 @@ static void fdd_printset_rec(FILE *ofile, int r, int *set)
 	 for (m=0 ; m<domain[n].binsize ; m++)
 	    if (set[domain[n].ivar[m]] != 0)
 	       used = 1;
-	 
+
 	 if (used)
 	 {
 	    if (!first)
@@ -767,12 +767,12 @@ static void fdd_printset_rec(FILE *ofile, int r, int *set)
 	    printf(":");
 
 	    var = domain[n].ivar;
-	    
+
 	    for (m=0 ; m<(1<<domain[n].binsize) ; m++)
 	    {
 	       binval = fdddec2bin(n, m);
 	       ok=1;
-	       
+
 	       for (i=0 ; i<domain[n].binsize && ok ; i++)
 		  if (set[var[i]] == 1  &&  binval[i] != 0)
 		     ok = 0;
@@ -800,10 +800,10 @@ static void fdd_printset_rec(FILE *ofile, int r, int *set)
    {
       set[bddlevel2var[LEVEL(r)]] = 1;
       fdd_printset_rec(ofile, LOW(r), set);
-      
+
       set[bddlevel2var[LEVEL(r)]] = 2;
       fdd_printset_rec(ofile, HIGH(r), set);
-      
+
       set[bddlevel2var[LEVEL(r)]] = 0;
    }
 }
@@ -828,17 +828,17 @@ int fdd_scanset(BDD r, int **varset, int *varnum)
 {
    int *fv, fn;
    int num,n,m,i;
-      
+
    if (!bddrunning)
       return bdd_error(BDD_RUNNING);
-   
+
    if ((n=bdd_scanset(r, &fv, &fn)) < 0)
       return n;
 
    for (n=0,num=0 ; n<fdvarnum ; n++)
    {
       int found=0;
-      
+
       for (m=0 ; m<domain[n].binsize && !found ; m++)
       {
 	 for (i=0 ; i<fn && !found ; i++)
@@ -856,7 +856,7 @@ int fdd_scanset(BDD r, int **varset, int *varnum)
    for (n=0,num=0 ; n<fdvarnum ; n++)
    {
       int found=0;
-      
+
       for (m=0 ; m<domain[n].binsize && !found ; m++)
       {
 	 for (i=0 ; i<fn && !found ; i++)
@@ -897,14 +897,14 @@ BDD fdd_makeset(int *varset, int varnum)
       bdd_error(BDD_RUNNING);
       return bddfalse;
    }
-   
+
    for (n=0 ; n<varnum ; n++)
       if (varset[n] < 0  ||  varset[n] >= fdvarnum)
       {
 	 bdd_error(BDD_VAR);
 	 return bddfalse;
       }
-	  
+
    for (n=0 ; n<varnum ; n++)
    {
       bdd_addref(res);
@@ -932,10 +932,10 @@ int fdd_intaddvarblock(int first, int last, int fixed)
 {
    bdd res = bddtrue, tmp;
    int n, err;
-   
+
    if (!bddrunning)
       return bdd_error(BDD_RUNNING);
-   
+
    if (first > last ||  first < 0  ||  last >= fdvarnum)
       return bdd_error(BDD_VARBLK);
 
@@ -948,7 +948,7 @@ int fdd_intaddvarblock(int first, int last, int fixed)
    }
 
    err = bdd_addvarblock(res, fixed);
-   
+
    bdd_delref(res);
    return err;
 }
@@ -972,10 +972,10 @@ int fdd_setpair(bddPair *pair, int p1, int p2)
 
    if (!bddrunning)
       return bdd_error(BDD_RUNNING);
-   
+
    if (p1<0 || p1>=fdvarnum || p2<0 || p2>=fdvarnum)
       return bdd_error(BDD_VAR);
-   
+
    if (domain[p1].binsize != domain[p2].binsize)
       return bdd_error(BDD_VARNUM);
 
@@ -1006,11 +1006,11 @@ int fdd_setpairs(bddPair *pair, int *p1, int *p2, int size)
 
    if (!bddrunning)
       return bdd_error(BDD_RUNNING);
-   
+
    for (n=0 ; n<size ; n++)
       if (p1[n]<0 || p1[n]>=fdvarnum || p2[n]<0 || p2[n]>=fdvarnum)
 	 return bdd_error(BDD_VAR);
-   
+
    for (n=0 ; n<size ; n++)
       if ((e=fdd_setpair(pair, p1[n], p2[n])) < 0)
 	 return e;
@@ -1033,7 +1033,7 @@ static void Domain_done(Domain* d)
 static void Domain_allocate(Domain* d, int range)
 {
    int calcsize = 2;
-   
+
    if (range <= 0  || range > INT_MAX/2)
    {
       bdd_error(BDD_RANGE);
diff --git a/buddy/src/fdd.h b/buddy/src/fddx.h
similarity index 98%
rename from buddy/src/fdd.h
rename to buddy/src/fddx.h
index 5cdfdb533..7a1494ef0 100644
--- a/buddy/src/fdd.h
+++ b/buddy/src/fddx.h
@@ -35,10 +35,10 @@
   DATE:  (C) february 1999
 *************************************************************************/
 
-#ifndef _FDD_H
-#define _FDD_H
+#ifndef _FDDX_H
+#define _FDDX_H
 
-#include "bdd.h"
+#include "bddx.h"
 
 
 #ifdef CPLUSPLUS
@@ -167,7 +167,7 @@ inline bdd fdd_neq(int bitnum, bdd *left, bdd *right)
 
 #endif /* CPLUSPLUS */
 
-#endif /* _FDD_H */
+#endif /* _FDDX_H */
 
 
 /* EOF */
diff --git a/buddy/src/imatrix.h b/buddy/src/imatrix.h
index f113a9228..b772525af 100644
--- a/buddy/src/imatrix.h
+++ b/buddy/src/imatrix.h
@@ -37,7 +37,7 @@
 #ifndef _IMATRIX_H
 #define _IMATRIX_H
 
-#include "bdd.h" /* for __purefn */
+#include "bddx.h" /* for __purefn */
 
 typedef struct _imatrix
 {
diff --git a/buddy/src/kernel.h b/buddy/src/kernel.h
index 84b6335b5..759d1cd07 100644
--- a/buddy/src/kernel.h
+++ b/buddy/src/kernel.h
@@ -42,7 +42,7 @@
 
 #include <limits.h>
 #include <setjmp.h>
-#include "bdd.h"
+#include "bddx.h"
 #ifdef HAVE_CONFIG_H
 # include "config.h"
 #endif
diff --git a/m4/buddy.m4 b/m4/buddy.m4
index f76859413..7e78e79b1 100644
--- a/m4/buddy.m4
+++ b/m4/buddy.m4
@@ -1,33 +1,5 @@
 AC_DEFUN([AX_CHECK_BUDDY], [
-  AC_ARG_WITH([included-buddy],
-	      [AC_HELP_STRING([--with-included-buddy],
-			      [use the BuDDy library included here])])
-  AC_CHECK_LIB([bdd], [bdd_implies],
-	       [need_included_buddy=no],
-	       [need_included_buddy=yes])
-
-  if test "$need_included_buddy" = yes; then
-     if test "$with_included_buddy" = no; then
-       AC_MSG_ERROR([Could not link with BuDDy.  Please install BuDDy first,
-		    set CPPFLAGS/LDFLAGS appropriately, or configure with
-		    --with-included-buddy])
-     else
-	with_included_buddy=yes
-     fi
-  fi
-
-  if test "$with_included_buddy" = yes;  then
-     BUDDY_LDFLAGS='$(top_builddir)/buddy/src/libbdd.la'
-     BUDDY_CPPFLAGS='-I$(top_srcdir)/buddy/src'
-  else
-     BUDDY_LDFLAGS='-lbdd'
-  fi
-  # We always configure BuDDy, this is needed to ensure
-  # it gets distributed properly.  Whether with_included_buddy is
-  # set or not affects whether we *use* or *build* BuDDy.
+  AC_SUBST([BUDDY_LDFLAGS], ['$(top_builddir)/buddy/src/libbddx.la'])
+  AC_SUBST([BUDDY_CPPFLAGS], ['-I$(top_srcdir)/buddy/src'])
   AC_CONFIG_SUBDIRS([buddy])
-
-  AM_CONDITIONAL([WITH_INCLUDED_BUDDY], [test "$with_included_buddy" = yes])
-  AC_SUBST([BUDDY_LDFLAGS])
-  AC_SUBST([BUDDY_CPPFLAGS])
 ])
diff --git a/src/ltlvisit/apcollect.hh b/src/ltlvisit/apcollect.hh
index 8e591f484..8dd46cee6 100644
--- a/src/ltlvisit/apcollect.hh
+++ b/src/ltlvisit/apcollect.hh
@@ -25,7 +25,7 @@
 
 #include "ltlast/atomic_prop.hh"
 #include <set>
-#include "bdd.h"
+#include <bddx.h>
 #include "tgba/fwd.hh"
 
 namespace spot
diff --git a/src/ltlvisit/simplify.hh b/src/ltlvisit/simplify.hh
index 19e62bdc4..e7e9e46bf 100644
--- a/src/ltlvisit/simplify.hh
+++ b/src/ltlvisit/simplify.hh
@@ -21,7 +21,7 @@
 # define SPOT_LTLVISIT_SIMPLIFY_HH
 
 #include "ltlast/formula.hh"
-#include "bdd.h"
+#include <bddx.h>
 #include "tgba/bdddict.hh"
 #include <iosfwd>
 
diff --git a/src/misc/bddlt.hh b/src/misc/bddlt.hh
index ed0057fb0..b1c92e332 100644
--- a/src/misc/bddlt.hh
+++ b/src/misc/bddlt.hh
@@ -1,7 +1,8 @@
-// Copyright (C) 2011 Laboratoire de Recherche et Developpement de
+// -*- coding: utf-8 -*-
+// Copyright (C) 2011, 2014 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
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
@@ -22,7 +23,7 @@
 #ifndef SPOT_MISC_BDDLT_HH
 # define SPOT_MISC_BDDLT_HH
 
-# include <bdd.h>
+# include <bddx.h>
 # include <functional>
 
 namespace spot
diff --git a/src/misc/bddop.hh b/src/misc/bddop.hh
index 5425ab702..213949dcf 100644
--- a/src/misc/bddop.hh
+++ b/src/misc/bddop.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2013 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2009, 2013, 2014 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -21,7 +21,7 @@
 # define SPOT_MISC_BDDOP_HH
 
 #include "common.hh"
-#include "bdd.h"
+#include <bddx.h>
 
 namespace spot
 {
diff --git a/src/misc/minato.hh b/src/misc/minato.hh
index bcc320d11..ad9e4dd00 100644
--- a/src/misc/minato.hh
+++ b/src/misc/minato.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2013 Laboratoire de Recherche et Développement
+// Copyright (C) 2009, 2013, 2014 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
@@ -24,7 +24,7 @@
 # define SPOT_MISC_MINATO_HH
 
 # include "common.hh"
-# include <bdd.h>
+# include <bddx.h>
 # include <stack>
 
 namespace spot
diff --git a/src/priv/acccompl.hh b/src/priv/acccompl.hh
index 43433e552..f65bf1074 100644
--- a/src/priv/acccompl.hh
+++ b/src/priv/acccompl.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013 Laboratoire de Recherche et Developpement de
-// l'Epita (LRDE)
+// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
+// Developpement de l'Epita (LRDE)
 //
 // This file is part of Spot, a model checking library.
 //
@@ -22,7 +22,7 @@
 # define SPOT_PRIV_ACCCOMPL_HH
 
 #include <map>
-#include <bdd.h>
+#include <bddx.h>
 #include "misc/hash.hh"
 #include "misc/bddlt.hh"
 
diff --git a/src/priv/accconv.hh b/src/priv/accconv.hh
index 00ef88737..639b8a5d2 100644
--- a/src/priv/accconv.hh
+++ b/src/priv/accconv.hh
@@ -1,5 +1,6 @@
-// Copyright (C) 2011, 2013 Laboratoire de Recherche et Developpement de
-// l'Epita (LRDE)
+// -*- coding: utf-8 -*-
+// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et
+// Developpement de l'Epita (LRDE)
 //
 // This file is part of Spot, a model checking library.
 //
@@ -19,7 +20,7 @@
 #ifndef SPOT_PRIV_ACCCONV_HH
 # define SPOT_PRIV_ACCCONV_HH
 
-#include <bdd.h>
+#include <bddx.h>
 #include "misc/hash.hh"
 #include "misc/bddlt.hh"
 
diff --git a/src/priv/accmap.hh b/src/priv/accmap.hh
index 0710422b0..e82f57dd4 100644
--- a/src/priv/accmap.hh
+++ b/src/priv/accmap.hh
@@ -20,7 +20,7 @@
 #ifndef SPOT_PRIV_ACCMAP_HH
 # define SPOT_PRIV_ACCMAP_HH
 
-#include <bdd.h>
+#include <bddx.h>
 #include "misc/hash.hh"
 #include "ltlast/formula.hh"
 #include "ltlenv/defaultenv.hh"
diff --git a/src/priv/bddalloc.cc b/src/priv/bddalloc.cc
index d385bc0c0..023e0c7cb 100644
--- a/src/priv/bddalloc.cc
+++ b/src/priv/bddalloc.cc
@@ -20,7 +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 <bdd.h>
+#include <bddx.h>
 #include <cassert>
 #include "bddalloc.hh"
 
diff --git a/src/tgba/bdddict.hh b/src/tgba/bdddict.hh
index c67b2aa41..921fc9ca1 100644
--- a/src/tgba/bdddict.hh
+++ b/src/tgba/bdddict.hh
@@ -27,7 +27,7 @@
 #include <set>
 #include <map>
 #include <iosfwd>
-#include <bdd.h>
+#include <bddx.h>
 #include <vector>
 #include <memory>
 #include "ltlast/formula.hh"
diff --git a/src/tgba/bddprint.hh b/src/tgba/bddprint.hh
index f8930ef6e..099e8dc3c 100644
--- a/src/tgba/bddprint.hh
+++ b/src/tgba/bddprint.hh
@@ -26,7 +26,7 @@
 #include <string>
 #include <iosfwd>
 #include "bdddict.hh"
-#include <bdd.h>
+#include <bddx.h>
 
 namespace spot
 {
diff --git a/src/tgba/tgbamask.hh b/src/tgba/tgbamask.hh
index 0d6dc046c..bfe11c698 100644
--- a/src/tgba/tgbamask.hh
+++ b/src/tgba/tgbamask.hh
@@ -20,8 +20,8 @@
 #ifndef SPOT_TGBA_TGBAMASK_HH
 # define SPOT_TGBA_TGBAMASK_HH
 
+#include <bddx.h>
 #include "tgbaproxy.hh"
-#include "bdd.h"
 
 namespace spot
 {
diff --git a/src/tgba/tgbasafracomplement.cc b/src/tgba/tgbasafracomplement.cc
index 978fff8ce..258f21ee7 100644
--- a/src/tgba/tgbasafracomplement.cc
+++ b/src/tgba/tgbasafracomplement.cc
@@ -24,7 +24,7 @@
 #include <sstream>
 #include <algorithm>
 #include "misc/bitvect.hh"
-#include "bdd.h"
+#include <bddx.h>
 #include "misc/hash.hh"
 #include "misc/bddlt.hh"
 #include "tgba/bdddict.hh"
diff --git a/src/tgbaalgos/emptiness.hh b/src/tgbaalgos/emptiness.hh
index 2173bf4a2..e411498a2 100644
--- a/src/tgbaalgos/emptiness.hh
+++ b/src/tgbaalgos/emptiness.hh
@@ -26,7 +26,7 @@
 #include <map>
 #include <list>
 #include <iosfwd>
-#include <bdd.h>
+#include <bddx.h>
 #include "misc/optionmap.hh"
 #include "tgba/tgbagraph.hh"
 #include "emptiness_stats.hh"
diff --git a/src/tgbaalgos/gtec/sccstack.hh b/src/tgbaalgos/gtec/sccstack.hh
index fc7b0f0ce..9433348bf 100644
--- a/src/tgbaalgos/gtec/sccstack.hh
+++ b/src/tgbaalgos/gtec/sccstack.hh
@@ -23,7 +23,7 @@
 #ifndef SPOT_TGBAALGOS_GTEC_SCCSTACK_HH
 # define SPOT_TGBAALGOS_GTEC_SCCSTACK_HH
 
-#include <bdd.h>
+#include <bddx.h>
 #include <list>
 #include "tgba/tgba.hh"
 
diff --git a/src/tgbaalgos/neverclaim.cc b/src/tgbaalgos/neverclaim.cc
index c8e39da2b..c39a3d5e7 100644
--- a/src/tgbaalgos/neverclaim.cc
+++ b/src/tgbaalgos/neverclaim.cc
@@ -22,7 +22,6 @@
 
 #include <ostream>
 #include <sstream>
-#include "bdd.h"
 #include "neverclaim.hh"
 #include "tgba/bddprint.hh"
 #include "tgba/tgbagraph.hh"
diff --git a/src/tgbaalgos/powerset.cc b/src/tgbaalgos/powerset.cc
index 0e18a8ea9..6e478885a 100644
--- a/src/tgbaalgos/powerset.cc
+++ b/src/tgbaalgos/powerset.cc
@@ -27,7 +27,6 @@
 #include "powerset.hh"
 #include "misc/hash.hh"
 #include "tgbaalgos/powerset.hh"
-#include "bdd.h"
 #include "tgbaalgos/sccinfo.hh"
 #include "tgbaalgos/cycles.hh"
 #include "tgbaalgos/gtec/gtec.hh"
diff --git a/src/tgbaalgos/sccfilter.hh b/src/tgbaalgos/sccfilter.hh
index b63b669db..a807d47cb 100644
--- a/src/tgbaalgos/sccfilter.hh
+++ b/src/tgbaalgos/sccfilter.hh
@@ -21,7 +21,7 @@
 # define SPOT_TGBAALGOS_SCCFILTER_HH
 
 #include "misc/common.hh"
-#include <bdd.h>
+#include <bddx.h>
 #include "tgba/fwd.hh"
 
 namespace spot
diff --git a/src/tgbaalgos/sccinfo.hh b/src/tgbaalgos/sccinfo.hh
index ec92a5761..0588dd5cb 100644
--- a/src/tgbaalgos/sccinfo.hh
+++ b/src/tgbaalgos/sccinfo.hh
@@ -21,7 +21,6 @@
 # define SPOT_TGBAALGOS_SCCINFO_HH
 
 #include <vector>
-#include "bdd.h"
 #include "tgba/tgbagraph.hh"
 
 namespace spot
diff --git a/src/tgbaalgos/weight.hh b/src/tgbaalgos/weight.hh
index 5d98251bd..9aa327a12 100644
--- a/src/tgbaalgos/weight.hh
+++ b/src/tgbaalgos/weight.hh
@@ -22,7 +22,7 @@
 
 #include <iosfwd>
 #include <map>
-#include <bdd.h>
+#include <bddx.h>
 #include "tgba/acc.hh"
 
 namespace spot
diff --git a/wrap/python/buddy.i b/wrap/python/buddy.i
index e25aecaf1..a87097961 100644
--- a/wrap/python/buddy.i
+++ b/wrap/python/buddy.i
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2012  Laboratoire de Recherche et
+// Copyright (C) 2010, 2011, 2012, 2014 Laboratoire de Recherche et
 // Développement de l'EPITA.
 // Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -64,9 +64,9 @@
 
 %{
 #include <sstream>
-#include "bdd.h"
-#include "fdd.h"
-#include "bvec.h"
+#include "bddx.h"
+#include "fddx.h"
+#include "bvecx.h"
 %}
 
 %typemap(in) (int* input_buf, int input_buf_size) {