diff --git a/buddy/ChangeLog b/buddy/ChangeLog
index 33a7c1f27..d04abef48 100644
--- a/buddy/ChangeLog
+++ b/buddy/ChangeLog
@@ -1,5 +1,13 @@
 2003-05-22  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
+	* src/pairs.c (bdd_mergepairs): New function.
+	(bdd_copypair): Revert 2003-05-20's change.  Use bdd_addref
+	to copy result variables.
+
+	* src/bdd.h (BDD_INVMERGE): New error code.
+	(bdd_mergepairs): Declare.
+	* src/kernel.c (errorstrings): Add string of BDDINV.
+
 	* src/bddop.c (bdd_simplify): Typo in doc, s/domaine/domain/.
 
 2003-05-20  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
diff --git a/buddy/src/bdd.h b/buddy/src/bdd.h
index 804516700..434173905 100644
--- a/buddy/src/bdd.h
+++ b/buddy/src/bdd.h
@@ -28,7 +28,7 @@
 ========================================================================*/
 
 /*************************************************************************
-  $Header: /Volumes/CVS/repository/spot/spot/buddy/src/bdd.h,v 1.3 2003/05/19 15:58:44 aduret Exp $
+  $Header: /Volumes/CVS/repository/spot/spot/buddy/src/bdd.h,v 1.4 2003/05/22 15:07:27 aduret Exp $
   FILE:  bdd.h
   DESCR: C,C++ User interface for the BDD package
   AUTH:  Jorn Lind
@@ -264,6 +264,7 @@ extern void     bdd_gbc(void);
 extern int      bdd_scanset(BDD, int**, int*);
 extern BDD      bdd_makeset(int *, int);
 extern bddPair* bdd_copypair(bddPair*);
+extern bddPair* bdd_mergepairs(bddPair*, bddPair*);
 extern bddPair* bdd_newpair(void);
 extern int      bdd_setpair(bddPair*, int, int);
 extern int      bdd_setpairs(bddPair*, int*, int*, int);
@@ -410,7 +411,9 @@ extern const BDD bddtrue;
 #define BVEC_SHIFT (-21)   /* Illegal shift-left/right parameter */
 #define BVEC_DIVZERO (-22) /* Division by zero */
 
-#define BDD_ERRNUM 24
+#define BDD_INVMERGE (-23) /* Merging clashing rewriting rules */
+
+#define BDD_ERRNUM 25
 
 /*************************************************************************
    If this file is included from a C++ compiler then the following
diff --git a/buddy/src/kernel.c b/buddy/src/kernel.c
index cfa696142..8f8569f0e 100644
--- a/buddy/src/kernel.c
+++ b/buddy/src/kernel.c
@@ -28,7 +28,7 @@
 ========================================================================*/
 
 /*************************************************************************
-  $Header: /Volumes/CVS/repository/spot/spot/buddy/src/kernel.c,v 1.4 2003/05/20 08:22:36 aduret Exp $
+  $Header: /Volumes/CVS/repository/spot/spot/buddy/src/kernel.c,v 1.5 2003/05/22 15:07:27 aduret Exp $
   FILE:  kernel.c
   DESCR: implements the bdd kernel functions.
   AUTH:  Jorn Lind
@@ -133,7 +133,8 @@ static char *errorstrings[BDD_ERRNUM] =
   "Bad size argument",
   "Mismatch in bitvector size",
   "Illegal shift-left/right parameter",
-  "Division by zero" };
+  "Division by zero",
+  "Unmergeable rewritings."};
 
 
 /*=== OTHER INTERNAL DEFINITIONS =======================================*/
diff --git a/buddy/src/pairs.c b/buddy/src/pairs.c
index 7265fd924..20d98f78a 100644
--- a/buddy/src/pairs.c
+++ b/buddy/src/pairs.c
@@ -28,7 +28,7 @@
 ========================================================================*/
 
 /*************************************************************************
-  $Header: /Volumes/CVS/repository/spot/spot/buddy/src/pairs.c,v 1.6 2003/05/22 12:07:52 aduret Exp $
+  $Header: /Volumes/CVS/repository/spot/spot/buddy/src/pairs.c,v 1.7 2003/05/22 15:07:27 aduret Exp $
   FILE:  pairs.c
   DESCR: Pair management for BDD package.
   AUTH:  Jorn Lind
@@ -203,7 +203,8 @@ bddPair *bdd_copypair(bddPair *from)
    if (p == NULL)
      return NULL;
 
-   memcpy(p->result, from->result, bddvarnum * sizeof(*p->result));
+   for (n=0 ; n<bddvarnum ; n++)
+     p->result[n] = bdd_addref(from->result[n]);
 
    p->id = update_pairsid();
    p->last = from->last;
@@ -212,6 +213,59 @@ bddPair *bdd_copypair(bddPair *from)
    return p;
 }
 
+/*
+NAME    {* bdd\_mergepairs *}
+SECTION {* kernel *}
+SHORT   {* merge two pair tables *}
+PROTO   {* bddPair *bdd_mergepairs(bddPair *left, bddPairs *right) *}
+DESCR   {* Create a table of pairs that can be used to perform the
+	   rewritings of both {\tt left} and {\tt right}.  This cannot work if
+	   the two tables contain incompatible rewrite pairs (for instance
+	   if left rewrite 1 to 2, and right rewrite 1 to 3).
+
+	   This function allocates a new table. The
+	   table can be freed by a call to {\tt bdd\_freepair}. *}
+RETURN  {* Returns a new table of pairs. *}
+ALSO    {* bdd\_newpair, bdd\_freepair, bdd\_replace, bdd\_setpair, bdd\_setpairs *}
+*/
+bddPair *bdd_mergepairs(bddPair *left, bddPair *right)
+{
+   int n;
+   bddPair *p;
+
+   p = bdd_copypair(left);
+   if (p == NULL)
+     return NULL;
+
+   for (n=0; n<bddvarnum; n++)
+     {
+       bdd nl = bdd_ithvar(n);
+
+       /* If P performs no rewriting for N, blindly use that of RIGHT.  */
+       if (nl == p->result[n])
+	 {
+	   bdd_delref(p->result[n]);
+	   p->result[n] = bdd_addref(right->result[n]);
+	 }
+       else
+	 /* If P rewrites N, make sure RIGHT doesn't rewrite it, or that
+	    it rewrites it to the same variable.  */
+	 if (nl != right->result[n] && right->result[n] != p->result[n])
+	   {
+	     bdd_freepair(p);
+	     bdd_error(BDD_INVMERGE);
+	     return NULL;
+	   }
+     }
+
+   if (p->last < right->last)
+     p->last = right->last;
+
+   /* We don't have to update the ID, because this pair was not
+      used since bdd_copypair were called. */
+   return p;
+}
+
 
 /*
 NAME    {* bdd\_setpair *}