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/fraSim.c | |
| 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/fraSim.c')
| -rw-r--r-- | src/aig/fra/fraSim.c | 3 |
1 files changed, 2 insertions, 1 deletions
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 ) |