diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-08-16 15:20:34 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-08-16 15:20:34 +0700 |
| commit | efa965463428a73a1c7888a8035bb0276aabefda (patch) | |
| tree | e7f9b7e940f018e73640d281394888ad0ee2b2fd | |
| parent | 7365052411bfc4d69f7724840ec607cae7f9d272 (diff) | |
| download | abc-efa965463428a73a1c7888a8035bb0276aabefda.tar.gz abc-efa965463428a73a1c7888a8035bb0276aabefda.tar.bz2 abc-efa965463428a73a1c7888a8035bb0276aabefda.zip | |
Bug fix in &bmcs.
| -rw-r--r-- | src/sat/bmc/bmcBmcS.c | 6 |
1 files 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; |