diff options
Diffstat (limited to 'src/aig')
| -rw-r--r-- | src/aig/cec/cecSeq.c | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c index 7e7549c0..dd561971 100644 --- a/src/aig/cec/cecSeq.c +++ b/src/aig/cec/cecSeq.c @@ -49,20 +49,30 @@ void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Abc_Cex_t assert( pCex->nBits == pCex->nRegs + pCex->nPis * (pCex->iFrame + 1) ); assert( pCex->nBits - pCex->nRegs + Gia_ManRegNum(pAig) <= Vec_PtrSize(vInfo) ); nWords = Vec_PtrReadWordsSimInfo( vInfo ); +/* + // user register values + assert( pCex->nRegs == Gia_ManRegNum(pAig) ); for ( k = 0; k < pCex->nRegs; k++ ) { pInfo = (unsigned *)Vec_PtrEntry( vInfo, k ); for ( w = 0; w < nWords; w++ ) pInfo[w] = Gia_InfoHasBit( pCex->pData, k )? ~0 : 0; } -/* +*/ + // print warning about register values + for ( k = 0; k < pCex->nRegs; k++ ) + if ( Gia_InfoHasBit( pCex->pData, k ) ) + break; + if ( k < pCex->nRegs ) + Abc_Print( 0, "The CEX has flop values different from 0, but they are currently not used by \"resim\".\n" ); + + // assign zero register values for ( k = 0; k < Gia_ManRegNum(pAig); k++ ) { pInfo = (unsigned *)Vec_PtrEntry( vInfo, k ); for ( w = 0; w < nWords; w++ ) pInfo[w] = 0; } -*/ for ( i = pCex->nRegs; i < pCex->nBits; i++ ) { pInfo = (unsigned *)Vec_PtrEntry( vInfo, k++ ); |