From 32712ec9abb3f27e3bd00690838b054f5bdc0f77 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 9 Feb 2017 14:17:19 -0800 Subject: Making sure 'inv_out' can match flops by name. --- src/proof/pdr/pdrInv.c | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/proof') 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 -- cgit v1.2.3