Commit 28ea3ade authored by Alan Mishchenko's avatar Alan Mishchenko

Improvements to the SAT sweeper (bug fix).

parent 36e8567e
......@@ -1273,7 +1273,7 @@ void Cec4_ManSatSolverRecycle( Cec4_Man_t * p )
int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pfEasy, int fVerbose )
{
abctime clk;
int nBTLimit = Vec_BitEntry(p->vFails, iObj0) || Vec_BitEntry(p->vFails, iObj1) ? p->pPars->nBTLimit/10 : p->pPars->nBTLimit;
int nBTLimit = Vec_BitEntry(p->vFails, iObj0) || Vec_BitEntry(p->vFails, iObj1) ? Abc_MaxInt(1, p->pPars->nBTLimit/10) : p->pPars->nBTLimit;
int nConfEnd, nConfBeg, status, iVar0, iVar1, Lits[2];
int UnsatConflicts[3] = {0};
if ( iObj1 < iObj0 )
......
......@@ -57,7 +57,7 @@ static int Abc_CommandGlucose( Abc_Frame_t * pAbc, int argc, char ** argv );
void Glucose2_Init(Abc_Frame_t *pAbc)
{
Cmd_CommandAdd( pAbc, "ABC9", "&glucose", Abc_CommandGlucose, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&glucose2", Abc_CommandGlucose, 0 );
}
void Glucose2_End( Abc_Frame_t * pAbc )
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment