4 files changed, 45 insertions, 2 deletions
diff --git a/src/bdd/cudd/cudd.h b/src/bdd/cudd/cudd.h
index 14f67abf..658e4eaf 100644
--- a/src/bdd/cudd/cudd.h
+++ b/src/bdd/cudd/cudd.h
@@ -720,6 +720,7 @@ EXTERN DdNode * Cudd_addRoundOff ARGS((DdManager *dd, DdNode *f, int N));
 EXTERN DdNode * Cudd_addWalsh ARGS((DdManager *dd, DdNode **x, DdNode **y, int n));
 EXTERN DdNode * Cudd_addResidue ARGS((DdManager *dd, int n, int m, int options, int top));
 EXTERN DdNode * Cudd_bddAndAbstract ARGS((DdManager *manager, DdNode *f, DdNode *g, DdNode *cube));
+EXTERN DdNode * Cudd_bddAndAbstractLimit ARGS((DdManager *manager, DdNode *f, DdNode *g, DdNode *cube, unsigned int limit));
 EXTERN int Cudd_ApaNumberOfDigits ARGS((int binaryDigits));
 EXTERN DdApaNumber Cudd_NewApaNumber ARGS((int digits));
 EXTERN void Cudd_ApaCopy ARGS((int digits, DdApaNumber source, DdApaNumber dest));
diff --git a/src/bdd/cudd/cuddAndAbs.c b/src/bdd/cudd/cuddAndAbs.c
index 9ee70498..cd928e80 100644
--- a/src/bdd/cudd/cuddAndAbs.c
+++ b/src/bdd/cudd/cuddAndAbs.c
@@ -109,6 +109,46 @@ Cudd_bddAndAbstract(
 } /* end of Cudd_bddAndAbstract */
 
 
+/**Function********************************************************************
+
+  Synopsis [Takes the AND of two BDDs and simultaneously abstracts the
+  variables in cube.  Returns NULL if too many nodes are required.]
+
+  Description [Takes the AND of two BDDs and simultaneously abstracts
+  the variables in cube. The variables are existentially abstracted.
+  Returns a pointer to the result is successful; NULL otherwise.
+  In particular, if the number of new nodes created exceeds
+  <code>limit</code>, this function returns NULL.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_bddAndAbstract]
+
+******************************************************************************/
+DdNode *
+Cudd_bddAndAbstractLimit(
+  DdManager * manager,
+  DdNode * f,
+  DdNode * g,
+  DdNode * cube,
+  unsigned int limit)
+{
+    DdNode *res;
+    unsigned int saveLimit = manager->maxLive;
+
+    manager->maxLive = (manager->keys - manager->dead) +
+      (manager->keysZ - manager->deadZ) + limit;
+    do {
+        manager->reordered = 0;
+        res = cuddBddAndAbstractRecur(manager, f, g, cube);
+    } while (manager->reordered == 1);
+    manager->maxLive = saveLimit;
+    return(res);
+
+} /* end of Cudd_bddAndAbstractLimit */
+
+
+
 /*---------------------------------------------------------------------------*/
 /* Definition of internal functions                                          */
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddInit.c b/src/bdd/cudd/cuddInit.c
index 43b2ac29..6be35970 100644
--- a/src/bdd/cudd/cuddInit.c
+++ b/src/bdd/cudd/cuddInit.c
@@ -174,7 +174,8 @@ Cudd_Init(
 
     unique->memused += sizeof(DdNode *) * unique->maxSize;
 
-    unique->bReached = NULL;
+    unique->bFunc = NULL;
+    unique->bFunc2 = NULL;
     return(unique);
 
 } /* end of Cudd_Init */
diff --git a/src/bdd/cudd/cuddInt.h b/src/bdd/cudd/cuddInt.h
index 84146132..f5becf84 100644
--- a/src/bdd/cudd/cuddInt.h
+++ b/src/bdd/cudd/cuddInt.h
@@ -439,7 +439,8 @@ struct DdManager {    /* specialized DD symbol table */
     int nvars;            /* variables used so far */
     int threshold;        /* for pseudo var threshold value*/
 #endif
-    DdNode * bReached;
+    DdNode * bFunc;
+    DdNode * bFunc2;
 };
 
 typedef struct Move {