From 6463f11625bcdac49c37df03f70cd08db88344c2 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sat, 7 Jun 2025 12:52:23 -0700
Subject: [PATCH] Fixing pointer-dependent behavior during BDD variable
 reordering.

---
 src/bdd/cudd/cuddInt.h     |  1 +
 src/bdd/cudd/cuddReorder.c | 18 +++++++++---------
 src/bdd/cudd/cuddTable.c   |  3 ++-
 3 files changed, 12 insertions(+), 10 deletions(-)

diff --git a/src/bdd/cudd/cuddInt.h b/src/bdd/cudd/cuddInt.h
index 2ccf86a76..c8e49a4ed 100644
--- a/src/bdd/cudd/cuddInt.h
+++ b/src/bdd/cudd/cuddInt.h
@@ -381,6 +381,7 @@ struct DdManager {      /* specialized DD symbol table */
 //    double allocated;           /* number of nodes allocated */
     ABC_INT64_T allocated;      /* number of nodes allocated */
                                 /* (not during reordering) */
+    ABC_INT64_T allocated2;     /* number of nodes allocated */
     double reclaimed;           /* number of nodes brought back from the dead */
     int isolated;               /* isolated projection functions */
     int *perm;                  /* current variable perm. (index to level) */
diff --git a/src/bdd/cudd/cuddReorder.c b/src/bdd/cudd/cuddReorder.c
index c48b0c138..105cc12a3 100644
--- a/src/bdd/cudd/cuddReorder.c
+++ b/src/bdd/cudd/cuddReorder.c
@@ -480,7 +480,7 @@ cuddDynamicAllocNode(
 
     node = table->nextFree;
     table->nextFree = node->next;
-    //node->Id = 0;
+    node->Id = (++table->allocated2<<4);
     return (node);
 
 } /* end of cuddDynamicAllocNode */
@@ -937,11 +937,11 @@ cuddSwapInPlace(
                 /* For each element tmp in collision list xlist[posn]. */
                 previousP = &(xlist[posn]);
                 tmp = *previousP;
-                while (f1 < cuddT(tmp)) {
+                while (cuddF2L(f1) < (cuddT(tmp) ? cuddF2L(cuddT(tmp)) : 0)) {
                     previousP = &(tmp->next);
                     tmp = *previousP;
                 }
-                while (f1 == cuddT(tmp) && f0 < cuddE(tmp)) {
+                while (f1 == cuddT(tmp) && cuddF2L(f0) < (cuddE(tmp) ? cuddF2L(cuddE(tmp)) : 0)) {
                     previousP = &(tmp->next);
                     tmp = *previousP;
                 }
@@ -998,11 +998,11 @@ cuddSwapInPlace(
                 /* For each element newf1 in collision list xlist[posn]. */
                 previousP = &(xlist[posn]);
                 newf1 = *previousP;
-                while (f11 < cuddT(newf1)) {
+                while (cuddF2L(f11) < (cuddT(newf1) ? cuddF2L(cuddT(newf1)) : 0)) {
                     previousP = &(newf1->next);
                     newf1 = *previousP;
                 }
-                while (f11 == cuddT(newf1) && f01 < cuddE(newf1)) {
+                while (f11 == cuddT(newf1) && cuddF2L(f01) < (cuddE(newf1) ? cuddF2L(cuddE(newf1)) : 0)) {
                     previousP = &(newf1->next);
                     newf1 = *previousP;
                 }
@@ -1052,11 +1052,11 @@ cuddSwapInPlace(
                 /* For each element newf0 in collision list xlist[posn]. */
                 previousP = &(xlist[posn]);
                 newf0 = *previousP;
-                while (f10 < cuddT(newf0)) {
+                while (cuddF2L(f10) < (cuddT(newf0) ? cuddF2L(cuddT(newf0)) : 0)) {
                     previousP = &(newf0->next);
                     newf0 = *previousP;
                 }
-                while (f10 == cuddT(newf0) && f00 < cuddE(newf0)) {
+                while (f10 == cuddT(newf0) && cuddF2L(f00) < (cuddE(newf0) ? cuddF2L(cuddE(newf0)) : 0)) {
                     previousP = &(newf0->next);
                     newf0 = *previousP;
                 }
@@ -1093,11 +1093,11 @@ cuddSwapInPlace(
             newykeys++;
             previousP = &(ylist[posn]);
             tmp = *previousP;
-            while (newf1 < cuddT(tmp)) {
+            while (cuddF2L(newf1) < (cuddT(tmp) ? cuddF2L(cuddT(tmp)) : 0)) {
                 previousP = &(tmp->next);
                 tmp = *previousP;
             }
-            while (newf1 == cuddT(tmp) && newf0 < cuddE(tmp)) {
+            while (newf1 == cuddT(tmp) && cuddF2L(newf0) < (cuddE(tmp) ? cuddF2L(cuddE(tmp)) : 0)) {
                 previousP = &(tmp->next);
                 tmp = *previousP;
             }
diff --git a/src/bdd/cudd/cuddTable.c b/src/bdd/cudd/cuddTable.c
index 04af1991a..6020f94c4 100644
--- a/src/bdd/cudd/cuddTable.c
+++ b/src/bdd/cudd/cuddTable.c
@@ -329,7 +329,7 @@ cuddAllocNode(
     unique->allocated++;
     node = unique->nextFree;
     unique->nextFree = node->next;
-    node->Id = (unique->allocated<<4);
+    node->Id = (++unique->allocated2<<4);
     return(node);
 
 } /* end of cuddAllocNode */
@@ -398,6 +398,7 @@ cuddInitTable(
     unique->looseUpTo = looseUpTo;
     unique->gcEnabled = 1;
     unique->allocated = 0;
+    unique->allocated2 = 0;
     unique->reclaimed = 0;
     unique->subtables = ABC_ALLOC(DdSubtable,unique->maxSize);
     if (unique->subtables == NULL) {