diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/sat/pdr/pdrCore.c | 8 | ||||
| -rw-r--r-- | src/sat/pdr/pdrSat.c | 3 |
2 files changed, 9 insertions, 2 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; diff --git a/src/sat/pdr/pdrSat.c b/src/sat/pdr/pdrSat.c index 79a675eb..627cb654 100644 --- a/src/sat/pdr/pdrSat.c +++ b/src/sat/pdr/pdrSat.c @@ -246,7 +246,8 @@ int Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ) pSat = Pdr_ManFetchSolver( p, k ); vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 0 ); RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 ); - assert( RetValue != l_Undef ); + if ( RetValue == l_Undef ) + return -1; return (RetValue == l_False); } |