Bug fix in &gencex.

berkeley-abc · Jan 1, 2025 · d5e1a5d · d5e1a5d
1 parent 350dcd3
commit d5e1a5d
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 1 deletion.
diff --git a/src/aig/gia/giaPat2.c b/src/aig/gia/giaPat2.c
@@ -965,6 +965,12 @@ Vec_Wec_t * Min_ManComputeCexes( Gia_Man_t * p, Vec_Int_t * vOuts0, int nMaxTrie
         if ( Vec_IntEntry(vStats[2], i) >= nMinCexes || Vec_IntEntry(vStats[1], i) > 10*Vec_IntEntry(vStats[2], i) )
             continue;
         {
+            assert( Gia_ObjIsCo(pObj) );
+            if ( Gia_ObjFaninId0p(p, pObj) == 0 ) {
+                if ( fVerbose )
+                    printf( "Output %d is driven by constant %d.\n", Gia_ObjCioId(pObj), Gia_ObjFaninC0(pObj) );
+                continue;
+            }
             abctime clk = Abc_Clock();
             int iObj  = Min_ManCo(pNew, i);
             int Index = Gia_ObjCioId(pObj);

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
@@ -54262,7 +54262,7 @@ int Abc_CommandAbc9GenCex( Abc_Frame_t * pAbc, int argc, char ** argv )
 usage:
     Abc_Print( -2, "usage: &gencex [-CM num] [-F file] [-stcbvh]\n" );
     Abc_Print( -2, "\t          generates satisfying assignments for each output of the miter\n" );
-    Abc_Print( -2, "\t-C num  : the number of timeframes [default = %d]\n",                  nMinCexes );
+    Abc_Print( -2, "\t-C num  : the number of satisfying assignments [default = %d]\n",      nMinCexes );
     Abc_Print( -2, "\t-M num  : the max simulation runs before using SAT [default = %d]\n",  nMaxTries );
     Abc_Print( -2, "\t-F file : the output file name [default = %s]\n",                      pFileName );
     Abc_Print( -2, "\t-s      : toggles using reverse simulation [default = %s]\n",          fUseSim  ? "yes": "no" );