summaryrefslogtreecommitdiffstats
path: root/src/sat/pdr
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2011-07-12 22:41:44 +0700
committerAlan Mishchenko <alanmi@berkeley.edu>2011-07-12 22:41:44 +0700
commitc4e859307580ea2bb18bf8b9f9e3c64a310f3bc9 (patch)
tree025f9771a7ec20625c9da2d8003be377fed4919a /src/sat/pdr
parentaf84c0d2056ecd11e057990c7d717c0a2e984941 (diff)
downloadabc-c4e859307580ea2bb18bf8b9f9e3c64a310f3bc9.tar.gz
abc-c4e859307580ea2bb18bf8b9f9e3c64a310f3bc9.tar.bz2
abc-c4e859307580ea2bb18bf8b9f9e3c64a310f3bc9.zip
Modified the PDR print-out to be compatible with Niklas.
Diffstat (limited to 'src/sat/pdr')
-rw-r--r--src/sat/pdr/pdrCore.c6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/sat/pdr/pdrCore.c b/src/sat/pdr/pdrCore.c
index 6289889b..cf8c231a 100644
--- a/src/sat/pdr/pdrCore.c
+++ b/src/sat/pdr/pdrCore.c
@@ -574,6 +574,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
}
else
{
+ if ( p->pPars->fVerbose )
+ Pdr_ManPrintProgress( p, 1, clock() - clkStart );
// open a new timeframe
assert( pCube == NULL );
Pdr_ManSetPropertyOutput( p, k );
@@ -583,8 +585,6 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
printf( "*** Clauses after frame %d:\n", k );
Pdr_ManPrintClauses( p, 0 );
}
- if ( p->pPars->fVerbose )
- Pdr_ManPrintProgress( p, 0, clock() - clkStart );
// push clauses into this timeframe
if ( Pdr_ManPushClauses( p ) )
{
@@ -598,7 +598,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
return 1; // UNSAT
}
if ( p->pPars->fVerbose )
- Pdr_ManPrintProgress( p, 1, clock() - clkStart );
+ Pdr_ManPrintProgress( p, 0, clock() - clkStart );
clkStart = clock();
}