Silencing warnings.

2 files changed, 6 insertions, 7 deletions

diff --git a/src/sat/bsat/satClause.h b/src/sat/bsat/satClause.h
index d5df71ad..79a43b4e 100644
--- a/src/sat/bsat/satClause.h
+++ b/src/sat/bsat/satClause.h
@@ -113,10 +113,11 @@ static inline double    Sat_MemMemoryAll( Sat_Mem_t * p )            { return 1.
 // k is page offset
 
 // this macro has to be fixed (Sat_MemClauseSize does not work for problem clauses in proof mode)
-//#define Sat_MemForEachClause( p, c, i, k )      \
-//    for ( i = 0; i <= p->iPage[0]; i += 2 )     \
-//        for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) )
-
+/*
+#define Sat_MemForEachClause( p, c, i, k )      \
+    for ( i = 0; i <= p->iPage[0]; i += 2 )     \
+        for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) )
+*/
 #define Sat_MemForEachLearned( p, c, i, k )     \
     for ( i = 1; i <= p->iPage[1]; i += 2 )     \
         for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) )
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 7597207b..bcd1921d 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -30,8 +30,6 @@ ABC_NAMESPACE_IMPL_START
 
 #define SAT_USE_PROOF_LOGGING
 
-static int Time = 0;
-
 //=================================================================================================
 // Debug:
  
@@ -1359,7 +1357,7 @@ void sat_solver2_reducedb(sat_solver2* s)
     int nLearnedOld = veci_size(&s->act_clas);
     int * act_clas = veci_begin(&s->act_clas);
     int * pPerm, * pSortValues, nCutoffValue, * pClaProofs;
-    int i, j, k, Id, nSelected, LastSize = 0;
+    int i, j, k, Id, nSelected;//, LastSize = 0;
     int Counter, CounterStart;
     clock_t clk = clock();
     static int Count = 0;