diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-01-31 16:38:49 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-01-31 16:38:49 -0800 |
| commit | 81dade194e30b6fa5f98352a76459c062d27e66f (patch) | |
| tree | 923d495c14b0dd42a55c623da9d3d155173eb7f9 | |
| parent | 367b20f04d2b42ab4c74fbb681e0d02f12de1ba6 (diff) | |
| download | abc-81dade194e30b6fa5f98352a76459c062d27e66f.tar.gz abc-81dade194e30b6fa5f98352a76459c062d27e66f.tar.bz2 abc-81dade194e30b6fa5f98352a76459c062d27e66f.zip | |
Rare bug fix in 'dch' resulting in choice nodes having internal fanout.
| -rw-r--r-- | src/proof/dch/dchChoice.c | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/src/proof/dch/dchChoice.c b/src/proof/dch/dchChoice.c index e2473de6..b5ccb765 100644 --- a/src/proof/dch/dchChoice.c +++ b/src/proof/dch/dchChoice.c @@ -456,7 +456,14 @@ void Dch_DeriveChoiceAigNode( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_ pObjNew = Aig_And( pAigNew, Aig_ObjChild0CopyRepr(pAigNew, pObj), Aig_ObjChild1CopyRepr(pAigNew, pObj) ); - pObjNew = Aig_ObjGetRepr( pAigNew, pObjNew ); +// pObjNew = Aig_ObjGetRepr( pAigNew, pObjNew ); + while ( 1 ) + { + Aig_Obj_t * pObjNew2 = pObjNew; + pObjNew = Aig_ObjGetRepr( pAigNew, pObjNew2 ); + if ( pObjNew == pObjNew2 ) + break; + } // assert( Aig_ObjRepr( pAigNew, pObjNew ) == NULL ); // assign the copy assert( pObj->pData == NULL ); |