From 7365052411bfc4d69f7724840ec607cae7f9d272 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 16 Aug 2017 15:02:47 +0700 Subject: Adding an option to bmc3 to use Satoko intead of the default SAT solver. --- src/sat/bmc/bmcBmcS.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/bmc/bmcBmcS.c b/src/sat/bmc/bmcBmcS.c index 5cb5994a..39121b8b 100644 --- a/src/sat/bmc/bmcBmcS.c +++ b/src/sat/bmc/bmcBmcS.c @@ -575,7 +575,7 @@ void Bmcs_ManPrintFrame( Bmcs_Man_t * p, int f, int nClauses, int Solver, abctim if ( !p->pPars->fVerbose ) return; Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" ); -#ifdef ABC_USE_EXT_SOLVERS +#ifndef ABC_USE_EXT_SOLVERS Abc_Print( 1, "Var =%8.0f. ", (double)solver_varnum(p->pSats[0]) ); Abc_Print( 1, "Cla =%9.0f. ", (double)solver_clausenum(p->pSats[0]) ); Abc_Print( 1, "Learn =%9.0f. ",(double)solver_learntnum(p->pSats[0]) ); -- cgit v1.2.3