diff options
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/pdr/pdrInv.c | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c index 8130d0a3..95adb10c 100644 --- a/src/proof/pdr/pdrInv.c +++ b/src/proof/pdr/pdrInv.c @@ -756,6 +756,8 @@ int Pdr_InvCheck_int( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose, sat_solver // check if this cube intersects with the complement of other cubes in the solver // if it does not intersect, then it is redundant and can be skipped status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 ); + if ( status != l_True && fVerbose ) + printf( "Finished checking clause %d (out of %d)...\r", i, pList[0] ); if ( status == l_Undef ) // timeout break; if ( status == l_False ) // unsat -- correct |