Skip to content

A
abc
Commit c4e85930 by Alan Mishchenko
Options

Modified the PDR print-out to be compatible with Niklas.

parent af84c0d2
Showing with 3 additions and 3 deletions
src/sat/pdr/pdrCore.c
...@@ -574,6 +574,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) ...@@ -574,6 +574,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
} }
else else
{ {
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, clock() - clkStart );
// open a new timeframe // open a new timeframe
assert( pCube == NULL ); assert( pCube == NULL );
Pdr_ManSetPropertyOutput( p, k ); Pdr_ManSetPropertyOutput( p, k );
...@@ -583,8 +585,6 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) ...@@ -583,8 +585,6 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
printf( "*** Clauses after frame %d:\n", k ); printf( "*** Clauses after frame %d:\n", k );
Pdr_ManPrintClauses( p, 0 ); Pdr_ManPrintClauses( p, 0 );
} }
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 0, clock() - clkStart );
// push clauses into this timeframe // push clauses into this timeframe
if ( Pdr_ManPushClauses( p ) ) if ( Pdr_ManPushClauses( p ) )
{ {
...@@ -598,7 +598,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) ...@@ -598,7 +598,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
return 1; // UNSAT return 1; // UNSAT
} }
if ( p->pPars->fVerbose ) if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, clock() - clkStart ); Pdr_ManPrintProgress( p, 0, clock() - clkStart );
clkStart = clock(); clkStart = clock();
} }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment