Corner-case bug in PDR.

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;

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);
 }