From e7d360811f8d6c285b96451819ec6a007cee3978 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sun, 10 Aug 2025 11:04:20 -0700
Subject: [PATCH] Fixed combo loop in choice computation.

---
 src/aig/gia/giaDup.c | 48 ++++++++++++++++++++++++++++++++++++++++++--
 src/base/abci/abc.c  |  4 ++--
 2 files changed, 48 insertions(+), 4 deletions(-)

diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 099f33693..8eb3e928f 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -6272,6 +6272,40 @@ Gia_Man_t * Gia_ManDupFanouts( Gia_Man_t * p )
     return pNew;    
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManDupChoicesMarkTfi_rec( Gia_Man_t * pGia, int iObj )
+{
+    if ( Gia_ObjIsTravIdCurrentId(pGia, iObj) )
+        return;
+    Gia_ObjSetTravIdCurrentId(pGia, iObj);
+    Gia_Obj_t * pObj = Gia_ManObj(pGia, iObj);
+    if ( !Gia_ObjIsAnd(pObj) )
+        return;
+    Gia_ManDupChoicesMarkTfi_rec( pGia, Gia_ObjFaninId0(pObj, iObj) );
+    Gia_ManDupChoicesMarkTfi_rec( pGia, Gia_ObjFaninId1(pObj, iObj) );
+    Gia_Obj_t * pSibl = Gia_ObjSiblObj( pGia, iObj );
+    if ( pSibl ) Gia_ManDupChoicesMarkTfi_rec( pGia, Gia_ObjId(pGia, pSibl) );
+}
+int Gia_ManDupChoicesCheckOverlap( Gia_Man_t * pGia, int iObj, int iFan0, int iFan1 )
+{
+    Gia_ManIncrementTravId( pGia );
+    Gia_ManDupChoicesMarkTfi_rec( pGia, Gia_ObjFaninId0(Gia_ManObj(pGia, iObj), iObj) );
+    Gia_ManDupChoicesMarkTfi_rec( pGia, Gia_ObjFaninId1(Gia_ManObj(pGia, iObj), iObj) );
+    if ( Gia_ObjIsTravIdCurrentId(pGia, iFan0) || Gia_ObjIsTravIdCurrentId(pGia, iFan1) )
+        return 1;
+    return 0;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Reorders choice nodes.]
@@ -6288,14 +6322,24 @@ void Gia_ManPrintChoices( Gia_Man_t * p )
     Gia_Obj_t * pObj; int i;
     Gia_ManForEachAnd( p, pObj, i )
         if ( p->pSibls[i] )
-            printf( "%d -> %d\n", i, p->pSibls[i] );
+            printf( "%d -> %d    ", i, p->pSibls[i] );
 }
 void Gia_ManReorderChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
 {
     if ( ~pObj->Value )
         return;
     assert( Gia_ObjIsAnd(pObj) );
-    Gia_Obj_t * pSibl = Gia_ObjSiblObj(p, Gia_ObjId(p, pObj));
+    int ObjId = Gia_ObjId(p, pObj);
+    Gia_Obj_t * pSibl = Gia_ObjSiblObj(p, ObjId);    
+    if ( pSibl ) {
+        int SiblId = Gia_ObjId(p, pSibl);
+        if ( Gia_ManDupChoicesCheckOverlap( p, SiblId, Gia_ObjFaninId0(pObj, ObjId), Gia_ObjFaninId1(pObj, ObjId) ) ) {
+            assert( p->pSibls[ObjId] == SiblId );
+            p->pSibls[ObjId] = p->pSibls[SiblId];
+            Gia_ManReorderChoices_rec( pNew, p, pObj );
+            return;
+        }        
+    }    
     Gia_ManReorderChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
     Gia_ManReorderChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
     if ( pSibl ) Gia_ManReorderChoices_rec( pNew, p, pSibl );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 8ab2ff672..c0da2150f 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -47482,8 +47482,8 @@ usage:
     Abc_Print( -2, "\t-f     : toggle using lighter logic synthesis [default = %s]\n", pPars->fLightSynth? "yes": "no" );
     Abc_Print( -2, "\t-r     : toggle skipping choices with redundant support [default = %s]\n", pPars->fSkipRedSupp? "yes": "no" );
     Abc_Print( -2, "\t-e     : toggle computing and merging equivalences [default = %s]\n", fEquiv? "yes": "no" );
-    Abc_Print( -2, "\t-m     : toggle minimizing logic level after merging equivalences [default = %s]\n", fRandom? "yes": "no" );
-    Abc_Print( -2, "\t-n     : toggle selecting random choices while merging equivalences [default = %s]\n", fMinLevel? "yes": "no" );
+    Abc_Print( -2, "\t-m     : toggle minimizing logic level after merging equivalences [default = %s]\n", fMinLevel? "yes": "no" );
+    Abc_Print( -2, "\t-n     : toggle selecting random choices while merging equivalences [default = %s]\n", fRandom? "yes": "no" );
     Abc_Print( -2, "\t-g     : toggle using GIA to prove equivalences [default = %s]\n", pPars->fUseGia? "yes": "no" );
     Abc_Print( -2, "\t-c     : toggle using circuit-based SAT vs. MiniSat [default = %s]\n", pPars->fUseCSat? "yes": "no" );
     Abc_Print( -2, "\t-x     : toggle using new choice computation [default = %s]\n", pPars->fUseNew? "yes": "no" );