diff options
Diffstat (limited to 'src/sat/pdr/pdrCore.c')
| -rw-r--r-- | src/sat/pdr/pdrCore.c | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/sat/pdr/pdrCore.c b/src/sat/pdr/pdrCore.c index e3c3781f..6b1e4850 100644 --- a/src/sat/pdr/pdrCore.c +++ b/src/sat/pdr/pdrCore.c @@ -443,7 +443,13 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube ) p->tContain += clock() - clk; // check if the cube is already contained - if ( Pdr_ManCheckCubeCs( p, pThis->iFrame, pThis->pState ) ) // cube is blocked by clauses in this frame + RetValue = Pdr_ManCheckCubeCs( p, pThis->iFrame, pThis->pState ); + if ( RetValue == -1 ) // cube is blocked by clauses in this frame + { + Pdr_OblDeref( pThis ); + return -1; + } + if ( RetValue ) // cube is blocked by clauses in this frame { Pdr_OblDeref( pThis ); continue; |