Unified the use of counter-examples in three packages.

30 files changed, 233 insertions, 769 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index ddedb4e2..f667d4e3 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -33,6 +33,7 @@
 #include <time.h>
 
 #include "vec.h"
+#include "utilCex.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
diff --git a/src/aig/bbr/bbrCex.c b/src/aig/bbr/bbrCex.c
index 8f99ea3c..4a1a1d67 100644
--- a/src/aig/bbr/bbrCex.c
+++ b/src/aig/bbr/bbrCex.c
@@ -19,7 +19,6 @@
 ***********************************************************************/
 
 #include "bbr.h"
-#include "ssw.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -60,7 +59,7 @@ Abc_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd,
 //printf( "\nDeriving counter-example.\n" );
 
     // allocate room for the counter-example
-    pCex = Ssw_SmlAllocCounterExample( Saig_ManRegNum(p), Saig_ManPiNum(p), Vec_PtrSize(vOnionRings)+1 );
+    pCex = Abc_CexAlloc( Saig_ManRegNum(p), Saig_ManPiNum(p), Vec_PtrSize(vOnionRings)+1 );
     pCex->iFrame = Vec_PtrSize(vOnionRings);
     pCex->iPo = iOutput;
     nPiOffset = Saig_ManRegNum(p) + Saig_ManPiNum(p) * Vec_PtrSize(vOnionRings);
@@ -153,7 +152,7 @@ Abc_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd,
     // verify the counter example
     if ( Vec_PtrSize(vOnionRings) < 1000 )
     {
-    RetValue = Ssw_SmlRunCounterExample( p, pCex );
+    RetValue = Saig_ManVerifyCex( p, pCex );
     if ( RetValue == 0 && !fSilent )
         printf( "Aig_ManVerifyUsingBdds(): Counter-example verification has FAILED.\n" );
     }
diff --git a/src/aig/bbr/bbrReach.c b/src/aig/bbr/bbrReach.c
index c2433d45..ef355992 100644
--- a/src/aig/bbr/bbrReach.c
+++ b/src/aig/bbr/bbrReach.c
@@ -19,7 +19,6 @@
 ***********************************************************************/
 
 #include "bbr.h"
-#include "ssw.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -568,7 +567,7 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, Saig_ParBbr_t * pPars )
         else
             Vec_IntPush( vInputMap, -1 );
     // create new pattern
-    pCexNew = Ssw_SmlAllocCounterExample( Saig_ManRegNum(pInit), Saig_ManPiNum(pInit), pCexOld->iFrame+1 );
+    pCexNew = Abc_CexAlloc( Saig_ManRegNum(pInit), Saig_ManPiNum(pInit), pCexOld->iFrame+1 );
     pCexNew->iFrame = pCexOld->iFrame;
     pCexNew->iPo    = pCexOld->iPo;
     // copy the bit-data
diff --git a/src/aig/cec/cecCec.c b/src/aig/cec/cecCec.c
index 0859a9ad..9fd8a03f 100644
--- a/src/aig/cec/cecCec.c
+++ b/src/aig/cec/cecCec.c
@@ -164,7 +164,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
     {
         if ( p->pCexComb != NULL )
         {
-            if ( p->pCexComb && !Gia_ManVerifyCounterExample( p, p->pCexComb, 1 ) )
+            if ( p->pCexComb && !Gia_ManVerifyCex( p, p->pCexComb, 1 ) )
                 Abc_Print( 1, "Counter-example simulation has failed.\n" );
             Abc_Print( 1, "Networks are NOT EQUIVALENT.  " );
             Abc_PrintTime( 1, "Time", clock() - clk );
@@ -220,7 +220,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
     fflush( stdout );
     RetValue = Cec_ManVerifyOld( pNew, pPars->fVerbose, &pPars->iOutFail );
     p->pCexComb = pNew->pCexComb; pNew->pCexComb = NULL;
-    if ( p->pCexComb && !Gia_ManVerifyCounterExample( p, p->pCexComb, 1 ) )
+    if ( p->pCexComb && !Gia_ManVerifyCex( p, p->pCexComb, 1 ) )
         Abc_Print( 1, "Counter-example simulation has failed.\n" );
     Gia_ManStop( pNew );
     return RetValue;
diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c
index b91e8523..c255d50e 100644
--- a/src/aig/cec/cecSeq.c
+++ b/src/aig/cec/cecSeq.c
@@ -338,7 +338,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
     }
     Gia_ManRandom( 1 );
     // prepare starting pattern
-    pState = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), 0, 0 );
+    pState = Abc_CexAlloc( Gia_ManRegNum(pAig), 0, 0 );
     pState->iFrame = -1;
     pState->iPo = -1;
     // prepare SAT solving
@@ -359,7 +359,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
             Abc_Print( 1, "Cec_ManSeqSemiformal: There are only trivial equiv candidates left (PO drivers). Quitting.\n" );
             break;
         }
-//        Gia_ManPrintCounterExample( pState );
+//        Abc_CexPrint( pState );
         // derive speculatively reduced model
 //        pSrm = Gia_ManSpecReduceInit( pAig, pState, pPars->nFrames, pPars->fDualOut );
         pSrm = Gia_ManSpecReduceInitFrames( pAig, pState, pPars->nFrames, &nFramesReal, pPars->fDualOut, pPars->nMinOutputs );
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index aee38d08..a0073ca1 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -376,12 +376,6 @@ extern Fra_Sml_t *         Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int
 extern Fra_Sml_t *         Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords );
 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
 
diff --git a/src/aig/fra/fraBmc.c b/src/aig/fra/fraBmc.c
index ae9e4bc5..3907fcdd 100644
--- a/src/aig/fra/fraBmc.c
+++ b/src/aig/fra/fraBmc.c
@@ -417,7 +417,7 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew
     clk = clock();
     iOutput = Fra_FraigMiterAssertedOutput( pBmc->pAigFrames );
     if ( iOutput >= 0 )
-        pAig->pSeqModel = Fra_SmlTrivCounterExample( pAig, iOutput );
+        pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig), iOutput );
     else
     {
         pBmc->pAigFraig = Fra_FraigEquivence( pBmc->pAigFrames, nBTLimit, 1 );
@@ -428,7 +428,7 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew
             ABC_FREE( pBmc->pAigFraig->pData );
         }
         else if ( iOutput >= 0 )
-            pAig->pSeqModel = Fra_SmlTrivCounterExample( pAig, iOutput );
+            pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig), iOutput );
     }
     if ( fVerbose )
     {
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 7608791f..4b893cb2 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -203,14 +203,14 @@ clk = clock();
 
     if ( pTemp->pSeqModel )
     {
-        if ( !Ssw_SmlRunCounterExample( pTemp, pTemp->pSeqModel ) )
+        if ( !Saig_ManVerifyCex( pTemp, pTemp->pSeqModel ) )
             printf( "Fra_FraigSec(): Counter-example verification has FAILED.\n" );
         if ( Saig_ManPiNum(p) != Saig_ManPiNum(pTemp) )
             printf( "The counter-example is invalid because of phase abstraction.\n" );
         else
         {
         ABC_FREE( p->pSeqModel );
-        p->pSeqModel = Ssw_SmlDupCounterExample( pTemp->pSeqModel, Aig_ManRegNum(p) );
+        p->pSeqModel = Abc_CexDup( pTemp->pSeqModel, Aig_ManRegNum(p) );
         ABC_FREE( pTemp->pSeqModel );
         }
     }
@@ -443,7 +443,7 @@ ABC_PRT( "Time", clock() - clk );
             else
             {
             ABC_FREE( p->pSeqModel );
-            p->pSeqModel = Ssw_SmlDupCounterExample( pNew->pSeqModel, Aig_ManRegNum(p) );
+            p->pSeqModel = Abc_CexDup( pNew->pSeqModel, Aig_ManRegNum(p) );
             ABC_FREE( pNew->pSeqModel );
             }
 
@@ -505,7 +505,7 @@ clk = clock();
                     RetValue = Inter_ManPerformInterpolation( pTemp, pPars, &Depth );
                     if ( pTemp->pSeqModel )
                     {
-                        pCex = p->pSeqModel = Ssw_SmlDupCounterExample( pTemp->pSeqModel, Aig_ManRegNum(p) );
+                        pCex = p->pSeqModel = Abc_CexDup( pTemp->pSeqModel, Aig_ManRegNum(p) );
                         pCex->iPo = i;
                         Aig_ManStop( pTemp );
                         break;
@@ -548,7 +548,7 @@ clk = clock();
             {
                 Abc_Cex_t * pCex;
                 pCex = pNew->pSeqModel = pNewOrpos->pSeqModel; pNewOrpos->pSeqModel = NULL;
-                pCex->iPo = Ssw_SmlFindOutputCounterExample( pNew, pNew->pSeqModel );
+                pCex->iPo = Saig_ManFindFailedPoCex( pNew, pNew->pSeqModel );
             }
             Aig_ManStop( pNewOrpos );
         }
@@ -598,7 +598,7 @@ ABC_PRT( "Time", clock() - clk );
             printf( "Running property directed reachability...\n" );
         RetValue = Pdr_ManSolve( pNewOrpos, pPars, &pCex );
         if ( pCex )
-            pCex->iPo = Ssw_SmlFindOutputCounterExample( pNew, pCex );
+            pCex->iPo = Saig_ManFindFailedPoCex( pNew, pCex );
         Aig_ManStop( pNewOrpos );
         pNew->pSeqModel = pCex;
     }
@@ -665,7 +665,7 @@ ABC_PRT( "Time", clock() - clkTotal );
         else
         {
         ABC_FREE( p->pSeqModel );
-        p->pSeqModel = Ssw_SmlDupCounterExample( pNew->pSeqModel, Aig_ManRegNum(p) );
+        p->pSeqModel = Abc_CexDup( pNew->pSeqModel, Aig_ManRegNum(p) );
         ABC_FREE( pNew->pSeqModel );
         }
     }
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index 25c30989..37620a16 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "fra.h"
+#include "saig.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -879,45 +880,6 @@ Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nW
 
 /**Function*************************************************************
 
-  Synopsis    [Allocates a counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Cex_t * Fra_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames )
-{
-    Abc_Cex_t * pCex;
-    int nWords = Aig_BitWordNum( nRegs + nRealPis * nFrames );
-    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;
-    return pCex;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Frees the counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_SmlFreeCounterExample( Abc_Cex_t * pCex )
-{
-    ABC_FREE( pCex );
-}
-
-/**Function*************************************************************
-
   Synopsis    [Creates sequential counter-example from the simulation info.]
 
   Description []
@@ -960,7 +922,7 @@ Abc_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p )
     assert( iBit < 32 * p->nWordsFrame );
 
     // allocate the counter example
-    pCex = Fra_SmlAllocCounterExample( Aig_ManRegNum(p->pAig), Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 );
+    pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 );
     pCex->iPo    = iPo;
     pCex->iFrame = iFrame;
 
@@ -981,10 +943,10 @@ Abc_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p )
         }
     }
     // verify the counter example
-    if ( !Fra_SmlRunCounterExample( p->pAig, pCex ) )
+    if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
     {
         printf( "Fra_SmlGetCounterExample(): Counter-example is invalid.\n" );
-        Fra_SmlFreeCounterExample( pCex );
+        Abc_CexFree( pCex );
         pCex = NULL;
     }
     return pCex;
@@ -1026,7 +988,7 @@ Abc_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, in
         }
     assert( iPo >= 0 );
     // allocate the counter example
-    pCex = Fra_SmlAllocCounterExample( Aig_ManRegNum(pAig), nTruePis, iFrame + 1 );
+    pCex = Abc_CexAlloc( Aig_ManRegNum(pAig), nTruePis, iFrame + 1 );
     pCex->iPo    = iPo;
     pCex->iFrame = iFrame;
 
@@ -1040,186 +1002,16 @@ Abc_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, in
     }
 
     // verify the counter example
-    if ( !Fra_SmlRunCounterExample( pAig, pCex ) )
+    if ( !Saig_ManVerifyCex( pAig, pCex ) )
     {
         printf( "Fra_SmlGetCounterExample(): Counter-example is invalid.\n" );
-        Fra_SmlFreeCounterExample( pCex );
+        Abc_CexFree( pCex );
         pCex = NULL;
     }
     return pCex;
 
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Make the trivial counter-example for the trivially asserted output.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut )
-{
-    Abc_Cex_t * pCex;
-    int nTruePis, nTruePos, iPo, iFrame;
-    assert( Aig_ManRegNum(pAig) > 0 );
-    nTruePis = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig);
-    nTruePos = Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig);
-    iPo = iFrameOut % nTruePos;
-    iFrame = iFrameOut / nTruePos;
-    // allocate the counter example
-    pCex = Fra_SmlAllocCounterExample( Aig_ManRegNum(pAig), nTruePis, iFrame + 1 );
-    pCex->iPo    = iPo;
-    pCex->iFrame = iFrame;
-    return pCex;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Resimulates the counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p )
-{
-    Fra_Sml_t * pSml;
-    Aig_Obj_t * pObj;
-    int RetValue, i, k, iBit;
-    assert( Aig_ManRegNum(pAig) > 0 );
-    assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) );
-    // start a new sequential simulator
-    pSml = Fra_SmlStart( pAig, 0, p->iFrame+1, 1 );
-    // assign simulation info for the registers
-    iBit = 0;
-    Aig_ManForEachLoSeq( pAig, pObj, i )
-        Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
-    // assign simulation info for the primary inputs
-    for ( i = 0; i <= p->iFrame; i++ )
-        Aig_ManForEachPiSeq( pAig, pObj, k )
-            Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
-    assert( iBit == p->nBits );
-    // run random simulation
-    Fra_SmlSimulateOne( pSml );
-    // check if the given output has failed
-    RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) );
-    Fra_SmlStop( pSml );
-    return RetValue;
-}
-
-/**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 []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Abc_Cex_t * p )
-{
-    Fra_Sml_t * pSml;
-    Aig_Obj_t * pObj;
-    int RetValue, i, k, iBit;
-    unsigned * pSims;
-    assert( Aig_ManRegNum(pAig) > 0 );
-    assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) );
-    // start a new sequential simulator
-    pSml = Fra_SmlStart( pAig, 0, p->iFrame+1, 1 );
-    // assign simulation info for the registers
-    iBit = 0;
-    Aig_ManForEachLoSeq( pAig, pObj, i )
-//        Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
-        Fra_SmlAssignConst( pSml, pObj, 0, 0 );
-    // assign simulation info for the primary inputs
-    iBit = p->nRegs;
-    for ( i = 0; i <= p->iFrame; i++ )
-        Aig_ManForEachPiSeq( pAig, pObj, k )
-            Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
-    assert( iBit == p->nBits );
-    // run random simulation
-    Fra_SmlSimulateOne( pSml );
-    // check if the given output has failed
-    RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) );
-
-    // write the output file
-    for ( i = 0; i <= p->iFrame; i++ )
-    {
-/*
-        Aig_ManForEachLoSeq( pAig, pObj, k )
-        {
-            pSims = Fra_ObjSim(pSml, pObj->Id);
-            fprintf( pFile, "%d", (int)(pSims[i] != 0) );
-        }
-        fprintf( pFile, " " );
-*/
-        Aig_ManForEachPiSeq( pAig, pObj, k )
-        {
-            pSims = Fra_ObjSim(pSml, pObj->Id);
-            fprintf( pFile, "%d", (int)(pSims[i] != 0) );
-        }
-/*
-        fprintf( pFile, " " );
-        Aig_ManForEachPoSeq( pAig, pObj, k )
-        {
-            pSims = Fra_ObjSim(pSml, pObj->Id);
-            fprintf( pFile, "%d", (int)(pSims[i] != 0) );
-        }
-        fprintf( pFile, " " );
-        Aig_ManForEachLiSeq( pAig, pObj, k )
-        {
-            pSims = Fra_ObjSim(pSml, pObj->Id);
-            fprintf( pFile, "%d", (int)(pSims[i] != 0) );
-        }
-*/
-        fprintf( pFile, "\n" );
-    }
-
-    Fra_SmlStop( pSml );
-    return RetValue;
-}
-
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/fsim/fsimSim.c b/src/aig/fsim/fsimSim.c
index 2da7db15..56aeab2f 100644
--- a/src/aig/fsim/fsimSim.c
+++ b/src/aig/fsim/fsimSim.c
@@ -434,7 +434,7 @@ Abc_Cex_t * Fsim_ManGenerateCounter( Aig_Man_t * pAig, int iFrame, int iOut, int
     Abc_Cex_t * p;
     unsigned * pData;
     int f, i, w, iPioId, Counter;
-    p = Ssw_SmlAllocCounterExample( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), iFrame+1 );
+    p = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), iFrame+1 );
     p->iFrame = iFrame;
     p->iPo = iOut;
     // fill in the binary data
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index e3546686..b2f039a7 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -33,6 +33,7 @@
 #include <time.h>
 
 #include "vec.h"
+#include "utilCex.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -788,17 +789,13 @@ extern Vec_Int_t *         Gia_ManCollectPoIds( Gia_Man_t * p );
 extern int                 Gia_ObjIsMuxType( Gia_Obj_t * pNode );
 extern int                 Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t ** ppFan0, Gia_Obj_t ** ppFan1 );
 extern Gia_Obj_t *         Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Obj_t ** ppNodeE );
-extern Abc_Cex_t *         Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames );
-extern Abc_Cex_t *         Gia_ManDeriveCexFromArray( Gia_Man_t * pAig, Vec_Int_t * vValues, int nSkip, int iFrame );
-extern Abc_Cex_t *         Gia_ManCreateFromComb( int nRegs, int nRealPis, int iPo, int * pModel );
-extern Abc_Cex_t *         Gia_ManDupCounterExample( Abc_Cex_t * p, int nRegsNew );
-extern int                 Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut );
-extern void                Gia_ManPrintCounterExample( Abc_Cex_t * p );
 extern int                 Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode );
 extern int                 Gia_ManHasChoices( Gia_Man_t * p );
 extern int                 Gia_ManHasDangling( Gia_Man_t * p );
 extern Vec_Int_t *         Gia_ManGetDangling( Gia_Man_t * p );
 extern void                Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj );
+extern int                 Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut );
+extern int                 Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p );
 /*=== giaCTas.c ===========================================================*/
 typedef struct Tas_Man_t_  Tas_Man_t;
 extern Tas_Man_t *         Tas_ManAlloc( Gia_Man_t * pAig, int nBTLimit );
@@ -808,8 +805,6 @@ extern void                Tas_ManSatPrintStats( Tas_Man_t * p );
 extern int                 Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
 extern int                 Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs );
 
- 
-
 
 ABC_NAMESPACE_HEADER_END
 
diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c
index 38e010f1..607e5ac6 100644
--- a/src/aig/gia/giaAbs.c
+++ b/src/aig/gia/giaAbs.c
@@ -530,8 +530,8 @@ void Gia_ManCexAbstractionStartNew( Gia_Man_t * pGia, Gia_ParAbs_t * pPars )
         {
             printf( "Problem is satisfiable. Found counter-example in frame %d.  ", nFrames-1 );
             Abc_PrintTime( 1, "Time", clk );
-            pGia->pCexSeq = Gia_ManDeriveCexFromArray( pGia, vCex, 0, nFrames-1 );
-            if ( !Gia_ManVerifyCounterExample( pGia, pGia->pCexSeq, 0 ) )
+            pGia->pCexSeq = Abc_CexCreate( Gia_ManRegNum(pGia), Gia_ManPiNum(pGia), Vec_IntArray(vCex), nFrames-1, 0, 0 );
+            if ( !Gia_ManVerifyCex( pGia, pGia->pCexSeq, 0 ) )
                 Abc_Print( 1, "Generated counter-example is INVALID.\n" );
             pPars->Status = 0;
         }
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 4ded9a78..71204548 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -416,7 +416,7 @@ Gia_Man_t * Gia_ManDup( Gia_Man_t * p )
     }
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
     if ( p->pCexSeq )
-        pNew->pCexSeq = Gia_ManDupCounterExample( p->pCexSeq, Gia_ManRegNum(p) );
+        pNew->pCexSeq = Abc_CexDup( p->pCexSeq, Gia_ManRegNum(p) );
     return pNew;
 }
 
@@ -764,7 +764,7 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
         Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
     if ( p->pCexSeq )
-        pNew->pCexSeq = Gia_ManDupCounterExample( p->pCexSeq, Gia_ManRegNum(p) );
+        pNew->pCexSeq = Abc_CexDup( p->pCexSeq, Gia_ManRegNum(p) );
     return pNew;
 }
 
diff --git a/src/aig/gia/giaEra2.c b/src/aig/gia/giaEra2.c
index 64464832..dedbc032 100644
--- a/src/aig/gia/giaEra2.c
+++ b/src/aig/gia/giaEra2.c
@@ -1758,7 +1758,7 @@ int Gia_ManArePerform( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbos
     // verify
     if ( pAig->pCexSeq )
     {
-        if ( !Gia_ManVerifyCounterExample( pAig, pAig->pCexSeq, 0 ) )
+        if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) )
             printf( "Generated counter-example is INVALID.                       \n" );
         else
             printf( "Generated counter-example verified correctly.               \n" );
@@ -1922,7 +1922,7 @@ Abc_Cex_t * Gia_ManAreDeriveCex( Gia_ManAre_t * p, Gia_StaAre_t * pLast )
             Vec_PtrPush( vStates, pSta );
     assert( Vec_PtrSize(vStates) >= 1 );
     // start the counter-example
-    pCex = Gia_ManAllocCounterExample( Gia_ManRegNum(p->pAig), Gia_ManPiNum(p->pAig), Vec_PtrSize(vStates) );
+    pCex = Abc_CexAlloc( Gia_ManRegNum(p->pAig), Gia_ManPiNum(p->pAig), Vec_PtrSize(vStates) );
     pCex->iFrame = Vec_PtrSize(vStates)-1;
     pCex->iPo = p->iOutFail;
     // compute states
diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c
index 1de1a2d4..18e02d81 100644
--- a/src/aig/gia/giaSim.c
+++ b/src/aig/gia/giaSim.c
@@ -436,7 +436,7 @@ Abc_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int
     Abc_Cex_t * p;
     unsigned * pData;
     int f, i, w, iPioId, Counter;
-    p = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
+    p = Abc_CexAlloc( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
     p->iFrame = iFrame;
     p->iPo    = iOut;
     // fill in the binary data
@@ -513,7 +513,7 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
             pPars->iOutFail = iOut;
             pAig->pCexSeq = Gia_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids );
             Abc_Print( 1, "Networks are NOT EQUIVALENT.   Output %d was asserted in frame %d.  ", iOut, i );
-            if ( !Gia_ManVerifyCounterExample( pAig, pAig->pCexSeq, 0 ) )
+            if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) )
             {
 //                Abc_Print( 1, "\n" );
                 Abc_Print( 1, "\nGenerated counter-example is INVALID.                    " );
diff --git a/src/aig/gia/giaSim2.c b/src/aig/gia/giaSim2.c
index 4131f942..e1a5aa07 100644
--- a/src/aig/gia/giaSim2.c
+++ b/src/aig/gia/giaSim2.c
@@ -606,7 +606,7 @@ Abc_Cex_t * Gia_Sim2GenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int
     Abc_Cex_t * p;
     unsigned * pData;
     int f, i, w, Counter;
-    p = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
+    p = Abc_CexAlloc( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
     p->iFrame = iFrame;
     p->iPo = iOut;
     // fill in the binary data
@@ -663,7 +663,7 @@ int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
             pPars->iOutFail = iOut;
             pAig->pCexSeq = Gia_Sim2GenerateCounter( pAig, i, iOut, p->nWords, iPat );
             Abc_Print( 1, "Networks are NOT EQUIVALENT.   Output %d was asserted in frame %d.  ", iOut, i );
-            if ( !Gia_ManVerifyCounterExample( pAig, pAig->pCexSeq, 0 ) )
+            if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) )
             {
 //                Abc_Print( 1, "\n" );
                 Abc_Print( 1, "\nGenerated counter-example is INVALID.                    " );
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 82bdb367..2794956a 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -829,244 +829,6 @@ Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Ob
 
 /**Function*************************************************************
 
-  Synopsis    [Allocates a counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames )
-{
-    Abc_Cex_t * pCex;
-    int nWords = Gia_BitWordNum( nRegs + nRealPis * nFrames );
-    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;
-    return pCex;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Prints the counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_ManPrintCex( Abc_Cex_t * p )
-{
-    int i, f, k;
-    for ( k = 0; k < p->nRegs; k++ )
-        printf( "%d", Gia_InfoHasBit(p->pData, k) );
-    printf( "\n" );
-    for ( f = 0; f <= p->iFrame; f++ )
-    {
-        for ( i = 0; i < p->nPis; i++ )
-            printf( "%d", Gia_InfoHasBit(p->pData, k++) );
-        printf( "\n" );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Cex_t * Gia_ManDeriveCexFromArray( Gia_Man_t * pAig, Vec_Int_t * vValues, int nSkip, int iFrame )
-{
-    Abc_Cex_t * pCex;
-    int i;
-    pCex = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
-    assert( Vec_IntSize(vValues) == nSkip + pCex->nBits );
-    pCex->iPo    = 0;
-    pCex->iFrame = iFrame;
-    for ( i = 0; i < pCex->nBits; i++ )
-        if ( Vec_IntEntry(vValues, nSkip + i) )
-            Gia_InfoSetBit( pCex->pData, i );
-    return pCex;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates a counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Cex_t * Gia_ManCreateFromComb( int nRegs, int nRealPis, int iPo, int * pModel )
-{
-    Abc_Cex_t * pCex;
-    int i;
-    pCex = Gia_ManAllocCounterExample( nRegs, nRealPis, 1 );
-    pCex->iPo    = iPo;
-    pCex->iFrame = 0;
-    for ( i = pCex->nRegs; i < pCex->nBits; i++ )
-        if ( pModel[i-pCex->nRegs] )
-            Gia_InfoSetBit( pCex->pData, i );
-    return pCex;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Resimulates the counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut )
-{
-    Gia_Obj_t * pObj, * pObjRi, * pObjRo;
-    int RetValue, i, k, iBit = 0;
-    Gia_ManCleanMark0(pAig);
-    Gia_ManForEachRo( pAig, pObj, i )
-        pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
-    for ( i = 0; i <= p->iFrame; i++ )
-    {
-        Gia_ManForEachPi( pAig, pObj, k )
-            pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
-        Gia_ManForEachAnd( pAig, pObj, k )
-            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
-                           (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
-        Gia_ManForEachCo( pAig, pObj, k )
-            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
-        if ( i == p->iFrame )
-            break;
-        Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
-        {
-            pObjRo->fMark0 = pObjRi->fMark0;
-        }
-    }
-    assert( iBit == p->nBits );
-    if ( fDualOut )
-        RetValue = Gia_ManPo(pAig, 2*p->iPo)->fMark0 ^ Gia_ManPo(pAig, 2*p->iPo+1)->fMark0;
-    else
-        RetValue = Gia_ManPo(pAig, p->iPo)->fMark0;
-    Gia_ManCleanMark0(pAig);
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Resimulates the counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Gia_ManVerifyCounterExampleAllOuts( Gia_Man_t * pAig, Abc_Cex_t * p )
-{
-    Gia_Obj_t * pObj, * pObjRi, * pObjRo;
-    int RetValue, i, k, iBit = 0;
-    Gia_ManCleanMark0(pAig);
-    Gia_ManForEachRo( pAig, pObj, i )
-        pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
-    for ( i = 0; i <= p->iFrame; i++ )
-    {
-        Gia_ManForEachPi( pAig, pObj, k )
-            pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
-        Gia_ManForEachAnd( pAig, pObj, k )
-            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
-                           (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
-        Gia_ManForEachCo( pAig, pObj, k )
-            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
-        Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
-            pObjRo->fMark0 = pObjRi->fMark0;
-    }
-    assert( iBit == p->nBits );
-    // remember the number of failed output
-    RetValue = -1;
-    Gia_ManForEachPo( pAig, pObj, i )
-        if ( Gia_ManPo(pAig, i)->fMark0 )
-        {
-            RetValue = i;
-            break;
-        }
-    Gia_ManCleanMark0(pAig);
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Make the trivial counter-example for the trivially asserted output.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Cex_t * Gia_ManDupCounterExample( Abc_Cex_t * p, int nRegsNew )
-{
-    Abc_Cex_t * pCex;
-    int i;
-    pCex = Gia_ManAllocCounterExample( nRegsNew, p->nPis, p->iFrame+1 );
-    pCex->iPo    = p->iPo;
-    pCex->iFrame = p->iFrame;
-    for ( i = p->nRegs; i < p->nBits; i++ )
-        if ( Gia_InfoHasBit(p->pData, i) )
-            Gia_InfoSetBit( pCex->pData, pCex->nRegs + i - p->nRegs );
-    return pCex;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints out the counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_ManPrintCounterExample( Abc_Cex_t * p )
-{
-    int i, f, k;
-    printf( "Counter-example: iPo = %d  iFrame = %d  nRegs = %d  nPis = %d  nBits = %d\n", 
-        p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits );
-    printf( "State    : " );
-    for ( k = 0; k < p->nRegs; k++ )
-        printf( "%d", Gia_InfoHasBit(p->pData, k) );
-    printf( "\n" );
-    for ( f = 0; f <= p->iFrame; f++ )
-    {
-        printf( "Frame %2d : ", f );
-        for ( i = 0; i < p->nPis; i++ )
-            printf( "%d", Gia_InfoHasBit(p->pData, k++) );
-        printf( "\n" );
-    }
-    assert( k == p->nBits );
-}
-
-/**Function*************************************************************
-
   Synopsis    [Dereferences the node's MFFC.]
 
   Description []
@@ -1371,6 +1133,91 @@ void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj )
 */
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Resimulates the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut )
+{
+    Gia_Obj_t * pObj, * pObjRi, * pObjRo;
+    int RetValue, i, k, iBit = 0;
+    Gia_ManCleanMark0(pAig);
+    Gia_ManForEachRo( pAig, pObj, i )
+        pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
+    for ( i = 0; i <= p->iFrame; i++ )
+    {
+        Gia_ManForEachPi( pAig, pObj, k )
+            pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
+        Gia_ManForEachAnd( pAig, pObj, k )
+            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
+                           (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
+        Gia_ManForEachCo( pAig, pObj, k )
+            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+        if ( i == p->iFrame )
+            break;
+        Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
+        {
+            pObjRo->fMark0 = pObjRi->fMark0;
+        }
+    }
+    assert( iBit == p->nBits );
+    if ( fDualOut )
+        RetValue = Gia_ManPo(pAig, 2*p->iPo)->fMark0 ^ Gia_ManPo(pAig, 2*p->iPo+1)->fMark0;
+    else
+        RetValue = Gia_ManPo(pAig, p->iPo)->fMark0;
+    Gia_ManCleanMark0(pAig);
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resimulates the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p )
+{
+    Gia_Obj_t * pObj, * pObjRi, * pObjRo;
+    int RetValue, i, k, iBit = 0;
+    Gia_ManCleanMark0(pAig);
+    Gia_ManForEachRo( pAig, pObj, i )
+        pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
+    for ( i = 0; i <= p->iFrame; i++ )
+    {
+        Gia_ManForEachPi( pAig, pObj, k )
+            pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
+        Gia_ManForEachAnd( pAig, pObj, k )
+            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
+                           (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
+        Gia_ManForEachCo( pAig, pObj, k )
+            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+        Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
+            pObjRo->fMark0 = pObjRi->fMark0;
+    }
+    assert( iBit == p->nBits );
+    // remember the number of failed output
+    RetValue = -1;
+    Gia_ManForEachPo( pAig, pObj, i )
+        if ( Gia_ManPo(pAig, i)->fMark0 )
+        {
+            RetValue = i;
+            break;
+        }
+    Gia_ManCleanMark0(pAig);
+    return RetValue;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/int/intCtrex.c b/src/aig/int/intCtrex.c
index 28b1e293..0aa60040 100644
--- a/src/aig/int/intCtrex.c
+++ b/src/aig/int/intCtrex.c
@@ -133,7 +133,7 @@ void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose )
     if ( status == l_True )
     {
         int i, * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
-        pCtrex = Ssw_SmlAllocCounterExample( Saig_ManRegNum(pAig), Saig_ManPiNum(pAig), nFrames );
+        pCtrex = Abc_CexAlloc( Saig_ManRegNum(pAig), Saig_ManPiNum(pAig), nFrames );
         pCtrex->iFrame = nFrames - 1;
         pCtrex->iPo = 0;
         for ( i = 0; i < Vec_IntSize(vCiIds); i++ )
@@ -145,7 +145,7 @@ void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose )
     sat_solver_delete( pSat );
     Vec_IntFree( vCiIds );
     // verify counter-example
-    status = Ssw_SmlRunCounterExample( pAig, pCtrex );
+    status = Saig_ManVerifyCex( pAig, pCtrex );
     if ( status == 0 )
         printf( "Inter_ManGetCounterExample(): Counter-example verification has FAILED.\n" );
     // report the results
diff --git a/src/aig/llb/llb2Core.c b/src/aig/llb/llb2Core.c
index 596a34af..4685db0e 100644
--- a/src/aig/llb/llb2Core.c
+++ b/src/aig/llb/llb2Core.c
@@ -94,7 +94,6 @@ DdNode * Llb_CoreComputeCube( DdManager * dd, Vec_Int_t * vVars, int fUseVarInde
 ***********************************************************************/
 Abc_Cex_t * Llb_CoreDeriveCex( Llb_Img_t * p )
 {
-    extern Abc_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames );
     Abc_Cex_t * pCex;
     Aig_Obj_t * pObj;
     Vec_Ptr_t * vSupps, * vQuant0, * vQuant1;
@@ -112,7 +111,7 @@ Abc_Cex_t * Llb_CoreDeriveCex( Llb_Img_t * p )
 //    Llb_ImgQuantifyFirst( p->pAig, p->vDdMans, vQuant0 );
 
     // allocate room for the counter-example
-    pCex = Ssw_SmlAllocCounterExample( Saig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Vec_PtrSize(p->vRings) );
+    pCex = Abc_CexAlloc( Saig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Vec_PtrSize(p->vRings) );
     pCex->iFrame = Vec_PtrSize(p->vRings) - 1;
     pCex->iPo = -1;
 
@@ -178,7 +177,7 @@ Abc_Cex_t * Llb_CoreDeriveCex( Llb_Img_t * p )
     }
     assert( nPiOffset == Saig_ManRegNum(p->pAig) );
     // update the output number
-    RetValue = Ssw_SmlFindOutputCounterExample( p->pInit, pCex );
+    RetValue = Saig_ManFindFailedPoCex( p->pInit, pCex );
     assert( RetValue >= 0 && RetValue < Saig_ManPoNum(p->pInit) ); // invalid CEX!!!
     pCex->iPo = RetValue;
     // cleanup
diff --git a/src/aig/llb/llb3Nonlin.c b/src/aig/llb/llb3Nonlin.c
index e52e28ca..62ce441c 100644
--- a/src/aig/llb/llb3Nonlin.c
+++ b/src/aig/llb/llb3Nonlin.c
@@ -237,7 +237,6 @@ DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd )
 ***********************************************************************/
 Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p )
 {
-    extern Abc_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames );
     Abc_Cex_t * pCex;
     Aig_Obj_t * pObj;
     Vec_Int_t * vVarsNs;
@@ -263,7 +262,7 @@ Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p )
     printf( "\n" );
 */
     // allocate room for the counter-example
-    pCex = Ssw_SmlAllocCounterExample( Saig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Vec_PtrSize(p->vRings) );
+    pCex = Abc_CexAlloc( Saig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Vec_PtrSize(p->vRings) );
     pCex->iFrame = Vec_PtrSize(p->vRings) - 1;
     pCex->iPo = -1;
 
@@ -330,7 +329,8 @@ Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p )
     }
     assert( nPiOffset == Saig_ManRegNum(p->pAig) );
     // update the output number
-    RetValue = Ssw_SmlFindOutputCounterExample( p->pInit, pCex );
+//Abc_CexPrint( pCex );
+    RetValue = Saig_ManFindFailedPoCex( p->pInit, pCex );
     assert( RetValue >= 0 && RetValue < Saig_ManPoNum(p->pInit) ); // invalid CEX!!!
     pCex->iPo = RetValue;
     // cleanup
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index b1017bdb..bf5681b9 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -149,6 +149,8 @@ extern Aig_Man_t *       Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFr
 extern Aig_Man_t *       Saig_ManDupOrpos( Aig_Man_t * p );
 extern Aig_Man_t *       Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs );
 extern Aig_Man_t *       Saig_ManDeriveAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops );
+extern int               Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p );
+extern int               Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p );
 /*=== saigHaig.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose );
 /*=== saigInd.c ==========================================================*/
diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c
index 938a66e2..471d5d2d 100644
--- a/src/aig/saig/saigAbs.c
+++ b/src/aig/saig/saigAbs.c
@@ -101,12 +101,12 @@ Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexA
     Abc_Cex_t * pCex;
     Aig_Obj_t * pObj;
     int i, f;
-    if ( !Ssw_SmlRunCounterExample( pAbs, pCexAbs ) )
+    if ( !Saig_ManVerifyCex( pAbs, pCexAbs ) )
         printf( "Saig_ManCexRemap(): The intial counter-example is invalid.\n" );
     else
         printf( "Saig_ManCexRemap(): The intial counter-example is correct.\n" );
     // start the counter-example
-    pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(p), Saig_ManPiNum(p), pCexAbs->iFrame+1 );
+    pCex = Abc_CexAlloc( Aig_ManRegNum(p), Saig_ManPiNum(p), pCexAbs->iFrame+1 );
     pCex->iFrame = pCexAbs->iFrame;
     pCex->iPo    = pCexAbs->iPo;
     // copy the bit data
@@ -121,10 +121,10 @@ Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexA
         }
     }
     // verify the counter example
-    if ( !Ssw_SmlRunCounterExample( p, pCex ) )
+    if ( !Saig_ManVerifyCex( p, pCex ) )
     {
         printf( "Saig_ManCexRemap(): Counter-example is invalid.\n" );
-        Ssw_SmlFreeCounterExample( pCex );
+        Abc_CexFree( pCex );
         pCex = NULL;
     }
     else
@@ -194,7 +194,7 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo
             printf( "Running property directed reachability...\n" );
         RetValue = Pdr_ManSolve( pAbsOrpos, pPars, &pCex );
         if ( pCex )
-            pCex->iPo = Ssw_SmlFindOutputCounterExample( pAbs, pCex );
+            pCex->iPo = Saig_ManFindFailedPoCex( pAbs, pCex );
         Aig_ManStop( pAbsOrpos );
         pAbs->pSeqModel = pCex;
         if ( RetValue )
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c
index 8aa3af80..cb506054 100644
--- a/src/aig/saig/saigBmc.c
+++ b/src/aig/saig/saigBmc.c
@@ -301,11 +301,10 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
             }
             else if ( status == l_True )
             {
-//                extern void * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel );
                 Vec_Int_t * vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames );
                 int * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
                 pModel[Aig_ManPiNum(pFrames)] = pObj->Id;
-                pAig->pSeqModel = (Abc_Cex_t *)Fra_SmlCopyCounterExample( pAig, pFrames, pModel );
+                pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pFrames, pModel );
                 ABC_FREE( pModel );
                 Vec_IntFree( vCiIds );
 
diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c
index 3d57ae6e..9c36deb3 100644
--- a/src/aig/saig/saigBmc2.c
+++ b/src/aig/saig/saigBmc2.c
@@ -637,7 +637,7 @@ Abc_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p )
     Aig_Obj_t * pObj, * pObjFrm;
     int i, f, iVarNum;
     // start the counter-example
-    pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), p->iFrameFail+1 );
+    pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), p->iFrameFail+1 );
     pCex->iFrame = p->iFrameFail;
     pCex->iPo    = p->iOutputFail;
     // copy the bit data
@@ -656,10 +656,10 @@ Abc_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p )
         }
     }
     // verify the counter example
-    if ( !Ssw_SmlRunCounterExample( p->pAig, pCex ) )
+    if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
     {
         printf( "Saig_BmcGenerateCounterExample(): Counter-example is invalid.\n" );
-        Ssw_SmlFreeCounterExample( pCex );
+        Abc_CexFree( pCex );
         pCex = NULL;
     }
     return pCex;
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c
index a75297f7..570e8a26 100644
--- a/src/aig/saig/saigBmc3.c
+++ b/src/aig/saig/saigBmc3.c
@@ -1108,8 +1108,7 @@ clkOther += clock() - clk2;
                 continue;
             if ( Lit == 1 )
             {
-                extern Abc_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut );
-                Abc_Cex_t * pCex = Fra_SmlTrivCounterExample( pAig, f*Saig_ManPoNum(pAig)+i );
+                Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i );
                 printf( "Output %d is trivially SAT in frame %d.\n", i, f );
                 if ( !pPars->fSolveAll )
                 {
@@ -1137,9 +1136,8 @@ clkOther += clock() - clk2;
             }
             else if ( status == l_True )
             {
-//                extern void * Fra_SmlSimpleCounterExample( Aig_Man_t * p, int * pModel, int iFrame, int iPo );
                 int * pModel = Sat_SolverGetModel( p->pSat, Vec_IntArray(p->vPiVars), Vec_IntSize(p->vPiVars) );
-                Abc_Cex_t * pCex = Fra_SmlSimpleCounterExample( pAig, pModel, f, i );
+                Abc_Cex_t * pCex = Abc_CexCreate( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), pModel, f, i, 1 );
                 ABC_FREE( pModel );
                 fFirst = 0;
                 if ( !pPars->fSolveAll )
diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c
index f4e557f8..b2b33bdb 100644
--- a/src/aig/saig/saigDup.c
+++ b/src/aig/saig/saigDup.c
@@ -265,6 +265,91 @@ Aig_Man_t * Saig_ManDeriveAbstraction( Aig_Man_t * p, Vec_Int_t * vFlops )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Resimulates the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p )
+{
+    Aig_Obj_t * pObj, * pObjRi, * pObjRo;
+    int RetValue, i, k, iBit = 0;
+    Aig_ManCleanMarkB(pAig);
+    Aig_ManConst1(pAig)->fMarkB = 1;
+    Saig_ManForEachLo( pAig, pObj, i )
+        pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++);
+    for ( i = 0; i <= p->iFrame; i++ )
+    {
+        Saig_ManForEachPi( pAig, pObj, k )
+            pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++);
+        Aig_ManForEachNode( pAig, pObj, k )
+            pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & 
+                           (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
+        Aig_ManForEachPo( pAig, pObj, k )
+            pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
+        if ( i == p->iFrame )
+            break;
+        Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
+            pObjRo->fMarkB = pObjRi->fMarkB;
+    }
+    assert( iBit == p->nBits );
+    RetValue = Aig_ManPo(pAig, p->iPo)->fMarkB;
+    Aig_ManCleanMarkB(pAig);
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resimulates the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p )
+{
+    Aig_Obj_t * pObj, * pObjRi, * pObjRo;
+    int RetValue, i, k, iBit = 0;
+    Aig_ManCleanMarkB(pAig);
+    Aig_ManConst1(pAig)->fMarkB = 1;
+    Saig_ManForEachLo( pAig, pObj, i )
+        pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++);
+    for ( i = 0; i <= p->iFrame; i++ )
+    {
+        Saig_ManForEachPi( pAig, pObj, k )
+            pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++);
+        Aig_ManForEachNode( pAig, pObj, k )
+            pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & 
+                           (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
+        Aig_ManForEachPo( pAig, pObj, k )
+            pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
+        if ( i == p->iFrame )
+            break;
+        Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
+            pObjRo->fMarkB = pObjRi->fMarkB;
+    }
+    assert( iBit == p->nBits );
+    // remember the number of failed output
+    RetValue = -1;
+    Saig_ManForEachPo( pAig, pObj, i )
+        if ( pObj->fMarkB )
+        {
+            RetValue = i;
+            break;
+        }
+    Aig_ManCleanMarkB(pAig);
+    return RetValue;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/saig/saigSimSeq.c b/src/aig/saig/saigSimSeq.c
index 37bb12b5..cc5a9e05 100644
--- a/src/aig/saig/saigSimSeq.c
+++ b/src/aig/saig/saigSimSeq.c
@@ -418,7 +418,7 @@ Abc_Cex_t * Raig_ManGenerateCounter( Aig_Man_t * pAig, int iFrame, int iOut, int
     Abc_Cex_t * p;
     unsigned * pData;
     int f, i, w, iPioId, Counter;
-    p = Ssw_SmlAllocCounterExample( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), iFrame+1 );
+    p = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), iFrame+1 );
     p->iFrame = iFrame;
     p->iPo = iOut;
     // fill in the binary data
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index bf8c918e..437e6ec8 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -123,18 +123,9 @@ extern int           Ssw_SmlNumFrames( Ssw_Sml_t * p );
 extern int           Ssw_SmlNumWordsTotal( Ssw_Sml_t * p );
 extern unsigned *    Ssw_SmlSimInfo( Ssw_Sml_t * p, Aig_Obj_t * pObj );
 extern int           Ssw_SmlObjsAreEqualWord( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
-extern Abc_Cex_t *   Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames );
-extern void          Ssw_SmlFreeCounterExample( Abc_Cex_t * pCex );
-extern int           Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p );
-extern int           Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p );
-extern Abc_Cex_t *   Ssw_SmlDupCounterExample( Abc_Cex_t * p, int nRegsNew );
-
-
 
 ABC_NAMESPACE_HEADER_END
 
-
-
 #endif
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ssw/sswBmc.c b/src/aig/ssw/sswBmc.c
index aba32304..d565d5d3 100644
--- a/src/aig/ssw/sswBmc.c
+++ b/src/aig/ssw/sswBmc.c
@@ -94,7 +94,7 @@ Abc_Cex_t * Ssw_BmcGetCounterExample( Ssw_Frm_t * pFrm, Ssw_Sat_t * pSat, int iP
     int f, i, nShift;
     assert( Saig_ManRegNum(pFrm->pAig) > 0 );
     // allocate the counter example
-    pCex = Ssw_SmlAllocCounterExample( Saig_ManRegNum(pFrm->pAig), Saig_ManPiNum(pFrm->pAig), iFrame + 1 );
+    pCex = Abc_CexAlloc( Saig_ManRegNum(pFrm->pAig), Saig_ManPiNum(pFrm->pAig), iFrame + 1 );
     pCex->iPo    = iPo;
     pCex->iFrame = iFrame;
     // create data-bits
diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c
index 404302f2..e68f08cd 100644
--- a/src/aig/ssw/sswSim.c
+++ b/src/aig/ssw/sswSim.c
@@ -1248,131 +1248,6 @@ unsigned * Ssw_SmlSimInfo( Ssw_Sml_t * p, Aig_Obj_t * pObj )
     return Ssw_ObjSim( p, pObj->Id );
 }
 
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates a counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames )
-{
-    Abc_Cex_t * pCex;
-    int nWords = Aig_BitWordNum( nRegs + nRealPis * nFrames );
-    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;
-    return pCex;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Frees the counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ssw_SmlFreeCounterExample( Abc_Cex_t * pCex )
-{
-    ABC_FREE( pCex );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Resimulates the counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p )
-{ 
-    Ssw_Sml_t * pSml;
-    Aig_Obj_t * pObj;
-    int RetValue, i, k, iBit;
-    if ( Saig_ManPiNum(pAig) != p->nPis )
-        return 0;
-//    if ( Saig_ManRegNum(pAig) != p->nRegs )
-//        return 0;
-//    assert( Aig_ManRegNum(pAig) > 0 );
-//    assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) );
-    // start a new sequential simulator
-    pSml = Ssw_SmlStart( pAig, 0, p->iFrame+1, 1 );
-    // assign simulation info for the registers
-    iBit = 0;
-    Saig_ManForEachLo( pAig, pObj, i )
-        Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
-    // assign simulation info for the primary inputs
-    iBit = Saig_ManRegNum(pAig);
-    for ( i = 0; i <= p->iFrame; i++ )
-        Saig_ManForEachPi( pAig, pObj, k )
-            Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
-//    assert( iBit == p->nBits );
-    // run random simulation
-    Ssw_SmlSimulateOne( pSml );
-    // check if the given output has failed
-    RetValue = !Ssw_SmlNodeIsZeroFrame( pSml, Aig_ManPo(pAig, p->iPo), p->iFrame );
-    Ssw_SmlStop( pSml );
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Resimulates the counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p )
-{
-    Ssw_Sml_t * pSml;
-    Aig_Obj_t * pObj;
-    int i, k, iBit, iOut;
-    assert( Aig_ManRegNum(pAig) > 0 );
-    assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) );
-    // start a new sequential simulator
-    pSml = Ssw_SmlStart( pAig, 0, p->iFrame+1, 1 );
-    // assign simulation info for the registers
-    iBit = 0;
-    Saig_ManForEachLo( pAig, pObj, i )
-        Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
-    // assign simulation info for the primary inputs
-    for ( i = 0; i <= p->iFrame; i++ )
-        Saig_ManForEachPi( pAig, pObj, k )
-            Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
-    assert( iBit == p->nBits );
-    // run random simulation
-    Ssw_SmlSimulateOne( pSml );
-    // check if the given output has failed
-    iOut = -1;
-    Saig_ManForEachPo( pAig, pObj, k )
-        if ( !Ssw_SmlNodeIsZeroFrame( pSml, Aig_ManPo(pAig, k), p->iFrame ) )
-        {
-            iOut = k;
-            break;
-        }
-    Ssw_SmlStop( pSml );
-    return iOut;
-}
-
 /**Function*************************************************************
 
   Synopsis    [Creates sequential counter-example from the simulation info.]
@@ -1417,7 +1292,7 @@ Abc_Cex_t * Ssw_SmlGetCounterExample( Ssw_Sml_t * p )
     assert( iBit < 32 * p->nWordsFrame );
 
     // allocate the counter example
-    pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(p->pAig), Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 );
+    pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 );
     pCex->iPo    = iPo;
     pCex->iFrame = iFrame;
 
@@ -1438,126 +1313,14 @@ Abc_Cex_t * Ssw_SmlGetCounterExample( Ssw_Sml_t * p )
         }
     }
     // verify the counter example
-    if ( !Ssw_SmlRunCounterExample( p->pAig, pCex ) )
+    if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
     {
         printf( "Ssw_SmlGetCounterExample(): Counter-example is invalid.\n" );
-        Ssw_SmlFreeCounterExample( pCex );
+        Abc_CexFree( pCex );
         pCex = NULL;
     }
     return pCex;
 }
- 
-/**Function*************************************************************
-
-  Synopsis    [Generates seq counter-example from the combinational one.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Cex_t * Ssw_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel )
-{
-    Abc_Cex_t * pCex;
-    Aig_Obj_t * pObj;
-    int i, nFrames, nTruePis, nTruePos, iPo, iFrame;
-    // get the number of frames
-    assert( Aig_ManRegNum(pAig) > 0 );
-    assert( Aig_ManRegNum(pFrames) == 0 );
-    nTruePis = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig);
-    nTruePos = Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig);
-    nFrames = Aig_ManPiNum(pFrames) / nTruePis;
-    assert( nTruePis * nFrames == Aig_ManPiNum(pFrames) );
-    assert( nTruePos * nFrames == Aig_ManPoNum(pFrames) );
-    // find the PO that failed
-    iPo = -1;
-    iFrame = -1;
-    Aig_ManForEachPo( pFrames, pObj, i )
-        if ( pObj->Id == pModel[Aig_ManPiNum(pFrames)] )
-        {
-            iPo = i % nTruePos;
-            iFrame = i / nTruePos;
-            break;
-        }
-    assert( iPo >= 0 );
-    // allocate the counter example
-    pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(pAig), nTruePis, iFrame + 1 );
-    pCex->iPo    = iPo;
-    pCex->iFrame = iFrame;
-
-    // copy the bit data
-    for ( i = 0; i < Aig_ManPiNum(pFrames); i++ )
-    {
-        if ( pModel[i] )
-            Aig_InfoSetBit( pCex->pData, pCex->nRegs + i );
-        if ( pCex->nRegs + i == pCex->nBits - 1 )
-            break;
-    }
-
-    // verify the counter example
-    if ( !Ssw_SmlRunCounterExample( pAig, pCex ) )
-    {
-        printf( "Ssw_SmlGetCounterExample(): Counter-example is invalid.\n" );
-        Ssw_SmlFreeCounterExample( pCex );
-        pCex = NULL;
-    }
-    return pCex;
-
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Make the trivial counter-example for the trivially asserted output.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Cex_t * Ssw_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut )
-{
-    Abc_Cex_t * pCex;
-    int nTruePis, nTruePos, iPo, iFrame;
-    assert( Aig_ManRegNum(pAig) > 0 );
-    nTruePis = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig);
-    nTruePos = Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig);
-    iPo = iFrameOut % nTruePos;
-    iFrame = iFrameOut / nTruePos;
-    // allocate the counter example
-    pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(pAig), nTruePis, iFrame + 1 );
-    pCex->iPo    = iPo;
-    pCex->iFrame = iFrame;
-    return pCex;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Make the trivial counter-example for the trivially asserted output.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Cex_t * Ssw_SmlDupCounterExample( Abc_Cex_t * p, int nRegsNew )
-{
-    Abc_Cex_t * pCex;
-    int i;
-    pCex = Ssw_SmlAllocCounterExample( nRegsNew, p->nPis, p->iFrame+1 );
-    pCex->iPo    = p->iPo;
-    pCex->iFrame = p->iFrame;
-    for ( i = p->nRegs; i < p->nBits; i++ )
-        if ( Aig_InfoHasBit(p->pData, i) )
-            Aig_InfoSetBit( pCex->pData, pCex->nRegs + i - p->nRegs );
-    return pCex;
-}
-
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///