luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Adding features for invariant minimization.

This commit is contained in:
Alan Mishchenko 2017-01-25 22:29:51 -08:00
parent 636332c63e
commit 57286e8ab6
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/proof/pdr/pdrInv.c
View File

@ -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 if ( status == l_False ) // unsat -- correct
continue; continue;
assert( status == l_True ); assert( status == l_True );
if ( fVerbose )
printf( "Inductiveness check failed for clause %d.\n", i );
nFailed++; nFailed++;
if ( fSkip ) if ( fSkip )
{ {
Vec_IntFree( vLits ); Vec_IntFree( vLits );
return 1; return 1;
} }
if ( fVerbose )
printf( "Inductiveness check failed for clause %d.\n", i );
} }
Vec_IntFree( vLits ); Vec_IntFree( vLits );
return nFailed + nFailedOuts; return nFailed + nFailedOuts;