diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-09 14:17:19 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-09 14:17:19 -0800 |
| commit | 32712ec9abb3f27e3bd00690838b054f5bdc0f77 (patch) | |
| tree | 65aa30b35d6c7b976d31ed29597c13223f0a9510 /src/proof/pdr | |
| parent | e20ef654d99d5cf1f0f73466b931d53833f6a1eb (diff) | |
| download | abc-32712ec9abb3f27e3bd00690838b054f5bdc0f77.tar.gz abc-32712ec9abb3f27e3bd00690838b054f5bdc0f77.tar.bz2 abc-32712ec9abb3f27e3bd00690838b054f5bdc0f77.zip | |
Making sure 'inv_out' can match flops by name.
Diffstat (limited to 'src/proof/pdr')
| -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 |