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/opt | |
| 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/opt')
| -rw-r--r-- | src/opt/res/resSat.c | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/opt/res/resSat.c b/src/opt/res/resSat.c index a17f92fa..17f3d661 100644 --- a/src/opt/res/resSat.c +++ b/src/opt/res/resSat.c @@ -279,7 +279,8 @@ int Res_SatSimulate( Res_Sim_t * p, int nPatsLimit, int fOnSet ) for ( i = 0; i < p->nTruePis; i++ ) { Var = (int)(ABC_PTRUINT_T)Abc_NtkPi(p->pAig,i)->pCopy; - value = (int)(pSat->model.ptr[Var] == l_True); +// value = (int)(pSat->model.ptr[Var] == l_True); + value = sat_solver_var_value(pSat, Var); if ( value ) Abc_InfoSetBit( (unsigned *)Vec_PtrEntry(vPats, i), k ); Lit = toLitCond( Var, value ); |