diff --git a/src/aig/gia/giaSatLut.c b/src/aig/gia/giaSatLut.c
index ba25ec90e..c4e11e674 100644
--- a/src/aig/gia/giaSatLut.c
+++ b/src/aig/gia/giaSatLut.c
@@ -1567,6 +1567,256 @@ int Gia_ManSimpleMapping( Gia_Man_t * p, int nBound, int nBTLimit, int nTimeout,
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+#define KSAT_OBJS  24
+#define KSAT_MINTS 64
+#define KSAT_SPACE (4+3*KSAT_OBJS+KSAT_MINTS)
+
+int Gia_KSatVarInv( int * pMap, int i )               { return pMap[i*KSAT_SPACE+0]; }
+int Gia_KSatVarAnd( int * pMap, int i )               { return pMap[i*KSAT_SPACE+1]; }
+int Gia_KSatVarEqu( int * pMap, int i )               { return pMap[i*KSAT_SPACE+2]; }
+int Gia_KSatVarRef( int * pMap, int i )               { return pMap[i*KSAT_SPACE+3]; }
+int Gia_KSatVarFan( int * pMap, int i, int f, int k ) { return pMap[i*KSAT_SPACE+4+f*KSAT_OBJS+k]; } 
+int Gia_KSatVarMin( int * pMap, int i, int m )        { return pMap[i*KSAT_SPACE+4+3*KSAT_OBJS+m]; } 
+
+void Gia_KSatSetInv( int * pMap, int i, int iVar )               { assert( -1 == pMap[i*KSAT_SPACE+0] ); pMap[i*KSAT_SPACE+0] = iVar; }
+void Gia_KSatSetAnd( int * pMap, int i, int iVar )               { assert( -1 == pMap[i*KSAT_SPACE+1] ); pMap[i*KSAT_SPACE+1] = iVar; }
+void Gia_KSatSetEqu( int * pMap, int i, int iVar )               { assert( -1 == pMap[i*KSAT_SPACE+2] ); pMap[i*KSAT_SPACE+2] = iVar; }
+void Gia_KSatSetRef( int * pMap, int i, int iVar )               { assert( -1 == pMap[i*KSAT_SPACE+3] ); pMap[i*KSAT_SPACE+3] = iVar; }
+void Gia_KSatSetFan( int * pMap, int i, int f, int k, int iVar ) { assert( -1 == pMap[i*KSAT_SPACE+4+f*KSAT_OBJS+k] ); pMap[i*KSAT_SPACE+4+f*KSAT_OBJS+k] = iVar; }  
+void Gia_KSatSetMin( int * pMap, int i, int m, int iVar )        { assert( -1 == pMap[i*KSAT_SPACE+4+3*KSAT_OBJS+m] ); pMap[i*KSAT_SPACE+4+3*KSAT_OBJS+m] = iVar; } 
+
+int Gia_KSatValInv( int * pMap, int i, Vec_Int_t * vRes )               { assert( -1 != pMap[i*KSAT_SPACE+0] ); return Vec_IntEntry( vRes, pMap[i*KSAT_SPACE+0] ); }
+int Gia_KSatValAnd( int * pMap, int i, Vec_Int_t * vRes )               { assert( -1 != pMap[i*KSAT_SPACE+1] ); return Vec_IntEntry( vRes, pMap[i*KSAT_SPACE+1] ); }
+int Gia_KSatValEqu( int * pMap, int i, Vec_Int_t * vRes )               { assert( -1 != pMap[i*KSAT_SPACE+2] ); return Vec_IntEntry( vRes, pMap[i*KSAT_SPACE+2] ); }
+int Gia_KSatValRef( int * pMap, int i, Vec_Int_t * vRes )               { assert( -1 != pMap[i*KSAT_SPACE+3] ); return Vec_IntEntry( vRes, pMap[i*KSAT_SPACE+3] ); }
+int Gia_KSatValFan( int * pMap, int i, int f, int k, Vec_Int_t * vRes ) { assert( -1 != pMap[i*KSAT_SPACE+4+f*KSAT_OBJS+k] ); return Vec_IntEntry( vRes, pMap[i*KSAT_SPACE+4+f*KSAT_OBJS+k] ); } 
+int Gia_KSatValMin( int * pMap, int i, int m, Vec_Int_t * vRes )        { assert( -1 != pMap[i*KSAT_SPACE+4+3*KSAT_OBJS+m] ); return Vec_IntEntry( vRes, pMap[i*KSAT_SPACE+4+3*KSAT_OBJS+m] ); }
+
+int * Gia_KSatMapInit( int nIns, int nNodes, word Truth, int * pnVars )
+{
+    assert( nIns + nNodes <= KSAT_OBJS );
+    assert( (1 << nIns) <= KSAT_MINTS );
+    int n, m, f, k, nVars = 2, * pMap = ABC_FALLOC( int, KSAT_OBJS*KSAT_SPACE );
+    for ( n = nIns; n < nIns+nNodes; n++ ) {
+        Gia_KSatSetInv(pMap, n, nVars++);
+        Gia_KSatSetAnd(pMap, n, nVars++);
+        Gia_KSatSetEqu(pMap, n, nVars++);
+        Gia_KSatSetRef(pMap, n, nVars++);
+    }
+    for ( n = nIns; n < nIns+nNodes; n++ ) {
+        for ( f = 0; f < 2; f++ )
+        for ( k = 0; k < n; k++ )
+            Gia_KSatSetFan(pMap, n, f, k, nVars++);
+        for ( k = n+1; k < nIns+nNodes; k++ )
+            Gia_KSatSetFan(pMap, n, 2, k, nVars++);
+    }
+    for ( m = 0; m < (1<<nIns); m++ ) {
+        for ( n = 0; n < nIns; n++ )
+            Gia_KSatSetMin(pMap, n, m, (m >> n) & 1 );
+        Gia_KSatSetMin(pMap, nIns+nNodes-1, m, (Truth >> m) & 1 );
+        for ( n = nIns; n < nIns+nNodes-1; n++ )
+            Gia_KSatSetMin(pMap, n, m, nVars++);
+    }
+    if ( pnVars ) *pnVars = nVars;
+    return pMap;
+}
+
+int Gia_KSatFindFan( int * pMap, int i, int f, Vec_Int_t * vRes ) 
+{ 
+    assert( f < 2 );
+    for ( int k = 0; k < i; k++ )
+        if ( Gia_KSatValFan( pMap, i, f, k, vRes ) )
+            return k;
+    assert( 0 );
+    return -1;
+}
+
+Gia_Man_t * Gia_ManDeriveKSatMapping( Vec_Int_t * vRes, int * pMap, int nIns, int nNodes, int fVerbose )
+{
+    Gia_Man_t * pNew = Gia_ManStart( nIns + nNodes + 2 );
+    pNew->pName = Abc_UtilStrsav( "test" );
+    int i, pCopy[256] = {0};
+    for ( i = 1; i <= nIns; i++ )
+        pCopy[i] = Gia_ManAppendCi( pNew );
+    for ( i = nIns; i < nIns+nNodes; i++ ) {
+        int iFan0 = Gia_KSatFindFan( pMap, i, 0, vRes );
+        int iFan1 = Gia_KSatFindFan( pMap, i, 1, vRes );
+        if ( iFan0 == iFan1 )
+            pCopy[i+1] = pCopy[iFan0+1];
+        else if ( Gia_KSatValAnd(pMap, i, vRes) )
+            pCopy[i+1] = Gia_ManAppendAnd( pNew, pCopy[iFan0+1], pCopy[iFan1+1] );
+        else
+            pCopy[i+1] = Gia_ManAppendOr( pNew, pCopy[iFan0+1], pCopy[iFan1+1] );
+        pCopy[i+1] = Abc_LitNotCond( pCopy[i+1], Gia_KSatValInv(pMap, i, vRes) );
+        if ( fVerbose ) {
+            printf( "%d = ", i );
+            if ( iFan0 == iFan1 )
+                printf( "INV( %d )\n", iFan0 );
+            else if ( Gia_KSatValAnd(pMap, i, vRes) ) 
+                printf( "%sAND( %d, %d )\n", Gia_KSatValInv(pMap, i, vRes) ? "N":"", iFan0, iFan1 );
+            else 
+                printf( "%sOR( %d, %d )\n", Gia_KSatValInv(pMap, i, vRes) ? "N":"", iFan0, iFan1 );
+            if ( i == nIns+nNodes-1 )
+                printf( "CO = %d\n", nIns+nNodes-1 );
+        }
+    }
+    Gia_ManAppendCo( pNew, pCopy[nIns+nNodes] );
+    return pNew;
+}
+
+Vec_Str_t * Gia_ManKSatCnf( int * pMap, int nIns, int nNodes, int nBound )
+{
+    Vec_Str_t * vStr = Vec_StrAlloc( 10000 );
+    int i, j, m, n, f, c, a, nLits = 0, pLits[256] = {0};
+    Gia_SatDumpLiteral( vStr, 1 );
+    Gia_SatDumpLiteral( vStr, 2 );   
+    // fanins are connected once
+    for ( n = nIns; n < nIns+nNodes; n++ )
+    for ( f = 0; f < 2; f++ ) {
+        nLits = 0;
+        for ( i = 0; i < n; i++ )
+            pLits[nLits++] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, i), 0 );
+        Gia_SatDumpClause( vStr, pLits, nLits );
+        for ( i = 0; i < n; i++ )
+        for ( j = 0; j < i; j++ ) {
+            pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, i), 1 );
+            pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, j), 1 );
+            Gia_SatDumpClause(  vStr, pLits, 2 );
+        }
+    }
+    for ( n = nIns; n < nIns+nNodes; n++ ) {
+        // fanins are equal
+        for ( i = 0; i < n; i++ ) {
+            pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 0, i), 1 );
+            pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 1, i), 1 );
+            pLits[2] = Abc_Var2Lit( Gia_KSatVarEqu(pMap, n), 0 );
+            Gia_SatDumpClause( vStr, pLits, 3 );
+        }
+        // if fanins are equal, inv is used
+        pLits[0] = Abc_Var2Lit( Gia_KSatVarEqu(pMap, n), 1 );
+        pLits[1] = Abc_Var2Lit( Gia_KSatVarInv(pMap, n), 0 );
+        Gia_SatDumpClause( vStr, pLits, 2 );
+        // fanin ordering 
+        for ( i = 0; i < n; i++ )
+        for ( j = 0; j < i; j++ ) {
+            pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 0, i), 1 );
+            pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 1, j), 1 );
+            Gia_SatDumpClause( vStr, pLits, 2 );
+        }
+    }    
+    for ( n = nIns; n < nIns+nNodes-1; n++ ) {
+        // there is a fanout to the node above
+        for ( i = n+1; i < nIns+nNodes; i++ ) 
+        for ( f = 0; f < 2; f++ ) {
+            pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, i, f, n), 1 );
+            pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 2, i), 0 );
+            Gia_SatDumpClause( vStr, pLits, 2 );            
+        }
+        // there is at least one fanout, except the last one
+        nLits = 0;
+        for ( i = n+1; i < nIns+nNodes; i++ )
+            pLits[nLits++] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 2, i), 0 );
+        assert( nLits > 0 );
+        Gia_SatDumpClause( vStr, pLits, nLits );
+    }
+    // there is more than one fanout, except the last one
+    for ( n = nIns; n < nIns+nNodes-1; n++ ) {
+        for ( i = n+1; i < nIns+nNodes; i++ )
+        for ( j = i+1; j < nIns+nNodes; j++ ) {
+            pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 2, i), 1 );
+            pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 2, j), 1 );
+            pLits[2] = Abc_Var2Lit( Gia_KSatVarRef(pMap, n), 0 );
+            Gia_SatDumpClause( vStr, pLits, 3 );               
+        }
+        // if more than one fanout, inv is used
+        pLits[0] = Abc_Var2Lit( Gia_KSatVarRef(pMap, n), 1 );
+        pLits[1] = Abc_Var2Lit( Gia_KSatVarInv(pMap, n), 0 );
+        Gia_SatDumpClause( vStr, pLits, 2 );
+        // if inv is not used, its fanins' invs are used
+        pLits[0] = Abc_Var2Lit( Gia_KSatVarInv(pMap, n), 0 );
+        for ( i = nIns; i < n; i++ ) 
+        for ( f = 0; f < 2; f++ ) {
+            pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, i), 1 );
+            pLits[2] = Abc_Var2Lit( Gia_KSatVarInv(pMap, i), 0 );
+            Gia_SatDumpClause( vStr, pLits, 3 );
+        }
+    }
+    // the last one always uses inverter
+    Gia_SatDumpLiteral( vStr, Abc_Var2Lit( Gia_KSatVarInv(pMap, nIns+nNodes-1), 0 ) );  
+    // for each minterm, for each pair of possible fanins, the node's output is determined using and/or and inv (4*N*N*M)
+    for ( m = 0; m < (1 << nIns); m++ )
+    for ( n = nIns; n < nIns+nNodes; n++ ) 
+    for ( c = 0; c < 2; c++ )
+    for ( a = 0; a < 2; a++ ) {        
+        // implications: Fan(f) & Mint(m) & !And & !Inv -> Val1
+        for ( f = 0; f < 2; f++ ) 
+        for ( i = 0; i < n; i++ ) {
+            pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, i), 1 );
+            pLits[1] = Abc_Var2Lit( Gia_KSatVarMin(pMap, i, m), !a );
+            pLits[2] = Abc_Var2Lit( Gia_KSatVarAnd(pMap, n), a );
+            pLits[3] = Abc_Var2Lit( Gia_KSatVarInv(pMap, n), c );
+            pLits[4] = Abc_Var2Lit( Gia_KSatVarMin(pMap, n, m), a^c );
+            Gia_SatDumpClause( vStr, pLits, 5 );
+        }
+        // large clauses: Fan(0) & Fan(1) & !Mint(m) & !Mint(m) & !And & !Inv -> Val0
+        for ( i = 0; i < n; i++ ) 
+        for ( j = i; j < n; j++ ) {
+            pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 0, i), 1 );
+            pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 1, j), 1 );
+            pLits[2] = Abc_Var2Lit( Gia_KSatVarMin(pMap, i, m), a );
+            pLits[3] = Abc_Var2Lit( Gia_KSatVarMin(pMap, j, m), a );
+            pLits[4] = Abc_Var2Lit( Gia_KSatVarAnd(pMap, n), a );
+            pLits[5] = Abc_Var2Lit( Gia_KSatVarInv(pMap, n), c );
+            pLits[6] = Abc_Var2Lit( Gia_KSatVarMin(pMap, n, m), a==c );
+            Gia_SatDumpClause( vStr, pLits, 7 );
+        }
+    }
+    // the number of nodes with duplicated fanins and without inv is maximized
+    Vec_StrPush( vStr, '\0' );
+    return vStr;    
+}
+
+Gia_Man_t * Gia_ManKSatMapping( word Truth, int nIns, int nNodes, int nBound, int nBTLimit, int nTimeout, int fVerbose )
+{
+    Gia_Man_t * pNew = NULL;
+    char * pFileNameI = (char *)"__temp__.cnf"; 
+    char * pFileNameO = (char *)"__temp__.out";
+    int nVars = 0, * pMap = Gia_KSatMapInit( nIns, nNodes, Truth, &nVars );
+    Vec_Str_t * vStr = Gia_ManKSatCnf( pMap, nIns, nNodes, nBound );
+    if ( !Gia_ManDumpCnf(pFileNameI, vStr, nVars) ) {
+        Vec_StrFree( vStr );
+        return NULL;
+    }
+    if ( fVerbose )
+        printf( "Vars = %d. Nodes = %d. Cardinality bound = %d.  SAT vars = %d. SAT clauses = %d. Conflict limit = %d. Timeout = %d.\n", 
+            nIns, nNodes, nBound,  nVars, Vec_StrCountEntry(vStr, '\n'), nBTLimit, nTimeout );
+    //char pFileName[100]; sprintf( pFileName, "temp%02d.cnf", nBound/2 );
+    //Gia_ManDumpCnf( pFileName, vStr, nVars );
+    Vec_StrFree( vStr );
+    Vec_Int_t * vRes = Gia_RunKadical( pFileNameI, pFileNameO, nBTLimit, nTimeout, 1 );
+    unlink( pFileNameI );
+    //unlink( pFileNameO );
+    if ( vRes == NULL )
+        return 0;
+    Vec_IntDrop( vRes, 0 );
+    pNew = Gia_ManDeriveKSatMapping( vRes, pMap, nIns, nNodes, fVerbose );
+    Vec_IntFree( vRes );
+    ABC_FREE( pMap );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 93fc10efb..2206a02b7 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -513,6 +513,7 @@ static int Abc_CommandAbc9Mf                 ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Nf                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Of                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Simap              ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Exmap              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Pack               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Edge               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9SatLut             ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1321,6 +1322,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&nf",           Abc_CommandAbc9Nf,           0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&of",           Abc_CommandAbc9Of,           0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&simap",        Abc_CommandAbc9Simap,        0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&exmap",        Abc_CommandAbc9Exmap,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&pack",         Abc_CommandAbc9Pack,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&edge",         Abc_CommandAbc9Edge,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&satlut",       Abc_CommandAbc9SatLut,       0 );
@@ -44393,7 +44395,7 @@ int Abc_CommandAbc9Simap( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'B':
             if ( globalUtilOptind >= argc )
             {
-                Abc_Print( -1, "Command line switch \"-N\" should be followed by a positive integer.\n" );
+                Abc_Print( -1, "Command line switch \"-B\" should be followed by a positive integer.\n" );
                 goto usage;
             }
             nBound = atoi(argv[globalUtilOptind]);
@@ -44456,6 +44458,126 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Exmap( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Gia_Man_t * Gia_ManKSatMapping( word Truth, int nIns, int nNodes, int nBound, int nBTLimit, int nTimeout, int fVerbose );
+    int c, nVars = 0, nNodes = 0, nBTLimit = 0, nBound = 0, nTimeout = 0, fVerbose = 0; Gia_Man_t * pTemp = NULL;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "NBCTvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-N\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nNodes = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nNodes < 0 )
+            {
+                Abc_Print( -1, "Bound on a solution should be a positive integer.\n" );
+                goto usage;
+            }
+            break;
+        case 'B':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-B\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nBound = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nBound < 0 )
+            {
+                Abc_Print( -1, "Bound on a solution should be a positive integer.\n" );
+                goto usage;
+            }
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nBTLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nBTLimit < 0 )
+            {
+                Abc_Print( -1, "Conflict limit should be a positive integer.\n" );
+                goto usage;
+            }
+            break;
+        case 'T':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-T\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nTimeout = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;            
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+        default:
+            goto usage;
+        }
+    }
+    if ( argc != globalUtilOptind + 1 )
+    {
+        Abc_Print( -1, "Truth table should be given on the command line.\n" );
+        return 1;
+    }
+    char * pTruth = argv[globalUtilOptind];
+    nVars = Abc_Base2Log(4*strlen(pTruth));
+    if ( (1 << nVars) != 4*strlen(pTruth) ) 
+    {
+        Abc_Print( -1, "The string (%s) does not look like a hex truth table.\n", pTruth );
+        return 1;
+    }
+    if ( nVars > 6 ) 
+    {
+        Abc_Print( -1, "Currently only works for functions of 6 of fewer inputs.\n" );
+        return 1;
+    }
+    if ( nNodes == 0 )
+    {
+        Abc_Print( -1, "The number of nodes should be given on the command line (-N <num>).\n" );
+        return 1;
+    }
+    word Truth = 0;
+    int nVars2 = Abc_TtReadHex( &Truth, pTruth );
+    assert( nVars2 == nVars );
+    pTemp = Gia_ManKSatMapping( Truth, nVars, nNodes, nBound, nBTLimit, nTimeout, fVerbose );
+    if ( pTemp ) Abc_FrameUpdateGia( pAbc, pTemp );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &exmap [-NBCT num] [-vh] <truth>\n" );
+    Abc_Print( -2, "\t           performs simple mapping of the truth table\n" );
+    Abc_Print( -2, "\t-N num   : the number of nodes [default = %d]\n", nNodes );
+    Abc_Print( -2, "\t-B num   : the bound on the solution size [default = %d]\n", nBound );
+    Abc_Print( -2, "\t-C num   : the conflict limit [default = %d]\n", nBTLimit );
+    Abc_Print( -2, "\t-T num   : runtime limit in seconds [default = %d]\n", nTimeout );    
+    Abc_Print( -2, "\t-v       : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h       : prints the command usage\n");
+    return 1;
+}
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -45818,6 +45940,8 @@ int Abc_CommandAbc9Rewire( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     pTemp = Gia_ManRewire( pAbc->pGia, nIters, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nDist, nSeed, nVerbose );
+    if ( pTemp->pName == NULL )
+        pTemp->pName = Abc_UtilStrsav(Extra_FileNameWithoutPath(pAbc->pGia->pName));
     Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;