Bug fix in PBA.

src/aig/gia/giaAbs.c

@@ -320,6 +320,7 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbo
     Gia_Man_t * pAbs;
     Aig_Man_t * pAig, * pOrig;
     Vec_Int_t * vFlops, * vFlopsNew, * vSelected;
+    int RetValue;
     if ( pGia->vFlopClasses == NULL )
     {
         printf( "Gia_ManPbaPerform(): Abstraction flop map is missing.\n" );
@@ -331,20 +332,23 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbo
     pAig = Gia_ManToAigSimple( pAbs );
     Gia_ManStop( pAbs );
     vFlopsNew = Saig_ManPbaDerive( pAig, Gia_ManPiNum(pGia), nFrames, nConfLimit, fVerbose );
-    Aig_ManStop( pAig );
     // derive new classes
     if ( pAig->pSeqModel == NULL )
     {
-        // the problem is UNSAT
-        vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses );
-        vSelected = Gia_ManFlopsSelect( vFlops, vFlopsNew );
-        Vec_IntFree( pGia->vFlopClasses );
-        pGia->vFlopClasses = Saig_ManFlops2Classes( Gia_ManRegNum(pGia), vSelected );
-        Vec_IntFree( vSelected );
-
-        Vec_IntFree( vFlopsNew );
-        Vec_IntFree( vFlops );
-        return -1;
+        // check if there is no timeout
+        if ( vFlopsNew != NULL )
+        {
+            // the problem is UNSAT
+            vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses );
+            vSelected = Gia_ManFlopsSelect( vFlops, vFlopsNew );
+            Vec_IntFree( pGia->vFlopClasses );
+            pGia->vFlopClasses = Saig_ManFlops2Classes( Gia_ManRegNum(pGia), vSelected );
+            Vec_IntFree( vSelected );
+
+            Vec_IntFree( vFlopsNew );
+            Vec_IntFree( vFlops );
+        }
+        RetValue = -1;
     }
     else if ( vFlopsNew == NULL )
     {
@@ -356,8 +360,7 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbo
         pOrig = Gia_ManToAigSimple( pGia );
         pGia->pCexSeq = Saig_ManCexRemap( pOrig, pAig, pAig->pSeqModel );
         Aig_ManStop( pOrig );
-        Aig_ManStop( pAig );
-        return 0;
+        RetValue = 0;
     }
     else
     {
@@ -366,8 +369,10 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbo
         Vec_Int_t * vAbsFfsToAdd = vFlopsNew;
         Gia_ManFlopsAddToClasses( pGia->vFlopClasses, vAbsFfsToAdd );
         Vec_IntFree( vAbsFfsToAdd );
-        return -1;
+        RetValue = -1;
     }
+    Aig_ManStop( pAig );
+    return RetValue;
 }
 
 

src/aig/saig/saigAbsPba.c

@@ -201,7 +201,7 @@ Abc_Cex_t * Saig_ManPbaDeriveCex( Aig_Man_t * pAig, sat_solver * pSat, Cnf_Dat_t
 ***********************************************************************/
 Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nFrames, int nConfLimit, int fVerbose )
 {
-    Vec_Int_t * vFlops, * vMapVar2FF, * vAssumps, * vPiVarMap;
+    Vec_Int_t * vFlops = NULL, * vMapVar2FF, * vAssumps, * vPiVarMap;
     Aig_Man_t * pFrames;
     sat_solver * pSat;
     Cnf_Dat_t * pCnf;
@@ -248,6 +248,8 @@ Abc_PrintTime( 1, "Solving", clock() - clk );
     {
         if ( RetValue == l_True )
         {
+            printf( "Saig_ManPerformPba(): The eproblem is SAT. Abstraction refinement is still not enabled.\n" );
+/*
             Vec_Int_t * vAbsFfsToAdd;
             ABC_FREE( pAig->pSeqModel );
             pAig->pSeqModel = Saig_ManPbaDeriveCex( pAig, pSat, pCnf, nFrames, vPiVarMap );
@@ -263,7 +265,8 @@ Abc_PrintTime( 1, "Solving", clock() - clk );
                 printf( "Adding %d registers to the abstraction.  ", Vec_IntSize(vAbsFfsToAdd) );
                 Abc_PrintTime( 0, "Time", clock() - clk );
             }
-            return vAbsFfsToAdd;
+            vFlops = vAbsFfsToAdd;
+*/
         }
         else
         {