diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-11-11 19:29:15 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-11-11 19:29:15 -0800 |
| commit | 9fe4c74952691c3a6cc87dc85edb43da11dd8c8e (patch) | |
| tree | 667b596287a3cb9d114dab498948a6587653eb7a | |
| parent | 8e6d4d3fe95e87d65dcf70296bafa9749204daae (diff) | |
| download | abc-9fe4c74952691c3a6cc87dc85edb43da11dd8c8e.tar.gz abc-9fe4c74952691c3a6cc87dc85edb43da11dd8c8e.tar.bz2 abc-9fe4c74952691c3a6cc87dc85edb43da11dd8c8e.zip | |
Corner-case bug in PDR.
| -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); } |