Version abc50915

29 files changed, 622 insertions, 197 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index c0fec75d..db66c49b 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -249,12 +249,12 @@ static inline int         Abc_NtkCiNum( Abc_Ntk_t * pNtk )           { return pN
 static inline int         Abc_NtkCoNum( Abc_Ntk_t * pNtk )           { return pNtk->vCos->nSize;          }
 
 // reading objects
-static inline Abc_Obj_t * Abc_NtkObj( Abc_Ntk_t * pNtk, int i )      { assert( i < Vec_PtrSize(pNtk->vObjs) ); return pNtk->vObjs->pArray[i];  }
-static inline Abc_Obj_t * Abc_NtkLatch( Abc_Ntk_t * pNtk, int i )    { assert( i < Vec_PtrSize(pNtk->vLats) ); return pNtk->vLats->pArray[i];  }
-static inline Abc_Obj_t * Abc_NtkPi( Abc_Ntk_t * pNtk, int i )       { assert( i < Abc_NtkPiNum(pNtk) ); return pNtk->vCis->pArray[i];      }
-static inline Abc_Obj_t * Abc_NtkPo( Abc_Ntk_t * pNtk, int i )       { assert( i < Abc_NtkPoNum(pNtk) ); return pNtk->vCos->pArray[i];      }
-static inline Abc_Obj_t * Abc_NtkCi( Abc_Ntk_t * pNtk, int i )       { assert( i < Abc_NtkCiNum(pNtk) ); return pNtk->vCis->pArray[i];      }
-static inline Abc_Obj_t * Abc_NtkCo( Abc_Ntk_t * pNtk, int i )       { assert( i < Abc_NtkCoNum(pNtk) ); return pNtk->vCos->pArray[i];      }
+static inline Abc_Obj_t * Abc_NtkObj( Abc_Ntk_t * pNtk, int i )      { assert( i < Vec_PtrSize(pNtk->vObjs) ); return (Abc_Obj_t *)pNtk->vObjs->pArray[i];  }
+static inline Abc_Obj_t * Abc_NtkLatch( Abc_Ntk_t * pNtk, int i )    { assert( i < Vec_PtrSize(pNtk->vLats) ); return (Abc_Obj_t *)pNtk->vLats->pArray[i];  }
+static inline Abc_Obj_t * Abc_NtkPi( Abc_Ntk_t * pNtk, int i )       { assert( i < Abc_NtkPiNum(pNtk) ); return (Abc_Obj_t *)pNtk->vCis->pArray[i];      }
+static inline Abc_Obj_t * Abc_NtkPo( Abc_Ntk_t * pNtk, int i )       { assert( i < Abc_NtkPoNum(pNtk) ); return (Abc_Obj_t *)pNtk->vCos->pArray[i];      }
+static inline Abc_Obj_t * Abc_NtkCi( Abc_Ntk_t * pNtk, int i )       { assert( i < Abc_NtkCiNum(pNtk) ); return (Abc_Obj_t *)pNtk->vCis->pArray[i];      }
+static inline Abc_Obj_t * Abc_NtkCo( Abc_Ntk_t * pNtk, int i )       { assert( i < Abc_NtkCoNum(pNtk) ); return (Abc_Obj_t *)pNtk->vCos->pArray[i];      }
 
 // reading data members of the object
 static inline unsigned    Abc_ObjType( Abc_Obj_t * pObj )            { return pObj->Type;               }
@@ -293,13 +293,13 @@ static inline int         Abc_ObjFanoutNum( Abc_Obj_t * pObj )       { return pO
 static inline int         Abc_ObjFaninId( Abc_Obj_t * pObj, int i)   { return pObj->vFanins.pArray[i].iFan; }
 static inline int         Abc_ObjFaninId0( Abc_Obj_t * pObj )        { return pObj->vFanins.pArray[0].iFan; }
 static inline int         Abc_ObjFaninId1( Abc_Obj_t * pObj )        { return pObj->vFanins.pArray[1].iFan; }
-static inline Abc_Obj_t * Abc_ObjFanout( Abc_Obj_t * pObj, int i )   { return pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[i].iFan ];   }
-static inline Abc_Obj_t * Abc_ObjFanout0( Abc_Obj_t * pObj )         { return pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[0].iFan ];   }
-static inline Abc_Obj_t * Abc_ObjFanin( Abc_Obj_t * pObj, int i )    { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[i].iFan  ];   }
-static inline Abc_Obj_t * Abc_ObjFanin0( Abc_Obj_t * pObj )          { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[0].iFan  ];   }
-static inline Abc_Obj_t * Abc_ObjFanin1( Abc_Obj_t * pObj )          { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[1].iFan  ];   }
-static inline Abc_Obj_t * Abc_ObjFanin0Ntk( Abc_Obj_t * pObj )       { return Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanin0(pObj) : pObj;     }
-static inline Abc_Obj_t * Abc_ObjFanout0Ntk( Abc_Obj_t * pObj )      { return Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanout0(pObj) : pObj;    }
+static inline Abc_Obj_t * Abc_ObjFanout( Abc_Obj_t * pObj, int i )   { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[i].iFan ];   }
+static inline Abc_Obj_t * Abc_ObjFanout0( Abc_Obj_t * pObj )         { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[0].iFan ];   }
+static inline Abc_Obj_t * Abc_ObjFanin( Abc_Obj_t * pObj, int i )    { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[i].iFan  ];   }
+static inline Abc_Obj_t * Abc_ObjFanin0( Abc_Obj_t * pObj )          { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[0].iFan  ];   }
+static inline Abc_Obj_t * Abc_ObjFanin1( Abc_Obj_t * pObj )          { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[1].iFan  ];   }
+static inline Abc_Obj_t * Abc_ObjFanin0Ntk( Abc_Obj_t * pObj )       { return (Abc_Obj_t *)(Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanin0(pObj)  : pObj);  }
+static inline Abc_Obj_t * Abc_ObjFanout0Ntk( Abc_Obj_t * pObj )      { return (Abc_Obj_t *)(Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanout0(pObj) : pObj);  }
 static inline bool        Abc_ObjFaninC( Abc_Obj_t * pObj, int i )   { return pObj->vFanins.pArray[i].fCompl;                               }
 static inline bool        Abc_ObjFaninC0( Abc_Obj_t * pObj )         { return pObj->vFanins.pArray[0].fCompl;                               }
 static inline bool        Abc_ObjFaninC1( Abc_Obj_t * pObj )         { return pObj->vFanins.pArray[1].fCompl;                               }
@@ -421,6 +421,8 @@ extern bool               Abc_AigNodeHasComplFanoutEdge( Abc_Obj_t * pNode );
 extern bool               Abc_AigNodeHasComplFanoutEdgeTrav( Abc_Obj_t * pNode );
 extern void               Abc_AigPrintNode( Abc_Obj_t * pNode );
 extern bool               Abc_AigNodeIsAcyclic( Abc_Obj_t * pNode, Abc_Obj_t * pRoot );
+extern void               Abc_AigCheckFaninOrder( Abc_Aig_t * pMan );
+extern void               Abc_AigRehash( Abc_Aig_t * pMan );
 /*=== abcAttach.c ==========================================================*/
 extern int                Abc_NtkAttach( Abc_Ntk_t * pNtk );
 /*=== abcBalance.c ==========================================================*/
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index 3e90aa76..639f4926 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -409,6 +409,7 @@ Abc_Obj_t * Abc_AigAndCreateFrom( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t *
     Key = Abc_HashKey2( p0, p1, pMan->nBins );
     pAnd->pNext      = pMan->pBins[Key];
     pMan->pBins[Key] = pAnd;
+    pMan->nEntries++;
     // create the cuts if defined
 //    if ( pAnd->pNtk->pManCut )
 //        Abc_NodeGetCuts( pAnd->pNtk->pManCut, pAnd );
@@ -542,6 +543,57 @@ clk = clock();
     pMan->nBins = nBinsNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Resizes the hash table of AIG nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_AigRehash( Abc_Aig_t * pMan )
+{
+    Abc_Obj_t ** pBinsNew;
+    Abc_Obj_t * pEnt, * pEnt2;
+    Abc_Fan_t * pArray;
+    unsigned Key;
+    int Counter, Temp, i;
+
+    // allocate a new array
+    pBinsNew = ALLOC( Abc_Obj_t *, pMan->nBins );
+    memset( pBinsNew, 0, sizeof(Abc_Obj_t *) * pMan->nBins );
+    // rehash the entries from the old table
+    Counter = 0;
+    for ( i = 0; i < pMan->nBins; i++ )
+        Abc_AigBinForEachEntrySafe( pMan->pBins[i], pEnt, pEnt2 )
+        {
+            // swap the fanins if needed
+            pArray = pEnt->vFanins.pArray;
+            if ( pArray[0].iFan > pArray[1].iFan )
+            {
+                Temp = pArray[0].iFan;
+                pArray[0].iFan = pArray[1].iFan;
+                pArray[1].iFan = Temp;
+                Temp = pArray[0].fCompl;
+                pArray[0].fCompl = pArray[1].fCompl;
+                pArray[1].fCompl = Temp;
+            }
+            // rehash the node
+            Key = Abc_HashKey2( Abc_ObjChild0(pEnt), Abc_ObjChild1(pEnt), pMan->nBins );
+            pEnt->pNext   = pBinsNew[Key];
+            pBinsNew[Key] = pEnt;
+            Counter++;
+        }
+    assert( Counter == pMan->nEntries );
+    // replace the table and the parameters
+    free( pMan->pBins );
+    pMan->pBins = pBinsNew;
+}
+
+
 
 
 
@@ -1157,6 +1209,34 @@ bool Abc_AigNodeIsAcyclic( Abc_Obj_t * pNode, Abc_Obj_t * pRoot )
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Resizes the hash table of AIG nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_AigCheckFaninOrder( Abc_Aig_t * pMan )
+{
+    Abc_Obj_t * pEnt;
+    int i;
+    for ( i = 0; i < pMan->nBins; i++ )
+        Abc_AigBinForEachEntry( pMan->pBins[i], pEnt )
+        {
+            if ( Abc_ObjRegular(Abc_ObjChild0(pEnt))->Id > Abc_ObjRegular(Abc_ObjChild1(pEnt))->Id )
+            {
+                int i0 = Abc_ObjRegular(Abc_ObjChild0(pEnt))->Id;
+                int i1 = Abc_ObjRegular(Abc_ObjChild1(pEnt))->Id;
+                int x = 0;
+                printf( "Node %d has incorrect ordering of fanins.\n", pEnt->Id );
+            }
+        }
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcNames.c b/src/base/abc/abcNames.c
index 53ac6e07..619cce23 100644
--- a/src/base/abc/abcNames.c
+++ b/src/base/abc/abcNames.c
@@ -283,6 +283,7 @@ void Abc_NtkDupCioNamesTable( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
         Abc_NtkLogicStoreName( Abc_NtkPi(pNtkNew,i),    Abc_ObjName(pObj) );
     Abc_NtkForEachPo( pNtk, pObj, i ) 
         Abc_NtkLogicStoreName( Abc_NtkPo(pNtkNew,i),    Abc_ObjName(pObj) );
+    if ( !Abc_NtkIsSeq(pNtk) )
     Abc_NtkForEachLatch( pNtk, pObj, i )
         Abc_NtkLogicStoreName( Abc_NtkLatch(pNtkNew,i), Abc_ObjName(pObj) );
 }
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index a237f75e..2720f169 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -72,7 +72,10 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func )
     else if ( Abc_NtkHasBdd(pNtk) )
         pNtk->pManFunc = Cudd_Init( 20, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
     else if ( Abc_NtkHasAig(pNtk) )
-        pNtk->pManFunc = Abc_AigAlloc( pNtk );
+    {
+        if ( Abc_NtkIsStrash(pNtk) )
+            pNtk->pManFunc = Abc_AigAlloc( pNtk );
+    }
     else if ( Abc_NtkHasMapping(pNtk) )
         pNtk->pManFunc = Abc_FrameReadLibGen();
     else
@@ -266,7 +269,7 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
     // start the network
     pNtkNew = Abc_NtkStartFrom( pNtk, pNtk->ntkType, pNtk->ntkFunc );
     // copy the internal nodes
-    if ( Abc_NtkHasAig(pNtk) )
+    if ( Abc_NtkIsStrash(pNtk) )
         Abc_AigDup( pNtk->pManFunc, pNtkNew->pManFunc );
     else
     {
@@ -278,6 +281,23 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
         Abc_NtkForEachObj( pNtk, pObj, i )
             Abc_ObjForEachFanin( pObj, pFanin, k )
                 Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
+        // if it is a sequential networ, transfer attributes on edges
+        if ( Abc_NtkIsSeq(pNtk) )
+        {
+            pNtkNew->vInits = Vec_IntStart( 2 * Abc_NtkObjNumMax(pNtkNew) );
+            Abc_NtkForEachObj( pNtk, pObj, i )
+            {
+                Abc_ObjForEachFanin( pObj, pFanin, k )
+                {
+                    if ( Abc_ObjFaninC(pObj, k) )
+                        Abc_ObjSetFaninC( pObj->pCopy, k );
+                    if ( Abc_ObjFaninL(pObj, k) > 0 )
+                        Abc_ObjSetFaninL( pObj->pCopy, k, Abc_ObjFaninL(pObj, k) );
+                }
+                Vec_IntWriteEntry( pNtkNew->vInits, 2*pObj->pCopy->Id+0, Vec_IntEntry(pNtk->vInits, 2*pObj->Id+0) );
+                Vec_IntWriteEntry( pNtkNew->vInits, 2*pObj->pCopy->Id+1, Vec_IntEntry(pNtk->vInits, 2*pObj->Id+1) );
+            }
+        }
     }
     // duplicate the EXDC Ntk
     if ( pNtk->pExdc )
@@ -504,7 +524,8 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     Vec_PtrFree( pNtk->vPtrTemp );
     Vec_IntFree( pNtk->vIntTemp );
     Vec_StrFree( pNtk->vStrTemp );
-    if ( pNtk->vInits )  Vec_IntFree( pNtk->vInits );
+    if ( pNtk->vInits ) Vec_IntFree( pNtk->vInits );
+    if ( pNtk->pModel ) free( pNtk->pModel );
     // free the hash table of Obj name into Obj ID
     stmm_free_table( pNtk->tName2Net );
     stmm_free_table( pNtk->tObj2Name );
@@ -526,7 +547,10 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     else if ( Abc_NtkHasBdd(pNtk) )
         Extra_StopManager( pNtk->pManFunc );
     else if ( Abc_NtkHasAig(pNtk) )
-        Abc_AigFree( pNtk->pManFunc );
+    {
+        if ( Abc_NtkIsStrash(pNtk) )
+            Abc_AigFree( pNtk->pManFunc );
+    }
     else if ( !Abc_NtkHasMapping(pNtk) )
         assert( 0 );
     free( pNtk );
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index 15753f4e..9471bb3f 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -158,7 +158,7 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
                 pObjNew->pData = Cudd_bddTransfer(pObj->pNtk->pManFunc, pNtkNew->pManFunc, pObj->pData), Cudd_Ref(pObjNew->pData);
             else if ( Abc_NtkHasMapping(pNtkNew) )
                 pObjNew->pData = pObj->pData;
-            else if ( Abc_NtkHasAig(pNtkNew) )
+            else if ( Abc_NtkIsStrash(pNtkNew) )
                 assert( 0 );
         }
     }
@@ -191,6 +191,13 @@ Abc_Obj_t * Abc_NtkDupConst1( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew )
     pConst1 = Abc_AigConst1(pNtkAig->pManFunc);
     if ( Abc_ObjFanoutNum(pConst1) > 0 )
         pConst1->pCopy = Abc_NodeCreateConst1( pNtkNew );
+    else
+    {
+        // skip the 0-th entry to allow one-to-one match of object IDs
+        if ( pConst1->Id == 0 && pNtkNew->nNodes == 0 )
+            Vec_PtrPush( pNtkNew->vObjs, NULL );
+    }
+
     return pConst1->pCopy; 
 } 
 
diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c
index 20a64246..e36f5219 100644
--- a/src/base/abc/abcShow.c
+++ b/src/base/abc/abcShow.c
@@ -96,7 +96,7 @@ void Abc_NtkShowAig( Abc_Ntk_t * pNtk )
     char FileNameDot[200];
     int i;
 
-    assert( Abc_NtkIsStrash(pNtk) );
+    assert( Abc_NtkHasAig(pNtk) );
     // create the file name
     Abc_ShowGetFileName( pNtk->pName, FileNameDot );
     // check that the file can be opened
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 4745273e..16be21fd 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -86,6 +86,7 @@ static int Abc_CommandFpga         ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandPga          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandSeq          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandUnseq        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRetime       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandCec          ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -163,6 +164,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "FPGA mapping", "pga",           Abc_CommandPga,              1 );
 
     Cmd_CommandAdd( pAbc, "Sequential",   "seq",           Abc_CommandSeq,              1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "unseq",         Abc_CommandUnseq,            1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "retime",        Abc_CommandRetime,           1 );
 
     Cmd_CommandAdd( pAbc, "Verification", "cec",           Abc_CommandCec,              0 );
@@ -949,9 +951,9 @@ int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsStrash(pNtk) )
+    if ( !Abc_NtkHasAig(pNtk) )
     {
-        fprintf( pErr, "Visualizing AIG can only be done for AIGs (run \"strash\").\n" );
+        fprintf( pErr, "Visualizing AIG can only be done for AIGs (run \"strash\" or \"seq\").\n" );
         return 1;
     }
     Abc_NtkShowAig( pNtk );
@@ -3906,7 +3908,6 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
-    extern Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk );
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -3931,8 +3932,8 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    printf( "This command is not yet implemented.\n" );
-    return 0;
+//    printf( "This command is not yet implemented.\n" );
+//    return 0;
 
     if ( !Abc_NtkIsStrash(pNtk) )
     {
@@ -3959,7 +3960,81 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 usage:
     fprintf( pErr, "usage: seq [-h]\n" );
-    fprintf( pErr, "\t        converts AIG into sequential AIG (while sweeping latches)\n" );
+    fprintf( pErr, "\t        converts AIG into sequential AIG\n" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandUnseq( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+    int fShare;
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fShare = 1;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "sh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 's':
+            fShare ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsSeq(pNtk) )
+    {
+        fprintf( pErr, "Works only for sequential AIG (run \"seq\").\n" );
+        return 1;
+    }
+
+    // share the latches on the fanout edges
+    if ( fShare )
+        Abc_NtkSeqShareFanouts(pNtk);
+
+    // get the new network
+    pNtkRes = Abc_NtkSeqToLogicSop( pNtk );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Converting sequential AIG into an SOP logic network has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: unseq [-sh]\n" );
+    fprintf( pErr, "\t        converts sequential AIG into an SOP logic network\n" );
+    fprintf( pErr, "\t-s    : toggle sharing latches [default = %s]\n", fShare? "yes": "no" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -3991,7 +4066,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fForward  = 0;
+    fForward  = 1;
     fBackward = 0;
     fInitial  = 0;
     util_getopt_reset();
@@ -4021,10 +4096,6 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    printf( "This command is not yet implemented.\n" );
-    return 0;
-
-
     if ( !Abc_NtkIsSeq(pNtk) )
     {
         fprintf( pErr, "Works only for sequential AIG.\n" );
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index 20f41c56..01317d1d 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -501,7 +501,7 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
                 pLatch->pCopy = Abc_ObjNotCond( Abc_AigConst1(pNtkFrames->pManFunc), Abc_LatchIsInit0(pLatch) );
         }
         if ( Counter )
-            printf( "Warning: %d uninitialized latches are replaced by free variables.\n", Counter );
+            printf( "Warning: %d uninitialized latches are replaced by free PI variables.\n", Counter );
     }
     
     // create the timeframes
@@ -521,12 +521,18 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
         Abc_NtkForEachLatch( pNtk, pLatch, i )
         {
             pLatchNew = Abc_NtkLatch(pNtkFrames, i);
-            Abc_ObjAddFanin( pLatchNew, Abc_ObjFanin0(pLatch)->pCopy );
+            Abc_ObjAddFanin( pLatchNew, pLatch->pCopy );
             Vec_PtrPush( pNtkFrames->vCis, pLatchNew );
             Vec_PtrPush( pNtkFrames->vCos, pLatchNew );
             Abc_NtkLogicStoreName( pLatchNew, Abc_ObjName(pLatch) );
         }
     }
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+        pLatch->pNext = NULL;
+
+    // remove dangling nodes
+    Abc_AigCleanup( pNtkFrames->pManFunc );
+
     // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtkFrames ) )
     {
@@ -586,7 +592,9 @@ void Abc_NtkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_
     }
     // transfer the implementation of the latch drivers to the latches
     Abc_NtkForEachLatch( pNtk, pLatch, i )
-        pLatch->pCopy = Abc_ObjChild0Copy(pLatch);
+        pLatch->pNext = Abc_ObjChild0Copy(pLatch);
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+        pLatch->pCopy = pLatch->pNext;
 }
 
 
diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c
index 3d9534c8..421e3059 100644
--- a/src/base/abci/abcRefactor.c
+++ b/src/base/abci/abcRefactor.c
@@ -144,6 +144,8 @@ pManRef->timeTotal = clock() - clkStart;
     Abc_NtkManRefStop( pManRef );
     // put the nodes into the DFS order and reassign their IDs
     Abc_NtkReassignIds( pNtk );
+    Abc_AigRehash( pNtk->pManFunc );
+//    Abc_AigCheckFaninOrder( pNtk->pManFunc );
     // fix the levels
     if ( fUpdateLevel )
         Abc_NtkStopReverseLevels( pNtk );
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index 91a99a57..b70d30e6 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -115,6 +115,8 @@ Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart );
     pNtk->pManCut = NULL;
     // put the nodes into the DFS order and reassign their IDs
     Abc_NtkReassignIds( pNtk );
+    Abc_AigRehash( pNtk->pManFunc );
+//    Abc_AigCheckFaninOrder( pNtk->pManFunc );
     // fix the levels
     if ( fUpdateLevel )
         Abc_NtkStopReverseLevels( pNtk );
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index b335086f..e5bc2547 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -52,7 +52,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
     assert( Abc_NtkLatchNum(pNtk) == 0 );
 
     if ( Abc_NtkPoNum(pNtk) > 1 )
-        fprintf( stdout, "Warning: The miter has more than 1 output. SAT will try to prove all of them.\n" );
+        fprintf( stdout, "Warning: The miter has %d outputs. SAT will try to prove all of them.\n", Abc_NtkPoNum(pNtk) );
 
     // load clauses into the solver
     clk = clock();
@@ -65,11 +65,11 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
     status = solver_simplify(pSat);
 //    printf( "Simplified the problem to %d variables and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) );
 //    PRT( "Time", clock() - clk );
-    if ( status == l_False )
+    if ( status == 0 )
     {
         solver_delete( pSat );
-        printf( "The problem is UNSATISFIABLE after simplification.\n" );
-        return 0;
+//        printf( "The problem is UNSATISFIABLE after simplification.\n" );
+        return -1;
     }
 
     // solve the miter
@@ -146,8 +146,10 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
         Abc_NodeAddClauses( pSat, pSop0, pSop1, pNode, vVars );
     }
     // add clauses for each PO
-    Abc_NtkForEachPo( pNtk, pNode, i )
-        Abc_NodeAddClausesTop( pSat, pNode, vVars );
+//    Abc_NtkForEachPo( pNtk, pNode, i )
+//        Abc_NodeAddClausesTop( pSat, pNode, vVars );
+
+    Abc_NodeAddClausesTop( pSat, Abc_NtkPo(pNtk, Abc_NtkPoNum(pNtk)-1), vVars );
 
     // delete
     Vec_StrFree( vCube );
diff --git a/src/base/abcs/abcRetImpl.c b/src/base/abcs/abcRetImpl.c
index 84b386bb..ea849c1c 100644
--- a/src/base/abcs/abcRetImpl.c
+++ b/src/base/abcs/abcRetImpl.c
@@ -224,7 +224,7 @@ void Abc_ObjRetimeForward( Abc_Obj_t * pObj )
         Init = ABC_INIT_DC;
     // add the init values to the fanouts
     Abc_ObjForEachFanout( pObj, pFanout, i )
-        Abc_ObjFaninLInsertLast( pFanout, Abc_ObjEdgeNum(pFanout, pObj), Init );
+        Abc_ObjFaninLInsertLast( pFanout, Abc_ObjEdgeNum(pObj, pFanout), Init );
 }
 
 /**Function*************************************************************
diff --git a/src/base/abcs/abcSeq.c b/src/base/abcs/abcSeq.c
index 3b266182..4a29fe0e 100644
--- a/src/base/abcs/abcSeq.c
+++ b/src/base/abcs/abcSeq.c
@@ -73,18 +73,21 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkNew;
     Vec_Ptr_t * vNodes;
-    Abc_Obj_t * pObj, * pFanin;
-    int i, Init, nLatches;
+    Abc_Obj_t * pObj, * pFaninNew;
+    unsigned Init;
+    int i, nLatches;
     // make sure it is an AIG without self-feeding latches
     assert( Abc_NtkIsStrash(pNtk) );
     assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 );
     // start the network
+    Abc_NtkCleanCopy( pNtk );
     pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG );
     // duplicate the name and the spec
     pNtkNew->pName = util_strsav(pNtk->pName);
     pNtkNew->pSpec = util_strsav(pNtk->pSpec);
     // clone const/PIs/POs
     Abc_NtkDupObj(pNtkNew, Abc_AigConst1(pNtk->pManFunc) );
+    pNtkNew->nNodes -= 1;
     Abc_NtkForEachPi( pNtk, pObj, i )
         Abc_NtkDupObj(pNtkNew, pObj);
     Abc_NtkForEachPo( pNtk, pObj, i )
@@ -98,8 +101,11 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
     vNodes = Abc_AigDfs( pNtk, 0, 0 );
     Vec_PtrForEachEntry( vNodes, pObj, i )
     {
+        if ( Abc_ObjFaninNum(pObj) != 2 )
+            continue;
         Abc_NtkDupObj(pNtkNew, pObj);
         pObj->pCopy->fPhase = pObj->fPhase; // needed for choices
+        pObj->pCopy->Level = pObj->Level; 
     }
     // relink the choice nodes
     Vec_PtrForEachEntry( vNodes, pObj, i )
@@ -114,20 +120,33 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
         // skip the constant and the PIs
         if ( Abc_ObjFaninNum(pObj) == 0 )
             continue;
+        if ( Abc_ObjIsLatch(pObj) )
+            continue;
         // process the first fanin
-        pFanin = Abc_NodeAigToSeq( pObj, 0, &nLatches, &Init );
-        Abc_ObjAddFanin( pObj->pCopy, Abc_ObjGetCopy(pFanin) );
+        pFaninNew = Abc_NodeAigToSeq( pObj, 0, &nLatches, &Init );
+        if ( nLatches > ABC_MAX_EDGE_LATCH )
+        {
+            printf( "The number of latches on an edge (%d) exceeds the limit (%d).\n", nLatches, ABC_MAX_EDGE_LATCH );
+            nLatches = ABC_MAX_EDGE_LATCH;
+        }
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
         Abc_ObjAddFaninL0( pObj->pCopy, nLatches );
-        Vec_IntWriteEntry( pNtkNew->vInits, 2 * i + 0, Init );
+        Vec_IntWriteEntry( pNtkNew->vInits, 2 * pObj->pCopy->Id + 0, Init );
         if ( Abc_ObjFaninNum(pObj) == 1 )
             continue;
         // process the second fanin
-        pFanin = Abc_NodeAigToSeq( pObj, 1, &nLatches, &Init );
-        Abc_ObjAddFanin( pObj->pCopy, Abc_ObjGetCopy(pFanin) );
+        pFaninNew = Abc_NodeAigToSeq( pObj, 1, &nLatches, &Init );
+        if ( nLatches > ABC_MAX_EDGE_LATCH )
+        {
+            printf( "The number of latches on an edge (%d) exceeds the limit (%d).\n", nLatches, ABC_MAX_EDGE_LATCH );
+            nLatches = ABC_MAX_EDGE_LATCH;
+        }
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
         Abc_ObjAddFaninL1( pObj->pCopy, nLatches );
-        Vec_IntWriteEntry( pNtkNew->vInits, 2 * i + 1, Init );
+        Vec_IntWriteEntry( pNtkNew->vInits, 2 * pObj->pCopy->Id + 1, Init );
     }
     // set the cutset composed of latch drivers
+    Vec_PtrFree( pNtkNew->vLats );
     pNtkNew->vLats = Abc_NtkAigCutsetCopy( pNtk );
     // copy EXDC and check correctness
     if ( pNtkNew->pExdc )
@@ -179,21 +198,24 @@ Vec_Ptr_t * Abc_NtkAigCutsetCopy( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 Abc_Obj_t * Abc_NodeAigToSeq( Abc_Obj_t * pObj, int Num, int * pnLatches, unsigned * pnInit )
 {
-    Abc_Obj_t * pFanin;
+    Abc_Obj_t * pFanin, * pFaninNew;
     Abc_InitType_t Init;
     // get the given fanin of the node
     pFanin = Abc_ObjFanin( pObj, Num );
+    // if fanin is the internal node, return its copy in the corresponding polarity
     if ( !Abc_ObjIsLatch(pFanin) )
     {
         *pnLatches = 0;
         *pnInit = 0;
-        return Abc_ObjChild( pObj, Num );
+        return Abc_ObjNotCond( pFanin->pCopy, Abc_ObjFaninC(pObj, Num) );
     }
-    pFanin = Abc_NodeAigToSeq( pFanin, 0, pnLatches, pnInit );
-    // get the new initial state
-    Init = Abc_LatchInit(pObj);
+    // fanin is a latch
+    // get the new fanins
+    pFaninNew = Abc_NodeAigToSeq( pFanin, 0, pnLatches, pnInit );
+    // get the initial state
+    Init = Abc_LatchInit(pFanin);
     // complement the initial state if the inv is retimed over the latch
-    if ( Abc_ObjIsComplement(pFanin) ) 
+    if ( Abc_ObjIsComplement(pFaninNew) ) 
     {
         if ( Init == ABC_INIT_ZERO )
             Init = ABC_INIT_ONE;
@@ -205,7 +227,7 @@ Abc_Obj_t * Abc_NodeAigToSeq( Abc_Obj_t * pObj, int Num, int * pnLatches, unsign
     // update the latch number and initial state
     (*pnLatches)++;
     (*pnInit) = ((*pnInit) << 2) | Init;
-    return Abc_ObjNotCond( pFanin, Abc_ObjFaninC(pObj,Num) );
+    return Abc_ObjNotCond( pFaninNew, Abc_ObjFaninC(pObj, Num) );
 }
 
 
@@ -225,16 +247,24 @@ Abc_Obj_t * Abc_NodeAigToSeq( Abc_Obj_t * pObj, int Num, int * pnLatches, unsign
 Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkNew; 
-    Abc_Obj_t * pObj, * pObjNew, * pFaninNew;
+    Abc_Obj_t * pObj, * pObjNew, * pFaninNew, * pConst1;
     int i, nCutNodes, nDigits;
     unsigned Init;
+    int nLatchMax = 0;
+
     assert( Abc_NtkIsSeq(pNtk) );
     // start the network without latches
     nCutNodes = pNtk->vLats->nSize; pNtk->vLats->nSize = 0;
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
     pNtk->vLats->nSize = nCutNodes;
     // create the constant node
-    Abc_NtkDupConst1( pNtk, pNtkNew );
+//    Abc_NtkDupConst1( pNtk, pNtkNew );
+    pConst1 = Abc_NtkObj(pNtk,0);
+    if ( !Abc_ObjIsNode(pConst1) )
+        pConst1 = NULL;
+    if ( pConst1 && Abc_ObjFanoutNum(pConst1) > 0 )
+        pConst1->pCopy = Abc_NodeCreateConst1( pNtkNew );
+
     // duplicate the nodes, create node functions
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
@@ -254,9 +284,12 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
     // connect the objects
     Abc_NtkForEachObj( pNtk, pObj, i )
     {
+        assert( (int)pObj->Id == i );
         // skip PIs and the constant
         if ( Abc_ObjFaninNum(pObj) == 0 )
             continue;
+        if ( nLatchMax < Abc_ObjFaninL0(pObj) )
+            nLatchMax = Abc_ObjFaninL0(pObj);
         // get the initial states of the latches on the fanin edge of this node
         Init = Vec_IntEntry( pNtk->vInits, 2 * pObj->Id );
         // create the edge
@@ -269,6 +302,8 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
                 Abc_ObjSetFaninC( pObj->pCopy, 0 );
             continue;
         }
+        if ( nLatchMax < Abc_ObjFaninL0(pObj) )
+            nLatchMax = Abc_ObjFaninL0(pObj);
         // get the initial states of the latches on the fanin edge of this node
         Init = Vec_IntEntry( pNtk->vInits, 2 * pObj->Id + 1 );
         // create the edge
@@ -276,6 +311,7 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
         Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
         // the complemented edges are subsumed by the node function
     }
+    printf( "The max edge latch num = %d.\n", nLatchMax );
     // count the number of digits in the latch names
     nDigits = Extra_Base10Log( Abc_NtkLatchNum(pNtkNew) );
     // add the latches and their names
@@ -289,11 +325,8 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
     }
     // fix the problem with complemented and duplicated CO edges
     Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
-    // duplicate the EXDC network
-    if ( pNtk->pExdc )
-        fprintf( stdout, "Warning: EXDC network is not copied.\n" );
     if ( !Abc_NtkCheck( pNtkNew ) )
-        fprintf( stdout, "Abc_NtkSeqToLogic(): Network check has failed.\n" );
+        fprintf( stdout, "Abc_NtkSeqToLogicSop(): Network check has failed.\n" );
     return pNtkNew;
 }
 
@@ -313,7 +346,10 @@ Abc_Obj_t * Abc_NodeSeqToLogic( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pFanin, int nLa
 {
     Abc_Obj_t * pLatch;
     if ( nLatches == 0 )
+    {
+        assert( pFanin->pCopy );
         return pFanin->pCopy;
+    }
     pFanin = Abc_NodeSeqToLogic( pNtkNew, pFanin, nLatches - 1, Init >> 2 );
     pLatch = Abc_NtkCreateLatch( pNtkNew );
     pLatch->pData = (void *)(Init & 3);
diff --git a/src/base/abcs/abcShare.c b/src/base/abcs/abcShare.c
index 4f12b7bc..d74d2577 100644
--- a/src/base/abcs/abcShare.c
+++ b/src/base/abcs/abcShare.c
@@ -25,7 +25,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 static void Abc_NodeSeqShareFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
-static void Abc_NodeSeqShareOne( Abc_Obj_t * pNode, int Init, Vec_Ptr_t * vNodes );
+static void Abc_NodeSeqShareOne( Abc_Obj_t * pNode, Abc_InitType_t Init, Vec_Ptr_t * vNodes );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -124,6 +124,8 @@ void Abc_NodeSeqShareOne( Abc_Obj_t * pNode, Abc_InitType_t Init, Vec_Ptr_t * vN
     Vec_PtrClear( vNodes );
     Abc_ObjForEachFanout( pNode, pFanout, i )
     {
+        if ( Abc_ObjFanoutL(pNode, pFanout) == 0 )
+            continue;
         Type = Abc_ObjFaninLGetInitLast( pFanout, Abc_ObjEdgeNum(pNode, pFanout) );
         if ( Type == Init )
             InitNew = Init;
diff --git a/src/base/abcs/abcUtils.c b/src/base/abcs/abcUtils.c
index a9f3254c..6b42b9a9 100644
--- a/src/base/abcs/abcUtils.c
+++ b/src/base/abcs/abcUtils.c
@@ -76,6 +76,41 @@ int Abc_NtkSeqLatchNumShared( Abc_Ntk_t * pNtk )
     return Counter;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Generates the printable edge label with the initial state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_ObjFaninGetInitPrintable( Abc_Obj_t * pObj, int Edge )
+{
+    static char Buffer[ABC_MAX_EDGE_LATCH + 1];
+    Abc_InitType_t Init;
+    int nLatches, i;
+
+    nLatches = Abc_ObjFaninL( pObj, Edge );
+    assert( nLatches <= ABC_MAX_EDGE_LATCH );
+    for ( i = 0; i < nLatches; i++ )
+    {
+        Init = Abc_ObjFaninLGetInitOne( pObj, Edge, i );
+        if ( Init == ABC_INIT_NONE )
+            Buffer[i] = '_';
+        else if ( Init == ABC_INIT_ZERO )
+            Buffer[i] = '0';
+        else if ( Init == ABC_INIT_ONE )
+            Buffer[i] = '1';
+        else if ( Init == ABC_INIT_DC )
+            Buffer[i] = 'x';
+        else assert( 0 );
+    }
+    Buffer[nLatches] = 0;
+    return Buffer;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abcs/abc_.c b/src/base/abcs/abc_.c
deleted file mode 100644
index bef3836f..00000000
--- a/src/base/abcs/abc_.c
+++ /dev/null
@@ -1,47 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [abc_.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Network and node package.]
-
-  Synopsis    []
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: abc_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
- 
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/base/abcs/abcs.h b/src/base/abcs/abcs.h
index ba0442c0..024fe57a 100644
--- a/src/base/abcs/abcs.h
+++ b/src/base/abcs/abcs.h
@@ -164,11 +164,17 @@ static inline void Abc_ObjFaninLSetInit( Abc_Obj_t * pObj, int Edge, unsigned In
     Vec_IntWriteEntry( pObj->pNtk->vInits, 2 * pObj->Id + Edge, Init );
 }
 
+// getting the init value of the given latch on the edge
+static inline Abc_InitType_t Abc_ObjFaninLGetInitOne( Abc_Obj_t * pObj, int Edge, int iLatch )  
+{
+    return 0x3 & (Abc_ObjFaninLGetInit(pObj, Edge) >> (2*iLatch));
+}
+
 // setting the init value of the given latch on the edge
 static inline void Abc_ObjFaninLSetInitOne( Abc_Obj_t * pObj, int Edge, int iLatch, Abc_InitType_t Init )  
 {
     unsigned EntryCur = Abc_ObjFaninLGetInit(pObj, Edge);
-    unsigned EntryNew = (EntryCur & ~(0x3 << iLatch)) | (Init << iLatch);
+    unsigned EntryNew = (EntryCur & ~(0x3 << (2*iLatch))) | (Init << (2*iLatch));
     assert( iLatch < Abc_ObjFaninL(pObj, Edge) );
     Abc_ObjFaninLSetInit( pObj, Edge, EntryNew );
 }
@@ -305,7 +311,7 @@ extern void               Abc_NtkSeqShareFanouts( Abc_Ntk_t * pNtk );
 /*=== abcUtil.c ==============================================================*/
 extern int                Abc_NtkSeqLatchNum( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkSeqLatchNumShared( Abc_Ntk_t * pNtk );
-
+extern char *             Abc_ObjFaninGetInitPrintable( Abc_Obj_t * pObj, int Edge );
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 89703214..7a6ca49f 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -876,9 +876,9 @@ int IoCommandWriteDot( Abc_Frame_t * pAbc, int argc, char **argv )
         return 0;
     }
 
-    if ( !Abc_NtkIsStrash(pAbc->pNtkCur) )
+    if ( !Abc_NtkHasAig(pAbc->pNtkCur) )
     {
-        fprintf( stdout, "IoCommandWriteDot(): Currently can only process logic networks with BDDs.\n" );
+        fprintf( stdout, "IoCommandWriteDot(): Currently can only process AIGs.\n" );
         return 0;
     }
 
diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c
index 97258c81..cd297db7 100644
--- a/src/base/io/ioWriteDot.c
+++ b/src/base/io/ioWriteDot.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "io.h"
+#include "abcs.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -191,7 +192,7 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow,
         fprintf( pFile, "  rank = same;\n" );
         // the labeling node of this level
         fprintf( pFile, "  Level%d;\n",  LevelMax );
-        // generat the PO nodes
+        // generate the PO nodes
         Vec_PtrForEachEntry( vNodes, pNode, i )
         {
             if ( !Abc_ObjIsCo(pNode) )
@@ -242,7 +243,19 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow,
         Vec_PtrForEachEntry( vNodes, pNode, i )
         {
             if ( !Abc_ObjIsCi(pNode) )
+            {
+                // check if the costant node is present
+                if ( Abc_ObjFaninNum(pNode) == 0 && Abc_ObjFanoutNum(pNode) > 0 )
+                {
+                    fprintf( pFile, "  Node%d [label = \"Const1\"", pNode->Id );
+                    fprintf( pFile, ", shape = ellipse" );
+                    if ( pNode->fMarkB )
+                        fprintf( pFile, ", style = filled" );
+                    fprintf( pFile, ", color = coral, fillcolor = coral" );
+                    fprintf( pFile, "];\n" );
+                }
                 continue;
+            }
             fprintf( pFile, "  Node%d%s [label = \"%s%s\"", pNode->Id, 
                 (Abc_ObjIsLatch(pNode)? "_out":""), Abc_ObjName(pNode), (Abc_ObjIsLatch(pNode)? "_out":"") );
             fprintf( pFile, ", shape = %s", (Abc_ObjIsLatch(pNode)? "box":"triangle") );
@@ -277,7 +290,11 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow,
             fprintf( pFile, "Node%d%s",  pNode->Id, (Abc_ObjIsLatch(pNode)? "_in":"") );
             fprintf( pFile, " -> " );
             fprintf( pFile, "Node%d%s",  Abc_ObjFaninId0(pNode), (Abc_ObjIsLatch(Abc_ObjFanin0(pNode))? "_out":"") );
-            fprintf( pFile, " [style = %s]", Abc_ObjFaninC0(pNode)? "dotted" : "bold" );
+            fprintf( pFile, " [" );
+            fprintf( pFile, "style = %s", Abc_ObjFaninC0(pNode)? "dotted" : "bold" );
+            if ( Abc_ObjFaninL0(pNode) > 0 )
+            fprintf( pFile, ", label = \"%s\"", Abc_ObjFaninGetInitPrintable(pNode,0) );
+            fprintf( pFile, "]" );
             fprintf( pFile, ";\n" );
         }
         if ( Abc_ObjFaninNum(pNode) == 1 )
@@ -288,7 +305,11 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow,
             fprintf( pFile, "Node%d",  pNode->Id );
             fprintf( pFile, " -> " );
             fprintf( pFile, "Node%d%s",  Abc_ObjFaninId1(pNode), (Abc_ObjIsLatch(Abc_ObjFanin1(pNode))? "_out":"") );
-            fprintf( pFile, " [style = %s]", Abc_ObjFaninC1(pNode)? "dotted" : "bold" );
+            fprintf( pFile, " [" );
+            fprintf( pFile, "style = %s", Abc_ObjFaninC1(pNode)? "dotted" : "bold" );
+            if ( Abc_ObjFaninL1(pNode) > 0 )
+            fprintf( pFile, ", label = \"%s\"", Abc_ObjFaninGetInitPrintable(pNode,1) );
+            fprintf( pFile, "]" );
             fprintf( pFile, ";\n" );
         }
         // generate the edges between the equivalent nodes
diff --git a/src/base/main/libSupport.c b/src/base/main/libSupport.c
new file mode 100644
index 00000000..51c137cf
--- /dev/null
+++ b/src/base/main/libSupport.c
@@ -0,0 +1,164 @@
+/**CFile****************************************************************
+
+  FileName    [libSupport.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The main package.]
+
+  Synopsis    [Support for external libaries.]
+
+  Author      [Mike Case]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: libSupport.c,v 1.1 2005/09/06 19:59:51 casem Exp $]
+
+***********************************************************************/
+
+#include "mainInt.h"
+#include <stdio.h>
+#include <string.h>
+
+#ifndef WIN32
+# include <sys/types.h>
+# include <dirent.h>
+# include <dlfcn.h>
+#endif
+
+#define MAX_LIBS 256
+static void* libHandles[MAX_LIBS+1]; // will be null terminated
+
+typedef void (*lib_init_end_func) (Abc_Frame_t * pAbc);
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+// This will find all the ABC library extensions in the current directory and load them all.
+////////////////////////////////////////////////////////////////////////////////////////////////////
+void open_libs() {
+    int curr_lib = 0;
+
+#ifdef WIN32
+    printf("Warning: open_libs WIN32 not implemented.\n");
+#else
+    DIR* dirp;
+    struct dirent* dp;
+
+    dirp = opendir(".");
+    while ((dp = readdir(dirp)) != NULL) {
+        if ((strncmp("libabc_", dp->d_name, 7) == 0) &&
+            (strcmp(".so", dp->d_name + strlen(dp->d_name) - 3) == 0)) {
+
+            // make sure we don't overflow the handle array
+            if (curr_lib >= MAX_LIBS) {
+                printf("Warning: maximum number of ABC libraries (%d) exceeded.  Not loading %s.\n",
+                       MAX_LIBS,
+                       dp->d_name);
+            }
+
+            // attempt to load it
+            else {
+                char* szPrefixed = malloc((strlen(dp->d_name) + 3) * sizeof(char));
+                strcpy(szPrefixed, "./");
+                strcat(szPrefixed, dp->d_name);
+
+                libHandles[curr_lib] = dlopen(szPrefixed, RTLD_NOW | RTLD_LOCAL);
+
+                // did the load succeed?
+                if (libHandles[curr_lib] != 0) {
+                    printf("Loaded ABC library: %s (Abc library extension #%d)\n", szPrefixed, curr_lib);
+                    curr_lib++;
+                } else {
+                    printf("Warning: failed to load ABC library %s:\n\t%s\n", szPrefixed, dlerror());
+                }
+
+                free(szPrefixed);
+            }
+        }
+    }
+    closedir(dirp);
+#endif
+
+    // null terminate the list of handles
+    libHandles[curr_lib] = 0;    
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+// This will close all open ABC library extensions
+////////////////////////////////////////////////////////////////////////////////////////////////////
+void close_libs() {
+#ifdef WIN32
+    printf("Warning: close_libs WIN32 not implemented.\n");
+#else
+    int i;
+    for (i = 0; libHandles[i] != 0; i++) {
+        if (dlclose(libHandles[i]) != 0) {
+            printf("Warning: failed to close library %d\n", i);
+        }
+        libHandles[i] = 0;
+    }
+#endif
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+// This will get a pointer to a function inside of an open library
+////////////////////////////////////////////////////////////////////////////////////////////////////
+void* get_fnct_ptr(int lib_num, char* sym_name) {
+#ifdef WIN32
+    printf("Warning: get_fnct_ptr WIN32 not implemented.\n");
+    return 0;
+#else
+    return dlsym(libHandles[lib_num], sym_name);
+#endif
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+// This will call an initialization function in every open library.
+////////////////////////////////////////////////////////////////////////////////////////////////////
+void call_inits(Abc_Frame_t* pAbc) {
+    int i;
+    lib_init_end_func init_func;
+    for (i = 0; libHandles[i] != 0; i++) {
+        init_func = (lib_init_end_func) get_fnct_ptr(i, "abc_init");
+        if (init_func == 0) {
+            printf("Warning: Failed to initialize library %d.\n", i);
+        } else {
+            (*init_func)(pAbc);
+        }
+    }
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+// This will call a shutdown function in every open library.
+////////////////////////////////////////////////////////////////////////////////////////////////////
+void call_ends(Abc_Frame_t* pAbc) {
+    int i;
+    lib_init_end_func end_func;
+    for (i = 0; libHandles[i] != 0; i++) {
+        end_func = (lib_init_end_func) get_fnct_ptr(i, "abc_end");
+        if (end_func == 0) {
+            printf("Warning: Failed to end library %d.\n", i);
+        } else {
+            (*end_func)(pAbc);
+        }
+    }
+}
+
+void Libs_Init(Abc_Frame_t * pAbc)
+{
+    open_libs();
+    call_inits(pAbc);
+}
+
+void Libs_End(Abc_Frame_t * pAbc)
+{
+    call_ends(pAbc);
+
+    // It's good practice to close our libraries at this point, but this can mess up any backtrace printed by Valgind.
+    //    close_libs();
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
diff --git a/src/base/main/main.c b/src/base/main/main.c
index 43ad6956..6668d088 100644
--- a/src/base/main/main.c
+++ b/src/base/main/main.c
@@ -216,7 +216,7 @@ int main( int argc, char * argv[] )
     }
      
     // if the memory should be freed, quit packages
-    if ( fStatus == -2 ) 
+    if ( fStatus < 0 ) 
     {
         // perform uninitializations
         Abc_FrameEnd( pAbc );
diff --git a/src/base/main/mainInit.c b/src/base/main/mainInit.c
index 13710dcb..186d58fe 100644
--- a/src/base/main/mainInit.c
+++ b/src/base/main/mainInit.c
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: mainInit.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: mainInit.c,v 1.3 2005/09/14 22:53:37 casem Exp $]
 
 ***********************************************************************/
 
@@ -38,6 +38,8 @@ extern void Mio_Init( Abc_Frame_t * pAbc );
 extern void Mio_End ( Abc_Frame_t * pAbc );
 extern void Super_Init( Abc_Frame_t * pAbc );
 extern void Super_End ( Abc_Frame_t * pAbc );
+extern void Libs_Init(Abc_Frame_t * pAbc);
+extern void Libs_End(Abc_Frame_t * pAbc);
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -63,6 +65,7 @@ void Abc_FrameInit( Abc_Frame_t * pAbc )
     Map_Init( pAbc );
     Mio_Init( pAbc );
     Super_Init( pAbc );
+    Libs_Init( pAbc );
 }
 
 
@@ -86,6 +89,7 @@ void Abc_FrameEnd( Abc_Frame_t * pAbc )
     Map_End( pAbc );
     Mio_End( pAbc );
     Super_End( pAbc );
+    Libs_End( pAbc );
 }
 
 
diff --git a/src/base/main/module.make b/src/base/main/module.make
index 59e1315e..7a04e533 100644
--- a/src/base/main/module.make
+++ b/src/base/main/module.make
@@ -1,4 +1,5 @@
 SRC +=  src/base/main/main.c \
     src/base/main/mainFrame.c \
     src/base/main/mainInit.c \
-    src/base/main/mainUtils.c
+    src/base/main/mainUtils.c \
+    src/base/main/libSupport.c
diff --git a/src/bdd/dsd/dsdProc.c b/src/bdd/dsd/dsdProc.c
index 08c029e1..543ad387 100644
--- a/src/bdd/dsd/dsdProc.c
+++ b/src/bdd/dsd/dsdProc.c
@@ -1255,7 +1255,7 @@ EXIT:
     s_CacheEntries++;
 
 
-#if 0
+/*
     if ( dsdKernelVerifyDecomposition(dd, pThis) == 0 )
     {
         // write the function, for which verification does not work
@@ -1277,7 +1277,7 @@ EXIT:
         cuddWriteFunctionSop( stdout, dd, zNewFunc, -1, dd->size, "1", s_pVarMask );
         Cudd_RecursiveDerefZdd( dd, zNewFunc );
     }
-#endif
+*/
 
     }
 
diff --git a/src/map/pga/pgaMan.c b/src/map/pga/pgaMan.c
index d7573ecf..b75a26c6 100644
--- a/src/map/pga/pgaMan.c
+++ b/src/map/pga/pgaMan.c
@@ -75,6 +75,7 @@ Pga_Man_t * Pga_ManStart( Pga_Params_t * pParams )
     {
         printf( "The nodes of the network are not DFS ordered.\n" );
 //        Abc_NtkReassignIds( pNtk );
+//        Abc_AigRehash( pNtk->pManFunc );
         return NULL;
     }
     // make sure there are no dangling nodes (unless they are choices)
diff --git a/src/misc/vec/vecVec.h b/src/misc/vec/vecVec.h
index 0ad5fd1e..9179336f 100644
--- a/src/misc/vec/vecVec.h
+++ b/src/misc/vec/vecVec.h
@@ -50,13 +50,13 @@ struct Vec_Vec_t_
 
 // iterators through levels 
 #define Vec_VecForEachLevel( vGlob, vVec, i )                                                 \
-    for ( i = 0; (i < Vec_VecSize(vGlob)) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ )
+    for ( i = 0; (i < Vec_VecSize(vGlob)) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ )
 #define Vec_VecForEachLevelStart( vGlob, vVec, i, LevelStart )                                \
-    for ( i = LevelStart; (i < Vec_VecSize(vGlob)) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ )
+    for ( i = LevelStart; (i < Vec_VecSize(vGlob)) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ )
 #define Vec_VecForEachLevelStartStop( vGlob, vVec, i, LevelStart, LevelStop )                 \
-    for ( i = LevelStart; (i <= LevelStop) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ )
+    for ( i = LevelStart; (i <= LevelStop) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ )
 #define Vec_VecForEachLevelReverse( vGlob, vVec, i )                                          \
-    for ( i = Vec_VecSize(vGlob) - 1; (i >= 0) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i-- )
+    for ( i = Vec_VecSize(vGlob) - 1; (i >= 0) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i-- )
 
 // iteratores through entries
 #define Vec_VecForEachEntry( vGlob, pEntry, i, k )                                            \
@@ -234,7 +234,7 @@ static inline void Vec_VecPush( Vec_Vec_t * p, int Level, void * Entry )
             p->pArray[i] = Vec_PtrAlloc( 0 );
         p->nSize = Level + 1;
     }
-    Vec_PtrPush( p->pArray[Level], Entry );
+    Vec_PtrPush( (Vec_Ptr_t*)p->pArray[Level], Entry );
 }
 
 /**Function*************************************************************
@@ -253,7 +253,7 @@ static inline void Vec_VecPushUnique( Vec_Vec_t * p, int Level, void * Entry )
     if ( p->nSize < Level + 1 )
         Vec_VecPush( p, Level, Entry );
     else
-        Vec_PtrPushUnique( p->pArray[Level], Entry );
+        Vec_PtrPushUnique( (Vec_Ptr_t*)p->pArray[Level], Entry );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/asat/solver.c b/src/sat/asat/solver.c
index 98024a7f..d248b115 100644
--- a/src/sat/asat/solver.c
+++ b/src/sat/asat/solver.c
@@ -317,11 +317,11 @@ static void clause_remove(solver* s, clause* c)
     vec_remove(solver_read_wlist(s,neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
 
     if (clause_learnt(c)){
-        s->stats.learnts--;
-        s->stats.learnts_literals -= clause_size(c);
+        s->solver_stats.learnts--;
+        s->solver_stats.learnts_literals -= clause_size(c);
     }else{
-        s->stats.clauses--;
-        s->stats.clauses_literals -= clause_size(c);
+        s->solver_stats.clauses--;
+        s->solver_stats.clauses_literals -= clause_size(c);
     }
 
     free(c);
@@ -409,7 +409,7 @@ static inline bool enqueue(solver* s, lit l, clause* from)
         s->trail[s->qtail++] = l;
 
         order_assigned(s, v);
-        return true;
+        return 1;
     }
 }
 
@@ -465,8 +465,8 @@ static void solver_record(solver* s, vec* cls)
     if (c != 0) {
         vec_push(&s->learnts,(void*)c);
         act_clause_bump(s,c);
-        s->stats.learnts++;
-        s->stats.learnts_literals += vec_size(cls);
+        s->solver_stats.learnts++;
+        s->solver_stats.learnts_literals += vec_size(cls);
     }
 }
 
@@ -521,7 +521,7 @@ static bool solver_lit_removable(solver* s, lit l, int minl)
                     for (j = top; j < vec_size(&s->tagged); j++)
                         tags[tagged[j]] = l_Undef;
                     vec_resize(&s->tagged,top);
-                    return false;
+                    return 0;
                 }
             }
         }else{
@@ -541,14 +541,14 @@ static bool solver_lit_removable(solver* s, lit l, int minl)
                         for (j = top; j < vec_size(&s->tagged); j++)
                             tags[tagged[j]] = l_Undef;
                         vec_resize(&s->tagged,top);
-                        return false;
+                        return 0;
                     }
                 }
             }
         }
     }
 
-    return true;
+    return 1;
 }
 
 static void solver_analyze(solver* s, clause* c, vec* learnt)
@@ -627,9 +627,9 @@ static void solver_analyze(solver* s, clause* c, vec* learnt)
     }
 
     // update size of learnt + statistics
-    s->stats.max_literals += vec_size(learnt);
+    s->solver_stats.max_literals += vec_size(learnt);
     vec_resize(learnt,j);
-    s->stats.tot_literals += j;
+    s->solver_stats.tot_literals += j;
 
     // clear tags
     tagged = (int*)vec_begin(&s->tagged);
@@ -684,7 +684,7 @@ clause* solver_propagate(solver* s)
         clause **end   = begin + vec_size(ws);
         clause **i, **j;
 
-        s->stats.propagations++;
+        s->solver_stats.propagations++;
         s->simpdb_props--;
 
         //printf("checking lit %d: "L_LIT"\n", vec_size(ws), L_lit(p));
@@ -746,7 +746,7 @@ clause* solver_propagate(solver* s)
             i++;
         }
 
-        s->stats.inspects += j - (clause**)vec_begin(ws);
+        s->solver_stats.inspects += j - (clause**)vec_begin(ws);
         vec_resize(ws,j - (clause**)vec_begin(ws));
     }
 
@@ -796,7 +796,7 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
 
     assert(s->root_level == solver_dlevel(s));
 
-    s->stats.starts++;
+    s->solver_stats.starts++;
     s->var_decay = (float)(1 / var_decay   );
     s->cla_decay = (float)(1 / clause_decay);
     vec_resize(&s->model,0);
@@ -811,7 +811,7 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
 #ifdef VERBOSEDEBUG
             printf(L_IND"**CONFLICT**\n", L_ind);
 #endif
-            s->stats.conflicts++; conflictC++;
+            s->solver_stats.conflicts++; conflictC++;
             if (solver_dlevel(s) == s->root_level){
                 vec_delete(&learnt_clause);
                 return l_False;
@@ -845,7 +845,7 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
                 solver_reducedb(s);
 
             // New variable decision:
-            s->stats.decisions++;
+            s->solver_stats.decisions++;
             next = order_select(s,(float)random_var_freq);
 
             if (next == var_Undef){
@@ -910,17 +910,17 @@ solver* solver_new(void)
     s->binary->size_learnt    = (2 << 1);
     s->verbosity              = 0;
 
-    s->stats.starts           = 0;
-    s->stats.decisions        = 0;
-    s->stats.propagations     = 0;
-    s->stats.inspects         = 0;
-    s->stats.conflicts        = 0;
-    s->stats.clauses          = 0;
-    s->stats.clauses_literals = 0;
-    s->stats.learnts          = 0;
-    s->stats.learnts_literals = 0;
-    s->stats.max_literals     = 0;
-    s->stats.tot_literals     = 0;
+    s->solver_stats.starts           = 0;
+    s->solver_stats.decisions        = 0;
+    s->solver_stats.propagations     = 0;
+    s->solver_stats.inspects         = 0;
+    s->solver_stats.conflicts        = 0;
+    s->solver_stats.clauses          = 0;
+    s->solver_stats.clauses_literals = 0;
+    s->solver_stats.learnts          = 0;
+    s->solver_stats.learnts_literals = 0;
+    s->solver_stats.max_literals     = 0;
+    s->solver_stats.tot_literals     = 0;
 
     return s;
 }
@@ -973,7 +973,7 @@ bool solver_addclause(solver* s, lit* begin, lit* end)
     lbool* values;
     lit last;
 
-    if (begin == end) return false;
+    if (begin == end) return 0;
 
     //printlits(begin,end); printf("\n");
     // insertion sort
@@ -996,7 +996,7 @@ bool solver_addclause(solver* s, lit* begin, lit* end)
         //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]));
         lbool sig = !lit_sign(*i); sig += sig - 1;
         if (*i == neg(last) || sig == values[lit_var(*i)])
-            return true;   // tautology
+            return 1;   // tautology
         else if (*i != last && values[lit_var(*i)] == l_Undef)
             last = *j++ = *i;
     }
@@ -1004,7 +1004,7 @@ bool solver_addclause(solver* s, lit* begin, lit* end)
     //printf("final: "); printlits(begin,j); printf("\n");
 
     if (j == begin)          // empty clause
-        return false;
+        return 0;
     else if (j - begin == 1) // unit clause
         return enqueue(s,*begin,(clause*)0);
 
@@ -1012,10 +1012,10 @@ bool solver_addclause(solver* s, lit* begin, lit* end)
     vec_push(&s->clauses,clause_new(s,begin,j,0));
 
 
-    s->stats.clauses++;
-    s->stats.clauses_literals += j - begin;
+    s->solver_stats.clauses++;
+    s->solver_stats.clauses_literals += j - begin;
 
-    return true;
+    return 1;
 }
 
 
@@ -1027,10 +1027,10 @@ bool   solver_simplify(solver* s)
     assert(solver_dlevel(s) == 0);
 
     if (solver_propagate(s) != 0)
-        return false;
+        return 0;
 
     if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
-        return true;
+        return 1;
 
     reasons = s->reasons;
     for (type = 0; type < 2; type++){
@@ -1050,13 +1050,13 @@ bool   solver_simplify(solver* s)
 
     s->simpdb_assigns = s->qhead;
     // (shouldn't depend on 'stats' really, but it will do for now)
-    s->simpdb_props   = (int)(s->stats.clauses_literals + s->stats.learnts_literals);
+    s->simpdb_props   = (int)(s->solver_stats.clauses_literals + s->solver_stats.learnts_literals);
 
-    return true;
+    return 1;
 }
 
 
-int   solver_solve(solver* s, lit* begin, lit* end, int nSeconds)
+bool solver_solve(solver* s, lit* begin, lit* end, int nSeconds)
 {
     double  nof_conflicts = 100;
     double  nof_learnts   = solver_nclauses(s) / 3;
@@ -1068,7 +1068,7 @@ int   solver_solve(solver* s, lit* begin, lit* end, int nSeconds)
     for (i = begin; i < end; i++)
         if ((lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]) == l_False || (assume(s,*i), solver_propagate(s) != 0)){
             solver_canceluntil(s,0);
-            return false; }
+            return l_False; }
 
     s->root_level = solver_dlevel(s);
 
@@ -1080,17 +1080,17 @@ int   solver_solve(solver* s, lit* begin, lit* end, int nSeconds)
     }
 
     while (status == l_Undef){
-        double Ratio = (s->stats.learnts == 0)? 0.0 :
-            s->stats.learnts_literals / (double)s->stats.learnts;
+        double Ratio = (s->solver_stats.learnts == 0)? 0.0 :
+            s->solver_stats.learnts_literals / (double)s->solver_stats.learnts;
 
         if (s->verbosity >= 1){
             printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n", 
-                (double)s->stats.conflicts,
-                (double)s->stats.clauses, 
-                (double)s->stats.clauses_literals,
+                (double)s->solver_stats.conflicts,
+                (double)s->solver_stats.clauses, 
+                (double)s->solver_stats.clauses_literals,
                 (double)nof_learnts, 
-                (double)s->stats.learnts, 
-                (double)s->stats.learnts_literals,
+                (double)s->solver_stats.learnts, 
+                (double)s->solver_stats.learnts_literals,
                 Ratio,
                 s->progress_estimate*100);
             fflush(stdout);
diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h
index 8e981198..9f80bc7e 100644
--- a/src/sat/asat/solver.h
+++ b/src/sat/asat/solver.h
@@ -36,16 +36,13 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #define bool int
 #endif
 
-static const bool  true      = 1;
-static const bool  false     = 0;
-
 typedef int                lit;
 typedef char               lbool;
 
 #ifdef _WIN32
-typedef signed __int64  sint64;   // compatible with MS VS 6.0
+typedef signed __int64     sint64;   // compatible with MS VS 6.0
 #else
-typedef long long       sint64;
+typedef long long          sint64;
 #endif
 
 static const int   var_Undef = -1;
@@ -132,7 +129,7 @@ struct solver_t
     double   progress_estimate;
     int      verbosity;     // Verbosity level. 0=silent, 1=some progress report, 2=everything
 
-    stats    stats;
+    stats    solver_stats;
 };
 
 #endif
diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index fcb1018f..d54a3119 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/src/sat/fraig/fraigSat.c
@@ -123,26 +123,32 @@ void Fraig_ManProveMiter( Fraig_Man_t * p )
 int Fraig_ManCheckMiter( Fraig_Man_t * p )
 {
     Fraig_Node_t * pNode;
+    int i;
     FREE( p->pModel );
-    // get the output node (it can be complemented!)
-    pNode = p->vOutputs->pArray[0];
-    // if the miter is constant 0, the problem is UNSAT
-    if ( pNode == Fraig_Not(p->pConst1) )
-        return 1;
-    // consider the special case when the miter is constant 1
-    if ( pNode == p->pConst1 )
+    for ( i = 0; i < p->vOutputs->nSize; i++ )
     {
-        // in this case, any counter example will do to distinquish it from constant 0
-        // here we pick the counter example composed of all zeros
-        p->pModel = Fraig_ManAllocCounterExample( p );
-        return 0;
+        // get the output node (it can be complemented!)
+        pNode = p->vOutputs->pArray[i];
+        // if the miter is constant 0, the problem is UNSAT
+        if ( pNode == Fraig_Not(p->pConst1) )
+            continue;
+        // consider the special case when the miter is constant 1
+        if ( pNode == p->pConst1 )
+        {
+            // in this case, any counter example will do to distinquish it from constant 0
+            // here we pick the counter example composed of all zeros
+            p->pModel = Fraig_ManAllocCounterExample( p );
+            return 0;
+        }
+        // save the counter example
+        p->pModel = Fraig_ManSaveCounterExample( p, pNode );
+        // if the model is not found, return undecided
+        if ( p->pModel == NULL )
+            return -1;
+        else
+            return 0;
     }
-    // save the counter example
-    p->pModel = Fraig_ManSaveCounterExample( p, pNode );
-    // if the model is not found, return undecided
-    if ( p->pModel == NULL )
-        return -1;
-    return 0;
+    return 1;
 }