From 58946372219a696f6b65a55a315501df6a4f24f8 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 4 Mar 2011 20:14:30 -0800 Subject: Yet another improvement in &abs_refine -s. --- src/aig/saig/saigSimExt2.c | 3 +++ 1 file changed, 3 insertions(+) (limited to 'src') 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 ); -- cgit v1.2.3