diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-05-13 10:19:29 +0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-05-13 10:19:29 +0800 |
| commit | 265db2a9d147417dc845445dbf28461ed0c5c621 (patch) | |
| tree | f5e5c306b8785f59f782e12a882178fc6c8f7251 /src/aig/llb/llb4Cex.c | |
| parent | 3c7842be32a25883b13d86d0d88530dc55f5cf15 (diff) | |
| download | abc-265db2a9d147417dc845445dbf28461ed0c5c621.tar.gz abc-265db2a9d147417dc845445dbf28461ed0c5c621.tar.bz2 abc-265db2a9d147417dc845445dbf28461ed0c5c621.zip | |
Fixing mismatch in reconcile.
Diffstat (limited to 'src/aig/llb/llb4Cex.c')
| -rw-r--r-- | src/aig/llb/llb4Cex.c | 12 |
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; |