Improved timeout in the BDD reachability engines.

11 files changed, 195 insertions, 39 deletions

diff --git a/src/aig/llb/llb1Reach.c b/src/aig/llb/llb1Reach.c
index 443d2d81..32944bef 100644
--- a/src/aig/llb/llb1Reach.c
+++ b/src/aig/llb/llb1Reach.c
@@ -48,9 +48,10 @@ DdNode * Llb_ManConstructOutBdd( Aig_Man_t * pAig, Aig_Obj_t * pNode, DdManager
     DdNode * bBdd0, * bBdd1, * bFunc;
     Vec_Ptr_t * vNodes;
     Aig_Obj_t * pObj;
-    int i;
+    int i, TimeStop;
     if ( Aig_ObjFanin0(pNode) == Aig_ManConst1(pAig) )
         return Cudd_NotCond( Cudd_ReadOne(dd), Aig_ObjFaninC0(pNode) );
+    TimeStop = dd->TimeStop;  dd->TimeStop = 0;
     vNodes = Aig_ManDfsNodes( pAig, &pNode, 1 );
     assert( Vec_PtrSize(vNodes) > 0 );
     Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
@@ -72,6 +73,7 @@ DdNode * Llb_ManConstructOutBdd( Aig_Man_t * pAig, Aig_Obj_t * pNode, DdManager
     if ( Aig_ObjIsPo(pNode) )
         bFunc = Cudd_NotCond( bFunc, Aig_ObjFaninC0(pNode) );
     Cudd_Deref( bFunc );
+    dd->TimeStop = TimeStop;
     return bFunc;
 }
 
@@ -98,7 +100,8 @@ DdNode * Llb_ManConstructGroupBdd( Llb_Man_t * p, Llb_Grp_t * pGroup )
     {
         bBdd0 = Cudd_NotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
         bBdd1 = Cudd_NotCond( Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
-        pObj->pData = Extra_bddAndTime( p->dd, bBdd0, bBdd1, p->pPars->TimeTarget );  
+//        pObj->pData = Extra_bddAndTime( p->dd, bBdd0, bBdd1, p->pPars->TimeTarget );  
+        pObj->pData = Cudd_bddAnd( p->dd, bBdd0, bBdd1 );  
         if ( pObj->pData == NULL )
         {
             Vec_PtrForEachEntryStop( Aig_Obj_t *, pGroup->vNodes, pObj, k, i )
@@ -117,7 +120,8 @@ DdNode * Llb_ManConstructGroupBdd( Llb_Man_t * p, Llb_Grp_t * pGroup )
             bBdd0 = (DdNode *)pObj->pData;
         bBdd1 = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
         bXor  = Cudd_bddXor( p->dd, bBdd0, bBdd1 );                  Cudd_Ref( bXor );
-        bRes  = Extra_bddAndTime( p->dd, bTemp = bRes, Cudd_Not(bXor), p->pPars->TimeTarget );  
+//        bRes  = Extra_bddAndTime( p->dd, bTemp = bRes, Cudd_Not(bXor), p->pPars->TimeTarget );  
+        bRes  = Cudd_bddAnd( p->dd, bTemp = bRes, Cudd_Not(bXor) );  
         if ( bRes == NULL )
         {
             Cudd_RecursiveDeref( p->dd, bTemp );
@@ -153,6 +157,8 @@ DdNode * Llb_ManConstructQuantCubeIntern( Llb_Man_t * p, Llb_Grp_t * pGroup, int
     Aig_Obj_t * pObj;
     DdNode * bRes, * bTemp, * bVar;
     int i, iGroupFirst, iGroupLast;
+    int TimeStop;
+    TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
     bRes = Cudd_ReadOne( p->dd );   Cudd_Ref( bRes );
     Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
     {
@@ -177,6 +183,7 @@ DdNode * Llb_ManConstructQuantCubeIntern( Llb_Man_t * p, Llb_Grp_t * pGroup, int
         Cudd_RecursiveDeref( p->dd, bTemp );
     }
     Cudd_Deref( bRes );
+    p->dd->TimeStop = TimeStop;
     return bRes;
 }
 
@@ -195,7 +202,8 @@ DdNode * Llb_ManConstructQuantCube( Llb_Man_t * p, Llb_Grp_t * pGroup, int iGrpP
 {
     Aig_Obj_t * pObj;
     DdNode * bRes, * bTemp, * bVar;
-    int i, iGroupLast;
+    int i, iGroupLast, TimeStop;
+    TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
     bRes = Cudd_ReadOne( p->dd );   Cudd_Ref( bRes );
     Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
     {
@@ -218,6 +226,7 @@ DdNode * Llb_ManConstructQuantCube( Llb_Man_t * p, Llb_Grp_t * pGroup, int iGrpP
         Cudd_RecursiveDeref( p->dd, bTemp );
     }
     Cudd_Deref( bRes );
+    p->dd->TimeStop = TimeStop;
     return bRes;
 }
 
@@ -236,7 +245,8 @@ DdNode * Llb_ManComputeInitState( Llb_Man_t * p, DdManager * dd )
 {
     Aig_Obj_t * pObj;
     DdNode * bRes, * bVar, * bTemp;
-    int i, iVar;
+    int i, iVar, TimeStop;
+    TimeStop = dd->TimeStop; dd->TimeStop = 0;
     bRes = Cudd_ReadOne( dd );   Cudd_Ref( bRes );
     Saig_ManForEachLo( p->pAig, pObj, i )
     {
@@ -246,6 +256,7 @@ DdNode * Llb_ManComputeInitState( Llb_Man_t * p, DdManager * dd )
         Cudd_RecursiveDeref( dd, bTemp );
     }
     Cudd_Deref( bRes );
+    dd->TimeStop = TimeStop;
     return bRes;
 }
 
@@ -280,12 +291,20 @@ DdNode * Llb_ManComputeImage( Llb_Man_t * p, DdNode * bInit )
         Cudd_Ref( bGroup );
         // quantify variables appearing only in this group
         bCube  = Llb_ManConstructQuantCubeIntern( p, pGroup, i );               Cudd_Ref( bCube );
-        bGroup = Cudd_bddExistAbstract( p->dd, bTemp = bGroup, bCube );         Cudd_Ref( bGroup );
+        bGroup = Cudd_bddExistAbstract( p->dd, bTemp = bGroup, bCube );         
+        if ( bGroup == NULL )
+        {
+            Cudd_RecursiveDeref( p->dd, bTemp );
+            Cudd_RecursiveDeref( p->dd, bCube );
+            return NULL;
+        }
+        Cudd_Ref( bGroup );
         Cudd_RecursiveDeref( p->dd, bTemp );
         Cudd_RecursiveDeref( p->dd, bCube );
         // perform partial product
         bCube  = Llb_ManConstructQuantCube( p, pGroup, i );                     Cudd_Ref( bCube );
-        bImage = Extra_bddAndAbstractTime( p->dd, bTemp = bImage, bGroup, bCube, p->pPars->TimeTarget );   
+//        bImage = Extra_bddAndAbstractTime( p->dd, bTemp = bImage, bGroup, bCube, p->pPars->TimeTarget );   
+        bImage = Cudd_bddAndAbstract( p->dd, bTemp = bImage, bGroup, bCube );   
         if ( bImage == NULL )
         {
             Cudd_RecursiveDeref( p->dd, bTemp );
@@ -331,9 +350,10 @@ DdNode * Llb_ManCreateConstraints( Llb_Man_t * p, Vec_Int_t * vHints, int fUseNs
 {
     DdNode * bConstr, * bFunc, * bTemp;
     Aig_Obj_t * pObj;
-    int i, Entry;
+    int i, Entry, TimeStop;
     if ( vHints == NULL )
         return Cudd_ReadOne( p->dd );
+    TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
     assert( Aig_ManPiNum(p->pAig) == Aig_ManPiNum(p->pAigGlo) );
     // assign const and PI nodes to the original AIG
     Aig_ManCleanData( p->pAig );
@@ -367,6 +387,7 @@ DdNode * Llb_ManCreateConstraints( Llb_Man_t * p, Vec_Int_t * vHints, int fUseNs
         Cudd_RecursiveDeref( p->dd, bFunc );
     }
     Cudd_Deref( bConstr );
+    p->dd->TimeStop = TimeStop;
     return bConstr;
 }
 
@@ -558,7 +579,8 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
         // remap these states into the current state vars
 //        bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pNs2Glo );    Cudd_Ref( bNext );
 //        Cudd_RecursiveDeref( p->dd, bTemp );
-        bNext = Extra_TransferPermuteTime( p->dd, p->ddG, bTemp = bNext, pNs2Glo, p->pPars->TimeTarget );    
+//        bNext = Extra_TransferPermuteTime( p->dd, p->ddG, bTemp = bNext, pNs2Glo, p->pPars->TimeTarget );    
+        bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pNs2Glo );    
         if ( bNext == NULL )
         {
             if ( !p->pPars->fSilent )
@@ -590,7 +612,14 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
         }
 
         // get the new states
-        bCurrent = Cudd_bddAnd( p->ddG, bNext, Cudd_Not(bReached) );                    Cudd_Ref( bCurrent );
+        bCurrent = Cudd_bddAnd( p->ddG, bNext, Cudd_Not(bReached) );
+        if ( bCurrent == NULL )
+        {
+            Cudd_RecursiveDeref( p->ddG,  bNext );        bNext = NULL;
+            Cudd_RecursiveDeref( p->ddG,  bReached );     bReached = NULL;
+            break;
+        }
+        Cudd_Ref( bCurrent );
         // minimize the new states with the reached states
 //        bCurrent = Cudd_bddConstrain( p->ddG, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
 //        bCurrent = Cudd_bddRestrict( p->ddG, bTemp = bCurrent, Cudd_Not(bReached) );  Cudd_Ref( bCurrent );
@@ -600,7 +629,8 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
         // remap these states into the current state vars
 //        bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Cs );   Cudd_Ref( bCurrent );
 //        Cudd_RecursiveDeref( p->ddG, bTemp );
-        bCurrent = Extra_TransferPermuteTime( p->ddG, p->dd, bTemp = bCurrent, pGlo2Cs, p->pPars->TimeTarget );    
+//        bCurrent = Extra_TransferPermuteTime( p->ddG, p->dd, bTemp = bCurrent, pGlo2Cs, p->pPars->TimeTarget );    
+        bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Cs );    
         if ( bCurrent == NULL )
         {
             if ( !p->pPars->fSilent )
@@ -617,7 +647,14 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
         
 
         // add to the reached states
-        bReached = Cudd_bddOr( p->ddG, bTemp = bReached, bNext );                       Cudd_Ref( bReached );
+        bReached = Cudd_bddOr( p->ddG, bTemp = bReached, bNext );                       
+        if ( bReached == NULL )
+        {
+            Cudd_RecursiveDeref( p->ddG,  bTemp );     bTemp = NULL;
+            Cudd_RecursiveDeref( p->ddG,  bNext );     bNext = NULL;
+            break;
+        }
+        Cudd_Ref( bReached );
         Cudd_RecursiveDeref( p->ddG, bTemp );
         Cudd_RecursiveDeref( p->ddG, bNext );
         bNext = NULL;
diff --git a/src/aig/llb/llb2Bad.c b/src/aig/llb/llb2Bad.c
index 8e2a37ff..9aecb9ff 100644
--- a/src/aig/llb/llb2Bad.c
+++ b/src/aig/llb/llb2Bad.c
@@ -63,7 +63,8 @@ DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, int TimeOut )
             continue;
         bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
         bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
-        pObj->pData = Extra_bddAndTime( dd, bBdd0, bBdd1, TimeOut );
+//        pObj->pData = Extra_bddAndTime( dd, bBdd0, bBdd1, TimeOut );
+        pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 );
         if ( pObj->pData == NULL )
         {
             Vec_PtrForEachEntryStop( Aig_Obj_t *, vNodes, pObj, k, i )
@@ -109,8 +110,9 @@ DdNode * Llb_BddQuantifyPis( Aig_Man_t * pInit, DdManager * dd, DdNode * bFunc )
 {
     DdNode * bVar, * bCube, * bTemp;
     Aig_Obj_t * pObj;
-    int i;
+    int i, TimeStop;
     assert( Cudd_ReadSize(dd) == Aig_ManPiNum(pInit) );
+    TimeStop = dd->TimeStop; dd->TimeStop = 0;
     // create PI cube
     bCube = Cudd_ReadOne( dd );  Cudd_Ref( bCube );
     Saig_ManForEachPi( pInit, pObj, i )    {
@@ -122,6 +124,7 @@ DdNode * Llb_BddQuantifyPis( Aig_Man_t * pInit, DdManager * dd, DdNode * bFunc )
     bFunc = Cudd_bddExistAbstract( dd, bFunc, bCube );  Cudd_Ref( bFunc );
     Cudd_RecursiveDeref( dd, bCube );
     Cudd_Deref( bFunc );
+    dd->TimeStop = TimeStop;
     return bFunc;
 }
 
diff --git a/src/aig/llb/llb2Core.c b/src/aig/llb/llb2Core.c
index 4685db0e..446f1a67 100644
--- a/src/aig/llb/llb2Core.c
+++ b/src/aig/llb/llb2Core.c
@@ -68,7 +68,8 @@ struct Llb_Img_t_
 DdNode * Llb_CoreComputeCube( DdManager * dd, Vec_Int_t * vVars, int fUseVarIndex, char * pValues )
 {
     DdNode * bRes, * bVar, * bTemp;
-    int i, iVar, Index;
+    int i, iVar, Index, TimeStop;
+    TimeStop = dd->TimeStop; dd->TimeStop = 0;
     bRes = Cudd_ReadOne( dd );   Cudd_Ref( bRes );
     Vec_IntForEachEntry( vVars, Index, i )
     {
@@ -78,6 +79,7 @@ DdNode * Llb_CoreComputeCube( DdManager * dd, Vec_Int_t * vVars, int fUseVarInde
         Cudd_RecursiveDeref( dd, bTemp );
     }
     Cudd_Deref( bRes );
+    dd->TimeStop = TimeStop;
     return bRes;
 }
 
@@ -102,6 +104,9 @@ Abc_Cex_t * Llb_CoreDeriveCex( Llb_Img_t * p )
     char * pValues = ABC_ALLOC( char, Cudd_ReadSize(p->ddR) );
     assert( Vec_PtrSize(p->vRings) > 0 );
 
+    p->dd->TimeStop  = 0;
+    p->ddR->TimeStop = 0;
+
     // get supports and quantified variables
     Vec_PtrReverseOrder( p->vDdMans );
     vSupps = Llb_ImgSupports( p->pAig, p->vDdMans, p->vVarsNs, p->vVarsCs, 1, 0 );
@@ -244,7 +249,15 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
         bReached = Cudd_bddTransfer( p->ddR, p->ddG, bCurrent );                 Cudd_Ref( bReached );
         Cudd_RecursiveDeref( p->ddR, bCurrent );
         // move init state to the working manager
-        bCurrent = Extra_TransferPermute( p->ddG, p->dd, bReached, pGlo2Loc );   Cudd_Ref( bCurrent );
+        bCurrent = Extra_TransferPermute( p->ddG, p->dd, bReached, pGlo2Loc );   
+        if ( bCurrent == NULL )
+        {
+            Cudd_RecursiveDeref( p->ddG, bReached );
+            if ( !p->pPars->fSilent )
+                printf( "Reached timeout (%d seconds) during transfer 0.\n", p->pPars->TimeLimit );
+            return -1;
+        }
+        Cudd_Ref( bCurrent );
     }
     else
     {
@@ -282,7 +295,17 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
         }
 
         // save the onion ring
-        bTemp = Extra_TransferPermute( p->dd, p->ddR, bCurrent, pLoc2GloR );    Cudd_Ref( bTemp );
+        bTemp = Extra_TransferPermute( p->dd, p->ddR, bCurrent, pLoc2GloR );  
+        if ( bTemp == NULL )
+        {
+            if ( !p->pPars->fSilent )
+                printf( "Reached timeout (%d seconds) during image computation.\n",  p->pPars->TimeLimit );
+            p->pPars->iFrame = nIters - 1;
+            Cudd_RecursiveDeref( p->dd,  bCurrent );  bCurrent = NULL;
+            Cudd_RecursiveDeref( p->ddG, bReached );  bReached = NULL;
+            return -1;
+        }
+        Cudd_Ref( bTemp );
         Vec_PtrPush( p->vRings, bTemp );
 
         // check it for bad states
@@ -325,7 +348,8 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
 //        bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pLoc2Glo );    Cudd_Ref( bNext );
 //        Cudd_RecursiveDeref( p->dd, bTemp );
 
-        bNext = Extra_TransferPermuteTime( p->dd, p->ddG, bTemp = bNext, pLoc2Glo, p->pPars->TimeTarget );    
+//        bNext = Extra_TransferPermuteTime( p->dd, p->ddG, bTemp = bNext, pLoc2Glo, p->pPars->TimeTarget );    
+        bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pLoc2Glo );    
         if ( bNext == NULL )
         {
             if ( !p->pPars->fSilent )
@@ -347,13 +371,24 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
         }
 
         // get the new states
-        bCurrent = Cudd_bddAnd( p->ddG, bNext, Cudd_Not(bReached) );                    Cudd_Ref( bCurrent );
+        bCurrent = Cudd_bddAnd( p->ddG, bNext, Cudd_Not(bReached) );                    
+        if ( bCurrent == NULL )
+        {
+            if ( !p->pPars->fSilent )
+                printf( "Reached timeout (%d seconds) during image computation in transfer 2.\n",  p->pPars->TimeLimit );
+            p->pPars->iFrame = nIters - 1;
+            Cudd_RecursiveDeref( p->ddG, bNext );  
+            Cudd_RecursiveDeref( p->ddG, bReached );   bReached = NULL;
+            return -1;
+        }
+        Cudd_Ref( bCurrent );
 
         // remap these states into the current state vars
 //        bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Loc );   Cudd_Ref( bCurrent );
 //        Cudd_RecursiveDeref( p->ddG, bTemp );
 
-        bCurrent = Extra_TransferPermuteTime( p->ddG, p->dd, bTemp = bCurrent, pGlo2Loc, p->pPars->TimeTarget );    
+//        bCurrent = Extra_TransferPermuteTime( p->ddG, p->dd, bTemp = bCurrent, pGlo2Loc, p->pPars->TimeTarget );    
+        bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Loc );    
         if ( bCurrent == NULL )
         {
             if ( !p->pPars->fSilent )
diff --git a/src/aig/llb/llb2Driver.c b/src/aig/llb/llb2Driver.c
index aab65317..3b4f23fc 100644
--- a/src/aig/llb/llb2Driver.c
+++ b/src/aig/llb/llb2Driver.c
@@ -129,7 +129,8 @@ DdNode * Llb_DriverPhaseCube( Aig_Man_t * pAig, Vec_Int_t * vDriRefs, DdManager
 {
     DdNode * bCube, * bVar, * bTemp;
     Aig_Obj_t * pObj;
-    int i;
+    int i, TimeStop;
+    TimeStop = dd->TimeStop; dd->TimeStop = 0;
     bCube = Cudd_ReadOne( dd );  Cudd_Ref( bCube );
     Saig_ManForEachLi( pAig, pObj, i )
     {
@@ -143,6 +144,7 @@ DdNode * Llb_DriverPhaseCube( Aig_Man_t * pAig, Vec_Int_t * vDriRefs, DdManager
         Cudd_RecursiveDeref( dd, bTemp );
     }
     Cudd_Deref( bCube );
+    dd->TimeStop = TimeStop;
     return bCube;
 }
 
@@ -181,7 +183,8 @@ DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs, int Tim
         bVar2 = Cudd_NotCond( bVar2, Aig_ObjFaninC0(pObj) );
         bProd = Cudd_bddXnor( dd, bVar1, bVar2 );              Cudd_Ref( bProd );
 //        bRes  = Cudd_bddAnd( dd, bTemp = bRes, bProd );        Cudd_Ref( bRes );
-        bRes  = Extra_bddAndTime( dd, bTemp = bRes, bProd, TimeTarget );  
+//        bRes  = Extra_bddAndTime( dd, bTemp = bRes, bProd, TimeTarget );  
+        bRes  = Cudd_bddAnd( dd, bTemp = bRes, bProd );  
         if ( bRes == NULL )
         {
             Cudd_RecursiveDeref( dd, bTemp );
diff --git a/src/aig/llb/llb2Image.c b/src/aig/llb/llb2Image.c
index 78ff9da1..caf8f9f7 100644
--- a/src/aig/llb/llb2Image.c
+++ b/src/aig/llb/llb2Image.c
@@ -200,7 +200,8 @@ DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUp
         bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
         bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
 //        pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 );   Cudd_Ref( (DdNode *)pObj->pData );
-        pObj->pData = Extra_bddAndTime( dd, bBdd0, bBdd1, TimeTarget );  
+//        pObj->pData = Extra_bddAndTime( dd, bBdd0, bBdd1, TimeTarget );  
+        pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 );  
         if ( pObj->pData == NULL )
         {
             Cudd_Quit( dd );
@@ -217,7 +218,8 @@ DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUp
         assert( Aig_ObjIsNode(pObj) );
         bProd = Cudd_bddXnor( dd, Cudd_bddIthVar(dd, Aig_ObjId(pObj)), (DdNode *)pObj->pData );   Cudd_Ref( bProd );
 //        bRes  = Cudd_bddAnd( dd, bTemp = bRes, bProd ); Cudd_Ref( bRes );
-        bRes  = Extra_bddAndTime( dd, bTemp = bRes, bProd, TimeTarget );  
+//        bRes  = Extra_bddAndTime( dd, bTemp = bRes, bProd, TimeTarget );  
+        bRes  = Cudd_bddAnd( dd, bTemp = bRes, bProd );  
         if ( bRes == NULL )
         {
             Cudd_Quit( dd );
@@ -257,7 +259,8 @@ DdNode * Llb_ImgComputeCube( Aig_Man_t * pAig, Vec_Int_t * vNodeIds, DdManager *
 {
     DdNode * bProd, * bTemp;
     Aig_Obj_t * pObj;
-    int i;
+    int i, TimeStop;
+    TimeStop = dd->TimeStop; dd->TimeStop = 0;
     bProd = Cudd_ReadOne(dd);   Cudd_Ref( bProd );
     Aig_ManForEachNodeVec( pAig, vNodeIds, pObj, i )
     {
@@ -265,6 +268,7 @@ DdNode * Llb_ImgComputeCube( Aig_Man_t * pAig, Vec_Int_t * vNodeIds, DdManager *
         Cudd_RecursiveDeref( dd, bTemp );
     }
     Cudd_Deref( bProd );
+    dd->TimeStop = TimeStop;
     return bProd;
 } 
 
@@ -376,7 +380,14 @@ DdNode * Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, DdManager *
     {
         // quantify unique vriables
         bCube  = Llb_ImgComputeCube( pAig, (Vec_Int_t *)Vec_PtrEntry(vQuant0, 0), dd ); Cudd_Ref( bCube );
-        bImage = Cudd_bddExistAbstract( dd, bTemp = bImage, bCube );                    Cudd_Ref( bImage );
+        bImage = Cudd_bddExistAbstract( dd, bTemp = bImage, bCube );                    
+        if ( bImage == NULL )
+        {
+            Cudd_RecursiveDeref( dd, bTemp );
+            Cudd_RecursiveDeref( dd, bCube );
+            return NULL;
+        }
+        Cudd_Ref( bImage );
         Cudd_RecursiveDeref( dd, bTemp );
         Cudd_RecursiveDeref( dd, bCube );
     }
@@ -387,13 +398,17 @@ DdNode * Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, DdManager *
 if ( fVerbose )
 printf( "   %2d : ", i );
         // transfer the BDD from the group manager to the main manager
-        bGroup = Cudd_bddTransfer( ddPart, dd, ddPart->bFunc );                           Cudd_Ref( bGroup );
+        bGroup = Cudd_bddTransfer( ddPart, dd, ddPart->bFunc );                           
+        if ( bGroup == NULL )
+            return NULL;
+        Cudd_Ref( bGroup );
 if ( fVerbose )
 printf( "Pt0 =%6d. Pt1 =%6d. ", Cudd_DagSize(ddPart->bFunc), Cudd_DagSize(bGroup) );
         // perform partial product
         bCube  = Llb_ImgComputeCube( pAig, (Vec_Int_t *)Vec_PtrEntry(vQuant1, i+1), dd ); Cudd_Ref( bCube );
 //        bImage = Cudd_bddAndAbstract( dd, bTemp = bImage, bGroup, bCube );                
-        bImage = Extra_bddAndAbstractTime( dd, bTemp = bImage, bGroup, bCube, TimeTarget );  
+//        bImage = Extra_bddAndAbstractTime( dd, bTemp = bImage, bGroup, bCube, TimeTarget );  
+        bImage = Cudd_bddAndAbstract( dd, bTemp = bImage, bGroup, bCube );  
         if ( bImage == NULL )
         {
             Cudd_RecursiveDeref( dd, bTemp );
diff --git a/src/aig/llb/llb3Image.c b/src/aig/llb/llb3Image.c
index 9bb01195..2c16c550 100644
--- a/src/aig/llb/llb3Image.c
+++ b/src/aig/llb/llb3Image.c
@@ -141,7 +141,8 @@ DdNode * Llb_NonlinCreateCube1( Llb_Mgr_t * p, Llb_Prt_t * pPart )
 {
     DdNode * bCube, * bTemp;
     Llb_Var_t * pVar;
-    int i;
+    int i, TimeStop;
+    TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
     bCube = Cudd_ReadOne(p->dd);   Cudd_Ref( bCube );
     Llb_PartForEachVar( p, pPart, pVar, i )
     {
@@ -153,6 +154,7 @@ DdNode * Llb_NonlinCreateCube1( Llb_Mgr_t * p, Llb_Prt_t * pPart )
         Cudd_RecursiveDeref( p->dd, bTemp );
     }
     Cudd_Deref( bCube );
+    p->dd->TimeStop = TimeStop;
     return bCube;
 }
 
@@ -171,7 +173,8 @@ DdNode * Llb_NonlinCreateCube2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * p
 {
     DdNode * bCube, * bTemp;
     Llb_Var_t * pVar;
-    int i;
+    int i, TimeStop;
+    TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
     bCube = Cudd_ReadOne(p->dd);   Cudd_Ref( bCube );
     Llb_PartForEachVar( p, pPart1, pVar, i )
     {
@@ -186,6 +189,7 @@ DdNode * Llb_NonlinCreateCube2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * p
         }
     }
     Cudd_Deref( bCube );
+    p->dd->TimeStop = TimeStop;
     return bCube;
 }
 
@@ -376,7 +380,8 @@ Extra_bddPrintSupport( p->dd, bCube );  printf( "\n" );
     Cudd_Ref( bFunc );
 */
 
-    bFunc = Extra_bddAndAbstractTime( p->dd, pPart1->bFunc, pPart2->bFunc, bCube, TimeOut );  
+//    bFunc = Extra_bddAndAbstractTime( p->dd, pPart1->bFunc, pPart2->bFunc, bCube, TimeOut );  
+    bFunc = Cudd_bddAndAbstract( p->dd, pPart1->bFunc, pPart2->bFunc, bCube );  
     if ( bFunc == NULL )
     {
         Cudd_RecursiveDeref( p->dd, bCube );
@@ -549,7 +554,8 @@ Vec_Ptr_t * Llb_NonlinBuildBdds( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t *
     {
         bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
         bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
-        pObj->pData = Extra_bddAndTime( dd, bBdd0, bBdd1, TimeOut );
+//        pObj->pData = Extra_bddAndTime( dd, bBdd0, bBdd1, TimeOut );
+        pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 );
         if ( pObj->pData == NULL )
         {
             Vec_PtrForEachEntryStop( Aig_Obj_t *, vNodes, pObj, k, i )
@@ -907,7 +913,14 @@ DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRo
     bFunc = Cudd_ReadOne(p->dd);   Cudd_Ref( bFunc );
     Llb_MgrForEachPart( p, pPart, i )
     {
-        bFunc = Cudd_bddAnd( p->dd, bTemp = bFunc, pPart->bFunc );   Cudd_Ref( bFunc );
+        bFunc = Cudd_bddAnd( p->dd, bTemp = bFunc, pPart->bFunc );
+        if ( bFunc == NULL )
+        {
+            Cudd_RecursiveDeref( p->dd, bTemp );
+            Llb_NonlinFree( p );
+            return NULL;
+        }
+        Cudd_Ref( bFunc );
         Cudd_RecursiveDeref( p->dd, bTemp );
     }
     nSuppMax = p->nSuppMax;
diff --git a/src/aig/llb/llb3Nonlin.c b/src/aig/llb/llb3Nonlin.c
index 62ce441c..c10db9e3 100644
--- a/src/aig/llb/llb3Nonlin.c
+++ b/src/aig/llb/llb3Nonlin.c
@@ -210,7 +210,8 @@ DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd )
 {
     Aig_Obj_t * pObj;
     DdNode * bRes, * bVar, * bTemp;
-    int i, iVar;
+    int i, iVar, TimeStop;
+    TimeStop = dd->TimeStop;  dd->TimeStop = 0;
     bRes = Cudd_ReadOne( dd );   Cudd_Ref( bRes );
     Saig_ManForEachLo( pAig, pObj, i )
     {
@@ -220,6 +221,7 @@ DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd )
         Cudd_RecursiveDeref( dd, bTemp );
     }
     Cudd_Deref( bRes );
+    dd->TimeStop = TimeStop;
     return bRes;
 }
 
@@ -245,6 +247,9 @@ Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p )
     char * pValues = ABC_ALLOC( char, Cudd_ReadSize(p->ddR) );
     assert( Vec_PtrSize(p->vRings) > 0 );
 
+    p->dd->TimeStop  = 0;
+    p->ddR->TimeStop = 0;
+
     // update quantifiable vars
     memset( p->pVars2Q, 0, sizeof(int) * Cudd_ReadSize(p->dd) );
     vVarsNs = Vec_IntAlloc( Aig_ManRegNum(p->pAig) );
@@ -437,7 +442,16 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
         }
 
         // save the onion ring
-        bTemp = Extra_TransferPermute( p->dd, p->ddR, bCurrent, Vec_IntArray(p->vCs2Glo) );    Cudd_Ref( bTemp );
+        bTemp = Extra_TransferPermute( p->dd, p->ddR, bCurrent, Vec_IntArray(p->vCs2Glo) );
+        if ( bTemp == NULL )
+        {
+            if ( !p->pPars->fSilent )
+                printf( "Reached timeout (%d seconds) during ring transfer.\n",  p->pPars->TimeLimit );
+            p->pPars->iFrame = nIters - 1;
+            Cudd_RecursiveDeref( p->dd,  bCurrent );  bCurrent = NULL;
+            return -1;
+        }
+        Cudd_Ref( bTemp );
         Vec_PtrPush( p->vRings, bTemp );
 
         // check it for bad states
@@ -533,7 +547,8 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
         // transfer to the state manager
         clk3 = clock();
         Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc2 );
-        p->ddG->bFunc2 = Extra_TransferPermuteTime( p->dd, p->ddG, bNext, Vec_IntArray(p->vNs2Glo), p->pPars->TimeTarget );    
+//        p->ddG->bFunc2 = Extra_TransferPermuteTime( p->dd, p->ddG, bNext, Vec_IntArray(p->vNs2Glo), p->pPars->TimeTarget );    
+        p->ddG->bFunc2 = Extra_TransferPermute( p->dd, p->ddG, bNext, Vec_IntArray(p->vNs2Glo) );    
         if ( p->ddG->bFunc2 == NULL )
         {
             if ( !p->pPars->fSilent )
@@ -548,12 +563,30 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
 
         // derive new states
         clk3 = clock();
-        p->ddG->bFunc2 = Cudd_bddAnd( p->ddG, bTemp = p->ddG->bFunc2, Cudd_Not(p->ddG->bFunc) );     Cudd_Ref( p->ddG->bFunc2 );
+        p->ddG->bFunc2 = Cudd_bddAnd( p->ddG, bTemp = p->ddG->bFunc2, Cudd_Not(p->ddG->bFunc) );     
+        if ( p->ddG->bFunc2 == NULL )
+        {
+            if ( !p->pPars->fSilent )
+                printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n",  p->pPars->TimeLimit );
+            p->pPars->iFrame = nIters - 1;
+            Cudd_RecursiveDeref( p->ddG, bTemp );  
+            return -1;
+        }
+        Cudd_Ref( p->ddG->bFunc2 );
         Cudd_RecursiveDeref( p->ddG, bTemp );
         if ( Cudd_IsConstant(p->ddG->bFunc2) )
             break;
         // add to the reached set
-        p->ddG->bFunc = Cudd_bddOr( p->ddG, bTemp = p->ddG->bFunc, p->ddG->bFunc2 );                 Cudd_Ref( p->ddG->bFunc );
+        p->ddG->bFunc = Cudd_bddOr( p->ddG, bTemp = p->ddG->bFunc, p->ddG->bFunc2 );                 
+        if ( p->ddG->bFunc == NULL )
+        {
+            if ( !p->pPars->fSilent )
+                printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n",  p->pPars->TimeLimit );
+            p->pPars->iFrame = nIters - 1;
+            Cudd_RecursiveDeref( p->ddG, bTemp );  
+            return -1;
+        }
+        Cudd_Ref( p->ddG->bFunc );
         Cudd_RecursiveDeref( p->ddG, bTemp );
         p->timeGloba += clock() - clk3;
 
@@ -564,7 +597,8 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
 
         // move new states to the working manager
         clk3 = clock();
-        bCurrent = Extra_TransferPermuteTime( p->ddG, p->dd, p->ddG->bFunc2, Vec_IntArray(p->vGlo2Cs), p->pPars->TimeTarget ); 
+//        bCurrent = Extra_TransferPermuteTime( p->ddG, p->dd, p->ddG->bFunc2, Vec_IntArray(p->vGlo2Cs), p->pPars->TimeTarget ); 
+        bCurrent = Extra_TransferPermute( p->ddG, p->dd, p->ddG->bFunc2, Vec_IntArray(p->vGlo2Cs) ); 
         if ( bCurrent == NULL )
         {
             if ( !p->pPars->fSilent )
diff --git a/src/bdd/cudd/cuddAndAbs.c b/src/bdd/cudd/cuddAndAbs.c
index 39695918..2f38490d 100644
--- a/src/bdd/cudd/cuddAndAbs.c
+++ b/src/bdd/cudd/cuddAndAbs.c
@@ -259,6 +259,9 @@ cuddBddAndAbstractRecur(
         }
     }
 
+    if ( manager->TimeStop && manager->TimeStop < clock() )
+        return NULL;
+
     if (topf == top) {
         index = F->index;
         ft = cuddT(F);
diff --git a/src/bdd/cudd/cuddBddIte.c b/src/bdd/cudd/cuddBddIte.c
index 1b152f02..4e75aab2 100644
--- a/src/bdd/cudd/cuddBddIte.c
+++ b/src/bdd/cudd/cuddBddIte.c
@@ -926,6 +926,9 @@ cuddBddAndRecur(
         if (r != NULL) return(r);
     }
 
+    if ( manager->TimeStop && manager->TimeStop < clock() )
+        return NULL;
+
     /* Here we can skip the use of cuddI, because the operands are known
     ** to be non-constant.
     */
diff --git a/src/bdd/cudd/cuddBridge.c b/src/bdd/cudd/cuddBridge.c
index d0f96a2f..97a6f393 100644
--- a/src/bdd/cudd/cuddBridge.c
+++ b/src/bdd/cudd/cuddBridge.c
@@ -975,6 +975,11 @@ cuddBddTransferRecur(
     /* Check the cache. */
     if (st_lookup(table, (const char *)f, (char **)&res))
         return(Cudd_NotCond(res,comple));
+
+    if ( ddS->TimeStop && ddS->TimeStop < clock() )
+        return NULL;
+    if ( ddD->TimeStop && ddD->TimeStop < clock() )
+        return NULL;
     
     /* Recursive step. */
     index = f->index;
diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c
index 69309a4d..11c7d959 100644
--- a/src/misc/extra/extraBddMisc.c
+++ b/src/misc/extra/extraBddMisc.c
@@ -1277,6 +1277,11 @@ extraTransferPermuteRecur(
     if ( st_lookup( table, ( char * ) f, ( char ** ) &res ) )
         return ( Cudd_NotCond( res, comple ) );
 
+    if ( ddS->TimeStop && ddS->TimeStop < clock() )
+        return NULL;
+    if ( ddD->TimeStop && ddD->TimeStop < clock() )
+        return NULL;
+
     /* Recursive step. */
     if ( Permute )
         index = Permute[f->index];