C++ portability changes.

18 files changed, 57 insertions, 51 deletions

diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index 086ab0a8..538b23e9 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -1063,7 +1063,7 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fSkipS
         vFlopMap = pNew->vFlopClasses; pNew->vFlopClasses = NULL;
         vGateMap = pNew->vGateClasses; pNew->vGateClasses = NULL;
         vObjMap  = pNew->vObjClasses;  pNew->vObjClasses  = NULL;
-        pManTime = pNew->pManTime;     pNew->pManTime     = NULL;
+        pManTime = (Tim_Man_t *)pNew->pManTime; pNew->pManTime     = NULL;
         pNew = Gia_ManCleanup( pTemp = pNew );
         if ( (vGateMap || vObjMap) && (Gia_ManObjNum(pNew) < Gia_ManObjNum(pTemp)) )
             printf( "Cleanup removed objects after reading. Old gate/object abstraction maps are invalid!\n" );
@@ -1555,7 +1555,7 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
     // write timing information
     if ( p->pManTime )
     {
-        Vec_Str_t * vStr = Tim_ManSave( p->pManTime );
+        Vec_Str_t * vStr = Tim_ManSave( (Tim_Man_t *)p->pManTime );
         unsigned char Buffer[10];
         int nSize = Vec_StrSize(vStr);
         Gia_WriteInt( Buffer, nSize );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index e49ce616..da0551fc 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -923,7 +923,7 @@ Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p )
 ***********************************************************************/
 Gia_Man_t * Gia_ManDupUnnomalize( Gia_Man_t * p )
 {
-    Tim_Man_t * pTime = p->pManTime;
+    Tim_Man_t * pTime = (Tim_Man_t *)p->pManTime;
     Gia_Man_t * pNew;
     Gia_Obj_t * pObj;
     int i, k, curCi, curCo, curNo, nodeLim;
diff --git a/src/aig/saig/saigConstr.c b/src/aig/saig/saigConstr.c
index 682c46cf..5f54ef83 100644
--- a/src/aig/saig/saigConstr.c
+++ b/src/aig/saig/saigConstr.c
@@ -292,8 +292,8 @@ Aig_Man_t * Saig_ManDupUnfoldConstrs( Aig_Man_t * pAig )
             Vec_VecFree( (Vec_Vec_t *)vConsAll );
             return Aig_ManDupDfs( pAig );
         }
-        Vec_PtrSort( vOuts, Saig_ManDupCompare );
-        Vec_PtrSort( vCons, Saig_ManDupCompare );
+        Vec_PtrSort( vOuts, (int (*)(void))Saig_ManDupCompare );
+        Vec_PtrSort( vCons, (int (*)(void))Saig_ManDupCompare );
         Vec_PtrPush( vOutsAll, vOuts );
         Vec_PtrPush( vConsAll, vCons );
     }
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index 7c1c05be..0476ec92 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -66,7 +66,7 @@ Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, double AreaMulti,
     Vec_Int_t * vSwitching = NULL;
     float * pSwitching = NULL;
     clock_t clk, clkTotal = clock();
-    Mio_Library_t * pLib = Abc_FrameReadLibGen();
+    Mio_Library_t * pLib = (Mio_Library_t *)Abc_FrameReadLibGen();
 
     assert( Abc_NtkIsStrash(pNtk) );
 
@@ -102,9 +102,9 @@ Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, double AreaMulti,
 
     // return the library to normal
     if ( AreaMulti != 0.0 )
-        Mio_LibraryMultiArea( Abc_FrameReadLibGen(), -AreaMulti );
+        Mio_LibraryMultiArea( (Mio_Library_t *)Abc_FrameReadLibGen(), -AreaMulti );
     if ( DelayMulti != 0.0 )
-        Mio_LibraryMultiDelay( Abc_FrameReadLibGen(), -DelayMulti );
+        Mio_LibraryMultiDelay( (Mio_Library_t *)Abc_FrameReadLibGen(), -DelayMulti );
 
     // print a warning about choice nodes
     if ( Abc_NtkGetChoiceNum( pNtk ) )
diff --git a/src/base/abci/abcRec2.c b/src/base/abci/abcRec2.c
index c84ea3ea..460fe71d 100644
--- a/src/base/abci/abcRec2.c
+++ b/src/base/abci/abcRec2.c
@@ -163,7 +163,7 @@ static inline int Rec_AppendObj( Abc_ManRec_t2 * p, Rec_Obj_t2 ** pObj )
     if ( p->nRecObjs == p->nRecObjsAlloc )
     {
         assert( p->nRecObjs > 0 );
-        p->pRecObjs = realloc(p->pRecObjs, 2 * p->nRecObjsAlloc * p->recObjSize );
+        p->pRecObjs = ABC_REALLOC( char, p->pRecObjs, 2 * p->nRecObjsAlloc * p->recObjSize );
         memset( p->pRecObjs + p->nRecObjsAlloc * p->recObjSize, 0, p->recObjSize * p->nRecObjsAlloc );
         p->nRecObjsAlloc *= 2;
         hasRealloced = 1;
@@ -2177,7 +2177,7 @@ void Abc_NtkRecCutTruthFromLib2( Gia_Man_t * pGia2, Vec_Ptr_t * vNodes, int nLea
     Vec_PtrForEachEntry( Gia_Obj_t *, vNodes, pObj, i )
     {
         Gia_ObjSetCopyF(pGia2, 0, pObj, i);
-        pSims = Vec_PtrEntry(vTtTemps, i);
+        pSims = (unsigned *)Vec_PtrEntry(vTtTemps, i);
         if ( i < nLeaves )
         {
             Kit_TruthCopy( pSims, (unsigned *)Vec_PtrEntry(vTtElems, i), nInputs );
diff --git a/src/base/abci/abcTim.c b/src/base/abci/abcTim.c
index a9cc4b96..35f1186d 100644
--- a/src/base/abci/abcTim.c
+++ b/src/base/abci/abcTim.c
@@ -385,11 +385,11 @@ void Abc_NtkTestTim( Abc_Ntk_t * pNtk, int fVerbose )
     // create GIA manager (pGia) with hierarhy/timing manager attached (pGia->pManTime)
     // while assuming that some nodes are white boxes (see Abc_NodeIsWhiteBox)
     pGia = Abc_NtkTestTimDeriveGia( pNtk, fVerbose );
-    printf( "Created GIA manager for network with %d white boxes.\n", Tim_ManBoxNum(pGia->pManTime) );
+    printf( "Created GIA manager for network with %d white boxes.\n", Tim_ManBoxNum((Tim_Man_t *)pGia->pManTime) );
 
     // print the timing manager
     if ( fVerbose )
-        Tim_ManPrint( pGia->pManTime );
+        Tim_ManPrint( (Tim_Man_t *)pGia->pManTime );
 
     // test writing both managers into a file and reading them back
     Abc_NtkTestTimByWritingFile( pGia, "test1.aig" );
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index bb031200..72f5c9dc 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -607,7 +607,7 @@ int Io_ReadBlifReorderFormalNames( Vec_Ptr_t * vTokens, Mio_Gate_t * pGate, Mio_
             pName = (char *)Vec_PtrEntry(vTokens, nSize - 1);
             if ( !strncmp( pNamePin, pName, Length ) && pName[Length] == '=' ) // the last entry is pTwin
             {
-                pName = Vec_PtrPop( vTokens );
+                pName = (char *)Vec_PtrPop( vTokens );
                 Vec_PtrPush( vTokens, NULL );
                 Vec_PtrPush( vTokens, pName );
                 return 1;
diff --git a/src/bool/lucky/luckyInt.h b/src/bool/lucky/luckyInt.h
index 4801b961..f236693c 100644
--- a/src/bool/lucky/luckyInt.h
+++ b/src/bool/lucky/luckyInt.h
@@ -24,13 +24,16 @@
 #include <math.h>
 #include <time.h>
 
-
 // comment out this line to run Lucky Code outside of ABC
 #define _RUNNING_ABC_
 
 #ifdef _RUNNING_ABC_
+
 #include "misc/util/abc_global.h"
+#include "lucky.h"
+
 #else
+
 #define ABC_NAMESPACE_HEADER_START
 #define ABC_NAMESPACE_HEADER_END
 #define ABC_NAMESPACE_IMPL_START
@@ -42,6 +45,18 @@ typedef unsigned __int64  word;
 #define inline __inline  // compatible with MS VS 6.0
 #define ABC_ALLOC(type, num)    ((type *) malloc(sizeof(type) * (num)))
 // #define LUCKY_VERIFY
+
+typedef struct
+{
+    int varN;
+    int* swapArray;
+    int swapCtr;
+    int totalSwaps;
+    int* flipArray;
+    int flipCtr;
+    int totalFlips; 
+}permInfo;
+
 #endif
 
 
@@ -71,17 +86,6 @@ typedef struct
     int positionToSwap2;
 } swapInfo;
 
-typedef struct
-{
-    int varN;
-    int* swapArray;
-    int swapCtr;
-    int totalSwaps;
-    int* flipArray;
-    int flipCtr;
-    int totalFlips; 
-}permInfo;
-
 
 static inline void TimePrint( char* Message )
 {
diff --git a/src/bool/lucky/luckySwapIJ.c b/src/bool/lucky/luckySwapIJ.c
index 9901f9cb..d1170f45 100644
--- a/src/bool/lucky/luckySwapIJ.c
+++ b/src/bool/lucky/luckySwapIJ.c
@@ -76,7 +76,7 @@ void swap_ij_case3( word* f,int totalVars, int i, int j)
     shift = (wwj - wwi)/2;
     WORDS_IN_TT = Kit_TruthWordNum_64bit(totalVars);
     SizeOfBlock = sizeof(word)*wwi/2;
-    temp = malloc(SizeOfBlock);
+    temp = (word *)malloc(SizeOfBlock);
     for(y=wwj/2; y<WORDS_IN_TT; y+=wwj)
         for(x=y-shift; x<y; x+=wwi)
         {
diff --git a/src/map/mapper/mapperTree.c b/src/map/mapper/mapperTree.c
index 9bf74ff2..8c23417c 100644
--- a/src/map/mapper/mapperTree.c
+++ b/src/map/mapper/mapperTree.c
@@ -162,7 +162,7 @@ int Map_LibraryReadFileTree( Map_SuperLib_t * pLib, FILE * pFile, char *pFileNam
     }
 
     pLibName = strtok( pTemp, " \t\r\n" );
-    pLib->pGenlib = Abc_FrameReadLibGen();
+    pLib->pGenlib = (Mio_Library_t *)Abc_FrameReadLibGen();
     if ( pLib->pGenlib == NULL || strcmp( Mio_LibraryReadName(pLib->pGenlib), pLibName ) )
     {
         printf( "Supergate library \"%s\" requires the use of genlib library \"%s\".\n", pFileName, pLibName );
@@ -410,7 +410,7 @@ int Map_LibraryReadFileTreeStr( Map_SuperLib_t * pLib, Vec_Str_t * vStr, char *
     }
 
     pLibName = strtok( pTemp, " \t\r\n" );
-    pLib->pGenlib = Abc_FrameReadLibGen();
+    pLib->pGenlib = (Mio_Library_t *)Abc_FrameReadLibGen();
 //    if ( pLib->pGenlib == NULL || strcmp( , pLibName ) )
     if ( pLib->pGenlib == NULL || Map_LibraryCompareLibNames(Mio_LibraryReadName(pLib->pGenlib), pLibName) )
     {
diff --git a/src/map/scl/scl.c b/src/map/scl/scl.c
index ee474c7d..f5c9d914 100644
--- a/src/map/scl/scl.c
+++ b/src/map/scl/scl.c
@@ -120,7 +120,7 @@ int Scl_CommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
     // read new library
     Abc_SclLoad( pFileName, (SC_Lib **)&pAbc->pLibScl );
     if ( fVerbose )
-        Abc_SclWriteText( "scl_out.txt", pAbc->pLibScl );
+        Abc_SclWriteText( "scl_out.txt", (SC_Lib *)pAbc->pLibScl );
     return 0;
 
 usage:
@@ -221,7 +221,7 @@ int Scl_CommandPrint( Abc_Frame_t * pAbc, int argc, char **argv )
     }
 
     // save current library
-    Abc_SclPrintCells( pAbc->pLibScl );
+    Abc_SclPrintCells( (SC_Lib *)pAbc->pLibScl );
     return 0;
 
 usage:
@@ -274,7 +274,7 @@ int Scl_CommandPrintGS( Abc_Frame_t * pAbc, int argc, char **argv )
     }
 
     // save current library
-    Abc_SclPrintGateSizes( pAbc->pLibScl, Abc_FrameReadNtk(pAbc) );
+    Abc_SclPrintGateSizes( (SC_Lib *)pAbc->pLibScl, Abc_FrameReadNtk(pAbc) );
     return 0;
 
 usage:
@@ -344,7 +344,7 @@ int Scl_CommandStime( Abc_Frame_t * pAbc, int argc, char **argv )
         return 1;
     }
 
-    Abc_SclTimePerform( pAbc->pLibScl, Abc_FrameReadNtk(pAbc), fUseWireLoads, fShowAll, fShort );
+    Abc_SclTimePerform( (SC_Lib *)pAbc->pLibScl, Abc_FrameReadNtk(pAbc), fUseWireLoads, fShowAll, fShort );
     return 0;
 
 usage:
@@ -611,7 +611,7 @@ int Scl_CommandGsize( Abc_Frame_t * pAbc, int argc, char **argv )
         return 1;
     }
 
-    Abc_SclSizingPerform( pAbc->pLibScl, Abc_FrameReadNtk(pAbc), pPars );
+    Abc_SclSizingPerform( (SC_Lib *)pAbc->pLibScl, Abc_FrameReadNtk(pAbc), pPars );
     return 0;
 
 usage:
@@ -717,7 +717,7 @@ int Scl_CommandUpsize( Abc_Frame_t * pAbc, int argc, char **argv )
         return 1;
     }
 
-    Abc_SclUpsizePerform( pAbc->pLibScl, pNtk, Window, Ratio, nIters, fVerbose );
+    Abc_SclUpsizePerform( (SC_Lib *)pAbc->pLibScl, pNtk, Window, Ratio, nIters, fVerbose );
     return 0;
 
 usage:
@@ -782,7 +782,7 @@ int Scl_CommandMinsize( Abc_Frame_t * pAbc, int argc, char **argv )
         return 1;
     }
 
-    Abc_SclMinsizePerform( pAbc->pLibScl, pNtk, fVerbose );
+    Abc_SclMinsizePerform( (SC_Lib *)pAbc->pLibScl, pNtk, fVerbose );
     return 0;
 
 usage:
diff --git a/src/map/scl/sclBuff.c b/src/map/scl/sclBuff.c
index 5a438cd4..808cd1ec 100644
--- a/src/map/scl/sclBuff.c
+++ b/src/map/scl/sclBuff.c
@@ -136,7 +136,7 @@ Abc_Obj_t * Abc_SclPerformBufferingOne( Abc_Obj_t * pObj, int Degree, int fVerbo
     // collect fanouts and sort by reverse level
     vFanouts = Vec_PtrAlloc( Abc_ObjFanoutNum(pObj) );
     Abc_NodeCollectFanouts( pObj, vFanouts );
-    Vec_PtrSort( vFanouts, Abc_NodeCompareLevels );
+    Vec_PtrSort( vFanouts, (int (*)(void))Abc_NodeCompareLevels );
     // select the first Degree fanouts
     pBuffer = Abc_NtkCreateNodeBuf( pObj->pNtk, NULL );
     // check if it is possible to not increase level
diff --git a/src/map/scl/sclInt.h b/src/map/scl/sclInt.h
index bf2ee0f5..9474e24d 100644
--- a/src/map/scl/sclInt.h
+++ b/src/map/scl/sclInt.h
@@ -198,8 +198,8 @@ static inline SC_Cell *   SC_LibCell( SC_Lib * p, int i )          { return (SC_
 static inline SC_Pin  *   SC_CellPin( SC_Cell * p, int i )         { return (SC_Pin *)Vec_PtrEntry(p->vPins, i);                   }
 static inline Vec_Wrd_t * SC_CellFunc( SC_Cell * p )               { return SC_CellPin(p, p->n_inputs)->vFunc;                     }
 
-static inline double      SC_LibCapFf( SC_Lib * p, double cap )    { return cap * p->unit_cap_fst * pow(10, 15 - p->unit_cap_snd); }
-static inline double      SC_LibTimePs( SC_Lib * p, double time )  { return time * pow(10, 12 - p->unit_time);                     }
+static inline double      SC_LibCapFf( SC_Lib * p, double cap )    { return cap * p->unit_cap_fst * pow(10.0, 15 - p->unit_cap_snd); }
+static inline double      SC_LibTimePs( SC_Lib * p, double time )  { return time * pow(10.0, 12 - p->unit_time);                     }
 
 #define SC_LibForEachCell( p, pCell, i )         Vec_PtrForEachEntry( SC_Cell *, p->vCells, pCell, i )
 #define SC_LibForEachCellClass( p, pCell, i )    Vec_PtrForEachEntry( SC_Cell *, p->vCellClasses, pCell, i )
diff --git a/src/map/scl/sclUtil.c b/src/map/scl/sclUtil.c
index f3a88e72..6a1f6a36 100644
--- a/src/map/scl/sclUtil.c
+++ b/src/map/scl/sclUtil.c
@@ -20,6 +20,7 @@
 
 #include "sclInt.h"
 #include "map/mio/mio.h"
+#include "bool/kit/kit.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -135,7 +136,7 @@ void Abc_SclLinkCells( SC_Lib * p )
             Vec_PtrPush( vList, pCell );
         qsort( (void *)Vec_PtrArray(vList), Vec_PtrSize(vList), sizeof(void *), (int(*)(const void *,const void *))Abc_SclCompareCells );
         // create new representative
-        pRepr = Vec_PtrEntry( vList, 0 );
+        pRepr = (SC_Cell *)Vec_PtrEntry( vList, 0 );
         pRepr->pNext = pRepr->pPrev = pRepr;
         pRepr->Order = 0;
         // relink cells
@@ -152,7 +153,6 @@ void Abc_SclLinkCells( SC_Lib * p )
 }
 void Abc_SclPrintCells( SC_Lib * p )
 {
-    extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
     SC_Cell * pCell, * pRepr;
     int i, k, j, nLength = 0;
     assert( Vec_PtrSize(p->vCellClasses) > 0 );
diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h
index 997c026e..03474a04 100644
--- a/src/misc/util/abc_global.h
+++ b/src/misc/util/abc_global.h
@@ -264,6 +264,12 @@ enum Abc_VerbLevel
     ABC_VERBOSE  =  2
 };
 
+// string printing
+extern char * vnsprintf(const char* format, va_list args);
+extern char * nsprintf(const char* format, ...);
+extern int Gia_ManToBridgeText( FILE * pFile, int Size, unsigned char * pBuffer );
+
+// misc printing procedures
 static inline void Abc_Print( int level, const char * format, ... )
 {
     extern ABC_DLL int Abc_FrameIsBridgeMode();
@@ -275,8 +281,6 @@ static inline void Abc_Print( int level, const char * format, ... )
     va_start( args, format );
     if ( Abc_FrameIsBridgeMode() )
     {
-        extern int Gia_ManToBridgeText( FILE * pFile, int Size, unsigned char * pBuffer );
-        extern char * vnsprintf(const char* format, va_list args);
         char * tmp = vnsprintf( format, args );
         Gia_ManToBridgeText( stdout, strlen(tmp), (unsigned char*)tmp );
         free( tmp );
@@ -362,9 +366,6 @@ extern void   Abc_QuickSort3( word * pData, int nSize, int fDecrease );
 extern void   Abc_QuickSortCostData( int * pCosts, int nSize, int fDecrease, word * pData, int * pResult );
 extern int *  Abc_QuickSortCost( int * pCosts, int nSize, int fDecrease );
 
-// string printing
-extern char * vnsprintf(const char* format, va_list args);
-extern char * nsprintf(const char* format, ...);
 
 
 ABC_NAMESPACE_HEADER_END
diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c
index 2b2cb8ea..698ab377 100644
--- a/src/proof/abs/absGla.c
+++ b/src/proof/abs/absGla.c
@@ -18,9 +18,10 @@
 
 ***********************************************************************/
 
+#include "base/main/main.h"
 #include "sat/cnf/cnf.h"
 #include "sat/bsat/satSolver2.h"
-#include "base/main/main.h"
+#include "bool/kit/kit.h"
 #include "abs.h"
 #include "absRef.h"
 //#include "absRef2.h"
@@ -83,8 +84,8 @@ struct Ga2_Man_t_
 static inline int         Ga2_ObjId( Ga2_Man_t * p, Gia_Obj_t * pObj )           { return Vec_IntEntry(p->vIds, Gia_ObjId(p->pGia, pObj));                                                  }
 static inline void        Ga2_ObjSetId( Ga2_Man_t * p, Gia_Obj_t * pObj, int i ) { Vec_IntWriteEntry(p->vIds, Gia_ObjId(p->pGia, pObj), i);                                                 }
 
-static inline Vec_Int_t * Ga2_ObjCnf0( Ga2_Man_t * p, Gia_Obj_t * pObj )         { assert(Ga2_ObjId(p,pObj) >= 0); return Vec_PtrEntry( p->vCnfs, 2*Ga2_ObjId(p,pObj)   );                  }
-static inline Vec_Int_t * Ga2_ObjCnf1( Ga2_Man_t * p, Gia_Obj_t * pObj )         { assert(Ga2_ObjId(p,pObj) >= 0); return Vec_PtrEntry( p->vCnfs, 2*Ga2_ObjId(p,pObj)+1 );                  }
+static inline Vec_Int_t * Ga2_ObjCnf0( Ga2_Man_t * p, Gia_Obj_t * pObj )         { assert(Ga2_ObjId(p,pObj) >= 0); return (Vec_Int_t *)Vec_PtrEntry( p->vCnfs, 2*Ga2_ObjId(p,pObj)   );                  }
+static inline Vec_Int_t * Ga2_ObjCnf1( Ga2_Man_t * p, Gia_Obj_t * pObj )         { assert(Ga2_ObjId(p,pObj) >= 0); return (Vec_Int_t *)Vec_PtrEntry( p->vCnfs, 2*Ga2_ObjId(p,pObj)+1 );                  }
 
 static inline int         Ga2_ObjIsAbs0( Ga2_Man_t * p, Gia_Obj_t * pObj )       { assert(Ga2_ObjId(p,pObj) >= 0); return Ga2_ObjId(p,pObj) >= 0         && Ga2_ObjId(p,pObj) < p->LimAbs;  }
 static inline int         Ga2_ObjIsLeaf0( Ga2_Man_t * p, Gia_Obj_t * pObj )      { assert(Ga2_ObjId(p,pObj) >= 0); return Ga2_ObjId(p,pObj) >= p->LimAbs && Ga2_ObjId(p,pObj) < p->LimPpi;  }
@@ -628,7 +629,6 @@ if ( fVerbose )
 ***********************************************************************/
 Vec_Int_t * Ga2_ManCnfCompute( unsigned uTruth, int nVars, Vec_Int_t * vCover )
 {
-    extern int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth );
     int RetValue;
     assert( nVars <= 5 );
     // transform truth table into the SOP
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 74393a5b..951940b3 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -1552,8 +1552,10 @@ void sat_solver2_reducedb(sat_solver2* s)
 
     // compact proof (compacts 'proofs' and update 'claProofs')
     if ( s->pPrf1 )
+    {
+        extern int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot );
         s->hProofPivot = Sat_ProofReduce( s->pPrf1, &s->claProofs, s->hProofPivot );
-
+    }
 
     // report the results
     TimeTotal += clock() - clk;
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index a1539637..8c32cbde 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -70,7 +70,6 @@ extern void         var_set_partA  (sat_solver2* s, int v, int partA);
 extern void *       Sat_ProofCore( sat_solver2 * s );
 extern void *       Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars );
 extern word *       Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars );
-extern int          Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot );
 extern void         Sat_ProofCheck( sat_solver2 * s );
 
 //=================================================================================================