summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-03-06 15:33:16 +0100
committerAlan Mishchenko <alanmi@berkeley.edu>2012-03-06 15:33:16 +0100
commit3634f60d7a53f3e0de21bda3702e0f5cdb957945 (patch)
tree1b6d1c2bff68601e36beea1f8e5b2f767bb5f1d7 /src/aig
parentabde9fe948eaa622c614de56331ef3cfc53c8adc (diff)
downloadabc-3634f60d7a53f3e0de21bda3702e0f5cdb957945.tar.gz
abc-3634f60d7a53f3e0de21bda3702e0f5cdb957945.tar.bz2
abc-3634f60d7a53f3e0de21bda3702e0f5cdb957945.zip
Fixing a bug and adding verification of minimized counter-example.
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/saig/saigAbsCba.c4
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;
}