Undoing previous change in 'resim' (do not initialize flops using their values in the CEX because the number of flops in the CEX can be different).

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++ );