summaryrefslogtreecommitdiffstats
path: root/src/proof/pdr/pdrMan.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-03-02 01:15:40 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2012-03-02 01:15:40 -0800
commitc47dc99a9402b57762073a786ac71027509a537b (patch)
tree75d4fcec2189de17af1ba72bc0961b8c969b386d /src/proof/pdr/pdrMan.c
parent4db9c63627301329530465ea459588a98411f79b (diff)
downloadabc-c47dc99a9402b57762073a786ac71027509a537b.tar.gz
abc-c47dc99a9402b57762073a786ac71027509a537b.tar.bz2
abc-c47dc99a9402b57762073a786ac71027509a537b.zip
Redirecting printf messages.
Diffstat (limited to 'src/proof/pdr/pdrMan.c')
-rw-r--r--src/proof/pdr/pdrMan.c4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c
index 33c94d40..73c12a7d 100644
--- a/src/proof/pdr/pdrMan.c
+++ b/src/proof/pdr/pdrMan.c
@@ -95,7 +95,7 @@ void Pdr_ManStop( Pdr_Man_t * p )
Aig_ManCleanMarkAB( p->pAig );
if ( p->pPars->fVerbose )
{
- printf( "Block =%5d Oblig =%6d Clause =%6d Call =%6d (sat=%.1f%%) Start =%4d\n",
+ Abc_Print( 1, "Block =%5d Oblig =%6d Clause =%6d Call =%6d (sat=%.1f%%) Start =%4d\n",
p->nBlocks, p->nObligs, p->nCubes, p->nCalls, 100.0 * p->nCallsS / p->nCalls, p->nStarts );
ABC_PRTP( "SAT solving", p->tSat, p->tTotal );
ABC_PRTP( " unsat ", p->tSatUnsat, p->tTotal );
@@ -107,7 +107,7 @@ void Pdr_ManStop( Pdr_Man_t * p )
ABC_PRTP( "CNF compute", p->tCnf, p->tTotal );
ABC_PRTP( "TOTAL ", p->tTotal, p->tTotal );
}
-// printf( "SS =%6d. SU =%6d. US =%6d. UU =%6d.\n", p->nCasesSS, p->nCasesSU, p->nCasesUS, p->nCasesUU );
+// Abc_Print( 1, "SS =%6d. SU =%6d. US =%6d. UU =%6d.\n", p->nCasesSS, p->nCasesSU, p->nCasesUS, p->nCasesUU );
Vec_PtrForEachEntry( sat_solver *, p->vSolvers, pSat, i )
sat_solver_delete( pSat );
Vec_PtrFree( p->vSolvers );