From efa965463428a73a1c7888a8035bb0276aabefda Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 16 Aug 2017 15:20:34 +0700 Subject: Bug fix in &bmcs. --- src/sat/bmc/bmcBmcS.c | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/sat/bmc/bmcBmcS.c b/src/sat/bmc/bmcBmcS.c index 39121b8b..e1533779 100644 --- a/src/sat/bmc/bmcBmcS.c +++ b/src/sat/bmc/bmcBmcS.c @@ -386,14 +386,14 @@ Bmcs_Man_t * Bmcs_ManStart( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) opts.garbage_max_ratio = (float) 0.3 + i * 0.05; // create SAT solvers p->pSats[i] = bmc_sat_solver_start( i ); - bmc_sat_solver_addvar( p->pSats[i] ); - bmc_sat_solver_addclause( p->pSats[i], &Lit, 1 ); - bmc_sat_solver_setstop( p->pSats[i], &p->fStopNow ); #ifdef ABC_USE_EXT_SOLVERS p->pSats[i]->SolverType = i; #else satoko_configure(p->pSats[i], &opts); #endif + bmc_sat_solver_addvar( p->pSats[i] ); + bmc_sat_solver_addclause( p->pSats[i], &Lit, 1 ); + bmc_sat_solver_setstop( p->pSats[i], &p->fStopNow ); } p->nSatVars = 1; return p; -- cgit v1.2.3