Commit 8281b56e by Alan Mishchenko

Compiler warnings.

parent 1c744cf1
...@@ -86,6 +86,7 @@ static inline int Pdr_ObjSatVar2FindOrAdd( Pdr_Man_t * p, int k, Aig_Obj_t * pOb ...@@ -86,6 +86,7 @@ static inline int Pdr_ObjSatVar2FindOrAdd( Pdr_Man_t * p, int k, Aig_Obj_t * pOb
int Lit = toLitCond( iVarNew, 1 ); int Lit = toLitCond( iVarNew, 1 );
int RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 ); int RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
assert( RetValue == 1 ); assert( RetValue == 1 );
(void) RetValue;
sat_solver_compress( pSat ); sat_solver_compress( pSat );
} }
} }
...@@ -131,6 +132,7 @@ int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj ) ...@@ -131,6 +132,7 @@ int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj )
} }
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) ); RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
assert( RetValue ); assert( RetValue );
(void) RetValue;
} }
Vec_IntFree( vLits ); Vec_IntFree( vLits );
return iVarThis; return iVarThis;
......
...@@ -546,6 +546,7 @@ static void sat_solver_record(sat_solver* s, veci* cls) ...@@ -546,6 +546,7 @@ static void sat_solver_record(sat_solver* s, veci* cls)
{ {
int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, begin, end ); int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, begin, end );
assert( RetValue ); assert( RetValue );
(void) RetValue;
} }
/////////////////////////////////// ///////////////////////////////////
/* /*
...@@ -1333,6 +1334,7 @@ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end) ...@@ -1333,6 +1334,7 @@ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
{ {
int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, begin, end ); int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, begin, end );
assert( RetValue ); assert( RetValue );
(void) RetValue;
} }
/////////////////////////////////// ///////////////////////////////////
...@@ -1522,6 +1524,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit ...@@ -1522,6 +1524,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
{ {
int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL ); int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL );
assert( RetValue ); assert( RetValue );
(void) RetValue;
} }
return l_False; return l_False;
} }
...@@ -1692,6 +1695,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit ...@@ -1692,6 +1695,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
{ {
int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL ); int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL );
assert( RetValue ); assert( RetValue );
(void) RetValue;
} }
//////////////////////////////////////////////// ////////////////////////////////////////////////
return status; return status;
......
...@@ -203,6 +203,7 @@ static void sat_solver_compress(sat_solver* s) ...@@ -203,6 +203,7 @@ static void sat_solver_compress(sat_solver* s)
{ {
int RetValue = sat_solver_simplify(s); int RetValue = sat_solver_simplify(s);
assert( RetValue != 0 ); assert( RetValue != 0 );
(void) RetValue;
} }
} }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment