From c3dfec7467ee4d0dab6e031a92e046729f2cff00 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 24 Jan 2017 20:49:47 -0800 Subject: Fixing windows compilation problem. --- src/sat/xsat/xsatBQueue.h | 3 ++- src/sat/xsat/xsatSolver.c | 2 +- src/sat/xsat/xsatSolver.h | 2 +- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/sat/xsat/xsatBQueue.h b/src/sat/xsat/xsatBQueue.h index 560f75c0..f75f3650 100644 --- a/src/sat/xsat/xsatBQueue.h +++ b/src/sat/xsat/xsatBQueue.h @@ -125,8 +125,9 @@ static inline void xSAT_BQueuePush( xSAT_BQueue_t * p, unsigned Value ) ***********************************************************************/ static inline int xSAT_BQueuePop( xSAT_BQueue_t * p ) { + int RetValue; assert( p->nSize >= 1 ); - int RetValue = p->pData[p->iFirst]; + RetValue = p->pData[p->iFirst]; p->nSum -= RetValue; p->iFirst = ( p->iFirst + 1 ) % p->nCap; p->nSize--; diff --git a/src/sat/xsat/xsatSolver.c b/src/sat/xsat/xsatSolver.c index 467f5f8d..9a98eec0 100644 --- a/src/sat/xsat/xsatSolver.c +++ b/src/sat/xsat/xsatSolver.c @@ -334,7 +334,7 @@ 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 ); diff --git a/src/sat/xsat/xsatSolver.h b/src/sat/xsat/xsatSolver.h index bf8bf419..36432e03 100644 --- a/src/sat/xsat/xsatSolver.h +++ b/src/sat/xsat/xsatSolver.h @@ -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 + iword nPropSimplify; /* Remaining number of propagations that must be * made before next execution of 'simplify()'. */ /* Temporary data used by Search method */ -- cgit v1.2.3