diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-01-25 14:16:31 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-01-25 14:16:31 +0700 |
| commit | 4aa434ad11355297dffa4b2384b5777e68e8ed8a (patch) | |
| tree | c4a4596f4eaa7b776addf2532ef352de4e655942 /src | |
| parent | 557448400ebaf0f4666665bd8bc87954e3c2a976 (diff) | |
| download | abc-4aa434ad11355297dffa4b2384b5777e68e8ed8a.tar.gz abc-4aa434ad11355297dffa4b2384b5777e68e8ed8a.tar.bz2 abc-4aa434ad11355297dffa4b2384b5777e68e8ed8a.zip | |
Updated CEX code to handle trivial CEX of the type (Abc_Cex_t*)1.
Diffstat (limited to 'src')
| -rw-r--r-- | src/misc/util/utilCex.c | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c index 75b99492..b0ce66be 100644 --- a/src/misc/util/utilCex.c +++ b/src/misc/util/utilCex.c @@ -146,6 +146,8 @@ Abc_Cex_t * Abc_CexDup( Abc_Cex_t * p, int nRegsNew ) { Abc_Cex_t * pCex; int i; + if ( p == (Abc_Cex_t *)(ABC_PTRINT_T)1 ) + return p; if ( nRegsNew == -1 ) nRegsNew = p->nRegs; pCex = Abc_CexAlloc( nRegsNew, p->nPis, p->iFrame+1 ); @@ -259,6 +261,11 @@ void Abc_CexPrintStats( Abc_Cex_t * p ) printf( "The counter example is NULL.\n" ); return; } + if ( p == (Abc_Cex_t *)(ABC_PTRINT_T)1 ) + { + printf( "The counter example is present but not available (pointer has value \"1\").\n" ); + return; + } for ( k = 0; k < p->nBits; k++ ) Counter += Abc_InfoHasBit(p->pData, k); printf( "CEX: Po =%4d Frame =%4d FF = %d PI = %d Bit =%8d 1s =%8d (%5.2f %%)\n", @@ -273,6 +280,11 @@ void Abc_CexPrintStatsInputs( Abc_Cex_t * p, int nInputs ) printf( "The counter example is NULL.\n" ); return; } + if ( p == (Abc_Cex_t *)(ABC_PTRINT_T)1 ) + { + printf( "The counter example is present but not available (pointer has value \"1\").\n" ); + return; + } for ( k = 0; k < p->nBits; k++ ) { Counter += Abc_InfoHasBit(p->pData, k); @@ -304,6 +316,11 @@ void Abc_CexPrint( Abc_Cex_t * p ) printf( "The counter example is NULL.\n" ); return; } + if ( p == (Abc_Cex_t *)(ABC_PTRINT_T)1 ) + { + printf( "The counter example is present but not available (pointer has value \"1\").\n" ); + return; + } Abc_CexPrintStats( p ); printf( "State : " ); for ( k = 0; k < p->nRegs; k++ ) @@ -350,6 +367,8 @@ void Abc_CexFreeP( Abc_Cex_t ** p ) ***********************************************************************/ void Abc_CexFree( Abc_Cex_t * p ) { + if ( p == (Abc_Cex_t *)(ABC_PTRINT_T)1 ) + return; ABC_FREE( p ); } |