diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-01-06 11:34:06 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-01-06 11:34:06 +0700 |
| commit | 10ad89490a6596dc51e27b6d7ebd0f2f0c606ed8 (patch) | |
| tree | 6966b842db8cf7ed2f504d259407043d53cb225e /src/aig/fra | |
| parent | 26b87c8c557972f4f942b9cb8baaf2f25d5b7b84 (diff) | |
| download | abc-10ad89490a6596dc51e27b6d7ebd0f2f0c606ed8.tar.gz abc-10ad89490a6596dc51e27b6d7ebd0f2f0c606ed8.tar.bz2 abc-10ad89490a6596dc51e27b6d7ebd0f2f0c606ed8.zip | |
Bug fix related to not properly resizing SAT solver's model array.
Diffstat (limited to 'src/aig/fra')
| -rw-r--r-- | src/aig/fra/fraClaus.c | 3 | ||||
| -rw-r--r-- | src/aig/fra/fraSim.c | 3 |
2 files changed, 4 insertions, 2 deletions
diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c index 90659333..9548c166 100644 --- a/src/aig/fra/fraClaus.c +++ b/src/aig/fra/fraClaus.c @@ -1303,7 +1303,8 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p ) if ( RetValue != l_False ) { // printf( "S- " ); - Fra_ClausSimInfoRecord( p, (int*)p->pSatMain->model.ptr + p->nFrames * p->pCnf->nVars ); +// Fra_ClausSimInfoRecord( p, (int*)p->pSatMain->model.ptr + p->nFrames * p->pCnf->nVars ); + Fra_ClausSimInfoRecord( p, (int*)p->pSatMain->model + p->nFrames * p->pCnf->nVars ); // RetValue = Fra_ClausSimInfoCheck(p, pStart + Beg, End - Beg); // assert( RetValue ); diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c index 37620a16..8f912915 100644 --- a/src/aig/fra/fraSim.c +++ b/src/aig/fra/fraSim.c @@ -244,7 +244,8 @@ void Fra_SmlSavePattern( Fra_Man_t * p ) int i; memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); Aig_ManForEachPi( p->pManFraig, pObj, i ) - if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True ) +// if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True ) + if ( sat_solver_var_value(p->pSat, Fra_ObjSatNum(pObj)) ) Aig_InfoSetBit( p->pPatWords, i ); if ( p->vCex ) |