From b44c519620c6174241f7ab942f07e9db9e9e0e5b Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Fri, 9 Sep 2016 15:39:33 +0200 Subject: Fix in BMS. --- src/base/abci/abcExact.c | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'src/base/abci') diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c index 00d534ec..7e2aa5b9 100644 --- a/src/base/abci/abcExact.c +++ b/src/base/abci/abcExact.c @@ -1324,6 +1324,11 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes ) { Vec_IntForEachEntry( pSes->vStairDecVars, j, i ) { + if ( pSes->nGates - 2 - i < 0 ) + { + Vec_IntFree( vLits ); + return 0; + } Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManSelectVar( pSes, pSes->nGates - 1 - i, j, pSes->nSpecVars + pSes->nGates - 2 - i ), 0 ) ); //printf( "dec %d for var %d\n", pSes->pStairDecFunc[i], j ); -- cgit v1.2.3