Version abc80702

3 files changed, 5 insertions, 7 deletions

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",