From 1e0bbef1ef6a6ff7f0293e0926a8ff2b396e0a3e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 19 Sep 2017 17:29:03 -0700 Subject: Uncommenting handling of initial values of the flops. --- abclib.dsp | 4 ++++ src/aig/gia/giaCex.c | 4 ++-- src/base/abc/abcLatch.c | 4 ++-- 3 files changed, 8 insertions(+), 4 deletions(-) diff --git a/abclib.dsp b/abclib.dsp index 31a19ceb..f07aae07 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -5255,6 +5255,10 @@ SOURCE=.\src\proof\cec\cecSat.c # End Source File # Begin Source File +SOURCE=.\src\proof\cec\cecSatG.c +# End Source File +# Begin Source File + SOURCE=.\src\proof\cec\cecSeq.c # End Source File # Begin Source File diff --git a/src/aig/gia/giaCex.c b/src/aig/gia/giaCex.c index 5a8125f3..7bd7fd50 100644 --- a/src/aig/gia/giaCex.c +++ b/src/aig/gia/giaCex.c @@ -90,8 +90,8 @@ int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs ) int RetValue, i, k, iBit = 0; assert( Gia_ManPiNum(pAig) == p->nPis ); Gia_ManCleanMark0(pAig); -// Gia_ManForEachRo( pAig, pObj, i ) -// pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++); + Gia_ManForEachRo( pAig, pObj, i ) + pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++); iBit = p->nRegs; for ( i = 0; i <= p->iFrame; i++ ) { diff --git a/src/base/abc/abcLatch.c b/src/base/abc/abcLatch.c index d30c7051..fcace105 100644 --- a/src/base/abc/abcLatch.c +++ b/src/base/abc/abcLatch.c @@ -738,8 +738,8 @@ int Abc_NtkVerifyCex( Abc_Ntk_t * pNtk, Abc_Cex_t * p ) Abc_NtkCleanMarkC( pNtk ); Abc_AigConst1(pNtk)->fMarkC = 1; // initialize flops -// Abc_NtkForEachLatch( pNtk, pObj, i ) -// Abc_ObjFanout0(pObj)->fMarkC = Abc_InfoHasBit(p->pData, iBit++); + Abc_NtkForEachLatch( pNtk, pObj, i ) + Abc_ObjFanout0(pObj)->fMarkC = Abc_InfoHasBit(p->pData, iBit++); // simulate timeframes iBit = p->nRegs; for ( i = 0; i <= p->iFrame; i++ ) -- cgit v1.2.3