summaryrefslogtreecommitdiffstats
path: root/src/aig/saig/saigSimExt2.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2011-03-04 20:14:30 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2011-03-04 20:14:30 -0800
commit58946372219a696f6b65a55a315501df6a4f24f8 (patch)
treea99a5b2cceb993fb5313d5b1cb8fdd62f033adbb /src/aig/saig/saigSimExt2.c
parentbfc39c1c33af820a8943aecd71a904fa42a808bd (diff)
downloadabc-58946372219a696f6b65a55a315501df6a4f24f8.tar.gz
abc-58946372219a696f6b65a55a315501df6a4f24f8.tar.bz2
abc-58946372219a696f6b65a55a315501df6a4f24f8.zip
Yet another improvement in &abs_refine -s.
Diffstat (limited to 'src/aig/saig/saigSimExt2.c')
-rw-r--r--src/aig/saig/saigSimExt2.c3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/aig/saig/saigSimExt2.c b/src/aig/saig/saigSimExt2.c
index 87b1e710..cb5d3b77 100644
--- a/src/aig/saig/saigSimExt2.c
+++ b/src/aig/saig/saigSimExt2.c
@@ -280,6 +280,7 @@ void Saig_ManExplorePaths_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int f, int fMax,
***********************************************************************/
Vec_Int_t * Saig_ManProcessCex( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose )
{
+ Aig_Obj_t * pObj;
Vec_Int_t * vRes, * vResInv;
int i, f, Value;
// assert( Aig_ManRegNum(p) > 0 );
@@ -288,6 +289,8 @@ Vec_Int_t * Saig_ManProcessCex( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCe
Value = Saig_ManSimDataInit2( p, pCex, vSimInfo );
assert( Value == SAIG_ONE_NEW );
// derive implications of constants and primary inputs
+ Saig_ManForEachLo( p, pObj, i )
+ Saig_ManSetAndDriveImplications_rec( p, pObj, 0, pCex->iFrame, vSimInfo );
for ( f = pCex->iFrame; f >= 0; f-- )
{
Saig_ManSetAndDriveImplications_rec( p, Aig_ManConst1(p), f, pCex->iFrame, vSimInfo );