summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abci/abcExact.c5
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 );