initial commit of public abc

19 files changed, 284 insertions, 157 deletions

diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index f661d2e5..b046cc47 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -21,6 +21,7 @@
 #ifndef __FRA_H__
 #define __FRA_H__
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -41,9 +42,10 @@
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
-#ifdef __cplusplus
-extern "C" {
-#endif 
+
+
+ABC_NAMESPACE_HEADER_START
+ 
 
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
@@ -55,7 +57,6 @@ typedef struct Fra_Sec_t_   Fra_Sec_t;
 typedef struct Fra_Man_t_   Fra_Man_t;
 typedef struct Fra_Cla_t_   Fra_Cla_t;
 typedef struct Fra_Sml_t_   Fra_Sml_t;
-typedef struct Fra_Cex_t_   Fra_Cex_t;
 typedef struct Fra_Bmc_t_   Fra_Bmc_t;
 
 // FRAIG parameters
@@ -180,17 +181,6 @@ struct Fra_Sml_t_
     unsigned         pData[0];          // simulation data for the nodes
 };
 
-// simulation manager
-struct Fra_Cex_t_
-{
-    int              iPo;               // the zero-based number of PO, for which verification failed
-    int              iFrame;            // the zero-based number of the time-frame, for which verificaiton failed
-    int              nRegs;             // the number of registers in the miter 
-    int              nPis;              // the number of primary inputs in the miter
-    int              nBits;             // the number of words of bit data used
-    unsigned         pData[0];          // the cex bit data (the number of bits: nRegs + (iFrame+1) * nPis)
-};
-
 // FRAIG manager
 struct Fra_Man_t_
 {
@@ -382,16 +372,18 @@ extern Fra_Sml_t *         Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrame
 extern void                Fra_SmlStop( Fra_Sml_t * p );
 extern Fra_Sml_t *         Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords, int fCheckMiter );
 extern Fra_Sml_t *         Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords );
-extern Fra_Cex_t *         Fra_SmlGetCounterExample( Fra_Sml_t * p );
-extern Fra_Cex_t *         Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel );
-extern void                Fra_SmlFreeCounterExample( Fra_Cex_t * p );
-extern Fra_Cex_t *         Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut );
-extern int                 Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_Cex_t * p );
-extern int                 Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Fra_Cex_t * p );
-
-#ifdef __cplusplus
-}
-#endif
+extern Abc_Cex_t *         Fra_SmlGetCounterExample( Fra_Sml_t * p );
+extern Abc_Cex_t *         Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel );
+extern void                Fra_SmlFreeCounterExample( Abc_Cex_t * p );
+extern Abc_Cex_t *         Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut );
+extern int                 Fra_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p );
+extern int                 Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Abc_Cex_t * p );
+extern Abc_Cex_t *         Fra_SmlSimpleCounterExample( Aig_Man_t * pAig, int * pModel, int iFrame, int iPo );
+
+
+ABC_NAMESPACE_HEADER_END
+
+
 
 #endif
 
diff --git a/src/aig/fra/fraBmc.c b/src/aig/fra/fraBmc.c
index 7b08d74d..ae9e4bc5 100644
--- a/src/aig/fra/fraBmc.c
+++ b/src/aig/fra/fraBmc.c
@@ -20,6 +20,9 @@
 
 #include "fra.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -68,7 +71,7 @@ static inline Aig_Obj_t *  Bmc_ObjChild1Frames( Aig_Obj_t * pObj, int i ) { asse
 ***********************************************************************/
 int Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
 {
-    Fra_Man_t * p = pObj0->pData;
+    Fra_Man_t * p = (Fra_Man_t *)pObj0->pData;
     Aig_Obj_t * pObjFrames0, * pObjFrames1;
     Aig_Obj_t * pObjFraig0, * pObjFraig1;
     int i;
@@ -99,7 +102,7 @@ int Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
 ***********************************************************************/
 int Fra_BmcNodeIsConst( Aig_Obj_t * pObj )
 {
-    Fra_Man_t * p = pObj->pData;
+    Fra_Man_t * p = (Fra_Man_t *)pObj->pData;
     return Fra_BmcNodesAreEqual( pObj, Aig_ManConst1(p->pManAig) );
 }
 
@@ -421,7 +424,7 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew
         iOutput = Fra_FraigMiterAssertedOutput( pBmc->pAigFraig );
         if ( pBmc->pAigFraig->pData )
         {
-            pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pBmc->pAigFrames, pBmc->pAigFraig->pData );
+            pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pBmc->pAigFrames, (int *)pBmc->pAigFraig->pData );
             ABC_FREE( pBmc->pAigFraig->pData );
         }
         else if ( iOutput >= 0 )
@@ -444,3 +447,5 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
index b7a78050..037e6c70 100644
--- a/src/aig/fra/fraCec.c
+++ b/src/aig/fra/fraCec.c
@@ -21,6 +21,9 @@
 #include "fra.h"
 #include "cnf.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -58,7 +61,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
         Cnf_DataTranformPolarity( pCnf, 0 );
 
     // convert into SAT solver
-    pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
     if ( pSat == NULL )
     {
         Cnf_DataFree( pCnf );
@@ -128,8 +131,9 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
     }
     else
         assert( 0 );
-//    ABC_PRT( "SAT sat_solver time", clock() - clk );
-//    printf( "The number of conflicts = %d.\n", (int)pSat->sat_solver_stats.conflicts );
+
+//    Abc_Print( 1, "The number of conflicts = %6d.  ", (int)pSat->stats.conflicts );
+//    Abc_PrintTime( 1, "Solving time", clock() - clk );
  
     // if the problem is SAT, get the counterexample
     if ( status == l_True )
@@ -283,7 +287,7 @@ int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimi
     vParts = Aig_ManMiterPartitioned( pMan1, pMan2, nPartSize, fSmart );
     // solve the partitions
     nOutputs = -1;
-    Vec_PtrForEachEntry( vParts, pAig, i )
+    Vec_PtrForEachEntry( Aig_Man_t *, vParts, pAig, i )
     {
         nOutputs++;
         if ( fVerbose )
@@ -319,7 +323,7 @@ int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimi
         fflush( stdout );
     }
     // free intermediate results
-    Vec_PtrForEachEntry( vParts, pAig, i )
+    Vec_PtrForEachEntry( Aig_Man_t *, vParts, pAig, i )
         Aig_ManStop( pAig );
     Vec_PtrFree( vParts );
     return RetValue;
@@ -395,3 +399,5 @@ ABC_PRT( "Time", clock() - clkTotal );
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index 94cac80a..9b1ad3f2 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -20,6 +20,9 @@
 
 #include "fra.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*
     The candidate equivalence classes are stored as a vector of pointers 
     to the array of pointers to the nodes in each class.
@@ -124,7 +127,7 @@ void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed )
         }
     }
     if ( vFailed )
-        Vec_PtrForEachEntry( vFailed, pObj, i )
+        Vec_PtrForEachEntry( Aig_Obj_t *, vFailed, pObj, i )
             p->pAig->pReprs[pObj->Id] = NULL;
 }
 
@@ -163,7 +166,7 @@ int Fra_ClassesCountLits( Fra_Cla_t * p )
     Aig_Obj_t ** pClass;
     int i, nNodes, nLits = 0;
     nLits = Vec_PtrSize( p->vClasses1 );
-    Vec_PtrForEachEntry( p->vClasses, pClass, i )
+    Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i )
     {
         nNodes = Fra_ClassCount( pClass );
         assert( nNodes > 1 );
@@ -187,7 +190,7 @@ int Fra_ClassesCountPairs( Fra_Cla_t * p )
 {
     Aig_Obj_t ** pClass;
     int i, nNodes, nPairs = 0;
-    Vec_PtrForEachEntry( p->vClasses, pClass, i )
+    Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i )
     {
         nNodes = Fra_ClassCount( pClass );
         assert( nNodes > 1 );
@@ -244,13 +247,13 @@ void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose )
 
     if ( fVeryVerbose )
     {
-        Vec_PtrForEachEntry( p->vClasses1, pObj, i )
+        Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i )
             assert( Fra_ClassObjRepr(pObj) == Aig_ManConst1(p->pAig) );
         printf( "Constants { " );
-        Vec_PtrForEachEntry( p->vClasses1, pObj, i )
+        Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i )
             printf( "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) );
         printf( "}\n" );
-        Vec_PtrForEachEntry( p->vClasses, pClass, i )
+        Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i )
         {
             printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) );
             Fra_PrintClass( p, pClass );
@@ -415,15 +418,15 @@ Aig_Obj_t ** Fra_RefineClassOne( Fra_Cla_t * p, Aig_Obj_t ** ppClass )
             Vec_PtrPush( p->vClassNew, pObj );
 /*
     printf( "Refining class (" );
-    Vec_PtrForEachEntry( p->vClassOld, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassOld, pObj, i )
         printf( "%d,", pObj->Id );
     printf( ") + (" );
-    Vec_PtrForEachEntry( p->vClassNew, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
         printf( "%d,", pObj->Id );
     printf( ")\n" );
 */
     // put the nodes back into the class memory
-    Vec_PtrForEachEntry( p->vClassOld, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassOld, pObj, i )
     {
         ppClass[i] = pObj;
         ppClass[Vec_PtrSize(p->vClassOld)+i] = NULL;
@@ -431,7 +434,7 @@ Aig_Obj_t ** Fra_RefineClassOne( Fra_Cla_t * p, Aig_Obj_t ** ppClass )
     }
     ppClass += 2*Vec_PtrSize(p->vClassOld);
     // put the new nodes into the class memory
-    Vec_PtrForEachEntry( p->vClassNew, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
     {
         ppClass[i] = pObj;
         ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
@@ -455,7 +458,7 @@ int Fra_RefineClassLastIter( Fra_Cla_t * p, Vec_Ptr_t * vClasses )
 {
     Aig_Obj_t ** pClass, ** pClass2;
     int nRefis;
-    pClass = Vec_PtrEntryLast( vClasses );
+    pClass = (Aig_Obj_t **)Vec_PtrEntryLast( vClasses );
     for ( nRefis = 0; (pClass2 = Fra_RefineClassOne( p, pClass )); nRefis++ )
     {
         // if the original class is trivial, remove it
@@ -495,7 +498,7 @@ int Fra_ClassesRefine( Fra_Cla_t * p )
     // refine the classes
     nRefis = 0;
     Vec_PtrClear( p->vClassesTemp );
-    Vec_PtrForEachEntry( p->vClasses, pClass, i )
+    Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i )
     {
         // add the class to the new array
         assert( pClass[0] != NULL );
@@ -533,7 +536,7 @@ int Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped )
     // collect all the nodes to be refined
     k = 0;
     Vec_PtrClear( p->vClassNew );
-    Vec_PtrForEachEntry( p->vClasses1, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i )
     {
         if ( p->pFuncNodeIsConst( pObj ) )
             Vec_PtrWriteEntry( p->vClasses1, k++, pObj );
@@ -545,19 +548,19 @@ int Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped )
         return 0;
 /*
     printf( "Refined const-1 class: {" );
-    Vec_PtrForEachEntry( p->vClassNew, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
         printf( " %d", pObj->Id );
     printf( " }\n" );
 */
     if ( Vec_PtrSize(p->vClassNew) == 1 )
     {
-        Fra_ClassObjSetRepr( Vec_PtrEntry(p->vClassNew,0), NULL );
+        Fra_ClassObjSetRepr( (Aig_Obj_t *)Vec_PtrEntry(p->vClassNew,0), NULL );
         return 1;
     }
     // create a new class composed of these nodes
     ppClass = p->pMemClassesFree;
     p->pMemClassesFree += 2 * Vec_PtrSize(p->vClassNew);
-    Vec_PtrForEachEntry( p->vClassNew, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
     {
         ppClass[i] = pObj;
         ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
@@ -658,7 +661,7 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p )
     printf( "Before: Const = %6d. Class = %6d.  ", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) );
     // remove nodes from classes whose weight is less than WeightMax/Ratio
     k = 0;
-    Vec_PtrForEachEntry( p->vClasses1, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i )
     {
         if ( pWeights[pObj->Id] >= WeightMax/Ratio )
             Vec_PtrWriteEntry( p->vClasses1, k++, pObj );
@@ -667,7 +670,7 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p )
     }
     Vec_PtrShrink( p->vClasses1, k );
     // in each class, compact the nodes
-    Vec_PtrForEachEntry( p->vClasses, ppClass, i )
+    Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, ppClass, i )
     {
         k = 1;
         for ( c = 1; ppClass[c]; c++ )
@@ -681,7 +684,7 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p )
     }
     // remove classes with only repr
     k = 0;
-    Vec_PtrForEachEntry( p->vClasses, ppClass, i )
+    Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, ppClass, i )
         if ( ppClass[1] != NULL )
             Vec_PtrWriteEntry( p->vClasses, k++, ppClass );
     Vec_PtrShrink( p->vClasses, k );
@@ -705,7 +708,7 @@ void Fra_ClassesSelectRepr( Fra_Cla_t * p )
     Aig_Obj_t ** pClass, * pNodeMin;
     int i, c, cMinSupp, nSuppSizeMin, nSuppSizeCur;
     // reassign representatives in each class
-    Vec_PtrForEachEntry( p->vClasses, pClass, i )
+    Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i )
     {
         // collect support sizes and find the min-support node
         cMinSupp = -1;
@@ -855,3 +858,5 @@ printf( "Assert miters = %6d. Output miters = %6d.\n",
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/fra/fraClau.c b/src/aig/fra/fraClau.c
index 96d06380..490c73ff 100644
--- a/src/aig/fra/fraClau.c
+++ b/src/aig/fra/fraClau.c
@@ -22,6 +22,9 @@
 #include "cnf.h"
 #include "satSolver.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*
     This code is inspired by the paper: Aaron Bradley and Zohar Manna, 
     "Checking safety by inductive generalization of counterexamples to 
@@ -233,7 +236,7 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan )
     Aig_ObjChild0Flip( Aig_ManPo(pFramesMain, 0) ); // complement the first output
     pCnfMain = Cnf_DeriveSimple( pFramesMain, 0 );
 //Cnf_DataWriteIntoFile( pCnfMain, "temp.cnf", 1 );
-    p->pSatMain = Cnf_DataWriteIntoSolver( pCnfMain, 1, 0 );
+    p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( pCnfMain, 1, 0 );
 /*
     {
         int i;
@@ -248,7 +251,7 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan )
     pFramesTest = Aig_ManFrames( pMan, 1, 0, 0, 1, 0, NULL );
     assert( Aig_ManPoNum(pFramesTest) == Aig_ManRegNum(pMan) );
     pCnfTest = Cnf_DeriveSimple( pFramesTest, Aig_ManRegNum(pMan) );
-    p->pSatTest = Cnf_DataWriteIntoSolver( pCnfTest, 1, 0 );
+    p->pSatTest = (sat_solver *)Cnf_DataWriteIntoSolver( pCnfTest, 1, 0 );
     p->nSatVarsTestBeg = p->nSatVarsTestCur = sat_solver_nvars( p->pSatTest );
 
     // derive one timeframe to be checked for BMC
@@ -256,7 +259,7 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan )
 //Aig_ManShow( pFramesBmc, 0, NULL );
     assert( Aig_ManPoNum(pFramesBmc) == Aig_ManRegNum(pMan) );
     pCnfBmc = Cnf_DeriveSimple( pFramesBmc, Aig_ManRegNum(pMan) );
-    p->pSatBmc = Cnf_DataWriteIntoSolver( pCnfBmc, 1, 0 );
+    p->pSatBmc = (sat_solver *)Cnf_DataWriteIntoSolver( pCnfBmc, 1, 0 );
 
     // create variable sets
     p->vSatVarsMainCs = Fra_ClauSaveInputVars( pFramesMain, pCnfMain, 2 * (Aig_ManPiNum(pMan)-Aig_ManRegNum(pMan)) );
@@ -756,3 +759,5 @@ int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose, int fVeryVerbose )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c
index e5fe3f40..90659333 100644
--- a/src/aig/fra/fraClaus.c
+++ b/src/aig/fra/fraClaus.c
@@ -22,6 +22,9 @@
 #include "cnf.h"
 #include "satSolver.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -818,7 +821,7 @@ clk = clock();
         int * pStart;
         // reset the solver
         if ( p->pSatMain )  sat_solver_delete( p->pSatMain );
-        p->pSatMain = Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
+        p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
         if ( p->pSatMain == NULL )
         {
             printf( "Error: Main solver is unsat.\n" );
@@ -1030,8 +1033,8 @@ void Fra_ClausSimInfoRecord( Clu_Man_t * p, int * pModel )
     {
         if ( pModel[i] == l_True )
         {
-            assert( Aig_InfoHasBit( Vec_PtrEntry(p->vCexes, i), p->nCexes ) == 0 );
-            Aig_InfoSetBit( Vec_PtrEntry(p->vCexes, i), p->nCexes );
+            assert( Aig_InfoHasBit( (unsigned *)Vec_PtrEntry(p->vCexes, i), p->nCexes ) == 0 );
+            Aig_InfoSetBit( (unsigned *)Vec_PtrEntry(p->vCexes, i), p->nCexes );
         }
     }
     p->nCexes++;
@@ -1056,7 +1059,7 @@ int Fra_ClausSimInfoCheck( Clu_Man_t * p, int * pLits, int nLits )
     {
         iVar = lit_var(pLits[i]) - p->nFrames * p->pCnf->nVars;
         assert( iVar > 0 && iVar < p->pCnf->nVars );
-        pSims[i] = Vec_PtrEntry( p->vCexes, iVar );
+        pSims[i] = (unsigned *)Vec_PtrEntry( p->vCexes, iVar );
     }
     nWords = p->nCexes / 32;
     for ( w = 0; w < nWords; w++ )
@@ -1098,7 +1101,7 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
 
     // reset the solver
     if ( p->pSatMain )  sat_solver_delete( p->pSatMain );
-    p->pSatMain = Cnf_DataWriteIntoSolver( p->pCnf, p->nFrames+1, 0 );
+    p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, p->nFrames+1, 0 );
     if ( p->pSatMain == NULL )
     {
         printf( "Error: Main solver is unsat.\n" );
@@ -1516,7 +1519,7 @@ Aig_Obj_t * Fra_ClausGetLiteral( Clu_Man_t * p, int * pVar2Id, int Lit )
     Aig_Obj_t * pLiteral;
     int NodeId = pVar2Id[ lit_var(Lit) ];
     assert( NodeId >= 0 );
-    pLiteral = Aig_ManObj( p->pAig, NodeId )->pData;
+    pLiteral = (Aig_Obj_t *)Aig_ManObj( p->pAig, NodeId )->pData;
     return Aig_NotCond( pLiteral, lit_sign(Lit) );
 }
 
@@ -1705,7 +1708,7 @@ if ( fVerbose )
 
     // check BMC
 clk = clock();
-    p->pSatBmc = Cnf_DataWriteIntoSolver( p->pCnf, p->nPref + p->nFrames, 1 );
+    p->pSatBmc = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, p->nPref + p->nFrames, 1 );
     if ( p->pSatBmc == NULL )
     {
         printf( "Error: BMC solver is unsat.\n" );
@@ -1725,7 +1728,7 @@ if ( fVerbose )
 
     // start the SAT solver
 clk = clock();
-    p->pSatMain = Cnf_DataWriteIntoSolver( p->pCnf, p->nFrames+1, 0 );
+    p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, p->nFrames+1, 0 );
     if ( p->pSatMain == NULL )
     {
         printf( "Error: Main solver is unsat.\n" );
@@ -1867,3 +1870,5 @@ clk = clock();
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/fra/fraCnf.c b/src/aig/fra/fraCnf.c
index 27da3fc5..5021e750 100644
--- a/src/aig/fra/fraCnf.c
+++ b/src/aig/fra/fraCnf.c
@@ -20,6 +20,9 @@
 
 #include "fra.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -134,7 +137,7 @@ void Fra_AddClausesSuper( Fra_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
     pLits = ABC_ALLOC( int, nLits );
     // suppose AND-gate is A & B = C
     // add !A => !C   or   A + !C
-    Vec_PtrForEachEntry( vSuper, pFanin, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
     {
         pLits[0] = toLitCond(Fra_ObjSatNum(Aig_Regular(pFanin)), Aig_IsComplement(pFanin));
         pLits[1] = toLitCond(Fra_ObjSatNum(pNode), 1);
@@ -142,7 +145,7 @@ void Fra_AddClausesSuper( Fra_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
         assert( RetValue );
     }
     // add A & B => C   or   !A + !B + C
-    Vec_PtrForEachEntry( vSuper, pFanin, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
         pLits[i] = toLitCond(Fra_ObjSatNum(Aig_Regular(pFanin)), !Aig_IsComplement(pFanin));
     pLits[nLits-1] = toLitCond(Fra_ObjSatNum(pNode), 0);
     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
@@ -246,7 +249,7 @@ void Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
     if ( pOld ) Fra_ObjAddToFrontier( p, pOld, vFrontier );
     if ( pNew ) Fra_ObjAddToFrontier( p, pNew, vFrontier );
     // explore nodes in the frontier
-    Vec_PtrForEachEntry( vFrontier, pNode, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vFrontier, pNode, i )
     {
         // create the supergate
         assert( Fra_ObjSatNum(pNode) );
@@ -258,14 +261,14 @@ void Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
             Vec_PtrPushUnique( vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) );
             Vec_PtrPushUnique( vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) );
             Vec_PtrPushUnique( vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) );
-            Vec_PtrForEachEntry( vFanins, pFanin, k )
+            Vec_PtrForEachEntry( Aig_Obj_t *, vFanins, pFanin, k )
                 Fra_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
             Fra_AddClausesMux( p, pNode );
         }
         else
         {
             vFanins = Fra_CollectSuper( pNode, fUseMuxes );
-            Vec_PtrForEachEntry( vFanins, pFanin, k )
+            Vec_PtrForEachEntry( Aig_Obj_t *, vFanins, pFanin, k )
                 Fra_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
             Fra_AddClausesSuper( p, pNode, vFanins );
         }
@@ -282,3 +285,5 @@ void Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index fad8c7bf..93c16e1e 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -20,6 +20,9 @@
 
 #include "fra.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -198,12 +201,12 @@ void Fra_FraigVerifyCounterEx( Fra_Man_t * p, Vec_Int_t * vCex )
     Aig_ManForEachPo( p->pManAig, pObj, i )
         pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
     // check if the classes hold
-    Vec_PtrForEachEntry( p->pCla->vClasses1, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->pCla->vClasses1, pObj, i )
     {
         if ( pObj->fPhase != pObj->fMarkB )
             printf( "The node %d is not constant under cex!\n", pObj->Id );
     }
-    Vec_PtrForEachEntry( p->pCla->vClasses, ppClass, i )
+    Vec_PtrForEachEntry( Aig_Obj_t **, p->pCla->vClasses, ppClass, i )
     {
         for ( c = 1; ppClass[c]; c++ )
             if ( (ppClass[0]->fPhase ^ ppClass[c]->fPhase) != (ppClass[0]->fMarkB ^ ppClass[c]->fMarkB) )
@@ -483,3 +486,5 @@ Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/fra/fraHot.c b/src/aig/fra/fraHot.c
index c4472121..29c9c33d 100644
--- a/src/aig/fra/fraHot.c
+++ b/src/aig/fra/fraHot.c
@@ -20,6 +20,9 @@
 
 #include "fra.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -143,8 +146,8 @@ Vec_Int_t * Fra_OneHotCompute( Fra_Man_t * p, Fra_Sml_t * pSim )
             continue;
         assert( i-nTruePis >= 0 );
 //        Aig_ManForEachLoSeq( pSim->pAig, pObj2, k )
-//        Vec_PtrForEachEntryStart( pSim->pAig->vPis, pObj2, k, Aig_ManPiNum(p)-Aig_ManRegNum(p) )
-        Vec_PtrForEachEntryStart( pSim->pAig->vPis, pObj2, k, i+1 )
+//        Vec_PtrForEachEntryStart( Aig_Obj_t *, pSim->pAig->vPis, pObj2, k, Aig_ManPiNum(p)-Aig_ManRegNum(p) )
+        Vec_PtrForEachEntryStart( Aig_Obj_t *, pSim->pAig->vPis, pObj2, k, i+1 )
         {
             if ( fSkipConstEqu && Fra_OneHotNodeIsConst(pSim, pObj2) )
                 continue;
@@ -201,7 +204,7 @@ void Fra_OneHotAssume( Fra_Man_t * p, Vec_Int_t * vOneHots )
         pObj2 = Aig_ManPi( p->pManFraig, nPiNum + Fra_LitReg(Out2) );
         pLits[0] = toLitCond( Fra_ObjSatNum(pObj1), Fra_LitSign(Out1) );
         pLits[1] = toLitCond( Fra_ObjSatNum(pObj2), Fra_LitSign(Out2) );
-        // add contraint to solver
+        // add constraint to solver
         if ( !sat_solver_addclause( p->pSat, pLits, pLits + 2 ) )
         {
             printf( "Fra_OneHotAssume(): Adding clause makes SAT solver unsat.\n" );
@@ -337,11 +340,11 @@ void Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots )
     Aig_ManRandom(1);
     for ( i = 0; i < nRegs; i++ )
     {
-        pSim1 = Vec_PtrEntry( vSimInfo, i );
+        pSim1 = (unsigned *)Vec_PtrEntry( vSimInfo, i );
         for ( w = 0; w < nSimWords; w++ )
             pSim1[w] = Fra_ObjRandomSim();
     }
-    pSimTot = Vec_PtrEntry( vSimInfo, nRegs );
+    pSimTot = (unsigned *)Vec_PtrEntry( vSimInfo, nRegs );
 
     // collect simulation info
     memset( pSimTot, 0, sizeof(unsigned) * nSimWords );
@@ -355,8 +358,8 @@ void Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots )
 //Fra_LitSign(Out1)? '-': '+', Fra_LitReg(Out1), 
 //Fra_LitSign(Out2)? '-': '+', Fra_LitReg(Out2) ); 
         Counter++;
-        pSim1 = Vec_PtrEntry( vSimInfo, Fra_LitReg(Out1) );
-        pSim2 = Vec_PtrEntry( vSimInfo, Fra_LitReg(Out2) );
+        pSim1 = (unsigned *)Vec_PtrEntry( vSimInfo, Fra_LitReg(Out1) );
+        pSim2 = (unsigned *)Vec_PtrEntry( vSimInfo, Fra_LitReg(Out2) );
         if ( Fra_LitSign(Out1) && Fra_LitSign(Out2) )
             for ( w = 0; w < nSimWords; w++ )
                 pSimTot[w] |=  pSim1[w] &  pSim2[w];
@@ -442,7 +445,7 @@ void Fra_OneHotAddKnownConstraint( Fra_Man_t * p, Vec_Ptr_t * vOnehots )
     // these constrants should be added to different timeframes!
     // (also note that PIs follow first - then registers)
     //
-    Vec_PtrForEachEntry( vOnehots, vGroup, k )
+    Vec_PtrForEachEntry( Vec_Int_t *, vOnehots, vGroup, k )
     {
         Vec_IntForEachEntry( vGroup, Out1, i )
         Vec_IntForEachEntryStart( vGroup, Out2, j, i+1 )
@@ -451,7 +454,7 @@ void Fra_OneHotAddKnownConstraint( Fra_Man_t * p, Vec_Ptr_t * vOnehots )
             pObj2 = Aig_ManPi( p->pManFraig, Out2 );
             pLits[0] = toLitCond( Fra_ObjSatNum(pObj1), 1 );
             pLits[1] = toLitCond( Fra_ObjSatNum(pObj2), 1 );
-            // add contraint to solver
+            // add constraint to solver
             if ( !sat_solver_addclause( p->pSat, pLits, pLits + 2 ) )
             {
                 printf( "Fra_OneHotAddKnownConstraint(): Adding clause makes SAT solver unsat.\n" );
@@ -469,3 +472,5 @@ void Fra_OneHotAddKnownConstraint( Fra_Man_t * p, Vec_Ptr_t * vOnehots )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c
index 716e83d5..34fa87e5 100644
--- a/src/aig/fra/fraImp.c
+++ b/src/aig/fra/fraImp.c
@@ -20,6 +20,9 @@
 
 #include "fra.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -211,12 +214,12 @@ Vec_Ptr_t * Fra_SmlSortUsingOnes( Fra_Sml_t * p, int fLatchCorr )
         // skip nodes participating in the classes
 //        if ( Fra_ClassObjRepr(pObj) )
 //            continue;
-        pMemory = Vec_PtrEntry( vNodes, pnBits[i] );
+        pMemory = (int *)Vec_PtrEntry( vNodes, pnBits[i] );
         pMemory[ pnNodes[pnBits[i]]++ ] = i;
     }
     // add 0s in the end
     nTotal = 0;
-    Vec_PtrForEachEntry( vNodes, pMemory, i )
+    Vec_PtrForEachEntry( int *, vNodes, pMemory, i )
     {
         pMemory[ pnNodes[i]++ ] = 0;
         nTotal += pnNodes[i];
@@ -335,8 +338,8 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in
     // count the total number of implications
     for ( k = nSimWords * 32; k > 0; k-- )
     for ( i = k - 1; i > 0; i-- )
-    for ( pNodesI = Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
-    for ( pNodesK = Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
+    for ( pNodesI = (int *)Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
+    for ( pNodesK = (int *)Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
         nImpsTotal++;
 
     // compute implications and their costs
@@ -347,8 +350,8 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in
         {
             // HERE WE ARE MISSING SOME POTENTIAL IMPLICATIONS (with complement!)
 
-            for ( pNodesI = Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
-            for ( pNodesK = Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
+            for ( pNodesI = (int *)Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
+            for ( pNodesK = (int *)Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
             {
                 nImpsTried++;
                 if ( !Sml_NodeCheckImp(pSeq, *pNodesI, *pNodesK) )
@@ -444,7 +447,7 @@ void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums )
                 Vec_IntWriteEntry( vImps, i, 0 );
                 break;
             }
-        }
+        } 
         if ( f < p->pPars->nFramesK )
             continue;
         // add constraints in each timeframe
@@ -465,7 +468,7 @@ void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums )
             // L => R      L' v R     (complement = L & R')
             pLits[0] = 2 * Left  + !fComplL;
             pLits[1] = 2 * Right +  fComplR;
-            // add contraint to solver
+            // add constraint to solver
             if ( !sat_solver_addclause( pSat, pLits, pLits + 2 ) )
             {
                 sat_solver_delete( pSat );
@@ -712,8 +715,8 @@ void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew )
         pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
         // record the implication: L' + R
         pMiter = Aig_Or( pNew, 
-            Aig_NotCond(pLeft->pData, !pLeft->fPhase), 
-            Aig_NotCond(pRight->pData, pRight->fPhase) ); 
+            Aig_NotCond((Aig_Obj_t *)pLeft->pData, !pLeft->fPhase), 
+            Aig_NotCond((Aig_Obj_t *)pRight->pData, pRight->fPhase) ); 
         Aig_ObjCreatePo( pNew, pMiter );
     }
     pNew->nAsserts = Aig_ManPoNum(pNew) - nPosOld;
@@ -724,3 +727,5 @@ void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 84b739a4..2f2d8f2d 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -21,6 +21,10 @@
 #include "fra.h"
 #include "cnf.h"
 #include "dar.h"
+#include "saig.h"
+
+ABC_NAMESPACE_IMPL_START
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -265,7 +269,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
     {
         // divide large clock domains into separate partitions
         vResult = Vec_PtrAlloc( 100 );
-        Vec_PtrForEachEntry( (Vec_Ptr_t *)pAig->vClockDoms, vPart, i )
+        Vec_PtrForEachEntry( Vec_Int_t *, (Vec_Ptr_t *)pAig->vClockDoms, vPart, i )
         {
             if ( nPartSize && Vec_IntSize(vPart) > nPartSize )
                 Aig_ManPartDivide( vResult, vPart, nPartSize, pPars->nOverSize );
@@ -281,7 +285,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
     {
         // print partitions
         printf( "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) );
-        Vec_PtrForEachEntry( vResult, vPart, i )
+        Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i )
         {
             sprintf( Buffer, "part%03d.aig", i );
             pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, NULL );
@@ -294,7 +298,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
 
     // perform SSW with partitions
     Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
-    Vec_PtrForEachEntry( vResult, vPart, i )
+    Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i )
     {
         pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack );
         // create the projection of 1-hot registers
@@ -498,7 +502,7 @@ p->timeTrav += clock() - clk2;
 //        Cnf_DataTranformPolarity( pCnf, 0 );
 //Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
 
-        p->pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+        p->pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
         p->nSatVars = pCnf->nVars;
         assert( p->pSat != NULL );
         if ( p->pSat == NULL )
@@ -523,7 +527,7 @@ p->timeTrav += clock() - clk2;
             if ( pCnf->pVarNums[pObj->Id] == -1 )
                 continue;
             Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
-            Fra_ObjSetFaninVec( pObj, (void *)1 );
+            Fra_ObjSetFaninVec( pObj, (Vec_Ptr_t *)1 );
         }
         Cnf_DataFree( pCnf );
 
@@ -653,7 +657,6 @@ finish:
 ***********************************************************************/
 int Fra_FraigInductionTest( char * pFileName, Fra_Ssw_t * pParams )
 {
-    extern Aig_Man_t * Saig_ManReadBlif( char * pFileName );
     FILE * pFile;
     char * pFilePairs;
     Aig_Man_t * pMan, * pNew;
@@ -678,7 +681,7 @@ int Fra_FraigInductionTest( char * pFileName, Fra_Ssw_t * pParams )
         Aig_ManPrintStats( pNew );
     }
     Aig_ManStop( pNew );
-    pNum2Id = pMan->pData;
+    pNum2Id = (int *)pMan->pData;
     // write the output file
     pFilePairs = Aig_FileNameGenericAppend( pFileName, ".pairs" );
     pFile = fopen( pFilePairs, "w" );
@@ -702,3 +705,5 @@ int Fra_FraigInductionTest( char * pFileName, Fra_Ssw_t * pParams )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/fra/fraIndVer.c b/src/aig/fra/fraIndVer.c
index 71faa346..32069cfb 100644
--- a/src/aig/fra/fraIndVer.c
+++ b/src/aig/fra/fraIndVer.c
@@ -21,6 +21,9 @@
 #include "fra.h"
 #include "cnf.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -72,7 +75,7 @@ int Fra_InvariantVerify( Aig_Man_t * pAig, int nFrames, Vec_Int_t * vClauses, Ve
     }
 */
     // derive initialized frames for the base case
-    pSat = Cnf_DataWriteIntoSolver( pCnf, nFrames, 1 );
+    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, nFrames, 1 );
     // check clauses in the base case
     Beg = 0;
     pStart = Vec_IntArray( vLits );
@@ -93,7 +96,7 @@ int Fra_InvariantVerify( Aig_Man_t * pAig, int nFrames, Vec_Int_t * vClauses, Ve
     sat_solver_delete( pSat );
 
     // derive initialized frames for the base case
-    pSat = Cnf_DataWriteIntoSolver( pCnf, nFrames + 1, 0 );
+    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, nFrames + 1, 0 );
     assert( pSat->size == 2 * pCnf->nVars );
     // add clauses to the first frame
     Beg = 0;
@@ -159,3 +162,5 @@ int Fra_InvariantVerify( Aig_Man_t * pAig, int nFrames, Vec_Int_t * vClauses, Ve
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c
index 16912f46..b18a8fcd 100644
--- a/src/aig/fra/fraLcr.c
+++ b/src/aig/fra/fraLcr.c
@@ -20,6 +20,9 @@
 
 #include "fra.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -197,7 +200,7 @@ void Fra_LcrAigPrepareTwo( Aig_Man_t * pAig, Fra_Man_t * p )
 ***********************************************************************/
 int Fra_LcrNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
 {
-    Fra_Man_t * pTemp = pObj0->pData;
+    Fra_Man_t * pTemp = (Fra_Man_t *)pObj0->pData;
     Fra_Lcr_t * pLcr = (Fra_Lcr_t *)pTemp->pBmc;
     Aig_Man_t * pFraig;
     Aig_Obj_t * pOut0, * pOut1;
@@ -215,7 +218,7 @@ int Fra_LcrNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
         return 1;
     }
     assert( nPart0 == nPart1 );
-    pFraig = Vec_PtrEntry( pLcr->vFraigs, nPart0 );
+    pFraig = (Aig_Man_t *)Vec_PtrEntry( pLcr->vFraigs, nPart0 );
     // get the fraig outputs
     pOut0 = Aig_ManPo( pFraig, pLcr->pInToOutNum[(long)pObj0->pNext] );
     pOut1 = Aig_ManPo( pFraig, pLcr->pInToOutNum[(long)pObj1->pNext] );
@@ -235,7 +238,7 @@ int Fra_LcrNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
 ***********************************************************************/
 int Fra_LcrNodeIsConst( Aig_Obj_t * pObj )
 {
-    Fra_Man_t * pTemp = pObj->pData;
+    Fra_Man_t * pTemp = (Fra_Man_t *)pObj->pData;
     Fra_Lcr_t * pLcr = (Fra_Lcr_t *)pTemp->pBmc;
     Aig_Man_t * pFraig;
     Aig_Obj_t * pOut;
@@ -243,7 +246,7 @@ int Fra_LcrNodeIsConst( Aig_Obj_t * pObj )
     assert( Aig_ObjIsPi(pObj) );
     // find the partition to which these nodes belong
     nPart = pLcr->pInToOutPart[(long)pObj->pNext];
-    pFraig = Vec_PtrEntry( pLcr->vFraigs, nPart );
+    pFraig = (Aig_Man_t *)Vec_PtrEntry( pLcr->vFraigs, nPart );
     // get the fraig outputs
     pOut = Aig_ManPo( pFraig, pLcr->pInToOutNum[(long)pObj->pNext] );
     return Aig_ObjFanin0(pOut) == Aig_ManConst1(pFraig);
@@ -264,14 +267,14 @@ Aig_Obj_t * Fra_LcrManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj
 {
     Aig_Obj_t * pObjNew;
     if ( pObj->pData )
-        return pObj->pData;
+        return (Aig_Obj_t *)pObj->pData;
     Fra_LcrManDup_rec( pNew, p, Aig_ObjFanin0(pObj) );
     if ( Aig_ObjIsBuf(pObj) )
-        return pObj->pData = Aig_ObjChild0Copy(pObj);
+        return (Aig_Obj_t *)(pObj->pData = Aig_ObjChild0Copy(pObj));
     Fra_LcrManDup_rec( pNew, p, Aig_ObjFanin1(pObj) );
     pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
     Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
-    return pObj->pData = pObjNew;
+    return (Aig_Obj_t *)(pObj->pData = pObjNew);
 }
 
 /**Function*************************************************************
@@ -308,7 +311,7 @@ Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr )
     Aig_ManCleanData( pLcr->pAig );
     pNew = Aig_ManStartFrom( pLcr->pAig );
     // go over the equivalence classes
-    Vec_PtrForEachEntry( pLcr->pCla->vClasses, ppClass, i )
+    Vec_PtrForEachEntry( Aig_Obj_t **, pLcr->pCla->vClasses, ppClass, i )
     {
         pMiter = Aig_ManConst0(pNew);
         for ( c = 0; ppClass[c]; c++ )
@@ -321,7 +324,7 @@ Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr )
         Aig_ObjCreatePo( pNew, pMiter );
     }
     // go over the constant candidates
-    Vec_PtrForEachEntry( pLcr->pCla->vClasses1, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, pLcr->pCla->vClasses1, pObj, i )
     {
         assert( Aig_ObjIsPi(pObj) );
         pObjPo = Aig_ManPo( pLcr->pAig, Offset+(long)pObj->pNext );
@@ -349,14 +352,14 @@ void Fra_LcrRemapPartitions( Vec_Ptr_t * vParts, Fra_Cla_t * pCla, int * pInToOu
     int Out, Offset, i, k, c;
     // compute the LO/LI offset
     Offset = Aig_ManPoNum(pCla->pAig) - Aig_ManPiNum(pCla->pAig);
-    Vec_PtrForEachEntry( vParts, vOne, i )
+    Vec_PtrForEachEntry( Vec_Int_t *, vParts, vOne, i )
     {
         vOneNew = Vec_IntAlloc( Vec_IntSize(vOne) );
         Vec_IntForEachEntry( vOne, Out, k )
         {
             if ( Out < Vec_PtrSize(pCla->vClasses) )
             {
-                ppClass = Vec_PtrEntry( pCla->vClasses, Out );
+                ppClass = (Aig_Obj_t **)Vec_PtrEntry( pCla->vClasses, Out );
                 for ( c = 0; ppClass[c]; c++ )
                 {
                     pInToOutPart[(long)ppClass[c]->pNext] = i;
@@ -366,7 +369,7 @@ void Fra_LcrRemapPartitions( Vec_Ptr_t * vParts, Fra_Cla_t * pCla, int * pInToOu
             }
             else
             {
-                pObjPi = Vec_PtrEntry( pCla->vClasses1, Out - Vec_PtrSize(pCla->vClasses) );
+                pObjPi = (Aig_Obj_t *)Vec_PtrEntry( pCla->vClasses1, Out - Vec_PtrSize(pCla->vClasses) );
                 pInToOutPart[(long)pObjPi->pNext] = i;
                 pInToOutNum[(long)pObjPi->pNext] = Vec_IntSize(vOneNew);
                 Vec_IntPush( vOneNew, Offset+(long)pObjPi->pNext );
@@ -393,7 +396,7 @@ Aig_Obj_t * Fra_LcrCreatePart_rec( Fra_Cla_t * pCla, Aig_Man_t * pNew, Aig_Man_t
 {
     assert( !Aig_IsComplement(pObj) );
     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
-        return pObj->pData;
+        return (Aig_Obj_t *)pObj->pData;
     Aig_ObjSetTravIdCurrent(p, pObj);
     if ( Aig_ObjIsPi(pObj) )
     {
@@ -404,13 +407,13 @@ Aig_Obj_t * Fra_LcrCreatePart_rec( Fra_Cla_t * pCla, Aig_Man_t * pNew, Aig_Man_t
         else
         {
             pObj->pData = Fra_LcrCreatePart_rec( pCla, pNew, p, pRepr );
-            pObj->pData = Aig_NotCond( pObj->pData, pRepr->fPhase ^ pObj->fPhase );
+            pObj->pData = Aig_NotCond( (Aig_Obj_t *)pObj->pData, pRepr->fPhase ^ pObj->fPhase );
         }
-        return pObj->pData;
+        return (Aig_Obj_t *)pObj->pData;
     }
     Fra_LcrCreatePart_rec( pCla, pNew, p, Aig_ObjFanin0(pObj) );
     Fra_LcrCreatePart_rec( pCla, pNew, p, Aig_ObjFanin1(pObj) );
-    return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    return (Aig_Obj_t *)(pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ));
 }
 
 /**Function*************************************************************
@@ -467,12 +470,12 @@ void Fra_ClassNodesMark( Fra_Lcr_t * p )
     // compute the LO/LI offset
     Offset = Aig_ManPoNum(p->pCla->pAig) - Aig_ManPiNum(p->pCla->pAig);
     // mark the nodes remaining in the classes
-    Vec_PtrForEachEntry( p->pCla->vClasses1, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->pCla->vClasses1, pObj, i )
     {
         pObj = Aig_ManPo( p->pCla->pAig, Offset+(long)pObj->pNext );
         pObj->fMarkA = 1;
     }
-    Vec_PtrForEachEntry( p->pCla->vClasses, ppClass, i )
+    Vec_PtrForEachEntry( Aig_Obj_t **, p->pCla->vClasses, ppClass, i )
     {
         for ( c = 0; ppClass[c]; c++ )
         {
@@ -500,12 +503,12 @@ void Fra_ClassNodesUnmark( Fra_Lcr_t * p )
     // compute the LO/LI offset
     Offset = Aig_ManPoNum(p->pCla->pAig) - Aig_ManPiNum(p->pCla->pAig);
     // mark the nodes remaining in the classes
-    Vec_PtrForEachEntry( p->pCla->vClasses1, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->pCla->vClasses1, pObj, i )
     {
         pObj = Aig_ManPo( p->pCla->pAig, Offset+(long)pObj->pNext );
         pObj->fMarkA = 0;
     }
-    Vec_PtrForEachEntry( p->pCla->vClasses, ppClass, i )
+    Vec_PtrForEachEntry( Aig_Obj_t **, p->pCla->vClasses, ppClass, i )
     {
         for ( c = 0; ppClass[c]; c++ )
         {
@@ -610,12 +613,12 @@ p->timePart += clock() - clk2;
         // derive AIGs for each partition
         Fra_ClassNodesMark( p );
         Vec_PtrClear( p->vFraigs );
-        Vec_PtrForEachEntry( p->vParts, vPart, i )
+        Vec_PtrForEachEntry( Vec_Int_t *, p->vParts, vPart, i )
         {
             int clk3 = clock();
             if ( TimeLimit != 0.0 && clock() > TimeToStop )
             {
-                Vec_PtrForEachEntry( p->vFraigs, pAigPart, i )
+                Vec_PtrForEachEntry( Aig_Man_t *, p->vFraigs, pAigPart, i )
                     Aig_ManStop( pAigPart );
                 Aig_ManCleanMarkA( pAig );
                 Aig_ManCleanMarkB( pAig );
@@ -657,7 +660,7 @@ ABC_PRT( "Time", clock() - clk3 );
         if ( Fra_ClassesRefine1( p->pCla, 0, NULL ) )
             p->fRefining = 1;
         // clean the fraigs
-        Vec_PtrForEachEntry( p->vFraigs, pAigPart, i )
+        Vec_PtrForEachEntry( Aig_Man_t *, p->vFraigs, pAigPart, i )
             Aig_ManStop( pAigPart );
 
         // repartition if needed
@@ -702,3 +705,5 @@ finish:
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index 8bdd147d..7e427e72 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -20,6 +20,9 @@
 
 #include "fra.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -307,3 +310,5 @@ void Fra_ManPrint( Fra_Man_t * p )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/fra/fraPart.c b/src/aig/fra/fraPart.c
index 6dfbd2e9..9556bb51 100644
--- a/src/aig/fra/fraPart.c
+++ b/src/aig/fra/fraPart.c
@@ -20,6 +20,9 @@
 
 #include "fra.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -63,7 +66,7 @@ ABC_PRT( "Supports", clock() - clk );
     // remove last entry
     Aig_ManForEachPo( p, pObj, i )
     {
-        vSup = Vec_VecEntry( vSupps, i );
+        vSup = (Vec_Int_t *)Vec_VecEntry( vSupps, i );
         Vec_IntPop( vSup );
         // remember support
 //        pObj->pNext = (Aig_Obj_t *)vSup;
@@ -74,7 +77,7 @@ clk = clock();
     vSuppsIn = Vec_VecStart( Aig_ManPiNum(p) );
     Aig_ManForEachPo( p, pObj, i )
     {
-        vSup = Vec_VecEntry( vSupps, i );
+        vSup = (Vec_Int_t *)Vec_VecEntry( vSupps, i );
         Vec_IntForEachEntry( vSup, Entry, k )
             Vec_VecPush( vSuppsIn, Entry, (void *)(ABC_PTRUINT_T)i );
     }
@@ -91,7 +94,7 @@ clk = clock();
     {
 //        Bar_ProgressUpdate( pProgress, i, NULL );
         // get old supports
-        vSup = Vec_VecEntry( vSupps, i );
+        vSup = (Vec_Int_t *)Vec_VecEntry( vSupps, i );
         if ( Vec_IntSize(vSup) < 2 )
             continue;
         // compute new supports
@@ -106,7 +109,7 @@ clk = clock();
 //            pObj = Aig_ManObj( p, Entry );
             // get support of this output
 //            vSup2 = (Vec_Int_t *)pObj->pNext;
-            vSup2 = Vec_VecEntry( vSupps, k );
+            vSup2 = (Vec_Int_t *)Vec_VecEntry( vSupps, k );
             // count the number of common vars
             nCommon = Vec_IntTwoCountCommon(vSup, vSup2);
             if ( nCommon < 2 )
@@ -197,7 +200,7 @@ ABC_PRT( "Supports", clock() - clk );
     // remove last entry
     Aig_ManForEachPo( p, pObj, i )
     {
-        vSup = Vec_VecEntry( vSupps, i );
+        vSup = (Vec_Int_t *)Vec_VecEntry( vSupps, i );
         Vec_IntPop( vSup );
         // remember support
 //        pObj->pNext = (Aig_Obj_t *)vSup;
@@ -210,7 +213,7 @@ clk = clock();
     {
         if ( i == p->nAsserts )
             break;
-        vSup = Vec_VecEntry( vSupps, i );
+        vSup = (Vec_Int_t *)Vec_VecEntry( vSupps, i );
         Vec_IntForEachEntry( vSup, Entry, k )
             Vec_VecPush( vSuppsIn, Entry, (void *)(ABC_PTRUINT_T)i );
     }
@@ -223,17 +226,17 @@ clk = clock();
     {
         if ( i % 50 != 0 )
             continue;
-        vSup = Vec_VecEntry( vSupps, i );
+        vSup = (Vec_Int_t *)Vec_VecEntry( vSupps, i );
         memset( pSupp, 0, sizeof(char) * Aig_ManPiNum(p) );
         // go through each input of this output
         Vec_IntForEachEntry( vSup, Entry, k )
         {
             pSupp[Entry] = 1;
-            vSup2 = Vec_VecEntry( vSuppsIn, Entry );
+            vSup2 = (Vec_Int_t *)Vec_VecEntry( vSuppsIn, Entry );
             // go though each assert of this input
             Vec_IntForEachEntry( vSup2, Entry2, m )
             {
-                vSup3 = Vec_VecEntry( vSupps, Entry2 );
+                vSup3 = (Vec_Int_t *)Vec_VecEntry( vSupps, Entry2 );
                 // go through each input of this assert
                 Vec_IntForEachEntry( vSup3, Entry3, n )
                 {
@@ -261,3 +264,5 @@ ABC_PRT( "Extension ", clock() - clk );
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c
index 039a660f..50503670 100644
--- a/src/aig/fra/fraSat.c
+++ b/src/aig/fra/fraSat.c
@@ -21,6 +21,9 @@
 #include <math.h>
 #include "fra.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -512,7 +515,7 @@ int Fra_SetActivityFactors_rec( Fra_Man_t * p, Aig_Obj_t * pObj, int LevelMin, i
     veci_push(&p->pSat->act_vars, Fra_ObjSatNum(pObj));
     // explore the fanins
     vFanins = Fra_ObjFaninVec( pObj );
-    Vec_PtrForEachEntry( vFanins, pFanin, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vFanins, pFanin, i )
         Counter += Fra_SetActivityFactors_rec( p, Aig_Regular(pFanin), LevelMin, LevelMax );
     return 1 + Counter;
 }
@@ -557,3 +560,5 @@ p->timeTrav += clock() - clk;
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index ccb3e7b1..1576a70a 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -23,6 +23,10 @@
 #include "int.h"
 #include "ssw.h"
 #include "saig.h"
+#include "bbr.h"
+
+ABC_NAMESPACE_IMPL_START
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -63,7 +67,7 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p )
     p->fInterpolation    =       1;  // enables interpolation
     p->fInterSeparate    =       0;  // enables interpolation for each outputs separately
     p->fReachability     =       1;  // enables BDD based reachability
-    p->fReorderImage     =       0;  // enables variable reordering during image computation
+    p->fReorderImage     =       1;  // enables variable reordering during image computation
     p->fStopOnFirstFail  =       1;  // enables stopping after first output of a miter has failed to prove
     p->fUseNewProver     =       0;  // enables new prover
     p->fSilent           =       0;  // disables all output
@@ -292,7 +296,7 @@ ABC_PRT( "Time", clock() - clk );
     // perform min-area retiming
     if ( pParSec->fRetimeRegs && pNew->nRegs )
     {
-    extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
+//    extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
 clk = clock();
     pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
     pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
@@ -353,9 +357,9 @@ clk = clock();
         Aig_ManSetRegNum( pNew, pNew->nRegs );
 //        pNew = Ssw_SignalCorrespondence( pTemp = pNew, pPars2 );
         if ( Aig_ManRegNum(pNew) > 0 )
-              pNew = Ssw_SignalCorrespondence( pTemp = pNew, pPars2 );
+            pNew = Ssw_SignalCorrespondence( pTemp = pNew, pPars2 );
         else
-              pNew = Aig_ManDupSimpleDfs( pTemp = pNew );
+            pNew = Aig_ManDupSimpleDfs( pTemp = pNew );
 
         if ( pNew == NULL )
         {
@@ -382,7 +386,7 @@ ABC_PRT( "Time", clock() - clk );
 //        if ( pParSec->fRetimeFirst && pNew->nRegs )
         if ( pNew->nRegs )
         {
-        extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
+//        extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
 clk = clock();
         pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
         pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
@@ -480,7 +484,7 @@ clk = clock();
         }
         else if ( pParSec->fInterSeparate )
         {
-            Ssw_Cex_t * pCex = NULL;
+            Abc_Cex_t * pCex = NULL;
             Aig_Man_t * pTemp, * pAux;
             Aig_Obj_t * pObjPo;
             int i, Counter = 0;
@@ -488,6 +492,8 @@ clk = clock();
             { 
                 if ( Aig_ObjFanin0(pObjPo) == Aig_ManConst1(pNew) )
                     continue;
+                if ( pPars->fVerbose )
+                    printf( "Solving output %2d (out of %2d):\n", i, Saig_ManPoNum(pNew) );
                 pTemp = Aig_ManDupOneOutput( pNew, i, 1 );
                 pTemp = Aig_ManScl( pAux = pTemp, 1, 1, 0 );
                 Aig_ManStop( pAux );
@@ -537,7 +543,7 @@ clk = clock();
             RetValue = Inter_ManPerformInterpolation( pNewOrpos, pPars, &Depth );
             if ( pNewOrpos->pSeqModel )
             {
-                Ssw_Cex_t * pCex;
+                Abc_Cex_t * pCex;
                 pCex = pNew->pSeqModel = pNewOrpos->pSeqModel; pNewOrpos->pSeqModel = NULL;
                 pCex->iPo = Ssw_SmlFindOutputCounterExample( pNew, pNew->pSeqModel );
             }
@@ -561,10 +567,19 @@ ABC_PRT( "Time", clock() - clk );
     // try reachability analysis
     if ( pParSec->fReachability && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManRegNum(pNew) < pParSec->nBddVarsMax )
     {
-        extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent );
+        Saig_ParBbr_t Pars, * pPars = &Pars;
+        Bbr_ManSetDefaultParams( pPars );
+        pPars->TimeLimit     = 0;
+        pPars->nBddMax       = pParSec->nBddMax;
+        pPars->nIterMax      = pParSec->nBddIterMax;
+        pPars->fPartition    = 1;
+        pPars->fReorder      = 1;
+        pPars->fReorderImage = 1;
+        pPars->fVerbose      = 0;
+        pPars->fSilent       = pParSec->fSilent;
         pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
         pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
-        RetValue = Aig_ManVerifyUsingBdds( pNew, pParSec->nBddMax, pParSec->nBddIterMax, 1, 1, pParSec->fReorderImage, 0, pParSec->fSilent );
+        RetValue = Aig_ManVerifyUsingBdds( pNew, pPars );
     }
 
 finish:
@@ -645,3 +660,5 @@ ABC_PRT( "Time", clock() - clkTotal );
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index 4f164e5c..25c30989 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -20,6 +20,9 @@
 
 #include "fra.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -41,7 +44,7 @@
 ***********************************************************************/
 int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize )
 {
-    Fra_Man_t * p = pObj->pData;
+    Fra_Man_t * p = (Fra_Man_t *)pObj->pData;
     static int s_FPrimes[128] = { 
         1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 
         1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, 
@@ -81,7 +84,7 @@ int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize )
 ***********************************************************************/
 int Fra_SmlNodeIsConst( Aig_Obj_t * pObj )
 {
-    Fra_Man_t * p = pObj->pData;
+    Fra_Man_t * p = (Fra_Man_t *)pObj->pData;
     unsigned * pSims;
     int i;
     pSims = Fra_ObjSim(p->pSml, pObj->Id);
@@ -104,7 +107,7 @@ int Fra_SmlNodeIsConst( Aig_Obj_t * pObj )
 ***********************************************************************/
 int Fra_SmlNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
 {
-    Fra_Man_t * p = pObj0->pData;
+    Fra_Man_t * p = (Fra_Man_t *)pObj0->pData;
     unsigned * pSims0, * pSims1;
     int i;
     pSims0 = Fra_ObjSim(p->pSml, pObj0->Id);
@@ -885,12 +888,12 @@ Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nW
   SeeAlso     []
 
 ***********************************************************************/
-Fra_Cex_t * Fra_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames )
+Abc_Cex_t * Fra_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames )
 {
-    Fra_Cex_t * pCex;
+    Abc_Cex_t * pCex;
     int nWords = Aig_BitWordNum( nRegs + nRealPis * nFrames );
-    pCex = (Fra_Cex_t *)ABC_ALLOC( char, sizeof(Fra_Cex_t) + sizeof(unsigned) * nWords );
-    memset( pCex, 0, sizeof(Fra_Cex_t) + sizeof(unsigned) * nWords );
+    pCex = (Abc_Cex_t *)ABC_ALLOC( char, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords );
+    memset( pCex, 0, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords );
     pCex->nRegs  = nRegs;
     pCex->nPis   = nRealPis;
     pCex->nBits  = nRegs + nRealPis * nFrames;
@@ -908,7 +911,7 @@ Fra_Cex_t * Fra_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_SmlFreeCounterExample( Fra_Cex_t * pCex )
+void Fra_SmlFreeCounterExample( Abc_Cex_t * pCex )
 {
     ABC_FREE( pCex );
 }
@@ -924,9 +927,9 @@ void Fra_SmlFreeCounterExample( Fra_Cex_t * pCex )
   SeeAlso     []
 
 ***********************************************************************/
-Fra_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p )
+Abc_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p )
 {
-    Fra_Cex_t * pCex;
+    Abc_Cex_t * pCex;
     Aig_Obj_t * pObj;
     unsigned * pSims;
     int iPo, iFrame, iBit, i, k;
@@ -998,9 +1001,9 @@ Fra_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Fra_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel )
+Abc_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel )
 {
-    Fra_Cex_t * pCex;
+    Abc_Cex_t * pCex;
     Aig_Obj_t * pObj;
     int i, nFrames, nTruePis, nTruePos, iPo, iFrame;
     // get the number of frames
@@ -1058,9 +1061,9 @@ Fra_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, in
   SeeAlso     []
 
 ***********************************************************************/
-Fra_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut )
+Abc_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut )
 {
-    Fra_Cex_t * pCex;
+    Abc_Cex_t * pCex;
     int nTruePis, nTruePos, iPo, iFrame;
     assert( Aig_ManRegNum(pAig) > 0 );
     nTruePis = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig);
@@ -1085,7 +1088,7 @@ Fra_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut )
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_Cex_t * p )
+int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p )
 {
     Fra_Sml_t * pSml;
     Aig_Obj_t * pObj;
@@ -1113,6 +1116,38 @@ int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_Cex_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Make the trivial counter-example for the trivially asserted output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Cex_t * Fra_SmlSimpleCounterExample( Aig_Man_t * pAig, int * pModel, int iFrame, int iPo )
+{
+    Abc_Cex_t * pCex;
+    int iBit;
+    pCex = Fra_SmlAllocCounterExample( Aig_ManRegNum(pAig), Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig), iFrame + 1 );
+    pCex->iPo    = iPo;
+    pCex->iFrame = iFrame;
+    for ( iBit = Aig_ManRegNum(pAig); iBit < pCex->nBits; iBit++ )
+        if ( pModel[iBit-Aig_ManRegNum(pAig)] )
+            Aig_InfoSetBit( pCex->pData, iBit );
+/*
+    if ( !Fra_SmlRunCounterExample( pAig, pCex ) )
+    {
+        printf( "Fra_SmlSimpleCounterExample(): Counter-example is invalid.\n" );
+//        Fra_SmlFreeCounterExample( pCex );
+//        pCex = NULL;
+    }
+*/
+    return pCex;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Resimulates the counter-example.]
 
   Description []
@@ -1122,7 +1157,7 @@ int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_Cex_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Fra_Cex_t * p )
+int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Abc_Cex_t * p )
 {
     Fra_Sml_t * pSml;
     Aig_Obj_t * pObj;
@@ -1191,3 +1226,5 @@ int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Fra_Cex_t * p )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/fra/fra_.c b/src/aig/fra/fra_.c
index 2b601587..8e5785ec 100644
--- a/src/aig/fra/fra_.c
+++ b/src/aig/fra/fra_.c
@@ -20,6 +20,9 @@
 
 #include "fra.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -46,3 +49,5 @@
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+