Bug fix in &sat -x.

src/base/abci/abc.c

@@ -2758,7 +2758,8 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_NtkPrintPoEquivs( pNtk );
         return 0;
     }
-    Abc_Print( 1,"Status = %d  Frames = %d   ", pAbc->Status, pAbc->nFrames );
+    if ( !pAbc->vStatuses )
+        Abc_Print( 1,"Status = %d  Frames = %d   ", pAbc->Status, pAbc->nFrames );
     if ( pAbc->pCex == NULL && pAbc->vCexVec == NULL )
         Abc_Print( 1,"Cex is not defined.\n" );
     else
@@ -2770,7 +2771,7 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
             Abc_Cex_t * pTemp;
             int nCexes = 0;
             int Counter = 0;
-            printf( "\n" );
+            //printf( "\n" );
             Vec_PtrForEachEntry( Abc_Cex_t *, pAbc->vCexVec, pTemp, c )
             {
                 if ( pTemp == (void *)(ABC_PTRINT_T)1 )

src/proof/cec/cecSolve.c

@@ -717,6 +717,8 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar
         {
             pObj->fMark0 = 0;
             pObj->fMark1 = 1;
+            if ( pPars->fSaveCexes )
+                Vec_PtrWriteEntry( pAig->vSeqModelVec, i, (Abc_Cex_t *)(ABC_PTRINT_T)1 );
             continue;
         }
         Bar_ProgressUpdate( pProgress, i, "SAT..." );