Merge f627fce into f2241ce

.github/actions/build/action.yml

@@ -42,8 +42,7 @@ runs:
       shell: bash
       run: |
         autoconf
-        #CFLAGS='-Werror' ${{ inputs.env }} ./configure ${{ inputs.config-opt }}
-        ${{ inputs.env }} ./configure ${{ inputs.config-opt }}
+        CFLAGS='-Werror' ${{ inputs.env }} ./configure ${{ inputs.config-opt }}
         # This is needed for yices2 to find libpoly.so.0. /usr/local/lib not searched by default?
         export LD_LIBRARY_PATH=/usr/local/lib/:${LD_LIBRARY_PATH}
         make MODE=${{ inputs.mode }}

src/mcsat/bool/clause_db.c

@@ -146,7 +146,6 @@ clause_ref_t clause_get_ref(const clause_db_t* db, const mcsat_tagged_clause_t*
 static
 bool clause_check(const mcsat_tagged_clause_t* clause, const variable_db_t* var_db, bool assert) {
   const mcsat_literal_t* lit;
-  uint32_t i;
 
   if (clause->tag.type == CLAUSE_DEFINITION) {
     if (!variable_db_is_variable(var_db, clause->tag.var, assert)) {
@@ -155,14 +154,12 @@ bool clause_check(const mcsat_tagged_clause_t* clause, const variable_db_t* var_
     }
   }
 
-  i = 0;
   lit = clause->clause.literals;
   while (*lit != mcsat_literal_null) {
     if (!variable_db_is_variable(var_db, literal_get_variable(*lit), assert)) {
       assert(!assert);
       return false;
     }
-    i ++;
     lit ++;
   }
 

src/mcsat/bv/bv_explainer.c

@@ -227,8 +227,6 @@ void bv_explainer_get_conflict(bv_explainer_t* exp, const ivector_t* conflict_in
   }
 
   if (ctx_trace_enabled(exp->ctx, "mcsat::bv::conflict::check")) {
-    static int conflict_count = 0;
-    conflict_count ++;
     bv_explainer_check_conflict(exp, conflict_out);
   }
 

src/mcsat/solver.c

@@ -2035,8 +2035,6 @@ void mcsat_analyze_conflicts(mcsat_solver_t* mcsat, uint32_t* restart_resource)
   if (trace_enabled(trace, "mcsat::conflict::check")) {
     // Don't check bool conflicts: they are implied by the formula (clauses)
     if (plugin_i != mcsat->bool_plugin_id) {
-      static int conflict_count = 0;
-      conflict_count ++;
       conflict_check(&conflict);
     }
   }

src/mcsat/weq/weak_eq_graph.c

@@ -1456,7 +1456,6 @@ void weq_graph_check_array_conflict(weq_graph_t* weq, ivector_t* conflict) {
   bool updates_present = false;
   uint32_t i;
   term_table_t* terms = weq->ctx->terms;
-  composite_term_t* t_desc = NULL;
   for (i = 0; ok && i < array_terms.size; ++i) {
     if (!eq_graph_term_has_value(weq->eq_graph, array_terms.data[i])) {
        ok = false;

src/solvers/bv/bv64_intervals.c

@@ -36,12 +36,12 @@
  */
 static inline bool add_underflow64(uint64_t a, uint64_t b, uint64_t c, uint32_t n) {
   assert(a == ((b + c) & mask64(n)));
-  return is_neg64(b, n) & is_neg64(c, n) & is_pos64(a, n);
+  return is_neg64(b, n) && is_neg64(c, n) && is_pos64(a, n);
 }
 
 static inline bool add_overflow64(uint64_t a, uint64_t b, uint64_t c, uint32_t n) {
   assert(a == ((b + c) & mask64(n)));
-  return is_pos64(b, n) & is_pos64(c, n) & is_neg64(a, n);
+  return is_pos64(b, n) && is_pos64(c, n) && is_neg64(a, n);
 }
 
 
@@ -52,12 +52,12 @@ static inline bool add_overflow64(uint64_t a, uint64_t b, uint64_t c, uint32_t n
  */
 static inline bool sub_underflow64(uint64_t a, uint64_t b, uint64_t c, uint32_t n) {
   assert(a == ((b - c) & mask64(n)));
-  return is_neg64(b, n) & is_pos64(c, n) & is_pos64(a, n);
+  return is_neg64(b, n) && is_pos64(c, n) && is_pos64(a, n);
 }
 
 static inline bool sub_overflow64(uint64_t a, uint64_t b, uint64_t c, uint32_t n) {
   assert(a == ((b - c) & mask64(n)));
-  return is_pos64(b, n) & is_neg64(c, n) & is_neg64(a, n);
+  return is_pos64(b, n) && is_neg64(c, n) && is_neg64(a, n);
 }
 
 

src/solvers/bv/bv_intervals.c

@@ -390,12 +390,12 @@ static void bv_interval_add_u_core(bv_interval_t *a, uint32_t *l, uint32_t *u, u
  */
 static inline bool add_overflow(uint32_t *a, uint32_t *b, bool sa, uint32_t n) {
   // sign bit of a0 = 0, sign bit of b = 0, sign bit of a = 1
-  return !sa & !bvconst_tst_bit(b, n-1) & bvconst_tst_bit(a, n-1);
+  return !sa && !bvconst_tst_bit(b, n-1) && bvconst_tst_bit(a, n-1);
 }
 
 static inline bool add_underflow(uint32_t *a, uint32_t *b, bool sa, uint32_t n) {
   // sign bit of a0 = 1, sign bit of b = 1, sign bit of a = 0
-  return sa & bvconst_tst_bit(b, n-1) & !bvconst_tst_bit(a, n-1);
+  return sa && bvconst_tst_bit(b, n-1) && !bvconst_tst_bit(a, n-1);
 }
 
 
@@ -482,12 +482,12 @@ static void bv_interval_sub_u_core(bv_interval_t *a, uint32_t *l, uint32_t *u, u
  */
 static inline bool sub_overflow(uint32_t *a, uint32_t *b, bool sa, uint32_t n) {
   // sign bit of a0 = 0, sign bit of b = 1, sign bit of a = 1
-  return !sa & bvconst_tst_bit(b, n-1) & bvconst_tst_bit(a, n-1);
+  return !sa && bvconst_tst_bit(b, n-1) && bvconst_tst_bit(a, n-1);
 }
 
 static inline bool sub_underflow(uint32_t *a, uint32_t *b, bool sa, uint32_t n) {
   // sign bit of a0 = 1, sign bit of b = 0, sign bit of a = 0
-  return sa & !bvconst_tst_bit(b, n-1) & !bvconst_tst_bit(a, n-1);
+  return sa && !bvconst_tst_bit(b, n-1) && !bvconst_tst_bit(a, n-1);
 }
 
 

src/solvers/cdcl/new_sat_solver.c

@@ -3827,7 +3827,7 @@ static inline bool var_is_eliminated(const sat_solver_t *solver, bvar_t x) {
  * Check whether variable x is active (i.e., not assigned at level 0) and not eliminated
  */
 static bool var_is_active(const sat_solver_t *solver, bvar_t x) {
-  return var_is_unassigned(solver, x) & ! var_is_eliminated(solver, x);
+  return var_is_unassigned(solver, x) && ! var_is_eliminated(solver, x);
 }
 
 /*

src/solvers/simplex/simplex.c

@@ -7172,7 +7172,7 @@ static void create_branch_atom(simplex_solver_t *solver, thvar_t x) {
   int32_t new_idx, lb, ub;
   literal_t l;
 
-  assert(arith_var_is_int(&solver->vtbl, x) & ! arith_var_value_is_int(&solver->vtbl, x));
+  assert(arith_var_is_int(&solver->vtbl, x) && ! arith_var_value_is_int(&solver->vtbl, x));
 
   bound = &solver->bound;
   lb = arith_var_lower_index(&solver->vtbl, x);

src/terms/power_products.c

@@ -865,13 +865,13 @@ bool pprod_equal(pprod_t *p1, pprod_t *p2) {
 
   if (p1 == p2) return true;
 
-  if (pp_is_var(p1) | pp_is_var(p2)) {
+  if (pp_is_var(p1) || pp_is_var(p2)) {
     // p1 and p2 are distinct variables
     // or only one of them is a variable
     return false;
   }
 
-  if (pp_is_empty(p1) | pp_is_empty(p2)) {
+  if (pp_is_empty(p1) || pp_is_empty(p2)) {
     // one empty and the other is not
     return false;
   }