Version abc60804

3 files changed, 6 insertions, 6 deletions

diff --git a/src/sat/msat/msatActivity.c b/src/sat/msat/msatActivity.c
index f808d9bc..23925669 100644
--- a/src/sat/msat/msatActivity.c
+++ b/src/sat/msat/msatActivity.c
@@ -46,7 +46,7 @@ void Msat_SolverVarBumpActivity( Msat_Solver_t * p, Msat_Lit_t Lit )
         return;
     Var = MSAT_LIT2VAR(Lit);
     if ( (p->pdActivity[Var] += p->dVarInc) > 1e100 )
-//    if ( (p->pdActivity[Var] += p->dVarInc * (1.0 + 0.005*p->pLevel[Var])) > 1e100 )
+//    if ( (p->pdActivity[Var] += p->dVarInc * (1.0 + 0.005*p->pActLevels[Var])) > 1e100 )
         Msat_SolverVarRescaleActivity( p );
     Msat_OrderUpdate( p->pOrder, Var );
 }
diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h
index 15932c67..7845ec0b 100644
--- a/src/sat/msat/msatInt.h
+++ b/src/sat/msat/msatInt.h
@@ -119,7 +119,7 @@ struct Msat_Solver_t_
     double              dClaDecay;   // INVERSE decay factor for clause activity: stores 1/decay.
 
     double *            pdActivity;  // A heuristic measurement of the activity of a variable.
-    int *               pLevels;     // the levels of the variables
+    int *               pActLevels;  // the levels of the variables
     double              dVarInc;     // Amount to bump next variable with.
     double              dVarDecay;   // INVERSE decay factor for variable activity: stores 1/decay. Use negative value for static variable order.
     Msat_Order_t *      pOrder;      // Keeps track of the decision variable order.
diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c
index 8c1542df..9317dcac 100644
--- a/src/sat/msat/msatSolverApi.c
+++ b/src/sat/msat/msatSolverApi.c
@@ -174,11 +174,11 @@ Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc,
     p->dVarDecay = dVarDecay;
 
     p->pdActivity = ALLOC( double, p->nVarsAlloc );
-    p->pLevels    = ALLOC( int, p->nVarsAlloc );
+    p->pActLevels = ALLOC( int, p->nVarsAlloc );
     for ( i = 0; i < p->nVarsAlloc; i++ )
     {
         p->pdActivity[i] = 0;
-        p->pLevels = 0;
+        p->pActLevels[i] = 0;
     }
 
     p->pAssigns  = ALLOC( int, p->nVarsAlloc ); 
@@ -243,7 +243,7 @@ void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc )
     p->nVarsAlloc = nVarsAlloc;
 
     p->pdActivity = REALLOC( double, p->pdActivity, p->nVarsAlloc );
-    p->pLevels    = REALLOC( int, p->pLevels, p->nVarsAlloc );
+    p->pActLevels = REALLOC( int, p->pActLevels, p->nVarsAlloc );
     for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
         p->pdActivity[i] = 0;
 
@@ -399,7 +399,7 @@ void Msat_SolverFree( Msat_Solver_t * p )
     Msat_ClauseVecFree( p->vLearned );
 
     FREE( p->pdActivity );
-    FREE( p->pLevels );
+    FREE( p->pActLevels );
     Msat_OrderFree( p->pOrder );
 
     for ( i = 0; i < 2 * p->nVarsAlloc; i++ )