The cube in PDR can have more than 2^15 literals.

src/sat/pdr/pdrInt.h

@@ -45,8 +45,8 @@ struct Pdr_Set_t_
 {
     word        Sign;      // signature
     int         nRefs;     // ref counter
-    short       nTotal;    // total literals
-    short       nLits;     // num flop literals
+    int         nTotal;    // total literals
+    int         nLits;     // num flop literals
     int         Lits[0];
 };
 

src/sat/pdr/pdrUtil.c

@@ -46,7 +46,7 @@ ABC_NAMESPACE_IMPL_START
 Pdr_Set_t * Pdr_SetAlloc( int nSize )
 {
     Pdr_Set_t * p;
-    assert( nSize < (1<<15) );
+    assert( nSize >= 0 && nSize < (1<<30) );
     p = (Pdr_Set_t *)ABC_CALLOC( char, sizeof(Pdr_Set_t) + nSize * sizeof(int) );
     return p;
 }
@@ -66,7 +66,7 @@ Pdr_Set_t * Pdr_SetCreate( Vec_Int_t * vLits, Vec_Int_t * vPiLits )
 {
     Pdr_Set_t * p;
     int i;
-    assert( Vec_IntSize(vLits) + Vec_IntSize(vPiLits) < (1<<15) );
+    assert( Vec_IntSize(vLits) + Vec_IntSize(vPiLits) < (1<<30) );
     p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + (Vec_IntSize(vLits) + Vec_IntSize(vPiLits)) * sizeof(int) );
     p->nLits  = Vec_IntSize(vLits);
     p->nTotal = Vec_IntSize(vLits) + Vec_IntSize(vPiLits);