Variable timeframe abstraction.

3 files changed, 332 insertions, 54 deletions

diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 6f87f348..e3baeb7b 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -52,7 +52,7 @@ struct Vta_Man_t_
     int           nObjsAlloc;   // the number of objects allocated
     int           nBins;        // number of hash table entries
     int *         pBins;        // hash table bins
-    Vta_Obj_t *   pObjs;        // hash table bins
+    Vta_Obj_t *   pObjs;        // storage for objects
     Vec_Int_t *   vOrder;       // objects in DPS order
     // abstraction
     int           nObjBits;     // the number of bits to represent objects
@@ -66,6 +66,7 @@ struct Vta_Man_t_
     Vec_Int_t *   vCla2Var;     // map clauses into variables
     Vec_Ptr_t *   vCores;       // unsat core for each frame
     sat_solver2 * pSat;         // incremental SAT solver
+    int           iPivot;
 };
 
 
@@ -77,11 +78,19 @@ struct Vta_Man_t_
 
 static inline int Vta_ValIs0( Vta_Obj_t * pThis, int fCompl )
 {
-    return (pThis->Value == VTA_VAR0 && !fCompl) || (pThis->Value == VTA_VAR1 && fCompl);
+    if ( pThis->Value == VTA_VAR1 && fCompl )
+        return 1;
+    if ( pThis->Value == VTA_VAR0 && !fCompl )
+        return 1;
+    return 0;
 }
 static inline int Vta_ValIs1( Vta_Obj_t * pThis, int fCompl )
 {
-    return (pThis->Value == VTA_VAR1 && !fCompl) || (pThis->Value == VTA_VAR0 && fCompl);
+    if ( pThis->Value == VTA_VAR0 && fCompl )
+        return 1;
+    if ( pThis->Value == VTA_VAR1 && !fCompl )
+        return 1;
+    return 0;
 }
 
 static inline Vta_Obj_t *  Vta_ManObj( Vta_Man_t * p, int i )           { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL;                     }
@@ -89,20 +98,21 @@ static inline int          Vta_ObjId( Vta_Man_t * p, Vta_Obj_t * pObj ) { assert
 
 #define Vta_ManForEachObj( p, pObj, i )                                 \
     for ( i = 1; (i < p->nObjs) && ((pObj) = Vta_ManObj(p, i)); i++ )
+#define Vta_ManForEachObjObj( p, pObjVta, pObjGia, i )                  \
+    for ( i = 1; (i < p->nObjs) && ((pObjVta) = Vta_ManObj(p, i)) && ((pObjGia) = Gia_ManObj(p->pGia, pObjVta->iObj)); i++ )
+#define Vta_ManForEachObjObjReverse( p, pObjVta, pObjGia, i )           \
+    for ( i = Vec_IntSize(vVec) - 1; (i >= 1) && ((pObjVta) = Vta_ManObj(p, i)) && ((pObjGia) = Gia_ManObj(p->pGia, pObjVta->iObj)); i++ )
+
 #define Vta_ManForEachObjVec( vVec, p, pObj, i )                        \
     for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))); i++ )
 #define Vta_ManForEachObjVecReverse( vVec, p, pObj, i )                 \
-    for ( i = Vec_IntSize(vVec) - 1; (i >= 1) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))); i-- )
+    for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))); i-- )
 
 #define Vta_ManForEachObjObjVec( vVec, p, pObj, pObjG, i )              \
     for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))) && ((pObjG) = Gia_ManObj(p->pGia, pObj->iObj)); i++ )
 #define Vta_ManForEachObjObjVecReverse( vVec, p, pObj, pObjG, i )       \
-    for ( i = Vec_IntSize(vVec) - 1; (i >= 1) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))) && ((pObjG) = Gia_ManObj(p->pGia, pObj->iObj)); i-- )
+    for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))) && ((pObjG) = Gia_ManObj(p->pGia, pObj->iObj)); i-- )
 
-#define Vta_ManForEachObjObj( p, pObjVta, pObjGia, i )                  \
-    for ( i = 1; (i < p->nObjs) && ((pObjVta) = Vta_ManObj(p, i)) && ((pObjGia) = Gia_ManObj(p->pGia, pObjVta->iObj)); i++ )
-#define Vta_ManForEachObjObjReverse( p, pObjVta, pObjGia, i )           \
-    for ( i = Vec_IntSize(vVec) - 1; (i >= 1) && ((pObjVta) = Vta_ManObj(p, i)) && ((pObjGia) = Gia_ManObj(p->pGia, pObjVta->iObj)); i++ )
 
 // abstraction is given as an array of integers:
 // - the first entry is the number of timeframes (F)
@@ -129,14 +139,15 @@ extern void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame );
 ***********************************************************************/
 void Gia_VtaSetDefaultParams( Gia_ParVta_t * p )
 {
-    int size = sizeof(Gia_ParVta_t);
     memset( p, 0, sizeof(Gia_ParVta_t) );
-    p->nFramesStart  =   10;  // the number of starting frames
-    p->nFramesMax    =    0;  // the max number of frames
-//    p->nFramesOver   =    4;  // the number of overlapping frames
-    p->nConfLimit    =    0;  // conflict limit
-    p->nTimeOut      =   60;  // timeout in seconds
-    p->fVerbose      =    1;  // verbosity flag
+    p->nFramesStart  =    5;   // starting frame 
+    p->nFramesMax    =   10;   // maximum frames
+    p->nFramesOver   =    3;   // overlap frames
+    p->nConfLimit    =    0;   // conflict limit
+    p->nTimeOut      =   60;   // timeout in seconds
+    p->fUseTermVars  =    0;   // use terminal variables
+    p->fVerbose      =    1;   // verbose flag
+    p->iFrame        =   -1;   // the number of frames covered 
 }
 
 /**Function*************************************************************
@@ -535,7 +546,7 @@ void Vta_ManCollectNodes_rec( Vta_Man_t * p, Vta_Obj_t * pThis, Vec_Int_t * vOrd
 {
     Gia_Obj_t * pObj;
     Vta_Obj_t * pThis0, * pThis1;
-    if ( !pThis->fVisit )
+    if ( pThis->fVisit )
         return;
     pThis->fVisit = 1;
     pObj = Gia_ManObj( p->pGia, pThis->iObj );
@@ -569,6 +580,54 @@ Vec_Int_t * Vta_ManCollectNodes( Vta_Man_t * p, int f )
   SeeAlso     []
 
 ***********************************************************************/
+void Vta_ManSatVerify( Vta_Man_t * p )
+{
+    Vta_Obj_t * pThis, * pThis0, * pThis1;
+    Gia_Obj_t * pObj;
+    int i;
+    Vta_ManForEachObj( p, pThis, i )
+        pThis->Value = (sat_solver2_var_value(p->pSat, i) ? VTA_VAR1 : VTA_VAR0);
+    Vta_ManForEachObjObj( p, pThis, pObj, i )
+    {
+        if ( !pThis->fAdded )
+            continue;
+        Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
+        if ( Gia_ObjIsAnd(pObj) )
+        {
+            int iVar  = Vta_ObjId(p, pThis);
+            int iVar0 = Vta_ObjId(p, pThis0);
+            int iVar1 = Vta_ObjId(p, pThis1);
+            if ( pThis->Value == VTA_VAR1 )
+                assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) );
+            else if ( pThis->Value == VTA_VAR0 )
+                assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) || Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) );
+            else assert( 0 );
+        }
+        else if ( Gia_ObjIsRo(p->pGia, pObj) )
+        {
+            pObj = Gia_ObjRoToRi( p->pGia, pObj );
+            if ( pThis->iFrame == 0 )
+                assert( pThis->Value == VTA_VAR0 );
+            else if ( pThis->Value == VTA_VAR0 )
+                assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) );
+            else if ( pThis->Value == VTA_VAR1 )
+                assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) );
+            else assert( 0 );
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Refines abstraction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
 {
     Abc_Cex_t * pCex = NULL;
@@ -578,17 +637,46 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
     Gia_Obj_t * pObj;
     int i, Counter;
 
+    Vta_ManSatVerify( p );
+
     // collect nodes in a topological order
     vOrder = Vta_ManCollectNodes( p, f );
     Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
     {
         pThis->Prio = VTA_LARGE;
-        pThis->Value = sat_solver2_var_value(p->pSat, i) ? VTA_VAR1 : VTA_VAR0;
+        pThis->Value = sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0;
         pThis->fVisit = 0;
     }
 
+    // verify
+    Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
+    {
+        if ( !pThis->fAdded )
+            continue;
+        Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
+        if ( Gia_ObjIsAnd(pObj) )
+        {
+            if ( pThis->Value == VTA_VAR1 )
+                assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) );
+            else if ( pThis->Value == VTA_VAR0 )
+                assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) || Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) );
+            else assert( 0 );
+        }
+        else if ( Gia_ObjIsRo(p->pGia, pObj) )
+        {
+            pObj = Gia_ObjRoToRi( p->pGia, pObj );
+            if ( pThis->iFrame == 0 )
+                assert( pThis->Value == VTA_VAR0 );
+            else if ( pThis->Value == VTA_VAR0 )
+                assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) );
+            else if ( pThis->Value == VTA_VAR1 )
+                assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) );
+            else assert( 0 );
+        }
+    }
+
     // compute distance in reverse order
-    pThis = Vta_ManObj( p, p->nObjs - 1 );
+    pThis = Vta_ManObj( p, Vec_IntEntryLast(vOrder) );
     pThis->Prio  = 1;
     // collect used and unused terms
     vTermsUsed   = Vec_PtrAlloc( 1015 );
@@ -638,6 +726,8 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
         pThis->Prio = Counter++;
     Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUnused, pThis, i )
         pThis->Prio = Counter++;
+//    printf( "Used %d  Unused %d\n", Vec_PtrSize(vTermsUsed), Vec_PtrSize(vTermsUnused) );
+
     Vec_PtrFree( vTermsUsed );
     Vec_PtrFree( vTermsUnused );
 
@@ -653,7 +743,6 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
         // assumes that values are assigned!!!
         assert( pThis->Value != 0 );
         // propagate
-        assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
         if ( Gia_ObjIsAnd(pObj) )
         {
             pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
@@ -688,12 +777,17 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
             else
                 pThis->Prio = 0;
         }
+        else if ( Gia_ObjIsConst0(pObj) )
+            pThis->Prio = 0;
+        else
+            assert( 0 );
     }
 
     // select important values
-    pTop = Vta_ManObj( p, Vec_IntEntryLast(p->vOrder) );
+    pTop = Vta_ManObj( p, Vec_IntEntryLast(vOrder) );
     pTop->fVisit = 1;
     vTermsToAdd = Vec_IntAlloc( 100 );
+    printf( "\n\n" );
     Vta_ManForEachObjObjVecReverse( vOrder, p, pThis, pObj, i )
     {
         if ( !pThis->fVisit )
@@ -703,13 +797,13 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
         // skip terminal objects
         if ( !pThis->fAdded )
         {
+            assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsConst0(pObj) || Gia_ObjIsPi(p->pGia, pObj) );
             Vec_IntPush( vTermsToAdd, Vta_ObjId(p, pThis) );
             continue;
         }
         // assumes that values are assigned!!!
         assert( pThis->Value != 0 );
         // propagate
-        assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
         if ( Gia_ObjIsAnd(pObj) )
         {
             pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
@@ -722,31 +816,45 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
                 assert( pThis1->Prio <= pThis->Prio );
                 pThis0->fVisit = 1;
                 pThis1->fVisit = 1;
+
+//                printf( "And1 %d requires %d %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis0), Vta_ObjId(p,pThis1) );
             }
             else if ( pThis->Value == VTA_VAR0 )
             {
                 if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
                 {
-                    if ( pThis0->Prio <= pThis1->Prio ) // choice!!!
+                    if ( pThis0->fVisit )
+                    {
+//                printf( "And0 %d requires %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis0) );
+                    }
+                    else if ( pThis1->fVisit )
+                    {
+//                printf( "And0 %d requires %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis1) );
+                    }
+                    else if ( pThis0->Prio <= pThis1->Prio ) // choice!!!
                     {
                         pThis0->fVisit = 1;
                         assert( pThis0->Prio == pThis->Prio );
+//                printf( "And0 %d requires %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis0) );
                     }
                     else
                     {
                         pThis1->fVisit = 1;
                         assert( pThis1->Prio == pThis->Prio );
+//                printf( "And0 %d requires %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis1) );
                     }
                 }
                 else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) )
                 {
                     pThis0->fVisit = 1;
                     assert( pThis0->Prio == pThis->Prio );
+//                printf( "And0 %d requires %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis0) );
                 }
                 else if ( Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
                 {
                     pThis1->fVisit = 1;
                     assert( pThis1->Prio == pThis->Prio );
+//                printf( "And0 %d requires %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis1) );
                 }
                 else assert( 0 );
             }
@@ -761,15 +869,17 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
                 assert( pThis0 );
                 pThis0->fVisit = 1;
                 assert( pThis0->Prio == pThis->Prio );
+//                printf( "Reg %d requires %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis0) );
             }
         }
-        else assert( 0 );
+        else if ( !Gia_ObjIsConst0(pObj) )
+            assert( 0 );
     }
+//printf( "\n" );
 
     // verify
-    Vta_ManForEachObjVec( p->vOrder, p, pThis, i )
-        if ( !pThis->fAdded )
-            pThis->Value = VTA_VARX;
+    Vta_ManForEachObjVec( vOrder, p, pThis, i )
+        pThis->Value = VTA_VARX;
     Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
     {
         assert( !pThis->fAdded );
@@ -786,6 +896,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
             pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
             pThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
             assert( pThis0 && pThis1 );
+//            printf( "AND %d  %d %d  ", Vta_ObjId(p, pThis), Vta_ObjId(p,pThis0), Vta_ObjId(p,pThis1) );
             if ( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) )
                 pThis->Value = VTA_VAR1;
             else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) || Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
@@ -806,17 +917,30 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
                     pThis->Value = VTA_VAR1;
                 else
                     pThis->Value = VTA_VARX;
+//            printf( "RO %d  ", Vta_ObjId(p, pThis), Vta_ObjId(p,pThis0) );
             }
             else
+            {
+//            printf( "RO %d frame0  ", Vta_ObjId(p, pThis) );
                 pThis->Value = VTA_VAR0;
+            }
+        }
+        else if ( Gia_ObjIsConst0(pObj) )
+        {
+//            printf( "CONST0 %d  ", Vta_ObjId(p, pThis) );
+            pThis->Value = VTA_VAR0;
         }
+        else assert( 0 );
+//        printf( "val = %d. \n", (pThis->Value==VTA_VAR0) ? 0 : ((pThis->Value==VTA_VAR0) ? 1 : 2 ) );
         // double check the solver
         assert( pThis->Value == VTA_VARX || (int)pThis->Value == (sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0) );
     }
 
     // check the output
-    if ( pTop->Value != VTA_VAR1 )
+    if ( !Vta_ValIs1(pTop, Gia_ObjFaninC0(Gia_ManPo(p->pGia, 0))) )
         printf( "Vta_ManRefineAbstraction(): Terminary simulation verification failed!\n" );
+    else
+        printf( "Verification OK.\n" );
 
     // produce true counter-example
     if ( pTop->Prio == 0 )
@@ -840,8 +964,9 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
     // perform refinement
     else
     {
-        Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
-            Vga_ManAddClausesOne( p, pThis->iObj, pThis->iFrame );
+        Vta_ManForEachObjObjVec( vTermsToAdd, p, pThis, pObj, i )
+            if ( !Gia_ObjIsPi(p->pGia, pObj) )
+                Vga_ManAddClausesOne( p, pThis->iObj, pThis->iFrame );
     }
     Vec_IntFree( vTermsToAdd );
     return pCex;
@@ -901,6 +1026,7 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
     p->vCla2Var    = Vec_IntAlloc( 1000 );
     p->vCores      = Vec_PtrAlloc( 100 );
     p->pSat        = sat_solver2_new();
+    p->iPivot      = Gia_ObjFaninId0p(p->pGia, Gia_ManPo(p->pGia, 0));
     return p;
 }
 
@@ -952,10 +1078,10 @@ Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat
     int nConfPrev = pSat->stats.conflicts;
     if ( piRetValue )
         *piRetValue = 1;
-    if ( pnConfls )
-        *pnConfls = 0;
     // solve the problem
     RetValue = sat_solver2_solve( pSat, &iLit, &iLit+1, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+    if ( pnConfls )
+        *pnConfls = (int)pSat->stats.conflicts - nConfPrev;
     if ( RetValue == l_Undef )
     {
         if ( piRetValue )
@@ -968,8 +1094,6 @@ Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat
             *piRetValue = 0;
         return NULL;
     }
-    if ( pnConfls )
-        *pnConfls = (int)pSat->stats.conflicts - nConfPrev;
     if ( fVerbose )
     {
 //        printf( "%6d", (int)pSat->stats.conflicts - nConfPrev );
@@ -1081,8 +1205,21 @@ void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame )
     Vta_Obj_t * pThis = Vga_ManFindOrAdd( p, iObj, iFrame );
     int iMainVar = Vta_ObjId(p, pThis);
     assert( pThis->iObj == iObj && pThis->iFrame == iFrame );
+
+    if ( iObj == 317 && iFrame == 0 )
+    {
+        int s = 0;
+    }
     if ( pThis->fAdded )
+    {
+//        if ( p->iPivot == iObj )
+//            printf( "Pivot in frame %d is already added\n", iFrame );
         return;
+    }
+//    if ( p->iPivot == iObj )
+//        printf( "Adding pivot in frame %d\n", iFrame );
+//    printf( "(%d,%d) ", iObj, iFrame );
+
     pThis->fAdded = 1;
     if ( Gia_ObjIsAnd(pObj) )
     {
@@ -1148,6 +1285,7 @@ void Vga_ManLoadSlice( Vta_Man_t * p, Vec_Int_t * vOne, int Lift )
     int i, Entry;
     Vec_IntForEachEntry( vOne, Entry, i )
         Vga_ManAddClausesOne( p, Entry & p->nObjMask, (Entry >> p->nObjBits) + Lift );
+    printf( "\n\n" );
 }
 
 /**Function*************************************************************
@@ -1169,6 +1307,49 @@ static inline int Vga_ManGetOutLit( Vta_Man_t * p, int f )
     return Abc_Var2Lit( Vta_ObjId(p, pThis), Gia_ObjFaninC0(pObj) );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Vga_ManPrintCore( Vta_Man_t * p, Vec_Int_t * vCore, int Lift )
+{
+    int i, Entry, iObj, iFrame;
+    Vec_IntForEachEntry( vCore, Entry, i )
+    {
+        iObj   = (Entry &  p->nObjMask);
+        iFrame = (Entry >> p->nObjBits);
+        printf( "%d*%d ", iObj, iFrame+Lift );
+    }
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Vga_ManRollBack( Vta_Man_t * p, int nObjOld )
+{
+    Vta_Obj_t * pThis  = p->pObjs + nObjOld;
+    Vta_Obj_t * pLimit = p->pObjs + p->nObjs;
+    for ( ; pThis < pLimit; pThis++ )
+        Vga_ManDelete( p, pThis->iObj, pThis->iFrame );
+    memset( p->pObjs + nObjOld, 0, sizeof(Vta_Obj_t) * (p->nObjs - nObjOld) );
+    p->nObjs = nObjOld;
+}
 
 /**Function*************************************************************
 
@@ -1208,34 +1389,54 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
         if ( f < p->pPars->nFramesStart )
             Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vFrames, f), 0 );
         else
+//        for ( f = 0; f < p->pPars->nFramesStart; f++ )
+//            Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vFrames, f), 0 );
         {
             // create bookmark to be used for rollback
+            int nObjOld;
+            int nClaOld;
+//start:            
+            nObjOld = p->nObjs;
+            nClaOld = Vec_IntSize(p->vCla2Var);
             sat_solver2_bookmark( p->pSat );
             // load the time frame
-            for ( i = 1; i <= Abc_MinInt(4, p->pPars->nFramesStart); i++ )
+            for ( i = 1; i <= Abc_MinInt(p->pPars->nFramesOver, p->pPars->nFramesStart); i++ )
+            {
                 Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vCores, f-i), i );
+//Vga_ManPrintCore( p, (Vec_Int_t *)Vec_PtrEntry(p->vCores, f-i), i );
+            }
             // iterate as long as there are counter-examples
-            while ( 1 )
+            for ( i = 1; ; i++ )
             {
-                vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, NULL );
+                vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
                 assert( (vCore != NULL) == (Status == 1) );
                 if ( Status == -1 ) // resource limit is reached
                     goto finish;
                 if ( vCore != NULL )
                     break;
+                printf( "Frame %d  iter %d...\n", f, i );
                 assert( Status == 0 );
                 pCex = Vta_ManRefineAbstraction( p, f );
-                goto finish;
+                if ( pCex != NULL )
+                    goto finish;
             }
             assert( Status == 1 );
+/*
             // valid core is obtained
             Vta_ManUnsatCoreRemap( p, vCore );
-            Vec_IntSort( vCore, 0 );
+printf( "Double checked core...\n" );
+Vga_ManPrintCore( p, vCore, 0 );
+//            Vec_IntSort( vCore, 0 );
             // update the SAT solver
             sat_solver2_rollback( p->pSat );
+            // update storage
+            Vga_ManRollBack( p, nObjOld );
+            Vec_IntShrink( p->vCla2Var, nClaOld );
             // load this timeframe
             Vga_ManLoadSlice( p, vCore, 0 );
+*/
             Vec_IntFree( vCore );
+//            goto start;
         }
         // run SAT solver
         vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls );
@@ -1252,13 +1453,20 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
         }
         // add the core
         Vta_ManUnsatCoreRemap( p, vCore );
+
+        if ( f >= p->pPars->nFramesStart )
+        {
+//            printf( "Core to record:\n" );
+//            Vga_ManPrintCore( p, vCore, 0 );
+        }
+
         // add in direct topological order
-        Vec_IntSort( vCore, 0 );
+//        Vec_IntSort( vCore, 1 );
         Vec_PtrPush( p->vCores, vCore );
         // print the result
         Vta_ManAbsPrintFrame( p, vCore, f+1, p->pPars->fVerbose );
-        if ( f == p->pPars->nFramesStart-1 )
-           break;
+//        if ( f == p->pPars->nFramesStart-1 )
+//           break;
     }
 finish:
     // analize the results
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 5d8d06f5..cee1b439 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -26404,7 +26404,7 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    Gia_ParVta_t Pars, Pars2, * pPars = &Pars;
+    Gia_ParVta_t Pars, * pPars = &Pars;
     int c;
     Gia_VtaSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
@@ -26483,7 +26483,7 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "The network is more than one PO (run \"orpos\").\n" );
         return 0;
     }
-    if ( pPars->nFramesMax > 0 )
+    if ( pPars->nFramesMax < 0 )
     {
         Abc_Print( 1, "The number of starting frames should be a positive integer.\n" );
         return 0;
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index f2215fea..1cc56fa9 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -141,7 +141,7 @@ static inline satset* clause_read   (sat_solver2* s, cla h)      { return (h & 1
 static inline cla     clause_handle (sat_solver2* s, satset* c)  { return c->learnt ? (satset_handle(&s->learnts, c)<<1)|1: satset_handle(&s->clauses, c)<<1;  }
 static inline int     clause_check  (sat_solver2* s, satset* c)  { return c->learnt ? satset_check(&s->learnts, c)  : satset_check(&s->clauses, c);            }
 static inline int     clause_proofid(sat_solver2* s, satset* c, int partA)  { return c->learnt ? (veci_begin(&s->claProofs)[c->Id]<<2) | (partA<<1) : (satset_handle(&s->clauses, c)<<2) | (partA<<1) | 1; }
-static inline int     clause_is_used(sat_solver2* s, cla h)      { return (h & 1) ? (h >> 1) < s->hLearntPivot : (h >> 1) < s->hClausePivot;                   }
+static inline int     clause_is_used(sat_solver2* s, cla h)      { return (h & 1) ? ((h >> 1) < s->hLearntPivot) : ((h >> 1) < s->hClausePivot);               }
 
 //static inline int     var_reason    (sat_solver2* s, int v)      { return (s->reasons[v]&1) ? 0 : s->reasons[v] >> 1;                   } 
 //static inline int     lit_reason    (sat_solver2* s, int l)      { return (s->reasons[lit_var(l)&1]) ? 0 : s->reasons[lit_var(l)] >> 1; } 
@@ -150,8 +150,8 @@ static inline int     clause_is_used(sat_solver2* s, cla h)      { return (h & 1
 static inline int     var_reason    (sat_solver2* s, int v)            { return s->reasons[v];           } 
 static inline int     lit_reason    (sat_solver2* s, int l)            { return s->reasons[lit_var(l)];  } 
 static inline satset* var_unit_clause(sat_solver2* s, int v)           { return clause_read(s, s->units[v]);                                          } 
-//static inline void    var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size && !s->units[v]); s->units[v] = i; s->nUnits++; } 
-static inline void    var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size); s->units[v] = i; s->nUnits++; } 
+static inline void    var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size && !s->units[v]); s->units[v] = i; s->nUnits++; } 
+//static inline void    var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size); s->units[v] = i; s->nUnits++; } 
 
 // these two only work after creating a clause before the solver is called
 int    clause_is_partA (sat_solver2* s, int h)                   { return clause_read(s, h)->partA;         }  
@@ -501,8 +501,12 @@ static void solver2_canceluntil(sat_solver2* s, int level) {
     for (c = s->qtail-1; c >= bound; c--) 
     {
         x = lit_var(trail[c]);
-        var_set_value(s, x, varX);
         s->reasons[x] = 0;
+//        if ( s->units[x] == 0 || var_level(s, x) > 0 )
+        {
+            var_set_value(s, x, varX);
+            s->units[x] = 0; // temporary?
+        }
         if ( c < lastLev )
             var_set_polar(s, x, !lit_sign(trail[c]));
     }
@@ -1551,7 +1555,7 @@ void sat_solver2_rollback( sat_solver2* s )
 {
     int i, k, j;
     assert( s->hClausePivot >= 1 && s->hClausePivot <= veci_size(&s->clauses) );
-    assert( s->hLearntPivot >= 1 && s->hLearntPivot <= veci_size(&s->clauses) );
+    assert( s->hLearntPivot >= 1 && s->hLearntPivot <= veci_size(&s->learnts) );
     assert( s->iVarPivot >= 0 && s->iVarPivot <= s->size );
     veci_resize(&s->order, 0);
     if ( s->hClausePivot > 1 || s->hLearntPivot > 1 )
@@ -1581,18 +1585,24 @@ void sat_solver2_rollback( sat_solver2* s )
                 s->units[i] = 0;
     }
     // reset
+    if ( s->hClausePivot < veci_size(&s->clauses) )
+    {
+        satset* first = satset_read(&s->clauses, s->hClausePivot);
+        s->stats.clauses = first->Id;
+        veci_resize(&s->clauses, s->hClausePivot);
+    }
     if ( s->hLearntPivot < veci_size(&s->learnts) )
     {
         satset* first = satset_read(&s->learnts, s->hLearntPivot);
-        veci_resize(&s->claActs,   first->Id);
+        veci_resize(&s->claActs,   first->Id+1);
         if ( s->fProofLogging ) {
-            veci_resize(&s->claProofs, first->Id);
+            veci_resize(&s->claProofs, first->Id+1);
             Sat_ProofReduce( s );
         }
+        s->stats.learnts = first->Id;
+        veci_resize(&s->learnts, s->hLearntPivot);
     }
-    veci_resize(&s->clauses, s->hClausePivot);
-    veci_resize(&s->learnts, s->hLearntPivot);
-    for ( i = s->iVarPivot; i < s->size*2; i++ )
+    for ( i = 2*s->iVarPivot; i < 2*s->size; i++ )
         s->wlists[i].size = 0;
     s->size = s->iVarPivot;
     // initialize other vars
@@ -1628,9 +1638,67 @@ void sat_solver2_rollback( sat_solver2* s )
         s->stats.learnts          = 0;
         s->stats.learnts_literals = 0;
         s->stats.tot_literals     = 0;
+        // initialize clause pointers
+        s->hClausePivot   =  1;
+        s->hLearntPivot   =  1;
+        s->hLearntLast    = -1; // the last learnt clause 
     }
 }
 
+// find the clause in the watcher lists
+int sat_solver2_find_clause( sat_solver2* s, int Hand, int fVerbose )
+{
+    int i, k, Found = 0;
+    if ( Hand >= s->clauses.size )
+        return 1;
+    for ( i = 0; i < s->size*2; i++ )
+    {
+        cla* pArray = veci_begin(&s->wlists[i]);
+        for ( k = 0; k < veci_size(&s->wlists[i]); k++ )
+            if ( (pArray[k] >> 1) == Hand )
+            {
+                if ( fVerbose )
+                printf( "Clause found in list %d.\n", k );
+                Found = 1;
+                break;
+            }
+    }
+    if ( Found == 0 )
+    {
+        if ( fVerbose )
+        printf( "Clause with hand %d is not found.\n", Hand );
+    }
+    return Found;
+}
+
+// verify that all clauses are satisfied
+void sat_solver2_verify( sat_solver2* s )
+{
+    satset * c;
+    int i, k, v, Counter = 0;
+    satset_foreach_entry( &s->clauses, c, i, 1 )
+    {
+        for ( k = 0; k < (int)c->nEnts; k++ )
+        {
+            v = lit_var(c->pEnts[k]);
+            if ( sat_solver2_var_value(s, v) ^ lit_sign(c->pEnts[k]) )
+                break;
+        }
+        if ( k == (int)c->nEnts )
+        {
+            printf( "Clause %d is not satisfied.   ", c->Id );
+            satset_print( c );
+            sat_solver2_find_clause( s, satset_handle(&s->clauses, c), 1 );
+            Counter++;
+        }
+    }
+    if ( Counter == 0 )
+        printf( "Verification passed.\n" );
+    else
+        printf( "Verification failed!\n" );
+}
+
+
 int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
 {
     int restart_iter = 0;
@@ -1798,6 +1866,8 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
         printf("==============================================================================\n");
 
     solver2_canceluntil(s,0);
+    if ( status == l_True )
+        sat_solver2_verify( s );
     return status;
 }