diff options
| -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; } |