Silencing warnings.

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

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;