%pdra: fixed bugs

src/base/wlc/wlcAbs.c

@@ -1545,7 +1545,9 @@ void Wla_ManRefine( Wla_Man_t * pWla )
 
     if ( pWla->fNewAbs )
     {
-        assert( pWla->pCex == NULL );
+        if ( pWla->pCex )
+            Abc_CexFree( pWla->pCex );
+        pWla->pCex = NULL;
         Gia_ManStop( pWla->pGia ); pWla->pGia = NULL;
         return;
     }

src/base/wlc/wlcPth.c

@@ -86,7 +86,7 @@ void * Wla_Bmc3Thread ( void * pArg )
 {
     int status;
     int RetValue = -1;
-    int nFramesNoChangeLim = 3;
+    int nFramesNoChangeLim = 10;
     Bmc3_ThData_t * pData = (Bmc3_ThData_t *)pArg;
     Abc_Ntk_t * pAbcNtk = Abc_NtkFromAigPhase( pData->pAig );
     Saig_ParBmc_t BmcPars, *pBmcPars = &BmcPars;
@@ -94,7 +94,7 @@ void * Wla_Bmc3Thread ( void * pArg )
     pBmcPars->pFuncStop = Wla_CallBackToStop;
     pBmcPars->RunId = pData->RunId;
 
-    if ( pData->pWla->nIters > 1 && pData->pWla->pPars->fShrinkAbs )
+    if ( pData->pWla->pPars->fShrinkAbs )
         pBmcPars->nFramesMax = pData->pWla->iCexFrame + nFramesNoChangeLim;
 
     RetValue = Abc_NtkDarBmc3( pAbcNtk, pBmcPars, 0 );
@@ -117,7 +117,7 @@ void * Wla_Bmc3Thread ( void * pArg )
         if ( pData->RunId < g_nRunIds && pData->fVerbose )
             Abc_Print( 1, "Bmc3 was cancelled. RunId=%d.\n", pData->RunId );
 
-        if ( pData->RunId == g_nRunIds )
+        if ( pData->pWla->nIters > 1 && pData->RunId == g_nRunIds )
         {
             RetValue = Wla_ManShrinkAbs( pData->pWla, pData->pWla->iCexFrame + nFramesNoChangeLim );
             pData->pWla->iCexFrame += nFramesNoChangeLim; 

src/proof/pdr/pdrIncr.c

@@ -160,7 +160,8 @@ int IPdr_ManCheckClauses( Pdr_Man_t * p )
                 printf( "Cube[%d][%d] not inductive!\n", k, j );
             }
 
-            assert( RetValue == 1 );
+            if ( RetValue == -1 )
+                return -1;
         }
     }