summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--src/sat/glucose/AbcGlucose.cpp4
-rw-r--r--src/sat/glucose/Options.h8
-rw-r--r--src/sat/glucose/Vec.h2
3 files changed, 7 insertions, 7 deletions
diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp
index 026a792e..8e82e654 100644
--- a/src/sat/glucose/AbcGlucose.cpp
+++ b/src/sat/glucose/AbcGlucose.cpp
@@ -121,8 +121,8 @@ void glucose_print_stats(Solver& s, abctime clk)
{
double cpu_time = (double)(unsigned)clk / CLOCKS_PER_SEC;
double mem_used = memUsed();
- printf("c restarts : %d (%d conflicts on average)\n", (int)s.starts, s.starts > 0 ? s.conflicts/s.starts : 0);
- printf("c blocked restarts : %d (multiple: %d) \n", (int)s.nbstopsrestarts,s.nbstopsrestartssame);
+ printf("c restarts : %d (%d conflicts on average)\n", (int)s.starts, s.starts > 0 ? (int)(s.conflicts/s.starts) : 0);
+ printf("c blocked restarts : %d (multiple: %d) \n", (int)s.nbstopsrestarts, (int)s.nbstopsrestartssame);
printf("c last block at restart : %d\n", (int)s.lastblockatrestart);
printf("c nb ReduceDB : %-12d\n", (int)s.nbReduceDB);
printf("c nb removed Clauses : %-12d\n", (int)s.nbRemovedClauses);
diff --git a/src/sat/glucose/Options.h b/src/sat/glucose/Options.h
index 08e9543e..598d66d6 100644
--- a/src/sat/glucose/Options.h
+++ b/src/sat/glucose/Options.h
@@ -62,7 +62,7 @@ class Option
struct OptionLt {
bool operator()(const Option* x, const Option* y) {
int test1 = strcmp(x->category, y->category);
- return test1 < 0 || test1 == 0 && strcmp(x->type_name, y->type_name) < 0;
+ return test1 < 0 || (test1 == 0 && strcmp(x->type_name, y->type_name) < 0);
}
};
@@ -284,15 +284,15 @@ class Int64Option : public Option
if (range.begin == INT64_MIN)
fprintf(stderr, "imin");
else
- fprintf(stderr, "%4d", range.begin);
+ fprintf(stderr, "%4d", (int)range.begin);
fprintf(stderr, " .. ");
if (range.end == INT64_MAX)
fprintf(stderr, "imax");
else
- fprintf(stderr, "%4d", range.end);
+ fprintf(stderr, "%4d", (int)range.end);
- fprintf(stderr, "] (default: %d)\n", value);
+ fprintf(stderr, "] (default: %d)\n", (int)value);
if (verbose){
fprintf(stderr, "\n %s\n", description);
fprintf(stderr, "\n");
diff --git a/src/sat/glucose/Vec.h b/src/sat/glucose/Vec.h
index 8db84a03..f44c65f0 100644
--- a/src/sat/glucose/Vec.h
+++ b/src/sat/glucose/Vec.h
@@ -96,7 +96,7 @@ template<class T>
void vec<T>::capacity(int min_cap) {
if (cap >= min_cap) return;
int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2
- if (add > INT_MAX - cap || ((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM)
+ if (add > INT_MAX - cap || (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM))
throw OutOfMemoryException();
}