Version abc80919

33 files changed, 1026 insertions, 229 deletions

diff --git a/src/aig/bbr/bbrCex.c b/src/aig/bbr/bbrCex.c
index f5981439..be5377af 100644
--- a/src/aig/bbr/bbrCex.c
+++ b/src/aig/bbr/bbrCex.c
@@ -19,48 +19,21 @@
 ***********************************************************************/
 
 #include "bbr.h"
+#include "ssw.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+extern DdNode * Bbr_bddComputeRangeCube( DdManager * dd, int iStart, int iStop );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Computes the initial state and sets up the variable map.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManStateVarMap( DdManager * dd, Aig_Man_t * p, int fVerbose )
-{
-    DdNode ** pbVarsX, ** pbVarsY;
-    Aig_Obj_t * pLatch;
-    int i;
-
-    // set the variable mapping for Cudd_bddVarMap()
-    pbVarsX = ALLOC( DdNode *, dd->size );
-    pbVarsY = ALLOC( DdNode *, dd->size );
-    Saig_ManForEachLo( p, pLatch, i )
-    {
-        pbVarsY[i] = dd->vars[ Saig_ManPiNum(p) + i ];
-        pbVarsX[i] = dd->vars[ Saig_ManCiNum(p) + i ];
-    }
-    Cudd_SetVarMap( dd, pbVarsX, pbVarsY, Saig_ManRegNum(p) );
-    FREE( pbVarsX );
-    FREE( pbVarsY );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
+  Synopsis    [Derives the counter-example using the set of reached states.]
 
   Description []
                
@@ -69,105 +42,122 @@ void Aig_ManStateVarMap( DdManager * dd, Aig_Man_t * p, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-int Aig_ManComputeCountExample( Aig_Man_t * p, DdManager * dd, DdNode ** pbParts, Vec_Ptr_t * vCareSets, int nBddMax, int fVerbose, int fSilent )
+Ssw_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd, 
+    DdNode ** pbParts, Vec_Ptr_t * vOnionRings, DdNode * bCubeFirst,
+    int iOutput, int fVerbose, int fSilent )
 {
-/*
-    Bbr_ImageTree_t * pTree = NULL; // Suppress "might be used uninitialized"
-    DdNode * bCubeCs;
-    DdNode * bCurrent;
-    DdNode * bNext = NULL; // Suppress "might be used uninitialized"
-    DdNode * bTemp;
-    DdNode ** pbVarsY;
+    Ssw_Cex_t * pCex;
     Aig_Obj_t * pObj;
-    int i, nIters, nBddSize;
-    int nThreshold = 10000;
-    int * pCex;
+    Bbr_ImageTree_t * pTree;
+    DdNode * bCubeNs, * bState, * bImage;
+    DdNode * bTemp, * bVar, * bRing;
+    int i, v, RetValue, nPiOffset;
     char * pValues;
+    int clk = clock();
 
     // allocate room for the counter-example
-    pCex = ALLOC( int, Vec_PtrSize(vCareSets) );
+    pCex = Ssw_SmlAllocCounterExample( 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);
+
+    // create the cube of NS variables
+    bCubeNs  = Bbr_bddComputeRangeCube( dd, Saig_ManCiNum(p), Saig_ManCiNum(p)+Saig_ManRegNum(p) );    Cudd_Ref( bCubeNs );
+    pTree = Bbr_bddImageStart( dd, bCubeNs, Saig_ManRegNum(p), pbParts, Saig_ManCiNum(p), dd->vars, fVerbose );
+    Cudd_RecursiveDeref( dd, bCubeNs );
+    if ( pTree == NULL )
+    {
+        if ( !fSilent )
+            printf( "BDDs blew up during qualitification scheduling.  " );
+        return NULL;
+    }
 
     // allocate room for the cube
     pValues = ALLOC( char, dd->size );
 
-    // collect the NS variables
-    // set the variable mapping for Cudd_bddVarMap()
-    pbVarsY = ALLOC( DdNode *, dd->size );
-    Aig_ManForEachPi( p, pObj, i )
-        pbVarsY[i] = dd->vars[ i ];
+    // get the last cube
+    RetValue = Cudd_bddPickOneCube( dd, bCubeFirst, pValues );
+    assert( RetValue );
 
-    // create the initial state and the variable map
-    Aig_ManStateVarMap( dd, p, fVerbose );
+    // write PIs of counter-example
+    Saig_ManForEachPi( p, pObj, i )
+        if ( pValues[i] == 1 )
+            Aig_InfoSetBit( pCex->pData, nPiOffset + i );
+    nPiOffset -= Saig_ManPiNum(p);
 
-    // start the image computation
-    bCubeCs  = Bbr_bddComputeRangeCube( dd, Aig_ManPiNum(p), 2*Saig_ManCiNum(p) );    Cudd_Ref( bCubeCs );
-    pTree = Bbr_bddImageStart( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), pbVarsY, fVerbose );
-    Cudd_RecursiveDeref( dd, bCubeCs );
-    free( pbVarsY );
-    if ( pTree == NULL )
+    // write state in terms of NS variables
+    bState = (dd)->one; Cudd_Ref( bState );
+    Saig_ManForEachLo( p, pObj, i )
     {
-        if ( !fSilent )
-            printf( "BDDs blew up during qualitification scheduling.  " );
-        return -1;
+        bVar = Cudd_NotCond( dd->vars[Saig_ManCiNum(p)+i], pValues[Saig_ManPiNum(p)+i] != 1 );
+        bState = Cudd_bddAnd( dd, bTemp = bState, bVar );  Cudd_Ref( bState );
+        Cudd_RecursiveDeref( dd, bTemp ); 
     }
 
-    // create counter-example in terms of next state variables
-    // pNext = ...
-
-    // perform reachability analisys
-    Vec_PtrForEachEntryReverse( vCareSets, pCurrent, i )
+    // perform backward analysis
+    Vec_PtrForEachEntryReverse( vOnionRings, bRing, v )
     { 
         // compute the next states
-        bImage = Bbr_bddImageCompute( pTree, bCurrent );           
+        bImage = Bbr_bddImageCompute( pTree, bState );           
         if ( bImage == NULL )
         {
+            Cudd_RecursiveDeref( dd, bState );
             if ( !fSilent )
                 printf( "BDDs blew up during image computation.  " );
             Bbr_bddImageTreeDelete( pTree );
-            return -1;
+            free( pValues );
+            return NULL;
         }
         Cudd_Ref( bImage );
+        Cudd_RecursiveDeref( dd, bState );
 
         // intersect with the previous set
-        bImage = Cudd_bddAnd( dd, pTemp = bImage, pCurrent );
-        Cudd_RecursiveDeref( dd, pTemp );
+        bImage = Cudd_bddAnd( dd, bTemp = bImage, bRing );  Cudd_Ref( bImage );
+        Cudd_RecursiveDeref( dd, bTemp );
 
         // find any assignment of the BDD
         RetValue = Cudd_bddPickOneCube( dd, bImage, pValues );
+        assert( RetValue );
+        Cudd_RecursiveDeref( dd, bImage );
 
-        // transform the assignment into the cube in terms of the next state vars
+        // write PIs of counter-example
+        Saig_ManForEachPi( p, pObj, i )
+            if ( pValues[i] == 1 )
+                Aig_InfoSetBit( pCex->pData, nPiOffset + i );
+        nPiOffset -= Saig_ManPiNum(p);
 
-
-        
-        // pCurrent = ...
-
-        // save values of the PI variables
-
-
-        // check if there are any new states
-        if ( Cudd_bddLeq( dd, bNext, bReached ) )
-            break;
-        // check the BDD size
-        nBddSize = Cudd_DagSize(bNext);
-        if ( nBddSize > nBddMax )
+        // check that we get the init state
+        if ( v == 0 )
+        {
+            Saig_ManForEachLo( p, pObj, i )
+                assert( pValues[Saig_ManPiNum(p)+i] == 0 );
             break;
-        // check the result
-        for ( i = 0; i < Saig_ManPoNum(p); i++ )
+        }
+
+        // write state in terms of NS variables
+        bState = (dd)->one; Cudd_Ref( bState );
+        Saig_ManForEachLo( p, pObj, i )
         {
-            if ( !Cudd_bddLeq( dd, bNext, Cudd_Not(pbOutputs[i]) ) )
-            {
-                if ( !fSilent )
-                    printf( "Output %d was asserted in frame %d.  ", i, nIters );
-                Cudd_RecursiveDeref( dd, bReached );
-                bReached = NULL;
-                break;
-            }
+            bVar = Cudd_NotCond( dd->vars[Saig_ManCiNum(p)+i], pValues[Saig_ManPiNum(p)+i] != 1 );
+            bState = Cudd_bddAnd( dd, bTemp = bState, bVar );  Cudd_Ref( bState );
+            Cudd_RecursiveDeref( dd, bTemp ); 
         }
-        if ( i < Saig_ManPoNum(p) )
-            break;
-        // get the new states
-        bCurrent = Cudd_bddAnd( dd, bNext, Cudd_Not(bReached) );        Cudd_Ref( bCurrent );
-*/
+    }
+    // cleanup
+    Bbr_bddImageTreeDelete( pTree );
+    free( pValues );
+    // verify the counter example
+    if ( Vec_PtrSize(vOnionRings) < 1000 )
+    {
+    RetValue = Ssw_SmlRunCounterExample( p, pCex );
+    if ( RetValue == 0 && !fSilent )
+        printf( "Aig_ManVerifyUsingBdds(): Counter-example verification has FAILED.\n" );
+    }
+    if ( fVerbose && !fSilent )
+    {
+    PRT( "Counter-example generation time", clock() - clk );
+    }
+    return pCex;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/bbr/bbrReach.c b/src/aig/bbr/bbrReach.c
index 94d6dbfc..05f7ef55 100644
--- a/src/aig/bbr/bbrReach.c
+++ b/src/aig/bbr/bbrReach.c
@@ -24,6 +24,10 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+extern void * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd, 
+    DdNode ** pbParts, Vec_Ptr_t * vOnionRings, DdNode * bCubeFirst, 
+    int iOutput, int fVerbose, int fSilent );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -212,25 +216,20 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
     DdNode * bCurrent;
     DdNode * bNext = NULL; // Suppress "might be used uninitialized"
     DdNode * bTemp;
-    DdNode ** pbVarsY;
-    Aig_Obj_t * pLatch;
     int i, nIters, nBddSize;
     int nThreshold = 10000;
+    Vec_Ptr_t * vOnionRings;
 
-    // collect the NS variables
-    // set the variable mapping for Cudd_bddVarMap()
-    pbVarsY = ALLOC( DdNode *, dd->size );
-    Saig_ManForEachLo( p, pLatch, i )
-        pbVarsY[i] = dd->vars[ Saig_ManCiNum(p) + i ];
+    // start the onion rings
+    vOnionRings = Vec_PtrAlloc( 1000 );
 
     // start the image computation
     bCubeCs  = Bbr_bddComputeRangeCube( dd, Saig_ManPiNum(p), Saig_ManCiNum(p) );    Cudd_Ref( bCubeCs );
     if ( fPartition )
-        pTree = Bbr_bddImageStart( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), pbVarsY, fVerbose );
+        pTree = Bbr_bddImageStart( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), fVerbose );
     else
-        pTree2 = Bbr_bddImageStart2( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), pbVarsY, fVerbose );
+        pTree2 = Bbr_bddImageStart2( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), fVerbose );
     Cudd_RecursiveDeref( dd, bCubeCs );
-    free( pbVarsY );
     if ( pTree == NULL )
     {
         if ( !fSilent )
@@ -241,6 +240,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
     // perform reachability analisys
     bCurrent = bInitial;   Cudd_Ref( bCurrent );
     bReached = bInitial;   Cudd_Ref( bReached );
+    Vec_PtrPush( vOnionRings, bCurrent );  Cudd_Ref( bCurrent );
     for ( nIters = 1; nIters <= nIterMax; nIters++ )
     { 
         // compute the next states
@@ -275,8 +275,14 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
         {
             if ( !Cudd_bddLeq( dd, bNext, Cudd_Not(pbOutputs[i]) ) )
             {
+                DdNode * bIntersect;
+                bIntersect = Cudd_bddIntersect( dd, bNext, pbOutputs[i] );  Cudd_Ref( bIntersect );
+                assert( p->pSeqModel == NULL );
+                p->pSeqModel = Aig_ManVerifyUsingBddsCountExample( p, dd, pbParts, 
+                    vOnionRings, bIntersect, i, fVerbose, fSilent ); 
+                Cudd_RecursiveDeref( dd, bIntersect );
                 if ( !fSilent )
-                    printf( "Output %d was asserted in frame %d.  ", i, nIters );
+                    printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", i, Vec_PtrSize(vOnionRings) );
                 Cudd_RecursiveDeref( dd, bReached );
                 bReached = NULL;
                 break;
@@ -286,6 +292,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
             break;
         // get the new states
         bCurrent = Cudd_bddAnd( dd, bNext, Cudd_Not(bReached) );        Cudd_Ref( bCurrent );
+        Vec_PtrPush( vOnionRings, bCurrent );  Cudd_Ref( bCurrent );
         // minimize the new states with the reached states
 //        bCurrent = Cudd_bddConstrain( dd, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
 //        Cudd_RecursiveDeref( dd, bTemp );
@@ -309,6 +316,10 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
             fprintf( stdout, "\r" );
     }
     Cudd_RecursiveDeref( dd, bNext );
+    // free the onion rings
+    Vec_PtrForEachEntry( vOnionRings, bTemp, i )
+        Cudd_RecursiveDeref( dd, bTemp );
+    Vec_PtrFree( vOnionRings );
     // undo the image tree
     if ( fPartition )
         Bbr_bddImageTreeDelete( pTree );
@@ -355,11 +366,15 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fParti
 {
     DdManager * dd;
     DdNode ** pbParts, ** pbOutputs;
-    DdNode * bInitial;
+    DdNode * bInitial, * bTemp;
     int RetValue, i, clk = clock();
+    Vec_Ptr_t * vOnionRings;
 
     assert( Saig_ManRegNum(p) > 0 );
 
+    // start the onion rings
+    vOnionRings = Vec_PtrAlloc( 1000 );
+
     // compute the global BDDs of the latches
     dd = Aig_ManComputeGlobalBdds( p, nBddMax, 1, fReorder, fVerbose );    
     if ( dd == NULL )
@@ -386,12 +401,22 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fParti
     {
         if ( !Cudd_bddLeq( dd, bInitial, Cudd_Not(pbOutputs[i]) ) )
         {
+            DdNode * bIntersect;
+            bIntersect = Cudd_bddIntersect( dd, bInitial, pbOutputs[i] );  Cudd_Ref( bIntersect );
+            assert( p->pSeqModel == NULL );
+            p->pSeqModel = Aig_ManVerifyUsingBddsCountExample( p, dd, pbParts, 
+                vOnionRings, bIntersect, i, fVerbose, fSilent ); 
+            Cudd_RecursiveDeref( dd, bIntersect );
             if ( !fSilent )
-                printf( "The miter output %d is proved REACHABLE in the initial state.  ", i );
+                printf( "The miter output %d is proved REACHABLE in the initial state (use \"write_counter\" to dump a witness). ", i );
             RetValue = 0;
             break;
         }
     }
+    // free the onion rings
+    Vec_PtrForEachEntry( vOnionRings, bTemp, i )
+        Cudd_RecursiveDeref( dd, bTemp );
+    Vec_PtrFree( vOnionRings );
     // explore reachable states
     if ( RetValue == -1 )
         RetValue = Aig_ManComputeReachable( dd, p, pbParts, bInitial, pbOutputs, nBddMax, nIterMax, fPartition, fReorder, fVerbose, fSilent ); 
diff --git a/src/aig/bbr/module.make b/src/aig/bbr/module.make
index 07a05869..dce30a21 100644
--- a/src/aig/bbr/module.make
+++ b/src/aig/bbr/module.make
@@ -1,3 +1,4 @@
-SRC +=    src/aig/bbr/bbrImage.c \
+SRC +=    src/aig/bbr/bbrCex.c \
+    src/aig/bbr/bbrImage.c \
     src/aig/bbr/bbrNtbdd.c \
     src/aig/bbr/bbrReach.c
diff --git a/src/aig/dch/dchSat.c b/src/aig/dch/dchSat.c
index e0a446f8..66c7f7b9 100644
--- a/src/aig/dch/dchSat.c
+++ b/src/aig/dch/dchSat.c
@@ -49,6 +49,8 @@ int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
     assert( !Aig_IsComplement(pNew) );
     assert( !Aig_IsComplement(pOld) );
     assert( pNew != pOld );
+
+//    p->nCallsSince++;  // experiment with this!!!
     
     // check if SAT solver needs recycling
     if ( p->pSat == NULL || 
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 9204c2a5..677123d8 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -22,6 +22,7 @@
 #include "ioa.h"
 #include "int.h"
 #include "ssw.h"
+#include "saig.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -172,7 +173,19 @@ clk = clock();
         }
     }
     pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, pParSec->fVeryVerbose, &nIter, TimeLeft );
-    p->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
+    if ( pTemp->pSeqModel )
+    {
+        if ( !Ssw_SmlRunCounterExample( pTemp, pTemp->pSeqModel ) )
+            printf( "Fra_FraigLatchCorrespondence(): 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
+        {
+        FREE( p->pSeqModel );
+        p->pSeqModel = Ssw_SmlDupCounterExample( pTemp->pSeqModel, Aig_ManRegNum(p) );
+        FREE( pTemp->pSeqModel );
+        }
+    }
     if ( pNew == NULL )
     {
         if ( p->pSeqModel )
@@ -188,6 +201,7 @@ PRT( "Time", clock() - clkTotal );
             printf( "SOLUTION: FAIL       " );
 PRT( "Time", clock() - clkTotal );
             }
+            Aig_ManStop( pTemp );
             return RetValue;
         }
         pNew = pTemp;
@@ -372,7 +386,17 @@ PRT( "Time", clock() - clk );
         }
         if ( pSml->fNonConstOut )
         {
-            p->pSeqModel = Fra_SmlGetCounterExample( pSml );
+            pNew->pSeqModel = Fra_SmlGetCounterExample( pSml );
+            // transfer to the original manager
+            if ( Saig_ManPiNum(p) != Saig_ManPiNum(pNew) )
+                printf( "The counter-example is invalid because of phase abstraction.\n" );
+            else
+            {
+            FREE( p->pSeqModel );
+            p->pSeqModel = Ssw_SmlDupCounterExample( pNew->pSeqModel, Aig_ManRegNum(p) );
+            FREE( pNew->pSeqModel );
+            }
+
             Fra_SmlStop( pSml );
             Aig_ManStop( pNew );
             RetValue = 0;
@@ -397,23 +421,38 @@ PRT( "Time", clock() - clkTotal );
 
     // try interplation
 clk = clock();
-    if ( pParSec->fInterpolation && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) == 1 )
+    Aig_ManSetRegNum( pNew, Aig_ManRegNum(pNew) );
+    if ( pParSec->fInterpolation && RetValue == -1 && Aig_ManRegNum(pNew) > 0 )
     {
         Inter_ManParams_t Pars, * pPars = &Pars;
         int Depth;
-        pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
-        pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
 
         Inter_ManSetDefaultParams( pPars );
         pPars->fVerbose = pParSec->fVeryVerbose;
-        RetValue = Inter_ManPerformInterpolation( pNew, pPars, &Depth );
+        if ( Saig_ManPoNum(pNew) == 1 )
+        {
+            RetValue = Inter_ManPerformInterpolation( pNew, pPars, &Depth );
+        }
+        else
+        {
+            Aig_Man_t * pNewOrpos = Said_ManDupOrpos( pNew );
+            RetValue = Inter_ManPerformInterpolation( pNewOrpos, pPars, &Depth );
+            if ( pNewOrpos->pSeqModel )
+            {
+                Ssw_Cex_t * pCex;
+                FREE( pNew->pSeqModel );
+                pCex = pNew->pSeqModel = pNewOrpos->pSeqModel; pNewOrpos->pSeqModel = NULL;
+                pCex->iPo = Ssw_SmlFindOutputCounterExample( pNew, pNew->pSeqModel );
+            }
+            Aig_ManStop( pNewOrpos );
+        }
 
         if ( pParSec->fVerbose )
         {
         if ( RetValue == 1 )
             printf( "Property proved using interpolation.  " );
         else if ( RetValue == 0 )
-            printf( "Property DISPROVED with cex at depth %d using interpolation.  ", Depth );
+            printf( "Property DISPROVED in frame %d using interpolation.  ", Depth );
         else if ( RetValue == -1 )
             printf( "Property UNDECIDED after interpolation.  " );
         else
@@ -431,70 +470,6 @@ PRT( "Time", clock() - clk );
         RetValue = Aig_ManVerifyUsingBdds( pNew, 100000, 1000, 1, 1, 0, pParSec->fSilent );
     }
 
-    // try one-output at a time
-    if ( RetValue == -1 && Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) > 1 )
-    {
-        Aig_Man_t * pNew2;
-        int i, TimeLimit2, RetValue2, fOneUnsolved = 0, iCount, Counter = 0;
-        // count unsolved outputs
-        for ( i = 0; i < Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew); i++ )
-            if ( !Aig_ObjIsConst1( Aig_ObjFanin0(Aig_ManPo(pNew,i)) ) )
-                Counter++;
-        if ( !pParSec->fSilent )
-            printf( "*** The miter has %d outputs (out of %d total) unsolved in the multi-output form.\n", 
-                Counter, Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) );
-        iCount = 0;
-        for ( i = 0; i < Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew); i++ )
-        {
-            int TimeLimitCopy = 0;
-            // get the remaining time for this output
-            if ( pParSec->TimeLimit )
-            {
-                TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
-                TimeLeft = AIG_MAX( TimeLeft, 0.0 );
-                if ( TimeLeft == 0.0 )
-                {
-                    if ( !pParSec->fSilent )
-                        printf( "Runtime limit exceeded.\n" );
-                    TimeOut = 1;
-                    goto finish;
-                }
-                TimeLimit2 = 1 + (int)TimeLeft;
-            }
-            else
-                TimeLimit2 = 0;
-            if ( Aig_ObjIsConst1( Aig_ObjFanin0(Aig_ManPo(pNew,i)) ) )
-                continue;
-            iCount++;
-            if ( !pParSec->fSilent )
-                printf( "*** Running output %d of the miter (number %d out of %d unsolved).\n", i, iCount, Counter );
-            pNew2 = Aig_ManDupOneOutput( pNew, i, 1 );
-            
-            TimeLimitCopy = pParSec->TimeLimit;
-            pParSec->TimeLimit = TimeLimit2;
-            pParSec->fRecursive = 1;
-            RetValue2 = Fra_FraigSec( pNew2, pParSec );
-            pParSec->fRecursive = 0;
-            pParSec->TimeLimit = TimeLimitCopy;
-
-            Aig_ManStop( pNew2 );
-            if ( RetValue2 == 0 )
-                goto finish;
-            if ( RetValue2 == -1 )
-            {
-                fOneUnsolved = 1;
-                if ( pParSec->fStopOnFirstFail )
-                    break;
-            }
-        }
-        if ( fOneUnsolved )
-            RetValue = -1;
-        else
-            RetValue = 1;
-        if ( !pParSec->fSilent )
-            printf( "*** Finished running separate outputs of the miter.\n" );
-    }
-
 finish:
     // report the miter
     if ( RetValue == 1 )
@@ -544,6 +519,17 @@ PRT( "Time", clock() - clkTotal );
             printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName );
         }
     }
+    if ( pNew->pSeqModel )
+    {
+        if ( Saig_ManPiNum(p) != Saig_ManPiNum(pNew) )
+            printf( "The counter-example is invalid because of phase abstraction.\n" );
+        else
+        {
+        FREE( p->pSeqModel );
+        p->pSeqModel = Ssw_SmlDupCounterExample( pNew->pSeqModel, Aig_ManRegNum(p) );
+        FREE( pNew->pSeqModel );
+        }
+    }
     if ( pNew )
         Aig_ManStop( pNew );
     return RetValue;
diff --git a/src/aig/int/int.h b/src/aig/int/int.h
index bc9c1237..e0c4e960 100644
--- a/src/aig/int/int.h
+++ b/src/aig/int/int.h
@@ -70,7 +70,7 @@ struct Inter_ManParams_t_
 
 /*=== intCore.c ==========================================================*/
 extern void       Inter_ManSetDefaultParams( Inter_ManParams_t * p );
-extern int        Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars, int * pDepth );
+extern int        Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars, int * piFrame );
 
 
 #ifdef __cplusplus
diff --git a/src/aig/int/intContain.c b/src/aig/int/intContain.c
index fa52e2b6..dcc80b29 100644
--- a/src/aig/int/intContain.c
+++ b/src/aig/int/intContain.c
@@ -200,19 +200,19 @@ int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter,
     assert( Vec_PtrSize(vMapRegs) == (nSteps + 1) * nRegs );
     // add main constraints to the timeframes
     ppNodes = (Aig_Obj_t **)Vec_PtrArray(vMapRegs);
-    if ( fBackward )
-    {
-        // p -> !p -> ... -> !p
-        Inter_ManAppendCone( pInter, pFrames, ppNodes + 0 * nRegs, 1 );
-        for ( f = 1; f <= nSteps; f++ )
+    if ( !fBackward )
+    { 
+        // forward inductive check: p -> p -> ... -> !p
+        for ( f = 0; f < nSteps; f++ )
             Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 0 );
+        Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 1 );
     }
     else
     {
-        // !p -> p -> ... -> p
-        for ( f = 0; f < nSteps; f++ )
+        // backward inductive check: p -> !p -> ... -> !p
+        Inter_ManAppendCone( pInter, pFrames, ppNodes + 0 * nRegs, 1 );
+        for ( f = 1; f <= nSteps; f++ )
             Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 0 );
-        Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 1 );
     }
     Vec_PtrFree( vMapRegs );
     Aig_ManCleanup( pFrames );
diff --git a/src/aig/int/intCore.c b/src/aig/int/intCore.c
index d959ff07..cc6c5f5b 100644
--- a/src/aig/int/intCore.c
+++ b/src/aig/int/intCore.c
@@ -40,13 +40,13 @@
 
 ***********************************************************************/
 void Inter_ManSetDefaultParams( Inter_ManParams_t * p )
-{
+{ 
     memset( p, 0, sizeof(Inter_ManParams_t) );
     p->nBTLimit     = 10000; // limit on the number of conflicts
     p->nFramesMax   = 40;    // the max number timeframes to unroll
     p->nFramesK     = 1;     // the number of timeframes to use in induction
     p->fRewrite     = 0;     // use additional rewriting to simplify timeframes
-    p->fTransLoop   = 1;     // add transition into the init state under new PI var
+    p->fTransLoop   = 0;     // add transition into the init state under new PI var
     p->fUsePudlak   = 0;     // use Pudluk interpolation procedure
     p->fUseOther    = 0;     // use other undisclosed option
     p->fUseMiniSat  = 0;     // use MiniSat-1.14p instead of internal proof engine
@@ -67,7 +67,7 @@ void Inter_ManSetDefaultParams( Inter_ManParams_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars, int * pDepth )
+int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars, int * piFrame )
 {
     extern int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward );
     Inter_Man_t * p;
@@ -109,7 +109,7 @@ p->timeCnf += clock() - clk;
     }
 
     // derive interpolant
-    *pDepth = -1;
+    *piFrame = -1;
     p->nFrames = 1;
     for ( s = 0; ; s++ )
     {
@@ -183,9 +183,10 @@ p->timeCnf += clock() - clk;
                 if ( i == 0 ) // real counterexample
                 {
                     if ( pPars->fVerbose )
-                        printf( "Found a real counterexample in the first frame.\n" );
+                        printf( "Found a real counterexample in frame %d.\n", p->nFrames );
                     p->timeTotal = clock() - clkTotal;
-                    *pDepth = p->nFrames + 1;
+                    *piFrame = p->nFrames;
+                    pAig->pSeqModel = Inter_ManGetCounterExample( pAig, p->nFrames+1, pPars->fVerbose );
                     Inter_ManStop( p );
                     return 0;
                 }
diff --git a/src/aig/int/intCtrex.c b/src/aig/int/intCtrex.c
new file mode 100644
index 00000000..5e417ce0
--- /dev/null
+++ b/src/aig/int/intCtrex.c
@@ -0,0 +1,157 @@
+/**CFile****************************************************************
+
+  FileName    [intCtrex.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Interpolation engine.]
+
+  Synopsis    [Counter-example generation after disproving the property.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 24, 2008.]
+
+  Revision    [$Id: intCtrex.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "intInt.h"
+#include "ssw.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Unroll the circuit the given number of timeframes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Inter_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
+{
+    Aig_Man_t * pFrames;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    int i, f;
+    assert( Saig_ManRegNum(pAig) > 0 );
+    assert( Saig_ManPoNum(pAig) == 1 );
+    pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
+    // map the constant node
+    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
+    // create variables for register outputs
+    Saig_ManForEachLo( pAig, pObj, i )
+        pObj->pData = Aig_ManConst0( pFrames );
+    // add timeframes
+    for ( f = 0; f < nFrames; f++ )
+    {
+        // create PI nodes for this frame
+        Saig_ManForEachPi( pAig, pObj, i )
+            pObj->pData = Aig_ObjCreatePi( pFrames );
+        // add internal nodes of this frame
+        Aig_ManForEachNode( pAig, pObj, i )
+            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+        if ( f == nFrames - 1 )
+            break;
+        // transfer to register outputs
+        Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
+            pObjLo->pData = pObjLi->pData = Aig_ObjChild0Copy(pObjLi);
+    }
+    // create POs for the output of the last frame
+    pObj = Aig_ManPo( pAig, 0 );
+    Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+    Aig_ManCleanup( pFrames );
+    return pFrames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Run the SAT solver on the unrolled instance.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose )
+{
+    int nConfLimit = 1000000;
+    Ssw_Cex_t * pCtrex = NULL;
+    Aig_Man_t * pFrames;
+    sat_solver * pSat;
+    Cnf_Dat_t * pCnf;
+    int status, clk = clock();
+    Vec_Int_t * vCiIds;
+    // create timeframes
+    assert( Saig_ManPoNum(pAig) == 1 );
+    pFrames = Inter_ManFramesBmc( pAig, nFrames );
+    // derive CNF
+    pCnf = Cnf_Derive( pFrames, 0 );
+    Cnf_DataTranformPolarity( pCnf, 0 );
+    vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames );
+    Aig_ManStop( pFrames );
+    // convert into SAT solver
+    pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+    Cnf_DataFree( pCnf );
+    if ( pSat == NULL )
+    {
+        Vec_IntFree( vCiIds );
+        return NULL;
+    }
+    // simplify the problem
+    status = sat_solver_simplify(pSat);
+    if ( status == 0 )
+    {
+        Vec_IntFree( vCiIds );
+        sat_solver_delete( pSat );
+        return NULL;
+    }
+    // solve the miter
+    status = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
+    // if the problem is SAT, get the counterexample
+    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->iFrame = nFrames - 1;
+        pCtrex->iPo = 0;
+        for ( i = 0; i < Vec_IntSize(vCiIds); i++ )
+            if ( pModel[i] )
+                Aig_InfoSetBit( pCtrex->pData, Saig_ManRegNum(pAig) + i );
+        free( pModel );
+    }
+    // free the sat_solver
+    sat_solver_delete( pSat );
+    Vec_IntFree( vCiIds );
+    // verify counter-example
+    status = Ssw_SmlRunCounterExample( pAig, pCtrex );
+    if ( status == 0 )
+        printf( "Inter_ManGetCounterExample(): Counter-example verification has FAILED.\n" );
+    // report the results
+    if ( fVerbose )
+    {
+        PRT( "Total ctrex generation time", clock() - clk );
+    }
+    return pCtrex;
+
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/int/intInt.h b/src/aig/int/intInt.h
index dbb4301e..c84fef2d 100644
--- a/src/aig/int/intInt.h
+++ b/src/aig/int/intInt.h
@@ -90,6 +90,9 @@ extern int           Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pO
 extern int           Inter_ManCheckEquivalence( Aig_Man_t * pNew, Aig_Man_t * pOld );
 extern int           Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward );
 
+/*=== intCtrex.c ==========================================================*/
+extern void *        Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose );
+
 /*=== intDup.c ==========================================================*/
 extern Aig_Man_t *   Inter_ManStartInitState( int nRegs );
 extern Aig_Man_t *   Inter_ManStartDuplicated( Aig_Man_t * p );
diff --git a/src/aig/int/intM114p.c b/src/aig/int/intM114p.c
index 77776f7e..6818fdce 100644
--- a/src/aig/int/intM114p.c
+++ b/src/aig/int/intM114p.c
@@ -108,7 +108,7 @@ M114p_Solver_t Inter_ManDeriveSatSolverM114p(
     }
     // connector clauses
     Aig_ManForEachPi( pFrames, pObj, i )
-    {
+    { 
         if ( i == Aig_ManRegNum(pAig) )
             break;
 //        Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] );
diff --git a/src/aig/int/module.make b/src/aig/int/module.make
index 0652ab39..cf0f827f 100644
--- a/src/aig/int/module.make
+++ b/src/aig/int/module.make
@@ -1,5 +1,6 @@
 SRC +=    src/aig/int/intContain.c \
     src/aig/int/intCore.c \
+    src/aig/int/intCtrex.c \
     src/aig/int/intDup.c \
     src/aig/int/intFrames.c \
     src/aig/int/intInter.c \
diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c
index 25f7a3ef..7c5a139c 100644
--- a/src/aig/ivy/ivyFraig.c
+++ b/src/aig/ivy/ivyFraig.c
@@ -324,6 +324,11 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars )
         if ( RetValue >= 0 )
             break;
 
+        // catch the situation when ref pattern detects the bug
+        RetValue = Ivy_FraigMiterStatus( pManAig );
+        if ( RetValue >= 0 )
+            break;
+
         // try fraiging followed by mitering
         if ( pParams->fUseFraiging )
         {
@@ -1338,10 +1343,10 @@ int Ivy_FraigCheckOutputSims( Ivy_FraigMan_t * p )
     Ivy_Obj_t * pObj;
     int i;
     // make sure the reference simulation pattern does not detect the bug
-    pObj = Ivy_ManPo( p->pManAig, 0 );
-    assert( Ivy_ObjFanin0(pObj)->fPhase == (unsigned)Ivy_ObjFaninC0(pObj) ); // Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) == 0
+//    pObj = Ivy_ManPo( p->pManAig, 0 );
     Ivy_ManForEachPo( p->pManAig, pObj, i )
     {
+        assert( Ivy_ObjFanin0(pObj)->fPhase == (unsigned)Ivy_ObjFaninC0(pObj) ); // Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) == 0
         // complement simulation info
 //        if ( Ivy_ObjFanin0(pObj)->fPhase ^ Ivy_ObjFaninC0(pObj) ) // Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj))
 //            Ivy_NodeComplementSim( p, Ivy_ObjFanin0(pObj) );
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index fcdb3de3..b09091fb 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -1,5 +1,6 @@
 SRC +=    src/aig/saig/saigBmc.c \
     src/aig/saig/saigCone.c \
+    src/aig/saig/saigDup.c \
     src/aig/saig/saigHaig.c \
     src/aig/saig/saigIoa.c \
     src/aig/saig/saigMiter.c \
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index da194f49..81f0fcf5 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -56,6 +56,8 @@ static inline int          Saig_ObjIsPi( Aig_Man_t * p, Aig_Obj_t * pObj )    {
 static inline int          Saig_ObjIsPo( Aig_Man_t * p, Aig_Obj_t * pObj )    { return Aig_ObjIsPo(pObj) && Aig_ObjPioNum(pObj) < Saig_ManPoNum(p); }
 static inline int          Saig_ObjIsLo( Aig_Man_t * p, Aig_Obj_t * pObj )    { return Aig_ObjIsPi(pObj) && Aig_ObjPioNum(pObj) >= Saig_ManPiNum(p); }
 static inline int          Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj )    { return Aig_ObjIsPo(pObj) && Aig_ObjPioNum(pObj) >= Saig_ManPoNum(p); }
+static inline Aig_Obj_t *  Saig_ObjLoToLi( Aig_Man_t * p, Aig_Obj_t * pObj )  { assert(Saig_ObjIsLo(p, pObj)); return (Aig_Obj_t *)Vec_PtrEntry(p->vPos, Saig_ManPoNum(p)+Aig_ObjPioNum(pObj)-Saig_ManPiNum(p));   }
+static inline Aig_Obj_t *  Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj )  { assert(Saig_ObjIsLi(p, pObj)); return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, Saig_ManPiNum(p)+Aig_ObjPioNum(pObj)-Saig_ManPoNum(p));   }
 
 // iterator over the primary inputs/outputs
 #define Saig_ManForEachPi( p, pObj, i )                                           \
@@ -80,6 +82,8 @@ static inline int          Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj )    {
 extern int               Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame );
 /*=== saigCone.c ==========================================================*/
 extern void              Saig_ManPrintCones( Aig_Man_t * p );
+/*=== saigDup.c ==========================================================*/
+extern Aig_Man_t *       Said_ManDupOrpos( Aig_Man_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 );
 /*=== saigIoa.c ==========================================================*/
diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c
new file mode 100644
index 00000000..1a050741
--- /dev/null
+++ b/src/aig/saig/saigDup.c
@@ -0,0 +1,74 @@
+/**CFile****************************************************************
+
+  FileName    [saigDup.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [Various duplication procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: saigDup.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates while ORing the POs of sequential circuit.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * pAig )
+{
+    Aig_Man_t * pAigNew;
+    Aig_Obj_t * pObj, * pMiter;
+    int i;
+    // start the new manager
+    pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
+    // map the constant node
+    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
+    // create variables for PIs
+    Aig_ManForEachPi( pAig, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pAigNew );
+    // add internal nodes of this frame
+    Aig_ManForEachNode( pAig, pObj, i )
+        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    // create PO of the circuit
+    pMiter = Aig_ManConst0( pAigNew );
+    Saig_ManForEachPo( pAig, pObj, i )
+        pMiter = Aig_Or( pAigNew, pMiter, Aig_ObjChild0Copy(pObj) );
+    Aig_ObjCreatePo( pAigNew, pMiter );
+    // transfer to register outputs
+    Saig_ManForEachLi( pAig, pObj, i )
+        Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
+    Aig_ManCleanup( pAigNew );
+    Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
+    return pAigNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c
index 12d323e2..0f0b1c06 100644
--- a/src/aig/saig/saigPhase.c
+++ b/src/aig/saig/saigPhase.c
@@ -756,7 +756,7 @@ Aig_Man_t * Saig_ManPerformAbstraction( Saig_Tsim_t * pTsi, int nFrames, int fVe
 //Aig_ManPrintStats( pFrames );
     Aig_ManSeqCleanup( pFrames );
 //Aig_ManPrintStats( pFrames );
-    Aig_ManPiCleanup( pFrames );
+//    Aig_ManPiCleanup( pFrames );
 //Aig_ManPrintStats( pFrames );
     free( pObjMap );
     return pFrames;
diff --git a/src/aig/ssw/module.make b/src/aig/ssw/module.make
index daf69370..c5668d6d 100644
--- a/src/aig/ssw/module.make
+++ b/src/aig/ssw/module.make
@@ -2,6 +2,7 @@ SRC +=    src/aig/ssw/sswAig.c \
     src/aig/ssw/sswClass.c \
     src/aig/ssw/sswCnf.c \
     src/aig/ssw/sswCore.c \
+    src/aig/ssw/sswLcorr.c \
     src/aig/ssw/sswMan.c \
     src/aig/ssw/sswPart.c \
     src/aig/ssw/sswPairs.c \
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index 91c2165a..2917f6d4 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -51,6 +51,9 @@ struct Ssw_Pars_t_
     int              nMinDomSize;   // min clock domain considered for optimization
     int              fPolarFlip;    // uses polarity adjustment
     int              fLatchCorr;    // perform register correspondence
+    int              fLatchCorrOpt; // perform register correspondence (optimized)
+    int              nSatVarMax;    // max number of SAT vars before recycling SAT solver (optimized latch corr only)
+    int              nCallsRecycle; // calls to perform before recycling SAT solver (optimized latch corr only)
     int              fSkipCheck;    // does not run equivalence check for unaffected cones
     int              fVerbose;      // verbose stats
     // internal parameters
@@ -86,6 +89,12 @@ extern Aig_Man_t *   Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t
 extern int           Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars );
 extern int           Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars );
 extern int           Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars );
+/*=== sswSim.c ===================================================*/
+extern Ssw_Cex_t *   Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames );
+extern void          Ssw_SmlFreeCounterExample( Ssw_Cex_t * pCex );
+extern int           Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p );
+extern int           Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p );
+extern Ssw_Cex_t *   Ssw_SmlDupCounterExample( Ssw_Cex_t * p, int nRegsNew );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c
index e186946a..81e8de8b 100644
--- a/src/aig/ssw/sswClass.c
+++ b/src/aig/ssw/sswClass.c
@@ -294,6 +294,28 @@ Aig_Obj_t ** Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSiz
 
 /**Function*************************************************************
 
+  Synopsis    [Stop representation of equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ClassesCollectClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, Vec_Ptr_t * vClass )
+{
+    int i;
+    Vec_PtrClear( vClass );
+    if ( p->pId2Class[pRepr->Id] == NULL )
+        return;
+    assert( p->pClassSizes[pRepr->Id] > 1 );
+    for ( i = 1; i < p->pClassSizes[pRepr->Id]; i++ )
+        Vec_PtrPush( vClass, p->pId2Class[pRepr->Id][i] );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Checks candidate equivalence classes.]
 
   Description []
diff --git a/src/aig/ssw/sswCnf.c b/src/aig/ssw/sswCnf.c
index b047a312..e4b8f9f6 100644
--- a/src/aig/ssw/sswCnf.c
+++ b/src/aig/ssw/sswCnf.c
@@ -264,6 +264,12 @@ void Ssw_ObjAddToFrontier( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontie
     assert( Ssw_ObjSatNum(p,pObj) == 0 );
     if ( Aig_ObjIsConst1(pObj) )
         return;
+    if ( p->pPars->fLatchCorrOpt )
+    {
+        Vec_PtrPush( p->vUsedNodes, pObj );
+        if ( Aig_ObjIsPi(pObj) )
+            Vec_PtrPush( p->vUsedPis, pObj );
+    }
     Ssw_ObjSetSatNum( p, pObj, p->nSatVars++ );
     sat_solver_setnvars( p->pSat, 100 * (1 + p->nSatVars / 100) );
     if ( Aig_ObjIsNode(pObj) )
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index 8e3ab01a..6a3e9264 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -52,6 +52,11 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
     p->fPolarFlip     =     0;  // uses polarity adjustment
     p->fLatchCorr     =     0;  // performs register correspondence
     p->fVerbose       =     0;  // verbose stats
+    // latch correspondence
+    p->fLatchCorrOpt  =     0;  // performs optimized register correspondence
+    p->nSatVarMax     =  5000;  // the max number of SAT variables
+    p->nCallsRecycle  =   100;  // calls to perform before recycling SAT solver
+    // return values
     p->nIters         =     0;  // the number of iterations performed
 }
 
@@ -81,8 +86,11 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
         printf( "Before BMC: " );
         Ssw_ClassesPrint( p->ppClasses, 0 );
     }
-    Ssw_ManSweepBmc( p );
-    Ssw_ManCleanup( p );
+    if ( !p->pPars->fLatchCorr )
+    { 
+        Ssw_ManSweepBmc( p );
+        Ssw_ManCleanup( p );
+    }
     if ( p->pPars->fVerbose )
     {
         printf( "After  BMC: " );
@@ -92,7 +100,10 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
     for ( nIter = 0; ; nIter++ )
     {
 clk = clock();
-        RetValue = Ssw_ManSweep( p );
+        if ( p->pPars->fLatchCorrOpt )
+            RetValue = Ssw_ManSweepLatch( p );
+        else
+            RetValue = Ssw_ManSweep( p );
         if ( p->pPars->fVerbose )
         {
             printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. F = %5d. ", 
@@ -134,6 +145,7 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
     Ssw_Pars_t Pars;
     Aig_Man_t * pAigNew;
     Ssw_Man_t * p;
+    assert( Aig_ManRegNum(pAig) > 0 );
     // reset random numbers
     Aig_ManRandom( 1 );
     // if parameters are not given, create them
@@ -148,14 +160,18 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
         return Aig_ManDupOrdered(pAig);
     }
     // check and update parameters
-    assert( Aig_ManRegNum(pAig) > 0 );
-    assert( pPars->nFramesK > 0 );
-    if ( pPars->nFramesK > 1 )
-        pPars->fSkipCheck = 0;
-    // perform partitioning
-    if ( (pPars->nPartSize > 0 && pPars->nPartSize < Aig_ManRegNum(pAig))
-         || (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0)  )
-        return Ssw_SignalCorrespondencePart( pAig, pPars );
+    if ( pPars->fLatchCorrOpt )
+        pPars->fLatchCorr = 1;
+    else
+    {
+        assert( pPars->nFramesK > 0 );
+        if ( pPars->nFramesK > 1 )
+            pPars->fSkipCheck = 0;
+        // perform partitioning
+        if ( (pPars->nPartSize > 0 && pPars->nPartSize < Aig_ManRegNum(pAig))
+             || (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0)  )
+            return Ssw_SignalCorrespondencePart( pAig, pPars );
+    }
     // start the induction manager
     p = Ssw_ManCreate( pAig, pPars );
     // compute candidate equivalence classes
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index 6824e239..5b4377c7 100644
--- a/src/aig/ssw/sswInt.h
+++ b/src/aig/ssw/sswInt.h
@@ -67,6 +67,11 @@ struct Ssw_Man_t_
     Vec_Ptr_t *      vFanins;        // fanins of the CNF node
     Vec_Ptr_t *      vSimRoots;      // the roots of cand const 1 nodes to simulate
     Vec_Ptr_t *      vSimClasses;    // the roots of cand equiv classes to simulate
+    // SAT solving (latch corr only)
+    int              nCallsSince;    // the number of calls since last recycling
+    int              nRecycles;      // the number of time SAT solver was recycled
+    Vec_Ptr_t *      vUsedNodes;     // the nodes with SAT variables
+    Vec_Ptr_t *      vUsedPis;       // the PIs with SAT variables
     // sequential simulator
     Ssw_Sml_t *      pSml;
     // counter example storage
@@ -145,6 +150,7 @@ extern int           Ssw_ClassesCand1Num( Ssw_Cla_t * p );
 extern int           Ssw_ClassesClassNum( Ssw_Cla_t * p );
 extern int           Ssw_ClassesLitNum( Ssw_Cla_t * p );
 extern Aig_Obj_t **  Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize );
+extern void          Ssw_ClassesCollectClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, Vec_Ptr_t * vClass );
 extern void          Ssw_ClassesCheck( Ssw_Cla_t * p );
 extern void          Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose );
 extern void          Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj );
@@ -161,6 +167,8 @@ extern int           Ssw_NodesAreEqualCex( void * p, Aig_Obj_t * pObj0, Aig_Obj_
 extern void          Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj );
 /*=== sswCore.c ===================================================*/
 extern Aig_Man_t *   Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p );
+/*=== sswLcorr.c ==========================================================*/
+extern int           Ssw_ManSweepLatch( Ssw_Man_t * p );
 /*=== sswMan.c ===================================================*/
 extern Ssw_Man_t *   Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
 extern void          Ssw_ManCleanup( Ssw_Man_t * p );
diff --git a/src/aig/ssw/sswLcorr.c b/src/aig/ssw/sswLcorr.c
new file mode 100644
index 00000000..dcc4f245
--- /dev/null
+++ b/src/aig/ssw/sswLcorr.c
@@ -0,0 +1,286 @@
+/**CFile****************************************************************
+
+  FileName    [sswLcorr.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Inductive prover with constraints.]
+
+  Synopsis    [Latch correspondence.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 1, 2008.]
+
+  Revision    [$Id: sswLcorr.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+#include "bar.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Recycles the SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManSatSolverRecycle( Ssw_Man_t * p )
+{
+    int Lit;
+    if ( p->pSat )
+    {
+        Aig_Obj_t * pObj;
+        int i;
+        Vec_PtrForEachEntry( p->vUsedNodes, pObj, i )
+            Ssw_ObjSetSatNum( p, pObj, 0 );
+        Vec_PtrClear( p->vUsedNodes );
+        Vec_PtrClear( p->vUsedPis );
+//        memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAigTotal) );
+        sat_solver_delete( p->pSat );
+    }
+    p->pSat = sat_solver_new();
+    sat_solver_setnvars( p->pSat, 1000 );
+    // var 0 is not used
+    // var 1 is reserved for const1 node - add the clause
+    p->nSatVars = 1;
+//    p->nSatVars = 0;
+    Lit = toLit( p->nSatVars );
+    if ( p->pPars->fPolarFlip )
+        Lit = lit_neg( Lit );
+    sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
+    Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pFrames), p->nSatVars++ );
+
+    p->nRecycles++;
+    p->nCallsSince = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Copy pattern from the solver into the internal storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_SmlSavePatternLatch( Ssw_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
+    Aig_ManForEachPi( p->pAig, pObj, i )
+        if ( Ssw_ManOriginalPiValue( p, pObj, 0 ) )
+            Aig_InfoSetBit( p->pPatWords, i );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Copy pattern from the solver into the internal storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_SmlSavePatternLatchPhase( Ssw_Man_t * p, int f )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
+    Aig_ManForEachPi( p->pAig, pObj, i )
+        if ( Aig_ObjPhaseReal( Ssw_ObjFraig(p, pObj, f) ) )
+            Aig_InfoSetBit( p->pPatWords, i );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Builds fraiged logic cone of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManBuildCone_rec( Ssw_Man_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pObjNew;
+    assert( !Aig_IsComplement(pObj) );
+    if ( Ssw_ObjFraig( p, pObj, 0 ) )
+        return;
+    assert( Aig_ObjIsNode(pObj) );
+    Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObj) );
+    Ssw_ManBuildCone_rec( p, Aig_ObjFanin1(pObj) );
+    pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, 0), Ssw_ObjChild1Fra(p, pObj, 0) );
+    Ssw_ObjSetFraig( p, pObj, 0, pObjNew );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recycles the SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManSweepLatchOne( Ssw_Man_t * p, Aig_Obj_t * pObjRepr, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pObjFraig, * pObjFraig2, * pObjReprFraig, * pObjLi;
+    int RetValue;
+    assert( Aig_ObjIsPi(pObj) );
+    assert( Aig_ObjIsPi(pObjRepr) || Aig_ObjIsConst1(pObjRepr) );
+    // get the fraiged node
+    pObjLi = Saig_ObjLoToLi( p->pAig, pObj ); 
+    Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObjLi) );
+    pObjFraig = Ssw_ObjChild0Fra( p, pObjLi, 0 );
+    // get the fraiged representative
+    if ( Aig_ObjIsPi(pObjRepr) )
+    {
+        pObjLi = Saig_ObjLoToLi( p->pAig, pObjRepr ); 
+        Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObjLi) );
+        pObjReprFraig = Ssw_ObjChild0Fra( p, pObjLi, 0 );
+    }
+    else 
+        pObjReprFraig = Ssw_ObjFraig( p, pObjRepr, 0 );
+    // if the fraiged nodes are the same, return
+    if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
+        return;
+    p->nCallsSince++;
+    // check equivalence of the two nodes
+    if ( (pObj->fPhase == pObjRepr->fPhase) != (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) )
+    {
+        p->nStrangers++;
+        Ssw_SmlSavePatternLatchPhase( p, 0 );
+    }
+    else
+    { 
+        RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
+        if ( RetValue == 1 )  // proved equivalent
+        {
+            pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
+            Ssw_ObjSetFraig( p, pObj, 0, pObjFraig2 );
+            return;
+        }
+        else if ( RetValue == -1 ) // timed out
+        {
+            Ssw_ClassesRemoveNode( p->ppClasses, pObj );
+            p->fRefined = 1;
+            return;
+        }
+        else // disproved the equivalence
+        {       
+            Ssw_SmlSavePatternLatch( p );
+        }
+    }
+    if ( p->pPars->nConstrs == 0 )
+        Ssw_ManResimulateCexTotalSim( p, pObj, pObjRepr, 0 );
+    else
+        Ssw_ManResimulateCexTotal( p, pObj, pObjRepr, 0 );
+    assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
+    p->fRefined = 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one iteration of sweeping latches.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_ManSweepLatch( Ssw_Man_t * p )
+{
+    Bar_Progress_t * pProgress = NULL;
+    Vec_Ptr_t * vClass;
+    Aig_Obj_t * pObj, * pRepr, * pTemp;
+    int i, k;
+
+    // start the timeframe
+    p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) );
+    // map constants and PIs
+    Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), 0, Aig_ManConst1(p->pFrames) );
+    Saig_ManForEachPi( p->pAig, pObj, i )
+        Ssw_ObjSetFraig( p, pObj, 0, Aig_ObjCreatePi(p->pFrames) );
+
+    // implement equivalence classes
+    Saig_ManForEachLo( p->pAig, pObj, i )
+    {
+        pRepr = Aig_ObjRepr( p->pAig, pObj );
+        if ( pRepr == NULL )
+            pTemp = Aig_ObjCreatePi(p->pFrames);
+        else
+            pTemp = Aig_NotCond( Ssw_ObjFraig(p, pRepr, 0), pRepr->fPhase ^ pObj->fPhase );
+        Ssw_ObjSetFraig( p, pObj, 0, pTemp );
+    }
+
+    // go through the registers
+    if ( p->pPars->fVerbose )
+        pProgress = Bar_ProgressStart( stdout, Aig_ManRegNum(p->pAig) );
+    vClass = Vec_PtrAlloc( 100 );
+    p->fRefined = 0;
+    Saig_ManForEachLo( p->pAig, pObj, i )
+    {
+        if ( p->pPars->fVerbose )
+            Bar_ProgressUpdate( pProgress, i, NULL );
+        // consider the case of constant candidate
+        if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
+            Ssw_ManSweepLatchOne( p, Aig_ManConst1(p->pAig), pObj );
+        else
+        {
+            // consider the case of equivalence class
+            Ssw_ClassesCollectClass( p->ppClasses, pObj, vClass );
+            if ( Vec_PtrSize(vClass) == 0 )
+                continue;
+            // try to prove equivalences in this class
+            Vec_PtrForEachEntry( vClass, pTemp, k )
+                if ( Aig_ObjRepr(p->pAig, pTemp) == pObj )
+                    Ssw_ManSweepLatchOne( p, pObj, pTemp );
+        }
+        // attempt recycling the SAT solver
+        if ( p->pPars->nSatVarMax && 
+             p->nSatVars > p->pPars->nSatVarMax &&
+             p->nCallsSince > p->pPars->nCallsRecycle )
+             Ssw_ManSatSolverRecycle( p );
+    }
+    Vec_PtrFree( vClass );
+    p->nSatFailsTotal += p->nSatFailsReal;
+    if ( p->pPars->fVerbose )
+        Bar_ProgressStop( pProgress );
+
+    // cleanup
+    Ssw_ClassesCheck( p->ppClasses );
+    return p->fRefined;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c
index 559f7b6c..33c716ce 100644
--- a/src/aig/ssw/sswMan.c
+++ b/src/aig/ssw/sswMan.c
@@ -58,6 +58,9 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
     p->vFanins       = Vec_PtrAlloc( 100 );
     p->vSimRoots     = Vec_PtrAlloc( 1000 );
     p->vSimClasses   = Vec_PtrAlloc( 1000 );
+    // SAT solving (latch corr only)
+    p->vUsedNodes    = Vec_PtrAlloc( 1000 );
+    p->vUsedPis      = Vec_PtrAlloc( 1000 );
     // allocate storage for sim pattern
     p->nPatWords     = Aig_BitWordNum( Saig_ManPiNum(pAig) * p->nFrames + Saig_ManRegNum(pAig) );
     p->pPatWords     = ALLOC( unsigned, p->nPatWords ); 
@@ -178,6 +181,8 @@ void Ssw_ManStop( Ssw_Man_t * p )
     Vec_PtrFree( p->vFanins );
     Vec_PtrFree( p->vSimRoots );
     Vec_PtrFree( p->vSimClasses );
+    Vec_PtrFree( p->vUsedNodes );
+    Vec_PtrFree( p->vUsedPis );
     FREE( p->pNodeToFraig );
     FREE( p->pSatVars );
     FREE( p->pPatWords );
@@ -209,6 +214,9 @@ void Ssw_ManStartSolver( Ssw_Man_t * p )
         Lit = lit_neg( Lit );
     sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
     Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pAig), p->nSatVars++ );
+
+    Vec_PtrClear( p->vUsedNodes );
+    Vec_PtrClear( p->vUsedPis );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c
index 64175b40..769e923c 100644
--- a/src/aig/ssw/sswSim.c
+++ b/src/aig/ssw/sswSim.c
@@ -1021,6 +1021,49 @@ int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Resimulates the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Ssw_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_SmlAssignConst( 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_SmlAssignConst( 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_SmlNodeIsZero( pSml, Aig_ManPo(pAig, k) ) )
+        {
+            iOut = k;
+            break;
+        }
+    Ssw_SmlStop( pSml );
+    return iOut;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Creates sequential counter-example from the simulation info.]
 
   Description []
@@ -1182,6 +1225,30 @@ Ssw_Cex_t * Ssw_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut )
 
 /**Function*************************************************************
 
+  Synopsis    [Make the trivial counter-example for the trivially asserted output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ssw_Cex_t * Ssw_SmlDupCounterExample( Ssw_Cex_t * p, int nRegsNew )
+{
+    Ssw_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;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Resimulates the counter-example.]
 
   Description []
diff --git a/src/aig/ssw/sswSimSat.c b/src/aig/ssw/sswSimSat.c
index 3fa39612..715750ca 100644
--- a/src/aig/ssw/sswSimSat.c
+++ b/src/aig/ssw/sswSimSat.c
@@ -113,6 +113,14 @@ int Ssw_ManOriginalPiValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
     {
         if ( Aig_Regular(pObjFraig)->fPhase )  Value ^= 1;
     }
+/*
+    if ( nVarNum==0 )
+        printf( "x" );
+    else if ( Value == 0 )
+        printf( "0" );
+    else
+        printf( "1" );
+*/
     return Value;
 }
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 26d72934..7247f8ed 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -3131,7 +3131,7 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: fx [-S num] [-D num] [-N num] [-sdzcvh]\n");
+    fprintf( pErr, "usage: fx [-SDN num] [-sdzcvh]\n");
     fprintf( pErr, "\t         performs unate fast extract on the current network\n");
     fprintf( pErr, "\t-S num : max number of single-cube divisors to consider [default = %d]\n", p->nSingleMax );  
     fprintf( pErr, "\t-D num : max number of double-cube divisors to consider [default = %d]\n", p->nPairsMax );  
@@ -13876,19 +13876,24 @@ int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     int nFramesP;
     int nConfMax;
+    int nVarsMax;
+    int fNewAlgor;
     int fVerbose;
     extern Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nFramesP   = 0;
+    nFramesP   =     0;
     nConfMax   = 10000;
-    fVerbose   = 0;
+    nVarsMax   =  5000;
+    fNewAlgor  =     0;
+    fVerbose   =     1;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "PCvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PCSnvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -13914,6 +13919,20 @@ int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nConfMax < 0 ) 
                 goto usage;
             break;
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-S\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nVarsMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nVarsMax < 0 ) 
+                goto usage;
+            break;
+        case 'n':
+            fNewAlgor ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -13943,7 +13962,10 @@ int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkDarLcorr( pNtk, nFramesP, nConfMax, fVerbose );
+    if ( fNewAlgor )
+        pNtkRes = Abc_NtkDarLcorrNew( pNtk, nVarsMax, nConfMax, fVerbose );
+    else
+        pNtkRes = Abc_NtkDarLcorr( pNtk, nFramesP, nConfMax, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Sequential sweeping has failed.\n" );
@@ -13954,10 +13976,12 @@ int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: lcorr [-P num] [-C num] [-vh]\n" );
+    fprintf( pErr, "usage: lcorr [-PCS num] [-nvh]\n" );
     fprintf( pErr, "\t         computes latch correspondence using 1-step induction\n" );
     fprintf( pErr, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP );
     fprintf( pErr, "\t-C num : max conflict number when proving latch equivalence [default = %d]\n", nConfMax );
+    fprintf( pErr, "\t-S num : the max number of SAT variables [default = %d]\n", nVarsMax );
+    fprintf( pErr, "\t-n     : toggle new algorithm [default = %s]\n", fNewAlgor? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index b84c5191..ac5ee882 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1316,6 +1316,50 @@ Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int f
 
 /**Function*************************************************************
 
+  Synopsis    [Computes latch correspondence.]
+
+  Description [] 
+               
+  SideEffects []
+
+  SeeAlso     []
+ 
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, int fVerbose )
+{
+    Ssw_Pars_t Pars, * pPars = &Pars;
+    Aig_Man_t * pMan, * pTemp;
+    Abc_Ntk_t * pNtkAig = NULL;
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
+    if ( pMan == NULL )
+        return NULL;
+    Ssw_ManSetDefaultParams( pPars );
+    pPars->fLatchCorrOpt = 1;
+//    pPars->nFramesAddSim = 0;
+    pPars->nBTLimit      = nConfMax;
+    pPars->nSatVarMax    = nVarsMax;
+    pPars->fVerbose      = fVerbose;
+    pMan = Ssw_SignalCorrespondence( pTemp = pMan, pPars );
+    Aig_ManStop( pTemp );
+    if ( pMan )
+    {
+        if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
+            pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
+        else
+        {
+            Abc_Obj_t * pObj;
+            int i;
+            pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+            Abc_NtkForEachLatch( pNtkAig, pObj, i )
+                Abc_LatchSetInit0( pObj );
+        }
+        Aig_ManStop( pMan );
+    }
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Gives the current ABC network to AIG manager for processing.]
 
   Description []
@@ -1342,6 +1386,8 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, in
     {
         int iFrame;
         RetValue = Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &iFrame );
+        FREE( pNtk->pModel );
+        FREE( pNtk->pSeqModel );
         pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
         if ( RetValue == 1 )
             printf( "No output was asserted in %d frames. ", iFrame );
@@ -1350,17 +1396,19 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, in
         else // if ( RetValue == 0 )
         {
             Fra_Cex_t * pCex = pNtk->pSeqModel;
-            printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump the trace). ", pCex->iPo, pCex->iFrame );
+            printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
         }
     }
     else
     {
         Fra_BmcPerformSimple( pMan, nFrames, nBTLimit, fRewrite, fVerbose );
+        FREE( pNtk->pModel );
+        FREE( pNtk->pSeqModel );
         pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
         if ( pNtk->pSeqModel )
         {
             Fra_Cex_t * pCex = pNtk->pSeqModel;
-            printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump the trace). ", pCex->iPo, pCex->iFrame );
+            printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
             RetValue = 0;
         }
         else
@@ -1388,7 +1436,7 @@ PRT( "Time", clock() - clk );
 int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars )
 {
     Aig_Man_t * pMan;
-    int RetValue, Depth, clk = clock();
+    int RetValue, iFrame, clk = clock();
     // derive the AIG manager
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
@@ -1397,11 +1445,16 @@ int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars )
         return -1;
     }
     assert( pMan->nRegs > 0 );
-    RetValue = Inter_ManPerformInterpolation( pMan, pPars, &Depth );
+    RetValue = Inter_ManPerformInterpolation( pMan, pPars, &iFrame );
     if ( RetValue == 1 )
         printf( "Property proved.  " );
     else if ( RetValue == 0 )
-        printf( "Property DISPROVED with counter-example at depth %d.  ", Depth );
+    {
+        printf( "Property DISPROVED in frame %d (use \"write_counter\" to dump a witness).  ", iFrame );
+        FREE( pNtk->pModel );
+        FREE( pNtk->pSeqModel );
+        pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
+    }
     else if ( RetValue == -1 )
         printf( "Property UNDECIDED.  " );
     else
@@ -1440,7 +1493,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
         Prove_ParamsSetDefault( pParams );
         RetValue = Abc_NtkIvyProve( &pNtkComb, pParams );
         // transfer model if given
-        pNtk->pModel = pNtkComb->pModel; pNtkComb->pModel = NULL;
+//        pNtk->pModel = pNtkComb->pModel; pNtkComb->pModel = NULL;
         Abc_NtkDelete( pNtkComb );
         // return the result, if solved
         if ( RetValue == 1 )
@@ -1485,11 +1538,15 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
     else
     {
         RetValue = Fra_FraigSec( pMan, pSecPar );
+        FREE( pNtk->pModel );
+        FREE( pNtk->pSeqModel );
         pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
         if ( pNtk->pSeqModel )
         {
             Fra_Cex_t * pCex = pNtk->pSeqModel;
-            printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump the trace).\n", pCex->iPo, pCex->iFrame );
+            printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness).\n", pCex->iPo, pCex->iFrame );
+            if ( !Ssw_SmlRunCounterExample( pMan, pNtk->pSeqModel ) )
+                printf( "Abc_NtkDarProve(): Counter-example verification has FAILED.\n" );
         }
     }
     Aig_ManStop( pMan );
@@ -1842,6 +1899,8 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int fVerbose )
         if ( pCex )
             printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ", 
                 nFrames, nWords, pCex->iPo, pCex->iFrame );
+        FREE( pNtk->pModel );
+        FREE( pNtk->pSeqModel );
         pNtk->pSeqModel = pCex;
         RetValue = 1;
     }
@@ -2341,6 +2400,9 @@ void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartitio
     if ( pMan == NULL )
         return;
     Aig_ManVerifyUsingBdds( pMan, nBddMax, nIterMax, fPartition, fReorder, fVerbose, 0 );
+    FREE( pNtk->pModel );
+    FREE( pNtk->pSeqModel );
+    pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
     Aig_ManStop( pMan );
 }
 
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 371adfc9..6d7948ab 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -1734,7 +1734,7 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
         fclose( pFile );
     }
     else
-    {
+    { 
         Fra_Cex_t * pCex = pNtk->pSeqModel;
         Abc_Obj_t * pObj;
         FILE * pFile;
diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/src/map/pcm/module.make
diff --git a/src/map/ply/module.make b/src/map/ply/module.make
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/src/map/ply/module.make
diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c
index 82f4e034..967639ae 100644
--- a/src/sat/bsat/satInterA.c
+++ b/src/sat/bsat/satInterA.c
@@ -544,7 +544,13 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
     int i, v, Var, PrevId;
     int fPrint = 0;
     int clk = clock();
-
+/*
+    if ( pFinal->Id == 5187 )
+    {
+        int x = 0;
+        Inta_ManPrintClause( p, pConflict );
+    }
+*/
     // collect resolvent literals
     if ( p->fProofVerif )
     {
@@ -573,13 +579,23 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
         if ( !p->pSeens[Var] )
             continue;
         p->pSeens[Var] = 0;
-
+/*
+        if ( pFinal->Id == 5187 )
+        {
+            printf( "pivot = %d  ", p->pTrail[i] );
+        }
+*/
         // skip literals of the resulting clause
         pReason = p->pReasons[Var];
         if ( pReason == NULL )
             continue;
         assert( p->pTrail[i] == pReason->pLits[0] );
-
+/*
+        if ( pFinal->Id == 5187 )
+        {
+            Inta_ManPrintClause( p, pReason );
+        }
+*/
         // add the variables to seen
         for ( v = 1; v < (int)pReason->nLits; v++ )
             p->pSeens[lit_var(pReason->pLits[v])] = 1;
@@ -657,6 +673,20 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
         int v1, v2; 
         if ( fPrint )
             Inta_ManPrintResolvent( p->pResLits, p->nResLits );
+/*
+        if ( pFinal->Id == 5187 )
+        {
+            Inta_ManPrintResolvent( p->pResLits, p->nResLits );
+            Inta_ManPrintClause( p, pFinal );
+        }
+*/
+/*
+        if ( p->nResLits != pFinal->nLits )
+        {
+            printf( "Recording clause %d: The resolvent is wrong (nRetLits = %d, pFinal->nLits = %d).\n", 
+                pFinal->Id, p->nResLits, pFinal->nLits );
+        }
+*/
         for ( v1 = 0; v1 < p->nResLits; v1++ )
         {
             for ( v2 = 0; v2 < (int)pFinal->nLits; v2++ )