diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2019-01-15 17:30:39 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2019-01-15 17:30:39 -0800 |
| commit | 36e5badf055e28a0f6560e9e55bfc4e1df6fec79 (patch) | |
| tree | 9a7f8c048fc9bd1c865b9cd571145220cfae990b /src/misc/util | |
| parent | 1779f545e3637c85b02bf4b66bf839ca27eb5355 (diff) | |
| download | abc-36e5badf055e28a0f6560e9e55bfc4e1df6fec79.tar.gz abc-36e5badf055e28a0f6560e9e55bfc4e1df6fec79.tar.bz2 abc-36e5badf055e28a0f6560e9e55bfc4e1df6fec79.zip | |
Procedure to trasnsform counter-examples.
Diffstat (limited to 'src/misc/util')
| -rw-r--r-- | src/misc/util/utilCex.c | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c index 59107dc9..f61879b0 100644 --- a/src/misc/util/utilCex.c +++ b/src/misc/util/utilCex.c @@ -463,16 +463,16 @@ Abc_Cex_t * Abc_CexTransformUndc( Abc_Cex_t * p, char * pInit ) int i, f, iBit, iAddPi = 0, nAddPis = 0; // count how many flops got a new PI for ( i = 0; i < nFlops; i++ ) - nAddPis += (int)(pInit[i] == 'x'); + nAddPis += (int)(pInit[i] == 'x' || pInit[i] == 'X'); // create new CEX pCex = Abc_CexAlloc( nFlops, p->nPis - nAddPis, p->iFrame + 1 ); pCex->iPo = p->iPo; pCex->iFrame = p->iFrame; for ( iBit = 0; iBit < nFlops; iBit++ ) { - if ( pInit[iBit] == '1' || (pInit[iBit] == 'x' && Abc_InfoHasBit(p->pData, p->nRegs + p->nPis - nAddPis + iAddPi)) ) + if ( pInit[iBit] == '1' || ((pInit[iBit] == 'x' || pInit[iBit] == 'X') && Abc_InfoHasBit(p->pData, p->nRegs + p->nPis - nAddPis + iAddPi)) ) Abc_InfoSetBit( pCex->pData, iBit ); - iAddPi += (int)(pInit[iBit] == 'x'); + iAddPi += (int)(pInit[iBit] == 'x' || pInit[iBit] == 'X'); } assert( iAddPi == nAddPis ); // add timeframes |