Upgrade to the latest CUDD 2.4.2.

1 files changed, 664 insertions, 634 deletions

diff --git a/src/bdd/cudd/cuddZddFuncs.c b/src/bdd/cudd/cuddZddFuncs.c
index 2560159c..41f7c64c 100644
--- a/src/bdd/cudd/cuddZddFuncs.c
+++ b/src/bdd/cudd/cuddZddFuncs.c
@@ -7,53 +7,81 @@
   Synopsis    [Functions to manipulate covers represented as ZDDs.]
 
   Description [External procedures included in this module:
-            <ul>
-            <li> Cudd_zddProduct();
-            <li> Cudd_zddUnateProduct();
-            <li> Cudd_zddWeakDiv();
-            <li> Cudd_zddWeakDivF();
-            <li> Cudd_zddDivide();
-            <li> Cudd_zddDivideF();
-            <li> Cudd_zddComplement();
-            </ul>
-           Internal procedures included in this module:
-            <ul>
-            <li> cuddZddProduct();
-            <li> cuddZddUnateProduct();
-            <li> cuddZddWeakDiv();
-            <li> cuddZddWeakDivF();
-            <li> cuddZddDivide();
-            <li> cuddZddDivideF();
-            <li> cuddZddGetCofactors3()
-            <li> cuddZddGetCofactors2()
-            <li> cuddZddComplement();
-            <li> cuddZddGetPosVarIndex();
-            <li> cuddZddGetNegVarIndex();
-            <li> cuddZddGetPosVarLevel();
-            <li> cuddZddGetNegVarLevel();
-            </ul>
-           Static procedures included in this module:
-            <ul>
-            </ul>
-          ]
+                    <ul>
+                    <li> Cudd_zddProduct();
+                    <li> Cudd_zddUnateProduct();
+                    <li> Cudd_zddWeakDiv();
+                    <li> Cudd_zddWeakDivF();
+                    <li> Cudd_zddDivide();
+                    <li> Cudd_zddDivideF();
+                    <li> Cudd_zddComplement();
+                    </ul>
+               Internal procedures included in this module:
+                    <ul>
+                    <li> cuddZddProduct();
+                    <li> cuddZddUnateProduct();
+                    <li> cuddZddWeakDiv();
+                    <li> cuddZddWeakDivF();
+                    <li> cuddZddDivide();
+                    <li> cuddZddDivideF();
+                    <li> cuddZddGetCofactors3()
+                    <li> cuddZddGetCofactors2()
+                    <li> cuddZddComplement();
+                    <li> cuddZddGetPosVarIndex();
+                    <li> cuddZddGetNegVarIndex();
+                    <li> cuddZddGetPosVarLevel();
+                    <li> cuddZddGetNegVarLevel();
+                    </ul>
+               Static procedures included in this module:
+                    <ul>
+                    </ul>
+              ]
 
   SeeAlso     []
 
   Author      [In-Ho Moon]
 
-  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.]
 
 ******************************************************************************/
 
-#include    "util_hack.h"
-#include    "cuddInt.h"
+#include "util_hack.h"
+#include "cuddInt.h"
 
 ABC_NAMESPACE_IMPL_START
 
 
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -74,7 +102,7 @@ ABC_NAMESPACE_IMPL_START
 /*---------------------------------------------------------------------------*/
 
 #ifndef lint
-static char rcsid[] DD_UNUSED = "$Id: cuddZddFuncs.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $";
+static char rcsid[] DD_UNUSED = "$Id: cuddZddFuncs.c,v 1.16 2008/04/25 07:39:33 fabio Exp $";
 #endif
 
 /*---------------------------------------------------------------------------*/
@@ -113,17 +141,17 @@ static char rcsid[] DD_UNUSED = "$Id: cuddZddFuncs.c,v 1.1.1.1 2003/02/24 22:23:
   SeeAlso     [Cudd_zddUnateProduct]
 
 ******************************************************************************/
-DdNode    *
+DdNode  *
 Cudd_zddProduct(
   DdManager * dd,
   DdNode * f,
   DdNode * g)
 {
-    DdNode    *res;
+    DdNode      *res;
 
     do {
-    dd->reordered = 0;
-    res = cuddZddProduct(dd, f, g);
+        dd->reordered = 0;
+        res = cuddZddProduct(dd, f, g);
     } while (dd->reordered == 1);
     return(res);
 
@@ -144,17 +172,17 @@ Cudd_zddProduct(
   SeeAlso     [Cudd_zddProduct]
 
 ******************************************************************************/
-DdNode    *
+DdNode  *
 Cudd_zddUnateProduct(
   DdManager * dd,
   DdNode * f,
   DdNode * g)
 {
-    DdNode    *res;
+    DdNode      *res;
 
     do {
-    dd->reordered = 0;
-    res = cuddZddUnateProduct(dd, f, g);
+        dd->reordered = 0;
+        res = cuddZddUnateProduct(dd, f, g);
     } while (dd->reordered == 1);
     return(res);
 
@@ -178,17 +206,17 @@ Cudd_zddUnateProduct(
   SeeAlso     [Cudd_zddDivide]
 
 ******************************************************************************/
-DdNode    *
+DdNode  *
 Cudd_zddWeakDiv(
   DdManager * dd,
   DdNode * f,
   DdNode * g)
 {
-    DdNode    *res;
+    DdNode      *res;
 
     do {
-    dd->reordered = 0;
-    res = cuddZddWeakDiv(dd, f, g);
+        dd->reordered = 0;
+        res = cuddZddWeakDiv(dd, f, g);
     } while (dd->reordered == 1);
     return(res);
 
@@ -209,17 +237,17 @@ Cudd_zddWeakDiv(
   SeeAlso     [Cudd_zddWeakDiv]
 
 ******************************************************************************/
-DdNode    *
+DdNode  *
 Cudd_zddDivide(
   DdManager * dd,
   DdNode * f,
   DdNode * g)
 {
-    DdNode    *res;
+    DdNode      *res;
 
     do {
-    dd->reordered = 0;
-    res = cuddZddDivide(dd, f, g);
+        dd->reordered = 0;
+        res = cuddZddDivide(dd, f, g);
     } while (dd->reordered == 1);
     return(res);
 
@@ -238,17 +266,17 @@ Cudd_zddDivide(
   SeeAlso     [Cudd_zddWeakDiv]
 
 ******************************************************************************/
-DdNode    *
+DdNode  *
 Cudd_zddWeakDivF(
   DdManager * dd,
   DdNode * f,
   DdNode * g)
 {
-    DdNode    *res;
+    DdNode      *res;
 
     do {
-    dd->reordered = 0;
-    res = cuddZddWeakDivF(dd, f, g);
+        dd->reordered = 0;
+        res = cuddZddWeakDivF(dd, f, g);
     } while (dd->reordered == 1);
     return(res);
 
@@ -267,17 +295,17 @@ Cudd_zddWeakDivF(
   SeeAlso     []
 
 ******************************************************************************/
-DdNode    *
+DdNode  *
 Cudd_zddDivideF(
   DdManager * dd,
   DdNode * f,
   DdNode * g)
 {
-    DdNode    *res;
+    DdNode      *res;
 
     do {
-    dd->reordered = 0;
-    res = cuddZddDivideF(dd, f, g);
+        dd->reordered = 0;
+        res = cuddZddDivideF(dd, f, g);
     } while (dd->reordered == 1);
     return(res);
 
@@ -300,26 +328,26 @@ Cudd_zddDivideF(
   SeeAlso     []
 
 ******************************************************************************/
-DdNode    *
+DdNode  *
 Cudd_zddComplement(
   DdManager *dd,
   DdNode *node)
 {
-    DdNode    *b, *isop, *zdd_I;
+    DdNode      *b, *isop, *zdd_I;
 
     /* Check cache */
     zdd_I = cuddCacheLookup1Zdd(dd, cuddZddComplement, node);
     if (zdd_I)
-    return(zdd_I);
+        return(zdd_I);
 
     b = Cudd_MakeBddFromZddCover(dd, node);
     if (!b)
-    return(NULL);
+        return(NULL);
     Cudd_Ref(b);
     isop = Cudd_zddIsop(dd, Cudd_Not(b), Cudd_Not(b), &zdd_I);
     if (!isop) {
-    Cudd_RecursiveDeref(dd, b);
-    return(NULL);
+        Cudd_RecursiveDeref(dd, b);
+        return(NULL);
     }
     Cudd_Ref(isop);
     Cudd_Ref(zdd_I);
@@ -348,21 +376,21 @@ Cudd_zddComplement(
   SeeAlso     [Cudd_zddProduct]
 
 ******************************************************************************/
-DdNode    *
+DdNode  *
 cuddZddProduct(
   DdManager * dd,
   DdNode * f,
   DdNode * g)
 {
-    int        v, top_f, top_g;
-    DdNode    *tmp, *term1, *term2, *term3;
-    DdNode    *f0, *f1, *fd, *g0, *g1, *gd;
-    DdNode    *R0, *R1, *Rd, *N0, *N1;
-    DdNode    *r;
-    DdNode    *one = DD_ONE(dd);
-    DdNode    *zero = DD_ZERO(dd);
-    int        flag;
-    int        pv, nv;
+    int         v, top_f, top_g;
+    DdNode      *tmp, *term1, *term2, *term3;
+    DdNode      *f0, *f1, *fd, *g0, *g1, *gd;
+    DdNode      *R0, *R1, *Rd, *N0, *N1;
+    DdNode      *r;
+    DdNode      *one = DD_ONE(dd);
+    DdNode      *zero = DD_ZERO(dd);
+    int         flag;
+    int         pv, nv;
 
     statLine(dd);
     if (f == zero || g == zero)
@@ -376,26 +404,26 @@ cuddZddProduct(
     top_g = dd->permZ[g->index];
 
     if (top_f > top_g)
-    return(cuddZddProduct(dd, g, f));
+        return(cuddZddProduct(dd, g, f));
 
     /* Check cache */
     r = cuddCacheLookup2Zdd(dd, cuddZddProduct, f, g);
     if (r)
-    return(r);
+        return(r);
 
-    v = f->index;    /* either yi or zi */
+    v = f->index;       /* either yi or zi */
     flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd);
     if (flag == 1)
-    return(NULL);
+        return(NULL);
     Cudd_Ref(f1);
     Cudd_Ref(f0);
     Cudd_Ref(fd);
     flag = cuddZddGetCofactors3(dd, g, v, &g1, &g0, &gd);
     if (flag == 1) {
-    Cudd_RecursiveDerefZdd(dd, f1);
-    Cudd_RecursiveDerefZdd(dd, f0);
-    Cudd_RecursiveDerefZdd(dd, fd);
-    return(NULL);
+        Cudd_RecursiveDerefZdd(dd, f1);
+        Cudd_RecursiveDerefZdd(dd, f0);
+        Cudd_RecursiveDerefZdd(dd, fd);
+        return(NULL);
     }
     Cudd_Ref(g1);
     Cudd_Ref(g0);
@@ -405,95 +433,95 @@ cuddZddProduct(
 
     Rd = cuddZddProduct(dd, fd, gd);
     if (Rd == NULL) {
-    Cudd_RecursiveDerefZdd(dd, f1);
-    Cudd_RecursiveDerefZdd(dd, f0);
-    Cudd_RecursiveDerefZdd(dd, fd);
-    Cudd_RecursiveDerefZdd(dd, g1);
-    Cudd_RecursiveDerefZdd(dd, g0);
-    Cudd_RecursiveDerefZdd(dd, gd);
-    return(NULL);
+        Cudd_RecursiveDerefZdd(dd, f1);
+        Cudd_RecursiveDerefZdd(dd, f0);
+        Cudd_RecursiveDerefZdd(dd, fd);
+        Cudd_RecursiveDerefZdd(dd, g1);
+        Cudd_RecursiveDerefZdd(dd, g0);
+        Cudd_RecursiveDerefZdd(dd, gd);
+        return(NULL);
     }
     Cudd_Ref(Rd);
 
     term1 = cuddZddProduct(dd, f0, g0);
     if (term1 == NULL) {
-    Cudd_RecursiveDerefZdd(dd, f1);
-    Cudd_RecursiveDerefZdd(dd, f0);
-    Cudd_RecursiveDerefZdd(dd, fd);
-    Cudd_RecursiveDerefZdd(dd, g1);
-    Cudd_RecursiveDerefZdd(dd, g0);
-    Cudd_RecursiveDerefZdd(dd, gd);
-    Cudd_RecursiveDerefZdd(dd, Rd);
-    return(NULL);
+        Cudd_RecursiveDerefZdd(dd, f1);
+        Cudd_RecursiveDerefZdd(dd, f0);
+        Cudd_RecursiveDerefZdd(dd, fd);
+        Cudd_RecursiveDerefZdd(dd, g1);
+        Cudd_RecursiveDerefZdd(dd, g0);
+        Cudd_RecursiveDerefZdd(dd, gd);
+        Cudd_RecursiveDerefZdd(dd, Rd);
+        return(NULL);
     }
     Cudd_Ref(term1);
     term2 = cuddZddProduct(dd, f0, gd);
     if (term2 == NULL) {
-    Cudd_RecursiveDerefZdd(dd, f1);
-    Cudd_RecursiveDerefZdd(dd, f0);
-    Cudd_RecursiveDerefZdd(dd, fd);
-    Cudd_RecursiveDerefZdd(dd, g1);
-    Cudd_RecursiveDerefZdd(dd, g0);
-    Cudd_RecursiveDerefZdd(dd, gd);
-    Cudd_RecursiveDerefZdd(dd, Rd);
-    Cudd_RecursiveDerefZdd(dd, term1);
-    return(NULL);
+        Cudd_RecursiveDerefZdd(dd, f1);
+        Cudd_RecursiveDerefZdd(dd, f0);
+        Cudd_RecursiveDerefZdd(dd, fd);
+        Cudd_RecursiveDerefZdd(dd, g1);
+        Cudd_RecursiveDerefZdd(dd, g0);
+        Cudd_RecursiveDerefZdd(dd, gd);
+        Cudd_RecursiveDerefZdd(dd, Rd);
+        Cudd_RecursiveDerefZdd(dd, term1);
+        return(NULL);
     }
     Cudd_Ref(term2);
     term3 = cuddZddProduct(dd, fd, g0);
     if (term3 == NULL) {
-    Cudd_RecursiveDerefZdd(dd, f1);
-    Cudd_RecursiveDerefZdd(dd, f0);
-    Cudd_RecursiveDerefZdd(dd, fd);
-    Cudd_RecursiveDerefZdd(dd, g1);
-    Cudd_RecursiveDerefZdd(dd, g0);
-    Cudd_RecursiveDerefZdd(dd, gd);
-    Cudd_RecursiveDerefZdd(dd, Rd);
-    Cudd_RecursiveDerefZdd(dd, term1);
-    Cudd_RecursiveDerefZdd(dd, term2);
-    return(NULL);
+        Cudd_RecursiveDerefZdd(dd, f1);
+        Cudd_RecursiveDerefZdd(dd, f0);
+        Cudd_RecursiveDerefZdd(dd, fd);
+        Cudd_RecursiveDerefZdd(dd, g1);
+        Cudd_RecursiveDerefZdd(dd, g0);
+        Cudd_RecursiveDerefZdd(dd, gd);
+        Cudd_RecursiveDerefZdd(dd, Rd);
+        Cudd_RecursiveDerefZdd(dd, term1);
+        Cudd_RecursiveDerefZdd(dd, term2);
+        return(NULL);
     }
     Cudd_Ref(term3);
     Cudd_RecursiveDerefZdd(dd, f0);
     Cudd_RecursiveDerefZdd(dd, g0);
     tmp = cuddZddUnion(dd, term1, term2);
     if (tmp == NULL) {
-    Cudd_RecursiveDerefZdd(dd, f1);
-    Cudd_RecursiveDerefZdd(dd, fd);
-    Cudd_RecursiveDerefZdd(dd, g1);
-    Cudd_RecursiveDerefZdd(dd, gd);
-    Cudd_RecursiveDerefZdd(dd, Rd);
-    Cudd_RecursiveDerefZdd(dd, term1);
-    Cudd_RecursiveDerefZdd(dd, term2);
-    Cudd_RecursiveDerefZdd(dd, term3);
-    return(NULL);
+        Cudd_RecursiveDerefZdd(dd, f1);
+        Cudd_RecursiveDerefZdd(dd, fd);
+        Cudd_RecursiveDerefZdd(dd, g1);
+        Cudd_RecursiveDerefZdd(dd, gd);
+        Cudd_RecursiveDerefZdd(dd, Rd);
+        Cudd_RecursiveDerefZdd(dd, term1);
+        Cudd_RecursiveDerefZdd(dd, term2);
+        Cudd_RecursiveDerefZdd(dd, term3);
+        return(NULL);
     }
     Cudd_Ref(tmp);
     Cudd_RecursiveDerefZdd(dd, term1);
     Cudd_RecursiveDerefZdd(dd, term2);
     R0 = cuddZddUnion(dd, tmp, term3);
     if (R0 == NULL) {
-    Cudd_RecursiveDerefZdd(dd, f1);
-    Cudd_RecursiveDerefZdd(dd, fd);
-    Cudd_RecursiveDerefZdd(dd, g1);
-    Cudd_RecursiveDerefZdd(dd, gd);
-    Cudd_RecursiveDerefZdd(dd, Rd);
-    Cudd_RecursiveDerefZdd(dd, term3);
-    Cudd_RecursiveDerefZdd(dd, tmp);
-    return(NULL);
+        Cudd_RecursiveDerefZdd(dd, f1);
+        Cudd_RecursiveDerefZdd(dd, fd);
+        Cudd_RecursiveDerefZdd(dd, g1);
+        Cudd_RecursiveDerefZdd(dd, gd);
+        Cudd_RecursiveDerefZdd(dd, Rd);
+        Cudd_RecursiveDerefZdd(dd, term3);
+        Cudd_RecursiveDerefZdd(dd, tmp);
+        return(NULL);
     }
     Cudd_Ref(R0);
     Cudd_RecursiveDerefZdd(dd, tmp);
     Cudd_RecursiveDerefZdd(dd, term3);
     N0 = cuddZddGetNode(dd, nv, R0, Rd); /* nv = zi */
     if (N0 == NULL) {
-    Cudd_RecursiveDerefZdd(dd, f1);
-    Cudd_RecursiveDerefZdd(dd, fd);
-    Cudd_RecursiveDerefZdd(dd, g1);
-    Cudd_RecursiveDerefZdd(dd, gd);
-    Cudd_RecursiveDerefZdd(dd, Rd);
-    Cudd_RecursiveDerefZdd(dd, R0);
-    return(NULL);
+        Cudd_RecursiveDerefZdd(dd, f1);
+        Cudd_RecursiveDerefZdd(dd, fd);
+        Cudd_RecursiveDerefZdd(dd, g1);
+        Cudd_RecursiveDerefZdd(dd, gd);
+        Cudd_RecursiveDerefZdd(dd, Rd);
+        Cudd_RecursiveDerefZdd(dd, R0);
+        return(NULL);
     }
     Cudd_Ref(N0);
     Cudd_RecursiveDerefZdd(dd, R0);
@@ -501,35 +529,35 @@ cuddZddProduct(
 
     term1 = cuddZddProduct(dd, f1, g1);
     if (term1 == NULL) {
-    Cudd_RecursiveDerefZdd(dd, f1);
-    Cudd_RecursiveDerefZdd(dd, fd);
-    Cudd_RecursiveDerefZdd(dd, g1);
-    Cudd_RecursiveDerefZdd(dd, gd);
-    Cudd_RecursiveDerefZdd(dd, N0);
-    return(NULL);
+        Cudd_RecursiveDerefZdd(dd, f1);
+        Cudd_RecursiveDerefZdd(dd, fd);
+        Cudd_RecursiveDerefZdd(dd, g1);
+        Cudd_RecursiveDerefZdd(dd, gd);
+        Cudd_RecursiveDerefZdd(dd, N0);
+        return(NULL);
     }
     Cudd_Ref(term1);
     term2 = cuddZddProduct(dd, f1, gd);
     if (term2 == NULL) {
-    Cudd_RecursiveDerefZdd(dd, f1);
-    Cudd_RecursiveDerefZdd(dd, fd);
-    Cudd_RecursiveDerefZdd(dd, g1);
-    Cudd_RecursiveDerefZdd(dd, gd);
-    Cudd_RecursiveDerefZdd(dd, N0);
-    Cudd_RecursiveDerefZdd(dd, term1);
-    return(NULL);
+        Cudd_RecursiveDerefZdd(dd, f1);
+        Cudd_RecursiveDerefZdd(dd, fd);
+        Cudd_RecursiveDerefZdd(dd, g1);
+        Cudd_RecursiveDerefZdd(dd, gd);
+        Cudd_RecursiveDerefZdd(dd, N0);
+        Cudd_RecursiveDerefZdd(dd, term1);
+        return(NULL);
     }
     Cudd_Ref(term2);
     term3 = cuddZddProduct(dd, fd, g1);
     if (term3 == NULL) {
-    Cudd_RecursiveDerefZdd(dd, f1);
-    Cudd_RecursiveDerefZdd(dd, fd);
-    Cudd_RecursiveDerefZdd(dd, g1);
-    Cudd_RecursiveDerefZdd(dd, gd);
-    Cudd_RecursiveDerefZdd(dd, N0);
-    Cudd_RecursiveDerefZdd(dd, term1);
-    Cudd_RecursiveDerefZdd(dd, term2);
-    return(NULL);
+        Cudd_RecursiveDerefZdd(dd, f1);
+        Cudd_RecursiveDerefZdd(dd, fd);
+        Cudd_RecursiveDerefZdd(dd, g1);
+        Cudd_RecursiveDerefZdd(dd, gd);
+        Cudd_RecursiveDerefZdd(dd, N0);
+        Cudd_RecursiveDerefZdd(dd, term1);
+        Cudd_RecursiveDerefZdd(dd, term2);
+        return(NULL);
     }
     Cudd_Ref(term3);
     Cudd_RecursiveDerefZdd(dd, f1);
@@ -538,30 +566,30 @@ cuddZddProduct(
     Cudd_RecursiveDerefZdd(dd, gd);
     tmp = cuddZddUnion(dd, term1, term2);
     if (tmp == NULL) {
-    Cudd_RecursiveDerefZdd(dd, N0);
-    Cudd_RecursiveDerefZdd(dd, term1);
-    Cudd_RecursiveDerefZdd(dd, term2);
-    Cudd_RecursiveDerefZdd(dd, term3);
-    return(NULL);
+        Cudd_RecursiveDerefZdd(dd, N0);
+        Cudd_RecursiveDerefZdd(dd, term1);
+        Cudd_RecursiveDerefZdd(dd, term2);
+        Cudd_RecursiveDerefZdd(dd, term3);
+        return(NULL);
     }
     Cudd_Ref(tmp);
     Cudd_RecursiveDerefZdd(dd, term1);
     Cudd_RecursiveDerefZdd(dd, term2);
     R1 = cuddZddUnion(dd, tmp, term3);
     if (R1 == NULL) {
-    Cudd_RecursiveDerefZdd(dd, N0);
-    Cudd_RecursiveDerefZdd(dd, term3);
-    Cudd_RecursiveDerefZdd(dd, tmp);
-    return(NULL);
+        Cudd_RecursiveDerefZdd(dd, N0);
+        Cudd_RecursiveDerefZdd(dd, term3);
+        Cudd_RecursiveDerefZdd(dd, tmp);
+        return(NULL);
     }
     Cudd_Ref(R1);
     Cudd_RecursiveDerefZdd(dd, tmp);
     Cudd_RecursiveDerefZdd(dd, term3);
     N1 = cuddZddGetNode(dd, pv, R1, N0); /* pv = yi */
     if (N1 == NULL) {
-    Cudd_RecursiveDerefZdd(dd, N0);
-    Cudd_RecursiveDerefZdd(dd, R1);
-    return(NULL);
+        Cudd_RecursiveDerefZdd(dd, N0);
+        Cudd_RecursiveDerefZdd(dd, R1);
+        return(NULL);
     }
     Cudd_Ref(N1);
     Cudd_RecursiveDerefZdd(dd, R1);
@@ -585,20 +613,20 @@ cuddZddProduct(
   SeeAlso     [Cudd_zddUnateProduct]
 
 ******************************************************************************/
-DdNode    *
+DdNode  *
 cuddZddUnateProduct(
   DdManager * dd,
   DdNode * f,
   DdNode * g)
 {
-    int        v, top_f, top_g;
-    DdNode    *term1, *term2, *term3, *term4;
-    DdNode    *sum1, *sum2;
-    DdNode    *f0, *f1, *g0, *g1;
-    DdNode    *r;
-    DdNode    *one = DD_ONE(dd);
-    DdNode    *zero = DD_ZERO(dd);
-    int        flag;
+    int         v, top_f, top_g;
+    DdNode      *term1, *term2, *term3, *term4;
+    DdNode      *sum1, *sum2;
+    DdNode      *f0, *f1, *g0, *g1;
+    DdNode      *r;
+    DdNode      *one = DD_ONE(dd);
+    DdNode      *zero = DD_ZERO(dd);
+    int         flag;
 
     statLine(dd);
     if (f == zero || g == zero)
@@ -612,68 +640,68 @@ cuddZddUnateProduct(
     top_g = dd->permZ[g->index];
 
     if (top_f > top_g)
-    return(cuddZddUnateProduct(dd, g, f));
+        return(cuddZddUnateProduct(dd, g, f));
 
     /* Check cache */
     r = cuddCacheLookup2Zdd(dd, cuddZddUnateProduct, f, g);
     if (r)
-    return(r);
+        return(r);
 
-    v = f->index;    /* either yi or zi */
+    v = f->index;       /* either yi or zi */
     flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0);
     if (flag == 1)
-    return(NULL);
+        return(NULL);
     Cudd_Ref(f1);
     Cudd_Ref(f0);
     flag = cuddZddGetCofactors2(dd, g, v, &g1, &g0);
     if (flag == 1) {
-    Cudd_RecursiveDerefZdd(dd, f1);
-    Cudd_RecursiveDerefZdd(dd, f0);
-    return(NULL);
+        Cudd_RecursiveDerefZdd(dd, f1);
+        Cudd_RecursiveDerefZdd(dd, f0);
+        return(NULL);
     }
     Cudd_Ref(g1);
     Cudd_Ref(g0);
 
     term1 = cuddZddUnateProduct(dd, f1, g1);
     if (term1 == NULL) {
-    Cudd_RecursiveDerefZdd(dd, f1);
-    Cudd_RecursiveDerefZdd(dd, f0);
-    Cudd_RecursiveDerefZdd(dd, g1);
-    Cudd_RecursiveDerefZdd(dd, g0);
-    return(NULL);
+        Cudd_RecursiveDerefZdd(dd, f1);
+        Cudd_RecursiveDerefZdd(dd, f0);
+        Cudd_RecursiveDerefZdd(dd, g1);
+        Cudd_RecursiveDerefZdd(dd, g0);
+        return(NULL);
     }
     Cudd_Ref(term1);
     term2 = cuddZddUnateProduct(dd, f1, g0);
     if (term2 == NULL) {
-    Cudd_RecursiveDerefZdd(dd, f1);
-    Cudd_RecursiveDerefZdd(dd, f0);
-    Cudd_RecursiveDerefZdd(dd, g1);
-    Cudd_RecursiveDerefZdd(dd, g0);
-    Cudd_RecursiveDerefZdd(dd, term1);
-    return(NULL);
+        Cudd_RecursiveDerefZdd(dd, f1);
+        Cudd_RecursiveDerefZdd(dd, f0);
+        Cudd_RecursiveDerefZdd(dd, g1);
+        Cudd_RecursiveDerefZdd(dd, g0);
+        Cudd_RecursiveDerefZdd(dd, term1);
+        return(NULL);
     }
     Cudd_Ref(term2);
     term3 = cuddZddUnateProduct(dd, f0, g1);
     if (term3 == NULL) {
-    Cudd_RecursiveDerefZdd(dd, f1);
-    Cudd_RecursiveDerefZdd(dd, f0);
-    Cudd_RecursiveDerefZdd(dd, g1);
-    Cudd_RecursiveDerefZdd(dd, g0);
-    Cudd_RecursiveDerefZdd(dd, term1);
-    Cudd_RecursiveDerefZdd(dd, term2);
-    return(NULL);
+        Cudd_RecursiveDerefZdd(dd, f1);
+        Cudd_RecursiveDerefZdd(dd, f0);
+        Cudd_RecursiveDerefZdd(dd, g1);
+        Cudd_RecursiveDerefZdd(dd, g0);
+        Cudd_RecursiveDerefZdd(dd, term1);
+        Cudd_RecursiveDerefZdd(dd, term2);
+        return(NULL);
     }
     Cudd_Ref(term3);
     term4 = cuddZddUnateProduct(dd, f0, g0);
     if (term4 == NULL) {
-    Cudd_RecursiveDerefZdd(dd, f1);
-    Cudd_RecursiveDerefZdd(dd, f0);
-    Cudd_RecursiveDerefZdd(dd, g1);
-    Cudd_RecursiveDerefZdd(dd, g0);
-    Cudd_RecursiveDerefZdd(dd, term1);
-    Cudd_RecursiveDerefZdd(dd, term2);
-    Cudd_RecursiveDerefZdd(dd, term3);
-    return(NULL);
+        Cudd_RecursiveDerefZdd(dd, f1);
+        Cudd_RecursiveDerefZdd(dd, f0);
+        Cudd_RecursiveDerefZdd(dd, g1);
+        Cudd_RecursiveDerefZdd(dd, g0);
+        Cudd_RecursiveDerefZdd(dd, term1);
+        Cudd_RecursiveDerefZdd(dd, term2);
+        Cudd_RecursiveDerefZdd(dd, term3);
+        return(NULL);
     }
     Cudd_Ref(term4);
     Cudd_RecursiveDerefZdd(dd, f1);
@@ -682,30 +710,30 @@ cuddZddUnateProduct(
     Cudd_RecursiveDerefZdd(dd, g0);
     sum1 = cuddZddUnion(dd, term1, term2);
     if (sum1 == NULL) {
-    Cudd_RecursiveDerefZdd(dd, term1);
-    Cudd_RecursiveDerefZdd(dd, term2);
-    Cudd_RecursiveDerefZdd(dd, term3);
-    Cudd_RecursiveDerefZdd(dd, term4);
-    return(NULL);
+        Cudd_RecursiveDerefZdd(dd, term1);
+        Cudd_RecursiveDerefZdd(dd, term2);
+        Cudd_RecursiveDerefZdd(dd, term3);
+        Cudd_RecursiveDerefZdd(dd, term4);
+        return(NULL);
     }
     Cudd_Ref(sum1);
     Cudd_RecursiveDerefZdd(dd, term1);
     Cudd_RecursiveDerefZdd(dd, term2);
     sum2 = cuddZddUnion(dd, sum1, term3);
     if (sum2 == NULL) {
-    Cudd_RecursiveDerefZdd(dd, term3);
-    Cudd_RecursiveDerefZdd(dd, term4);
-    Cudd_RecursiveDerefZdd(dd, sum1);
-    return(NULL);
+        Cudd_RecursiveDerefZdd(dd, term3);
+        Cudd_RecursiveDerefZdd(dd, term4);
+        Cudd_RecursiveDerefZdd(dd, sum1);
+        return(NULL);
     }
     Cudd_Ref(sum2);
     Cudd_RecursiveDerefZdd(dd, sum1);
     Cudd_RecursiveDerefZdd(dd, term3);
     r = cuddZddGetNode(dd, v, sum2, term4);
     if (r == NULL) {
-    Cudd_RecursiveDerefZdd(dd, term4);
-    Cudd_RecursiveDerefZdd(dd, sum2);
-    return(NULL);
+        Cudd_RecursiveDerefZdd(dd, term4);
+        Cudd_RecursiveDerefZdd(dd, sum2);
+        return(NULL);
     }
     Cudd_Ref(r);
     Cudd_RecursiveDerefZdd(dd, sum2);
@@ -729,47 +757,47 @@ cuddZddUnateProduct(
   SeeAlso     [Cudd_zddWeakDiv]
 
 ******************************************************************************/
-DdNode    *
+DdNode  *
 cuddZddWeakDiv(
   DdManager * dd,
   DdNode * f,
   DdNode * g)
 {
-    int        v;
-    DdNode    *one = DD_ONE(dd);
-    DdNode    *zero = DD_ZERO(dd);
-    DdNode    *f0, *f1, *fd, *g0, *g1, *gd;
-    DdNode    *q, *tmp;
-    DdNode    *r;
-    int        flag;
+    int         v;
+    DdNode      *one = DD_ONE(dd);
+    DdNode      *zero = DD_ZERO(dd);
+    DdNode      *f0, *f1, *fd, *g0, *g1, *gd;
+    DdNode      *q, *tmp;
+    DdNode      *r;
+    int         flag;
 
     statLine(dd);
     if (g == one)
-    return(f);
+        return(f);
     if (f == zero || f == one)
-    return(zero);
+        return(zero);
     if (f == g)
-    return(one);
+        return(one);
 
     /* Check cache. */
     r = cuddCacheLookup2Zdd(dd, cuddZddWeakDiv, f, g);
     if (r)
-    return(r);
+        return(r);
 
     v = g->index;
 
     flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd);
     if (flag == 1)
-    return(NULL);
+        return(NULL);
     Cudd_Ref(f1);
     Cudd_Ref(f0);
     Cudd_Ref(fd);
     flag = cuddZddGetCofactors3(dd, g, v, &g1, &g0, &gd);
     if (flag == 1) {
-    Cudd_RecursiveDerefZdd(dd, f1);
-    Cudd_RecursiveDerefZdd(dd, f0);
-    Cudd_RecursiveDerefZdd(dd, fd);
-    return(NULL);
+        Cudd_RecursiveDerefZdd(dd, f1);
+        Cudd_RecursiveDerefZdd(dd, f0);
+        Cudd_RecursiveDerefZdd(dd, fd);
+        return(NULL);
     }
     Cudd_Ref(g1);
     Cudd_Ref(g0);
@@ -778,98 +806,98 @@ cuddZddWeakDiv(
     q = g;
 
     if (g0 != zero) {
-    q = cuddZddWeakDiv(dd, f0, g0);
-    if (q == NULL) {
-        Cudd_RecursiveDerefZdd(dd, f1);
-        Cudd_RecursiveDerefZdd(dd, f0);
-        Cudd_RecursiveDerefZdd(dd, fd);
-        Cudd_RecursiveDerefZdd(dd, g1);
-        Cudd_RecursiveDerefZdd(dd, g0);
-        Cudd_RecursiveDerefZdd(dd, gd);
-        return(NULL);
-    }
-    Cudd_Ref(q);
+        q = cuddZddWeakDiv(dd, f0, g0);
+        if (q == NULL) {
+            Cudd_RecursiveDerefZdd(dd, f1);
+            Cudd_RecursiveDerefZdd(dd, f0);
+            Cudd_RecursiveDerefZdd(dd, fd);
+            Cudd_RecursiveDerefZdd(dd, g1);
+            Cudd_RecursiveDerefZdd(dd, g0);
+            Cudd_RecursiveDerefZdd(dd, gd);
+            return(NULL);
+        }
+        Cudd_Ref(q);
     }
     else
-    Cudd_Ref(q);
+        Cudd_Ref(q);
     Cudd_RecursiveDerefZdd(dd, f0);
     Cudd_RecursiveDerefZdd(dd, g0);
 
     if (q == zero) {
-    Cudd_RecursiveDerefZdd(dd, f1);
-    Cudd_RecursiveDerefZdd(dd, g1);
-    Cudd_RecursiveDerefZdd(dd, fd);
-    Cudd_RecursiveDerefZdd(dd, gd);
-    cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, zero);
-    Cudd_Deref(q);
-    return(zero);
-    }
-
-    if (g1 != zero) {
-    Cudd_RecursiveDerefZdd(dd, q);
-    tmp = cuddZddWeakDiv(dd, f1, g1);
-    if (tmp == NULL) {
         Cudd_RecursiveDerefZdd(dd, f1);
         Cudd_RecursiveDerefZdd(dd, g1);
         Cudd_RecursiveDerefZdd(dd, fd);
         Cudd_RecursiveDerefZdd(dd, gd);
-        return(NULL);
+        cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, zero);
+        Cudd_Deref(q);
+        return(zero);
     }
-    Cudd_Ref(tmp);
-    Cudd_RecursiveDerefZdd(dd, f1);
-    Cudd_RecursiveDerefZdd(dd, g1);
-    if (q == g)
-        q = tmp;
-    else {
-        q = cuddZddIntersect(dd, q, tmp);
-        if (q == NULL) {
-        Cudd_RecursiveDerefZdd(dd, fd);
-        Cudd_RecursiveDerefZdd(dd, gd);
-        return(NULL);
+
+    if (g1 != zero) {
+        Cudd_RecursiveDerefZdd(dd, q);
+        tmp = cuddZddWeakDiv(dd, f1, g1);
+        if (tmp == NULL) {
+            Cudd_RecursiveDerefZdd(dd, f1);
+            Cudd_RecursiveDerefZdd(dd, g1);
+            Cudd_RecursiveDerefZdd(dd, fd);
+            Cudd_RecursiveDerefZdd(dd, gd);
+            return(NULL);
+        }
+        Cudd_Ref(tmp);
+        Cudd_RecursiveDerefZdd(dd, f1);
+        Cudd_RecursiveDerefZdd(dd, g1);
+        if (q == g)
+            q = tmp;
+        else {
+            q = cuddZddIntersect(dd, q, tmp);
+            if (q == NULL) {
+                Cudd_RecursiveDerefZdd(dd, fd);
+                Cudd_RecursiveDerefZdd(dd, gd);
+                return(NULL);
+            }
+            Cudd_Ref(q);
+            Cudd_RecursiveDerefZdd(dd, tmp);
         }
-        Cudd_Ref(q);
-        Cudd_RecursiveDerefZdd(dd, tmp);
-    }
     }
     else {
-    Cudd_RecursiveDerefZdd(dd, f1);
-    Cudd_RecursiveDerefZdd(dd, g1);
+        Cudd_RecursiveDerefZdd(dd, f1);
+        Cudd_RecursiveDerefZdd(dd, g1);
     }
 
     if (q == zero) {
-    Cudd_RecursiveDerefZdd(dd, fd);
-    Cudd_RecursiveDerefZdd(dd, gd);
-    cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, zero);
-    Cudd_Deref(q);
-    return(zero);
+        Cudd_RecursiveDerefZdd(dd, fd);
+        Cudd_RecursiveDerefZdd(dd, gd);
+        cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, zero);
+        Cudd_Deref(q);
+        return(zero);
     }
 
     if (gd != zero) {
-    Cudd_RecursiveDerefZdd(dd, q);
-    tmp = cuddZddWeakDiv(dd, fd, gd);
-    if (tmp == NULL) {
+        Cudd_RecursiveDerefZdd(dd, q);
+        tmp = cuddZddWeakDiv(dd, fd, gd);
+        if (tmp == NULL) {
+            Cudd_RecursiveDerefZdd(dd, fd);
+            Cudd_RecursiveDerefZdd(dd, gd);
+            return(NULL);
+        }
+        Cudd_Ref(tmp);
         Cudd_RecursiveDerefZdd(dd, fd);
         Cudd_RecursiveDerefZdd(dd, gd);
-        return(NULL);
-    }
-    Cudd_Ref(tmp);
-    Cudd_RecursiveDerefZdd(dd, fd);
-    Cudd_RecursiveDerefZdd(dd, gd);
-    if (q == g)
-        q = tmp;
-    else {
-        q = cuddZddIntersect(dd, q, tmp);
-        if (q == NULL) {
-        Cudd_RecursiveDerefZdd(dd, tmp);
-        return(NULL);
+        if (q == g)
+            q = tmp;
+        else {
+            q = cuddZddIntersect(dd, q, tmp);
+            if (q == NULL) {
+                Cudd_RecursiveDerefZdd(dd, tmp);
+                return(NULL);
+            }
+            Cudd_Ref(q);
+            Cudd_RecursiveDerefZdd(dd, tmp);
         }
-        Cudd_Ref(q);
-        Cudd_RecursiveDerefZdd(dd, tmp);
-    }
     }
     else {
-    Cudd_RecursiveDerefZdd(dd, fd);
-    Cudd_RecursiveDerefZdd(dd, gd);
+        Cudd_RecursiveDerefZdd(dd, fd);
+        Cudd_RecursiveDerefZdd(dd, gd);
     }
 
     cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, q);
@@ -890,34 +918,34 @@ cuddZddWeakDiv(
   SeeAlso     [Cudd_zddWeakDivF]
 
 ******************************************************************************/
-DdNode    *
+DdNode  *
 cuddZddWeakDivF(
   DdManager * dd,
   DdNode * f,
   DdNode * g)
 {
-    int        v, top_f, top_g, vf, vg;
-    DdNode    *one = DD_ONE(dd);
-    DdNode    *zero = DD_ZERO(dd);
-    DdNode    *f0, *f1, *fd, *g0, *g1, *gd;
-    DdNode    *q, *tmp;
-    DdNode    *r;
-    DdNode    *term1, *term0, *termd;
-    int        flag;
-    int        pv, nv;
+    int         v, top_f, top_g, vf, vg;
+    DdNode      *one = DD_ONE(dd);
+    DdNode      *zero = DD_ZERO(dd);
+    DdNode      *f0, *f1, *fd, *g0, *g1, *gd;
+    DdNode      *q, *tmp;
+    DdNode      *r;
+    DdNode      *term1, *term0, *termd;
+    int         flag;
+    int         pv, nv;
 
     statLine(dd);
     if (g == one)
-    return(f);
+        return(f);
     if (f == zero || f == one)
-    return(zero);
+        return(zero);
     if (f == g)
-    return(one);
+        return(one);
 
     /* Check cache. */
     r = cuddCacheLookup2Zdd(dd, cuddZddWeakDivF, f, g);
     if (r)
-    return(r);
+        return(r);
 
     top_f = dd->permZ[f->index];
     top_g = dd->permZ[g->index];
@@ -926,87 +954,87 @@ cuddZddWeakDivF(
     v = ddMin(top_f, top_g);
 
     if (v == top_f && vf < vg) {
-    v = f->index;
-    flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd);
-    if (flag == 1)
-        return(NULL);
-    Cudd_Ref(f1);
-    Cudd_Ref(f0);
-    Cudd_Ref(fd);
-
-    pv = cuddZddGetPosVarIndex(dd, v);
-    nv = cuddZddGetNegVarIndex(dd, v);
-
-    term1 = cuddZddWeakDivF(dd, f1, g);
-    if (term1 == NULL) {
+        v = f->index;
+        flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd);
+        if (flag == 1)
+            return(NULL);
+        Cudd_Ref(f1);
+        Cudd_Ref(f0);
+        Cudd_Ref(fd);
+
+        pv = cuddZddGetPosVarIndex(dd, v);
+        nv = cuddZddGetNegVarIndex(dd, v);
+
+        term1 = cuddZddWeakDivF(dd, f1, g);
+        if (term1 == NULL) {
+            Cudd_RecursiveDerefZdd(dd, f1);
+            Cudd_RecursiveDerefZdd(dd, f0);
+            Cudd_RecursiveDerefZdd(dd, fd);
+            return(NULL);
+        }
+        Cudd_Ref(term1);
         Cudd_RecursiveDerefZdd(dd, f1);
+        term0 = cuddZddWeakDivF(dd, f0, g);
+        if (term0 == NULL) {
+            Cudd_RecursiveDerefZdd(dd, f0);
+            Cudd_RecursiveDerefZdd(dd, fd);
+            Cudd_RecursiveDerefZdd(dd, term1);
+            return(NULL);
+        }
+        Cudd_Ref(term0);
         Cudd_RecursiveDerefZdd(dd, f0);
+        termd = cuddZddWeakDivF(dd, fd, g);
+        if (termd == NULL) {
+            Cudd_RecursiveDerefZdd(dd, fd);
+            Cudd_RecursiveDerefZdd(dd, term1);
+            Cudd_RecursiveDerefZdd(dd, term0);
+            return(NULL);
+        }
+        Cudd_Ref(termd);
         Cudd_RecursiveDerefZdd(dd, fd);
-        return(NULL);
-    }
-    Cudd_Ref(term1);
-    Cudd_RecursiveDerefZdd(dd, f1);
-    term0 = cuddZddWeakDivF(dd, f0, g);
-    if (term0 == NULL) {
-        Cudd_RecursiveDerefZdd(dd, f0);
-        Cudd_RecursiveDerefZdd(dd, fd);
-        Cudd_RecursiveDerefZdd(dd, term1);
-        return(NULL);
-    }
-    Cudd_Ref(term0);
-    Cudd_RecursiveDerefZdd(dd, f0);
-    termd = cuddZddWeakDivF(dd, fd, g);
-    if (termd == NULL) {
-        Cudd_RecursiveDerefZdd(dd, fd);
-        Cudd_RecursiveDerefZdd(dd, term1);
-        Cudd_RecursiveDerefZdd(dd, term0);
-        return(NULL);
-    }
-    Cudd_Ref(termd);
-    Cudd_RecursiveDerefZdd(dd, fd);
 
-    tmp = cuddZddGetNode(dd, nv, term0, termd); /* nv = zi */
-    if (tmp == NULL) {
-        Cudd_RecursiveDerefZdd(dd, term1);
+        tmp = cuddZddGetNode(dd, nv, term0, termd); /* nv = zi */
+        if (tmp == NULL) {
+            Cudd_RecursiveDerefZdd(dd, term1);
+            Cudd_RecursiveDerefZdd(dd, term0);
+            Cudd_RecursiveDerefZdd(dd, termd);
+            return(NULL);
+        }
+        Cudd_Ref(tmp);
         Cudd_RecursiveDerefZdd(dd, term0);
         Cudd_RecursiveDerefZdd(dd, termd);
-        return(NULL);
-    }
-    Cudd_Ref(tmp);
-    Cudd_RecursiveDerefZdd(dd, term0);
-    Cudd_RecursiveDerefZdd(dd, termd);
-    q = cuddZddGetNode(dd, pv, term1, tmp); /* pv = yi */
-    if (q == NULL) {
+        q = cuddZddGetNode(dd, pv, term1, tmp); /* pv = yi */
+        if (q == NULL) {
+            Cudd_RecursiveDerefZdd(dd, term1);
+            Cudd_RecursiveDerefZdd(dd, tmp);
+            return(NULL);
+        }
+        Cudd_Ref(q);
         Cudd_RecursiveDerefZdd(dd, term1);
         Cudd_RecursiveDerefZdd(dd, tmp);
-        return(NULL);
-    }
-    Cudd_Ref(q);
-    Cudd_RecursiveDerefZdd(dd, term1);
-    Cudd_RecursiveDerefZdd(dd, tmp);
 
-    cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, q);
-    Cudd_Deref(q);
-    return(q);
+        cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, q);
+        Cudd_Deref(q);
+        return(q);
     }
 
     if (v == top_f)
-    v = f->index;
+        v = f->index;
     else
-    v = g->index;
+        v = g->index;
 
     flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd);
     if (flag == 1)
-    return(NULL);
+        return(NULL);
     Cudd_Ref(f1);
     Cudd_Ref(f0);
     Cudd_Ref(fd);
     flag = cuddZddGetCofactors3(dd, g, v, &g1, &g0, &gd);
     if (flag == 1) {
-    Cudd_RecursiveDerefZdd(dd, f1);
-    Cudd_RecursiveDerefZdd(dd, f0);
-    Cudd_RecursiveDerefZdd(dd, fd);
-    return(NULL);
+        Cudd_RecursiveDerefZdd(dd, f1);
+        Cudd_RecursiveDerefZdd(dd, f0);
+        Cudd_RecursiveDerefZdd(dd, fd);
+        return(NULL);
     }
     Cudd_Ref(g1);
     Cudd_Ref(g0);
@@ -1015,98 +1043,98 @@ cuddZddWeakDivF(
     q = g;
 
     if (g0 != zero) {
-    q = cuddZddWeakDivF(dd, f0, g0);
-    if (q == NULL) {
-        Cudd_RecursiveDerefZdd(dd, f1);
-        Cudd_RecursiveDerefZdd(dd, f0);
-        Cudd_RecursiveDerefZdd(dd, fd);
-        Cudd_RecursiveDerefZdd(dd, g1);
-        Cudd_RecursiveDerefZdd(dd, g0);
-        Cudd_RecursiveDerefZdd(dd, gd);
-        return(NULL);
-    }
-    Cudd_Ref(q);
+        q = cuddZddWeakDivF(dd, f0, g0);
+        if (q == NULL) {
+            Cudd_RecursiveDerefZdd(dd, f1);
+            Cudd_RecursiveDerefZdd(dd, f0);
+            Cudd_RecursiveDerefZdd(dd, fd);
+            Cudd_RecursiveDerefZdd(dd, g1);
+            Cudd_RecursiveDerefZdd(dd, g0);
+            Cudd_RecursiveDerefZdd(dd, gd);
+            return(NULL);
+        }
+        Cudd_Ref(q);
     }
     else
-    Cudd_Ref(q);
+        Cudd_Ref(q);
     Cudd_RecursiveDerefZdd(dd, f0);
     Cudd_RecursiveDerefZdd(dd, g0);
 
     if (q == zero) {
-    Cudd_RecursiveDerefZdd(dd, f1);
-    Cudd_RecursiveDerefZdd(dd, g1);
-    Cudd_RecursiveDerefZdd(dd, fd);
-    Cudd_RecursiveDerefZdd(dd, gd);
-    cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, zero);
-    Cudd_Deref(q);
-    return(zero);
-    }
-
-    if (g1 != zero) {
-    Cudd_RecursiveDerefZdd(dd, q);
-    tmp = cuddZddWeakDivF(dd, f1, g1);
-    if (tmp == NULL) {
         Cudd_RecursiveDerefZdd(dd, f1);
         Cudd_RecursiveDerefZdd(dd, g1);
         Cudd_RecursiveDerefZdd(dd, fd);
         Cudd_RecursiveDerefZdd(dd, gd);
-        return(NULL);
+        cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, zero);
+        Cudd_Deref(q);
+        return(zero);
     }
-    Cudd_Ref(tmp);
-    Cudd_RecursiveDerefZdd(dd, f1);
-    Cudd_RecursiveDerefZdd(dd, g1);
-    if (q == g)
-        q = tmp;
-    else {
-        q = cuddZddIntersect(dd, q, tmp);
-        if (q == NULL) {
-        Cudd_RecursiveDerefZdd(dd, fd);
-        Cudd_RecursiveDerefZdd(dd, gd);
-        return(NULL);
+
+    if (g1 != zero) {
+        Cudd_RecursiveDerefZdd(dd, q);
+        tmp = cuddZddWeakDivF(dd, f1, g1);
+        if (tmp == NULL) {
+            Cudd_RecursiveDerefZdd(dd, f1);
+            Cudd_RecursiveDerefZdd(dd, g1);
+            Cudd_RecursiveDerefZdd(dd, fd);
+            Cudd_RecursiveDerefZdd(dd, gd);
+            return(NULL);
+        }
+        Cudd_Ref(tmp);
+        Cudd_RecursiveDerefZdd(dd, f1);
+        Cudd_RecursiveDerefZdd(dd, g1);
+        if (q == g)
+            q = tmp;
+        else {
+            q = cuddZddIntersect(dd, q, tmp);
+            if (q == NULL) {
+                Cudd_RecursiveDerefZdd(dd, fd);
+                Cudd_RecursiveDerefZdd(dd, gd);
+                return(NULL);
+            }
+            Cudd_Ref(q);
+            Cudd_RecursiveDerefZdd(dd, tmp);
         }
-        Cudd_Ref(q);
-        Cudd_RecursiveDerefZdd(dd, tmp);
-    }
     }
     else {
-    Cudd_RecursiveDerefZdd(dd, f1);
-    Cudd_RecursiveDerefZdd(dd, g1);
+        Cudd_RecursiveDerefZdd(dd, f1);
+        Cudd_RecursiveDerefZdd(dd, g1);
     }
 
     if (q == zero) {
-    Cudd_RecursiveDerefZdd(dd, fd);
-    Cudd_RecursiveDerefZdd(dd, gd);
-    cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, zero);
-    Cudd_Deref(q);
-    return(zero);
+        Cudd_RecursiveDerefZdd(dd, fd);
+        Cudd_RecursiveDerefZdd(dd, gd);
+        cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, zero);
+        Cudd_Deref(q);
+        return(zero);
     }
 
     if (gd != zero) {
-    Cudd_RecursiveDerefZdd(dd, q);
-    tmp = cuddZddWeakDivF(dd, fd, gd);
-    if (tmp == NULL) {
+        Cudd_RecursiveDerefZdd(dd, q);
+        tmp = cuddZddWeakDivF(dd, fd, gd);
+        if (tmp == NULL) {
+            Cudd_RecursiveDerefZdd(dd, fd);
+            Cudd_RecursiveDerefZdd(dd, gd);
+            return(NULL);
+        }
+        Cudd_Ref(tmp);
         Cudd_RecursiveDerefZdd(dd, fd);
         Cudd_RecursiveDerefZdd(dd, gd);
-        return(NULL);
-    }
-    Cudd_Ref(tmp);
-    Cudd_RecursiveDerefZdd(dd, fd);
-    Cudd_RecursiveDerefZdd(dd, gd);
-    if (q == g)
-        q = tmp;
-    else {
-        q = cuddZddIntersect(dd, q, tmp);
-        if (q == NULL) {
-        Cudd_RecursiveDerefZdd(dd, tmp);
-        return(NULL);
+        if (q == g)
+            q = tmp;
+        else {
+            q = cuddZddIntersect(dd, q, tmp);
+            if (q == NULL) {
+                Cudd_RecursiveDerefZdd(dd, tmp);
+                return(NULL);
+            }
+            Cudd_Ref(q);
+            Cudd_RecursiveDerefZdd(dd, tmp);
         }
-        Cudd_Ref(q);
-        Cudd_RecursiveDerefZdd(dd, tmp);
-    }
     }
     else {
-    Cudd_RecursiveDerefZdd(dd, fd);
-    Cudd_RecursiveDerefZdd(dd, gd);
+        Cudd_RecursiveDerefZdd(dd, fd);
+        Cudd_RecursiveDerefZdd(dd, gd);
     }
 
     cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, q);
@@ -1127,81 +1155,81 @@ cuddZddWeakDivF(
   SeeAlso     [Cudd_zddDivide]
 
 ******************************************************************************/
-DdNode    *
+DdNode  *
 cuddZddDivide(
   DdManager * dd,
   DdNode * f,
   DdNode * g)
 {
-    int        v;
-    DdNode    *one = DD_ONE(dd);
-    DdNode    *zero = DD_ZERO(dd);
-    DdNode    *f0, *f1, *g0, *g1;
-    DdNode    *q, *r, *tmp;
-    int        flag;
+    int         v;
+    DdNode      *one = DD_ONE(dd);
+    DdNode      *zero = DD_ZERO(dd);
+    DdNode      *f0, *f1, *g0, *g1;
+    DdNode      *q, *r, *tmp;
+    int         flag;
 
     statLine(dd);
     if (g == one)
-    return(f);
+        return(f);
     if (f == zero || f == one)
-    return(zero);
+        return(zero);
     if (f == g)
-    return(one);
+        return(one);
 
     /* Check cache. */
     r = cuddCacheLookup2Zdd(dd, cuddZddDivide, f, g);
     if (r)
-    return(r);
+        return(r);
 
     v = g->index;
 
     flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0);
     if (flag == 1)
-    return(NULL);
+        return(NULL);
     Cudd_Ref(f1);
     Cudd_Ref(f0);
     flag = cuddZddGetCofactors2(dd, g, v, &g1, &g0);    /* g1 != zero */
     if (flag == 1) {
-    Cudd_RecursiveDerefZdd(dd, f1);
-    Cudd_RecursiveDerefZdd(dd, f0);
-    return(NULL);
+        Cudd_RecursiveDerefZdd(dd, f1);
+        Cudd_RecursiveDerefZdd(dd, f0);
+        return(NULL);
     }
     Cudd_Ref(g1);
     Cudd_Ref(g0);
 
     r = cuddZddDivide(dd, f1, g1);
     if (r == NULL) {
-    Cudd_RecursiveDerefZdd(dd, f1);
-    Cudd_RecursiveDerefZdd(dd, f0);
-    Cudd_RecursiveDerefZdd(dd, g1);
-    Cudd_RecursiveDerefZdd(dd, g0);
-    return(NULL);
-    }
-    Cudd_Ref(r);
-
-    if (r != zero && g0 != zero) {
-    tmp = r;
-    q = cuddZddDivide(dd, f0, g0);
-    if (q == NULL) {
-        Cudd_RecursiveDerefZdd(dd, f1);
-        Cudd_RecursiveDerefZdd(dd, f0);
-        Cudd_RecursiveDerefZdd(dd, g1);
-        Cudd_RecursiveDerefZdd(dd, g0);
-        return(NULL);
-    }
-    Cudd_Ref(q);
-    r = cuddZddIntersect(dd, r, q);
-    if (r == NULL) {
         Cudd_RecursiveDerefZdd(dd, f1);
         Cudd_RecursiveDerefZdd(dd, f0);
         Cudd_RecursiveDerefZdd(dd, g1);
         Cudd_RecursiveDerefZdd(dd, g0);
-        Cudd_RecursiveDerefZdd(dd, q);
         return(NULL);
     }
     Cudd_Ref(r);
-    Cudd_RecursiveDerefZdd(dd, q);
-    Cudd_RecursiveDerefZdd(dd, tmp);
+
+    if (r != zero && g0 != zero) {
+        tmp = r;
+        q = cuddZddDivide(dd, f0, g0);
+        if (q == NULL) {
+            Cudd_RecursiveDerefZdd(dd, f1);
+            Cudd_RecursiveDerefZdd(dd, f0);
+            Cudd_RecursiveDerefZdd(dd, g1);
+            Cudd_RecursiveDerefZdd(dd, g0);
+            return(NULL);
+        }
+        Cudd_Ref(q);
+        r = cuddZddIntersect(dd, r, q);
+        if (r == NULL) {
+            Cudd_RecursiveDerefZdd(dd, f1);
+            Cudd_RecursiveDerefZdd(dd, f0);
+            Cudd_RecursiveDerefZdd(dd, g1);
+            Cudd_RecursiveDerefZdd(dd, g0);
+            Cudd_RecursiveDerefZdd(dd, q);
+            return(NULL);
+        }
+        Cudd_Ref(r);
+        Cudd_RecursiveDerefZdd(dd, q);
+        Cudd_RecursiveDerefZdd(dd, tmp);
     }
 
     Cudd_RecursiveDerefZdd(dd, f1);
@@ -1227,81 +1255,81 @@ cuddZddDivide(
   SeeAlso     [Cudd_zddDivideF]
 
 ******************************************************************************/
-DdNode    *
+DdNode  *
 cuddZddDivideF(
   DdManager * dd,
   DdNode * f,
   DdNode * g)
 {
-    int        v;
-    DdNode    *one = DD_ONE(dd);
-    DdNode    *zero = DD_ZERO(dd);
-    DdNode    *f0, *f1, *g0, *g1;
-    DdNode    *q, *r, *tmp;
-    int        flag;
+    int         v;
+    DdNode      *one = DD_ONE(dd);
+    DdNode      *zero = DD_ZERO(dd);
+    DdNode      *f0, *f1, *g0, *g1;
+    DdNode      *q, *r, *tmp;
+    int         flag;
 
     statLine(dd);
     if (g == one)
-    return(f);
+        return(f);
     if (f == zero || f == one)
-    return(zero);
+        return(zero);
     if (f == g)
-    return(one);
+        return(one);
 
     /* Check cache. */
     r = cuddCacheLookup2Zdd(dd, cuddZddDivideF, f, g);
     if (r)
-    return(r);
+        return(r);
 
     v = g->index;
 
     flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0);
     if (flag == 1)
-    return(NULL);
+        return(NULL);
     Cudd_Ref(f1);
     Cudd_Ref(f0);
     flag = cuddZddGetCofactors2(dd, g, v, &g1, &g0);    /* g1 != zero */
     if (flag == 1) {
-    Cudd_RecursiveDerefZdd(dd, f1);
-    Cudd_RecursiveDerefZdd(dd, f0);
-    return(NULL);
+        Cudd_RecursiveDerefZdd(dd, f1);
+        Cudd_RecursiveDerefZdd(dd, f0);
+        return(NULL);
     }
     Cudd_Ref(g1);
     Cudd_Ref(g0);
 
     r = cuddZddDivideF(dd, f1, g1);
     if (r == NULL) {
-    Cudd_RecursiveDerefZdd(dd, f1);
-    Cudd_RecursiveDerefZdd(dd, f0);
-    Cudd_RecursiveDerefZdd(dd, g1);
-    Cudd_RecursiveDerefZdd(dd, g0);
-    return(NULL);
-    }
-    Cudd_Ref(r);
-
-    if (r != zero && g0 != zero) {
-    tmp = r;
-    q = cuddZddDivideF(dd, f0, g0);
-    if (q == NULL) {
-        Cudd_RecursiveDerefZdd(dd, f1);
-        Cudd_RecursiveDerefZdd(dd, f0);
-        Cudd_RecursiveDerefZdd(dd, g1);
-        Cudd_RecursiveDerefZdd(dd, g0);
-        return(NULL);
-    }
-    Cudd_Ref(q);
-    r = cuddZddIntersect(dd, r, q);
-    if (r == NULL) {
         Cudd_RecursiveDerefZdd(dd, f1);
         Cudd_RecursiveDerefZdd(dd, f0);
         Cudd_RecursiveDerefZdd(dd, g1);
         Cudd_RecursiveDerefZdd(dd, g0);
-        Cudd_RecursiveDerefZdd(dd, q);
         return(NULL);
     }
     Cudd_Ref(r);
-    Cudd_RecursiveDerefZdd(dd, q);
-    Cudd_RecursiveDerefZdd(dd, tmp);
+
+    if (r != zero && g0 != zero) {
+        tmp = r;
+        q = cuddZddDivideF(dd, f0, g0);
+        if (q == NULL) {
+            Cudd_RecursiveDerefZdd(dd, f1);
+            Cudd_RecursiveDerefZdd(dd, f0);
+            Cudd_RecursiveDerefZdd(dd, g1);
+            Cudd_RecursiveDerefZdd(dd, g0);
+            return(NULL);
+        }
+        Cudd_Ref(q);
+        r = cuddZddIntersect(dd, r, q);
+        if (r == NULL) {
+            Cudd_RecursiveDerefZdd(dd, f1);
+            Cudd_RecursiveDerefZdd(dd, f0);
+            Cudd_RecursiveDerefZdd(dd, g1);
+            Cudd_RecursiveDerefZdd(dd, g0);
+            Cudd_RecursiveDerefZdd(dd, q);
+            return(NULL);
+        }
+        Cudd_Ref(r);
+        Cudd_RecursiveDerefZdd(dd, q);
+        Cudd_RecursiveDerefZdd(dd, tmp);
     }
 
     Cudd_RecursiveDerefZdd(dd, f1);
@@ -1321,7 +1349,7 @@ cuddZddDivideF(
   Synopsis    [Computes the three-way decomposition of f w.r.t. v.]
 
   Description [Computes the three-way decomposition of function f (represented
-  by a ZDD) wit respect to variable v.]
+  by a ZDD) wit respect to variable v.  Returns 0 if successful; 1 otherwise.]
 
   SideEffects [The results are returned in f1, f0, and fd.]
 
@@ -1337,10 +1365,10 @@ cuddZddGetCofactors3(
   DdNode ** f0,
   DdNode ** fd)
 {
-    DdNode    *pc, *nc;
-    DdNode    *zero = DD_ZERO(dd);
-    int        top, hv, ht, pv, nv;
-    int        level;
+    DdNode      *pc, *nc;
+    DdNode      *zero = DD_ZERO(dd);
+    int         top, hv, ht, pv, nv;
+    int         level;
 
     top = dd->permZ[f->index];
     level = dd->permZ[v];
@@ -1348,96 +1376,96 @@ cuddZddGetCofactors3(
     ht = top >> 1;
 
     if (hv < ht) {
-    *f1 = zero;
-    *f0 = zero;
-    *fd = f;
+        *f1 = zero;
+        *f0 = zero;
+        *fd = f;
     }
     else {
-    pv = cuddZddGetPosVarIndex(dd, v);
-    nv = cuddZddGetNegVarIndex(dd, v);
-
-    /* not to create intermediate ZDD node */
-    if (cuddZddGetPosVarLevel(dd, v) < cuddZddGetNegVarLevel(dd, v)) {
-        pc = cuddZddSubset1(dd, f, pv);
-        if (pc == NULL)
-        return(1);
-        Cudd_Ref(pc);
-        nc = cuddZddSubset0(dd, f, pv);
-        if (nc == NULL) {
-        Cudd_RecursiveDerefZdd(dd, pc);
-        return(1);
-        }
-        Cudd_Ref(nc);
-
-        *f1 = cuddZddSubset0(dd, pc, nv);
-        if (*f1 == NULL) {
-        Cudd_RecursiveDerefZdd(dd, pc);
-        Cudd_RecursiveDerefZdd(dd, nc);
-        return(1);
-        }
-        Cudd_Ref(*f1);
-        *f0 = cuddZddSubset1(dd, nc, nv);
-        if (*f0 == NULL) {
-        Cudd_RecursiveDerefZdd(dd, pc);
-        Cudd_RecursiveDerefZdd(dd, nc);
-        Cudd_RecursiveDerefZdd(dd, *f1);
-        return(1);
+        pv = cuddZddGetPosVarIndex(dd, v);
+        nv = cuddZddGetNegVarIndex(dd, v);
+
+        /* not to create intermediate ZDD node */
+        if (cuddZddGetPosVarLevel(dd, v) < cuddZddGetNegVarLevel(dd, v)) {
+            pc = cuddZddSubset1(dd, f, pv);
+            if (pc == NULL)
+                return(1);
+            Cudd_Ref(pc);
+            nc = cuddZddSubset0(dd, f, pv);
+            if (nc == NULL) {
+                Cudd_RecursiveDerefZdd(dd, pc);
+                return(1);
+            }
+            Cudd_Ref(nc);
+
+            *f1 = cuddZddSubset0(dd, pc, nv);
+            if (*f1 == NULL) {
+                Cudd_RecursiveDerefZdd(dd, pc);
+                Cudd_RecursiveDerefZdd(dd, nc);
+                return(1);
+            }
+            Cudd_Ref(*f1);
+            *f0 = cuddZddSubset1(dd, nc, nv);
+            if (*f0 == NULL) {
+                Cudd_RecursiveDerefZdd(dd, pc);
+                Cudd_RecursiveDerefZdd(dd, nc);
+                Cudd_RecursiveDerefZdd(dd, *f1);
+                return(1);
+            }
+            Cudd_Ref(*f0);
+
+            *fd = cuddZddSubset0(dd, nc, nv);
+            if (*fd == NULL) {
+                Cudd_RecursiveDerefZdd(dd, pc);
+                Cudd_RecursiveDerefZdd(dd, nc);
+                Cudd_RecursiveDerefZdd(dd, *f1);
+                Cudd_RecursiveDerefZdd(dd, *f0);
+                return(1);
+            }
+            Cudd_Ref(*fd);
+        } else {
+            pc = cuddZddSubset1(dd, f, nv);
+            if (pc == NULL)
+                return(1);
+            Cudd_Ref(pc);
+            nc = cuddZddSubset0(dd, f, nv);
+            if (nc == NULL) {
+                Cudd_RecursiveDerefZdd(dd, pc);
+                return(1);
+            }
+            Cudd_Ref(nc);
+
+            *f0 = cuddZddSubset0(dd, pc, pv);
+            if (*f0 == NULL) {
+                Cudd_RecursiveDerefZdd(dd, pc);
+                Cudd_RecursiveDerefZdd(dd, nc);
+                return(1);
+            }
+            Cudd_Ref(*f0);
+            *f1 = cuddZddSubset1(dd, nc, pv);
+            if (*f1 == NULL) {
+                Cudd_RecursiveDerefZdd(dd, pc);
+                Cudd_RecursiveDerefZdd(dd, nc);
+                Cudd_RecursiveDerefZdd(dd, *f0);
+                return(1);
+            }
+            Cudd_Ref(*f1);
+
+            *fd = cuddZddSubset0(dd, nc, pv);
+            if (*fd == NULL) {
+                Cudd_RecursiveDerefZdd(dd, pc);
+                Cudd_RecursiveDerefZdd(dd, nc);
+                Cudd_RecursiveDerefZdd(dd, *f1);
+                Cudd_RecursiveDerefZdd(dd, *f0);
+                return(1);
+            }
+            Cudd_Ref(*fd);
         }
-        Cudd_Ref(*f0);
 
-        *fd = cuddZddSubset0(dd, nc, nv);
-        if (*fd == NULL) {
         Cudd_RecursiveDerefZdd(dd, pc);
         Cudd_RecursiveDerefZdd(dd, nc);
-        Cudd_RecursiveDerefZdd(dd, *f1);
-        Cudd_RecursiveDerefZdd(dd, *f0);
-        return(1);
-        }
-        Cudd_Ref(*fd);
-    } else {
-        pc = cuddZddSubset1(dd, f, nv);
-        if (pc == NULL)
-        return(1);
-        Cudd_Ref(pc);
-        nc = cuddZddSubset0(dd, f, nv);
-        if (nc == NULL) {
-        Cudd_RecursiveDerefZdd(dd, pc);
-        return(1);
-        }
-        Cudd_Ref(nc);
-
-        *f0 = cuddZddSubset0(dd, pc, pv);
-        if (*f0 == NULL) {
-        Cudd_RecursiveDerefZdd(dd, pc);
-        Cudd_RecursiveDerefZdd(dd, nc);
-        return(1);
-        }
-        Cudd_Ref(*f0);
-        *f1 = cuddZddSubset1(dd, nc, pv);
-        if (*f1 == NULL) {
-        Cudd_RecursiveDerefZdd(dd, pc);
-        Cudd_RecursiveDerefZdd(dd, nc);
-        Cudd_RecursiveDerefZdd(dd, *f1);
-        return(1);
-        }
-        Cudd_Ref(*f1);
-
-        *fd = cuddZddSubset0(dd, nc, pv);
-        if (*fd == NULL) {
-        Cudd_RecursiveDerefZdd(dd, pc);
-        Cudd_RecursiveDerefZdd(dd, nc);
-        Cudd_RecursiveDerefZdd(dd, *f1);
-        Cudd_RecursiveDerefZdd(dd, *f0);
-        return(1);
-        }
-        Cudd_Ref(*fd);
-    }
-
-    Cudd_RecursiveDerefZdd(dd, pc);
-    Cudd_RecursiveDerefZdd(dd, nc);
-    Cudd_Deref(*f1);
-    Cudd_Deref(*f0);
-    Cudd_Deref(*fd);
+        Cudd_Deref(*f1);
+        Cudd_Deref(*f0);
+        Cudd_Deref(*fd);
     }
     return(0);
 
@@ -1465,11 +1493,11 @@ cuddZddGetCofactors2(
 {
     *f1 = cuddZddSubset1(dd, f, v);
     if (*f1 == NULL)
-    return(1);
+        return(1);
     *f0 = cuddZddSubset0(dd, f, v);
     if (*f0 == NULL) {
-    Cudd_RecursiveDerefZdd(dd, *f1);
-    return(1);
+        Cudd_RecursiveDerefZdd(dd, *f1);
+        return(1);
     }
     return(0);
 
@@ -1490,26 +1518,26 @@ cuddZddGetCofactors2(
   SeeAlso     []
 
 ******************************************************************************/
-DdNode    *
+DdNode  *
 cuddZddComplement(
   DdManager * dd,
   DdNode *node)
 {
-    DdNode    *b, *isop, *zdd_I;
+    DdNode      *b, *isop, *zdd_I;
 
     /* Check cache */
     zdd_I = cuddCacheLookup1Zdd(dd, cuddZddComplement, node);
     if (zdd_I)
-    return(zdd_I);
+        return(zdd_I);
 
     b = cuddMakeBddFromZddCover(dd, node);
     if (!b)
-    return(NULL);
+        return(NULL);
     cuddRef(b);
     isop = cuddZddIsop(dd, Cudd_Not(b), Cudd_Not(b), &zdd_I);
     if (!isop) {
-    Cudd_RecursiveDeref(dd, b);
-    return(NULL);
+        Cudd_RecursiveDeref(dd, b);
+        return(NULL);
     }
     cuddRef(isop);
     cuddRef(zdd_I);
@@ -1538,7 +1566,7 @@ cuddZddGetPosVarIndex(
   DdManager * dd,
   int index)
 {
-    int    pv = (index >> 1) << 1;
+    int pv = (index >> 1) << 1;
     return(pv);
 } /* end of cuddZddGetPosVarIndex */
 
@@ -1559,7 +1587,7 @@ cuddZddGetNegVarIndex(
   DdManager * dd,
   int index)
 {
-    int    nv = index | 0x1;
+    int nv = index | 0x1;
     return(nv);
 } /* end of cuddZddGetPosVarIndex */
 
@@ -1580,7 +1608,7 @@ cuddZddGetPosVarLevel(
   DdManager * dd,
   int index)
 {
-    int    pv = cuddZddGetPosVarIndex(dd, index);
+    int pv = cuddZddGetPosVarIndex(dd, index);
     return(dd->permZ[pv]);
 } /* end of cuddZddGetPosVarLevel */
 
@@ -1601,8 +1629,10 @@ cuddZddGetNegVarLevel(
   DdManager * dd,
   int index)
 {
-    int    nv = cuddZddGetNegVarIndex(dd, index);
+    int nv = cuddZddGetNegVarIndex(dd, index);
     return(dd->permZ[nv]);
 } /* end of cuddZddGetNegVarLevel */
+
+
 ABC_NAMESPACE_IMPL_END