diff options
Diffstat (limited to 'src/proof/pdr')
| -rw-r--r-- | src/proof/pdr/pdrInv.c | 13 | ||||
| -rw-r--r-- | src/proof/pdr/pdrMan.c | 2 |
2 files changed, 12 insertions, 3 deletions
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c index 554add9b..baade033 100644 --- a/src/proof/pdr/pdrInv.c +++ b/src/proof/pdr/pdrInv.c @@ -50,7 +50,16 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time ) Vec_Ptr_t * vVec; int i, ThisSize, Length, LengthStart; if ( Vec_PtrSize(p->vSolvers) < 2 ) + { + printf( "Frame " ); + printf( "Clauses " ); + printf( "Max Queue " ); + printf( "Flops " ); + printf( "Cex " ); + printf( "Time" ); + printf( "\n" ); return; + } if ( Abc_FrameIsBatchMode() && !fClose ) return; // count the total length of the printout @@ -81,9 +90,9 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time ) for ( i = ThisSize; i < 70; i++ ) Abc_Print( 1, " " ); Abc_Print( 1, "%5d", p->nQueMax ); - Abc_Print( 1, "%5d", p->vAbsFlops ? Vec_IntCountPositive(p->vAbsFlops) : p->nAbsFlops ); + Abc_Print( 1, "%6d", p->vAbsFlops ? Vec_IntCountPositive(p->vAbsFlops) : p->nAbsFlops ); if ( p->pPars->fUseAbs ) - Abc_Print( 1, "%5d", p->nCexes ); + Abc_Print( 1, "%4d", p->nCexes ); Abc_Print( 1, "%10.2f sec", 1.0*Time/CLOCKS_PER_SEC ); if ( p->pPars->fSolveAll ) Abc_Print( 1, " CEX =%4d", p->pPars->nFailOuts ); diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c index c19041ee..abe8c0a8 100644 --- a/src/proof/pdr/pdrMan.c +++ b/src/proof/pdr/pdrMan.c @@ -455,7 +455,7 @@ Abc_Cex_t * Pdr_ManDeriveCexAbs( Pdr_Man_t * p ) int i, f, Lit, Flop, nFrames = 0; int nPis = Saig_ManPiNum(p->pAig); int nFfRefined = 0; - if ( !p->pPars->fUseAbs ) + if ( !p->pPars->fUseAbs || !p->vMapPpi2Ff ) return Pdr_ManDeriveCex(p); // restore previous map Vec_IntForEachEntry( p->vMapPpi2Ff, Flop, i ) |