summaryrefslogtreecommitdiffstats
path: root/src/aig/llb
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2011-05-13 10:19:29 +0800
committerAlan Mishchenko <alanmi@berkeley.edu>2011-05-13 10:19:29 +0800
commit265db2a9d147417dc845445dbf28461ed0c5c621 (patch)
treef5e5c306b8785f59f782e12a882178fc6c8f7251 /src/aig/llb
parent3c7842be32a25883b13d86d0d88530dc55f5cf15 (diff)
downloadabc-265db2a9d147417dc845445dbf28461ed0c5c621.tar.gz
abc-265db2a9d147417dc845445dbf28461ed0c5c621.tar.bz2
abc-265db2a9d147417dc845445dbf28461ed0c5c621.zip
Fixing mismatch in reconcile.
Diffstat (limited to 'src/aig/llb')
-rw-r--r--src/aig/llb/llb4Cex.c12
1 files changed, 11 insertions, 1 deletions
diff --git a/src/aig/llb/llb4Cex.c b/src/aig/llb/llb4Cex.c
index 42515a77..6c4cedfb 100644
--- a/src/aig/llb/llb4Cex.c
+++ b/src/aig/llb/llb4Cex.c
@@ -237,7 +237,17 @@ Vec_Ptr_t * Llb4_Nonlin4VerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p )
}
*/
assert( iBit == p->nBits );
- if ( Aig_ManPo(pAig, p->iPo)->fMarkB == 0 )
+// if ( Aig_ManPo(pAig, p->iPo)->fMarkB == 0 )
+// Vec_PtrFreeP( &vStates );
+ for ( i = Saig_ManPoNum(pAig) - 1; i >= 0; i-- )
+ {
+ if ( Aig_ManPo(pAig, i)->fMarkB )
+ {
+ p->iPo = i;
+ break;
+ }
+ }
+ if ( i == -1 )
Vec_PtrFreeP( &vStates );
Aig_ManCleanMarkB(pAig);
return vStates;