Adding procedures to find the care bits of a counter-example (update).

src/aig/saig/saig.h

@@ -176,7 +176,7 @@ extern Aig_Man_t *       Saig_ManDecPropertyOutput( Aig_Man_t * pAig, int nLits,
 /*=== saigPhase.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose );
 /*=== saigRefSat.c ==========================================================*/
-extern Abc_Cex_t *       Saig_ManRefineCexSat( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose );
+extern Abc_Cex_t *       Saig_ManFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose );
 /*=== saigRetFwd.c ==========================================================*/
 extern void              Saig_ManMarkAutonomous( Aig_Man_t * p );
 extern Aig_Man_t *       Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, int fVerbose );

src/aig/saig/saigRefSat.c

@@ -393,7 +393,7 @@ Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Cex_t * Saig_ManRefineCexSat( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose )
+Abc_Cex_t * Saig_ManFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose )
 {
     Abc_Cex_t * pCare = NULL;
     int clk = clock();

src/base/abci/abc.c

@@ -8770,7 +8770,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         Abc_Cex_t * pNew;
         Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
-        pNew = Saig_ManRefineCexSat( pAig, pAbc->pCex, 0, 0 );
+        pNew = Saig_ManFindCexCareBits( pAig, pAbc->pCex, 0, 0 );
         Aig_ManStop( pAig );
         Abc_FrameReplaceCex( pAbc, &pNew );
     }