Bug fix in 'dsat <file.cnf>' when the number of classes in listed incorrectly.

7 files changed, 137 insertions, 109 deletions

diff --git a/src/sat/xsat/xsatBQueue.h b/src/sat/xsat/xsatBQueue.h
index 37951684..6c170c93 100644
--- a/src/sat/xsat/xsatBQueue.h
+++ b/src/sat/xsat/xsatBQueue.h
@@ -24,6 +24,7 @@
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
+
 #include "misc/util/abc_global.h"
 
 ABC_NAMESPACE_HEADER_START
@@ -31,6 +32,7 @@ ABC_NAMESPACE_HEADER_START
 ////////////////////////////////////////////////////////////////////////
 ///                    STRUCTURE DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
+
 typedef struct xSAT_BQueue_t_ xSAT_BQueue_t;
 struct xSAT_BQueue_t_
 {
@@ -38,13 +40,14 @@ struct xSAT_BQueue_t_
     int nCap;
     int iFirst;
     int iEmpty;
-    uint64_t nSum;
-    uint32_t * pData;
+    word nSum;
+    word * pData;
 };
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DECLARATIONS                        ///
 ////////////////////////////////////////////////////////////////////////
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -60,7 +63,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( uint32_t, nCap );
+    p->pData = ABC_CALLOC( word, nCap );
     return p;
 }
 
@@ -92,7 +95,7 @@ static inline void xSAT_BQueueFree( xSAT_BQueue_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-static inline void xSAT_BQueuePush( xSAT_BQueue_t * p, uint32_t Value )
+static inline void xSAT_BQueuePush( xSAT_BQueue_t * p, word Value )
 {
     if ( p->nSize == p->nCap )
     {
@@ -125,8 +128,8 @@ static inline void xSAT_BQueuePush( xSAT_BQueue_t * p, uint32_t Value )
 ***********************************************************************/
 static inline int xSAT_BQueuePop( xSAT_BQueue_t * p )
 {
-    assert( p->nSize >= 1 );
     int RetValue = p->pData[p->iFirst];
+    assert( p->nSize >= 1 );
     p->nSum -= RetValue;
     p->iFirst = ( p->iFirst + 1 ) % p->nCap;
     p->nSize--;
@@ -144,9 +147,9 @@ static inline int xSAT_BQueuePop( xSAT_BQueue_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-static inline uint32_t xSAT_BQueueAvg( xSAT_BQueue_t * p )
+static inline word xSAT_BQueueAvg( xSAT_BQueue_t * p )
 {
-    return ( uint32_t )( p->nSum / ( ( uint64_t ) p->nSize ) );
+    return ( word )( p->nSum / ( ( word ) p->nSize ) );
 }
 
 /**Function*************************************************************
diff --git a/src/sat/xsat/xsatClause.h b/src/sat/xsat/xsatClause.h
index 39f0a0c8..d05eb6de 100644
--- a/src/sat/xsat/xsatClause.h
+++ b/src/sat/xsat/xsatClause.h
@@ -96,7 +96,7 @@ static void xSAT_ClausePrint( xSAT_Clause_t * pCla )
     int i;
 
     printf("{ ");
-    for ( i = 0; i < pCla->nSize; i++ )
+    for ( i = 0; i < (int)pCla->nSize; i++ )
         printf("%d ", pCla->pData[i].Lit );
     printf("}\n");
 }
diff --git a/src/sat/xsat/xsatMemory.h b/src/sat/xsat/xsatMemory.h
index 3a961b97..3324a563 100644
--- a/src/sat/xsat/xsatMemory.h
+++ b/src/sat/xsat/xsatMemory.h
@@ -36,10 +36,10 @@ ABC_NAMESPACE_HEADER_START
 typedef struct xSAT_Mem_t_ xSAT_Mem_t;
 struct xSAT_Mem_t_
 {
-    uint32_t   nSize;
-    uint32_t   nCap;
-    uint32_t   nWasted;
-    uint32_t * pData;
+    unsigned   nSize;
+    unsigned   nCap;
+    unsigned   nWasted;
+    unsigned * pData;
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -58,7 +58,7 @@ struct xSAT_Mem_t_
 ***********************************************************************/
 static inline xSAT_Clause_t *  xSAT_MemClauseHand( xSAT_Mem_t * p, int h )
 {
-    return h != UINT32_MAX ? ( xSAT_Clause_t * )( p->pData + h ) : NULL;
+    return h != 0xFFFFFFFF ? ( xSAT_Clause_t * )( p->pData + h ) : NULL;
 }
 
 /**Function*************************************************************
@@ -72,21 +72,21 @@ static inline xSAT_Clause_t *  xSAT_MemClauseHand( xSAT_Mem_t * p, int h )
   SeeAlso     []
 
 ***********************************************************************/
-static inline void xSAT_MemGrow( xSAT_Mem_t * p, uint32_t nCap )
+static inline void xSAT_MemGrow( xSAT_Mem_t * p, unsigned nCap )
 {
+    unsigned nPrevCap = p->nCap;
     if ( p->nCap >= nCap )
         return;
 
-    uint32_t nPrevCap = p->nCap;
     while (p->nCap < nCap)
     {
-        uint32_t 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(uint32_t, p->pData, p->nCap);
+    p->pData = ABC_REALLOC(unsigned, p->pData, p->nCap);
 }
 
 /**Function*************************************************************
@@ -156,12 +156,13 @@ static inline void xSAT_MemFree( xSAT_Mem_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-static inline uint32_t xSAT_MemAppend( xSAT_Mem_t * p, int nSize )
+static inline unsigned xSAT_MemAppend( xSAT_Mem_t * p, int nSize )
 {
+    unsigned nPrevSize;
     assert(nSize > 0);
     xSAT_MemGrow(p, p->nSize + nSize);
 
-    uint32_t nPrevSize = p->nSize;
+    nPrevSize = p->nSize;
     p->nSize += nSize;
     assert(p->nSize > nPrevSize);
 
@@ -179,9 +180,9 @@ static inline uint32_t xSAT_MemAppend( xSAT_Mem_t * p, int nSize )
   SeeAlso     []
 
 ***********************************************************************/
-static inline uint32_t xSAT_MemCRef( xSAT_Mem_t * p, uint32_t * pC )
+static inline unsigned xSAT_MemCRef( xSAT_Mem_t * p, unsigned * pC )
 {
-    return ( uint32_t )( pC - &(p->pData[0]) );
+    return ( unsigned )( pC - &(p->pData[0]) );
 }
 
 /**Function*************************************************************
@@ -195,7 +196,7 @@ static inline uint32_t xSAT_MemCRef( xSAT_Mem_t * p, uint32_t * pC )
   SeeAlso     []
 
 ***********************************************************************/
-static inline uint32_t xSAT_MemCap( xSAT_Mem_t * p )
+static inline unsigned xSAT_MemCap( xSAT_Mem_t * p )
 {
     return p->nCap;
 }
@@ -211,7 +212,7 @@ static inline uint32_t xSAT_MemCap( xSAT_Mem_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-static inline uint32_t xSAT_MemWastedCap( xSAT_Mem_t * p )
+static inline unsigned xSAT_MemWastedCap( xSAT_Mem_t * p )
 {
     return p->nWasted;
 }
diff --git a/src/sat/xsat/xsatSolver.c b/src/sat/xsat/xsatSolver.c
index d6968a2d..91b0c595 100644
--- a/src/sat/xsat/xsatSolver.c
+++ b/src/sat/xsat/xsatSolver.c
@@ -101,8 +101,9 @@ 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;
 
-    for ( int i = 0; i < Vec_IntSize( s->vActivity ); i++ )
+    for ( i = 0; i < Vec_IntSize( s->vActivity ); i++ )
         pActivity[i] >>= 19;
 
     s->nVarActInc >>= 19;
@@ -166,7 +167,7 @@ static inline void xSAT_SolverClaActRescale( xSAT_Solver_t * s )
 
     Vec_IntForEachEntry( s->vLearnts, CRef, i )
     {
-        pC = xSAT_SolverReadClause( s, (uint32_t) CRef );
+        pC = xSAT_SolverReadClause( s, (unsigned) CRef );
         pC->pData[pC->nSize].Act >>= 14;
     }
     s->nClaActInc >>= 14;
@@ -221,9 +222,10 @@ 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;
 
     s->nStamp++;
-    for ( int i = 0; i < pCla->nSize; i++ )
+    for ( i = 0; i < (int)pCla->nSize; i++ )
     {
         int Level = Vec_IntEntry( s->vLevels, xSAT_Lit2Var( pCla->pData[i].Lit ) );
         if ( (unsigned) Vec_IntEntry( s->vStamp, Level ) != s->nStamp )
@@ -238,9 +240,10 @@ 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;
 
     s->nStamp++;
-    for ( int i = 0; i < Vec_IntSize( vLits ); i++ )
+    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 )
@@ -263,17 +266,18 @@ static inline int xSAT_SolverClaCalcLBD2( xSAT_Solver_t * s, Vec_Int_t * vLits )
   SeeAlso     []
 
 ***********************************************************************/
-uint32_t xSAT_SolverClaNew( xSAT_Solver_t * s, Vec_Int_t * vLits , int fLearnt )
+unsigned xSAT_SolverClaNew( xSAT_Solver_t * s, Vec_Int_t * vLits , int fLearnt )
 {
-    assert( Vec_IntSize( vLits ) > 1);
-    assert( fLearnt == 0 || fLearnt == 1 );
-
-    uint32_t CRef;
+    unsigned CRef;
     xSAT_Clause_t * pCla;
     xSAT_Watcher_t w1;
     xSAT_Watcher_t w2;
+    unsigned nWords;
 
-    uint32_t nWords = 3 + fLearnt + Vec_IntSize( vLits );
+    assert( Vec_IntSize( vLits ) > 1);
+    assert( fLearnt == 0 || fLearnt == 1 );
+
+    nWords = 3 + fLearnt + Vec_IntSize( vLits );
     CRef = xSAT_MemAppend( s->pMemory, nWords );
     pCla = xSAT_SolverReadClause( s, CRef );
     pCla->fLearnt = fLearnt;
@@ -326,11 +330,11 @@ uint32_t xSAT_SolverClaNew( xSAT_Solver_t * s, Vec_Int_t * vLits , int fLearnt )
   SeeAlso     []
 
 ***********************************************************************/
-int xSAT_SolverEnqueue( xSAT_Solver_t* s, int Lit, uint32_t Reason )
+int xSAT_SolverEnqueue( xSAT_Solver_t* s, int Lit, unsigned Reason )
 {
     int Var = xSAT_Lit2Var( Lit );
 
-    Vec_StrWriteEntry( s->vAssigns, Var, xSAT_LitSign( Lit ) );
+    Vec_StrWriteEntry( s->vAssigns, Var, (char)xSAT_LitSign( Lit ) );
     Vec_IntWriteEntry( s->vLevels, Var, xSAT_SolverDecisionLevel( s ) );
     Vec_IntWriteEntry( s->vReasons, Var, (int) Reason );
     Vec_IntPush( s->vTrail, Lit );
@@ -370,16 +374,17 @@ 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;
 
-    for ( int c = Vec_IntSize( s->vTrail ) - 1; c >= Vec_IntEntry( s->vTrailLim, Level ); c-- )
+    for ( c = Vec_IntSize( s->vTrail ) - 1; c >= Vec_IntEntry( s->vTrailLim, Level ); c-- )
     {
         int Var = xSAT_Lit2Var( Vec_IntEntry( s->vTrail, c ) );
 
         Vec_StrWriteEntry( s->vAssigns, Var, VarX );
         Vec_IntWriteEntry( s->vReasons, Var, ( int ) CRefUndef );
-        Vec_StrWriteEntry( s->vPolarity, Var, xSAT_LitSign( Vec_IntEntry( s->vTrail, c ) ) );
+        Vec_StrWriteEntry( s->vPolarity, Var, ( char )xSAT_LitSign( Vec_IntEntry( s->vTrail, c ) ) );
 
         if ( !xSAT_HeapInHeap( s->hOrder, Var ) )
             xSAT_HeapInsert( s->hOrder, Var );
@@ -405,17 +410,17 @@ static int xSAT_SolverIsLitRemovable( xSAT_Solver_t* s, int Lit, int MinLevel )
 {
     int top = Vec_IntSize( s->vTagged );
 
-    assert( (uint32_t) 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 v = Vec_IntPop(  s->vStack );
-        assert( (uint32_t) Vec_IntEntry( s->vReasons, v ) != CRefUndef);
-        xSAT_Clause_t* c = xSAT_SolverReadClause(s, ( uint32_t ) Vec_IntEntry( s->vReasons, v ) );
+        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);
 
         if( c->nSize == 2 && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[0] ) ) == xSAT_LitSign( xSAT_NegLit( Lits[0] ) ) )
         {
@@ -423,12 +428,12 @@ static int xSAT_SolverIsLitRemovable( xSAT_Solver_t* s, int Lit, int MinLevel )
             ABC_SWAP( int, Lits[0], Lits[1] );
         }
 
-        for (i = 1; i < c->nSize; i++)
+        for (i = 1; i < (int)c->nSize; i++)
         {
             int v = xSAT_Lit2Var( Lits[i] );
             if ( !Vec_StrEntry( s->vSeen, v ) && Vec_IntEntry( s->vLevels, v ) )
             {
-                if ( (uint32_t) 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] );
@@ -474,7 +479,7 @@ 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 ( (uint32_t) 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 );
 
@@ -483,33 +488,40 @@ static void xSAT_SolverClaMinimisation( xSAT_Solver_t * s, Vec_Int_t * vLits )
     {
         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_Watcher_t * pWatcher;
 
         s->nStamp++;
         Vec_IntForEachEntry( vLits, Lit, i )
             Vec_IntWriteEntry( s->vStamp, xSAT_Lit2Var( Lit ), s->nStamp );
 
-        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;
+        ws = xSAT_VecWatchListEntry( s->vBinWatches, FlaseLit );
+        begin = xSAT_WatchListArray( ws );
+        end   = begin + xSAT_WatchListSize( ws );
+        pWatcher;
 
-        int nb = 0;
+        nb = 0;
         for ( pWatcher = begin; pWatcher < end; pWatcher++ )
         {
             int ImpLit = pWatcher->Blocker;
 
-            if ( Vec_IntEntry( s->vStamp, xSAT_Lit2Var( ImpLit ) ) == s->nStamp && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( ImpLit ) ) == xSAT_LitSign( ImpLit ) )
+            if ( Vec_IntEntry( s->vStamp, xSAT_Lit2Var( ImpLit ) ) == (int)s->nStamp && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( ImpLit ) ) == xSAT_LitSign( ImpLit ) )
             {
                 nb++;
                 Vec_IntWriteEntry( s->vStamp, xSAT_Lit2Var( ImpLit ), s->nStamp - 1 );
             }
         }
 
-        int l = Vec_IntSize( vLits ) - 1;
+        l = Vec_IntSize( vLits ) - 1;
         if ( nb > 0 )
         {
             for ( i = 1; i < Vec_IntSize( vLits ) - nb; i++ )
-                if ( Vec_IntEntry( s->vStamp, xSAT_Lit2Var( pLits[i] ) ) != s->nStamp )
+                if ( Vec_IntEntry( s->vStamp, xSAT_Lit2Var( pLits[i] ) ) != (int)s->nStamp )
                 {
                     int TempLit = pLits[l];
                     pLits[l] = pLits[i];
@@ -533,20 +545,22 @@ static void xSAT_SolverClaMinimisation( xSAT_Solver_t * s, Vec_Int_t * vLits )
   SeeAlso     []
 
 ***********************************************************************/
-static void xSAT_SolverAnalyze( xSAT_Solver_t* s, uint32_t ConfCRef, Vec_Int_t * vLearnt, int * OutBtLevel, unsigned * nLBD )
+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 p       = LitUndef;
     int Idx     = Vec_IntSize( s->vTrail ) - 1;
     int* Lits;
+    int Lit;
     int i, j;
 
     Vec_IntPush( vLearnt, LitUndef );
     do
     {
+        xSAT_Clause_t * c;
         assert( ConfCRef != CRefUndef );
-        xSAT_Clause_t * c = xSAT_SolverReadClause(s, ConfCRef);
+        c = xSAT_SolverReadClause(s, ConfCRef);
         Lits = &( c->pData[0].Lit );
 
         if( p != LitUndef && c->nSize == 2 && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var(Lits[0])) == xSAT_LitSign( xSAT_NegLit( Lits[0] ) ) )
@@ -569,7 +583,7 @@ static void xSAT_SolverAnalyze( xSAT_Solver_t* s, uint32_t ConfCRef, Vec_Int_t *
             }
         }
 
-        for ( j = ( p == LitUndef ? 0 : 1 ); j < c->nSize; j++ )
+        for ( j = ( p == LitUndef ? 0 : 1 ); j < (int)c->nSize; j++ )
         {
             int Var = xSAT_Lit2Var( Lits[j] );
 
@@ -592,7 +606,7 @@ static void xSAT_SolverAnalyze( xSAT_Solver_t* s, uint32_t ConfCRef, Vec_Int_t *
 
         // Next clause to look at
         p = trail[Idx+1];
-        ConfCRef = (uint32_t) 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--;
 
@@ -638,7 +652,6 @@ static void xSAT_SolverAnalyze( xSAT_Solver_t* s, uint32_t ConfCRef, Vec_Int_t *
         Vec_IntClear( s->vLastDLevel );
     }
 
-    int Lit;
     Vec_IntForEachEntry( s->vTagged, Lit, i )
         Vec_StrWriteEntry( s->vSeen, xSAT_Lit2Var( Lit ), 0 );
     Vec_IntClear( s->vTagged );
@@ -655,9 +668,9 @@ static void xSAT_SolverAnalyze( xSAT_Solver_t* s, uint32_t ConfCRef, Vec_Int_t *
   SeeAlso     []
 
 ***********************************************************************/
-uint32_t xSAT_SolverPropagate( xSAT_Solver_t* s )
+unsigned xSAT_SolverPropagate( xSAT_Solver_t* s )
 {
-    uint32_t hConfl = CRefUndef;
+    unsigned hConfl = CRefUndef;
     int * Lits;
     int NegLit;
     int nProp = 0;
@@ -689,13 +702,16 @@ uint32_t xSAT_SolverPropagate( xSAT_Solver_t* s )
 
         for ( i = j = begin; i < end; )
         {
+            xSAT_Clause_t* c;
+            xSAT_Watcher_t w;
+
             if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( i->Blocker ) ) == xSAT_LitSign( i->Blocker ) )
             {
                 *j++ = *i++;
                 continue;
             }
 
-            xSAT_Clause_t* c = xSAT_SolverReadClause( s, i->CRef );
+            c = xSAT_SolverReadClause( s, i->CRef );
             Lits = &( c->pData[0].Lit );
 
             // Make sure the false literal is data[1]:
@@ -707,8 +723,9 @@ uint32_t xSAT_SolverPropagate( xSAT_Solver_t* s )
             }
             assert( Lits[1] == NegLit );
 
-            xSAT_Watcher_t w = { .CRef = i->CRef,
-                                 .Blocker = Lits[0] };
+            w.CRef = i->CRef;
+            w.Blocker = Lits[0];
+
             // If 0th watch is true, then clause is already satisfied.
             if ( Lits[0] != i->Blocker && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[0] ) ) == xSAT_LitSign( Lits[0] ) )
                 *j++ = w;
@@ -774,7 +791,7 @@ void xSAT_SolverReduceDB( xSAT_Solver_t * s )
     abctime clk = Abc_Clock();
     int nLearnedOld = Vec_IntSize( s->vLearnts );
     int i, limit;
-    uint32_t CRef;
+    unsigned CRef;
     xSAT_Clause_t * c;
     xSAT_Clause_t ** learnts_cls;
 
@@ -795,10 +812,11 @@ void xSAT_SolverReduceDB( xSAT_Solver_t * s )
     Vec_IntClear( s->vLearnts );
     for ( i = 0; i < nLearnedOld; i++ )
     {
+        unsigned CRef;
         c = learnts_cls[i];
-        uint32_t CRef = xSAT_MemCRef( s->pMemory, (uint32_t * ) c );
+        CRef = xSAT_MemCRef( s->pMemory, (unsigned * ) c );
         assert(c->fMark == 0);
-        if ( c->fCanBeDel && c->nLBD > 2 && c->nSize > 2 && (uint32_t) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( c->pData[0].Lit ) ) != CRef && ( i < limit ) )
+        if ( c->fCanBeDel && c->nLBD > 2 && c->nSize > 2 && (unsigned) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( c->pData[0].Lit ) ) != CRef && ( i < limit ) )
         {
             c->fMark = 1;
             s->Stats.nLearntLits -= c->nSize;
@@ -838,19 +856,19 @@ void xSAT_SolverReduceDB( xSAT_Solver_t * s )
 ***********************************************************************/
 char xSAT_SolverSearch( xSAT_Solver_t * s )
 {
-    ABC_INT64_T conflictC  = 0;
+    iword conflictC  = 0;
 
     s->Stats.nStarts++;
     for (;;)
     {
-        uint32_t hConfl = xSAT_SolverPropagate( s );
+        unsigned hConfl = xSAT_SolverPropagate( s );
 
         if ( hConfl != CRefUndef )
         {
             /* Conflict */
             int BacktrackLevel;
             unsigned nLBD;
-            uint32_t CRef;
+            unsigned CRef;
 
             s->Stats.nConflicts++;
             conflictC++;
@@ -859,7 +877,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 * 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 );
@@ -879,7 +897,7 @@ char xSAT_SolverSearch( xSAT_Solver_t * s )
         {
             /* No conflict */
             int NextVar;
-            if ( xSAT_BQueueIsValid( s->bqLBD ) && ( ( xSAT_BQueueAvg( s->bqLBD ) * s->Config.K ) > ( s->nSumLBD / s->Stats.nConflicts ) ) )
+            if ( xSAT_BQueueIsValid( s->bqLBD ) && ( ( (iword)xSAT_BQueueAvg( s->bqLBD ) * s->Config.K ) > ( s->nSumLBD / (iword)s->Stats.nConflicts ) ) )
             {
                 xSAT_BQueueClean( s->bqLBD );
                 xSAT_SolverCancelUntil( s, 0 );
@@ -923,17 +941,20 @@ char xSAT_SolverSearch( xSAT_Solver_t * s )
   SeeAlso     []
 
 ***********************************************************************/
-void xSAT_SolverClaRealloc( xSAT_Mem_t * pDest, xSAT_Mem_t * pSrc, uint32_t * pCRef )
+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;
+
     if ( pOldCla->fReallocd )
     {
-        *pCRef = (uint32_t) pOldCla->nSize;
+        *pCRef = (unsigned) pOldCla->nSize;
         return;
     }
 
-    uint32_t nNewCRef = xSAT_MemAppend( pDest, 3 + pOldCla->fLearnt + pOldCla->nSize );
-    xSAT_Clause_t * pNewCla = xSAT_MemClauseHand( pDest, nNewCRef );
+    nNewCRef = xSAT_MemAppend( pDest, 3 + pOldCla->fLearnt + pOldCla->nSize );
+    pNewCla = xSAT_MemClauseHand( pDest, nNewCRef );
 
     memcpy( pNewCla, pOldCla, ( 3 + pOldCla->fLearnt + pOldCla->nSize ) * 4 );
 
@@ -956,7 +977,7 @@ void xSAT_SolverClaRealloc( xSAT_Mem_t * pDest, xSAT_Mem_t * pSrc, uint32_t * pC
 void xSAT_SolverGarbageCollect( xSAT_Solver_t * s )
 {
     int i;
-    uint32_t * pArray;
+    unsigned * pArray;
     xSAT_Mem_t * pNewMemMngr = xSAT_MemAlloc(  xSAT_MemCap( s->pMemory ) - xSAT_MemWastedCap( s->pMemory ) );
 
     for ( i = 0; i < 2 * Vec_StrSize( s->vAssigns ); i++ )
@@ -977,14 +998,14 @@ void xSAT_SolverGarbageCollect( xSAT_Solver_t * s )
     }
 
     for ( i = 0; i < Vec_IntSize( s->vTrail ); i++ )
-        if ( (uint32_t) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( Vec_IntEntry( s->vTrail, i ) ) ) != CRefUndef )
+        if ( (unsigned) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( Vec_IntEntry( s->vTrail, i ) ) ) != CRefUndef )
             xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, &( Vec_IntArray( s->vReasons )[xSAT_Lit2Var( Vec_IntEntry( s->vTrail, i ) )] ) );
 
-    pArray = ( uint32_t * ) Vec_IntArray( s->vLearnts );
+    pArray = ( unsigned * ) Vec_IntArray( s->vLearnts );
     for ( i = 0; i < Vec_IntSize( s->vLearnts ); i++ )
         xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, &(pArray[i]) );
 
-    pArray = (uint32_t *) 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 a6d646c6..2bcd93b7 100644
--- a/src/sat/xsat/xsatSolver.h
+++ b/src/sat/xsat/xsatSolver.h
@@ -70,7 +70,7 @@ enum
     LitUndef = -2
 };
 
-#define CRefUndef UINT32_MAX
+#define CRefUndef 0xFFFFFFFF
 
 ////////////////////////////////////////////////////////////////////////
 ///                    STRUCTURE DEFINITIONS                         ///
@@ -81,8 +81,8 @@ struct xSAT_SolverOptions_t_
     char fVerbose;
 
     // Limits
-    ABC_INT64_T nConfLimit;    // external limit on the number of conflicts
-    ABC_INT64_T nInsLimit;     // external limit on the number of implications
+    word nConfLimit;    // external limit on the number of conflicts
+    word nInsLimit;     // external limit on the number of implications
     abctime     nRuntimeLimit; // external limit on runtime
 
     // Constants used for restart heuristic
@@ -105,13 +105,13 @@ struct xSAT_Stats_t_
     unsigned nStarts;
     unsigned nReduceDB;
 
-    ABC_INT64_T nDecisions;
-    ABC_INT64_T nPropagations;
-    ABC_INT64_T nInspects;
-    ABC_INT64_T nConflicts;
+    word nDecisions;
+    word nPropagations;
+    word nInspects;
+    word nConflicts;
 
-    ABC_INT64_T nClauseLits;
-    ABC_INT64_T nLearntLits;
+    word nClauseLits;
+    word 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()'. */
-    int64_t nPropSimplify;   /* Remaining number of propagations that must be
+    word nPropSimplify;   /* Remaining number of propagations that must be
                               * made before next execution of 'simplify()'. */
 
     /* Temporary data used by Search method */
@@ -195,16 +195,17 @@ static inline int xSAT_SolverDecisionLevel( xSAT_Solver_t * s )
     return Vec_IntSize( s->vTrailLim );
 }
 
-static inline xSAT_Clause_t * xSAT_SolverReadClause( xSAT_Solver_t * s, uint32_t h )
+static inline xSAT_Clause_t * xSAT_SolverReadClause( xSAT_Solver_t * s, unsigned h )
 {
     return xSAT_MemClauseHand( s->pMemory, h );
 }
 
 static inline int xSAT_SolverIsClauseSatisfied( xSAT_Solver_t * s, xSAT_Clause_t * pCla )
 {
+    int i;
     int * lits = &( pCla->pData[0].Lit );
 
-    for ( int i = 0; i < pCla->nSize; i++ )
+    for ( i = 0; i < (int)pCla->nSize; i++ )
         if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( lits[i] ) ) == xSAT_LitSign( ( lits[i] ) ) )
             return true;
 
@@ -232,14 +233,14 @@ static inline void xSAT_SolverPrintState( xSAT_Solver_t * s )
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DECLARATIONS                        ///
 ////////////////////////////////////////////////////////////////////////
-extern uint32_t xSAT_SolverClaNew( xSAT_Solver_t* s, Vec_Int_t * vLits, int fLearnt );
+extern unsigned xSAT_SolverClaNew( xSAT_Solver_t* s, Vec_Int_t * vLits, int fLearnt );
 extern char    xSAT_SolverSearch( xSAT_Solver_t * s );
 
 extern void xSAT_SolverGarbageCollect( xSAT_Solver_t * s );
 
-extern int xSAT_SolverEnqueue( xSAT_Solver_t* s, int Lit, uint32_t From );
+extern int xSAT_SolverEnqueue( xSAT_Solver_t* s, int Lit, unsigned From );
 extern void xSAT_SolverCancelUntil( xSAT_Solver_t* s, int Level);
-extern uint32_t xSAT_SolverPropagate( xSAT_Solver_t* s );
+extern unsigned xSAT_SolverPropagate( xSAT_Solver_t* s );
 extern void xSAT_SolverRebuildOrderHeap( xSAT_Solver_t* s );
 
 ABC_NAMESPACE_HEADER_END
diff --git a/src/sat/xsat/xsatSolverAPI.c b/src/sat/xsat/xsatSolverAPI.c
index 7ee817ee..43c2d06e 100644
--- a/src/sat/xsat/xsatSolverAPI.c
+++ b/src/sat/xsat/xsatSolverAPI.c
@@ -32,23 +32,23 @@ ABC_NAMESPACE_IMPL_START
 
 xSAT_SolverOptions_t DefaultConfig =
 {
-    .fVerbose = 1,
+    1,     //.fVerbose = 1,
 
-    .nConfLimit = 0,
-    .nInsLimit = 0,
-    .nRuntimeLimit = 0,
+    0,     //.nConfLimit = 0,
+    0,     //.nInsLimit = 0,
+    0,     //.nRuntimeLimit = 0,
 
-    .K = 0.8,
-    .R = 1.4,
-    .nFirstBlockRestart = 10000,
-    .nSizeLBDQueue = 50,
-    .nSizeTrailQueue = 5000,
+    0.8,   //.K = 0.8,
+    1.4,   //.R = 1.4,
+    10000, //.nFirstBlockRestart = 10000,
+    50,    //.nSizeLBDQueue = 50,
+    5000,  //.nSizeTrailQueue = 5000,
 
-    .nConfFirstReduce = 2000,
-    .nIncReduce = 300,
-    .nSpecialIncReduce = 1000,
+    2000,  //.nConfFirstReduce = 2000,
+    300,   //.nIncReduce = 300,
+    1000,  //.nSpecialIncReduce = 1000,
 
-    .nLBDFrozenClause = 30
+    30     //.nLBDFrozenClause = 30
 };
 
 /**Function*************************************************************
@@ -142,6 +142,7 @@ void xSAT_SolverDestroy( xSAT_Solver_t * s )
     Vec_StrFree( s->vAssigns );
     Vec_IntFree( s->vLevels );
     Vec_IntFree( s->vReasons );
+    Vec_IntFree( s->vStamp );
 
     xSAT_BQueueFree(s->bqLBD);
     xSAT_BQueueFree(s->bqTrail);
@@ -163,7 +164,7 @@ void xSAT_SolverDestroy( xSAT_Solver_t * s )
 int xSAT_SolverSimplify( xSAT_Solver_t * s )
 {
     int i, j;
-    uint32_t CRef;
+    unsigned CRef;
     assert( xSAT_SolverDecisionLevel(s) == 0 );
 
     if ( xSAT_SolverPropagate(s) != CRefUndef )
diff --git a/src/sat/xsat/xsatWatchList.h b/src/sat/xsat/xsatWatchList.h
index 454cfe44..2ba13c24 100644
--- a/src/sat/xsat/xsatWatchList.h
+++ b/src/sat/xsat/xsatWatchList.h
@@ -34,7 +34,7 @@ ABC_NAMESPACE_HEADER_START
 typedef struct xSAT_Watcher_t_ xSAT_Watcher_t;
 struct xSAT_Watcher_t_
 {
-    uint32_t CRef;
+    unsigned CRef;
     int Blocker;
 };
 
@@ -162,7 +162,7 @@ static inline xSAT_Watcher_t* xSAT_WatchListArray( xSAT_WatchList_t * v )
   SeeAlso     []
 
 ***********************************************************************/
-static inline void xSAT_WatchListRemove( xSAT_WatchList_t * v, uint32_t CRef )
+static inline void xSAT_WatchListRemove( xSAT_WatchList_t * v, unsigned CRef )
 {
     xSAT_Watcher_t* ws = xSAT_WatchListArray(v);
     int j = 0;
@@ -207,7 +207,8 @@ static inline xSAT_VecWatchList_t * xSAT_VecWatchListAlloc( int nCap )
 ***********************************************************************/
 static inline void xSAT_VecWatchListFree( xSAT_VecWatchList_t* v )
 {
-    for( int i = 0; i < v->nSize; i++ )
+    int i;
+    for( i = 0; i < v->nSize; i++ )
         xSAT_WatchListFree( v->pArray + i );
 
     ABC_FREE( v->pArray );