Version abc71208

12 files changed, 1207 insertions, 129 deletions

diff --git a/src/aig/aig/aigHaig.c b/src/aig/aig/aigHaig.c
index 273dc723..eaf9fd05 100644
--- a/src/aig/aig/aigHaig.c
+++ b/src/aig/aig/aigHaig.c
@@ -192,7 +192,7 @@ clk = clock();
 //    pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
 //Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
     // create the SAT solver to be used for this problem
-    pSat = Cnf_DataWriteIntoSolver( pCnf );
+    pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
 
     printf( "HAIG regs = %d. HAIG nodes = %d. Outputs = %d.\n", 
         Aig_ManRegNum(pHaig), Aig_ManNodeNum(pHaig), Aig_ManPoNum(pHaig) );
diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
index 5c7a594e..77c87f3f 100644
--- a/src/aig/cnf/cnf.h
+++ b/src/aig/cnf/cnf.h
@@ -134,7 +134,7 @@ extern void            Cnf_ManStop( Cnf_Man_t * p );
 extern Vec_Int_t *     Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
 extern void            Cnf_DataFree( Cnf_Dat_t * p );
 extern void            Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable );
-void *                 Cnf_DataWriteIntoSolver( Cnf_Dat_t * p );
+void *                 Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit );
 /*=== cnfMap.c ========================================================*/
 extern void            Cnf_DeriveMapping( Cnf_Man_t * p );
 extern int             Cnf_ManMapForCnf( Cnf_Man_t * p );
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c
index 1edc012a..4ac06b48 100644
--- a/src/aig/cnf/cnfMan.c
+++ b/src/aig/cnf/cnfMan.c
@@ -172,12 +172,13 @@ void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable )
   SeeAlso     []
 
 ***********************************************************************/
-void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p )
+void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit )
 {
     sat_solver * pSat;
-    int i, status;
+    int i, f, status;
+    assert( nFrames > 0 );
     pSat = sat_solver_new();
-    sat_solver_setnvars( pSat, p->nVars );
+    sat_solver_setnvars( pSat, p->nVars * nFrames );
     for ( i = 0; i < p->nClauses; i++ )
     {
         if ( !sat_solver_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) )
@@ -186,6 +187,63 @@ void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p )
             return NULL;
         }
     }
+    if ( nFrames > 1 )
+    {
+        Aig_Obj_t * pObjLo, * pObjLi;
+        int nLitsAll, * pLits, Lits[2];
+        nLitsAll = 2 * p->nVars;
+        pLits = p->pClauses[0];
+        for ( f = 1; f < nFrames; f++ )
+        {
+            // add equality of register inputs/outputs for different timeframes
+            Aig_ManForEachLiLoSeq( p->pMan, pObjLi, pObjLo, i )
+            {
+                Lits[0] = (f-1)*nLitsAll + toLitCond( p->pVarNums[pObjLi->Id], 0 );
+                Lits[1] =  f   *nLitsAll + toLitCond( p->pVarNums[pObjLo->Id], 1 );
+                if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
+                {
+                    sat_solver_delete( pSat );
+                    return NULL;
+                }
+                Lits[0]++;
+                Lits[1]--;
+                if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
+                {
+                    sat_solver_delete( pSat );
+                    return NULL;
+                }
+            }
+            // add clauses for the next timeframe
+            for ( i = 0; i < p->nLiterals; i++ )
+                pLits[i] += nLitsAll;
+            for ( i = 0; i < p->nClauses; i++ )
+            {
+                if ( !sat_solver_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) )
+                {
+                    sat_solver_delete( pSat );
+                    return NULL;
+                }
+            }
+        }
+        // return literals to their original state
+        nLitsAll = (f-1) * nLitsAll;
+        for ( i = 0; i < p->nLiterals; i++ )
+            pLits[i] -= nLitsAll;
+    }
+    if ( fInit )
+    {
+        Aig_Obj_t * pObjLo;
+        int Lits[1];
+        Aig_ManForEachLoSeq( p->pMan, pObjLo, i )
+        {
+            Lits[0] = toLitCond( p->pVarNums[pObjLo->Id], 1 );
+            if ( !sat_solver_addclause( pSat, Lits, Lits + 1 ) )
+            {
+                sat_solver_delete( pSat );
+                return NULL;
+            }
+        }
+    }
     status = sat_solver_simplify(pSat);
     if ( status == 0 )
     {
diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c
index a46069e6..8c23d859 100644
--- a/src/aig/cnf/cnfWrite.c
+++ b/src/aig/cnf/cnfWrite.c
@@ -207,6 +207,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
     // allocate CNF
     pCnf = ALLOC( Cnf_Dat_t, 1 );
     memset( pCnf, 0, sizeof(Cnf_Dat_t) );
+    pCnf->pMan = p->pManAig;
     pCnf->nLiterals = nLiterals;
     pCnf->nClauses = nClauses;
     pCnf->pClauses = ALLOC( int *, nClauses + 1 );
@@ -346,6 +347,7 @@ Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs )
     // allocate CNF
     pCnf = ALLOC( Cnf_Dat_t, 1 );
     memset( pCnf, 0, sizeof(Cnf_Dat_t) );
+    pCnf->pMan = p;
     pCnf->nLiterals = nLiterals;
     pCnf->nClauses = nClauses;
     pCnf->pClauses = ALLOC( int *, nClauses + 1 );
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
index 3e69e02f..bdab25dd 100644
--- a/src/aig/fra/fraCec.c
+++ b/src/aig/fra/fraCec.c
@@ -54,7 +54,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVe
     pCnf = Cnf_Derive( pMan, 0 );
 //    pCnf = Cnf_DeriveSimple( pMan, 0 );
     // convert into the SAT solver
-    pSat = Cnf_DataWriteIntoSolver( pCnf );
+    pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
     vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
     Cnf_DataFree( pCnf );
     // solve SAT
diff --git a/src/aig/fra/fraClau.c b/src/aig/fra/fraClau.c
index ea71c83b..ea8406c7 100644
--- a/src/aig/fra/fraClau.c
+++ b/src/aig/fra/fraClau.c
@@ -233,7 +233,7 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan )
     Aig_ObjChild0Flip( Aig_ManPo(pFramesMain, 0) ); // complement the first output
     pCnfMain = Cnf_DeriveSimple( pFramesMain, 0 );
 //Cnf_DataWriteIntoFile( pCnfMain, "temp.cnf", 1 );
-    p->pSatMain = Cnf_DataWriteIntoSolver( pCnfMain );
+    p->pSatMain = Cnf_DataWriteIntoSolver( pCnfMain, 1, 0 );
 /*
     {
         int i;
@@ -248,7 +248,7 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan )
     pFramesTest = Aig_ManFrames( pMan, 1, 0, 0, 1, NULL );
     assert( Aig_ManPoNum(pFramesTest) == Aig_ManRegNum(pMan) );
     pCnfTest = Cnf_DeriveSimple( pFramesTest, Aig_ManRegNum(pMan) );
-    p->pSatTest = Cnf_DataWriteIntoSolver( pCnfTest );
+    p->pSatTest = Cnf_DataWriteIntoSolver( pCnfTest, 1, 0 );
     p->nSatVarsTestBeg = p->nSatVarsTestCur = sat_solver_nvars( p->pSatTest );
 
     // derive one timeframe to be checked for BMC
@@ -256,7 +256,7 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan )
 //Aig_ManShow( pFramesBmc, 0, NULL );
     assert( Aig_ManPoNum(pFramesBmc) == Aig_ManRegNum(pMan) );
     pCnfBmc = Cnf_DeriveSimple( pFramesBmc, Aig_ManRegNum(pMan) );
-    p->pSatBmc = Cnf_DataWriteIntoSolver( pCnfBmc );
+    p->pSatBmc = Cnf_DataWriteIntoSolver( pCnfBmc, 1, 0 );
 
     // create variable sets
     p->vSatVarsMainCs = Fra_ClauSaveInputVars( pFramesMain, pCnfMain, 2 * (Aig_ManPiNum(pMan)-Aig_ManRegNum(pMan)) );
@@ -496,11 +496,11 @@ void Fra_ClauReduceClause( Vec_Int_t * vMain, Vec_Int_t * vNew )
         LitN = Vec_IntEntry( vNew, j );
         VarM = lit_var( LitM );
         VarN = lit_var( LitN );
-        if ( VarM > VarN )
+        if ( VarM < VarN )
         {
             assert( 0 );
         }
-        else if ( VarM < VarN )
+        else if ( VarM > VarN )
         {
             j++;
         }
@@ -587,14 +587,14 @@ void Fra_ClauMinimizeClause( Cla_Man_t * p, Vec_Int_t * vBasis, Vec_Int_t * vExt
         // copy literals without the given one
         Vec_IntClear( vBasis );
         Vec_IntForEachEntry( vExtra, iLit2, k )
-            if ( iLit2 != iLit )
+            if ( k != i )
                 Vec_IntPush( vBasis, iLit2 );
         // try whether it is inductive
         if ( !Fra_ClauCheckClause( p, vBasis, NULL ) )
             continue;
         // the clause is inductive
         // remove the literal
-        for ( k = iLit; k < Vec_IntSize(vExtra)-1; k++ )
+        for ( k = i; k < Vec_IntSize(vExtra)-1; k++ )
             Vec_IntWriteEntry( vExtra, k, Vec_IntEntry(vExtra,k+1) );
         Vec_IntShrink( vExtra, Vec_IntSize(vExtra)-1 );
     }
@@ -620,11 +620,11 @@ void Fra_ClauPrintClause( Vec_Int_t * vSatCsVars, Vec_Int_t * vCex )
         LitM = Vec_IntEntry( vCex, i );
         VarM = lit_var( LitM );
         VarN = Vec_IntEntry( vSatCsVars, j );
-        if ( VarM > VarN )
+        if ( VarM < VarN )
         {
             assert( 0 );
         }
-        else if ( VarM < VarN )
+        else if ( VarM > VarN )
         {
             j++;
             printf( "-" );
@@ -650,7 +650,7 @@ void Fra_ClauPrintClause( Vec_Int_t * vSatCsVars, Vec_Int_t * vCex )
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose )
+int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose, int fVeryVerbose )
 {
     Cla_Man_t * p;
     int Iter, RetValue, fFailed, i;
@@ -669,7 +669,7 @@ int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose )
             printf( "%4d : ", Iter );
         // remap clause into the test manager
         Fra_ClauRemapClause( p->pMapCsMainToCsTest, p->vCexMain0, p->vCexMain, 0 );
-        if ( fVerbose )
+        if ( fVerbose && fVeryVerbose )
             Fra_ClauPrintClause( p->vSatVarsTestCs, p->vCexMain );
         // the main counter-example is in p->vCexMain
         // intermediate counter-examples are in p->vCexTest
@@ -679,8 +679,17 @@ int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose )
         {
             Fra_ClauReduceClause( p->vCexMain, p->vCexTest );
             Fra_ClauRemapClause( p->pMapCsTestToNsBmc, p->vCexMain, p->vCexBmc, 0 );
-            if ( !Fra_ClauCheckBmc(p, p->vCexBmc) )
+
+//            if ( !Fra_ClauCheckBmc(p, p->vCexBmc) )
+            if ( Vec_IntSize(p->vCexMain) < 1 )
             {
+                Vec_IntComplement( p->vCexMain0 ); 
+                RetValue = sat_solver_addclause( p->pSatMain, Vec_IntArray(p->vCexMain0), Vec_IntArray(p->vCexMain0) + Vec_IntSize(p->vCexMain0) );
+                if ( RetValue == 0 )
+                {
+                    printf( "\nProperty is proved after %d iterations.\n", Iter+1 );
+                    return 0;
+                }
                 fFailed = 1;
                 break;
             }
@@ -698,14 +707,21 @@ int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose )
             continue;
         }
         if ( fVerbose )
-            printf( " LitsAfterRed = %3d.  ", Vec_IntSize(p->vCexMain) );
+            printf( "  " );
+        if ( fVerbose && fVeryVerbose )
+            Fra_ClauPrintClause( p->vSatVarsTestCs, p->vCexMain );
+        if ( fVerbose )
+            printf( " LitsInd = %3d.  ", Vec_IntSize(p->vCexMain) );
         // minimize the inductive property
         Vec_IntClear( p->vCexBase );
+        if ( Vec_IntSize(p->vCexMain) > 1 )
 //        Fra_ClauMinimizeClause_rec( p, p->vCexBase, p->vCexMain );
-//        Fra_ClauMinimizeClause( p, p->vCexBase, p->vCexMain );
+            Fra_ClauMinimizeClause( p, p->vCexBase, p->vCexMain );
         assert( Vec_IntSize(p->vCexMain) > 0 );
+        if ( fVerbose && fVeryVerbose )
+            Fra_ClauPrintClause( p->vSatVarsTestCs, p->vCexMain );
         if ( fVerbose )
-            printf( " LitsAfterMin = %3d.  ", Vec_IntSize(p->vCexMain) );
+            printf( " LitsRed = %3d.  ", Vec_IntSize(p->vCexMain) );
         if ( fVerbose )
             printf( "\n" );
         // add the clause to the solver
@@ -716,6 +732,12 @@ int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose )
             Iter++;
             break;
         }
+        if ( p->pSatMain->qtail != p->pSatMain->qhead )
+        {
+            RetValue = sat_solver_simplify(p->pSatMain);
+            assert( RetValue != 0 );
+            assert( p->pSatMain->qtail == p->pSatMain->qhead );
+        }
     }
 
     // report the results
diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c
new file mode 100644
index 00000000..8024431e
--- /dev/null
+++ b/src/aig/fra/fraClaus.c
@@ -0,0 +1,912 @@
+/**CFile****************************************************************
+
+  FileName    [fraClaus.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [New FRAIG package.]
+
+  Synopsis    [Induction with clause strengthening.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 30, 2007.]
+
+  Revision    [$Id: fraClau.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fra.h"
+#include "cnf.h"
+#include "satSolver.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Clu_Man_t_    Clu_Man_t;
+struct Clu_Man_t_
+{
+    // parameters
+    int              nFrames;
+    int              nClausesMax;
+    int              fVerbose;
+    int              fVeryVerbose;
+    int              nSimWords;
+    int              nSimFrames;
+    // the network
+    Aig_Man_t *      pAig;
+    // SAT solvers
+    sat_solver *     pSatMain;
+    sat_solver *     pSatBmc;
+    // CNF for the test solver
+    Cnf_Dat_t *      pCnf;
+    // the counter example
+    Vec_Int_t *      vValues;
+    // clauses
+    Vec_Int_t *      vLits;
+    Vec_Int_t *      vClauses;
+    Vec_Int_t *      vCosts;
+    int              nClauses;
+    // counter-examples
+    Vec_Ptr_t *      vCexes;
+    int              nCexes;
+    int              nCexesAlloc;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Runs the SAT solver on the problem.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_ClausRunBmc( Clu_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int * pLits;
+    int nBTLimit = 0;
+    int i, RetValue;
+    pLits = ALLOC( int, p->nFrames + 1 );
+    // set the output literals
+    pObj = Aig_ManPo(p->pAig, 0);
+    for ( i = 0; i < p->nFrames; i++ )
+        pLits[i] = i * 2 * p->pCnf->nVars + toLitCond( p->pCnf->pVarNums[pObj->Id], 0 ); 
+    // try to solve the problem
+//    sat_solver_act_var_clear( p->pSatBmc );
+//    RetValue = sat_solver_solve( p->pSatBmc, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+    for ( i = 0; i < p->nFrames; i++ )
+    {
+        RetValue = sat_solver_solve( p->pSatBmc, pLits + i, pLits + i + 1, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+        if ( RetValue != l_False )
+        {
+            free( pLits );
+            return 0;
+        }
+    }
+    free( pLits );
+
+/*
+    // get the counter-example
+    assert( RetValue == l_True );
+    nVarsTot = p->nFrames * p->pCnf->nVars;
+    Aig_ManForEachObj( p->pAig, pObj, i )
+        Vec_IntWriteEntry( p->vValues, i, sat_solver_var_value(p->pSatBmc, nVarsTot + p->pCnf->pVarNums[i]) );
+*/
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Runs the SAT solver on the problem.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_ClausRunSat( Clu_Man_t * p )
+{
+    int nBTLimit = 0;
+    Aig_Obj_t * pObj;
+    int * pLits;
+    int i, nVarsTot, RetValue;
+    pLits = ALLOC( int, p->nFrames + 1 );
+    // set the output literals
+    pObj = Aig_ManPo(p->pAig, 0);
+    for ( i = 0; i <= p->nFrames; i++ )
+        pLits[i] = i * 2 * p->pCnf->nVars + toLitCond( p->pCnf->pVarNums[pObj->Id], i != p->nFrames ); 
+    // try to solve the problem
+//    sat_solver_act_var_clear( p->pSatMain );
+//    RetValue = sat_solver_solve( p->pSatMain, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+    RetValue = sat_solver_solve( p->pSatMain, pLits, pLits + p->nFrames + 1, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+    free( pLits );
+    if ( RetValue == l_False )
+        return 1;
+    // get the counter-example
+    assert( RetValue == l_True );
+    nVarsTot = p->nFrames * p->pCnf->nVars;
+    Aig_ManForEachObj( p->pAig, pObj, i )
+        Vec_IntWriteEntry( p->vValues, i, sat_solver_var_value(p->pSatMain, nVarsTot + p->pCnf->pVarNums[i]) );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Runs the SAT solver on the problem.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_ClausRunSat0( Clu_Man_t * p )
+{
+    int nBTLimit = 0;
+    Aig_Obj_t * pObj;
+    int Lits[2], RetValue;
+    pObj = Aig_ManPo(p->pAig, 0);
+    Lits[0] = toLitCond( p->pCnf->pVarNums[pObj->Id], 0 ); 
+    RetValue = sat_solver_solve( p->pSatMain, Lits, Lits + 1, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+    if ( RetValue == l_False )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Processes the clauses.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+/*
+int Fra_ClausProcessClausesCut( Clu_Man_t * p, Dar_Cut_t * pCut )
+{
+    unsigned * pSimsC[4], * pSimsS[4];
+    int pLits[4];
+    int i, b, k, iMint, uMask, RetValue, nLeaves, nWordsTotal, nCounter;
+    // compute parameters
+    nLeaves = pCut->nLeaves;
+    nWordsTotal = p->pComb->nWordsTotal;
+    assert( nLeaves > 1 && nLeaves < 5 );
+    assert( nWordsTotal == p->pSeq->nWordsTotal );
+    // get parameters
+    for ( i = 0; i < (int)pCut->nLeaves; i++ )
+    {
+        pSimsC[i] = Fra_ObjSim( p->pComb, pCut->pLeaves[i] );
+        pSimsS[i] = Fra_ObjSim( p->pSeq,  pCut->pLeaves[i] );
+    }
+    // add combinational patterns
+    uMask = 0;
+    for ( i = 0; i < nWordsTotal; i++ )
+        for ( k = 0; k < 32; k++ )
+        {
+            iMint = 0;
+            for ( b = 0; b < nLeaves; b++ )
+                if ( pSimsC[b][i] & (1 << k) )
+                    iMint |= (1 << b);
+            uMask |= (1 << iMint);
+        }
+    // remove sequential patterns
+    for ( i = 0; i < nWordsTotal; i++ )
+        for ( k = 0; k < 32; k++ )
+        {
+            iMint = 0;
+            for ( b = 0; b < nLeaves; b++ )
+                if ( pSimsS[b][i] & (1 << k) )
+                    iMint |= (1 << b);
+            uMask &= ~(1 << iMint);
+        }
+    if ( uMask == 0 )
+        return 0;
+    // add clauses for the remaining patterns
+    nCounter = 0;
+    for ( i = 0; i < (1<<nLeaves); i++ )
+    {
+        if ( (uMask & (1 << i)) == 0 )
+            continue;
+        nCounter++;
+//        continue;
+
+        // add every third clause
+//        if ( (nCounter % 2) == 0 )
+//            continue;
+
+        for ( b = 0; b < nLeaves; b++ )
+            pLits[b] = toLitCond( p->pCnf->pVarNums[pCut->pLeaves[b]], (i&(1<<b)) );
+        // add the clause
+        RetValue = sat_solver_addclause( p->pSatMain, pLits, pLits + nLeaves );
+//        assert( RetValue == 1 );
+        if ( RetValue == 0 )
+        {
+            printf( "Already UNSAT after %d clauses.\n", nCounter );
+            return -1;
+        }
+    }
+    return nCounter;
+}
+*/
+
+
+/**Function*************************************************************
+
+  Synopsis    [Return combinations appearing in the cut.]
+
+  Description [This procedure is taken from "Hacker's Delight" by H.S.Warren.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void transpose32a( unsigned a[32] ) 
+{
+    int j, k;
+    unsigned long m, t;
+    for ( j = 16, m = 0x0000FFFF; j; j >>= 1, m ^= m << j ) 
+    {
+        for ( k = 0; k < 32; k = ((k | j) + 1) & ~j ) 
+        {
+            t = (a[k] ^ (a[k|j] >> j)) & m;
+            a[k] ^= t;
+            a[k|j] ^= (t << j);
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Return combinations appearing in the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_ClausProcessClausesCut( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t * pCut, int * pScores )
+{
+    unsigned Matrix[32];
+    unsigned * pSims[4], uWord;
+    int nSeries, i, k, j;
+    // compute parameters
+    assert( pCut->nLeaves > 1 && pCut->nLeaves < 5 );
+    assert( pSimMan->nWordsTotal % 8 == 0 );
+    // get parameters
+    for ( i = 0; i < (int)pCut->nLeaves; i++ )
+        pSims[i] = Fra_ObjSim( pSimMan, pCut->pLeaves[i] );
+    // add combinational patterns
+    memset( pScores, 0, sizeof(int) * 16 );
+    nSeries = pSimMan->nWordsTotal / 8;
+    for ( i = 0; i < nSeries; i++ )
+    {
+        memset( Matrix, 0, sizeof(unsigned) * 32 );
+        for ( k = 0; k < 8; k++ )
+            for ( j = 0; j < (int)pCut->nLeaves; j++ )
+                Matrix[31-(k*4+j)] = pSims[j][i*8+k];
+/*
+        for ( k = 0; k < 32; k++ )
+        {
+            Extra_PrintBinary( stdout, Matrix + k, 32 ); printf( "\n" );
+        }
+        printf( "\n" );
+*/
+        transpose32a( Matrix );
+/*
+        for ( k = 0; k < 32; k++ )
+        {
+            Extra_PrintBinary( stdout, Matrix + k, 32 ); printf( "\n" );
+        }
+        printf( "\n" );
+*/
+        for ( k = 0; k < 32; k++ )
+            for ( j = 0, uWord = Matrix[k]; j < 8; j++, uWord >>= 4 )
+                pScores[uWord & 0xF]++;
+    }
+    // collect patterns
+    uWord = 0;
+    for ( i = 0; i < 16; i++ )
+        if ( pScores[i] )
+            uWord |= (1 << i);
+//    Extra_PrintBinary( stdout, &uWord, 16 ); printf( "\n" );
+    return (int)uWord;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Return combinations appearing in the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_ClausProcessClausesCut2( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t * pCut, int * pScores )
+{
+    unsigned * pSims[4], uWord;
+    int iMint, i, k, b;
+    // compute parameters
+    assert( pCut->nLeaves > 1 && pCut->nLeaves < 5 );
+    assert( pSimMan->nWordsTotal % 8 == 0 );
+    // get parameters
+    for ( i = 0; i < (int)pCut->nLeaves; i++ )
+        pSims[i] = Fra_ObjSim( pSimMan, pCut->pLeaves[i] );
+    // add combinational patterns
+    memset( pScores, 0, sizeof(int) * 16 );
+    for ( i = 0; i < pSimMan->nWordsTotal; i++ )
+        for ( k = 0; k < 32; k++ )
+        {
+            iMint = 0;
+            for ( b = 0; b < (int)pCut->nLeaves; b++ )
+                if ( pSims[b][i] & (1 << k) )
+                    iMint |= (1 << b);
+            pScores[iMint]++;
+        }
+    // collect patterns
+    uWord = 0;
+    for ( i = 0; i < 16; i++ )
+        if ( pScores[i] )
+            uWord |= (1 << i);
+//    Extra_PrintBinary( stdout, &uWord, 16 ); printf( "\n" );
+    return (int)uWord;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Processes the clauses.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ClausRecordClause( Clu_Man_t * p, Dar_Cut_t * pCut, int iMint, int Cost )
+{
+    int i;
+    for ( i = 0; i < (int)pCut->nLeaves; i++ )
+        Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pCut->pLeaves[i]], (iMint&(1<<i)) ) );
+    Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
+    Vec_IntPush( p->vCosts, Cost );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Processes the clauses.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_ClausProcessClauses( Clu_Man_t * p )
+{
+    Aig_MmFixed_t * pMemCuts;
+    Fra_Sml_t * pComb, * pSeq;
+    Aig_Obj_t * pObj;
+    Dar_Cut_t * pCut;
+    int Scores[16], uScores, i, k, j, clk, nCuts = 0;
+
+    // simulate the AIG
+clk = clock();
+    srand( 0xAABBAABB );
+    pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nSimFrames, p->nSimWords/p->nSimFrames );
+    if ( pSeq->fNonConstOut )
+    {
+        printf( "Property failed after sequential simulation!\n" );
+        Fra_SmlStop( pSeq );
+        return 0;
+    }
+PRT( "Sim-seq", clock() - clk );
+
+    // generate cuts for all nodes, assign cost, and find best cuts
+clk = clock();
+    pMemCuts = Dar_ManComputeCuts( p->pAig, 10 );
+PRT( "Cuts   ", clock() - clk );
+
+    // collect sequential info for each cut
+clk = clock();
+    Aig_ManForEachNode( p->pAig, pObj, i )
+        Dar_ObjForEachCut( pObj, pCut, k )
+            if ( pCut->nLeaves > 1 )
+            {
+                pCut->uTruth = Fra_ClausProcessClausesCut( p, pSeq, pCut, Scores );
+//                uScores = Fra_ClausProcessClausesCut2( p, pSeq, pCut, Scores );
+//                if ( uScores != pCut->uTruth )
+//                {
+//                    int x = 0;
+//                }
+            }
+PRT( "Infoseq", clock() - clk );
+    Fra_SmlStop( pSeq );
+
+    // perform combinational simulation
+clk = clock();
+    srand( 0xAABBAABB );
+    pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords );
+PRT( "Sim-cmb", clock() - clk );
+
+    // collect combinational info for each cut
+clk = clock();
+    Aig_ManForEachNode( p->pAig, pObj, i )
+        Dar_ObjForEachCut( pObj, pCut, k )
+            if ( pCut->nLeaves > 1 )
+            {
+                nCuts++;
+                uScores = Fra_ClausProcessClausesCut( p, pComb, pCut, Scores );
+                uScores &= ~pCut->uTruth; pCut->uTruth = 0;
+                if ( uScores == 0 )
+                    continue;
+                // write the clauses
+                for ( j = 0; j < (1<<pCut->nLeaves); j++ )
+                    if ( uScores & (1 << j) )
+                        Fra_ClausRecordClause( p, pCut, j, Scores[j] );
+
+            }
+    Fra_SmlStop( pComb );
+    Aig_MmFixedStop( pMemCuts, 0 );
+PRT( "Infocmb", clock() - clk );
+
+    printf( "Node = %5d. Non-triv cuts = %7d. Clauses = %6d. Clause per cut = %6.2f.\n", 
+        Aig_ManNodeNum(p->pAig), nCuts, Vec_IntSize(p->vClauses), 1.0*Vec_IntSize(p->vClauses)/nCuts );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts AIG into the SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_ClausBmcClauses( Clu_Man_t * p )
+{
+    int nBTLimit = 0;
+    int * pStart, nLitsTot, RetValue, Beg, End, Counter, i, k, f;
+/*
+    for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
+        printf( "%d ", p->vLits->pArray[i] );
+    printf( "\n" );
+*/
+    // add the clauses
+    Counter = 0;
+    nLitsTot = 2 * p->pCnf->nVars;
+    for ( f = 0; f < p->nFrames; f++ )
+    {
+        Beg = 0;
+        Vec_IntForEachEntry( p->vClauses, End, i )
+        {
+            if ( Vec_IntEntry( p->vCosts, i ) == -1 )
+            {
+                Beg = End;
+                continue;
+            }
+            assert( Vec_IntEntry( p->vCosts, i ) > 0 );
+            assert( End - Beg < 5 );
+            pStart = Vec_IntArray(p->vLits);
+            for ( k = Beg; k < End; k++ )
+                pStart[k] = lit_neg( pStart[k] );
+            RetValue = sat_solver_solve( p->pSatBmc, pStart + Beg, pStart + End, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+            for ( k = Beg; k < End; k++ )
+                pStart[k] = lit_neg( pStart[k] );
+            if ( RetValue != l_False )
+            {
+                Beg = End;
+                Vec_IntWriteEntry( p->vCosts, i, -1 );
+                Counter++;
+                continue;
+            }
+/*
+            // add the clause
+            RetValue = sat_solver_addclause( p->pSatBmc, pStart + Beg, pStart + End );
+    //        assert( RetValue == 1 );
+            if ( RetValue == 0 )
+            {
+                printf( "Error: Solver is UNSAT after adding BMC clauses.\n" );
+                return -1;
+            }
+*/
+            Beg = End;
+
+            // simplify the solver
+            if ( p->pSatBmc->qtail != p->pSatBmc->qhead )
+            {
+                RetValue = sat_solver_simplify(p->pSatBmc);
+                assert( RetValue != 0 );
+                assert( p->pSatBmc->qtail == p->pSatBmc->qhead );
+            }
+        }
+        // increment literals
+        for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
+            p->vLits->pArray[i] += nLitsTot;
+    }
+
+    // return clauses back to normal
+    nLitsTot = p->nFrames * nLitsTot;
+    for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
+        p->vLits->pArray[i] -= nLitsTot;
+/*
+    for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
+        printf( "%d ", p->vLits->pArray[i] );
+    printf( "\n" );
+*/
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts AIG into the SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_ClausInductiveClauses( Clu_Man_t * p )
+{
+    int nBTLimit = 0;
+    int * pStart, nLitsTot, RetValue, Beg, End, Counter, i, k, f;
+
+    // reset the solver
+    if ( p->pSatMain )  sat_solver_delete( p->pSatMain );
+    p->pSatMain = Cnf_DataWriteIntoSolver( p->pCnf, p->nFrames+1, 0 );
+    if ( p->pSatMain == NULL )
+    {
+        printf( "Error: Main solver is unsat.\n" );
+        return -1;
+    }
+/*
+    // check if the property holds
+    if ( Fra_ClausRunSat0( p ) )
+        printf( "Property holds without strengthening.\n" );
+    else
+        printf( "Property does not hold without strengthening.\n" );
+*/
+    // add the clauses
+    nLitsTot = 2 * p->pCnf->nVars;
+    for ( f = 0; f < p->nFrames; f++ )
+    {
+        Beg = 0;
+        Vec_IntForEachEntry( p->vClauses, End, i )
+        {
+            if ( Vec_IntEntry( p->vCosts, i ) == -1 )
+            {
+                Beg = End;
+                continue;
+            }
+            assert( Vec_IntEntry( p->vCosts, i ) > 0 );
+            assert( End - Beg < 5 );
+            pStart = Vec_IntArray(p->vLits);
+            // add the clause to all timeframes
+            RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
+            if ( RetValue == 0 )
+            {
+                printf( "Error: Solver is UNSAT after adding assumption clauses.\n" );
+                return -1;
+            }
+            Beg = End;
+        }
+        // increment literals
+        for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
+            p->vLits->pArray[i] += nLitsTot;
+    }
+
+    // simplify the solver
+    if ( p->pSatMain->qtail != p->pSatMain->qhead )
+    {
+        RetValue = sat_solver_simplify(p->pSatMain);
+        assert( RetValue != 0 );
+        assert( p->pSatMain->qtail == p->pSatMain->qhead );
+    }
+  
+    // check if the property holds
+    if ( Fra_ClausRunSat0( p ) )
+    {
+//        printf( "Property holds with strengthening.\n" );
+        printf( " Property holds.  " );
+    }
+    else
+    {
+        printf( " Property fails.  " );
+        return -2;
+    }
+
+/*
+    // add the property for the first K frames
+    for ( i = 0; i < p->nFrames; i++ )
+    {
+        Aig_Obj_t * pObj;
+        int Lits[2];
+        // set the output literals
+        pObj = Aig_ManPo(p->pAig, 0);
+        Lits[0] = i * nLitsTot + toLitCond( p->pCnf->pVarNums[pObj->Id], 1 ); 
+        // add the clause
+        RetValue = sat_solver_addclause( p->pSatMain, Lits, Lits + 1 );
+//        assert( RetValue == 1 );
+        if ( RetValue == 0 )
+        {
+            printf( "Error: Solver is UNSAT after adding property for the first K frames.\n" );
+            return -1;
+        }
+    }
+*/
+
+    // simplify the solver
+    if ( p->pSatMain->qtail != p->pSatMain->qhead )
+    {
+        RetValue = sat_solver_simplify(p->pSatMain);
+        assert( RetValue != 0 );
+        assert( p->pSatMain->qtail == p->pSatMain->qhead );
+    }
+
+
+    // check the clause in the last timeframe
+    Beg = 0;
+    Counter = 0;
+    Vec_IntForEachEntry( p->vClauses, End, i )
+    {
+        if ( Vec_IntEntry( p->vCosts, i ) == -1 )
+        {
+            Beg = End;
+            continue;
+        }
+        assert( Vec_IntEntry( p->vCosts, i ) > 0 );
+        assert( End - Beg < 5 );
+        pStart = Vec_IntArray(p->vLits);
+
+        for ( k = Beg; k < End; k++ )
+            pStart[k] = lit_neg( pStart[k] );
+        RetValue = sat_solver_solve( p->pSatMain, pStart + Beg, pStart + End, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+        for ( k = Beg; k < End; k++ )
+            pStart[k] = lit_neg( pStart[k] );
+
+        // the problem is not solved
+        if ( RetValue != l_False )
+        {
+            Beg = End;
+            Vec_IntWriteEntry( p->vCosts, i, -1 );
+            Counter++;
+            continue;
+        }
+        // add the clause
+        RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
+//        assert( RetValue == 1 );
+        if ( RetValue == 0 )
+        {
+            printf( "Error: Solver is UNSAT after adding BMC clauses.\n" );
+            return -1;
+        }
+        Beg = End;
+
+        // simplify the solver
+        if ( p->pSatMain->qtail != p->pSatMain->qhead )
+        {
+            RetValue = sat_solver_simplify(p->pSatMain);
+            assert( RetValue != 0 );
+            assert( p->pSatMain->qtail == p->pSatMain->qhead );
+        }
+    }
+
+    // return clauses back to normal
+    nLitsTot = p->nFrames * nLitsTot;
+    for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
+        p->vLits->pArray[i] -= nLitsTot;
+
+    return Counter;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Converts AIG into the SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Clu_Man_t * Fra_ClausAlloc( Aig_Man_t * pAig, int nFrames, int nClausesMax, int fVerbose, int fVeryVerbose )
+{
+    Clu_Man_t * p;
+    p = ALLOC( Clu_Man_t, 1 );
+    memset( p, 0, sizeof(Clu_Man_t) );
+    p->pAig         = pAig;
+    p->nFrames      = nFrames;
+    p->nClausesMax  = nClausesMax;
+    p->fVerbose     = fVerbose;
+    p->fVeryVerbose = fVeryVerbose;
+    p->nSimWords    = 256;//1024;//64;
+    p->nSimFrames   = 16;//8;//32;
+    p->vValues      = Vec_IntStart( Aig_ManObjNumMax(p->pAig) );
+
+    p->vLits        = Vec_IntAlloc( 1<<14 );
+    p->vClauses     = Vec_IntAlloc( 1<<12 );
+    p->vCosts       = Vec_IntAlloc( 1<<12 );
+
+    p->nCexesAlloc  = 1024;
+    p->vCexes       = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p->pAig), p->nCexesAlloc/32 );
+    Vec_PtrCleanSimInfo( p->vCexes, 0, p->nCexesAlloc/32 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts AIG into the SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ClausFree( Clu_Man_t * p )
+{
+    if ( p->vCexes )    Vec_PtrFree( p->vCexes );
+    if ( p->vLits )     Vec_IntFree( p->vLits );
+    if ( p->vClauses )  Vec_IntFree( p->vClauses );
+    if ( p->vCosts )    Vec_IntFree( p->vCosts );
+    if ( p->vValues )   Vec_IntFree( p->vValues );
+    if ( p->pCnf )      Cnf_DataFree( p->pCnf );
+    if ( p->pSatMain )  sat_solver_delete( p->pSatMain );
+    if ( p->pSatBmc )   sat_solver_delete( p->pSatBmc );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts AIG into the SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nClausesMax, int fBmc, int fVerbose, int fVeryVerbose )
+{
+    Clu_Man_t * p;
+    int clk, clkTotal = clock();
+    int Iter, Counter;
+
+    assert( Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig) == 1 );
+
+    // create the manager
+    p = Fra_ClausAlloc( pAig, nFrames, nClausesMax, fVerbose, fVeryVerbose );
+
+clk = clock();
+    // derive CNF
+    p->pAig->nRegs++;
+    p->pCnf = Cnf_DeriveSimple( p->pAig, Aig_ManPoNum(p->pAig) );
+    p->pAig->nRegs--;
+PRT( "CNF    ", clock() - clk );
+
+    // check BMC
+clk = clock();
+    p->pSatBmc = Cnf_DataWriteIntoSolver( p->pCnf, p->nFrames, 1 );
+    if ( p->pSatBmc == NULL )
+    {
+        printf( "Error: BMC solver is unsat.\n" );
+        Fra_ClausFree( p );
+        return 1;
+    }
+    if ( !Fra_ClausRunBmc( p ) )
+    {
+        printf( "Problem trivially fails the base case.\n" );
+        Fra_ClausFree( p );
+        return 1;
+    }
+PRT( "SAT try", clock() - clk );
+
+    // start the SAT solver
+clk = clock();
+    p->pSatMain = Cnf_DataWriteIntoSolver( p->pCnf, p->nFrames+1, 0 );
+    if ( p->pSatMain == NULL )
+    {
+        printf( "Error: Main solver is unsat.\n" );
+        Fra_ClausFree( p );
+        return 1;
+    } 
+    // try solving without additional clauses
+    if ( Fra_ClausRunSat( p ) )
+    {
+        printf( "Problem is inductive without strengthening.\n" );
+        Fra_ClausFree( p );
+        return 1;
+    }
+PRT( "SAT try", clock() - clk );
+ 
+    // collect the candidate inductive clauses using 4-cuts
+clk = clock();
+    Fra_ClausProcessClauses( p );
+    p->nClauses = Vec_IntSize( p->vClauses );
+PRT( "Clauses", clock() - clk );
+
+
+    // check clauses using BMC
+    if ( fBmc ) 
+    {
+clk = clock();
+        Counter = Fra_ClausBmcClauses( p );
+        p->nClauses -= Counter;
+        printf( "BMC disproved %d clauses.\n", Counter );
+PRT( "Cla-bmc", clock() - clk );
+    }
+
+
+    // prove clauses inductively
+clk = clock();
+    Counter = 1;
+    for ( Iter = 0; Counter > 0; Iter++ )
+    {
+        printf( "Iter %3d :  Begin = %5d. ", Iter, p->nClauses );
+        Counter = Fra_ClausInductiveClauses( p );
+        if ( Counter > 0 )
+           p->nClauses -= Counter;
+        printf( "End = %5d. ", p->nClauses );
+//        printf( "\n" );
+        PRT( "Time", clock() - clk );
+        clk = clock();
+    }
+    if ( Counter == -1 )
+        printf( "Fra_Claus(): Internal error.\n" );
+    else if ( Counter == -2 )
+        printf( "Property FAILS after %d iterations of refinement.\n", Iter );
+    else
+        printf( "Property HOLDS inductively after strengthening.\n" );
+
+/*
+clk = clock();
+    if ( Fra_ClausRunSat( p ) )
+        printf( "Problem is solved.\n" );
+    else
+        printf( "Problem is unsolved.\n" );
+PRT( "SAT try", clock() - clk );
+*/
+
+PRT( "TOTAL  ", clock() - clkTotal );
+printf( "\n" );
+    // clean the manager
+    Fra_ClausFree( p );
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 6cfdc3ff..dbc6401f 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -339,7 +339,7 @@ PRT( "Time", clock() - clk );
 //    Aig_ManDumpBlif( pManAigNew, "frame_aig.blif" );
 //    Fra_ManPartitionTest2( pManAigNew );
 //    Aig_ManStop( pManAigNew );
-
+ 
     // iterate the inductive case
     p->pCla->fRefinement = 1;
     for ( nIter = 0; p->pCla->fRefinement; nIter++ )
@@ -365,7 +365,7 @@ p->timeTrav += clock() - clk2;
             pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
 //Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
 
-        p->pSat = Cnf_DataWriteIntoSolver( pCnf );
+        p->pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
         p->nSatVars = pCnf->nVars;
         assert( p->pSat != NULL );
         if ( p->pSat == NULL )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 20aa7247..3b238779 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -6193,8 +6193,11 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;//, * pNtkRes;
     int c;
+    int fBmc;
+    int nFrames;
     int nLevels;
     int fVerbose;
+    int fVeryVerbose;
 //    extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk );
 //    extern Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk );
 //    extern void Abc_NtkMaxFlowTest( Abc_Ntk_t * pNtk );
@@ -6207,20 +6210,34 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
     extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
     extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
-    extern int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
+    extern int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nStepsMax, int fBmc, int fVerbose, int fVeryVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    fVeryVerbose = 0;
     fVerbose = 1;
-    nLevels  = 1000;
+    fBmc     = 1;
+    nFrames  = 1;
+    nLevels  = 200;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Nvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FNbvwh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFrames = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFrames < 0 ) 
+                goto usage;
+            break;
         case 'N':
             if ( globalUtilOptind >= argc )
             {
@@ -6232,9 +6249,15 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nLevels < 0 ) 
                 goto usage;
             break;
+        case 'b':
+            fBmc ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
+        case 'w':
+            fVeryVerbose ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -6355,12 +6378,13 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
 */
 //    Abc_NtkDarHaigRecord( pNtk );
-    Abc_NtkDarClau( pNtk, 1000, fVerbose );
+    Abc_NtkDarClau( pNtk, nFrames, nLevels, fBmc, fVerbose, fVeryVerbose );
     return 0;
 usage:
-    fprintf( pErr, "usage: test [-h]\n" );
+    fprintf( pErr, "usage: test [-vwh]\n" );
     fprintf( pErr, "\t         testbench for new procedures\n" );
     fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-w     : toggle printing very verbose information [default = %s]\n", fVeryVerbose? "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 67f22eb7..e23b04dd 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -56,12 +56,20 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
         assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) );
         Abc_NtkForEachCi( pNtk, pObj, i )
             if ( i < Abc_NtkPiNum(pNtk) )
+            {
                 assert( Abc_ObjIsPi(pObj) );
+                if ( !Abc_ObjIsPi(pObj) )
+                    printf( "Abc_NtkToDar(): Temporary bug: The PI ordering is wrong!\n" );
+            }
             else
                 assert( Abc_ObjIsBo(pObj) );
         Abc_NtkForEachCo( pNtk, pObj, i )
             if ( i < Abc_NtkPoNum(pNtk) )
+            {
                 assert( Abc_ObjIsPo(pObj) );
+                if ( !Abc_ObjIsPo(pObj) )
+                    printf( "Abc_NtkToDar(): Temporary bug: The PO ordering is wrong!\n" );
+            }
             else
                 assert( Abc_ObjIsBi(pObj) );
         // print warning about initial values
@@ -1401,9 +1409,10 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
+int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nStepsMax, int fBmc, int fVerbose, int fVeryVerbose )
 {
-    extern int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose );
+    extern int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose, int fVeryVerbose );
+    extern int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nClauses, int fBmc, int fVerbose, int fVeryVerbose );
     Aig_Man_t * pMan;
     if ( Abc_NtkPoNum(pNtk) != 1 )
     {
@@ -1418,7 +1427,8 @@ int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
         Vec_IntFree( pMan->vFlopNums ); 
     pMan->vFlopNums = NULL;
 
-    Fra_Clau( pMan, nStepsMax, fVerbose );
+//    Fra_Clau( pMan, nStepsMax, fVerbose, fVeryVerbose );
+    Fra_Claus( pMan, nFrames, nStepsMax, fBmc, fVerbose, fVeryVerbose );
     Aig_ManStop( pMan );
     return 1;
 }
diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c
index d3c4c878..273b2d5a 100644
--- a/src/base/io/ioReadAiger.c
+++ b/src/base/io/ioReadAiger.c
@@ -237,8 +237,8 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
             Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
             Counter++;
         }
-        if ( Counter )
-            printf( "Io_ReadAiger(): Added %d default names for nameless I/O/register objects.\n", Counter );
+//        if ( Counter )
+//            printf( "Io_ReadAiger(): Added %d default names for nameless I/O/register objects.\n", Counter );
     }
     else
     {
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
index 1862bc7c..9595bc72 100644
--- a/src/misc/vec/vecPtr.h
+++ b/src/misc/vec/vecPtr.h
@@ -151,71 +151,6 @@ static inline Vec_Ptr_t * Vec_PtrAllocArrayCopy( void ** pArray, int nSize )
 
 /**Function*************************************************************
 
-  Synopsis    [Allocates the array of simulation info.]
-
-  Description [Allocates the array containing given number of entries, 
-  each of which contains given number of unsigned words of simulation data.
-  The resulting array can be freed using regular procedure Vec_PtrFree().
-  It is the responsibility of the user to ensure this array is never grown.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Ptr_t * Vec_PtrAllocSimInfo( int nEntries, int nWords )
-{
-    void ** pMemory;
-    unsigned * pInfo;
-    int i;
-    pMemory = (void **)ALLOC( char, (sizeof(void *) + sizeof(unsigned) * nWords) * nEntries );
-    pInfo = (unsigned *)(pMemory + nEntries);
-    for ( i = 0; i < nEntries; i++ )
-        pMemory[i] = pInfo + i * nWords;
-    return Vec_PtrAllocArray( pMemory, nEntries );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates the array of truth tables for the given number of vars.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Ptr_t * Vec_PtrAllocTruthTables( int nVars )
-{
-    Vec_Ptr_t * p;
-    unsigned Masks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
-    unsigned * pTruth;
-    int i, k, nWords;
-    nWords = (nVars <= 5 ? 1 : (1 << (nVars - 5)));
-    p = Vec_PtrAllocSimInfo( nVars, nWords );
-    for ( i = 0; i < nVars; i++ )
-    {
-        pTruth = (unsigned *)p->pArray[i];
-        if ( i < 5 )
-        {
-            for ( k = 0; k < nWords; k++ )
-                pTruth[k] = Masks[i];
-        }
-        else
-        {
-            for ( k = 0; k < nWords; k++ )
-                if ( k & (1 << (i-5)) )
-                    pTruth[k] = ~(unsigned)0;
-                else
-                    pTruth[k] = 0;
-        }
-    }
-    return p;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Duplicates the integer array.]
 
   Description []
@@ -348,37 +283,6 @@ static inline void * Vec_PtrEntry( Vec_Ptr_t * p, int i )
 
 /**Function*************************************************************
 
-  Synopsis    [Resizes the array of simulation info.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_PtrDoubleSimInfo( Vec_Ptr_t * vInfo )
-{
-    Vec_Ptr_t * vInfoNew;
-    int nWords;
-    assert( Vec_PtrSize(vInfo) > 2 );
-    // get the new array
-    nWords = (unsigned *)Vec_PtrEntry(vInfo,1) - (unsigned *)Vec_PtrEntry(vInfo,0);
-    vInfoNew = Vec_PtrAllocSimInfo( 2*Vec_PtrSize(vInfo), nWords );
-    // copy the simulation info
-    memcpy( Vec_PtrEntry(vInfoNew,0), Vec_PtrEntry(vInfo,0), Vec_PtrSize(vInfo) * nWords * 4 );
-    // replace the array
-    free( vInfo->pArray );
-    vInfo->pArray = vInfoNew->pArray;
-    vInfo->nSize *= 2;
-    vInfo->nCap *= 2;
-    // free the old array
-    vInfoNew->pArray = NULL;
-    free( vInfoNew );
-}
-
-/**Function*************************************************************
-
   Synopsis    []
 
   Description []
@@ -753,6 +657,152 @@ static inline void Vec_PtrUniqify( Vec_Ptr_t * p, int (*Vec_PtrSortCompare)() )
     p->nSize = k;
 }
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the array of simulation info.]
+
+  Description [Allocates the array containing given number of entries, 
+  each of which contains given number of unsigned words of simulation data.
+  The resulting array can be freed using regular procedure Vec_PtrFree().
+  It is the responsibility of the user to ensure this array is never grown.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Ptr_t * Vec_PtrAllocSimInfo( int nEntries, int nWords )
+{
+    void ** pMemory;
+    unsigned * pInfo;
+    int i;
+    pMemory = (void **)ALLOC( char, (sizeof(void *) + sizeof(unsigned) * nWords) * nEntries );
+    pInfo = (unsigned *)(pMemory + nEntries);
+    for ( i = 0; i < nEntries; i++ )
+        pMemory[i] = pInfo + i * nWords;
+    return Vec_PtrAllocArray( pMemory, nEntries );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Cleans simulation info of each entry beginning with iWord.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrCleanSimInfo( Vec_Ptr_t * vInfo, int iWord, int nWords )
+{
+    int i;
+    for ( i = 0; i < vInfo->nSize; i++ )
+        memset( (char*)Vec_PtrEntry(vInfo,i) + 4*iWord, 0, 4*(nWords-iWord) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resizes the array of simulation info.]
+
+  Description [Doubles the number of objects for which siminfo is allocated.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrDoubleSimInfo( Vec_Ptr_t * vInfo )
+{
+    Vec_Ptr_t * vInfoNew;
+    int nWords;
+    assert( Vec_PtrSize(vInfo) > 1 );
+    // get the new array
+    nWords = (unsigned *)Vec_PtrEntry(vInfo,1) - (unsigned *)Vec_PtrEntry(vInfo,0);
+    vInfoNew = Vec_PtrAllocSimInfo( 2*Vec_PtrSize(vInfo), nWords );
+    // copy the simulation info
+    memcpy( Vec_PtrEntry(vInfoNew,0), Vec_PtrEntry(vInfo,0), Vec_PtrSize(vInfo) * nWords * 4 );
+    // replace the array
+    free( vInfo->pArray );
+    vInfo->pArray = vInfoNew->pArray;
+    vInfo->nSize *= 2;
+    vInfo->nCap *= 2;
+    // free the old array
+    vInfoNew->pArray = NULL;
+    free( vInfoNew );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resizes the array of simulation info.]
+
+  Description [Doubles the number of simulation patterns stored for each object.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrReallocSimInfo( Vec_Ptr_t * vInfo )
+{
+    Vec_Ptr_t * vInfoNew;
+    int nWords, i;
+    assert( Vec_PtrSize(vInfo) > 1 );
+    // get the new array
+    nWords = (unsigned *)Vec_PtrEntry(vInfo,1) - (unsigned *)Vec_PtrEntry(vInfo,0);
+    vInfoNew = Vec_PtrAllocSimInfo( Vec_PtrSize(vInfo), 2*nWords );
+    // copy the simulation info
+    for ( i = 0; i < vInfo->nSize; i++ )
+        memcpy( Vec_PtrEntry(vInfoNew,i), Vec_PtrEntry(vInfo,i), nWords * 4 );
+    // replace the array
+    free( vInfo->pArray );
+    vInfo->pArray = vInfoNew->pArray;
+    // free the old array
+    vInfoNew->pArray = NULL;
+    free( vInfoNew );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the array of truth tables for the given number of vars.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Ptr_t * Vec_PtrAllocTruthTables( int nVars )
+{
+    Vec_Ptr_t * p;
+    unsigned Masks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
+    unsigned * pTruth;
+    int i, k, nWords;
+    nWords = (nVars <= 5 ? 1 : (1 << (nVars - 5)));
+    p = Vec_PtrAllocSimInfo( nVars, nWords );
+    for ( i = 0; i < nVars; i++ )
+    {
+        pTruth = (unsigned *)p->pArray[i];
+        if ( i < 5 )
+        {
+            for ( k = 0; k < nWords; k++ )
+                pTruth[k] = Masks[i];
+        }
+        else
+        {
+            for ( k = 0; k < nWords; k++ )
+                if ( k & (1 << (i-5)) )
+                    pTruth[k] = ~(unsigned)0;
+                else
+                    pTruth[k] = 0;
+        }
+    }
+    return p;
+}
+
 #endif