diff options
| author | Mathias Soeken <mathias.soeken@epfl.ch> | 2016-09-09 15:39:33 +0200 |
|---|---|---|
| committer | Mathias Soeken <mathias.soeken@epfl.ch> | 2016-09-09 15:39:33 +0200 |
| commit | b44c519620c6174241f7ab942f07e9db9e9e0e5b (patch) | |
| tree | 02b8ded31989617bc06957d02d6904c606ceedcd /src | |
| parent | 2f2ed1bce15575f37e3a96e3c2f3f9a139e3922e (diff) | |
| download | abc-b44c519620c6174241f7ab942f07e9db9e9e0e5b.tar.gz abc-b44c519620c6174241f7ab942f07e9db9e9e0e5b.tar.bz2 abc-b44c519620c6174241f7ab942f07e9db9e9e0e5b.zip | |
Fix in BMS.
Diffstat (limited to 'src')
| -rw-r--r-- | src/base/abci/abcExact.c | 5 |
1 files changed, 5 insertions, 0 deletions
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 ); |