3 files changed, 4 insertions, 4 deletions
diff --git a/src/sat/satoko/act_clause.h b/src/sat/satoko/act_clause.h
index 5a2fda2b..2e80a1e6 100644
--- a/src/sat/satoko/act_clause.h
+++ b/src/sat/satoko/act_clause.h
@@ -26,9 +26,9 @@ static inline void clause_act_rescale(solver_t *s)
 
     vec_uint_foreach(s->learnts, cref, i) {
         clause = clause_read(s, cref);
-        clause->data[clause->size].act *= 1e-20;
+        clause->data[clause->size].act *= (float)1e-20;
     }
-    s->clause_act_inc  *= 1e-20;
+    s->clause_act_inc  *= (float)1e-20;
 }
 
 /** Increment the activity value of one clause ('clause')
diff --git a/src/sat/satoko/cnf_reader.c b/src/sat/satoko/cnf_reader.c
index 5e4b92f9..9fbbda65 100644
--- a/src/sat/satoko/cnf_reader.c
+++ b/src/sat/satoko/cnf_reader.c
@@ -97,7 +97,7 @@ static void read_clause(char **token, vec_uint_t *lits)
             break;
         sign = (var > 0);
         var = abs(var) - 1;
-        vec_uint_push_back(lits, var2lit((unsigned) var, !sign));
+        vec_uint_push_back(lits, var2lit((unsigned) var, (char)!sign));
     }
 }
 
diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c
index 8c06bbe8..a4114e54 100644
--- a/src/sat/satoko/solver.c
+++ b/src/sat/satoko/solver.c
@@ -330,7 +330,7 @@ static inline int solver_rst(solver_t *s)
 
 static inline int solver_block_rst(solver_t *s)
 {
-    return s->stats.n_conflicts > s->opts.fst_block_rst &&
+    return s->stats.n_conflicts > (int)s->opts.fst_block_rst &&
            b_queue_is_valid(s->bq_lbd) &&
            ((long)vec_uint_size(s->trail) > (s->opts.b_rst * (long)b_queue_avg(s->bq_trail)));
 }