diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-17 17:39:42 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-17 17:39:42 -0700 |
| commit | 6dc3a0a2469b4cf9b5d753dd66776a7b45583a56 (patch) | |
| tree | e7c79e4bc3bd5d820ef9296bbc8a8fc491eaf1e3 /src/aig/saig | |
| parent | 1f9abfd7a8c2d3978ee58d4be2d07cc633a5008d (diff) | |
| download | abc-6dc3a0a2469b4cf9b5d753dd66776a7b45583a56.tar.gz abc-6dc3a0a2469b4cf9b5d753dd66776a7b45583a56.tar.bz2 abc-6dc3a0a2469b4cf9b5d753dd66776a7b45583a56.zip | |
Bug fix in bmc3.
Diffstat (limited to 'src/aig/saig')
| -rw-r--r-- | src/aig/saig/saigBmc3.c | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index ac0be651..294f6b64 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -1240,12 +1240,17 @@ int Saig_ManBmcRunTerSim_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame ) ***********************************************************************/ int Saig_ManBmcCreateCnf( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame ) { + int Lit; // perform terminary simulation int Value = Saig_ManBmcRunTerSim_rec( p, pObj, iFrame ); if ( Value != SAIG_TER_UND ) return (int)(Value == SAIG_TER_ONE); // construct CNF if value is ternary - return Saig_ManBmcCreateCnf_rec( p, pObj, iFrame ); + Lit = Saig_ManBmcCreateCnf_rec( p, pObj, iFrame ); + // extend the SAT solver + if ( p->nSatVars > sat_solver_nvars(p->pSat) ) + sat_solver_setnvars( p->pSat, p->nSatVars ); + return Lit; } |