Version abc80702

7 files changed, 13 insertions, 15 deletions

diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
index 5872f5bc..e755d8d4 100644
--- a/src/sat/csat/csat_apis.c
+++ b/src/sat/csat/csat_apis.c
@@ -169,8 +169,10 @@ void ABC_UseOnlyCoreSatSolver( ABC_Manager mng )
 ***********************************************************************/
 int ABC_AddGate( ABC_Manager mng, enum GateType type, char * name, int nofi, char ** fanins, int dc_attr )
 {
-    Abc_Obj_t * pObj, * pFanin;
-    char * pSop, * pNewName;
+    Abc_Obj_t * pObj = NULL; // Suppress "might be used uninitialized"
+    Abc_Obj_t * pFanin;
+    char * pSop = NULL; // Suppress "might be used uninitialized"
+    char * pNewName;
     int i;
 
     // save the name in the local memory manager
diff --git a/src/sat/fraig/fraigFeed.c b/src/sat/fraig/fraigFeed.c
index 8a3cc6c7..e1e8d12c 100644
--- a/src/sat/fraig/fraigFeed.c
+++ b/src/sat/fraig/fraigFeed.c
@@ -634,7 +634,6 @@ void Fraig_FeedBackCheckTable( Fraig_Man_t * p )
     Fraig_HashTable_t * pT = p->pTableF;
     Fraig_Node_t * pEntF, * pEntD;
     int i, k, m, nPairs;
-    int clk = clock();
 
     nPairs = 0;
     for ( i = 0; i < pT->nBins; i++ )
diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h
index dc7bc815..c13d7083 100644
--- a/src/sat/fraig/fraigInt.h
+++ b/src/sat/fraig/fraigInt.h
@@ -107,7 +107,7 @@
 // copied from "extra.h" for stand-aloneness
 #define Fraig_PrintTime(a,t)      printf( "%s = ", (a) ); printf( "%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) )
 
-#define Fraig_HashKey2(a,b,TSIZE) (((unsigned)(a) + (unsigned)(b) * 12582917) % TSIZE)
+#define Fraig_HashKey2(a,b,TSIZE) (((PORT_PTRUINT_T)(a) + (PORT_PTRUINT_T)(b) * 12582917) % TSIZE)
 //#define Fraig_HashKey2(a,b,TSIZE) (( ((unsigned)(a)->Num * 19) ^ ((unsigned)(b)->Num * 1999) ) % TSIZE)
 //#define Fraig_HashKey2(a,b,TSIZE) ( ((unsigned)((a)->Num + (b)->Num) * ((a)->Num + (b)->Num + 1) / 2) % TSIZE)
 // the other two hash functions give bad distribution of hash chain lengths (not clear why)
diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c
index 12cb5c45..cbeef4c6 100644
--- a/src/sat/fraig/fraigMan.c
+++ b/src/sat/fraig/fraigMan.c
@@ -95,13 +95,13 @@ void Prove_ParamsPrint( Prove_Params_t * pParams )
     printf( "Multiplicative coeficient for mitering: %.2f\n", pParams->nMiteringLimitMulti );
     printf( "Starting number of rewriting iterations: %d\n", pParams->nRewritingLimitStart );
     printf( "Multiplicative coeficient for rewriting: %.2f\n", pParams->nRewritingLimitMulti );
-    printf( "Starting number of conflicts in fraiging: %d\n", pParams->nFraigingLimitMulti );
+    printf( "Starting number of conflicts in fraiging: %.2f\n", pParams->nFraigingLimitMulti );
     printf( "Multiplicative coeficient for fraiging: %.2f\n", pParams->nRewritingLimitMulti );
-    printf( "BDD size limit for bailing out: %.2f\n", pParams->nBddSizeLimit );
+    printf( "BDD size limit for bailing out: %d\n", pParams->nBddSizeLimit );
     printf( "BDD reordering enabled: %s\n", pParams->fBddReorder? "yes":"no" );
     printf( "Last-gasp mitering limit: %d\n", pParams->nMiteringLimitLast );
-    printf( "Total conflict limit: %d\n", pParams->nTotalBacktrackLimit );
-    printf( "Total inspection limit: %d\n", pParams->nTotalInspectLimit );
+    printf( "Total conflict limit: %lld\n", pParams->nTotalBacktrackLimit );
+    printf( "Total inspection limit: %lld\n", pParams->nTotalInspectLimit );
     printf( "Parameter dump complete.\n" );
 }
 
@@ -347,7 +347,6 @@ void Fraig_ManCreateSolver( Fraig_Man_t * p )
 void Fraig_ManPrintStats( Fraig_Man_t * p )
 {
     double nMemory;
-    int clk = clock();
     nMemory = ((double)(p->vInputs->nSize + p->vNodes->nSize) * 
         (sizeof(Fraig_Node_t) + sizeof(unsigned)*(p->nWordsRand + p->nWordsDyna) /*+ p->nSuppWords*sizeof(unsigned)*/))/(1<<20);
     printf( "Words: Random = %d. Dynamic = %d. Used = %d. Memory = %0.2f Mb.\n", 
diff --git a/src/sat/msat/msatRead.c b/src/sat/msat/msatRead.c
index 738562ef..20453fed 100644
--- a/src/sat/msat/msatRead.c
+++ b/src/sat/msat/msatRead.c
@@ -196,8 +196,8 @@ static void Msat_ReadClause( char ** pIn, Msat_Solver_t * p, Msat_IntVec_t * pLi
 ***********************************************************************/
 static bool Msat_ReadDimacs( char * pText, Msat_Solver_t ** pS, bool fVerbose ) 
 {
-    Msat_Solver_t * p;
-    Msat_IntVec_t * pLits;
+    Msat_Solver_t * p = NULL; // Suppress "might be used uninitialized"
+    Msat_IntVec_t * pLits = NULL; // Suppress "might be used uninitialized"
     char * pIn = pText;
     int nVars, nClas;
     while ( 1 )
diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c
index f9fee73c..e86ab511 100644
--- a/src/sat/msat/msatSolverCore.c
+++ b/src/sat/msat/msatSolverCore.c
@@ -138,8 +138,6 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra
     double nConflictsLimit, nLearnedLimit;
     Msat_Type_t Status;
     int timeStart = clock();
-    int64 nConflictsOld = p->Stats.nConflicts;
-    int64 nDecisionsOld = p->Stats.nDecisions;
 
 //    p->pFreq = ALLOC( int, p->nVarsAlloc );
 //    memset( p->pFreq, 0, sizeof(int) * p->nVarsAlloc );
diff --git a/src/sat/msat/msatVec.c b/src/sat/msat/msatVec.c
index 75f53047..36ad55ba 100644
--- a/src/sat/msat/msatVec.c
+++ b/src/sat/msat/msatVec.c
@@ -399,8 +399,8 @@ void Msat_IntVecPushUniqueOrder( Msat_IntVec_t * p, int Entry, int fIncrease )
     {
         Entry1 = p->pArray[i  ];
         Entry2 = p->pArray[i-1];
-        if ( fIncrease && Entry1 >= Entry2 || 
-            !fIncrease && Entry1 <= Entry2 )
+        if (( fIncrease && Entry1 >= Entry2) ||
+            (!fIncrease && Entry1 <= Entry2) )
             break;
         p->pArray[i  ] = Entry2;
         p->pArray[i-1] = Entry1;