From 36e5badf055e28a0f6560e9e55bfc4e1df6fec79 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 15 Jan 2019 17:30:39 -0800 Subject: Procedure to trasnsform counter-examples. --- src/misc/util/utilCex.c | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/misc/util') 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 -- cgit v1.2.3