Upgrade to the latest CUDD 2.4.2.

1 files changed, 757 insertions, 723 deletions

diff --git a/src/bdd/cudd/cuddSubsetSP.c b/src/bdd/cudd/cuddSubsetSP.c
index d336187b..cddc58ed 100644
--- a/src/bdd/cudd/cuddSubsetSP.c
+++ b/src/bdd/cudd/cuddSubsetSP.c
@@ -9,35 +9,62 @@
 
 
   Description  [External procedures included in this module:
-        <ul>
-        <li> Cudd_SubsetShortPaths()
-        <li> Cudd_SupersetShortPaths()
-        </ul>
-        Internal procedures included in this module:
-        <ul>
-        <li> cuddSubsetShortPaths()
-        </ul> 
-        Static procedures included in this module:
-        <ul>
-        <li> BuildSubsetBdd()
-        <li> CreatePathTable()
-        <li> AssessPathLength()
-        <li> CreateTopDist()
-        <li> CreateBotDist()
-        <li> ResizeNodeDistPages()
-        <li> ResizeQueuePages()
-        <li> stPathTableDdFree()
-        </ul>
-        ]
+                <ul>
+                <li> Cudd_SubsetShortPaths()
+                <li> Cudd_SupersetShortPaths()
+                </ul>
+                Internal procedures included in this module:
+                <ul>
+                <li> cuddSubsetShortPaths()
+                </ul>
+                Static procedures included in this module:
+                <ul>
+                <li> BuildSubsetBdd()
+                <li> CreatePathTable()
+                <li> AssessPathLength()
+                <li> CreateTopDist()
+                <li> CreateBotDist()
+                <li> ResizeNodeDistPages()
+                <li> ResizeQueuePages()
+                <li> stPathTableDdFree()
+                </ul>
+                ]
 
   SeeAlso     [cuddSubsetHB.c]
 
   Author      [Kavita Ravi]
 
-  Copyright   [This file was created at the University of Colorado at
-  Boulder.  The University of Colorado at Boulder makes no warranty
-  about the suitability of this software for any purpose.  It is
-  presented on an AS IS basis.]
+  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
+
+  All rights reserved.
+
+  Redistribution and use in source and binary forms, with or without
+  modification, are permitted provided that the following conditions
+  are met:
+
+  Redistributions of source code must retain the above copyright
+  notice, this list of conditions and the following disclaimer.
+
+  Redistributions in binary form must reproduce the above copyright
+  notice, this list of conditions and the following disclaimer in the
+  documentation and/or other materials provided with the distribution.
+
+  Neither the name of the University of Colorado nor the names of its
+  contributors may be used to endorse or promote products derived from
+  this software without specific prior written permission.
+
+  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
+  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
+  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
+  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
+  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
+  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+  POSSIBILITY OF SUCH DAMAGE.]
 
 ******************************************************************************/
 
@@ -47,25 +74,26 @@
 ABC_NAMESPACE_IMPL_START
 
 
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
 
 #define DEFAULT_PAGE_SIZE 2048 /* page size to store the BFS queue element type */
 #define DEFAULT_NODE_DIST_PAGE_SIZE 2048 /*  page sizesto store NodeDist_t type */
-#define MAXSHORTINT        ((DdHalfWord) ~0) /* constant defined to store
-                       * maximum distance of a node
-                       * from the root or the
-                       * constant
-                       */
+#define MAXSHORTINT     ((DdHalfWord) ~0) /* constant defined to store
+                                           * maximum distance of a node
+                                           * from the root or the
+                                           * constant
+                                           */
 #define INITIAL_PAGES 128 /* number of initial pages for the
-               * queue/NodeDist_t type */
+                           * queue/NodeDist_t type */
 
 /*---------------------------------------------------------------------------*/
 /* Stucture declarations                                                     */
 /*---------------------------------------------------------------------------*/
 
-/* structure created to store subset results for each node and distances with 
+/* structure created to store subset results for each node and distances with
  * odd and even parity of the node from the root and sink. Main data structure
  * in this procedure.
  */
@@ -98,7 +126,7 @@ typedef struct NodeDist NodeDist_t;
 /*---------------------------------------------------------------------------*/
 
 #ifndef lint
-static char rcsid[] DD_UNUSED = "$Id: cuddSubsetSP.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $";
+static char rcsid[] DD_UNUSED = "$Id: cuddSubsetSP.c,v 1.34 2009/02/19 16:23:19 fabio Exp $";
 #endif
 
 #ifdef DD_DEBUG
@@ -108,21 +136,21 @@ static int thishit;
 #endif
 
 
-static     int         memOut; /* flag to indicate out of memory */
+static  int             memOut; /* flag to indicate out of memory */
 static  DdNode          *zero, *one; /* constant functions */
 
 static  NodeDist_t      **nodeDistPages; /* pointers to the pages */
-static    int        nodeDistPageIndex; /* index to next element */
-static    int        nodeDistPage; /* index to current page */
-static    int        nodeDistPageSize = DEFAULT_NODE_DIST_PAGE_SIZE; /* page size */
-static    int        maxNodeDistPages; /* number of page pointers */
+static  int             nodeDistPageIndex; /* index to next element */
+static  int             nodeDistPage; /* index to current page */
+static  int             nodeDistPageSize = DEFAULT_NODE_DIST_PAGE_SIZE; /* page size */
+static  int             maxNodeDistPages; /* number of page pointers */
 static  NodeDist_t      *currentNodeDistPage; /* current page */
 
 static  DdNode          ***queuePages; /* pointers to the pages */
-static    int        queuePageIndex;    /* index to next element */
-static    int        queuePage; /* index to current page */
-static    int        queuePageSize = DEFAULT_PAGE_SIZE; /* page size */
-static    int        maxQueuePages; /* number of page pointers */
+static  int             queuePageIndex; /* index to next element */
+static  int             queuePage; /* index to current page */
+static  int             queuePageSize = DEFAULT_PAGE_SIZE; /* page size */
+static  int             maxQueuePages; /* number of page pointers */
 static  DdNode          **currentQueuePage; /* current page */
 
 
@@ -130,23 +158,30 @@ static  DdNode          **currentQueuePage; /* current page */
 /* Macro declarations                                                        */
 /*---------------------------------------------------------------------------*/
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 /**AutomaticStart*************************************************************/
 
 /*---------------------------------------------------------------------------*/
 /* Static function prototypes                                                */
 /*---------------------------------------------------------------------------*/
 
-static void ResizeNodeDistPages ARGS(());
-static void ResizeQueuePages ARGS(());
-static void CreateTopDist ARGS((st_table *pathTable, int parentPage, int parentQueueIndex, int topLen, DdNode **childPage, int childQueueIndex, int numParents, FILE *fp));
-static int CreateBotDist ARGS((DdNode *node, st_table *pathTable, unsigned int *pathLengthArray, FILE *fp));
-static st_table * CreatePathTable ARGS((DdNode *node, unsigned int *pathLengthArray, FILE *fp));
-static unsigned int AssessPathLength ARGS((unsigned int *pathLengthArray, int threshold, int numVars, unsigned int *excess, FILE *fp));
-static DdNode * BuildSubsetBdd ARGS((DdManager *dd, st_table *pathTable, DdNode *node, struct AssortedInfo *info, st_table *subsetNodeTable));
-static enum st_retval stPathTableDdFree ARGS((char *key, char *value, char *arg));
+static void ResizeNodeDistPages (void);
+static void ResizeQueuePages (void);
+static void CreateTopDist (st_table *pathTable, int parentPage, int parentQueueIndex, int topLen, DdNode **childPage, int childQueueIndex, int numParents, FILE *fp);
+static int CreateBotDist (DdNode *node, st_table *pathTable, unsigned int *pathLengthArray, FILE *fp);
+static st_table * CreatePathTable (DdNode *node, unsigned int *pathLengthArray, FILE *fp);
+static unsigned int AssessPathLength (unsigned int *pathLengthArray, int threshold, int numVars, unsigned int *excess, FILE *fp);
+static DdNode * BuildSubsetBdd (DdManager *dd, st_table *pathTable, DdNode *node, struct AssortedInfo *info, st_table *subsetNodeTable);
+static enum st_retval stPathTableDdFree (char *key, char *value, char *arg);
 
 /**AutomaticEnd***************************************************************/
 
+#ifdef __cplusplus
+}
+#endif
 
 /*---------------------------------------------------------------------------*/
 /* Definition of Exported functions                                          */
@@ -193,8 +228,8 @@ Cudd_SubsetShortPaths(
 
     memOut = 0;
     do {
-    dd->reordered = 0;
-    subset = cuddSubsetShortPaths(dd, f, numVars, threshold, hardlimit);
+        dd->reordered = 0;
+        subset = cuddSubsetShortPaths(dd, f, numVars, threshold, hardlimit);
     } while((dd->reordered ==1) && (!memOut));
 
     return(subset);
@@ -246,8 +281,8 @@ Cudd_SupersetShortPaths(
     g = Cudd_Not(f);
     memOut = 0;
     do {
-    dd->reordered = 0;
-    subset = cuddSubsetShortPaths(dd, g, numVars, threshold, hardlimit);
+        dd->reordered = 0;
+        subset = cuddSubsetShortPaths(dd, g, numVars, threshold, hardlimit);
     } while((dd->reordered ==1) && (!memOut));
 
     return(Cudd_NotCond(subset, (subset != NULL)));
@@ -291,7 +326,7 @@ cuddSubsetShortPaths(
     unsigned int  *pathLengthArray;
     unsigned int maxpath, oddLen, evenLen, pathLength, *excess;
     int i;
-    NodeDist_t     *nodeStat;
+    NodeDist_t  *nodeStat;
     struct AssortedInfo *info;
     st_table *subsetNodeTable;
 
@@ -302,17 +337,17 @@ cuddSubsetShortPaths(
       /* set default value */
       numVars = Cudd_ReadSize(dd);
     }
-    
+
     if (threshold > numVars) {
-    threshold = threshold - numVars;
+        threshold = threshold - numVars;
     }
     if (f == NULL) {
-    fprintf(dd->err, "Cannot partition, nil object\n");
-    dd->errorCode = CUDD_INVALID_ARG;
-    return(NULL);
+        fprintf(dd->err, "Cannot partition, nil object\n");
+        dd->errorCode = CUDD_INVALID_ARG;
+        return(NULL);
     }
     if (Cudd_IsConstant(f))
-    return (f);
+        return (f);
 
     pathLengthArray = ABC_ALLOC(unsigned int, numVars+1);
     for (i = 0; i < numVars+1; i++) pathLengthArray[i] = 0;
@@ -325,101 +360,103 @@ cuddSubsetShortPaths(
     pathTable = CreatePathTable(f, pathLengthArray, dd->err);
 
     if ((pathTable == NULL) || (memOut)) {
-    if (pathTable != NULL)
-        st_free_table(pathTable);
-    ABC_FREE(pathLengthArray);
-    return (NIL(DdNode));
+        if (pathTable != NULL)
+            st_free_table(pathTable);
+        ABC_FREE(pathLengthArray);
+        return (NIL(DdNode));
     }
 
     excess = ABC_ALLOC(unsigned int, 1);
     *excess = 0;
     maxpath = AssessPathLength(pathLengthArray, threshold, numVars, excess,
-                   dd->err);
+                               dd->err);
 
     if (maxpath != (unsigned) (numVars + 1)) {
 
-    info = ABC_ALLOC(struct AssortedInfo, 1);
-    info->maxpath = maxpath;
-    info->findShortestPath = 0;
-    info->thresholdReached = *excess;
-    info->maxpathTable = st_init_table(st_ptrcmp, st_ptrhash);
-    info->threshold = threshold;
+        info = ABC_ALLOC(struct AssortedInfo, 1);
+        info->maxpath = maxpath;
+        info->findShortestPath = 0;
+        info->thresholdReached = *excess;
+        info->maxpathTable = st_init_table(st_ptrcmp, st_ptrhash);
+        info->threshold = threshold;
 
 #ifdef DD_DEBUG
-    (void) fprintf(dd->out, "Path length array\n");
-    for (i = 0; i < (numVars+1); i++) {
-        if (pathLengthArray[i])
-        (void) fprintf(dd->out, "%d ",i);
-    }
-    (void) fprintf(dd->out, "\n");
-    for (i = 0; i < (numVars+1); i++) {
-        if (pathLengthArray[i])
-        (void) fprintf(dd->out, "%d ",pathLengthArray[i]);
-    }
-    (void) fprintf(dd->out, "\n");
-    (void) fprintf(dd->out, "Maxpath  = %d, Thresholdreached = %d\n",
-               maxpath, info->thresholdReached);
+        (void) fprintf(dd->out, "Path length array\n");
+        for (i = 0; i < (numVars+1); i++) {
+            if (pathLengthArray[i])
+                (void) fprintf(dd->out, "%d ",i);
+        }
+        (void) fprintf(dd->out, "\n");
+        for (i = 0; i < (numVars+1); i++) {
+            if (pathLengthArray[i])
+                (void) fprintf(dd->out, "%d ",pathLengthArray[i]);
+        }
+        (void) fprintf(dd->out, "\n");
+        (void) fprintf(dd->out, "Maxpath  = %d, Thresholdreached = %d\n",
+                       maxpath, info->thresholdReached);
 #endif
 
-    N = Cudd_Regular(f);
-    if (!st_lookup(pathTable, (char *)N, (char **)&nodeStat)) {
-        fprintf(dd->err, "Something wrong, root node must be in table\n");
-        dd->errorCode = CUDD_INTERNAL_ERROR;
-        return(NULL);
-    } else {
-        if ((nodeStat->oddTopDist != MAXSHORTINT) &&
-        (nodeStat->oddBotDist != MAXSHORTINT))
-        oddLen = (nodeStat->oddTopDist + nodeStat->oddBotDist);
-        else
-        oddLen = MAXSHORTINT;
-
-        if ((nodeStat->evenTopDist != MAXSHORTINT) &&
-        (nodeStat->evenBotDist != MAXSHORTINT))
-        evenLen = (nodeStat->evenTopDist +nodeStat->evenBotDist);
-        else
-        evenLen = MAXSHORTINT;
-
-        pathLength = (oddLen <= evenLen) ? oddLen : evenLen;
-        if (pathLength > maxpath) {
-        (void) fprintf(dd->err, "All computations are bogus, since root has path length greater than max path length within threshold %d, %d\n", maxpath, pathLength);
-        dd->errorCode = CUDD_INTERNAL_ERROR;
-        return(NULL);
+        N = Cudd_Regular(f);
+        if (!st_lookup(pathTable, (const char *)N, (char **)&nodeStat)) {
+            fprintf(dd->err, "Something wrong, root node must be in table\n");
+            dd->errorCode = CUDD_INTERNAL_ERROR;
+            ABC_FREE(excess);
+            ABC_FREE(info);
+            return(NULL);
+        } else {
+            if ((nodeStat->oddTopDist != MAXSHORTINT) &&
+                (nodeStat->oddBotDist != MAXSHORTINT))
+                oddLen = (nodeStat->oddTopDist + nodeStat->oddBotDist);
+            else
+                oddLen = MAXSHORTINT;
+
+            if ((nodeStat->evenTopDist != MAXSHORTINT) &&
+                (nodeStat->evenBotDist != MAXSHORTINT))
+                evenLen = (nodeStat->evenTopDist +nodeStat->evenBotDist);
+            else
+                evenLen = MAXSHORTINT;
+
+            pathLength = (oddLen <= evenLen) ? oddLen : evenLen;
+            if (pathLength > maxpath) {
+                (void) fprintf(dd->err, "All computations are bogus, since root has path length greater than max path length within threshold %u, %u\n", maxpath, pathLength);
+                dd->errorCode = CUDD_INTERNAL_ERROR;
+                return(NULL);
+            }
         }
-    }
 
 #ifdef DD_DEBUG
-    numCalls = 0;
-    hits = 0;
-    thishit = 0;
+        numCalls = 0;
+        hits = 0;
+        thishit = 0;
 #endif
-    /* initialize a table to store computed nodes */
-    if (hardlimit) {
-        subsetNodeTable = st_init_table(st_ptrcmp, st_ptrhash);
-    } else {
-        subsetNodeTable = NIL(st_table);
-    }
-    subset = BuildSubsetBdd(dd, pathTable, f, info, subsetNodeTable);
-    if (subset != NULL) {
-        cuddRef(subset);
-    }
-    /* record the number of times a computed result for a node is hit */
+        /* initialize a table to store computed nodes */
+        if (hardlimit) {
+            subsetNodeTable = st_init_table(st_ptrcmp, st_ptrhash);
+        } else {
+            subsetNodeTable = NIL(st_table);
+        }
+        subset = BuildSubsetBdd(dd, pathTable, f, info, subsetNodeTable);
+        if (subset != NULL) {
+            cuddRef(subset);
+        }
+        /* record the number of times a computed result for a node is hit */
 
 #ifdef DD_DEBUG
-    (void) fprintf(dd->out, "Hits = %d, New==Node = %d, NumCalls = %d\n",
-        hits, thishit, numCalls);
+        (void) fprintf(dd->out, "Hits = %d, New==Node = %d, NumCalls = %d\n",
+                hits, thishit, numCalls);
 #endif
 
-    if (subsetNodeTable != NIL(st_table)) {
-        st_free_table(subsetNodeTable);
-    }
-    st_free_table(info->maxpathTable);
-    st_foreach(pathTable, (ST_PFSR)stPathTableDdFree, (char *)dd);
+        if (subsetNodeTable != NIL(st_table)) {
+            st_free_table(subsetNodeTable);
+        }
+        st_free_table(info->maxpathTable);
+        st_foreach(pathTable, stPathTableDdFree, (char *)dd);
 
-    ABC_FREE(info);
+        ABC_FREE(info);
 
     } else {/* if threshold larger than size of dd */
-    subset = f;
-    cuddRef(subset);
+        subset = f;
+        cuddRef(subset);
     }
     ABC_FREE(excess);
     st_free_table(pathTable);
@@ -430,21 +467,21 @@ cuddSubsetShortPaths(
 #ifdef DD_DEBUG
     /* check containment of subset in f */
     if (subset != NULL) {
-    DdNode *check;
-    check = Cudd_bddIteConstant(dd, subset, f, one);
-    if (check != one) {
-        (void) fprintf(dd->err, "Wrong partition\n");
-        dd->errorCode = CUDD_INTERNAL_ERROR;
-        return(NULL);
-    }
+        DdNode *check;
+        check = Cudd_bddIteConstant(dd, subset, f, one);
+        if (check != one) {
+            (void) fprintf(dd->err, "Wrong partition\n");
+            dd->errorCode = CUDD_INTERNAL_ERROR;
+            return(NULL);
+        }
     }
 #endif
 
     if (subset != NULL) {
-    cuddDeref(subset);
-    return(subset);
+        cuddDeref(subset);
+        return(subset);
     } else {
-    return(NULL);
+        return(NULL);
     }
 
 } /* end of cuddSubsetShortPaths */
@@ -465,15 +502,14 @@ cuddSubsetShortPaths(
   next page when the end of the page is reached and allocates new
   pages when necessary. ]
 
-  SideEffects [Changes the size of  pages, page, page index, maximum 
+  SideEffects [Changes the size of  pages, page, page index, maximum
   number of pages freeing stuff in case of memory out. ]
 
   SeeAlso     []
 
 ******************************************************************************/
 static void
-ResizeNodeDistPages(
-   )
+ResizeNodeDistPages(void)
 {
     int i;
     NodeDist_t **newNodeDistPages;
@@ -482,34 +518,34 @@ ResizeNodeDistPages(
     nodeDistPage++;
 
     /* If the current page index is larger than the number of pages
-     * allocated, allocate a new page array. Page numbers are incremented by 
+     * allocated, allocate a new page array. Page numbers are incremented by
      * INITIAL_PAGES
      */
     if (nodeDistPage == maxNodeDistPages) {
-    newNodeDistPages = ABC_ALLOC(NodeDist_t *,maxNodeDistPages + INITIAL_PAGES);
-    if (newNodeDistPages == NULL) {
-        for (i = 0; i < nodeDistPage; i++) ABC_FREE(nodeDistPages[i]);
-        ABC_FREE(nodeDistPages);
-        memOut = 1;
-        return;
-    } else {
-        for (i = 0; i < maxNodeDistPages; i++) {
-        newNodeDistPages[i] = nodeDistPages[i];
+        newNodeDistPages = ABC_ALLOC(NodeDist_t *,maxNodeDistPages + INITIAL_PAGES);
+        if (newNodeDistPages == NULL) {
+            for (i = 0; i < nodeDistPage; i++) ABC_FREE(nodeDistPages[i]);
+            ABC_FREE(nodeDistPages);
+            memOut = 1;
+            return;
+        } else {
+            for (i = 0; i < maxNodeDistPages; i++) {
+                newNodeDistPages[i] = nodeDistPages[i];
+            }
+            /* Increase total page count */
+            maxNodeDistPages += INITIAL_PAGES;
+            ABC_FREE(nodeDistPages);
+            nodeDistPages = newNodeDistPages;
         }
-        /* Increase total page count */
-        maxNodeDistPages += INITIAL_PAGES;
-        ABC_FREE(nodeDistPages);
-        nodeDistPages = newNodeDistPages;
-    }
     }
     /* Allocate a new page */
     currentNodeDistPage = nodeDistPages[nodeDistPage] = ABC_ALLOC(NodeDist_t,
-                                  nodeDistPageSize);
+                                                              nodeDistPageSize);
     if (currentNodeDistPage == NULL) {
-    for (i = 0; i < nodeDistPage; i++) ABC_FREE(nodeDistPages[i]);
-    ABC_FREE(nodeDistPages);
-    memOut = 1;
-    return;
+        for (i = 0; i < nodeDistPage; i++) ABC_FREE(nodeDistPages[i]);
+        ABC_FREE(nodeDistPages);
+        memOut = 1;
+        return;
     }
     /* reset page index */
     nodeDistPageIndex = 0;
@@ -520,56 +556,55 @@ ResizeNodeDistPages(
 
 /**Function********************************************************************
 
-  Synopsis    [Resize the number of pages allocated to store nodes in the BFS 
+  Synopsis    [Resize the number of pages allocated to store nodes in the BFS
   traversal of the Bdd  .]
 
-  Description [Resize the number of pages allocated to store nodes in the BFS 
+  Description [Resize the number of pages allocated to store nodes in the BFS
   traversal of the Bdd. The procedure  moves the counter to the
   next page when the end of the page is reached and allocates new
   pages when necessary.]
 
-  SideEffects [Changes the size of pages, page, page index, maximum 
+  SideEffects [Changes the size of pages, page, page index, maximum
   number of pages freeing stuff in case of memory out. ]
 
   SeeAlso     []
 
 ******************************************************************************/
 static void
-ResizeQueuePages(
-   )
+ResizeQueuePages(void)
 {
     int i;
     DdNode ***newQueuePages;
 
     queuePage++;
     /* If the current page index is larger than the number of pages
-     * allocated, allocate a new page array. Page numbers are incremented by 
+     * allocated, allocate a new page array. Page numbers are incremented by
      * INITIAL_PAGES
      */
     if (queuePage == maxQueuePages) {
-    newQueuePages = ABC_ALLOC(DdNode **,maxQueuePages + INITIAL_PAGES);
-    if (newQueuePages == NULL) {
-        for (i = 0; i < queuePage; i++) ABC_FREE(queuePages[i]);
-        ABC_FREE(queuePages);
-        memOut = 1;
-        return;
-    } else {
-        for (i = 0; i < maxQueuePages; i++) {
-        newQueuePages[i] = queuePages[i];
+        newQueuePages = ABC_ALLOC(DdNode **,maxQueuePages + INITIAL_PAGES);
+        if (newQueuePages == NULL) {
+            for (i = 0; i < queuePage; i++) ABC_FREE(queuePages[i]);
+            ABC_FREE(queuePages);
+            memOut = 1;
+            return;
+        } else {
+            for (i = 0; i < maxQueuePages; i++) {
+                newQueuePages[i] = queuePages[i];
+            }
+            /* Increase total page count */
+            maxQueuePages += INITIAL_PAGES;
+            ABC_FREE(queuePages);
+            queuePages = newQueuePages;
         }
-        /* Increase total page count */
-        maxQueuePages += INITIAL_PAGES;
-        ABC_FREE(queuePages);
-        queuePages = newQueuePages;
-    }
     }
     /* Allocate a new page */
     currentQueuePage = queuePages[queuePage] = ABC_ALLOC(DdNode *,queuePageSize);
     if (currentQueuePage == NULL) {
-    for (i = 0; i < queuePage; i++) ABC_FREE(queuePages[i]);
-    ABC_FREE(queuePages);
-    memOut = 1;
-    return;
+        for (i = 0; i < queuePage; i++) ABC_FREE(queuePages[i]);
+        ABC_FREE(queuePages);
+        memOut = 1;
+        return;
     }
     /* reset page index */
     queuePageIndex = 0;
@@ -619,145 +654,145 @@ CreateTopDist(
     /* set queue index to the next available entry for addition */
     /* set queue page to page of addition */
     if ((queuePages[parentPage] == childPage) && (parentQueueIndex ==
-                          childQueueIndex)) {
-    fprintf(fp, "Should not happen that they are equal\n");
+                                                  childQueueIndex)) {
+        fprintf(fp, "Should not happen that they are equal\n");
     }
     assert(queuePageIndex == childQueueIndex);
     assert(currentQueuePage == childPage);
 #endif
     /* number children added to queue is initialized , needed for
-     * numParents in the next call 
+     * numParents in the next call
      */
     childrenCount = 0;
     /* process all the nodes in this level */
     while (numParents) {
-    numParents--;
-    if (parentQueueIndex == queuePageSize) {
-        parentPage++;
-        parentQueueIndex = 0;
-    }
-    /* a parent to process */
-    node = *(queuePages[parentPage] + parentQueueIndex);
-    parentQueueIndex++;
-    /* get its children */
-    N = Cudd_Regular(node);
-    Nv = Cudd_T(N);
-    Nnv = Cudd_E(N);
-
-    Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
-    Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
-
-    processingDone = 2;
-    while (processingDone) {
-        /* processing the THEN and the ELSE children, the THEN
-         * child first
-         */
-        if (processingDone == 2) {
-        child = Nv;
-        } else {
-        child = Nnv;
+        numParents--;
+        if (parentQueueIndex == queuePageSize) {
+            parentPage++;
+            parentQueueIndex = 0;
         }
-
-        regChild = Cudd_Regular(child);
-        /* dont process if the child is a constant */
-        if (!Cudd_IsConstant(child)) {
-        /* check is already visited, if not add a new entry in
-         * the path Table
-         */
-        if (!st_lookup(pathTable, (char *)regChild, (char **)&nodeStat)) {
-            /* if not in table, has never been visited */
-            /* create entry for table */
-            if (nodeDistPageIndex == nodeDistPageSize)
-            ResizeNodeDistPages();
-            if (memOut) {
-            for (i = 0; i <= queuePage; i++) ABC_FREE(queuePages[i]);
-            ABC_FREE(queuePages);
-            st_free_table(pathTable);
-            return;
-            }
-            /* New entry for child in path Table is created here */
-            nodeStat = currentNodeDistPage + nodeDistPageIndex;
-            nodeDistPageIndex++;
-
-            /* Initialize fields of the node data */
-            nodeStat->oddTopDist = MAXSHORTINT;
-            nodeStat->evenTopDist = MAXSHORTINT;
-            nodeStat->evenBotDist = MAXSHORTINT;
-            nodeStat->oddBotDist = MAXSHORTINT;
-            nodeStat->regResult = NULL;
-            nodeStat->compResult = NULL;
-            /* update the table entry element, the distance keeps
-             * track of the parity of the path from the root
+        /* a parent to process */
+        node = *(queuePages[parentPage] + parentQueueIndex);
+        parentQueueIndex++;
+        /* get its children */
+        N = Cudd_Regular(node);
+        Nv = Cudd_T(N);
+        Nnv = Cudd_E(N);
+
+        Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
+        Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
+
+        processingDone = 2;
+        while (processingDone) {
+            /* processing the THEN and the ELSE children, the THEN
+             * child first
              */
-            if (Cudd_IsComplement(child)) {
-            nodeStat->oddTopDist = (DdHalfWord) topLen + 1;
+            if (processingDone == 2) {
+                child = Nv;
             } else {
-            nodeStat->evenTopDist = (DdHalfWord) topLen + 1;
+                child = Nnv;
             }
 
-            /* insert entry element for  child in the table */
-            if (st_insert(pathTable, (char *)regChild,
-                  (char *)nodeStat) == ST_OUT_OF_MEM) {
-            memOut = 1;
-            for (i = 0; i <= nodeDistPage; i++)
-                ABC_FREE(nodeDistPages[i]);
-            ABC_FREE(nodeDistPages);
-            for (i = 0; i <= queuePage; i++) ABC_FREE(queuePages[i]);
-            ABC_FREE(queuePages);
-            st_free_table(pathTable);
-            return;
-            }
-
-            /* Create list element for this child to process its children.
-             * If this node has been processed already, then it appears
-             * in the path table and hence is never added to the list
-             * again.
-             */
-
-            if (queuePageIndex == queuePageSize) ResizeQueuePages();
-            if (memOut) {
-            for (i = 0; i <= nodeDistPage; i++)
-                ABC_FREE(nodeDistPages[i]);
-            ABC_FREE(nodeDistPages);
-            st_free_table(pathTable);
-            return;
-            }
-            *(currentQueuePage + queuePageIndex) = child;
-            queuePageIndex++;
-
-            childrenCount++;
-        } else {
-            /* if not been met in a path with this parity before */
-            /* put in list */
-            if (((Cudd_IsComplement(child)) && (nodeStat->oddTopDist ==
-              MAXSHORTINT)) || ((!Cudd_IsComplement(child)) &&
-                  (nodeStat->evenTopDist == MAXSHORTINT))) {
-
-            if (queuePageIndex == queuePageSize) ResizeQueuePages();
-            if (memOut) {
-                for (i = 0; i <= nodeDistPage; i++)
-                ABC_FREE(nodeDistPages[i]);
-                ABC_FREE(nodeDistPages);
-                st_free_table(pathTable);
-                return;
-
-            }
-            *(currentQueuePage + queuePageIndex) = child;
-            queuePageIndex++;
-
-            /* update the distance with the appropriate parity */
-            if (Cudd_IsComplement(child)) {
-                nodeStat->oddTopDist = (DdHalfWord) topLen + 1;
-            } else {
-                nodeStat->evenTopDist = (DdHalfWord) topLen + 1;
-            }
-            childrenCount++;
-            }
-
-        } /* end of else (not found in st_table) */
-        } /*end of if Not constant child */
-        processingDone--;
-    } /*end of while processing Nv, Nnv */
+            regChild = Cudd_Regular(child);
+            /* dont process if the child is a constant */
+            if (!Cudd_IsConstant(child)) {
+                /* check is already visited, if not add a new entry in
+                 * the path Table
+                 */
+                if (!st_lookup(pathTable, (const char *)regChild, (char **)&nodeStat)) {
+                    /* if not in table, has never been visited */
+                    /* create entry for table */
+                    if (nodeDistPageIndex == nodeDistPageSize)
+                        ResizeNodeDistPages();
+                    if (memOut) {
+                        for (i = 0; i <= queuePage; i++) ABC_FREE(queuePages[i]);
+                        ABC_FREE(queuePages);
+                        st_free_table(pathTable);
+                        return;
+                    }
+                    /* New entry for child in path Table is created here */
+                    nodeStat = currentNodeDistPage + nodeDistPageIndex;
+                    nodeDistPageIndex++;
+
+                    /* Initialize fields of the node data */
+                    nodeStat->oddTopDist = MAXSHORTINT;
+                    nodeStat->evenTopDist = MAXSHORTINT;
+                    nodeStat->evenBotDist = MAXSHORTINT;
+                    nodeStat->oddBotDist = MAXSHORTINT;
+                    nodeStat->regResult = NULL;
+                    nodeStat->compResult = NULL;
+                    /* update the table entry element, the distance keeps
+                     * track of the parity of the path from the root
+                     */
+                    if (Cudd_IsComplement(child)) {
+                        nodeStat->oddTopDist = (DdHalfWord) topLen + 1;
+                    } else {
+                        nodeStat->evenTopDist = (DdHalfWord) topLen + 1;
+                    }
+
+                    /* insert entry element for  child in the table */
+                    if (st_insert(pathTable, (char *)regChild,
+                                  (char *)nodeStat) == ST_OUT_OF_MEM) {
+                        memOut = 1;
+                        for (i = 0; i <= nodeDistPage; i++)
+                            ABC_FREE(nodeDistPages[i]);
+                        ABC_FREE(nodeDistPages);
+                        for (i = 0; i <= queuePage; i++) ABC_FREE(queuePages[i]);
+                        ABC_FREE(queuePages);
+                        st_free_table(pathTable);
+                        return;
+                    }
+
+                    /* Create list element for this child to process its children.
+                     * If this node has been processed already, then it appears
+                     * in the path table and hence is never added to the list
+                     * again.
+                     */
+
+                    if (queuePageIndex == queuePageSize) ResizeQueuePages();
+                    if (memOut) {
+                        for (i = 0; i <= nodeDistPage; i++)
+                            ABC_FREE(nodeDistPages[i]);
+                        ABC_FREE(nodeDistPages);
+                        st_free_table(pathTable);
+                        return;
+                    }
+                    *(currentQueuePage + queuePageIndex) = child;
+                    queuePageIndex++;
+
+                    childrenCount++;
+                } else {
+                    /* if not been met in a path with this parity before */
+                    /* put in list */
+                    if (((Cudd_IsComplement(child)) && (nodeStat->oddTopDist ==
+                          MAXSHORTINT)) || ((!Cudd_IsComplement(child)) &&
+                                  (nodeStat->evenTopDist == MAXSHORTINT))) {
+
+                        if (queuePageIndex == queuePageSize) ResizeQueuePages();
+                        if (memOut) {
+                            for (i = 0; i <= nodeDistPage; i++)
+                                ABC_FREE(nodeDistPages[i]);
+                            ABC_FREE(nodeDistPages);
+                            st_free_table(pathTable);
+                            return;
+
+                        }
+                        *(currentQueuePage + queuePageIndex) = child;
+                        queuePageIndex++;
+
+                        /* update the distance with the appropriate parity */
+                        if (Cudd_IsComplement(child)) {
+                            nodeStat->oddTopDist = (DdHalfWord) topLen + 1;
+                        } else {
+                            nodeStat->evenTopDist = (DdHalfWord) topLen + 1;
+                        }
+                        childrenCount++;
+                    }
+
+                } /* end of else (not found in st_table) */
+            } /*end of if Not constant child */
+            processingDone--;
+        } /*end of while processing Nv, Nnv */
     }  /*end of while numParents */
 
 #ifdef DD_DEBUG
@@ -766,11 +801,11 @@ CreateTopDist(
 #endif
 
     if (childrenCount != 0) {
-    topLen++;
-    childPage = currentQueuePage;
-    childQueueIndex = queuePageIndex;
-    CreateTopDist(pathTable, parentPage, parentQueueIndex, topLen,
-              childPage, childQueueIndex, childrenCount, fp);
+        topLen++;
+        childPage = currentQueuePage;
+        childQueueIndex = queuePageIndex;
+        CreateTopDist(pathTable, parentPage, parentQueueIndex, topLen,
+                      childPage, childQueueIndex, childrenCount, fp);
     }
 
     return;
@@ -813,29 +848,29 @@ CreateBotDist(
     int processingDone;
 
     if (Cudd_IsConstant(node))
-    return(1);
+        return(1);
     N = Cudd_Regular(node);
     /* each node has one table entry */
     /* update as you go down the min dist of each node from
        the root in each (odd and even) parity */
-    if (!st_lookup(pathTable, (char *)N, (char **)&nodeStat)) {
-    fprintf(fp, "Something wrong, the entry doesn't exist\n");
-    return(0);
+    if (!st_lookup(pathTable, (const char *)N, (char **)&nodeStat)) {
+        fprintf(fp, "Something wrong, the entry doesn't exist\n");
+        return(0);
     }
 
     /* compute length of odd parity distances */
     if ((nodeStat->oddTopDist != MAXSHORTINT) &&
-    (nodeStat->oddBotDist != MAXSHORTINT))
-    oddLen = (nodeStat->oddTopDist + nodeStat->oddBotDist);
+        (nodeStat->oddBotDist != MAXSHORTINT))
+        oddLen = (nodeStat->oddTopDist + nodeStat->oddBotDist);
     else
-    oddLen = MAXSHORTINT;
+        oddLen = MAXSHORTINT;
 
     /* compute length of even parity distances */
     if (!((nodeStat->evenTopDist == MAXSHORTINT) ||
-      (nodeStat->evenBotDist == MAXSHORTINT)))
-    evenLen = (nodeStat->evenTopDist +nodeStat->evenBotDist);
+          (nodeStat->evenBotDist == MAXSHORTINT)))
+        evenLen = (nodeStat->evenTopDist +nodeStat->evenBotDist);
     else
-    evenLen = MAXSHORTINT;
+        evenLen = MAXSHORTINT;
 
     /* assign pathlength to minimum of the two */
     pathLength = (oddLen <= evenLen) ? oddLen : evenLen;
@@ -846,116 +881,115 @@ CreateBotDist(
     /* process each child */
     processingDone = 0;
     while (processingDone != 2) {
-    if (!processingDone) {
-        child = Nv;
-    } else {
-        child = Nnv;
-    }
-
-    realChild = Cudd_NotCond(child, Cudd_IsComplement(node));
-    regChild = Cudd_Regular(child);
-    if (Cudd_IsConstant(realChild)) {
-        /* Found a minterm; count parity and shortest distance
-        ** from the constant.
-        */
-        if (Cudd_IsComplement(child))
-        nodeStat->oddBotDist = 1;
-        else
-        nodeStat->evenBotDist = 1;
-    } else { 
-        /* If node not in table, recur. */
-        if (!st_lookup(pathTable, (char *) regChild,
-               (char **)&nodeStatChild)) {
-        fprintf(fp, "Something wrong, node in table should have been created in top dist proc.\n");
-        return(0);
+        if (!processingDone) {
+            child = Nv;
+        } else {
+            child = Nnv;
         }
 
-        if (nodeStatChild->oddBotDist == MAXSHORTINT) {
-        if (nodeStatChild->evenBotDist == MAXSHORTINT) {
-            if (!CreateBotDist(realChild, pathTable, pathLengthArray, fp))
-            return(0);
+        realChild = Cudd_NotCond(child, Cudd_IsComplement(node));
+        regChild = Cudd_Regular(child);
+        if (Cudd_IsConstant(realChild)) {
+            /* Found a minterm; count parity and shortest distance
+            ** from the constant.
+            */
+            if (Cudd_IsComplement(child))
+                nodeStat->oddBotDist = 1;
+            else
+                nodeStat->evenBotDist = 1;
         } else {
-            fprintf(fp, "Something wrong, both bot nodeStats should be there\n");
-            return(0);
-        }
-        }
+            /* If node not in table, recur. */
+            if (!st_lookup(pathTable, (const char *)regChild, (char **)&nodeStatChild)) {
+                fprintf(fp, "Something wrong, node in table should have been created in top dist proc.\n");
+                return(0);
+            }
+
+            if (nodeStatChild->oddBotDist == MAXSHORTINT) {
+                if (nodeStatChild->evenBotDist == MAXSHORTINT) {
+                    if (!CreateBotDist(realChild, pathTable, pathLengthArray, fp))
+                        return(0);
+                } else {
+                    fprintf(fp, "Something wrong, both bot nodeStats should be there\n");
+                    return(0);
+                }
+            }
 
-        /* Update shortest distance from the constant depending on
-        **  parity. */
-
-        if (Cudd_IsComplement(child)) {
-        /* If parity on the edge then add 1 to even distance
-        ** of child to get odd parity distance and add 1 to
-        ** odd distance of child to get even parity
-        ** distance. Change distance of current node only if
-        ** the calculated distance is less than existing
-        ** distance. */
-        if (nodeStatChild->oddBotDist != MAXSHORTINT)
-            botDist = nodeStatChild->oddBotDist + 1;
-        else
-            botDist = MAXSHORTINT;
-        if (nodeStat->evenBotDist > botDist )
-            nodeStat->evenBotDist = botDist;
-
-        if (nodeStatChild->evenBotDist != MAXSHORTINT)
-            botDist = nodeStatChild->evenBotDist + 1;
-        else
-            botDist = MAXSHORTINT;
-        if (nodeStat->oddBotDist > botDist)
-            nodeStat->oddBotDist = botDist;
+            /* Update shortest distance from the constant depending on
+            **  parity. */
 
-        } else {
-        /* If parity on the edge then add 1 to even distance
-        ** of child to get even parity distance and add 1 to
-        ** odd distance of child to get odd parity distance.
-        ** Change distance of current node only if the
-        ** calculated distance is lesser than existing
-        ** distance. */
-        if (nodeStatChild->evenBotDist != MAXSHORTINT)
-            botDist = nodeStatChild->evenBotDist + 1;
-        else
-            botDist = MAXSHORTINT;
-        if (nodeStat->evenBotDist > botDist)
-            nodeStat->evenBotDist = botDist;
-
-        if (nodeStatChild->oddBotDist != MAXSHORTINT)
-            botDist = nodeStatChild->oddBotDist + 1;
-        else
-            botDist = MAXSHORTINT;
-        if (nodeStat->oddBotDist > botDist)
-            nodeStat->oddBotDist = botDist;
-        }
-    } /* end of else (if not constant child ) */
-    processingDone++;
+            if (Cudd_IsComplement(child)) {
+                /* If parity on the edge then add 1 to even distance
+                ** of child to get odd parity distance and add 1 to
+                ** odd distance of child to get even parity
+                ** distance. Change distance of current node only if
+                ** the calculated distance is less than existing
+                ** distance. */
+                if (nodeStatChild->oddBotDist != MAXSHORTINT)
+                    botDist = nodeStatChild->oddBotDist + 1;
+                else
+                    botDist = MAXSHORTINT;
+                if (nodeStat->evenBotDist > botDist )
+                    nodeStat->evenBotDist = botDist;
+
+                if (nodeStatChild->evenBotDist != MAXSHORTINT)
+                    botDist = nodeStatChild->evenBotDist + 1;
+                else
+                    botDist = MAXSHORTINT;
+                if (nodeStat->oddBotDist > botDist)
+                    nodeStat->oddBotDist = botDist;
+
+            } else {
+                /* If parity on the edge then add 1 to even distance
+                ** of child to get even parity distance and add 1 to
+                ** odd distance of child to get odd parity distance.
+                ** Change distance of current node only if the
+                ** calculated distance is lesser than existing
+                ** distance. */
+                if (nodeStatChild->evenBotDist != MAXSHORTINT)
+                    botDist = nodeStatChild->evenBotDist + 1;
+                else
+                    botDist = MAXSHORTINT;
+                if (nodeStat->evenBotDist > botDist)
+                    nodeStat->evenBotDist = botDist;
+
+                if (nodeStatChild->oddBotDist != MAXSHORTINT)
+                    botDist = nodeStatChild->oddBotDist + 1;
+                else
+                    botDist = MAXSHORTINT;
+                if (nodeStat->oddBotDist > botDist)
+                    nodeStat->oddBotDist = botDist;
+            }
+        } /* end of else (if not constant child ) */
+        processingDone++;
     } /* end of while processing Nv, Nnv */
 
     /* Compute shortest path length on the fly. */
     if ((nodeStat->oddTopDist != MAXSHORTINT) &&
-    (nodeStat->oddBotDist != MAXSHORTINT))
-    oddLen = (nodeStat->oddTopDist + nodeStat->oddBotDist);
+        (nodeStat->oddBotDist != MAXSHORTINT))
+        oddLen = (nodeStat->oddTopDist + nodeStat->oddBotDist);
     else
-    oddLen = MAXSHORTINT;
+        oddLen = MAXSHORTINT;
 
     if ((nodeStat->evenTopDist != MAXSHORTINT) &&
-    (nodeStat->evenBotDist != MAXSHORTINT))
-    evenLen = (nodeStat->evenTopDist +nodeStat->evenBotDist);
+        (nodeStat->evenBotDist != MAXSHORTINT))
+        evenLen = (nodeStat->evenTopDist +nodeStat->evenBotDist);
     else
-    evenLen = MAXSHORTINT;
+        evenLen = MAXSHORTINT;
 
     /* Update path length array that has number of nodes of a particular
     ** path length. */
     if (oddLen < pathLength ) {
-    if (pathLength != MAXSHORTINT)
-        pathLengthArray[pathLength]--;
-    if (oddLen != MAXSHORTINT)
-        pathLengthArray[oddLen]++;
-    pathLength = oddLen;
+        if (pathLength != MAXSHORTINT)
+            pathLengthArray[pathLength]--;
+        if (oddLen != MAXSHORTINT)
+            pathLengthArray[oddLen]++;
+        pathLength = oddLen;
     }
     if (evenLen < pathLength ) {
-    if (pathLength != MAXSHORTINT)
-        pathLengthArray[pathLength]--;
-    if (evenLen != MAXSHORTINT)
-        pathLengthArray[evenLen]++;
+        if (pathLength != MAXSHORTINT)
+            pathLengthArray[pathLength]--;
+        if (evenLen != MAXSHORTINT)
+            pathLengthArray[evenLen]++;
     }
 
     return(1);
@@ -999,21 +1033,21 @@ CreatePathTable(
     int childQueueIndex, parentQueueIndex;
 
     /* Creating path Table for storing data about nodes */
-    pathTable = st_init_table(st_ptrcmp, st_ptrhash);;
+    pathTable = st_init_table(st_ptrcmp,st_ptrhash);
 
     /* initializing pages for info about each node */
     maxNodeDistPages = INITIAL_PAGES;
     nodeDistPages = ABC_ALLOC(NodeDist_t *, maxNodeDistPages);
     if (nodeDistPages == NULL) {
-    goto OUT_OF_MEM;
+        goto OUT_OF_MEM;
     }
     nodeDistPage = 0;
     currentNodeDistPage = nodeDistPages[nodeDistPage] =
-    ABC_ALLOC(NodeDist_t, nodeDistPageSize);
+        ABC_ALLOC(NodeDist_t, nodeDistPageSize);
     if (currentNodeDistPage == NULL) {
-    for (i = 0; i <= nodeDistPage; i++) ABC_FREE(nodeDistPages[i]);
-    ABC_FREE(nodeDistPages);
-    goto OUT_OF_MEM;
+        for (i = 0; i <= nodeDistPage; i++) ABC_FREE(nodeDistPages[i]);
+        ABC_FREE(nodeDistPages);
+        goto OUT_OF_MEM;
     }
     nodeDistPageIndex = 0;
 
@@ -1021,14 +1055,14 @@ CreatePathTable(
     maxQueuePages = INITIAL_PAGES;
     queuePages = ABC_ALLOC(DdNode **, maxQueuePages);
     if (queuePages == NULL) {
-    goto OUT_OF_MEM;
+        goto OUT_OF_MEM;
     }
     queuePage = 0;
     currentQueuePage  = queuePages[queuePage] = ABC_ALLOC(DdNode *, queuePageSize);
     if (currentQueuePage == NULL) {
-    for (i = 0; i <= queuePage; i++) ABC_FREE(queuePages[i]);
-    ABC_FREE(queuePages);
-    goto OUT_OF_MEM;
+        for (i = 0; i <= queuePage; i++) ABC_FREE(queuePages[i]);
+        ABC_FREE(queuePages);
+        goto OUT_OF_MEM;
     }
     queuePageIndex = 0;
 
@@ -1045,12 +1079,12 @@ CreatePathTable(
 
     if (nodeDistPageIndex == nodeDistPageSize) ResizeNodeDistPages();
     if (memOut) {
-    for (i = 0; i <= nodeDistPage; i++) ABC_FREE(nodeDistPages[i]);
-    ABC_FREE(nodeDistPages);
-    for (i = 0; i <= queuePage; i++) ABC_FREE(queuePages[i]);
-    ABC_FREE(queuePages);
-    st_free_table(pathTable);
-    goto OUT_OF_MEM;
+        for (i = 0; i <= nodeDistPage; i++) ABC_FREE(nodeDistPages[i]);
+        ABC_FREE(nodeDistPages);
+        for (i = 0; i <= queuePage; i++) ABC_FREE(queuePages[i]);
+        ABC_FREE(queuePages);
+        st_free_table(pathTable);
+        goto OUT_OF_MEM;
     }
 
     nodeStat = currentNodeDistPage + nodeDistPageIndex;
@@ -1065,22 +1099,22 @@ CreatePathTable(
 
     insertValue = st_insert(pathTable, (char *)N, (char *)nodeStat);
     if (insertValue == ST_OUT_OF_MEM) {
-    memOut = 1;
-    for (i = 0; i <= nodeDistPage; i++) ABC_FREE(nodeDistPages[i]);
-    ABC_FREE(nodeDistPages);
-    for (i = 0; i <= queuePage; i++) ABC_FREE(queuePages[i]);
-    ABC_FREE(queuePages);
-    st_free_table(pathTable);
-    goto OUT_OF_MEM;
+        memOut = 1;
+        for (i = 0; i <= nodeDistPage; i++) ABC_FREE(nodeDistPages[i]);
+        ABC_FREE(nodeDistPages);
+        for (i = 0; i <= queuePage; i++) ABC_FREE(queuePages[i]);
+        ABC_FREE(queuePages);
+        st_free_table(pathTable);
+        goto OUT_OF_MEM;
     } else if (insertValue == 1) {
-    fprintf(fp, "Something wrong, the entry exists but didnt show up in st_lookup\n");
-    return(NULL);
+        fprintf(fp, "Something wrong, the entry exists but didnt show up in st_lookup\n");
+        return(NULL);
     }
 
     if (Cudd_IsComplement(node)) {
-    nodeStat->oddTopDist = 0;
+        nodeStat->oddTopDist = 0;
     } else {
-    nodeStat->evenTopDist = 0;
+        nodeStat->evenTopDist = 0;
     }
     numParents = 1;
     /* call the function that counts the distance of each node from the
@@ -1090,10 +1124,10 @@ CreatePathTable(
     numCalls = 0;
 #endif
     CreateTopDist(pathTable, parentPage, parentQueueIndex, (int) topLen,
-          childPage, childQueueIndex, numParents, fp);
+                  childPage, childQueueIndex, numParents, fp);
     if (memOut) {
-    fprintf(fp, "Out of Memory and cant count path lengths\n");
-    goto OUT_OF_MEM;
+        fprintf(fp, "Out of Memory and cant count path lengths\n");
+        goto OUT_OF_MEM;
     }
 
 #ifdef DD_DEBUG
@@ -1151,24 +1185,24 @@ AssessPathLength(
      * below zero
      */
     while ((i < (unsigned) numVars+1) && (temp > 0)) {
-    if (pathLengthArray[i] > 0) {
-        maxpath = i;
-        temp = temp - pathLengthArray[i];
-    }
-    i++;
+        if (pathLengthArray[i] > 0) {
+            maxpath = i;
+            temp = temp - pathLengthArray[i];
+        }
+        i++;
     }
     /* if all nodes of max path are needed */
     if (temp >= 0) {
-    maxpath++; /* now maxpath  becomes the next maxppath or max number
-              of variables */
-    *excess = 0;
+        maxpath++; /* now maxpath  becomes the next maxppath or max number
+                      of variables */
+        *excess = 0;
     } else { /* normal case when subset required is less than size of
-        original BDD */
-    *excess = temp + pathLengthArray[maxpath];
+                original BDD */
+        *excess = temp + pathLengthArray[maxpath];
     }
 
     if (maxpath == 0) {
-    fprintf(fp, "Path Length array seems to be all zeroes, check\n");
+        fprintf(fp, "Path Length array seems to be all zeroes, check\n");
     }
     return(maxpath);
 
@@ -1227,14 +1261,12 @@ BuildSubsetBdd(
 {
     DdNode *N, *Nv, *Nnv;
     DdNode *ThenBranch, *ElseBranch, *childBranch;
-    DdNode *child, *regChild;
-    DdNode *regNnv = NULL, *regNv = NULL; // Suppress "might be used uninitialized"
+    DdNode *child, *regChild, *regNnv, *regNv;
     NodeDist_t *nodeStatNv, *nodeStat, *nodeStatNnv;
     DdNode *neW, *topv, *regNew;
     char *entry;
     unsigned int topid;
-    unsigned int childPathLength, oddLen, evenLen;
-    unsigned int NnvPathLength = -1, NvPathLength = -1; // Suppress "might be used uninitialized"
+    unsigned int childPathLength, oddLen, evenLen, NnvPathLength, NvPathLength;
     unsigned int NvBotDist, NnvBotDist;
     int tiebreakChild;
     int  processingDone, thenDone, elseDone;
@@ -1244,14 +1276,14 @@ BuildSubsetBdd(
     numCalls++;
 #endif
     if (Cudd_IsConstant(node))
-    return(node);
+        return(node);
 
     N = Cudd_Regular(node);
     /* Find node in table. */
-    if (!st_lookup(pathTable, (char *)N, (char **)&nodeStat)) {
-    (void) fprintf(dd->err, "Something wrong, node must be in table \n");
-    dd->errorCode = CUDD_INTERNAL_ERROR;
-    return(NULL);
+    if (!st_lookup(pathTable, (const char *)N, (char **)&nodeStat)) {
+        (void) fprintf(dd->err, "Something wrong, node must be in table \n");
+        dd->errorCode = CUDD_INTERNAL_ERROR;
+        return(NULL);
     }
     /* If the node in the table has been visited, then return the corresponding
     ** Dd. Since a node can become a subset of itself, its
@@ -1263,22 +1295,22 @@ BuildSubsetBdd(
 
     /* If this node is reached with an odd parity, get odd parity results. */
     if (Cudd_IsComplement(node)) {
-    if  (nodeStat->compResult != NULL) {
+        if  (nodeStat->compResult != NULL) {
 #ifdef DD_DEBUG
-        hits++;
+            hits++;
 #endif
-        return(nodeStat->compResult);
-    }
+            return(nodeStat->compResult);
+        }
     } else {
-    /* if this node is reached with an even parity, get even parity
-     * results
-     */
-    if (nodeStat->regResult != NULL) {
+        /* if this node is reached with an even parity, get even parity
+         * results
+         */
+        if (nodeStat->regResult != NULL) {
 #ifdef DD_DEBUG
-        hits++;
+            hits++;
 #endif
-        return(nodeStat->regResult);
-    }
+            return(nodeStat->regResult);
+        }
     }
 
 
@@ -1299,220 +1331,220 @@ BuildSubsetBdd(
     ElseBranch = NULL;
     /* if then child constant, branch is the child */
     if (Cudd_IsConstant(Nv)) {
-    /*shortest path found */
-    if ((Nv == DD_ONE(dd)) && (info->findShortestPath)) {
-        info->findShortestPath = 0;
-    }
+        /*shortest path found */
+        if ((Nv == DD_ONE(dd)) && (info->findShortestPath)) {
+            info->findShortestPath = 0;
+        }
 
-    ThenBranch = Nv;
-    cuddRef(ThenBranch);
-    if (ThenBranch == NULL) {
-        return(NULL);
-    }
+        ThenBranch = Nv;
+        cuddRef(ThenBranch);
+        if (ThenBranch == NULL) {
+            return(NULL);
+        }
 
-    thenDone++;
-    processingDone++;
-    NvBotDist = MAXSHORTINT;
+        thenDone++;
+        processingDone++;
+        NvBotDist = MAXSHORTINT;
     } else {
-    /* Derive regular child for table lookup. */
-    regNv = Cudd_Regular(Nv);
-    /* Get node data for shortest path length. */
-    if (!st_lookup(pathTable, (char *)regNv, (char **)&nodeStatNv) ) {
-        (void) fprintf(dd->err, "Something wrong, node must be in table\n");
-        dd->errorCode = CUDD_INTERNAL_ERROR;
-        return(NULL);
-    }
-    /* Derive shortest path length for child. */
-    if ((nodeStatNv->oddTopDist != MAXSHORTINT) &&
-        (nodeStatNv->oddBotDist != MAXSHORTINT)) {
-        oddLen = (nodeStatNv->oddTopDist + nodeStatNv->oddBotDist);
-    } else {
-        oddLen = MAXSHORTINT;
-    }
+        /* Derive regular child for table lookup. */
+        regNv = Cudd_Regular(Nv);
+        /* Get node data for shortest path length. */
+        if (!st_lookup(pathTable, (const char *)regNv, (char **)&nodeStatNv) ) {
+            (void) fprintf(dd->err, "Something wrong, node must be in table\n");
+            dd->errorCode = CUDD_INTERNAL_ERROR;
+            return(NULL);
+        }
+        /* Derive shortest path length for child. */
+        if ((nodeStatNv->oddTopDist != MAXSHORTINT) &&
+            (nodeStatNv->oddBotDist != MAXSHORTINT)) {
+            oddLen = (nodeStatNv->oddTopDist + nodeStatNv->oddBotDist);
+        } else {
+            oddLen = MAXSHORTINT;
+        }
 
-    if ((nodeStatNv->evenTopDist != MAXSHORTINT) &&
-        (nodeStatNv->evenBotDist != MAXSHORTINT)) {
-        evenLen = (nodeStatNv->evenTopDist +nodeStatNv->evenBotDist);
-    } else {
-        evenLen = MAXSHORTINT;
-    }
+        if ((nodeStatNv->evenTopDist != MAXSHORTINT) &&
+            (nodeStatNv->evenBotDist != MAXSHORTINT)) {
+            evenLen = (nodeStatNv->evenTopDist +nodeStatNv->evenBotDist);
+        } else {
+            evenLen = MAXSHORTINT;
+        }
 
-    NvPathLength = (oddLen <= evenLen) ? oddLen : evenLen;
-    NvBotDist = (oddLen <= evenLen) ? nodeStatNv->oddBotDist:
-                                               nodeStatNv->evenBotDist;
+        NvPathLength = (oddLen <= evenLen) ? oddLen : evenLen;
+        NvBotDist = (oddLen <= evenLen) ? nodeStatNv->oddBotDist:
+                                                   nodeStatNv->evenBotDist;
     }
     /* if else child constant, branch is the child */
     if (Cudd_IsConstant(Nnv)) {
-    /*shortest path found */
-    if ((Nnv == DD_ONE(dd)) && (info->findShortestPath)) {
-        info->findShortestPath = 0;
-    }
+        /*shortest path found */
+        if ((Nnv == DD_ONE(dd)) && (info->findShortestPath)) {
+            info->findShortestPath = 0;
+        }
 
-    ElseBranch = Nnv;
-    cuddRef(ElseBranch);
-    if (ElseBranch == NULL) {
-        return(NULL);
-    }
+        ElseBranch = Nnv;
+        cuddRef(ElseBranch);
+        if (ElseBranch == NULL) {
+            return(NULL);
+        }
 
-    elseDone++;
-    processingDone++;
-    NnvBotDist = MAXSHORTINT;
-    } else {
-    /* Derive regular child for table lookup. */
-    regNnv = Cudd_Regular(Nnv);
-    /* Get node data for shortest path length. */
-    if (!st_lookup(pathTable, (char *)regNnv, (char **)&nodeStatNnv) ) {
-        (void) fprintf(dd->err, "Something wrong, node must be in table\n");
-        dd->errorCode = CUDD_INTERNAL_ERROR;
-        return(NULL);
-    }
-    /* Derive shortest path length for child. */
-    if ((nodeStatNnv->oddTopDist != MAXSHORTINT) &&
-        (nodeStatNnv->oddBotDist != MAXSHORTINT)) {
-        oddLen = (nodeStatNnv->oddTopDist + nodeStatNnv->oddBotDist);
+        elseDone++;
+        processingDone++;
+        NnvBotDist = MAXSHORTINT;
     } else {
-        oddLen = MAXSHORTINT;
-    }
+        /* Derive regular child for table lookup. */
+        regNnv = Cudd_Regular(Nnv);
+        /* Get node data for shortest path length. */
+        if (!st_lookup(pathTable, (const char *)regNnv, (char **)&nodeStatNnv) ) {
+            (void) fprintf(dd->err, "Something wrong, node must be in table\n");
+            dd->errorCode = CUDD_INTERNAL_ERROR;
+            return(NULL);
+        }
+        /* Derive shortest path length for child. */
+        if ((nodeStatNnv->oddTopDist != MAXSHORTINT) &&
+            (nodeStatNnv->oddBotDist != MAXSHORTINT)) {
+            oddLen = (nodeStatNnv->oddTopDist + nodeStatNnv->oddBotDist);
+        } else {
+            oddLen = MAXSHORTINT;
+        }
 
-    if ((nodeStatNnv->evenTopDist != MAXSHORTINT) &&
-        (nodeStatNnv->evenBotDist != MAXSHORTINT)) {
-        evenLen = (nodeStatNnv->evenTopDist +nodeStatNnv->evenBotDist);
-    } else {
-        evenLen = MAXSHORTINT;
-    }
+        if ((nodeStatNnv->evenTopDist != MAXSHORTINT) &&
+            (nodeStatNnv->evenBotDist != MAXSHORTINT)) {
+            evenLen = (nodeStatNnv->evenTopDist +nodeStatNnv->evenBotDist);
+        } else {
+            evenLen = MAXSHORTINT;
+        }
 
-    NnvPathLength = (oddLen <= evenLen) ? oddLen : evenLen;
-    NnvBotDist = (oddLen <= evenLen) ? nodeStatNnv->oddBotDist :
-                                               nodeStatNnv->evenBotDist;
+        NnvPathLength = (oddLen <= evenLen) ? oddLen : evenLen;
+        NnvBotDist = (oddLen <= evenLen) ? nodeStatNnv->oddBotDist :
+                                                   nodeStatNnv->evenBotDist;
     }
 
     tiebreakChild = (NvBotDist <= NnvBotDist) ? 1 : 0;
     /* while both children not processed */
     while (processingDone != 2) {
-    if (!processingDone) {
-        /* if no child processed */
-        /* pick the child with shortest path length and record which one
-         * picked
-         */
-        if ((NvPathLength < NnvPathLength) ||
-        ((NvPathLength == NnvPathLength) && (tiebreakChild == 1))) {
-        child = Nv;
-        regChild = regNv;
-        thenDone = 1;
-        childPathLength = NvPathLength;
-        } else {
-        child = Nnv;
-        regChild = regNnv;
-        elseDone = 1;
-        childPathLength = NnvPathLength;
-        } /* then path length less than else path length */
-    } else {
-        /* if one child processed, process the other */
-        if (thenDone) {
-        child = Nnv;
-        regChild = regNnv;
-        elseDone = 1;
-        childPathLength = NnvPathLength;
+        if (!processingDone) {
+            /* if no child processed */
+            /* pick the child with shortest path length and record which one
+             * picked
+             */
+            if ((NvPathLength < NnvPathLength) ||
+                ((NvPathLength == NnvPathLength) && (tiebreakChild == 1))) {
+                child = Nv;
+                regChild = regNv;
+                thenDone = 1;
+                childPathLength = NvPathLength;
+            } else {
+                child = Nnv;
+                regChild = regNnv;
+                elseDone = 1;
+                childPathLength = NnvPathLength;
+            } /* then path length less than else path length */
         } else {
-        child = Nv;
-        regChild = regNv;
-        thenDone = 1;
-        childPathLength = NvPathLength;
-        } /* end of else pick the Then child if ELSE child processed */
-    } /* end of else one child has been processed */
-
-    /* ignore (replace with constant 0) all nodes which lie on paths larger
-     * than the maximum length of the path required
-     */
-    if (childPathLength > info->maxpath) {
-        /* record nodes visited */
-        childBranch = zero;
-    } else {
-        if (childPathLength < info->maxpath) {
-        if (info->findShortestPath) {
-            info->findShortestPath = 0;
-        }
-        childBranch = BuildSubsetBdd(dd, pathTable, child, info,
-                         subsetNodeTable);
-
-        } else { /* Case: path length of node = maxpath */
-        /* If the node labeled with maxpath is found in the
-        ** maxpathTable, use it to build the subset BDD.  */
-        if (st_lookup(info->maxpathTable, (char *)regChild,
-                  (char **)&entry)) {
-            /* When a node that is already been chosen is hit,
-            ** the quest for a complete path is over.  */
-            if (info->findShortestPath) {
-            info->findShortestPath = 0;
-            }
-            childBranch = BuildSubsetBdd(dd, pathTable, child, info,
-                         subsetNodeTable);
+            /* if one child processed, process the other */
+            if (thenDone) {
+                child = Nnv;
+                regChild = regNnv;
+                elseDone = 1;
+                childPathLength = NnvPathLength;
+            } else {
+                child = Nv;
+                regChild = regNv;
+                thenDone = 1;
+                childPathLength = NvPathLength;
+            } /* end of else pick the Then child if ELSE child processed */
+        } /* end of else one child has been processed */
+
+        /* ignore (replace with constant 0) all nodes which lie on paths larger
+         * than the maximum length of the path required
+         */
+        if (childPathLength > info->maxpath) {
+            /* record nodes visited */
+            childBranch = zero;
         } else {
-            /* If node is not found in the maxpathTable and
-            ** the threshold has been reached, then if the
-            ** path needs to be completed, continue. Else
-            ** replace the node with a zero.  */
-            if (info->thresholdReached <= 0) {
-            if (info->findShortestPath) {
-                if (st_insert(info->maxpathTable, (char *)regChild,
-                      (char *)NIL(char)) == ST_OUT_OF_MEM) {
-                memOut = 1;
-                (void) fprintf(dd->err, "OUT of memory\n");
-                info->thresholdReached = 0;
-                childBranch = zero;
-                } else {
-                info->thresholdReached--;
-                childBranch = BuildSubsetBdd(dd, pathTable,
-                            child, info,subsetNodeTable);
+            if (childPathLength < info->maxpath) {
+                if (info->findShortestPath) {
+                    info->findShortestPath = 0;
                 }
-            } else { /* not find shortest path, we dont need this
-                    node */
-                childBranch = zero;
+                childBranch = BuildSubsetBdd(dd, pathTable, child, info,
+                                             subsetNodeTable);
+
+            } else { /* Case: path length of node = maxpath */
+                /* If the node labeled with maxpath is found in the
+                ** maxpathTable, use it to build the subset BDD.  */
+                if (st_lookup(info->maxpathTable, (char *)regChild,
+                              (char **)&entry)) {
+                    /* When a node that is already been chosen is hit,
+                    ** the quest for a complete path is over.  */
+                    if (info->findShortestPath) {
+                        info->findShortestPath = 0;
+                    }
+                    childBranch = BuildSubsetBdd(dd, pathTable, child, info,
+                                                 subsetNodeTable);
+                } else {
+                    /* If node is not found in the maxpathTable and
+                    ** the threshold has been reached, then if the
+                    ** path needs to be completed, continue. Else
+                    ** replace the node with a zero.  */
+                    if (info->thresholdReached <= 0) {
+                        if (info->findShortestPath) {
+                            if (st_insert(info->maxpathTable, (char *)regChild,
+                                          (char *)NIL(char)) == ST_OUT_OF_MEM) {
+                                memOut = 1;
+                                (void) fprintf(dd->err, "OUT of memory\n");
+                                info->thresholdReached = 0;
+                                childBranch = zero;
+                            } else {
+                                info->thresholdReached--;
+                                childBranch = BuildSubsetBdd(dd, pathTable,
+                                                    child, info,subsetNodeTable);
+                            }
+                        } else { /* not find shortest path, we dont need this
+                                    node */
+                            childBranch = zero;
+                        }
+                    } else { /* Threshold hasn't been reached,
+                             ** need the node. */
+                        if (st_insert(info->maxpathTable, (char *)regChild,
+                                      (char *)NIL(char)) == ST_OUT_OF_MEM) {
+                            memOut = 1;
+                            (void) fprintf(dd->err, "OUT of memory\n");
+                            info->thresholdReached = 0;
+                            childBranch = zero;
+                        } else {
+                            info->thresholdReached--;
+                            if (info->thresholdReached <= 0) {
+                                info->findShortestPath = 1;
+                            }
+                            childBranch = BuildSubsetBdd(dd, pathTable,
+                                                 child, info, subsetNodeTable);
+
+                        } /* end of st_insert successful */
+                    } /* end of threshold hasnt been reached yet */
+                } /* end of else node not found in maxpath table */
+            } /* end of if (path length of node = maxpath) */
+        } /* end if !(childPathLength > maxpath) */
+        if (childBranch == NULL) {
+            /* deref other stuff incase reordering has taken place */
+            if (ThenBranch != NULL) {
+                Cudd_RecursiveDeref(dd, ThenBranch);
+                ThenBranch = NULL;
             }
-            } else { /* Threshold hasn't been reached,
-                 ** need the node. */
-            if (st_insert(info->maxpathTable, (char *)regChild,
-                      (char *)NIL(char)) == ST_OUT_OF_MEM) {
-                memOut = 1;
-                (void) fprintf(dd->err, "OUT of memory\n");
-                info->thresholdReached = 0;
-                childBranch = zero;
-            } else {
-                info->thresholdReached--;
-                if (info->thresholdReached <= 0) {
-                info->findShortestPath = 1;
-                }
-                childBranch = BuildSubsetBdd(dd, pathTable,
-                         child, info, subsetNodeTable);
-
-            } /* end of st_insert successful */
-            } /* end of threshold hasnt been reached yet */
-        } /* end of else node not found in maxpath table */
-        } /* end of if (path length of node = maxpath) */
-    } /* end if !(childPathLength > maxpath) */
-    if (childBranch == NULL) {
-        /* deref other stuff incase reordering has taken place */
-        if (ThenBranch != NULL) {
-        Cudd_RecursiveDeref(dd, ThenBranch);
-        ThenBranch = NULL;
-        }
-        if (ElseBranch != NULL) {
-        Cudd_RecursiveDeref(dd, ElseBranch);
-        ElseBranch = NULL;
+            if (ElseBranch != NULL) {
+                Cudd_RecursiveDeref(dd, ElseBranch);
+                ElseBranch = NULL;
+            }
+            return(NULL);
         }
-        return(NULL);
-    }
 
-    cuddRef(childBranch);
+        cuddRef(childBranch);
 
-    if (child == Nv) {
-        ThenBranch = childBranch;
-    } else {
-        ElseBranch = childBranch;
-    }
-    processingDone++;
+        if (child == Nv) {
+            ThenBranch = childBranch;
+        } else {
+            ElseBranch = childBranch;
+        }
+        processingDone++;
 
-    } /*end of while processing Nv, Nnv */      
+    } /*end of while processing Nv, Nnv */
 
     info->findShortestPath = 0;
     topid = Cudd_NodeReadIndex(N);
@@ -1520,7 +1552,7 @@ BuildSubsetBdd(
     cuddRef(topv);
     neW = cuddBddIteRecur(dd, topv, ThenBranch, ElseBranch);
     if (neW != NULL) {
-    cuddRef(neW);
+        cuddRef(neW);
     }
     Cudd_RecursiveDeref(dd, topv);
     Cudd_RecursiveDeref(dd, ThenBranch);
@@ -1529,76 +1561,76 @@ BuildSubsetBdd(
 
     /* Hard Limit of threshold has been imposed */
     if (subsetNodeTable != NIL(st_table)) {
-    /* check if a new node is created */
-    regNew = Cudd_Regular(neW);
-    /* subset node table keeps all new nodes that have been created to keep
-     * a running count of how many nodes have been built in the subset.
-     */
-    if (!st_lookup(subsetNodeTable, (char *)regNew, (char **)&entry)) {
-        if (!Cudd_IsConstant(regNew)) {
-        if (st_insert(subsetNodeTable, (char *)regNew,
-                  (char *)NULL) == ST_OUT_OF_MEM) {
-            (void) fprintf(dd->err, "Out of memory\n");
-            return (NULL);
-        }
-        if (st_count(subsetNodeTable) > info->threshold) {
-            info->thresholdReached = 0;
-        }
+        /* check if a new node is created */
+        regNew = Cudd_Regular(neW);
+        /* subset node table keeps all new nodes that have been created to keep
+         * a running count of how many nodes have been built in the subset.
+         */
+        if (!st_lookup(subsetNodeTable, (char *)regNew, (char **)&entry)) {
+            if (!Cudd_IsConstant(regNew)) {
+                if (st_insert(subsetNodeTable, (char *)regNew,
+                              (char *)NULL) == ST_OUT_OF_MEM) {
+                    (void) fprintf(dd->err, "Out of memory\n");
+                    return (NULL);
+                }
+                if (st_count(subsetNodeTable) > info->threshold) {
+                    info->thresholdReached = 0;
+                }
+            }
         }
     }
-    }
 
 
     if (neW == NULL) {
-    return(NULL);
+        return(NULL);
     } else {
-    /*store computed result in regular form*/
-    if (Cudd_IsComplement(node)) {
-        nodeStat->compResult = neW;
-        cuddRef(nodeStat->compResult);
-        /* if the new node is the same as the corresponding node in the
-         * original bdd then its complement need not be computed as it
-         * cannot be larger than the node itself
-         */
-        if (neW == node) {
+        /*store computed result in regular form*/
+        if (Cudd_IsComplement(node)) {
+            nodeStat->compResult = neW;
+            cuddRef(nodeStat->compResult);
+            /* if the new node is the same as the corresponding node in the
+             * original bdd then its complement need not be computed as it
+             * cannot be larger than the node itself
+             */
+            if (neW == node) {
 #ifdef DD_DEBUG
-        thishit++;
+                thishit++;
 #endif
-        /* if a result for the node has already been computed, then
-         * it can only be smaller than teh node itself. hence store
-         * the node result in order not to break recombination
-         */
-        if (nodeStat->regResult != NULL) {
-            Cudd_RecursiveDeref(dd, nodeStat->regResult);
-        }
-        nodeStat->regResult = Cudd_Not(neW);
-        cuddRef(nodeStat->regResult);
-        }
+                /* if a result for the node has already been computed, then
+                 * it can only be smaller than teh node itself. hence store
+                 * the node result in order not to break recombination
+                 */
+                if (nodeStat->regResult != NULL) {
+                    Cudd_RecursiveDeref(dd, nodeStat->regResult);
+                }
+                nodeStat->regResult = Cudd_Not(neW);
+                cuddRef(nodeStat->regResult);
+            }
 
-    } else {
-        nodeStat->regResult = neW;
-        cuddRef(nodeStat->regResult);
-        if (neW == node) {
+        } else {
+            nodeStat->regResult = neW;
+            cuddRef(nodeStat->regResult);
+            if (neW == node) {
 #ifdef DD_DEBUG
-        thishit++;
+                thishit++;
 #endif
-        if (nodeStat->compResult != NULL) {
-            Cudd_RecursiveDeref(dd, nodeStat->compResult);
-        }
-        nodeStat->compResult = Cudd_Not(neW);
-        cuddRef(nodeStat->compResult);
+                if (nodeStat->compResult != NULL) {
+                    Cudd_RecursiveDeref(dd, nodeStat->compResult);
+                }
+                nodeStat->compResult = Cudd_Not(neW);
+                cuddRef(nodeStat->compResult);
+            }
         }
-    } 
 
-    cuddDeref(neW);
-    return(neW);
+        cuddDeref(neW);
+        return(neW);
     } /* end of else i.e. Subset != NULL */
 } /* end of BuildSubsetBdd */
 
 
 /**Function********************************************************************
 
-  Synopsis     [Procedure to free the result dds stored in the NodeDist pages.]
+  Synopsis     [Procedure to free te result dds stored in the NodeDist pages.]
 
   Description [None]
 
@@ -1619,13 +1651,15 @@ stPathTableDdFree(
     nodeStat = (NodeDist_t *)value;
     dd = (DdManager *)arg;
     if (nodeStat->regResult != NULL) {
-    Cudd_RecursiveDeref(dd, nodeStat->regResult);
+        Cudd_RecursiveDeref(dd, nodeStat->regResult);
     }
     if (nodeStat->compResult != NULL) {
-    Cudd_RecursiveDeref(dd, nodeStat->compResult);
+        Cudd_RecursiveDeref(dd, nodeStat->compResult);
     }
     return(ST_CONTINUE);
 
 } /* end of stPathTableFree */
+
+
 ABC_NAMESPACE_IMPL_END