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 /src/sat/pdr/pdrSat.c | |
| parent | 8e6d4d3fe95e87d65dcf70296bafa9749204daae (diff) | |
| download | abc-9fe4c74952691c3a6cc87dc85edb43da11dd8c8e.tar.gz abc-9fe4c74952691c3a6cc87dc85edb43da11dd8c8e.tar.bz2 abc-9fe4c74952691c3a6cc87dc85edb43da11dd8c8e.zip | |
Corner-case bug in PDR.
Diffstat (limited to 'src/sat/pdr/pdrSat.c')
| -rw-r--r-- | src/sat/pdr/pdrSat.c | 3 |
1 files changed, 2 insertions, 1 deletions
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); } |