diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-09-05 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-09-05 08:01:00 -0700 |
| commit | 092c7be0ffb89d869e8eaeb04de12779ce96e8b9 (patch) | |
| tree | fe4ae0c41d0481c1c3f9eec7689f49cba58cd4e8 /src/aig/dch/dchSimSat.c | |
| parent | 73c8aa7c400bab320cea56529241e1d396f1e0f5 (diff) | |
| download | abc-092c7be0ffb89d869e8eaeb04de12779ce96e8b9.tar.gz abc-092c7be0ffb89d869e8eaeb04de12779ce96e8b9.tar.bz2 abc-092c7be0ffb89d869e8eaeb04de12779ce96e8b9.zip | |
Version abc80905
Diffstat (limited to 'src/aig/dch/dchSimSat.c')
| -rw-r--r-- | src/aig/dch/dchSimSat.c | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/aig/dch/dchSimSat.c b/src/aig/dch/dchSimSat.c index 1fefa6eb..7a6865bd 100644 --- a/src/aig/dch/dchSimSat.c +++ b/src/aig/dch/dchSimSat.c @@ -108,8 +108,11 @@ void Dch_ManResimulateSolved_rec( Dch_Man_t * p, Aig_Obj_t * pObj ) Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj); if ( Aig_ObjIsPi(pObj) ) { - Aig_Obj_t * pObjFraig = Dch_ObjFraig( pObj ); - int nVarNum = Dch_ObjSatNum( p, pObjFraig ); + Aig_Obj_t * pObjFraig; + int nVarNum; + pObjFraig = Dch_ObjFraig( pObj ); + assert( !Aig_IsComplement(pObjFraig) ); + nVarNum = Dch_ObjSatNum( p, pObjFraig ); // get the value from the SAT solver // (account for the fact that some vars may be minimized away) pObj->fMarkB = !nVarNum? 0 : sat_solver_var_value( p->pSat, nVarNum ); |