Fixes to make xSAT compile with old compilers.

Small typos and variables renaming.

8 files changed, 119 insertions, 136 deletions

diff --git a/src/sat/xsat/xsatBQueue.h b/src/sat/xsat/xsatBQueue.h
index 6c170c93..560f75c0 100644
--- a/src/sat/xsat/xsatBQueue.h
+++ b/src/sat/xsat/xsatBQueue.h
@@ -24,7 +24,6 @@
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
-
 #include "misc/util/abc_global.h"
 
 ABC_NAMESPACE_HEADER_START
@@ -32,7 +31,6 @@ ABC_NAMESPACE_HEADER_START
 ////////////////////////////////////////////////////////////////////////
 ///                    STRUCTURE DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
-
 typedef struct xSAT_BQueue_t_ xSAT_BQueue_t;
 struct xSAT_BQueue_t_
 {
@@ -41,13 +39,12 @@ struct xSAT_BQueue_t_
     int iFirst;
     int iEmpty;
     word nSum;
-    word * pData;
+    unsigned * pData;
 };
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DECLARATIONS                        ///
 ////////////////////////////////////////////////////////////////////////
-
 /**Function*************************************************************
 
   Synopsis    []
@@ -63,7 +60,7 @@ static inline xSAT_BQueue_t * xSAT_BQueueNew( int nCap )
 {
     xSAT_BQueue_t * p = ABC_CALLOC( xSAT_BQueue_t, 1 );
     p->nCap = nCap;
-    p->pData = ABC_CALLOC( word, nCap );
+    p->pData = ABC_CALLOC( unsigned, nCap );
     return p;
 }
 
@@ -95,7 +92,7 @@ static inline void xSAT_BQueueFree( xSAT_BQueue_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-static inline void xSAT_BQueuePush( xSAT_BQueue_t * p, word Value )
+static inline void xSAT_BQueuePush( xSAT_BQueue_t * p, unsigned Value )
 {
     if ( p->nSize == p->nCap )
     {
@@ -128,8 +125,8 @@ static inline void xSAT_BQueuePush( xSAT_BQueue_t * p, word Value )
 ***********************************************************************/
 static inline int xSAT_BQueuePop( xSAT_BQueue_t * p )
 {
-    int RetValue = p->pData[p->iFirst];
     assert( p->nSize >= 1 );
+    int RetValue = p->pData[p->iFirst];
     p->nSum -= RetValue;
     p->iFirst = ( p->iFirst + 1 ) % p->nCap;
     p->nSize--;
@@ -147,9 +144,9 @@ static inline int xSAT_BQueuePop( xSAT_BQueue_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-static inline word xSAT_BQueueAvg( xSAT_BQueue_t * p )
+static inline unsigned xSAT_BQueueAvg( xSAT_BQueue_t * p )
 {
-    return ( word )( p->nSum / ( ( word ) p->nSize ) );
+    return ( unsigned )( p->nSum / ( ( word ) p->nSize ) );
 }
 
 /**Function*************************************************************
diff --git a/src/sat/xsat/xsatClause.h b/src/sat/xsat/xsatClause.h
index d05eb6de..ef353198 100644
--- a/src/sat/xsat/xsatClause.h
+++ b/src/sat/xsat/xsatClause.h
@@ -39,7 +39,7 @@ struct xSAT_Clause_t_
     unsigned fReallocd :  1;
     unsigned fCanBeDel :  1;
     unsigned nLBD      : 28;
-    unsigned nSize;
+    int nSize;
     union {
         int Lit;
         unsigned Act;
@@ -60,7 +60,7 @@ struct xSAT_Clause_t_
   SeeAlso     []
 
 ***********************************************************************/
-static int xSAT_ClauseCompare( const void * p1, const void * p2 )
+static inline int xSAT_ClauseCompare( const void * p1, const void * p2 )
 {
     xSAT_Clause_t * pC1 = ( xSAT_Clause_t * ) p1;
     xSAT_Clause_t * pC2 = ( xSAT_Clause_t * ) p2;
@@ -91,12 +91,12 @@ static int xSAT_ClauseCompare( const void * p1, const void * p2 )
   SeeAlso     []
 
 ***********************************************************************/
-static void xSAT_ClausePrint( xSAT_Clause_t * pCla )
+static inline void xSAT_ClausePrint( xSAT_Clause_t * pCla )
 {
     int i;
 
     printf("{ ");
-    for ( i = 0; i < (int)pCla->nSize; i++ )
+    for ( i = 0; i < pCla->nSize; i++ )
         printf("%d ", pCla->pData[i].Lit );
     printf("}\n");
 }
diff --git a/src/sat/xsat/xsatHeap.h b/src/sat/xsat/xsatHeap.h
index 409ce460..2e873e59 100644
--- a/src/sat/xsat/xsatHeap.h
+++ b/src/sat/xsat/xsatHeap.h
@@ -48,7 +48,7 @@ struct xSAT_Heap_t_
   SeeAlso     []
 
 ***********************************************************************/
-static inline int xSAT_HeapSize( xSAT_Heap_t * h )
+inline int xSAT_HeapSize( xSAT_Heap_t * h )
 {
     return Vec_IntSize( h->vHeap );
 }
@@ -64,7 +64,7 @@ static inline int xSAT_HeapSize( xSAT_Heap_t * h )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int xSAT_HeapInHeap( xSAT_Heap_t * h, int Var )
+inline int xSAT_HeapInHeap( xSAT_Heap_t * h, int Var )
 {
     return ( Var < Vec_IntSize( h->vIndices ) ) && ( Vec_IntEntry( h->vIndices, Var ) >= 0 );
 }
diff --git a/src/sat/xsat/xsatMemory.h b/src/sat/xsat/xsatMemory.h
index 3324a563..129c2f50 100644
--- a/src/sat/xsat/xsatMemory.h
+++ b/src/sat/xsat/xsatMemory.h
@@ -77,16 +77,14 @@ static inline void xSAT_MemGrow( xSAT_Mem_t * p, unsigned nCap )
     unsigned nPrevCap = p->nCap;
     if ( p->nCap >= nCap )
         return;
-
     while (p->nCap < nCap)
     {
-        unsigned delta = ((p->nCap >> 1) + (p->nCap >> 3) + 2) & ~1;
+        unsigned delta = ( ( p->nCap >> 1 ) + ( p->nCap >> 3 ) + 2 ) & ~1;
         p->nCap += delta;
         assert(p->nCap >= nPrevCap);
     }
-
     assert(p->nCap > 0);
-    p->pData = ABC_REALLOC(unsigned, p->pData, p->nCap);
+    p->pData = ABC_REALLOC( unsigned, p->pData, p->nCap );
 }
 
 /**Function*************************************************************
@@ -160,12 +158,10 @@ static inline unsigned xSAT_MemAppend( xSAT_Mem_t * p, int nSize )
 {
     unsigned nPrevSize;
     assert(nSize > 0);
-    xSAT_MemGrow(p, p->nSize + nSize);
-
+    xSAT_MemGrow( p, p->nSize + nSize );
     nPrevSize = p->nSize;
     p->nSize += nSize;
     assert(p->nSize > nPrevSize);
-
     return nPrevSize;
 }
 
diff --git a/src/sat/xsat/xsatSolver.c b/src/sat/xsat/xsatSolver.c
index 5806409e..467f5f8d 100644
--- a/src/sat/xsat/xsatSolver.c
+++ b/src/sat/xsat/xsatSolver.c
@@ -46,7 +46,7 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-static inline int xSAT_SolverDecide( xSAT_Solver_t* s )
+static inline int xSAT_SolverDecide( xSAT_Solver_t * s )
 {
     int NextVar = VarUndef;
 
@@ -74,7 +74,7 @@ static inline int xSAT_SolverDecide( xSAT_Solver_t* s )
   SeeAlso     []
 
 ***********************************************************************/
-void xSAT_SolverRebuildOrderHeap( xSAT_Solver_t* s )
+void xSAT_SolverRebuildOrderHeap( xSAT_Solver_t * s )
 {
     Vec_Int_t * vTemp = Vec_IntAlloc( Vec_StrSize( s->vAssigns ) );
     int Var;
@@ -100,14 +100,14 @@ void xSAT_SolverRebuildOrderHeap( xSAT_Solver_t* s )
 ***********************************************************************/
 static inline void xSAT_SolverVarActRescale( xSAT_Solver_t * s )
 {
-    unsigned * pActivity = (unsigned *) Vec_IntArray( s->vActivity );
     int i;
+    unsigned * pActivity = ( unsigned * ) Vec_IntArray( s->vActivity );
 
     for ( i = 0; i < Vec_IntSize( s->vActivity ); i++ )
         pActivity[i] >>= 19;
 
     s->nVarActInc >>= 19;
-    s->nVarActInc = Abc_MaxInt( s->nVarActInc, (1 << 5) );
+    s->nVarActInc = Abc_MaxInt( s->nVarActInc, ( 1 << 5 ) );
 }
 
 /**Function*************************************************************
@@ -121,9 +121,9 @@ static inline void xSAT_SolverVarActRescale( xSAT_Solver_t * s )
   SeeAlso     []
 
 ***********************************************************************/
-static inline void xSAT_SolverVarActBump( xSAT_Solver_t* s, int Var )
+static inline void xSAT_SolverVarActBump( xSAT_Solver_t * s, int Var )
 {
-    unsigned * pActivity = (unsigned *) Vec_IntArray( s->vActivity );
+    unsigned * pActivity = ( unsigned * ) Vec_IntArray( s->vActivity );
 
     pActivity[Var] += s->nVarActInc;
     if ( pActivity[Var] & 0x80000000 )
@@ -167,7 +167,7 @@ static inline void xSAT_SolverClaActRescale( xSAT_Solver_t * s )
 
     Vec_IntForEachEntry( s->vLearnts, CRef, i )
     {
-        pC = xSAT_SolverReadClause( s, (unsigned) CRef );
+        pC = xSAT_SolverReadClause( s, ( unsigned ) CRef );
         pC->pData[pC->nSize].Act >>= 14;
     }
     s->nClaActInc >>= 14;
@@ -221,16 +221,16 @@ static inline void xSAT_SolverClaActDecay( xSAT_Solver_t * s )
 ***********************************************************************/
 static inline int xSAT_SolverClaCalcLBD( xSAT_Solver_t * s, xSAT_Clause_t * pCla )
 {
-    int nLBD = 0;
     int i;
+    int nLBD = 0;
 
     s->nStamp++;
-    for ( i = 0; i < (int)pCla->nSize; i++ )
+    for ( i = 0; i < pCla->nSize; i++ )
     {
         int Level = Vec_IntEntry( s->vLevels, xSAT_Lit2Var( pCla->pData[i].Lit ) );
-        if ( (unsigned) Vec_IntEntry( s->vStamp, Level ) != s->nStamp )
+        if ( ( unsigned ) Vec_IntEntry( s->vStamp, Level ) != s->nStamp )
         {
-            Vec_IntWriteEntry( s->vStamp, Level, (int) s->nStamp );
+            Vec_IntWriteEntry( s->vStamp, Level, ( int ) s->nStamp );
             nLBD++;
         }
     }
@@ -239,16 +239,16 @@ static inline int xSAT_SolverClaCalcLBD( xSAT_Solver_t * s, xSAT_Clause_t * pCla
 
 static inline int xSAT_SolverClaCalcLBD2( xSAT_Solver_t * s, Vec_Int_t * vLits )
 {
-    int nLBD = 0;
     int i;
+    int nLBD = 0;
 
     s->nStamp++;
     for ( i = 0; i < Vec_IntSize( vLits ); i++ )
     {
         int Level = Vec_IntEntry( s->vLevels, xSAT_Lit2Var( Vec_IntEntry( vLits, i ) ) );
-        if ( (unsigned) Vec_IntEntry( s->vStamp, Level ) != s->nStamp )
+        if ( ( unsigned ) Vec_IntEntry( s->vStamp, Level ) != s->nStamp )
         {
-            Vec_IntWriteEntry( s->vStamp, Level, (int) s->nStamp );
+            Vec_IntWriteEntry( s->vStamp, Level, ( int ) s->nStamp );
             nLBD++;
         }
     }
@@ -330,13 +330,13 @@ unsigned xSAT_SolverClaNew( xSAT_Solver_t * s, Vec_Int_t * vLits , int fLearnt )
   SeeAlso     []
 
 ***********************************************************************/
-int xSAT_SolverEnqueue( xSAT_Solver_t* s, int Lit, unsigned Reason )
+int xSAT_SolverEnqueue( xSAT_Solver_t * s, int Lit, unsigned Reason )
 {
     int Var = xSAT_Lit2Var( Lit );
 
-    Vec_StrWriteEntry( s->vAssigns, Var, (char)xSAT_LitSign( Lit ) );
+    Vec_StrWriteEntry( s->vAssigns, Var, xSAT_LitSign( Lit ) );
     Vec_IntWriteEntry( s->vLevels, Var, xSAT_SolverDecisionLevel( s ) );
-    Vec_IntWriteEntry( s->vReasons, Var, (int) Reason );
+    Vec_IntWriteEntry( s->vReasons, Var, ( int ) Reason );
     Vec_IntPush( s->vTrail, Lit );
 
     return true;
@@ -353,7 +353,7 @@ int xSAT_SolverEnqueue( xSAT_Solver_t* s, int Lit, unsigned Reason )
   SeeAlso     []
 
 ***********************************************************************/
-static inline void xSAT_SolverNewDecision( xSAT_Solver_t* s, int Lit )
+static inline void xSAT_SolverNewDecision( xSAT_Solver_t * s, int Lit )
 {
     assert( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lit ) ) == VarX );
     s->Stats.nDecisions++;
@@ -375,6 +375,7 @@ static inline void xSAT_SolverNewDecision( xSAT_Solver_t* s, int Lit )
 void xSAT_SolverCancelUntil( xSAT_Solver_t * s, int Level )
 {
     int c;
+
     if ( xSAT_SolverDecisionLevel( s ) <= Level )
         return;
 
@@ -410,30 +411,30 @@ static int xSAT_SolverIsLitRemovable( xSAT_Solver_t* s, int Lit, int MinLevel )
 {
     int top = Vec_IntSize( s->vTagged );
 
-    assert( (unsigned) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( Lit ) ) != CRefUndef );
+    assert( ( unsigned ) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( Lit ) ) != CRefUndef );
     Vec_IntClear( s->vStack );
     Vec_IntPush( s->vStack, xSAT_Lit2Var( Lit ) );
 
     while ( Vec_IntSize( s->vStack ) )
     {
+        int i;
         int v = Vec_IntPop(  s->vStack );
         xSAT_Clause_t* c = xSAT_SolverReadClause(s, ( unsigned ) Vec_IntEntry( s->vReasons, v ) );
-        int* Lits = &( c->pData[0].Lit );
-        int  i;
-        assert( (unsigned) Vec_IntEntry( s->vReasons, v ) != CRefUndef);
+        int * Lits = &( c->pData[0].Lit );
 
+        assert( (unsigned) Vec_IntEntry( s->vReasons, v ) != CRefUndef);
         if( c->nSize == 2 && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[0] ) ) == xSAT_LitSign( xSAT_NegLit( Lits[0] ) ) )
         {
             assert( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[1] ) ) == xSAT_LitSign( ( Lits[1] ) ) );
             ABC_SWAP( int, Lits[0], Lits[1] );
         }
 
-        for (i = 1; i < (int)c->nSize; i++)
+        for ( i = 1; i < c->nSize; i++ )
         {
             int v = xSAT_Lit2Var( Lits[i] );
             if ( !Vec_StrEntry( s->vSeen, v ) && Vec_IntEntry( s->vLevels, v ) )
             {
-                if ( (unsigned) Vec_IntEntry( s->vReasons, v ) != CRefUndef && ((1 << (Vec_IntEntry( s->vLevels, v ) & 31)) & MinLevel))
+                if ( ( unsigned ) Vec_IntEntry( s->vReasons, v ) != CRefUndef && ( ( 1 << (Vec_IntEntry( s->vLevels, v ) & 31 ) ) & MinLevel ) )
                 {
                     Vec_IntPush( s->vStack, v );
                     Vec_IntPush( s->vTagged, Lits[i] );
@@ -443,7 +444,7 @@ static int xSAT_SolverIsLitRemovable( xSAT_Solver_t* s, int Lit, int MinLevel )
                 {
                     int Lit;
                     Vec_IntForEachEntryStart( s->vTagged, Lit, i, top )
-                        Vec_StrWriteEntry( s->vSeen, xSAT_Lit2Var(Lit), 0 );
+                        Vec_StrWriteEntry( s->vSeen, xSAT_Lit2Var( Lit ), 0 );
                     Vec_IntShrink( s->vTagged, top );
                     return 0;
                 }
@@ -479,40 +480,34 @@ static void xSAT_SolverClaMinimisation( xSAT_Solver_t * s, Vec_Int_t * vLits )
     /* Remove reduntant literals */
     Vec_IntAppend( s->vTagged, vLits );
     for ( i = j = 1; i < Vec_IntSize( vLits ); i++ )
-        if ( (unsigned) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( pLits[i] ) ) == CRefUndef || !xSAT_SolverIsLitRemovable( s, pLits[i], MinLevel ) )
+        if ( ( unsigned ) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( pLits[i] ) ) == CRefUndef || !xSAT_SolverIsLitRemovable( s, pLits[i], MinLevel ) )
             pLits[j++] = pLits[i];
     Vec_IntShrink( vLits, j );
 
     /* Binary Resolution */
     if( Vec_IntSize( vLits ) <= 30 && xSAT_SolverClaCalcLBD2( s, vLits ) <= 6 )
     {
+        int nb, l;
         int Lit;
         int FlaseLit = xSAT_NegLit( pLits[0] );
-        int nb;
-        int l;
-
-        xSAT_WatchList_t * ws;
-        xSAT_Watcher_t * begin;
-        xSAT_Watcher_t * end;
+        xSAT_WatchList_t * ws = xSAT_VecWatchListEntry( s->vBinWatches, FlaseLit );
+        xSAT_Watcher_t * begin = xSAT_WatchListArray( ws );
+        xSAT_Watcher_t * end   = begin + xSAT_WatchListSize( ws );
         xSAT_Watcher_t * pWatcher;
 
         s->nStamp++;
         Vec_IntForEachEntry( vLits, Lit, i )
-            Vec_IntWriteEntry( s->vStamp, xSAT_Lit2Var( Lit ), s->nStamp );
-
-        ws = xSAT_VecWatchListEntry( s->vBinWatches, FlaseLit );
-        begin = xSAT_WatchListArray( ws );
-        end   = begin + xSAT_WatchListSize( ws );
+            Vec_IntWriteEntry( s->vStamp, xSAT_Lit2Var( Lit ), ( int ) s->nStamp );
 
         nb = 0;
         for ( pWatcher = begin; pWatcher < end; pWatcher++ )
         {
             int ImpLit = pWatcher->Blocker;
 
-            if ( Vec_IntEntry( s->vStamp, xSAT_Lit2Var( ImpLit ) ) == (int)s->nStamp && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( ImpLit ) ) == xSAT_LitSign( ImpLit ) )
+            if ( ( unsigned ) Vec_IntEntry( s->vStamp, xSAT_Lit2Var( ImpLit ) ) == s->nStamp && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( ImpLit ) ) == xSAT_LitSign( ImpLit ) )
             {
                 nb++;
-                Vec_IntWriteEntry( s->vStamp, xSAT_Lit2Var( ImpLit ), s->nStamp - 1 );
+                Vec_IntWriteEntry( s->vStamp, xSAT_Lit2Var( ImpLit ), ( int )( s->nStamp - 1 ) );
             }
         }
 
@@ -520,7 +515,7 @@ static void xSAT_SolverClaMinimisation( xSAT_Solver_t * s, Vec_Int_t * vLits )
         if ( nb > 0 )
         {
             for ( i = 1; i < Vec_IntSize( vLits ) - nb; i++ )
-                if ( Vec_IntEntry( s->vStamp, xSAT_Lit2Var( pLits[i] ) ) != (int)s->nStamp )
+                if ( ( unsigned ) Vec_IntEntry( s->vStamp, xSAT_Lit2Var( pLits[i] ) ) != s->nStamp )
                 {
                     int TempLit = pLits[l];
                     pLits[l] = pLits[i];
@@ -546,43 +541,44 @@ static void xSAT_SolverClaMinimisation( xSAT_Solver_t * s, Vec_Int_t * vLits )
 ***********************************************************************/
 static void xSAT_SolverAnalyze( xSAT_Solver_t* s, unsigned ConfCRef, Vec_Int_t * vLearnt, int * OutBtLevel, unsigned * nLBD )
 {
-    int* trail   = Vec_IntArray( s->vTrail );
-    int Count     = 0;
+    int * trail = Vec_IntArray( s->vTrail );
+    int Count   = 0;
     int p       = LitUndef;
     int Idx     = Vec_IntSize( s->vTrail ) - 1;
-    int* Lits;
+    int * Lits;
     int Lit;
     int i, j;
 
     Vec_IntPush( vLearnt, LitUndef );
     do
     {
-        xSAT_Clause_t * c;
+        xSAT_Clause_t * pCla;
+
         assert( ConfCRef != CRefUndef );
-        c = xSAT_SolverReadClause(s, ConfCRef);
-        Lits = &( c->pData[0].Lit );
+        pCla = xSAT_SolverReadClause(s, ConfCRef);
+        Lits = &( pCla->pData[0].Lit );
 
-        if( p != LitUndef && c->nSize == 2 && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var(Lits[0])) == xSAT_LitSign( xSAT_NegLit( Lits[0] ) ) )
+        if( p != LitUndef && pCla->nSize == 2 && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[0] ) ) == xSAT_LitSign( xSAT_NegLit( Lits[0] ) ) )
         {
             assert( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[1] ) ) == xSAT_LitSign( ( Lits[1] ) ) );
             ABC_SWAP( int, Lits[0], Lits[1] );
         }
 
-        if ( c->fLearnt )
-            xSAT_SolverClaActBump( s, c );
+        if ( pCla->fLearnt )
+            xSAT_SolverClaActBump( s, pCla );
 
-        if ( c->fLearnt && c->nLBD > 2 )
+        if ( pCla->fLearnt && pCla->nLBD > 2 )
         {
-            unsigned int nblevels = xSAT_SolverClaCalcLBD(s, c);
-            if ( nblevels + 1 < c->nLBD )
+            unsigned int nLevels = xSAT_SolverClaCalcLBD( s, pCla );
+            if ( nLevels + 1 < pCla->nLBD )
             {
-                if (c->nLBD <= s->Config.nLBDFrozenClause)
-                    c->fCanBeDel = 0;
-                c->nLBD = nblevels;
+                if ( pCla->nLBD <= s->Config.nLBDFrozenClause )
+                    pCla->fCanBeDel = 0;
+                pCla->nLBD = nLevels;
             }
         }
 
-        for ( j = ( p == LitUndef ? 0 : 1 ); j < (int)c->nSize; j++ )
+        for ( j = ( p == LitUndef ? 0 : 1 ); j < pCla->nSize; j++ )
         {
             int Var = xSAT_Lit2Var( Lits[j] );
 
@@ -605,14 +601,13 @@ static void xSAT_SolverAnalyze( xSAT_Solver_t* s, unsigned ConfCRef, Vec_Int_t *
 
         // Next clause to look at
         p = trail[Idx+1];
-        ConfCRef = (unsigned) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( p ) );
+        ConfCRef = ( unsigned ) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( p ) );
         Vec_StrWriteEntry( s->vSeen, xSAT_Lit2Var( p ), 0 );
         Count--;
 
     } while ( Count > 0 );
 
     Vec_IntArray( vLearnt )[0] = xSAT_NegLit( p );
-
     xSAT_SolverClaMinimisation( s, vLearnt );
 
     // Find the backtrack level
@@ -677,41 +672,38 @@ unsigned xSAT_SolverPropagate( xSAT_Solver_t* s )
     while ( s->iQhead < Vec_IntSize( s->vTrail ) )
     {
         int p = Vec_IntEntry( s->vTrail, s->iQhead++ );
-
         xSAT_WatchList_t* ws = xSAT_VecWatchListEntry( s->vBinWatches, p );
         xSAT_Watcher_t* begin = xSAT_WatchListArray( ws );
         xSAT_Watcher_t* end   = begin + xSAT_WatchListSize( ws );
         xSAT_Watcher_t *i, *j;
 
         nProp++;
-        for (i = begin; i < end; i++)
+        for ( i = begin; i < end; i++ )
         {
-            if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var(i->Blocker)) == xSAT_LitSign(xSAT_NegLit(i->Blocker)))
+            if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( i->Blocker ) ) == xSAT_LitSign( xSAT_NegLit( i->Blocker ) ) )
             {
                 return i->CRef;
             }
-            else if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var(i->Blocker)) == VarX)
-                xSAT_SolverEnqueue(s, i->Blocker, i->CRef);
+            else if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( i->Blocker ) ) == VarX )
+                xSAT_SolverEnqueue( s, i->Blocker, i->CRef );
         }
 
-
-        ws    = xSAT_VecWatchListEntry( s->vWatches, p);
+        ws    = xSAT_VecWatchListEntry( s->vWatches, p );
         begin = xSAT_WatchListArray( ws );
         end   = begin + xSAT_WatchListSize( ws );
 
         for ( i = j = begin; i < end; )
         {
-            xSAT_Clause_t* c;
+            xSAT_Clause_t * pCla;
             xSAT_Watcher_t w;
-
             if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( i->Blocker ) ) == xSAT_LitSign( i->Blocker ) )
             {
                 *j++ = *i++;
                 continue;
             }
 
-            c = xSAT_SolverReadClause( s, i->CRef );
-            Lits = &( c->pData[0].Lit );
+            pCla = xSAT_SolverReadClause( s, i->CRef );
+            Lits = &( pCla->pData[0].Lit );
 
             // Make sure the false literal is data[1]:
             NegLit = xSAT_NegLit( p );
@@ -731,8 +723,8 @@ unsigned xSAT_SolverPropagate( xSAT_Solver_t* s )
             else
             {
                 // Look for new watch:
-                int* stop = Lits + c->nSize;
-                int* k;
+                int * stop = Lits + pCla->nSize;
+                int * k;
                 for ( k = Lits + 2; k < stop; k++ )
                 {
                     if (Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( *k ) ) != !xSAT_LitSign( *k ) )
@@ -791,7 +783,7 @@ void xSAT_SolverReduceDB( xSAT_Solver_t * s )
     int nLearnedOld = Vec_IntSize( s->vLearnts );
     int i, limit;
     unsigned CRef;
-    xSAT_Clause_t * c;
+    xSAT_Clause_t * pCla;
     xSAT_Clause_t ** learnts_cls;
 
     learnts_cls = ABC_ALLOC( xSAT_Clause_t *, nLearnedOld );
@@ -812,21 +804,22 @@ void xSAT_SolverReduceDB( xSAT_Solver_t * s )
     for ( i = 0; i < nLearnedOld; i++ )
     {
         unsigned CRef;
-        c = learnts_cls[i];
-        CRef = xSAT_MemCRef( s->pMemory, (unsigned * ) c );
-        assert(c->fMark == 0);
-        if ( c->fCanBeDel && c->nLBD > 2 && c->nSize > 2 && (unsigned) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( c->pData[0].Lit ) ) != CRef && ( i < limit ) )
+
+        pCla = learnts_cls[i];
+        CRef = xSAT_MemCRef( s->pMemory, ( unsigned * ) pCla );
+        assert( pCla->fMark == 0 );
+        if ( pCla->fCanBeDel && pCla->nLBD > 2 && pCla->nSize > 2 && (unsigned) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( pCla->pData[0].Lit ) ) != CRef && ( i < limit ) )
         {
-            c->fMark = 1;
-            s->Stats.nLearntLits -= c->nSize;
-            xSAT_WatchListRemove( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit( c->pData[0].Lit ) ), CRef );
-            xSAT_WatchListRemove( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit( c->pData[1].Lit ) ), CRef );
+            pCla->fMark = 1;
+            s->Stats.nLearntLits -= pCla->nSize;
+            xSAT_WatchListRemove( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit( pCla->pData[0].Lit ) ), CRef );
+            xSAT_WatchListRemove( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit( pCla->pData[1].Lit ) ), CRef );
         }
         else
         {
-            if (!c->fCanBeDel)
+            if ( !pCla->fCanBeDel )
                 limit++;
-            c->fCanBeDel = 1;
+            pCla->fCanBeDel = 1;
             Vec_IntPush( s->vLearnts, CRef );
         }
     }
@@ -876,7 +869,7 @@ char xSAT_SolverSearch( xSAT_Solver_t * s )
                 return LBoolFalse;
 
             xSAT_BQueuePush( s->bqTrail, Vec_IntSize( s->vTrail ) );
-            if ( s->Stats.nConflicts > s->Config.nFirstBlockRestart && xSAT_BQueueIsValid( s->bqLBD ) && ( Vec_IntSize( s->vTrail ) > ( s->Config.R * (iword)xSAT_BQueueAvg( s->bqTrail ) ) ) )
+            if ( s->Stats.nConflicts > s->Config.nFirstBlockRestart && xSAT_BQueueIsValid( s->bqLBD ) && ( Vec_IntSize( s->vTrail ) > ( s->Config.R * ( iword ) xSAT_BQueueAvg( s->bqTrail ) ) ) )
                 xSAT_BQueueClean(s->bqLBD);
 
             Vec_IntClear( s->vLearntClause );
@@ -896,7 +889,7 @@ char xSAT_SolverSearch( xSAT_Solver_t * s )
         {
             /* No conflict */
             int NextVar;
-            if ( xSAT_BQueueIsValid( s->bqLBD ) && ( ( (iword)xSAT_BQueueAvg( s->bqLBD ) * s->Config.K ) > ( s->nSumLBD / (iword)s->Stats.nConflicts ) ) )
+            if ( xSAT_BQueueIsValid( s->bqLBD ) && ( ( ( iword )xSAT_BQueueAvg( s->bqLBD ) * s->Config.K ) > ( s->nSumLBD / s->Stats.nConflicts ) ) )
             {
                 xSAT_BQueueClean( s->bqLBD );
                 xSAT_SolverCancelUntil( s, 0 );
@@ -942,23 +935,20 @@ char xSAT_SolverSearch( xSAT_Solver_t * s )
 ***********************************************************************/
 void xSAT_SolverClaRealloc( xSAT_Mem_t * pDest, xSAT_Mem_t * pSrc, unsigned * pCRef )
 {
-    xSAT_Clause_t * pOldCla = xSAT_MemClauseHand( pSrc, *pCRef );
     unsigned nNewCRef;
     xSAT_Clause_t * pNewCla;
+    xSAT_Clause_t * pOldCla = xSAT_MemClauseHand( pSrc, *pCRef );
 
     if ( pOldCla->fReallocd )
     {
-        *pCRef = (unsigned) pOldCla->nSize;
+        *pCRef = ( unsigned ) pOldCla->nSize;
         return;
     }
-
     nNewCRef = xSAT_MemAppend( pDest, 3 + pOldCla->fLearnt + pOldCla->nSize );
     pNewCla = xSAT_MemClauseHand( pDest, nNewCRef );
-
     memcpy( pNewCla, pOldCla, ( 3 + pOldCla->fLearnt + pOldCla->nSize ) * 4 );
-
     pOldCla->fReallocd = 1;
-    pOldCla->nSize = (unsigned) nNewCRef;
+    pOldCla->nSize = ( unsigned ) nNewCRef;
     *pCRef = nNewCRef;
 }
 
@@ -997,14 +987,14 @@ void xSAT_SolverGarbageCollect( xSAT_Solver_t * s )
     }
 
     for ( i = 0; i < Vec_IntSize( s->vTrail ); i++ )
-        if ( (unsigned) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( Vec_IntEntry( s->vTrail, i ) ) ) != CRefUndef )
-            xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, (unsigned *)&( Vec_IntArray( s->vReasons )[xSAT_Lit2Var( Vec_IntEntry( s->vTrail, i ) )] ) );
+        if ( ( unsigned ) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( Vec_IntEntry( s->vTrail, i ) ) ) != CRefUndef )
+            xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, ( unsigned * ) &( Vec_IntArray( s->vReasons )[xSAT_Lit2Var( Vec_IntEntry( s->vTrail, i ) )] ) );
 
     pArray = ( unsigned * ) Vec_IntArray( s->vLearnts );
     for ( i = 0; i < Vec_IntSize( s->vLearnts ); i++ )
         xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, &(pArray[i]) );
 
-    pArray = (unsigned *) Vec_IntArray( s->vClauses );
+    pArray = ( unsigned * ) Vec_IntArray( s->vClauses );
     for ( i = 0; i < Vec_IntSize( s->vClauses ); i++ )
         xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, &(pArray[i]) );
 
diff --git a/src/sat/xsat/xsatSolver.h b/src/sat/xsat/xsatSolver.h
index 2bcd93b7..bf8bf419 100644
--- a/src/sat/xsat/xsatSolver.h
+++ b/src/sat/xsat/xsatSolver.h
@@ -81,9 +81,9 @@ struct xSAT_SolverOptions_t_
     char fVerbose;
 
     // Limits
-    word nConfLimit;    // external limit on the number of conflicts
-    word nInsLimit;     // external limit on the number of implications
-    abctime     nRuntimeLimit; // external limit on runtime
+    iword   nConfLimit;    // external limit on the number of conflicts
+    iword   nInsLimit;     // external limit on the number of implications
+    abctime nRuntimeLimit; // external limit on runtime
 
     // Constants used for restart heuristic
     double K; // Forces a restart
@@ -105,13 +105,13 @@ struct xSAT_Stats_t_
     unsigned nStarts;
     unsigned nReduceDB;
 
-    word nDecisions;
-    word nPropagations;
-    word nInspects;
-    word nConflicts;
+    iword nDecisions;
+    iword nPropagations;
+    iword nInspects;
+    iword nConflicts;
 
-    word nClauseLits;
-    word nLearntLits;
+    iword nClauseLits;
+    iword nLearntLits;
 };
 
 struct xSAT_Solver_t_
@@ -143,7 +143,7 @@ struct xSAT_Solver_t_
 
     int     nAssignSimplify; /* Number of top-level assignments since last
                               * execution of 'simplify()'. */
-    word nPropSimplify;   /* Remaining number of propagations that must be
+    int64_t nPropSimplify;   /* Remaining number of propagations that must be
                               * made before next execution of 'simplify()'. */
 
     /* Temporary data used by Search method */
@@ -203,10 +203,10 @@ static inline xSAT_Clause_t * xSAT_SolverReadClause( xSAT_Solver_t * s, unsigned
 static inline int xSAT_SolverIsClauseSatisfied( xSAT_Solver_t * s, xSAT_Clause_t * pCla )
 {
     int i;
-    int * lits = &( pCla->pData[0].Lit );
+    int * Lits = &( pCla->pData[0].Lit );
 
-    for ( i = 0; i < (int)pCla->nSize; i++ )
-        if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( lits[i] ) ) == xSAT_LitSign( ( lits[i] ) ) )
+    for ( i = 0; i < pCla->nSize; i++ )
+        if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[i] ) ) == xSAT_LitSign( ( Lits[i] ) ) )
             return true;
 
     return false;
diff --git a/src/sat/xsat/xsatSolverAPI.c b/src/sat/xsat/xsatSolverAPI.c
index 43c2d06e..7746dc0b 100644
--- a/src/sat/xsat/xsatSolverAPI.c
+++ b/src/sat/xsat/xsatSolverAPI.c
@@ -51,6 +51,7 @@ xSAT_SolverOptions_t DefaultConfig =
     30     //.nLBDFrozenClause = 30
 };
 
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -125,7 +126,6 @@ void xSAT_SolverDestroy( xSAT_Solver_t * s )
     xSAT_VecWatchListFree( s->vWatches );
     xSAT_VecWatchListFree( s->vBinWatches );
 
-    // delete vectors
     xSAT_HeapFree(s->hOrder);
     Vec_IntFree( s->vTrailLim );
     Vec_IntFree( s->vTrail );
diff --git a/src/sat/xsat/xsatWatchList.h b/src/sat/xsat/xsatWatchList.h
index 2ba13c24..284be100 100644
--- a/src/sat/xsat/xsatWatchList.h
+++ b/src/sat/xsat/xsatWatchList.h
@@ -118,9 +118,9 @@ static inline void xSAT_WatchListShrink( xSAT_WatchList_t * v, int k )
 static inline void xSAT_WatchListPush( xSAT_WatchList_t * v, xSAT_Watcher_t e )
 {
     assert( v );
-    if (v->nSize == v->nCap)
+    if ( v->nSize == v->nCap )
     {
-        int newsize = (v->nCap < 4) ? 4 : (v->nCap / 2) * 3;
+        int newsize = ( v->nCap < 4 ) ? 4 : ( v->nCap / 2 ) * 3;
 
         v->pArray = ABC_REALLOC( xSAT_Watcher_t, v->pArray, newsize );
         if ( v->pArray == NULL )
@@ -167,9 +167,9 @@ static inline void xSAT_WatchListRemove( xSAT_WatchList_t * v, unsigned CRef )
     xSAT_Watcher_t* ws = xSAT_WatchListArray(v);
     int j = 0;
 
-    for (; ws[j].CRef != CRef; j++);
-    assert(j < xSAT_WatchListSize(v));
-    memmove(v->pArray + j, v->pArray + j + 1, (v->nSize - j - 1) * sizeof(xSAT_Watcher_t));
+    for ( ; ws[j].CRef != CRef; j++ );
+    assert( j < xSAT_WatchListSize( v ) );
+    memmove( v->pArray + j, v->pArray + j + 1, ( v->nSize - j - 1 ) * sizeof( xSAT_Watcher_t ) );
     v->nSize -= 1;
 }
 
@@ -190,7 +190,7 @@ static inline xSAT_VecWatchList_t * xSAT_VecWatchListAlloc( int nCap )
 
     v->nCap   = 4;
     v->nSize  = 0;
-    v->pArray = (xSAT_WatchList_t *) ABC_CALLOC(xSAT_WatchList_t, sizeof( xSAT_WatchList_t ) * v->nCap);
+    v->pArray = ( xSAT_WatchList_t * ) ABC_CALLOC(xSAT_WatchList_t, sizeof( xSAT_WatchList_t ) * v->nCap);
     return v;
 }
 
@@ -233,7 +233,7 @@ static inline void xSAT_VecWatchListPush( xSAT_VecWatchList_t* v )
         int newsize = (v->nCap < 4) ? v->nCap * 2 : (v->nCap / 2) * 3;
 
         v->pArray = ABC_REALLOC( xSAT_WatchList_t, v->pArray, newsize );
-        memset( v->pArray + v->nCap, 0, sizeof(xSAT_WatchList_t) * (newsize - v->nCap) );
+        memset( v->pArray + v->nCap, 0, sizeof( xSAT_WatchList_t ) * ( newsize - v->nCap ) );
         if ( v->pArray == NULL )
         {
             printf( "Failed to realloc memory from %.1f MB to %.1f MB.\n",