diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-03-06 15:33:16 +0100 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-03-06 15:33:16 +0100 |
| commit | 3634f60d7a53f3e0de21bda3702e0f5cdb957945 (patch) | |
| tree | 1b6d1c2bff68601e36beea1f8e5b2f767bb5f1d7 /src | |
| parent | abde9fe948eaa622c614de56331ef3cfc53c8adc (diff) | |
| download | abc-3634f60d7a53f3e0de21bda3702e0f5cdb957945.tar.gz abc-3634f60d7a53f3e0de21bda3702e0f5cdb957945.tar.bz2 abc-3634f60d7a53f3e0de21bda3702e0f5cdb957945.zip | |
Fixing a bug and adding verification of minimized counter-example.
Diffstat (limited to 'src')
| -rw-r--r-- | src/aig/saig/saigAbsCba.c | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/aig/saig/saigAbsCba.c b/src/aig/saig/saigAbsCba.c index 022c298b..4873eb64 100644 --- a/src/aig/saig/saigAbsCba.c +++ b/src/aig/saig/saigAbsCba.c @@ -763,9 +763,9 @@ Abc_CexPrintStats( pCare ); } // verify the reduced counter-example using ternary simulation if ( !Saig_ManCexVerifyUsingTernary( pAig, pCex, pCare ) ) - printf( "Saig_ManCbaFindCexCareBits(): Counter-example verification has failed!!!\n" ); + printf( "Saig_ManCbaFindCexCareBits(): Minimized counter-example verification has failed!!!\n" ); else if ( fVerbose ) - printf( "Saig_ManCbaFindCexCareBits(): Counter-example verification is successful.\n" ); + printf( "Saig_ManCbaFindCexCareBits(): Minimized counter-example verification is successful.\n" ); Aig_ManCleanMarkAB( pAig ); return pCare; } |