summaryrefslogtreecommitdiffstats
path: root/src/sat/pdr/pdrCore.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/pdr/pdrCore.c')
-rw-r--r--src/sat/pdr/pdrCore.c4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/sat/pdr/pdrCore.c b/src/sat/pdr/pdrCore.c
index 8b58bde1..742ce381 100644
--- a/src/sat/pdr/pdrCore.c
+++ b/src/sat/pdr/pdrCore.c
@@ -130,7 +130,7 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
int i, j, k, m, RetValue = 0, kMax = Vec_PtrSize(p->vSolvers)-1;
int Counter = 0;
int clk = clock();
- Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, 1, kMax-1 )
+ Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, 1, kMax )
{
Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
vArrayK1 = (Vec_Ptr_t *)Vec_VecEntry( p->vClauses, k+1 );
@@ -229,7 +229,7 @@ int Pdr_ManCheckContainment( Pdr_Man_t * p, int k, Pdr_Set_t * pSet )
Pdr_Set_t * pThis;
Vec_Ptr_t * vArrayK;
int i, j, kMax = Vec_PtrSize(p->vSolvers)-1;
- Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, i, k, kMax )
+ Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, i, k, kMax+1 )
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pThis, j )
if ( Pdr_SetContains( pSet, pThis ) )
return 1;