From 3634f60d7a53f3e0de21bda3702e0f5cdb957945 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 6 Mar 2012 15:33:16 +0100 Subject: Fixing a bug and adding verification of minimized counter-example. --- src/aig/saig/saigAbsCba.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/aig/saig') 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; } -- cgit v1.2.3