diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-01-25 22:29:51 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-01-25 22:29:51 -0800 |
| commit | 57286e8ab692d2df5df6e4077134b913229ba33f (patch) | |
| tree | c404f12c1c8ab7d77b52cea9fe123815d639ccc0 /src/proof/pdr/pdrInv.c | |
| parent | 636332c63e31d15112f89e89a4689351ed3b66ca (diff) | |
| download | abc-57286e8ab692d2df5df6e4077134b913229ba33f.tar.gz abc-57286e8ab692d2df5df6e4077134b913229ba33f.tar.bz2 abc-57286e8ab692d2df5df6e4077134b913229ba33f.zip | |
Adding features for invariant minimization.
Diffstat (limited to 'src/proof/pdr/pdrInv.c')
| -rw-r--r-- | src/proof/pdr/pdrInv.c | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c index 0d27ce7e..8b04c53b 100644 --- a/src/proof/pdr/pdrInv.c +++ b/src/proof/pdr/pdrInv.c @@ -759,14 +759,14 @@ int Pdr_InvCheck_int( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose, sat_solver if ( status == l_False ) // unsat -- correct continue; assert( status == l_True ); + if ( fVerbose ) + printf( "Inductiveness check failed for clause %d.\n", i ); nFailed++; if ( fSkip ) { Vec_IntFree( vLits ); return 1; } - if ( fVerbose ) - printf( "Inductiveness check failed for clause %d.\n", i ); } Vec_IntFree( vLits ); return nFailed + nFailedOuts; |