From 6dc3a0a2469b4cf9b5d753dd66776a7b45583a56 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 17 Sep 2012 17:39:42 -0700 Subject: Bug fix in bmc3. --- src/aig/saig/saigBmc3.c | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'src') 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; } -- cgit v1.2.3